Conda，Condi，Conde，conduit [英] conda, condi, conde, condu
问题描述
我正在阅读推理的Schemer 。
我有一些关于 conde 如何工作的直觉。
，我找不到一个正式的定义 conde / conda / condu / condi do。
我知道https://www.cs.indiana.edu/~webyrd/ ，但这似乎有例子而不是定义。
是否有 conde ， conda ，
在Prolog中， condA 是软切， * - 是 一次和软裁剪的组合，使得（once（A）* - > B; false）表示（A，！，B）中的 cut ：
A * - > B; C %%软切，condA
一次（A）* - > B; C %%承诺选择，condU
在 condA ，如果目标 A 成功，所有解决方案都会传递到第一个子句 B 并且没有尝试任何替代子句 C 。 once / 1 允许其参数目标仅成功一次（只保留一个解决方案，如果有）。
strong> condE 是一个简单的断点， condI
这里尝试忠实地翻译这本书的代码，w / out逻辑变量和统一，分成18行Haskell（其中并置是curried函数应用程序，：表示 cons ）。看看这是否澄清了一些问题：
- 顺序流组合（
mplus）：
1）[] ++：ys = ys
（2）（x：xs）++：ys = x：（xs ++：ys）
- 交替流组合（
mplusI） ：
（3）[] ++ / ys = ys
（4）（x：xs）++ / ys = x :( ys ++ / xs）
b $ b
- 顺序Feed（
bind）：
（5）[]>> ;: g = []
）（x：xs）> ;:g = gx ++：（xs>> ;:g）
- 替换Feed（
bindI）：
（7）[]> （x：xs）> / g = gx ++ /（xs> / g）
$ b b
或目标组合（condE）：
（9）（f ||：g）x = fx ++：gx
- $ b b
- 替换
OR目标组合（condI）：
（10）（f || / g）x = fx ++ / gx
AND目标组合（all）：
（11）（f&& ;:g）x = fx> ;:g
- 替换
AND（allI）：
< pre class =lang-none prettyprint-override>
（12）（f&& / g）x = fx> / g
- 特殊目标
（13）true x = [x] - 重新打包相同解决方案的sigleton列表
（14）false x = []空列表，表示解决方案被拒绝
目标
重新编写 所有
（all）= true
（all g1）= g1
（all g1 g2 g3 ...）=（\x-> g1 x>> ;:（g2 g3 ...））
=== g1&& ;:（g2& $ b（allI g1 g2 g3 ...）=（\x-> g1 x> /（allI g2 g3 ...））
=== g1&& / &&&&&&&&&&（/>>&&...;）...
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 ...）...）=pre>
（g1& ;:g2&& ;: ...）||：（h1& ;:h2 &&：...）||：...
（cond1（g1 g2 ...）（h1 h2 ...）...）=
（g1& ：g2&& ;: ...）|| /（h1& ;:h2&& ;: ...）|| / ...
所以在Haskell中没有任何特殊的语法，普通运算符就足够了。可以使用任何组合，如果需要，可以使用
&& / amp; /，而不是&&：。但是OTOHcondI也可以实现为接受要实现的目标的集合（列表，树等）的函数，一些聪明的策略选择他们最有可能或最需要的，而不只是简单的二进制交替如|| /运算符（或
接下来，书的
condA 可以通过两个新运算符〜<>和||〜， 一起工作。我们可以像例中那样以自然的方式使用它们。g1〜 g2&& ;: ... ||〜h1〜 h2& ;: ... ... ||〜... ||〜gelse
直观地读为
IF g1 THEN g2 AND ... OR-ELSE IF h1 THEN ... OR-ELSE gelse。
IF-THEN目标组合是为了产生一个try目标，目标：
（15）（g〜〜> h）fx = []的情况gx> f x; ys - > ys>> ;: h
OR-ELSE目标组合的尝试目标和一个简单的目标简单地称为其尝试目标与第二个，失败的目标，所以它只是一个方便的语法自动分组的操作数：
（16） f）x = gfx
如果 ||〜 OR-ELSE 绑定能力小于 ~~> IF-THEN 运算符，并且也成为右关联，并且 ~~> 运算符的绑定力仍小于&&：等，上述示例的合理分组自动生成为
（g1〜〜>（g2&& ;: ...））||〜 |〜（... ||〜gelse）...）
c $ c> ||〜链必须是一个简单的目标。这没有什么限制，因为 condA 表格的最后一个子句等同于简单的 AND - 其目标的组合（或简单 false 也可以使用）。
我们甚至可以有更多类型的尝试目标，由不同种类的 IF 运算符表示，如果我们想：
- 在成功的子句中使用替代Feed（以模拟可能被称为
condAI是本书中的一个）：
g - / h）fx = []的情况gx。 f x; ys - > ys> / h
- em>一次以产生 cut 效果，以模型
condU：
（18）（g〜〜>！h）fx = case gx [] - > f x; （y：_） - > hy
最后，重写 condA 和 condU 简单：
（condA（g1 g2 ...）（h1 h2 ...）...）=
g1〜 ; g2&& ;: ... ||〜h1〜 h2& ;: ... ... ||〜...
（condU（g1 g2 ...）（h1 h2 ...）...）=
g1〜 〜>！ g2&& ;: ... ||〜h1〜〜>！ h2&& ;: ... ||〜...
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", *->, and condU is "committed choice" – a combination of once and a soft cut, so that (once(A) *-> B ; false) expresses the cut in (A, !, B):
A *-> B ; C %% soft cut, condA
once(A) *-> B ; C %% committed choice, condU
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. once/1 allows its argument goal to succeed only once (keeps only one solution, if any).
condE is a simple disjunction, and condI is a disjunction which alternates between the solutions of its constituents.
Here's an attempt at faithfully translating the book's code, w/out logical variables and unification, into 18 lines of Haskell (where juxtaposition is curried function application, and : means cons). 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 operators suffice. Any combination can be used, with &&/ instead of &&: if needed. But OTOH 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
If the ||~ "OR-ELSE" operator is given less binding power than the ~~> "IF-THEN" operator and made right-associative too, and ~~> operator has 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 &&: ... ||~ ...
这篇关于Conda，Condi，Conde，conduit的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
