unification

1熱度

2回答

我想仔細看看OCaml中的類型推斷的實現，我的OCaml似乎安裝在/usr/local/lib/ocaml裏面，但沒有.ml裏面好像包含了一段代碼類型推理。。任何人都可以幫忙嗎？

3熱度

2回答

我使用序言腳本來完成所有查詢，代碼是這樣： :- initialization(run). writeln(T) :- write(T), nl. queryAll :- forall(query(Q), (Q -> writeln('yes':Q) ; writeln('no ':Q))). run :- queryAll, ha

1熱度

3回答

約Prolog的統一

傻詳細查詢在Prolog： ?-P=[A|B], P=[1,_]. P = [1, _G1091], A = 1, B = [_G1091] B被示出爲[_G1091]表示它是一個非實例變量。但是，如果我改變一點點...... ?-P=[A|B], P=[1|_]. P = [1,B], A = 1, 突然它不是有意展示我說B的非實例但仍然是一個變量準備統一任何東西..怎麼來的？

2熱度

1回答

Prolog中的統一

這是一個關於Prolog統一過去的問題。我們應該說，如果他們統一，然後實例化。 f(a,g(b,a)) and f(X,g(Y,X)) 這統一相當= X，G（B，A）= G（Y，X）及頗爲直截了當 f(g(Y),h(c,d)) and f(X,h(W,d)) 我不認爲這一個統一，因爲克（Y ）=/X，儘管h（c，d）與h（W，d）一致。雖然X = g（Y）是否可能，因爲大寫X直到它找到解

4熱度

1回答

統一基於列表樹的算法

我需要統一算法來處理以下情況。我的表達式樹中的每個節點都有一個列表（關聯）或一組（關聯和交換）的子項。我想獲得所有可能的匹配到一個特定的模式。這裏是一個例子。讓我們假設我們正在處理的矩陣，使+是可交換*是不可交換的表達：A + B*C*D + E 或者：Add(A, Mul(B, C, D), E) 模式：X + Y*Z 我看兩場比賽 X: A + E Y: B Z: C * D X

2熱度

1回答

連接到prolog的統一跟蹤輸出

我正在嘗試調查在非類型化語言上使用自定義類型推斷語言的項目的可行性。（語言本身並不重要，但恰巧是PHP）。我的第一個想法是對此進行類型統一。我在Haskell中編寫了一些代碼，所以我知道從最終用戶的角度來看類型統一是如何工作的，但是我從未深入到算法的細節中。在這一點上，我可以解析一個PHP代碼文件，建立一組相應的規則，並且想要開始針對這些規則運行統一算法。與其重新發明車輪，我想我會使用現有的統

0熱度

1回答

廣度優先分辨算法

我想實現一個解析算法，它試圖獲得空集，因爲它解決了候選子句。我想算法來解決寬度優先的順序的候選父子句。然而，我在一個點糊塗了：令S是在知識基礎和目標條款的否定所有條款的結合，當我們試圖S中再次解決的候選人的條款與那些，我們得到S' 作爲算法的第二步，我們是否應該嘗試用S'來解析S和S'或S'？它應該如何繼續？例如; 假設知識庫+ neg。的目標集包括組子句如 P（A，B）^ Q（Z），用

0熱度

1回答

查找值

我有一組的形式pair/2的定義和謂詞propagate/3： pair(1, 2). pair(2, 3). pair(3, 4). pair(4, 5). propagate([], _, []) :- !. propagate([pair(N, Num)|Tail], Num, [N|ResultTail]) :- propagate(Tail, Num, Resul

1熱度

1回答

統合＆換人

在Haskell，我已經定義了一個多態數據類型Subst a與單個構造S :: [(String, a)] -> Subst a爲這樣： data Subst a where S :: [(String, a)] -> Subst a deriving (Show) 我想定義一個函數get::String -> Subst a -> Maybe a採用可變名字和一個取代，並

0熱度

1回答

類型錯誤在Haskell功能

我已經寫了一個Haskell功能，像這樣： shift :: Subst a -> Subst a shift (S s) = [(x, (subst s' d)) | (x,d) <- s] where s' = [(x,d) | (x,d) <- s, null (vars d)] 與數據類型，像這樣data Subst a = S [(String,a)] 我已經聲明sub