conda,condi,conde,condu

Question

我正在阅读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(其中并置是curried函数应用,并且:意味着缺点).看看这是否澄清了事情:

• 顺序流组合(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的翻译,就没有必要执行书的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

Reasoned Schemer涵盖conda(软切)和导管(承诺选择).你也可以在William Byrd 关于miniKanren的优秀论文中找到他们行为的解释.你已经将这篇文章标记为关于core.logic.要明确core.logic是基于最新版本的miniKanren而不是The Reasoned Schemer中提供的版本.miniKanren总是交错析取的目标- 康迪和交织变种不再存在.康德 现在是 康迪.