Continuations Made Simple (hopefully) and Illustrated

[Tim Peters]

[Denys Duchier, posts a Python propositional tautology checker
 using Continuation Passing Style;
 Tim posts a variant in "straight Python", then sez...
]

> People are invited to play with both and do the "compare &
> contrast" bit for themselves <wink>.  I don't think either
> version is a pure win on all counts, but the CPS version
> certainly has attractions!

Here's one very special attraction of the CPS version:  it works <0.1 wink>.
The thing I posted was simply a greedy recursive search.  So "the first"
assignment of values to vars "that works" is taken at each level of the
expression, and if a successful assignment to one subexpression X is such
that a later subexpression Y fails, there's no backtracking to try a
different set of assignments in X (that may allow Y to succeed too).

An example is the expression:

   OR(AND(P, NOT(P)), NOT(P)).isValid()

Falsifying that requires falsifying both AND(P, NOT(P)) and NOT(P).
Falsifying AND(P, NOT(P)) requires falisfying either P or NOT(P).  My
program falsifies P (i.e., sets P to 0), then goes back up to the top
expression, and sees that it's impossible to falsify NOT(P) when P is 0.  It
therefore reports that the whole expression can't be falsfied (i.e., is
valid).

That's incorrect.  When it failed to falsify NOT(p), it *should* backtrack
to AND(P, NOT(P)) and try falsifying the NOT(P) half of that instead.  Then
it would set P to 1, and go on to discover that P=1 also falsifies the RHS
of the original expression too, so that P=1 falsifies the entire expression.

So my version failed to capture the most important feature of the CPS
version -- keep that in mind when you "compare & contrast" <wink>.

chastenedly y'rs  - tim