23

カレーチュートリアルのセクション3.13.3から:


残存する操作は 剛体 と呼ばれ、縮小する操作は 柔軟 と呼ばれます。定義されたすべての演算は柔軟ですが、算術演算などのほとんどのプリミティブ演算は、推測が合理的なオプションではないため、厳密です。たとえば、プレリュードでは、リスト連結操作を次のように定義しています。

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

操作「++」は柔軟であるため、特定のプロパティを満たすリストを検索するために使用できます。

Prelude> x ++ [3,4] =:= [1,2,3,4]       where x free
Free variables in goal: x
Result: success
Bindings:
x=[1,2] ?

一方、加算「+」などの事前定義された算術演算は厳格です。したがって、論理変数を引数として「+」を呼び出すと、次のように失敗します。

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

カリーは、中断されるゴールを書くことを警戒しているようには見えない. 目標が中断されるかどうかを事前に検出できるのは、どのタイプのシステムですか?

4

1 に答える 1

3

あなたが説明したことは、モードチェックのように聞こえます。これは、一般に、特定の入力セットに対してどの出力が使用可能になるかをチェックします。モードチェックを非常に真剣に行う言語 Mercury をチェックすることをお勧めします。

于 2011-04-10T09:19:24.930 に答える