Continuations Made Simple (hopefully) and Illustrated

[Tim Peters]

[Denys Duchier, with a nice exposition on CPS (Continuation Passing
 Style), and some wonderfully clumsy <wink> Python code using it]

Thanks, Denys -- this was fun!  Just a few comments:

> ...
> You can write continuation passing programs in Python, or in any
> language that supports some form of closures and automated garbage
> collection.

Except that Python doesn't optimize tail calls:  the stack keeps growing.
This limits the value of the approach for "real work" in Python.

> The application that I know best concerns `search'.  This is very
> much related to the on-going thread on iterators.  I learned the
> technique, which I describe below, from my erstwhile advisor Drew
> McDermott, many years ago.  This is an old AI technique which Drew
> called "generators".  However, I should like to point out that,
> contrary to Tim's characterization, generators (in Drew's sense)
> do not necessarily behave in a `stack-like manner'; although it
> is extremely rare to come up with one that doesn't :-)

I should always (and 75% of the time do <wink>) qualify my use of
"generators" with "as in the Icon language", whose generators are strictly
stack-like.  This restriction makes them especially easy to implement.

Demo/threads/Generator.py (in the Python source distribution) implements a
more general flavor of generator that need not be stack-like.

I've rarely needed the full power of the latter, although they allow an odd
efficiency trick:  in the Icon flavor of generator, a recursive generator
nested (say) 1000 levels deep that produces "a result" has to pass it all
the way up 1000 levels of call chain to get it back to its ultimate
consumer, then "resume back down" 1000 levels to get the next result.  The
Generator.py in the distribution is more coroutine-like, and allows to pass
the result directly to the consumer.  OTOH, Generator.py builds on native OS
threads, which for normal (shallow) usage is much less efficient than a
straight implementation without threads.

> ...
> class Baz:
>   def __init__(self,foo1,foo2):
>     self.one = foo1
>     self.two = foo2
>   def search(self,info,yes,no):
>     return self.one.search(
>       info,yes,
>       lambda self=self,info=info,yes=yes,no=no: \
>       self.two.search(info,yes,no))
>
> What becomes evident in the above is that Python's lack of real
> closures makes it a bit painful to write what in a functional language
> is truly succinct and elegant.

OTOH, a true functional language's lack of mutable state makes it a bit
painful to write object-based code that in Python is truly succinct and
elegant.  Python simply wasn't designed for the style of code above, and
Guido is remarkably unapologetic for that <wink>.

> 3. CHECKING THE VALIDITY OF PROPOSITIONAL FORMULAE

[and some really cool CPS-in-Python code that implements a tautology
 checker; see the original post, or
   http://www.ps.uni-sb.de/~duchier/python/validity.py
]

This is a good opportunity to contrast styles.  The first thing that struck
me while playing with the code is that, when a formula is not valid, I want
to see a set of bindings that demonstrates that.  It's cool that it can be
done with a one-token change:

      lambda alist,no:     1,
to
      lambda alist,no: alist,

I was delighted to see that, since my years'-old "real experience" with CPS
tricks left me wary of getting anything to work right again after changes in
problem requirements <0.5 wink>.

I'll attach a fairly idiomatic Python version, a drop-in replacement for
your Formula class tree, but where satisfy and falsify return witnessing
bindings when they succeed.  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!

One subtlety is that the code below is very easy to change to make
Conjunction and Disjunction work directly with an arbitrary # of conjunctees
etc.  This is clumsier in CPS, which is why Denys wrote a front end to
compile n-ary AND and OR into nested binary operators <wink>.

leaving-it-to-chris-to-write-the-continuation-variant-ly y'rs  - tim


# A gross modification of code that contained this copyright notice:
# Copyright (c) Feb 2000, by Denys Duchier, Universitaet des Saarlandes

class Formula:
    def isValid(self):
        """a formula is valid iff it cannot be falsified"""
        success, alist = self.falsify({})
        if success:
            print self, "can be falsified:\n", alist
        else:
            print self, "is valid"
    # satisfy and falsify are wrappers that allow tracing.
    # _satisfy and _falsify do the actual work.
    # satisfy attempts to find some binding of variables such that
    # the formula is true; falsify to find some binding such that
    # the formula is false.  They return the two-tuple
    #    success, bindings
    # where success is 1 if successful (else 0); and, if 1, bindings
    # is a set of witnessing bindings (if success is 0, bindings is
    # meaningless).
    tracing = 0
    def satisfy(self, alist):
        if Formula.tracing:
            print "satisfy", self, "alist=", alist
        return self._satisfy(alist)
    def falsify(self, alist):
        if Formula.tracing:
            print "falsify", self, "alist=", alist
        return self._falsify(alist)

class Conjunction(Formula):
    def __init__(self,p,q):
        self.p = p
        self.q = q
    def __str__(self):
        return '('+str(self.p)+' & '+str(self.q)+')'
    def _satisfy(self, alist):
        success, alist = self.p.satisfy(alist)
        if success:
            success, alist = self.q.satisfy(alist)
            if success:
                return 1, alist
        return 0, ()
    def _falsify(self, alist):
        for child in self.p, self.q:
            success, alist2 = child.falsify(alist)
            if success:
                return 1, alist2
        return 0, {}

class Disjunction(Formula):
    def __init__(self,p,q):
        self.p = p
        self.q = q
    def __str__(self):
        return '('+str(self.p)+' | '+str(self.q)+')'
    def _satisfy(self, alist):
        for child in self.p, self.q:
            success, alist2 = child.satisfy(alist)
            if success:
                return 1, alist2
        return 0, {}
    def _falsify(self, alist):
        success, alist = self.p.falsify(alist)
        if success:
            success, alist = self.q.falsify(alist)
            if success:
                return 1, alist
        return 0, {}

class Negation(Formula):
    def __init__(self,p):
        self.p = p
    def __str__(self):
        return '!'+str(self.p)
    def _satisfy(self, alist):
        return self.p.falsify(alist)
    def _falsify(self, alist):
        return self.p.satisfy(alist)

class Variable(Formula):
    def __init__(self,v):
        self.v = v
    def __str__(self):
        return self.v
    def __bind(self, alist, value):
        if alist.has_key(self.v):
            return alist[self.v] == value, alist
        else:
            alist = alist.copy()
            alist[self.v] = value
            return 1, alist
    def _satisfy(self, alist):
        return self.__bind(alist, 1)
    def _falsify(self, alist):
        return self.__bind(alist, 0)

The rest of Denys's code works unchanged with the above.