2011-01-12 10 views
23

どのようなタイプのシステムは、論理言語の目標停止を防ぐことができますか? <a href="http://www-ps.informatik.uni-kiel.de/currywiki/documentation/tutorial" rel="nofollow">curry tutorial</a>のセクション3.13.3から


狭める操作が柔軟と呼ばれ、一方、剛性と呼ばれるresiduate操作。定義されたすべての演算は柔軟性がありますが、算術演算のようなほとんどのプリミティブ演算は、推測が合理的なオプションではないため、剛性があります。

Prelude> x ++ [3,4] =:= [1,2,3,4]  where x free 
Free variables in goal: x 
Result: success 
Bindings: 
x=[1,2] ? 
:操作「++」我々は、特定の特性を満足リストを検索するために使用することができ、柔軟であるので

infixr 5 ++ 
... 
(++)    :: [a] -> [a] -> [a] 
[]  ++ ys = ys 
(x:xs) ++ ys  = x : xs ++ ys 

次のようたとえば、プレリュードは、リストの連結動作を規定します

一方、加算 "+"のような所定の算術演算は厳格である。したがって、 コールは、「+」は、論理変数と引数はヒラメするよう:

Prelude> x + 2 =:= 4 where x free 
Free variables in goal: x 
*** Goal suspended! 

カレーが中断される書き込みの目標を防ぐためには表示されません。どんなタイプのシステムが、目標が中断されるかどうか事前に検出できるか?

+5

IMOのような質問は、(おそらく、http://cstheory.stackexchange.comの)型システムの専門家や(彼らのメーリングリストの)カレーの専門家によって早く答えられます。 –

答えて

3

説明したことは、モードチェックのように聞こえます。モードチェックは、一般に、特定の入力セットに対してどの出力が利用できるかをチェックします。あなたはモードのチェックを非常に真剣に受け入れる言語Mercuryをチェックしたいかもしれません。

関連する問題