conda，condi，conde，condu

Question

我在閱讀the Reasoned Schemer。

我對conde的工作原理有一些直覺。

但是，我找不到什麼conde/conda/condu/condi做的正式定義。我知道https://www.cs.indiana.edu/~webyrd/但這似乎有例子，而不是定義。

conde，conda，condi,condu是否有正式的定義？

Answer 1

在Prolog的話來說，condA是「軟切」，*->，並condU是「犯選擇」 –的once組合和柔軟的剪裁，讓(once(A) *-> B ; false)表達剪切在(A, !, B)：

A  *-> B ; C %% soft cut, condA 
once(A) *-> B ; C %% committed choice, condU 

condA，如果目標A成功，則將所有解決方案傳遞給第一個子句B，並且未嘗試替代子句C。 once/1允許其論證目標只能成功一次（只保留一個解決方案，如果有的話）。

condE是一個簡單的析取，並condI是其成分的解決方案之間交替的析取。

---

下面是在忠實地平移所述書的代碼，瓦特/輸出邏輯變量和統一，到18行的Haskell的嘗試（其中並置是咖喱功能的應用程序，:裝置缺點）。看看這個澄清的事情：

• 順序流結合（的 「mplus 」一書）：

(1) []  ++: ys = ys 
    (2) (x:xs) ++: ys = x:(xs ++: ys) 

• 交替流結合（「 mplusI」）：

(3) []  ++/ ys = ys 
    (4) (x:xs) ++/ ys = x:(ys ++/ xs) 

• 順序進料（ 「bind 」）：

(5) []  >>: g = [] 
    (6) (x:xs) >>: g = g x ++: (xs >>: g) 

• 交替進料（「 bindI」）：

(7) []  >>/ g = [] 
    (8) (x:xs) >>/ g = g x ++/ (xs >>/ g) 

• 「OR」 目標組合（ 「condE 」）：

(9) (f ||: g) x = f x ++: g x 

• 「交替OR」 目標組合（「 condI」）：

(10) (f ||/ g) x = f x ++/ g x 

• 「AND」 的目標組合（ 「all 」）：

(11) (f &&: g) x = f x >>: g 

• 「交替AND」 的目標相結合（的「 allI」 一書）：

(12) (f &&/ g) x = f x >>/ g 

• 個特殊目標

(13) true x = [x] -- a sigleton list with the same solution repackaged 
    (14) false x = [] -- an empty list, meaning the solution is rejected 

的（可能已更新）解決方案，給定（可能局部的）的解決方案的一個問題目標產品流（可能爲空）。

爲all重新編寫規則是：

(all) = true 
(all g1) = g1 
(all g1 g2 g3 ...) = (\x -> g1 x >>: (all g2 g3 ...)) 
        === g1 &&: (g2 &&: (g3 &&: ...)) 
(allI g1 g2 g3 ...) = (\x -> g1 x >>/ (allI g2 g3 ...)) 
        === g1 &&/ (g2 &&/ (g3 &&/ ...)) 

爲condX重新編寫規則是：

(condX) = false 
(condX (else g1 g2 ...)) = (all g1 g2 ...) === g1 &&: (g2 &&: (...)) 
(condX (g1 g2 ...))  = (all g1 g2 ...) === g1 &&: (g2 &&: (...)) 
(condX (g1 g2 ...) (h1 h2 ...) ...) = 
    (ifX g1 (all g2 ...) (ifX h1 (all h2 ...) (...))) 

要在最後condE和condI到達翻譯，t這裏是沒有必要實施本書的ifE和ifI，因爲它們進一步降低到簡單操作的組合，與被認爲是右關聯的所有運營商：

(condE (g1 g2 ...) (h1 h2 ...) ...) = 
    (g1 &&: g2 &&: ...) ||: (h1 &&: h2 &&: ...) ||: ... 
(condI (g1 g2 ...) (h1 h2 ...) ...) = 
    (g1 &&: g2 &&: ...) ||/ (h1 &&: h2 &&: ...) ||/ ... 

