unification

1熱度

1回答

我對Prolog完全陌生，很難理解它的統一系統。我的問題如下：我有一個約束整數，一個源數組和一個目標數組（它們都是整數數組）。我想過濾Source數組中的元素，以便其餘元素在Target數組中具有對應元素，以便Source數組中的元素與Target數組中的元素之間的差異完全是Constraint。示例：Constraint = 1，Source = [1,5,7]，Target = [2,3,

2熱度

1回答

手動派生`zipWith類型。 uncurry`

我想獲得的zipWith . uncurry zipWith . uncurry = (.) zipWith uncurry類型 - 與(a3 -> b3 -> c3)和c1與[a2] -> [b2] -> [c2]更換a1級聯作爲功能 (.) :: (b1 -> c1) -> (a1 -> b1) -> a1 -> c1 zipWith :: (a2 -> b2 -> c2) -> [a2]

0熱度

2回答

序言列表統一

我想進一步理解Prolog，以及它如何處理列表統一。所以我堅持這個例子，我知道答案，因爲我執行的代碼，但我不明白它是如何工作的。 [X,a,X,f(X,a)|Y] = [Z,Z|Y] 答案是： X=Z Z=a Y=_ L=[a,f(a,a)|Y] 我知道，頭與其他頭相結合，所以如果我做出一些改變，像這樣的： let C=[X,a,X,f(X,a)] let D=[Z,Z] 和統

0熱度

1回答

Prolog - 如何在分割變量列表時保留信息？

作爲後續問題我last question（感謝帕特里克），我有一個變量列表這樣的，這是從一個謂語to_var_list(InputList, X)一個輸出： X = [_G1426, _G1429, _G1432, 9, _G1438, _G1441]. 現在我想分裂名單按「9」，所以結果應該是這樣的： Result = [[_G1426, _G1429, _G1432],[_G1438,

0熱度

1回答

手冊推導

我不明白爲什麼q的類型是Ord t => [t] -> [a]而不是Ord a => [a] -> [a] q [] = [] q (x:xs) = q us ++ q ws where us = filter (<=x) xs ws = filter (>=x) xs 在什麼情況下輸入類型可以從輸出不同？謝謝，塞巴斯蒂安。

0熱度

1回答

爲什麼評估init的結果。削減[1,2,3]`不同於`（init。cuts）[1,2,3]`？

我試圖理解爲什麼這兩個評價：(init . cuts) [1,2,3]和init . cuts [1,2,3]是不同的，其中： cuts :: [a] -> [([a],[a])] cuts xs = zipWith splitAt [0..length xs] (repeat xs) 首先給出了我的預期結果：（[]，[1,2,3]），（[1]，[2,3]），（[1,2]，[3]）]，但是

2熱度

1回答

伊德里斯統一驚人的失敗

我試圖讓人們可以稱之爲伊德里斯的可判斷的分析器。起初我只是在分析自然數，但遇到了意想不到的問題。產生它的代碼的最小例子是這樣的： data Digit : Char -> Type where Zero : Digit '0' One : Digit '1' digitToNat : Digit a -> Nat digitToNat Zero = 0 digitToN

8熱度

1回答

與伊德里斯

類型謂詞生成運行時證明我使用此類型推理可以在其上進行可判定的解析字符串： data Every : (a -> Type) -> List a -> Type where Nil : {P : a -> Type} -> Every P [] (::) : {P : a -> Type} -> P x -> Every P xs -> Every P (x::xs) 例如，

1熱度

1回答

避免匹配（λx.x）

考慮理論 theory Scratch imports Main begin notepad begin fix P and f g h :: "int ⇒ int" assume prems: "P f" "P g" "P h" assume comp: "⋀ f g. P f ⟹ P g ⟹ P (λ x. f (g x))" have "

28熱度

2回答

是否有可能在Haskell 98中獲得無限種類的錯誤？

我正在爲一種新的函數式編程語言實現一種系統，我目前正在編寫統一兩種函數。有四種情況下，兩個考慮： +---------+---------+-------------------------------------------------------+ | k1 | k2 | action | +=========+=========+==================