問題タブ [unification]

これが失敗する理由を誰か教えてください。

X は最初に a にインスタンス化され、次に削除され、次に b に変換され、X = b になるというのが私の仮定でした。試してみると、間違っていることがわかりますが、その理由はわかりません。

ありがとうございました。

試験のためにPrologを学習しようとしています。

私のスライドによると、算術式は定数と統一されていません。理由はありますか？

例えば

は0と一体化しません(X-1)。

だから私の質問は次のとおりです。定数と算術式の間に統一があった場合、場合によっては問題になりますか?

次のタイプの理由を理解しようとしています。

(flip .) is: (a -> a1 -> b -> c) -> a -> b -> a1 -> c

まず、次のタイプです。

flip: is (a -> b -> c) -> b -> a -> c (.): is (b -> c) -> (a -> b) -> a -> c

変数の名前を変更して、説明をより明確にするため、型は次のようになります。

flip: is (ax -> bx -> cx) -> bx -> ax -> cx (.): is (by -> cy) -> (ay -> by) -> ay -> cy

次に、次のように置き換えてみます。

ax = (by -> cy) bx = (ay -> by) cx = ay -> cy

したがって、結果の型は (ay -> by) (by -> cy) -> ay -> cy となり、正しい結果とは異なります。

何か助けはありますか？

ありがとう、セバスチャン。

fun g x = ys where ys = [x] ++ filter (curry g x) ysの型が である理由を理解しようとしてい((a, a) -> Bool) -> a -> [a]ます。

という事は承知しています：

filter :: (a -> Bool) -> [a] -> [a]そしてそれcurry :: ((a, b) -> c) -> a -> b -> c

しかし、私は続行する方法を理解していません。

次のタイプを手動で派生させたい:

f1 x xs = (filter . (<)) x xs

を初めて見xたので、次のようになります。

次に(<)、このタイプがあります：

(< x)次のタイプを統合できる場合にのみ言えます。

それで

そう

フィルタにはこのタイプがあります

xs を見るのは初めてなので、

(filter . (<)) x xs次のタイプを統合できる場合にのみ言えます。

したがって、正しいタイプが（GHCiに尋ねる）の場合f1 :: (a2 -> Bool) -> [a2] -> [a2]、 と同じタイプのが得られます。filterOrd a => a -> [a] -> [a]

何か助けはありますか？

((.) folderr) のタイプを手動で派生させようとしています

それで：

私が得るタイプを一致させる：

しかし、その後、この表現を減らす方法について混乱します。

何か助けはありますか？

ありがとう、
セバスチャン。

(foldr (.)) のタイプを手動で派生させようとしています

それで：

だから私はそれを得る(foldr (.)) :: (a2 -> b2) -> [(b2 -> c2)] -> (a2 -> b2)

しかし、GHCi は次のように返します。:t (foldr (.)) :: (a -> b) -> [b -> b] -> a -> b

なぜ b2 と c2 は同じですか?

ありがとう、
セバスチャン。