conda, condi, conde, condu

Asked 1/6, 2012 at 2:8 Answered 12/4, 2019 at 14:48

Solved clojure scheme clojure-core.logic minikanren reasoned-schemer

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?

Threecolor answered 1/6, 2012 at 2:8 Comment(0)

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 true and false (or "success" and "failure"):

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

And why are they called true and false? Because for any goal g, we have e.g.

  (g &&: true) x  =  g x >>: true  =  g x >>: (\ x -> [x] )  =  g x
  (false &&: g) x  =  false x >>: g  =  [] >>: g  =  []  =  false x
  -- ... etc.

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 shorthand for foo = (\ x -> y )
a @@ b = y is shorthand 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).

Stereophonic answered 1/6, 2012 at 10:51 Comment(3)

5 uparrows on stack overflow is not worthy of this response. I hope you turn this into a blog post or something. – Threecolor 1/6, 2012 at 20:13

As a followup: is COND? == OR? and ALL? == AND? ? – Threecolor 1/6, 2012 at 23:23

@Threecolor more or less. CONDe is Prolog's OR (disjunction), and ALL - Prolog's AND (conjunction). CONDi, ALLi, are a variation on sub-goals solutions merging order, trying to build-in the prevention of non-productive behaviour into the system in advance. – Stereophonic 2/6, 2012 at 9:56

The Reasoned Schemer covers conda (soft cut) and condu (committed choice). You'll also find explanations of their behavior in William Byrd's excellent dissertation on miniKanren. You've tagged this post as being about core.logic. To be clear core.logic is based on a more recent version of miniKanren than the one presented in The Reasoned Schemer. miniKanren is always interleaves disjunctive goals - condi and the interleaving variants no longer exist. conde is condi now.

Judejudea answered 1/6, 2012 at 12:34 Comment(1)

FWIW to people reading today, the second edition of The Reasoned Schemer now uses an interleaving conde by default. – Backstretch 17/2, 2020 at 19:59

By Example, using core.logic:

conde will run every group, succeed if at least one group succeeds, and return all results from all successful groups.

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

conda and condu: both will stop after the first successful group(top to bottom)

conda returns all results from only the first successful group.

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

condu returns only one result from only the first successful group.

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

No idea what condi does though.

Tonjatonjes answered 31/12, 2016 at 18:8 Comment(3)

Not a formal definition but it might help – Tonjatonjes 31/12, 2016 at 18:12

as dnolen writes in his answer here, conde of core.logic is condi of the book. conde of the book processes its subgoals in order, sequentially. if first successive subgoal produced an infinite stream of answers, no other successful subgoals' solutions would show up in the combined solutions stream. condi of the book remedied that by interleaving the streams. – Stereophonic 13/2, 2017 at 6:40

awesome! now i know. didnt catch the stream/interleaving part back when. revisiting core.logic src as of now – Tonjatonjes 26/2, 2017 at 1:35

According to the ISO Prolog core standard control structures such as (,)/2, (;)/2 and (->)/2 are cut transparent. (*->)/2 is not found in the ISO Prolog core standard, but usually Prolog systems implement it also cut transparent.

This means one cannot translate:

once(A) *-> B;C

Into A, !, B; C. Because the later might be embedded in other control structures, and if there are disjunctions among them, these choice points would be also cut away. What on the other hand seems reasonable, to view it as A -> B; C,

known simply as ISO Prolog core standard if-then-else. The thus defined behaviour of the cut, is for example useful to break out of repeat loops, without throwing an exception. The usual programming pattern is more difficult to archive with if-then-else.

Radiograph answered 12/4, 2019 at 14:48 Comment(3)

you probably meant some goal like (X=1;X=2),(Y=1,!,Z=1 ; Z=2) producing just one result, whereas both (X=1;X=2),(Y=1 -> Z=1 ; Z=2) and (X=1;X=2),(once(Y=1) *-> Z=1 ; Z=2) producing two? but the book doesn't have ! or -> in the first place. all it has is these stream manipulations. – Stereophonic 15/4, 2019 at 5:20

thanks for the link. my answer is not about the Prolog translation though. the Haskell code in it is a translation of the Scheme code from the book. and since there's no cut in the book's language, I think the two Prolog snippets are also a correct translation of conda and condu into Prolog (even though it wasn't at all the goal of the answer; just an illustration). cascading the *-> shouldn't be a problem, right? even in Prolog this is about the parenthesization issues, which can always be fixed / made explicit by defining auxiliary predicates instead, to prevent the cut leakage. – Stereophonic 15/4, 2019 at 8:10

(I assume very few of the book readers / minikanren users / know Prolog, relatively speaking ... even Haskell was an edgy choice back then, but it has become more popular with the years, and the code is so simple, it's basically a pseudocode). – Stereophonic 15/4, 2019 at 8:14

Recommended topics

Hot tags