康达，康迪，康德，康德 [英] conda, condi, conde, condu

查看：16 发布时间：2022/1/2 22:28:43 clojure scheme clojure-core.logic minikanren reasoned-schemer

本文介绍了康达，康迪，康德，康德的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

我正在阅读The Reasoned Schemer.

我对 conde 的工作原理有一些直觉.

然而，我找不到什么conde/conda/condu/condi的正式定义做.

我知道 https://www.cs.indiana.edu/~webyrd/ 但似乎有例子而不是定义.

有没有conde、conda、condi、condu的正式定义?

解决方案

在 Prolog 中，

condA 是软剪辑" 又名 *->，其中 A *->乙;C 就像(A, B ; not(A), C)，只是更好 ;而
condU 是承诺的选择"，once 和软剪辑的组合所以 (once(A) *-> B ; false) 表示 (A, !, B) (里面有 cut ):

condA: A *->乙;C % 软切，% (A , B ; 不是(A) , C)条件:一次(A)*->乙;C % 承诺的选择，% (A , !, B ; not(A) , C)

(with ; 表示或" 和 , 表示和"，即分别是目标的分离和连接).

在condA中，如果目标A成功，则所有的解都传递给第一个子句B 并且没有尝试替代子句 C.

在 condU 中，once/1 允许其参数目标仅成功一次(仅保留一个解决方案，如果有).

condE 是连词的简单分离，condI 是交替在其组成部分的解决方案之间，交错其流.

这是将本书的代码忠实地翻译成 18 行 Haskell 的尝试，它主要是一个懒惰的 Lisp 语法.⁽*⁾ 看看这是否说明问题:

