[comp.lang.lisp] explicit continuations

duchier@cs.yale.edu (Denys Duchier) (09/06/90)

In article <1621@anaxagoras.ils.nwu.edu> krulwich@ils.nwu.edu (Bruce Krulwich) writes:
 >  The best answer that I've found to all of these problems is to have the
 >  function take continuation parameters for all of the end-cases

Yes.

 >  The following could be how a database retrieval system could be called.  The
 >  first arg is the proposition, the second is the continuation to call in the
 >  success case, and the third is the continuation to call in the failure case.
 >
 >  (query '(on a b) 
 >    #'(lambda (bindings) (format t "A is ~S" (cdr (assoc 'a bindings))))
 >    #'(lambda () (format t "I failed...")))

No. This is not quite right. In general, the success continuation
ought to take a failure continuation as an argument. Consider for
example the problem of deciding whether a formula of propositional
logic is a tautology. Here is a (deliberately unclever--cleverness
often begets obfuscation) implementation of a decision procedure using
explicit continuations.

This is simply an illustration of the technique (do not send
suggestions for improvements).

--Denys

(define (tautology? p)
  (falsify p '() (lambda (assignments fail) '#f) (lambda () '#t)))

(define (falsify p assignments continue fail)
  (cond ((ass equiv? p assignments) =>
         (lambda (assignment)
	   (if (cdr assignment)
	       (fail)
	       (continue assignments fail))))
	((atom? p)
	 (continue (cons (cons p '#f) assignments) fail))
	((eq? 'AND (car p))
	 (falsify-some (cdr p) assignments continue fail))
	((eq? 'OR  (car p))
	 (falsify-all  (cdr p) assignments continue fail))
	((eq? 'NOT (car p))
	 (verify (cadr p) assignments continue fail))
	((eq? 'IF  (car p))
	 (verify (cadr p) assignments
	   (lambda (assignments fail)
	     (falsify (caddr p) assignments continue fail))
	   fail))
	(t (continue (cons (cons p '#f) assignments) fail))))

(define (verify p assignments continue fail)
  (cond ((ass equiv? p assignments) =>
         (lambda (assignment)
	   (if (cdr assignment)
	       (continue assignments fail)
	       (fail))))
	((atom? p)
	 (continue (cons (cons p '#t) assignments) fail))
	((eq? 'AND (car p))
	 (verify-all (cdr p) assignments continue fail))
	((eq? 'OR  (car p))
	 (verify-some  (cdr p) assignments continue fail))
	((eq? 'NOT (car p))
	 (falsify (cadr p) assignments continue fail))
	((eq? 'IF  (car p))
	 (falsify (cadr p) assignments continue
	   (lambda () (verify (caddr p) assignments continue fail))))
	(t (continue (cons (cons p '#t) assignments) fail))))

(define (falsify-all l assignments continue fail)
  (if (null? l)
      (continue assignments fail)
      (falsify (car l) assignments
	(lambda (assignments fail)
	  (falsify-all (cdr l) assignments continue fail))
	fail)))

(define (verify-all l assignments continue fail)
  (if (null? l)
      (continue assignments fail)
      (verify (car l) assignments
	(lambda (assignments fail)
	  (verify-all (cdr l) assignments continue fail))
	fail)))

(define (falsify-some l assignments continue fail)
  (if (null? l)
      (fail)
      (falsify (car l) assignments continue
	(lambda ()
	  (falsify-some (cdr l) assignments continue fail)))))

(define (verify-some l assignments continue fail)
  (if (null? l)
      (fail)
      (falsify (car l) assignments continue
	(lambda ()
	  (verify-some (cdr l) assignments continue fail)))))