所以沒有必要對任何Haskell中特殊的「語法」，普通的運算符就足夠了。可以使用任何組合，如果需要，可以使用&&/而不是&&:。但OTOH condI也可以實現爲接受要實現的目標的集合（列表，樹等）的函數，其將使用一些智能策略來挑選它們中最可能或最需要的一個等等，而不僅僅是簡單的二元交替，如||/運營商（或ifI的書）。

其次，這本書的condA可以通過兩種新的運營商，~~>和||~，同心協力進行建模。我們可以以自然的方式使用它們，例如，

g1 ~~> g2 &&: ... ||~ h1 ~~> h2 &&: ... ||~ ... ||~ gelse 

它可以直觀地被讀作「IF g1 THEN g2 AND ... OR-ELSE IF h1 THEN ... OR-ELSE gelse」。

• 「IF-THEN」的目標組合是生產必須以失敗延續進球被稱爲「試一試」的目標：

(15) (g ~~> h) f x = case g x of [] -> f x ; ys -> ys >>: h 

• 「OR-ELSE」的目標，結合「嘗試「目標和一個簡單的目標只是簡單地將其」嘗試「目標稱爲失敗後的第二個目標，所以它只不過是用於自動分組操作數的便利語法：

(16) (g ||~ f) x = g f x 

如果||~「OR-ELSE」算符給出更低結合力比~~>「IF-THEN」運營商和製造右關聯也和~~>運營商仍然較少結合力比&&:和上面的一樣，明智的分組示例是自動製造

(g1 ~~> (g2 &&: ...)) ||~ ((h1 ~~> (h2 &&: ...)) ||~ (... ||~ gelse)...) 

在||~鏈最後目標必須因而是一個簡單的目標。真的沒有什麼限制，因爲condA的最後一個條款無論如何都是簡單的「AND」 - 它的目標組合（或簡單的false也可以使用）。

就是這樣。我們甚至可以有更多類型的嘗試，目標，通過不同種類的「IF」運營商的代表，如果我們想：一個成功的條款

• 交替使用飼料（模型能夠做什麼被稱爲condAI ，如果有一個在這本書）：

(17) (g ~~>/ h) f x = case g x of [] -> f x ; ys -> ys >>/ h 

• 使用成功的解決了信息流中只一次產生切效果，模型condU：

(18) (g ~~>! h) f x = case g x of [] -> f x ; (y:_) -> h y 

這樣，最後，condA和書的condU重新寫入規則是簡單的：

(condA (g1 g2 ...) (h1 h2 ...) ...) = 
     g1 ~~> g2 &&: ... ||~ h1 ~~> h2 &&: ... ||~ ... 

(condU (g1 g2 ...) (h1 h2 ...) ...) = 
     g1 ~~>! g2 &&: ... ||~ h1 ~~>! h2 &&: ... ||~ ... 

Answer 2

The Reasoned Schemer涵蓋了conda（soft cut）和condu（承諾選擇）。您還可以在William Byrd的優秀dissertation on miniKanren中找到他們的行爲解釋。您已將此帖標記爲關於core.logic。要明確core.logic是基於最近版本的miniKanren，而不是在The Reasoned Schemer中提出的版本。 miniKanren總是插入分離目標 - condi並且交織變體不再存在。 condeiscondi now。

Answer 3

通過實例，使用core.logic：

孔德將運行每個小組，成功，如果至少一個組成功，回報所有成功的組中的所有結果。

user> (run* [w q] 
       (conde [u#] 
         [(or* [(== w 1) (== w 2)]) 
         (== q :first)] 
         [(== q :second)])) 
([_0 :second] [1 :first] [2 :first]) 

暢達和condu：雙方將停止在第一次成功後組（從上到下）

暢達收益僅第一個成功的組中的所有結果。

user> (run* [w q] 
       (conda [u#] 
         [(or* [(== w 1) (== w 2)]) 
         (== q :first)] 
         [(== q :second)])) 
([1 :first] [2 :first]) 

condu 返回只從第一組成功只有一個結果。

user> (run* [w q] 
       (condu [u#] 
         [(or* [(== w 1) (== w 2)]) 
         (== q :first)] 
         [(== q :second)])) 
([1 :first]) 

不知道雖然condi做了什麼。