顺序流组合(本书的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=fx>>/g
```

特殊目标

 (13) true x = [x] -- 重新打包相同解的单例列表(14) false x = [] -- 一个空列表，表示该解被拒绝

目标产生(可能是更新的)解决方案的流(可能是空的)，给定一个(可能是部分)问题的解决方案.

all 的重写规则是:

(all) = true(所有 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 (所有 h2 ...) (...) ))

要获得最终的condE 和condI 的翻译，无需执行本书的ifE 和 ifI，因为它们进一步简化为简单的运算符组合，所有运算符都被认为是 右结合:

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

所以不需要任何特殊的语法"；在 Haskell 中，普通的二进制中缀运算符就足够了.任何组合都可以在任何地方使用，根据需要使用 &&/ 而不是 &&:.但另一方面 condI 也可以实现为一个函数来接受要实现的目标集合(列表、树等)，这将使用一些智能策略选择一个最有可能或最需要的等等，而不仅仅是像 ||/ 运算符(或 ifI书).

接下来，这本书的condA可以用两个新运算符建模，~~>和<代码>||~，一起工作.我们可以以自然的方式使用它们，例如

g1 ~~>g2 &&: ... ||~ h1 ~~>h2 &&: ... ||~ ... ||~ 凝胶

可以直观地读作IF g1 THEN g2 AND ... OR-ELSE IF h1 THEN ... OR-ELSE gelse":

"IF-THEN"目标组合是产生一个 try" 目标，该目标必须使用失败继续目标来调用:
```
 (15) (g ~~> h) f x = case g x of [] ->f x ;是->y >>: h
```
"OR-ELSE"try 目标和简单目标的目标组合只是简单地调用它的 try 目标和第二个失败时目标，因此它只不过是一种用于自动分组的便捷语法操作数:
```
 (16) (g ||~ f) x = g f x
```

使用OR-ELSE"||~ 运算符比IF-THEN"具有更少的约束力；~~> 操作符也做了右结合，而且 ~~> 操作符比 && 的约束力还小:等等，上面例子的合理分组自动产生为

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

||~ 链中的最后一个目标因此必须是一个简单的目标.这真的没有限制，因为 condA 形式的最后一个子句无论如何等价于简单的AND"-其目标的组合(或简单的false 也可以使用.

仅此而已.我们甚至可以有更多类型的try目标，由不同类型的IF"表示.运营商，如果我们想要:

在成功的子句中使用交替提要(模拟可能被称为 condAI 的内容，如果书中有的话):
```
 (17) (g ~~>/h) f x = case g x of [] ->f x ;是->y >>/h
```
只使用成功的解决方案流一次产生cut效果，对condU进行建模:
```
 (18) (g ~~>! h) f x = case g x of [] ->f x ;(y:_) ->嗨
```

所以，最后，本书condA和condU的重写规则很简单:

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

⁽*⁾ 即:

简单的并列就是柯里化函数应用，
f a b c === (((f a) b) c) === f(a, b, c)
( a -> b ) 是 lambda 函数， (lambda (a) b)
foo x = y 是 foo = ( x -> y )
a @@ b = y 是(@@) ab = y 的简写，中缀运算符的定义@@
括号( ) 只是为了分组
[] 是空列表，and
: 的意思是 cons -- 两者都是构造函数(lazy，因为整个语言都是lazy，即根据需要调用)，在定义中=的右边；并作为解构模式，在 left 上(或在模式匹配的 case 表达式中).

I'm reading the Reasoned Schemer.

I have some intuition about how conde works.

However, I can't find a formal definition of what conde/conda/condu/condi do.

I'm aware of https://www.cs.indiana.edu/~webyrd/ but that seems to have examples rather than definitions.

Is there a formal definition of conde, conda, condi, condu somewhere?

解决方案

In Prolog's terms,

condA is "soft cut" a.k.a. *->, where A *-> B ; C is like (A, B ; not(A), C), only better ; whereas
condU is "committed choice", a combination of once and a soft cut so that (once(A) *-> B ; false) expresses (A, !, B) (with the cut inside):

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

(with ; meaning "or" and , meaning "and", i.e. disjunction and conjunction of goals, respectively).

In condA, if the goal A succeeds, all the solutions are passed through to the first clause B and no alternative clauses C are tried.

In condU, once/1 allows its argument goal to succeed only once (keeps only one solution, if any).

condE is a simple disjunction of conjunctions, and condI is a disjunction which alternates between the solutions of its constituents, interleaving the streams thereof.

Here's an attempt at faithfully translating the book's code, w/out the logical variables and unification, into 18 lines of Haskell which is mostly a lazy Lisp with syntax.⁽*⁾ See if this clarifies things:

Sequential stream combination ("mplus" of the book):

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

Alternating stream combination ("mplusI"):

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

Sequential feed ("bind"):

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

Alternating feed ("bindI"):

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

"OR" goal combination ("condE"):
```
  (9)   (f ||: g) x  =  f x ++: g x
```
"Alternating OR" goal combination ("condI"):
```
  (10)  (f ||/ g) x  =  f x ++/ g x
```
"AND" goal combination ("all"):
```
  (11)  (f &&: g) x  =  f x >>: g
```
"Alternating AND" goal combination ("allI" of the book):
```
  (12)  (f &&/ g) x  =  f x >>/ g
```

Special goals

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

Goals produce streams (possibly empty) of (possibly updated) solutions, given a (possibly partial) solution to a problem.

Re-write rules for all are:

(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 &&/ ... ))

Re-write rules for condX are:

(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 ...) (...) ))

To arrive at the final condE and condI's translation, there's no need to implement the book's ifE and ifI, since they reduce further to simple operator combinations, with all the operators considered to be right-associative:

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

So there's no need for any special "syntax" in Haskell, plain binary infix operators suffice. Any combination can be used anywhere, with &&/ instead of &&: as needed. But on the other hand condI could also be implemented as a function to accept a collection (list, tree etc.) of goals to be fulfilled, that would use some smart strategy to pick of them one most likely or most needed etc, and not just simple binary alternation as in ||/ operator (or ifI of the book).

Next, the book's condA can be modeled by two new operators, ~~> and ||~, working together. We can use them in a natural way as in e.g.

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

which can intuitively be read as "IF g1 THEN g2 AND ... OR-ELSE IF h1 THEN ... OR-ELSE gelse":

"IF-THEN" goal combination is to produce a "try" goal which must be called with a failure-continuation goal:
```
  (15)  (g ~~> h) f x  =  case g x of [] -> f x  ;  ys -> ys >>: h
```
"OR-ELSE" goal combination of a try goal and a simple goal simply calls its try goal with a second, on-failure goal, so it's nothing more than a convenience syntax for automatic grouping of operands:
```
  (16)  (g ||~ f) x  =  g f x
```

With the "OR-ELSE" ||~ operator given less binding power than the "IF-THEN" ~~> operator and made right-associative too, and ~~> operator having still less binding power than &&: and the like, sensible grouping of the above example is automatically produced as

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

Last goal in an ||~ chain must thus be a simple goal. That's no limitation really, since last clause of condA form is equivalent anyway to simple "AND"-combination of its goals (or simple false can be used just as well).

That's all. We can even have more types of try goals, represented by different kinds of "IF" operators, if we want:

use alternating feed in a successful clause (to model what could've been called condAI, if there were one in the book):
```
  (17)  (g ~~>/ h) f x  =  case g x of [] -> f x  ;  ys -> ys >>/ h
```
use the successful solution stream only once to produce the cut effect, to model condU:
```
  (18)  (g ~~>! h) f x  =  case g x of [] -> f x  ;  (y:_) -> h y
```

So that, finally, the re-write rules for condA and condU of the book are simply:

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

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

⁽*⁾ which is:

simple juxtaposition is curried function application,
f a b c =~= (((f a) b) c) =~= f(a, b, c)
( a -> b ) is lambda function, (lambda (a) b)
foo x = y is shortcut for foo = ( x -> y )
a @@ b = y is shortcut for (@@) a b = y, definition of an infix operator @@
parentheses ( ) are just for grouping
[] is the empty list, and
: means cons -- both as a constructor ( lazy, as the whole language is lazy, i.e. call by need ), on the right of = in definitions; and as a destructuring pattern, on the left (or in pattern-matching case expressions).

这篇关于康达，康迪，康德，康德的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！

查看全文

康达，康迪，康德，康德 [英] conda, condi, conde, condu

问题描述

相关文章

其他开发最新文章

热门教程

热门工具

登录关闭

康达，康迪，康德，康德 [英] conda, condi, conde, condu

问题描述

相关文章

其他开发最新文章

热门教程

热门工具

登录 关闭

登录关闭