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.*->
, whereA *-> B ; C
is like(A, B ; not(A), C)
, only better ; whereascondU
is "committed choice", a combination ofonce
and a soft cut so that(once(A) *-> B ; false)
expresses(A, !, B)
(with the cut inside):(with
;
meaning "or" and,
meaning "and", i.e. disjunction and conjunction of goals, respectively).In
condA
, if the goalA
succeeds, all the solutions are passed through to the first clauseB
and no alternative clausesC
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, andcondI
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:
mplus
" of the book):Alternating stream combination ("
mplusI
"):Sequential feed ("
bind
"):Alternating feed ("
bindI
"):"
OR
" goal combination ("condE
"):"Alternating
OR
" goal combination ("condI
"):"
AND
" goal combination ("all
"):"Alternating
AND
" goal combination ("allI
" of the book):Special goals
true
andfalse
(or "success" and "failure"):And why are they called
true
andfalse
? Because for any goalg
, we have e.g.Goals produce streams (possibly empty) of (possibly updated) solutions, given a (possibly partial) solution to a problem.
Re-write rules for
all
are:Re-write rules for
condX
are:To arrive at the final
condE
andcondI
's translation, there's no need to implement the book'sifE
andifI
, since they reduce further to simple operator combinations, with all the operators considered to be right-associative: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 handcondI
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 (orifI
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.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:"
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: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 asLast goal in an
||~
chain must thus be a simple goal. That's no limitation really, since last clause ofcondA
form is equivalent anyway to simple "AND
"-combination of its goals (or simplefalse
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):use the successful solution stream only once to produce the cut effect, to model
condU
:So that, finally, the re-write rules for
condA
andcondU
of the book are simply:(*) which is:
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 forfoo = (\ x -> y )
a @@ b = y
is shorthand for(@@) a b = y
, definition of an infix operator@@
(
)
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-matchingcase
expressions).