From 1b4cd42d5c8e39f62e8f7b51cfdb817e60ab5a0a Mon Sep 17 00:00:00 2001 From: Jay McCarthy Date: Fri, 23 Apr 2010 17:00:38 -0600 Subject: [PATCH] Rewrote documentation and working on cut --- collects/schelog/INSTALL | 85 -- collects/schelog/README | 55 - collects/schelog/examples/bible.rkt | 14 +- collects/schelog/examples/england.rkt | 20 +- collects/schelog/examples/games.rkt | 16 +- collects/schelog/examples/houses.rkt | 20 +- collects/schelog/examples/mapcol.rkt | 16 +- collects/schelog/examples/puzzle.rkt | 4 +- collects/schelog/examples/toys.rkt | 26 +- collects/schelog/info.ss | 2 + collects/schelog/main.rkt | 3 + collects/schelog/makefile | 48 - collects/schelog/manifest | 20 - collects/schelog/schelog-version.tex | 1 - collects/schelog/schelog.bib | 95 -- collects/schelog/schelog.rkt | 711 +++++------ collects/schelog/schelog.scrbl | 1422 ++++++++++++++++++++++ collects/schelog/schelog.tex | 1572 ------------------------- 18 files changed, 1842 insertions(+), 2288 deletions(-) delete mode 100644 collects/schelog/INSTALL delete mode 100644 collects/schelog/README create mode 100644 collects/schelog/main.rkt delete mode 100644 collects/schelog/makefile delete mode 100644 collects/schelog/manifest delete mode 100644 collects/schelog/schelog-version.tex delete mode 100644 collects/schelog/schelog.bib create mode 100644 collects/schelog/schelog.scrbl delete mode 100644 collects/schelog/schelog.tex diff --git a/collects/schelog/INSTALL b/collects/schelog/INSTALL deleted file mode 100644 index 3acb4689a2..0000000000 --- a/collects/schelog/INSTALL +++ /dev/null @@ -1,85 +0,0 @@ -Installing Schelog - - -*** JBC, 2010-04-22: I conjecture that (as a collection -within the PLT tree) installation directions are now -superfluous. The below is preserved for posterity. - - - - -- - -First, obtain the Schelog distribution. This is -available at - -http://www.ccs.neu.edu/~dorai/schelog/schelog.html - -Gunzipping and untarring this file produces a directory -called "schelog". This directory contains, among other -subsidiary files: - -the Schelog code file "schelog.scm"; - -the file INSTALL, which you are now reading. - -- - -The file schelog.scm in the distribution loads in -MzScheme (and some other Scheme dialects) without -configuration. If it does not load in your -dialect, you can configure Schelog for it using -the scmxlate package, which is available at -http://www.ccs.neu.edu/~dorai/scmxlate/scmxlate.html - -Start your Scheme in the schelog directory, and load -the file scmxlate/scmxlate.scm , using the correct -relative or full pathname. You will be asked what your -Scheme dialect is. Answer appropriately. The -following symbols are used by the porting -mechanism to identify the corresponding Scheme -dialects: bigloo (Bigloo); gambit (Gambit); guile -(Guile); mitscheme (MIT Scheme); mzscheme (MzScheme); -petite (Petite Chez Scheme); pscheme (Pocket Scheme); -scm (SCM); stk (STk). - -scmxlate will generate a file called -"my-schelog.scm", which you may rename to -"schelog.scm". - -Load schelog.scm into your Scheme in order to use -Schelog. - -The distribution comes with an "examples" subdirectory -containing some sample Schelog programs. In order to -try an example file, load it into your Scheme after -ensuring that "schelog.scm" has already been loaded. -Follow the instructions in the example file. - -- - -The file "schelog.tex" contains a tutorial on Schelog. Run it -through (plain) TeX to obtain viewable/printable -documentation. (You will need to run TeX twice to resolve -cross references.) - -You can get a browsable version of the document by -calling - -tex2page schelog.tex - -This browsable version is also available for Web -viewing at - -http://www.ccs.neu.edu/~dorai/schelog/schelog.html - -tex2page is available at - -http://www.ccs.neu.edu/~dorai/tex2page/tex2page-doc.html - -- - -Concise bug reports, questions, and suggestions -may be emailed to - -ds26 at gte dot com diff --git a/collects/schelog/README b/collects/schelog/README deleted file mode 100644 index 2fc9397a94..0000000000 --- a/collects/schelog/README +++ /dev/null @@ -1,55 +0,0 @@ -README -Schelog -Dorai Sitaram -ds26@gte.com - - -*** JBC 2010-04-22: this package has been TAMPERED WITH in an unscrupulous and -undisciplined way by John Clements 2010-04-22 in order to see how difficult it -would be to get it to compile in PLT 4.2.5. The answer is "not hard", but it's -certainly not portable any more, and crucially the two macros that cause -capture of the ! symbol now require uses of the macro to supply the bang, thus -making them non-capturing. - -TODO: -- pull some part of the docs across from their tex format -- figure out what to do with the makefile (delete it?) -- turn more of the implicit test cases into explicit test cases -- clean up this README file -- figure out whether there are copyright issues - - - ... - -Schelog is for you if you are interested in any or all -of the following: Scheme, Prolog, logic, logic -programming, AI, and expert systems. - -Schelog is an embedding of logic programming a la -Prolog in Scheme. "Embedding" means you don't lose -Scheme: You can use Prolog-style and conventional -Scheme code fragments alongside each other. Schelog -contains the full repertoire of Prolog features, -including meta-logical and second-order ("set") -predicates, leaving out only those features that could -be more easily and more efficiently done with Scheme -subexpressions. The Schelog distribution includes -examples and comprehensive documentation. - -Schelog has been tested successfully on the following -Scheme dialects: - -Bigloo, Gambit, Guile, MIT Scheme, MzScheme, Petite -Chez Scheme, Pocket Scheme, SCM, and STk. - - ... - -The Schelog distribution is available at the URL: - - http://www.cs.rice.edu/CS/PLT/packages/schelog/ - -Unpacking (using gunzip and tar xf) the Schelog distribution -produces a directory called "schelog". In it is a file -called INSTALL which contains detailed installation -instructions. Read INSTALL now. - diff --git a/collects/schelog/examples/bible.rkt b/collects/schelog/examples/bible.rkt index 7a055e10ea..242c48ae02 100644 --- a/collects/schelog/examples/bible.rkt +++ b/collects/schelog/examples/bible.rkt @@ -9,7 +9,7 @@ ;(%father X Y) :- X is the father of Y. (define %father - (%rel ! () + (%rel () (('terach 'abraham)) (('terach 'nachor)) (('terach 'haran)) (('abraham 'isaac)) (('haran 'lot)) (('haran 'milcah)) (('haran 'yiscah)))) @@ -17,14 +17,14 @@ ;(%mother X Y) :- X is the mother of Y. (define %mother - (%rel ! () (('sarah 'isaac)))) + (%rel () (('sarah 'isaac)))) (define %male - (%rel ! () + (%rel () (('terach)) (('abraham)) (('isaac)) (('lot)) (('haran)) (('nachor)))) (define %female - (%rel ! () + (%rel () (('sarah)) (('milcah)) (('yiscah)))) ;AoP, ch. 17. Finding all the children of a particular @@ -36,13 +36,13 @@ (define %children-1 (letrec ((children-aux - (%rel ! (x a cc c) + (%rel (x a cc c) ((x a cc) (%father x c) (%not (%member c a)) ! (children-aux x (cons c a) cc)) ((x cc cc))))) - (%rel ! (x cc) + (%rel (x cc) ((x cc) (children-aux x '() cc))))) (define terachs-kids-test @@ -79,7 +79,7 @@ ;Uses set predicate %bag-of (define %children - (%rel ! (x kids c) + (%rel (x kids c) ((kids) (%set-of c (%father x c) kids)))) (define dad-kids-test-2 diff --git a/collects/schelog/examples/england.rkt b/collects/schelog/examples/england.rkt index 3a911d6400..15fc6ee400 100644 --- a/collects/schelog/examples/england.rkt +++ b/collects/schelog/examples/england.rkt @@ -11,47 +11,47 @@ ;The file england2.scm uses a Scheme-like syntax. (define %male - (%rel ! () + (%rel () (('philip)) (('charles)) (('andrew)) (('edward)) (('mark)) (('william)) (('harry)) (('peter)))) (define %female - (%rel ! () + (%rel () (('elizabeth)) (('anne)) (('diana)) (('sarah)) (('zara)))) (define %husband-of - (%rel ! () + (%rel () (('philip 'elizabeth)) (('charles 'diana)) (('mark 'anne)) (('andrew 'sarah)))) (define %wife-of - (%rel ! (w h) + (%rel (w h) ((w h) (%husband-of h w)))) (define %married-to - (%rel ! (x y) + (%rel (x y) ((x y) (%husband-of x y)) ((x y) (%wife-of x y)))) (define %father-of - (%rel ! () + (%rel () (('philip 'charles)) (('philip 'anne)) (('philip 'andrew)) (('philip 'edward)) (('charles 'william)) (('charles 'harry)) (('mark 'peter)) (('mark 'zara)))) (define %mother-of - (%rel ! (m c f) + (%rel (m c f) ((m c) (%wife-of m f) (%father-of f c)))) (define %child-of - (%rel ! (c p) + (%rel (c p) ((c p) (%father-of p c)) ((c p) (%mother-of p c)))) (define %parent-of - (%rel ! (p c) + (%rel (p c) ((p c) (%child-of c p)))) (define %brother-of - (%rel ! (b x f) + (%rel (b x f) ((b x) (%male b) (%father-of f b) (%father-of f x) (%/= b x)))) diff --git a/collects/schelog/examples/games.rkt b/collects/schelog/examples/games.rkt index 9575a08595..9a001b760d 100644 --- a/collects/schelog/examples/games.rkt +++ b/collects/schelog/examples/games.rkt @@ -20,7 +20,7 @@ (list 'person name country sport))) (define %games - (%rel ! (clues queries solution the-men + (%rel (clues queries solution the-men n1 n2 n3 c1 c2 c3 s1 s2 s3) ((clues queries solution) (%= the-men @@ -29,7 +29,7 @@ (%games-queries the-men queries solution)))) (define %games-clues - (%rel ! (the-men clue1-man1 clue1-man2 clue2-man1 clue2-man2 clue3-man) + (%rel (the-men clue1-man1 clue1-man2 clue2-man1 clue2-man2 clue3-man) ((the-men (list (%did-better clue1-man1 clue1-man2 the-men) @@ -46,7 +46,7 @@ (%sport clue3-man 'cricket)))))) (define %games-queries - (%rel ! (the-men man1 man2 aussies-name dicks-sport) + (%rel (the-men man1 man2 aussies-name dicks-sport) ((the-men (list (%member man1 the-men) @@ -61,25 +61,25 @@ (list 'richard 'plays dicks-sport)))))) (define %did-better - (%rel ! (a b c) + (%rel (a b c) ((a b (list a b c))) ((a c (list a b c))) ((b c (list a b c))))) (define %name - (%rel ! (name country sport) + (%rel (name country sport) (((person name country sport) name)))) (define %country - (%rel ! (name country sport) + (%rel (name country sport) (((person name country sport) country)))) (define %sport - (%rel ! (name country sport) + (%rel (name country sport) (((person name country sport) sport)))) (define %first - (%rel ! (car cdr) + (%rel (car cdr) (((cons car cdr) car)))) ;;With the above as the database, and also loading the file diff --git a/collects/schelog/examples/houses.rkt b/collects/schelog/examples/houses.rkt index 08e4601215..fc25dcf75b 100644 --- a/collects/schelog/examples/houses.rkt +++ b/collects/schelog/examples/houses.rkt @@ -29,25 +29,25 @@ (lambda (hue nation pet drink cigarette) (list 'house hue nation pet drink cigarette))) -(define %hue (%rel ! (h) (((house h (_) (_) (_) (_)) h)))) -(define %nation (%rel ! (n) (((house (_) n (_) (_) (_)) n)))) -(define %pet (%rel ! (p) (((house (_) (_) p (_) (_)) p)))) -(define %drink (%rel ! (d) (((house (_) (_) (_) d (_)) d)))) -(define %cigarette (%rel ! (c) (((house (_) (_) (_) (_) c) c)))) +(define %hue (%rel (h) (((house h (_) (_) (_) (_)) h)))) +(define %nation (%rel (n) (((house (_) n (_) (_) (_)) n)))) +(define %pet (%rel (p) (((house (_) (_) p (_) (_)) p)))) +(define %drink (%rel (d) (((house (_) (_) (_) d (_)) d)))) +(define %cigarette (%rel (c) (((house (_) (_) (_) (_) c) c)))) (define %adjacent - (%rel ! (a b) + (%rel (a b) ((a b (list a b (_) (_) (_)))) ((a b (list (_) a b (_) (_)))) ((a b (list (_) (_) a b (_)))) ((a b (list (_) (_) (_) a b))))) (define %middle - (%rel ! (a) + (%rel (a) ((a (list (_) (_) a (_) (_)))))) (define %houses - (%rel ! (row-of-houses clues queries solution + (%rel (row-of-houses clues queries solution h1 h2 h3 h4 h5 n1 n2 n3 n4 n5 p1 p2 p3 p4 p5 d1 d2 d3 d4 d5 c1 c2 c3 c4 c5) ((clues queries solution) @@ -62,7 +62,7 @@ (%houses-queries row-of-houses queries solution)))) (define %houses-clues - (%rel ! (row-of-houses abode1 abode2 abode3 abode4 abode5 abode6 abode7 + (%rel (row-of-houses abode1 abode2 abode3 abode4 abode5 abode6 abode7 abode8 abode9 abode10 abode11 abode12 abode13 abode14 abode15) ((row-of-houses (list @@ -126,7 +126,7 @@ (%hue abode15 'blue)))))) (define %houses-queries - (%rel ! (row-of-houses abode1 abode2 zebra-owner water-drinker) + (%rel (row-of-houses abode1 abode2 zebra-owner water-drinker) ((row-of-houses (list (%member abode1 row-of-houses) diff --git a/collects/schelog/examples/mapcol.rkt b/collects/schelog/examples/mapcol.rkt index 3c0de24d9c..4ed29869af 100644 --- a/collects/schelog/examples/mapcol.rkt +++ b/collects/schelog/examples/mapcol.rkt @@ -9,21 +9,21 @@ ;; is this different from the %member provided by schelog? fencing that one out. (define %member - (%rel ! (X Xs Y Ys) + (%rel (X Xs Y Ys) ((X (cons X Xs))) ((X (cons Y Ys)) (%member X Ys)))) ;(%members x y) holds if x is a subset of y (define %members - (%rel ! (X Xs Ys) + (%rel (X Xs Ys) (((cons X Xs) Ys) (%member X Ys) (%members Xs Ys)) (('() Ys)))) ;(%select x y z) holds if z is y with one less occurrence of x (define %select - (%rel ! (X Xs Y Ys Zs) + (%rel (X Xs Y Ys Zs) ((X (cons X Xs) Xs)) ((X (cons Y Ys) (cons Y Zs)) (%select X Ys Zs)))) @@ -35,26 +35,26 @@ (list 'region name color neighbors))) (define %color-map - (%rel ! (Region Regions Colors) + (%rel (Region Regions Colors) (((cons Region Regions) Colors) (%color-region Region Colors) (%color-map Regions Colors)) (('() Colors)))) (define %color-region - (%rel ! (Name Color Neighbors Colors Colors1) + (%rel (Name Color Neighbors Colors Colors1) (((region Name Color Neighbors) Colors) (%select Color Colors Colors1) (%members Neighbors Colors1)))) (define %test-color - (%rel ! (Name Map Colors) + (%rel (Name Map Colors) ((Name Map) (%map Name Map) (%colors Colors) (%color-map Map Colors)))) (define %map - (%rel ! (A B C D E F G H I L P S) + (%rel (A B C D E F G H I L P S) (('test (list (region 'a A (list B C D)) (region 'b B (list A C E)) @@ -76,7 +76,7 @@ (region 'austria A (list I S G))))))) (define %colors - (%rel ! () + (%rel () (('(red yellow blue white))))) ;ask (%which (M) (%test-color 'test M)) or diff --git a/collects/schelog/examples/puzzle.rkt b/collects/schelog/examples/puzzle.rkt index 302fcd9594..08092a4eff 100644 --- a/collects/schelog/examples/puzzle.rkt +++ b/collects/schelog/examples/puzzle.rkt @@ -19,13 +19,13 @@ ; solve([]). (define %solve-puzzle - (%rel ! (clues queries solution) + (%rel (clues queries solution) ((clues queries solution) (%solve clues) (%solve queries)))) (define %solve - (%rel ! (clue clues) + (%rel (clue clues) (((cons clue clues)) clue (%solve clues)) diff --git a/collects/schelog/examples/toys.rkt b/collects/schelog/examples/toys.rkt index 628a071dea..c90c8e49ba 100644 --- a/collects/schelog/examples/toys.rkt +++ b/collects/schelog/examples/toys.rkt @@ -8,14 +8,14 @@ ;(%length l n) holds if length(l) = n (define %length - (%rel ! (h t n m) + (%rel (h t n m) (('() 0)) (((cons h t) n) (%length t m) (%is n (+ m 1))))) ;(%delete x y z) holds if z is y with all x's removed (define %delete - (%rel ! (x y z w) + (%rel (x y z w) ((x '() '())) ((x (cons x w) y) (%delete x w y)) ((x (cons z w) (cons z y)) (%not (%= x z)) (%delete x w y)))) @@ -23,7 +23,7 @@ ;(%remdup x y) holds if y is x without duplicates (define %remdup - (%rel ! (x y z w) + (%rel (x y z w) (('() '())) (((cons x y) (cons x z)) (%delete x y w) (%remdup w z)))) @@ -31,31 +31,31 @@ ;counting duplicates '(define %count - (%rel ! (x n y) + (%rel (x n y) ((x n) (%remdup x y) (%length y n)))) ;same thing (define %count (letrec ((countaux - (%rel ! (m n m+1 x y z) + (%rel (m n m+1 x y z) (('() m m)) (((cons x y) m n) (%delete x y z) (%is m+1 (+ m 1)) (countaux z m+1 n))))) - (%rel ! (x n) + (%rel (x n) ((x n) (countaux x 0 n))))) ;(%append x y z) holds if z is the concatenation of x and y (define %append - (%rel ! (x y z w) + (%rel (x y z w) (('() x x)) (((cons x y) z (cons x w)) (%append y z w)))) ;(%reverse x y) holds if the y is the reversal of x '(define %reverse - (%rel ! (x y z yy) + (%rel (x y z yy) (('() '())) (((cons x y) z) (%reverse y yy) (%append yy (list x) z)))) @@ -63,16 +63,16 @@ (define %reverse (letrec ((revaux - (%rel ! (x y z w) + (%rel (x y z w) (('() y y)) (((cons x y) z w) (revaux y (cons x z) w))))) - (%rel ! (x y) + (%rel (x y) ((x y) (revaux x '() y))))) ;(%fact n m) holds if m = n! '(define %fact - (%rel ! (n n! n-1 n-1!) + (%rel (n n! n-1 n-1!) ((0 1)) ((n n!) (%is n-1 (- n 1)) (%fact n-1 n-1!) (%is n! (* n n-1!))))) @@ -80,9 +80,9 @@ (define %fact (letrec ((factaux - (%rel ! (n! m x m-1 xx) + (%rel (n! m x m-1 xx) ((0 n! n!)) ((m x n!) (%is m-1 (- m 1)) (%is xx (* x m)) (factaux m-1 xx n!))))) - (%rel ! (n n!) + (%rel (n n!) ((n n!) (factaux n 1 n!))))) diff --git a/collects/schelog/info.ss b/collects/schelog/info.ss index 13a63c4835..7905bec2a8 100644 --- a/collects/schelog/info.ss +++ b/collects/schelog/info.ss @@ -1,2 +1,4 @@ #lang setup/infotab +(define scribblings + '(("schelog.scrbl" (multi-page) (tool)))) diff --git a/collects/schelog/main.rkt b/collects/schelog/main.rkt new file mode 100644 index 0000000000..141fff5b0f --- /dev/null +++ b/collects/schelog/main.rkt @@ -0,0 +1,3 @@ +#lang racket +(require "schelog.rkt") +(provide (all-from-out "schelog.rkt")) \ No newline at end of file diff --git a/collects/schelog/makefile b/collects/schelog/makefile deleted file mode 100644 index 69d8cb0ce5..0000000000 --- a/collects/schelog/makefile +++ /dev/null @@ -1,48 +0,0 @@ -# JBC, 2010-04-22: -# this makefile could probably be usefully rendered in scheme... but -# I'm not going to try. - - -TRIGGER_FILES = history manifest makefile version.tex \ - schelog.scm schelog.tex - -default: - @echo Please read the file INSTALL. - -%.html: %.tex - tex2page $(@:%.html=%) - while grep -i "rerun: tex2page" $(@:%.html=%.hlog); do \ - tex2page $(@:%.html=%); \ - done - -schelog.pdf: schelog.tex - pdftex $^ - -schelog.tar: - echo tar cf schelog.tar schelog/manifest > .tarscript - for f in `grep "^[^;]" manifest`; do \ - echo tar uf schelog.tar schelog/$$f >> .tarscript; \ - done - chmod +x .tarscript - cd ..; schelog/.tarscript - mv ../schelog.tar . - -schelog.tar.bz2: $(TRIGGER_FILES) - make schelog.tar - bzip2 -f schelog.tar - -schelog.tar.gz: $(TRIGGER_FILES) - make schelog.tar - gzip -f schelog.tar - -html: schelog.html - -pdf: schelog.pdf - -dist: schelog.tar.bz2 - -webdist: schelog.tar.gz html - -clean: - @rm -f *~ *.bak - cd dialects; rm -f *~ *.bak diff --git a/collects/schelog/manifest b/collects/schelog/manifest deleted file mode 100644 index 5d3091d762..0000000000 --- a/collects/schelog/manifest +++ /dev/null @@ -1,20 +0,0 @@ -COPYING -README -manifest -makefile -schelog-version.tex -INSTALL -history -schelog.tex -schelog.scm -schelog.bib -dialects/*.scm -examples/bible.scm -examples/england.scm -examples/england2.scm -examples/games.scm -examples/holland.scm -examples/houses.scm -examples/mapcol.scm -examples/puzzle.scm -examples/toys.scm diff --git a/collects/schelog/schelog-version.tex b/collects/schelog/schelog-version.tex deleted file mode 100644 index 5dca9b0e71..0000000000 --- a/collects/schelog/schelog-version.tex +++ /dev/null @@ -1 +0,0 @@ -2003-06-01% last change diff --git a/collects/schelog/schelog.bib b/collects/schelog/schelog.bib deleted file mode 100644 index 98e6a41ba1..0000000000 --- a/collects/schelog/schelog.bib +++ /dev/null @@ -1,95 +0,0 @@ - -@book{sicp, - author = "Harold Abelson and Gerald Jay {Sussman with Julie Sussman}", - title = "\urlp{Structure and Interpretation of - Computer Programs (``SICP'')}{http://mitpress.mit.edu/sicp/full-text/book/book.html}", - edition = "2nd", - publisher = "MIT Press", - year = 1996, -} - -@book{aop, - author = "Leon Sterling and Ehud Shapiro", - title = "\urlh{http://mitpress.mit.edu/book-home.tcl?isbn=0262193388}{The Art - of Prolog}", - publisher = "MIT Press", - year = 1994, - edition = "2nd", -} - -@book{tls, - author = "Daniel P Friedman and Matthias Felleisen", - title = "\urlh{http://www.ccs.neu.edu/~matthias/BTLS}{The Little Schemer}", - publisher = "MIT Press", - year = 1996, - edition = "4th", -} - -@book{tss, - author = "Daniel P Friedman and Matthias Felleisen", - title = "\urlh{http://www.ccs.neu.edu/~matthias/BTSS}{The Seasoned Schemer}", - publisher = "MIT Press", - year = 1996, -} - -@book{eopl, - author = "Daniel P Friedman and Mitchell Wand and Christopher T Haynes", - title = "\urlh{http://mitpress.mit.edu/book-home.tcl?isbn=0262061457}{Essentials - of Programming Languages}", - publisher = "MIT Press, McGraw-Hill", - year = 1992, -} - -@book{bratko, - author = "Ivan Bratko", - title = "Prolog Programming for Artificial Intelligence", - publisher = "Addison-Wesley", - year = 1986, -} - -@book{campbell, - editor = "J A Campbell", - title = "Implementations of Prolog", - publisher = "Ellis Horwood", - year = 1984, -} - -@book{ok:prolog, - author = "Richard A O'Keefe", - title = "\urlh{http://mitpress.mit.edu/book-home.tcl?isbn=0262150395}{The - Craft of Prolog}", - publisher = "MIT Press", - year = 1990, -} - -@inproceedings{logick, - author = "Christopher T Haynes", - title = "{Logic continuations}", - booktitle = "{J Logic Program}", - year = 1987, - note = "vol 4", - pages = "157--176", -} - -@misc{r5rs, - author = "Richard Kelsey and William Clinger and - Jonathan {Rees (eds)}", - title = "\urlp{Revised\^{}5 - Report on the Algorithmic Language Scheme - (``R5RS'')}{http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs.html}", - year = 1998, -} - -@misc{t-y-scheme, - author = "Dorai Sitaram", - title = "\urlp{Teach Yourself Scheme - in Fixnum Days}{http://www.ccs.neu.edu/~dorai/t-y-scheme/t-y-scheme.html}", -} - -@techreport{mf:prolog, - author = "Matthias Felleisen", - title = "{Transliterating Prolog into Scheme}", - institution = "{Indiana U Comp Sci Dept}", - year = 1985, - number = 182, -} diff --git a/collects/schelog/schelog.rkt b/collects/schelog/schelog.rkt index b18a68903e..264e5badd1 100644 --- a/collects/schelog/schelog.rkt +++ b/collects/schelog/schelog.rkt @@ -41,15 +41,15 @@ ;;unbound refs point to themselves (lambda opt (vector schelog:*ref* - (if (null? opt) schelog:*unbound* - (car opt))))) + (if (null? opt) schelog:*unbound* + (car opt))))) (define _ schelog:make-ref) (define schelog:ref? (lambda (r) (and (vector? r) - (eq? (vector-ref r 0) schelog:*ref*)))) + (eq? (vector-ref r 0) schelog:*ref*)))) (define schelog:deref (lambda (r) @@ -83,41 +83,41 @@ (lambda (r) (let ((r2 (schelog:deref r))) (and (vector? r2) - (eq? (vector-ref r2 0) schelog:*frozen*))))) + (eq? (vector-ref r2 0) schelog:*frozen*))))) ;deref a structure completely (except the frozen ones, i.e.) (define schelog:deref* (lambda (s) (cond ((schelog:ref? s) - (if (schelog:frozen-ref? s) s - (schelog:deref* (schelog:deref s)))) - ((pair? s) (cons (schelog:deref* (car s)) - (schelog:deref* (cdr s)))) - ((vector? s) - (list->vector (map schelog:deref* (vector->list s)))) - (else s)))) + (if (schelog:frozen-ref? s) s + (schelog:deref* (schelog:deref s)))) + ((pair? s) (cons (schelog:deref* (car s)) + (schelog:deref* (cdr s)))) + ((vector? s) + (list->vector (map schelog:deref* (vector->list s)))) + (else s)))) ;%let introduces new logic variables (define-syntax %let (syntax-rules () ((%let (x ...) . e) - (let ((x (schelog:make-ref)) ...) - . e)))) + (let ((x (schelog:make-ref)) ...) + . e)))) #;(define-macro %let - (lambda (xx . ee) - `(let ,(map (lambda (x) `(,x (schelog:make-ref))) xx) - ,@ee))) + (lambda (xx . ee) + `(let ,(map (lambda (x) `(,x (schelog:make-ref))) xx) + ,@ee))) ;the unify predicate -(define *schelog-use-occurs-check?* #f) +(define schelog-use-occurs-check? (make-parameter #f)) (define schelog:occurs-in? (lambda (var term) - (and *schelog-use-occurs-check?* + (and (schelog-use-occurs-check?) (let loop ((term term)) (cond ((eqv? var term) #t) ((schelog:ref? term) @@ -134,45 +134,45 @@ (lambda (t1 t2) (lambda (fk) (letrec - ((cleanup-n-fail - (lambda (s) - (for-each schelog:unbind-ref! s) - (fk 'fail))) - (unify1 - (lambda (t1 t2 s) - ;(printf "unify1 ~s ~s~%" t1 t2) - (cond ((eqv? t1 t2) s) - ((schelog:ref? t1) - (cond ((schelog:unbound-ref? t1) - (cond ((schelog:occurs-in? t1 t2) - (cleanup-n-fail s)) - (else + ((cleanup-n-fail + (lambda (s) + (for-each schelog:unbind-ref! s) + (fk 'fail))) + (unify1 + (lambda (t1 t2 s) + ;(printf "unify1 ~s ~s~%" t1 t2) + (cond ((eqv? t1 t2) s) + ((schelog:ref? t1) + (cond ((schelog:unbound-ref? t1) + (cond ((schelog:occurs-in? t1 t2) + (cleanup-n-fail s)) + (else (schelog:set-ref! t1 t2) (cons t1 s)))) - ((schelog:frozen-ref? t1) - (cond ((schelog:ref? t2) - (cond ((schelog:unbound-ref? t2) - ;(printf "t2 is unbound~%") - (unify1 t2 t1 s)) - ((schelog:frozen-ref? t2) - (cleanup-n-fail s)) - (else + ((schelog:frozen-ref? t1) + (cond ((schelog:ref? t2) + (cond ((schelog:unbound-ref? t2) + ;(printf "t2 is unbound~%") + (unify1 t2 t1 s)) + ((schelog:frozen-ref? t2) + (cleanup-n-fail s)) + (else (unify1 t1 (schelog:deref t2) s)))) - (else (cleanup-n-fail s)))) - (else + (else (cleanup-n-fail s)))) + (else ;(printf "derefing t1~%") (unify1 (schelog:deref t1) t2 s)))) - ((schelog:ref? t2) (unify1 t2 t1 s)) - ((and (pair? t1) (pair? t2)) - (unify1 (cdr t1) (cdr t2) - (unify1 (car t1) (car t2) s))) - ((and (string? t1) (string? t2)) - (if (string=? t1 t2) s - (cleanup-n-fail s))) - ((and (vector? t1) (vector? t2)) - (unify1 (vector->list t1) - (vector->list t2) s)) - (else + ((schelog:ref? t2) (unify1 t2 t1 s)) + ((and (pair? t1) (pair? t2)) + (unify1 (cdr t1) (cdr t2) + (unify1 (car t1) (car t2) s))) + ((and (string? t1) (string? t2)) + (if (string=? t1 t2) s + (cleanup-n-fail s))) + ((and (vector? t1) (vector? t2)) + (unify1 (vector->list t1) + (vector->list t2) s)) + (else (for-each schelog:unbind-ref! s) (fk 'fail)))))) (let ((s (unify1 t1 t2 '()))) @@ -188,24 +188,24 @@ ((%or g ...) (lambda (__fk) (call-with-current-continuation - (lambda (__sk) - (call-with-current-continuation - (lambda (__fk) - (__sk ((schelog:deref* g) __fk)))) - ... - (__fk 'fail))))))) + (lambda (__sk) + (call-with-current-continuation + (lambda (__fk) + (__sk ((schelog:deref* g) __fk)))) + ... + (__fk 'fail))))))) #;(define-macro %or - (lambda gg - `(lambda (__fk) - (call-with-current-continuation - (lambda (__sk) - ,@(map (lambda (g) - `(call-with-current-continuation - (lambda (__fk) - (__sk ((schelog:deref* ,g) __fk))))) - gg) - (__fk 'fail)))))) + (lambda gg + `(lambda (__fk) + (call-with-current-continuation + (lambda (__sk) + ,@(map (lambda (g) + `(call-with-current-continuation + (lambda (__fk) + (__sk ((schelog:deref* ,g) __fk))))) + gg) + (__fk 'fail)))))) ;conjunction @@ -214,73 +214,76 @@ ((%and g ...) (lambda (__fk) (let* ((__fk ((schelog:deref* g) __fk)) - ...) - __fk))))) + ...) + __fk))))) #;(define-macro %and - (lambda gg - `(lambda (__fk) - (let* ,(map (lambda (g) `(__fk ((schelog:deref* ,g) __fk))) gg) - __fk)))) + (lambda gg + `(lambda (__fk) + (let* ,(map (lambda (g) `(__fk ((schelog:deref* ,g) __fk))) gg) + __fk)))) + +(define (! fk) (error '! "May only be used inside goal expression.")) ;cut -;; rather arbitrarily made this macro non- -;; capturing by requiring ! to be supplied at -;; macro use... not changing docs... -- JBC 2010 -(define-syntax %cut-delimiter - (syntax-rules () - ((%cut-delimiter ! g) - (lambda (__fk) - (let ((! (lambda (__fk2) __fk))) - ((schelog:deref* g) __fk)))))) +(define-syntax (%cut-delimiter stx) + (syntax-case stx () + ((%cut-delimiter g) + (with-syntax ([! #'!]) + (syntax/loc stx + (lambda (__fk) + (let ((! (lambda (__fk2) __fk))) + ((schelog:deref* g) __fk)))))))) #;(define-macro %cut-delimiter - (lambda (g) - `(lambda (__fk) - (let ((! (lambda (__fk2) __fk))) - ((schelog:deref* ,g) __fk))))) + (lambda (g) + `(lambda (__fk) + (let ((! (lambda (__fk2) __fk))) + ((schelog:deref* ,g) __fk))))) ;Prolog-like sugar -(define-syntax %rel - (syntax-rules () - ((%rel ! (v ...) ((a ...) subgoal ...) ...) - (lambda __fmls - (lambda (__fk) - (call-with-current-continuation - (lambda (__sk) - (let ((! (lambda (fk1) __fk))) - (%let (v ...) - (call-with-current-continuation - (lambda (__fk) - (let* ((__fk ((%= __fmls (list a ...)) __fk)) - (__fk ((schelog:deref* subgoal) __fk)) - ...) - (__sk __fk)))) - ... - (__fk 'fail)))))))))) +(define-syntax (%rel stx) + (syntax-case stx () + ((%rel (v ...) ((a ...) subgoal ...) ...) + (with-syntax ([! #'!]) + (syntax/loc stx + (lambda __fmls + (lambda (__fk) + (call-with-current-continuation + (lambda (__sk) + (let ((! (lambda (fk1) __fk))) + (%let (v ...) + (call-with-current-continuation + (lambda (__fk) + (let* ((__fk ((%= __fmls (list a ...)) __fk)) + (__fk ((schelog:deref* subgoal) __fk)) + ...) + (__sk __fk)))) + ... + (__fk 'fail)))))))))))) #;(define-macro %rel - (lambda (vv . cc) - `(lambda __fmls - (lambda (__fk) - (call-with-current-continuation - (lambda (__sk) - (let ((! (lambda (fk1) __fk))) - (%let ,vv - ,@(map (lambda (c) - `(call-with-current-continuation - (lambda (__fk) - (let* ((__fk ((%= __fmls (list ,@(car c))) - __fk)) - ,@(map (lambda (sg) - `(__fk ((schelog:deref* ,sg) - __fk))) - (cdr c))) - (__sk __fk))))) - cc) - (__fk 'fail))))))))) + (lambda (vv . cc) + `(lambda __fmls + (lambda (__fk) + (call-with-current-continuation + (lambda (__sk) + (let ((! (lambda (fk1) __fk))) + (%let ,vv + ,@(map (lambda (c) + `(call-with-current-continuation + (lambda (__fk) + (let* ((__fk ((%= __fmls (list ,@(car c))) + __fk)) + ,@(map (lambda (sg) + `(__fk ((schelog:deref* ,sg) + __fk))) + (cdr c))) + (__sk __fk))))) + cc) + (__fk 'fail))))))))) ;the fail and true preds @@ -300,28 +303,28 @@ ((%is v e) (lambda (__fk) ((%= v (%is (1) e __fk)) __fk))) - + ((%is (1) (quote x) fk) (quote x)) ((%is (1) (x ...) fk) ((%is (1) x fk) ...)) ((%is (1) x fk) (if (and (schelog:ref? x) (schelog:unbound-ref? x)) - (fk 'fail) (schelog:deref* x))))) + (fk 'fail) (schelog:deref* x))))) #;(define-macro %is - (lambda (v e) - (letrec ((%is-help (lambda (e fk) - (cond ((pair? e) - (cond ((eq? (car e) 'quote) e) - (else - (map (lambda (e1) - (%is-help e1 fk)) e)))) - (else - `(if (and (schelog:ref? ,e) - (schelog:unbound-ref? ,e)) - (,fk 'fail) (schelog:deref* ,e))))))) - `(lambda (__fk) - ((%= ,v ,(%is-help e '__fk)) __fk))))) + (lambda (v e) + (letrec ((%is-help (lambda (e fk) + (cond ((pair? e) + (cond ((eq? (car e) 'quote) e) + (else + (map (lambda (e1) + (%is-help e1 fk)) e)))) + (else + `(if (and (schelog:ref? ,e) + (schelog:unbound-ref? ,e)) + (,fk 'fail) (schelog:deref* ,e))))))) + `(lambda (__fk) + ((%= ,v ,(%is-help e '__fk)) __fk))))) ;defining arithmetic comparison operators @@ -336,28 +339,28 @@ (define %< (schelog:make-binary-arithmetic-relation <)) (define %<= (schelog:make-binary-arithmetic-relation <=)) (define %=/= (schelog:make-binary-arithmetic-relation - (lambda (m n) (not (= m n))))) + (lambda (m n) (not (= m n))))) ;type predicates (define schelog:constant? (lambda (x) (cond ((schelog:ref? x) - (cond ((schelog:unbound-ref? x) #f) - ((schelog:frozen-ref? x) #t) - (else (schelog:constant? (schelog:deref x))))) - ((pair? x) #f) - ((vector? x) #f) - (else #t)))) + (cond ((schelog:unbound-ref? x) #f) + ((schelog:frozen-ref? x) #t) + (else (schelog:constant? (schelog:deref x))))) + ((pair? x) #f) + ((vector? x) #f) + (else #t)))) (define schelog:compound? (lambda (x) (cond ((schelog:ref? x) (cond ((schelog:unbound-ref? x) #f) - ((schelog:frozen-ref? x) #f) - (else (schelog:compound? (schelog:deref x))))) - ((pair? x) #t) - ((vector? x) #t) - (else #f)))) + ((schelog:frozen-ref? x) #f) + (else (schelog:compound? (schelog:deref x))))) + ((pair? x) #t) + ((vector? x) #t) + (else #f)))) (define %constant (lambda (x) @@ -374,12 +377,12 @@ (define schelog:var? (lambda (x) (cond ((schelog:ref? x) - (cond ((schelog:unbound-ref? x) #t) - ((schelog:frozen-ref? x) #f) - (else (schelog:var? (schelog:deref x))))) - ((pair? x) (or (schelog:var? (car x)) (schelog:var? (cdr x)))) - ((vector? x) (schelog:var? (vector->list x))) - (else #f)))) + (cond ((schelog:unbound-ref? x) #t) + ((schelog:frozen-ref? x) #f) + (else (schelog:var? (schelog:deref x))))) + ((pair? x) (or (schelog:var? (car x)) (schelog:var? (cdr x)))) + ((vector? x) (schelog:var? (vector->list x))) + (else #f)))) (define %var (lambda (x) @@ -395,11 +398,11 @@ (lambda (p) (lambda args (lambda (fk) - (if (call-with-current-continuation - (lambda (k) - ((apply p args) (lambda (d) (k #f))))) - (fk 'fail) - fk))))) + (if (call-with-current-continuation + (lambda (k) + ((apply p args) (lambda (d) (k #f))))) + (fk 'fail) + fk))))) (define %/= (schelog:make-negation %=)) @@ -409,45 +412,45 @@ (define schelog:ident? (lambda (x y) (cond ((schelog:ref? x) - (cond ((schelog:unbound-ref? x) - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) (eq? x y)) - ((schelog:frozen-ref? y) #f) - (else (schelog:ident? x (schelog:deref y))))) - (else #f))) - ((schelog:frozen-ref? x) - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) #f) - ((schelog:frozen-ref? y) (eq? x y)) - (else (schelog:ident? x (schelog:deref y))))) - (else #f))) - (else (schelog:ident? (schelog:deref x) y)))) - ((pair? x) - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) #f) - ((schelog:frozen-ref? y) #f) - (else (schelog:ident? x (schelog:deref y))))) - ((pair? y) - (and (schelog:ident? (car x) (car y)) - (schelog:ident? (cdr x) (cdr y)))) - (else #f))) - ((vector? x) - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) #f) - ((schelog:frozen-ref? y) #f) - (else (schelog:ident? x (schelog:deref y))))) - ((vector? y) - (schelog:ident? (vector->list x) - (vector->list y))) - (else #f))) - (else - (cond ((schelog:ref? y) - (cond ((schelog:unbound-ref? y) #f) - ((schelog:frozen-ref? y) #f) - (else (schelog:ident? x (schelog:deref y))))) - ((pair? y) #f) - ((vector? y) #f) - (else (eqv? x y))))))) + (cond ((schelog:unbound-ref? x) + (cond ((schelog:ref? y) + (cond ((schelog:unbound-ref? y) (eq? x y)) + ((schelog:frozen-ref? y) #f) + (else (schelog:ident? x (schelog:deref y))))) + (else #f))) + ((schelog:frozen-ref? x) + (cond ((schelog:ref? y) + (cond ((schelog:unbound-ref? y) #f) + ((schelog:frozen-ref? y) (eq? x y)) + (else (schelog:ident? x (schelog:deref y))))) + (else #f))) + (else (schelog:ident? (schelog:deref x) y)))) + ((pair? x) + (cond ((schelog:ref? y) + (cond ((schelog:unbound-ref? y) #f) + ((schelog:frozen-ref? y) #f) + (else (schelog:ident? x (schelog:deref y))))) + ((pair? y) + (and (schelog:ident? (car x) (car y)) + (schelog:ident? (cdr x) (cdr y)))) + (else #f))) + ((vector? x) + (cond ((schelog:ref? y) + (cond ((schelog:unbound-ref? y) #f) + ((schelog:frozen-ref? y) #f) + (else (schelog:ident? x (schelog:deref y))))) + ((vector? y) + (schelog:ident? (vector->list x) + (vector->list y))) + (else #f))) + (else + (cond ((schelog:ref? y) + (cond ((schelog:unbound-ref? y) #f) + ((schelog:frozen-ref? y) #f) + (else (schelog:ident? x (schelog:deref y))))) + ((pair? y) #f) + ((vector? y) #f) + (else (eqv? x y))))))) (define %== (lambda (x y) @@ -463,49 +466,49 @@ (lambda (s) (let ((dict '())) (let loop ((s s)) - (cond ((schelog:ref? s) - (cond ((or (schelog:unbound-ref? s) (schelog:frozen-ref? s)) - (let ((x (assq s dict))) - (if x (cdr x) - (let ((y (schelog:freeze-ref s))) - (set! dict (cons (cons s y) dict)) - y)))) - ;((schelog:frozen-ref? s) s) ;? - (else (loop (schelog:deref s))))) - ((pair? s) (cons (loop (car s)) (loop (cdr s)))) - ((vector? s) - (list->vector (map loop (vector->list s)))) - (else s)))))) + (cond ((schelog:ref? s) + (cond ((or (schelog:unbound-ref? s) (schelog:frozen-ref? s)) + (let ((x (assq s dict))) + (if x (cdr x) + (let ((y (schelog:freeze-ref s))) + (set! dict (cons (cons s y) dict)) + y)))) + ;((schelog:frozen-ref? s) s) ;? + (else (loop (schelog:deref s))))) + ((pair? s) (cons (loop (car s)) (loop (cdr s)))) + ((vector? s) + (list->vector (map loop (vector->list s)))) + (else s)))))) (define schelog:melt (lambda (f) (cond ((schelog:ref? f) - (cond ((schelog:unbound-ref? f) f) - ((schelog:frozen-ref? f) (schelog:thaw-frozen-ref f)) - (else (schelog:melt (schelog:deref f))))) - ((pair? f) - (cons (schelog:melt (car f)) (schelog:melt (cdr f)))) - ((vector? f) - (list->vector (map schelog:melt (vector->list f)))) - (else f)))) + (cond ((schelog:unbound-ref? f) f) + ((schelog:frozen-ref? f) (schelog:thaw-frozen-ref f)) + (else (schelog:melt (schelog:deref f))))) + ((pair? f) + (cons (schelog:melt (car f)) (schelog:melt (cdr f)))) + ((vector? f) + (list->vector (map schelog:melt (vector->list f)))) + (else f)))) (define schelog:melt-new (lambda (f) (let ((dict '())) (let loop ((f f)) - (cond ((schelog:ref? f) - (cond ((schelog:unbound-ref? f) f) - ((schelog:frozen-ref? f) - (let ((x (assq f dict))) - (if x (cdr x) - (let ((y (schelog:make-ref))) - (set! dict (cons (cons f y) dict)) - y)))) - (else (loop (schelog:deref f))))) - ((pair? f) (cons (loop (car f)) (loop (cdr f)))) - ((vector? f) - (list->vector (map loop (vector->list f)))) - (else f)))))) + (cond ((schelog:ref? f) + (cond ((schelog:unbound-ref? f) f) + ((schelog:frozen-ref? f) + (let ((x (assq f dict))) + (if x (cdr x) + (let ((y (schelog:make-ref))) + (set! dict (cons (cons f y) dict)) + y)))) + (else (loop (schelog:deref f))))) + ((pair? f) (cons (loop (car f)) (loop (cdr f)))) + ((vector? f) + (list->vector (map loop (vector->list f)))) + (else f)))))) (define schelog:copy (lambda (s) @@ -537,9 +540,9 @@ (lambda (g) (lambda (fk) (if (call-with-current-continuation - (lambda (k) - ((schelog:deref* g) (lambda (d) (k #f))))) - (fk 'fail) fk)))) + (lambda (k) + ((schelog:deref* g) (lambda (d) (k #f))))) + (fk 'fail) fk)))) ;assert, asserta @@ -548,42 +551,42 @@ %fail)) (define-syntax %assert - (syntax-rules (!) + (syntax-rules () ((%assert rel-name (v ...) ((a ...) subgoal ...) ...) - (set! rel-name - (let ((__old-rel rel-name) - (__new-addition (%rel (v ...) ((a ...) subgoal ...) ...))) - (lambda __fmls - (%or (apply __old-rel __fmls) - (apply __new-addition __fmls)))))))) - -(define-syntax %assert-a - (syntax-rules (!) - ((%assert-a rel-name (v ...) ((a ...) subgoal ...) ...) - (set! rel-name - (let ((__old-rel rel-name) - (__new-addition (%rel (v ...) ((a ...) subgoal ...) ...))) - (lambda __fmls - (%or (apply __new-addition __fmls) - (apply __old-rel __fmls)))))))) - -#;(define-macro %assert - (lambda (rel-name vv . cc) - `(set! ,rel-name - (let ((__old-rel ,rel-name) - (__new-addition (%rel ,vv ,@cc))) + (set! rel-name + (let ((__old-rel rel-name) + (__new-addition (%rel (v ...) ((a ...) subgoal ...) ...))) (lambda __fmls (%or (apply __old-rel __fmls) - (apply __new-addition __fmls))))))) + (apply __new-addition __fmls)))))))) -#;(define-macro %assert-a - (lambda (rel-name vv . cc) - `(set! ,rel-name - (let ((__old-rel ,rel-name) - (__new-addition (%rel ,vv ,@cc))) +(define-syntax %assert-a + (syntax-rules () + ((%assert-a rel-name (v ...) ((a ...) subgoal ...) ...) + (set! rel-name + (let ((__old-rel rel-name) + (__new-addition (%rel (v ...) ((a ...) subgoal ...) ...))) (lambda __fmls (%or (apply __new-addition __fmls) - (apply __old-rel __fmls))))))) + (apply __old-rel __fmls)))))))) + +#;(define-macro %assert + (lambda (rel-name vv . cc) + `(set! ,rel-name + (let ((__old-rel ,rel-name) + (__new-addition (%rel ,vv ,@cc))) + (lambda __fmls + (%or (apply __old-rel __fmls) + (apply __new-addition __fmls))))))) + +#;(define-macro %assert-a + (lambda (rel-name vv . cc) + `(set! ,rel-name + (let ((__old-rel ,rel-name) + (__new-addition (%rel ,vv ,@cc))) + (lambda __fmls + (%or (apply __new-addition __fmls) + (apply __old-rel __fmls))))))) ;set predicates @@ -594,13 +597,13 @@ (define-syntax %free-vars (syntax-rules () ((%free-vars (v ...) g) - (cons 'schelog:goal-with-free-vars - (cons (list v ...) g))))) + (cons 'schelog:goal-with-free-vars + (cons (list v ...) g))))) #;(define-macro %free-vars - (lambda (vv g) - `(cons 'schelog:goal-with-free-vars - (cons (list ,@vv) ,g)))) + (lambda (vv g) + `(cons 'schelog:goal-with-free-vars + (cons (list ,@vv) ,g)))) (define schelog:goal-with-free-vars? (lambda (x) @@ -619,38 +622,38 @@ (lambda (kons fvv lv goal bag) (lambda (fk) (call-with-current-continuation - (lambda (sk) - (let ((lv2 (cons fvv lv))) - (let* ((acc '()) - (fk-final - (lambda (d) - ;;(set! acc (reverse! acc)) - (sk ((schelog:separate-bags fvv bag acc) fk)))) - (fk-retry (goal fk-final))) - (set! acc (kons (schelog:deref* lv2) acc)) - (fk-retry 'retry)))))))) + (lambda (sk) + (let ((lv2 (cons fvv lv))) + (let* ((acc '()) + (fk-final + (lambda (d) + ;;(set! acc (reverse! acc)) + (sk ((schelog:separate-bags fvv bag acc) fk)))) + (fk-retry (goal fk-final))) + (set! acc (kons (schelog:deref* lv2) acc)) + (fk-retry 'retry)))))))) (define schelog:separate-bags (lambda (fvv bag acc) ;;(format #t "Accum: ~s~%" acc) (let ((bags (let loop ((acc acc) - (current-fvv #f) (current-bag '()) - (bags '())) + (current-fvv #f) (current-bag '()) + (bags '())) (if (null? acc) - (cons (cons current-fvv current-bag) bags) - (let ((x (car acc))) - (let ((x-fvv (car x)) (x-lv (cdr x))) - (if (or (not current-fvv) (equal? x-fvv current-fvv)) - (loop (cdr acc) x-fvv (cons x-lv current-bag) bags) - (loop (cdr acc) x-fvv (list x-lv) - (cons (cons current-fvv current-bag) bags))))))))) + (cons (cons current-fvv current-bag) bags) + (let ((x (car acc))) + (let ((x-fvv (car x)) (x-lv (cdr x))) + (if (or (not current-fvv) (equal? x-fvv current-fvv)) + (loop (cdr acc) x-fvv (cons x-lv current-bag) bags) + (loop (cdr acc) x-fvv (list x-lv) + (cons (cons current-fvv current-bag) bags))))))))) ;;(format #t "Bags: ~a~%" bags) (if (null? bags) (%= bag '()) - (let ((fvv-bag (cons fvv bag))) - (let loop ((bags bags)) - (if (null? bags) %fail - (%or (%= fvv-bag (car bags)) - (loop (cdr bags)))))))))) + (let ((fvv-bag (cons fvv bag))) + (let loop ((bags bags)) + (if (null? bags) %fail + (%or (%= fvv-bag (car bags)) + (loop (cdr bags)))))))))) (define %bag-of (schelog:make-bag-of cons)) (define %set-of (schelog:make-bag-of schelog:set-cons)) @@ -660,12 +663,12 @@ (define %bag-of-1 (lambda (x g b) (%and (%bag-of x g b) - (%= b (cons (_) (_)))))) + (%= b (cons (_) (_)))))) (define %set-of-1 (lambda (x g s) (%and (%set-of x g s) - (%= s (cons (_) (_)))))) + (%= s (cons (_) (_)))))) ;user interface @@ -680,42 +683,42 @@ (syntax-rules () ((%which (v ...) g) (%let (v ...) - (call-with-current-continuation - (lambda (__qk) - (set-box! schelog:*more-k* __qk) - (set-box! schelog:*more-fk* - ((schelog:deref* g) - (lambda (d) - (set-box! schelog:*more-fk* #f) - ((unbox schelog:*more-k*) #f)))) - ((unbox schelog:*more-k*) - (map (lambda (nam val) (list nam (schelog:deref* val))) - '(v ...) - (list v ...))))))))) - -#;(define-macro %which - (lambda (vv g) - `(%let ,vv (call-with-current-continuation (lambda (__qk) - (set! schelog:*more-k* __qk) - (set! schelog:*more-fk* - ((schelog:deref* ,g) - (lambda (d) - (set! schelog:*more-fk* #f) - (schelog:*more-k* #f)))) - (schelog:*more-k* + (set-box! schelog:*more-k* __qk) + (set-box! schelog:*more-fk* + ((schelog:deref* g) + (lambda (d) + (set-box! schelog:*more-fk* #f) + ((unbox schelog:*more-k*) #f)))) + ((unbox schelog:*more-k*) (map (lambda (nam val) (list nam (schelog:deref* val))) - ',vv - (list ,@vv)))))))) + '(v ...) + (list v ...))))))))) + +#;(define-macro %which + (lambda (vv g) + `(%let ,vv + (call-with-current-continuation + (lambda (__qk) + (set! schelog:*more-k* __qk) + (set! schelog:*more-fk* + ((schelog:deref* ,g) + (lambda (d) + (set! schelog:*more-fk* #f) + (schelog:*more-k* #f)))) + (schelog:*more-k* + (map (lambda (nam val) (list nam (schelog:deref* val))) + ',vv + (list ,@vv)))))))) (define %more (lambda () (call-with-current-continuation - (lambda (k) - (set-box! schelog:*more-k* k) - (if (unbox schelog:*more-fk*) ((unbox schelog:*more-fk*) 'more) - #f))))) + (lambda (k) + (set-box! schelog:*more-k* k) + (if (unbox schelog:*more-fk*) ((unbox schelog:*more-fk*) 'more) + #f))))) ;end of embedding code. The following are ;some utilities, written in Schelog @@ -723,42 +726,42 @@ (define %member (lambda (x y) (%let (xs z zs) - (%or - (%= y (cons x xs)) - (%and (%= y (cons z zs)) - (%member x zs)))))) + (%or + (%= y (cons x xs)) + (%and (%= y (cons z zs)) + (%member x zs)))))) (define %if-then-else (lambda (p q r) - (%cut-delimiter ! - (%or - (%and p ! q) - r)))) + (%cut-delimiter + (%or + (%and p ! q) + r)))) ;the above could also have been written in a more ;Prolog-like fashion, viz. #;'(define %member - (%rel ! (x xs y ys) - ((x (cons x xs))) - ((x (cons y ys)) (%member x ys)))) + (%rel ! (x xs y ys) + ((x (cons x xs))) + ((x (cons y ys)) (%member x ys)))) #;'(define %if-then-else - (%rel ! (p q r) - ((p q r) p ! q) - ((p q r) r))) + (%rel ! (p q r) + ((p q r) p ! q) + ((p q r) r))) (define %append - (%rel ! (x xs ys zs) - (('() ys ys)) - (((cons x xs) ys (cons x zs)) - (%append xs ys zs)))) + (%rel (x xs ys zs) + (('() ys ys)) + (((cons x xs) ys (cons x zs)) + (%append xs ys zs)))) (define %repeat ;;failure-driven loop - (%rel ! () - (()) - (() (%repeat)))) + (%rel () + (()) + (() (%repeat)))) ; deprecated names -- retained here for backward-compatibility @@ -769,12 +772,12 @@ #;(define %notunify %/=) #;(define-macro %cut - (lambda e - `(%cur-delimiter ,@e))) + (lambda e + `(%cur-delimiter ,@e))) #;(define-macro rel - (lambda e - `(%rel ,@e))) + (lambda e + `(%rel ,@e))) (define %eq %=:=) (define %gt %>) (define %ge %>=) @@ -788,8 +791,8 @@ #;(define-macro %exists (lambda (vv g) g)) #;(define-macro which - (lambda e - `(%which ,@e))) + (lambda e + `(%which ,@e))) (define more %more) ;end of file diff --git a/collects/schelog/schelog.scrbl b/collects/schelog/schelog.scrbl new file mode 100644 index 0000000000..23de1cbb03 --- /dev/null +++ b/collects/schelog/schelog.scrbl @@ -0,0 +1,1422 @@ +#lang scribble/manual +@(require scribble/eval + (for-syntax scheme) + (for-label schelog + (except-in scheme _))) + +@(define schelog-eval (make-base-eval)) +@(schelog-eval '(require schelog)) + +@title{@bold{Schelog}: Prolog-style logic programming in Scheme} + +@author{Dorai Sitaram} + +@margin-note{Adapted for Racket by Dorai Sitaram, John Clements, and Jay McCarthy.} + +@defmodule[schelog] + +Schelog is an @emph{embedding} of +Prolog-style logic programming in Scheme. ``Embedding'' +means you don't lose Scheme: You can use Prolog-style and +conventional Scheme code fragments alongside each other. +Schelog contains the full repertoire of Prolog features, +including meta-logical and second-order (``set'') +predicates, leaving out only those features that could more +easily and more efficiently be done with Scheme +subexpressions. + +The Schelog implementation uses the approach to logic +programming described in Felleisen @cite{mf:prolog} and +Haynes @cite{logick}. In contrast to earlier Lisp simulations of +Prolog @cite{campbell}, +which used explicit continuation +arguments to store failure (backtrack) information, the +Felleisen and Haynes model uses the implicit reified +continuations of Scheme as provided by the operator +@scheme[call-with-current-continuation] (aka @scheme[call/cc]). This +allows Schelog to be an @emph{embedding}, ie, logic +programming is not built as a new language on top of Scheme, +but is used alongside Scheme's other features. Both styles +of programming may be mixed to any extent that a project +needs. + +The Schelog user does not need to know about the +implementation mechanism or about @scheme[call/cc] and +continuations to get on with the business of +doing logic programming with Schelog. + +This text is a gentle introduction to Schelog syntax +and programming. It assumes a working knowledge of +Scheme and an awareness of, if not actual programming +experience with, Prolog. If you need assistance in +either language, you may consult +@cite["sicp" "tls" "tss" "eopl" "r5rs" "t-y-scheme"] for Scheme, and +@cite["bratko" "ok:prolog" "aop"] for Prolog. +There are doubtless many other excellent books and +online documents available. + +@table-of-contents[] + +@section[#:tag "simple"]{Simple Goals and Queries} + +Schelog objects are the same as Scheme objects. However, there +are two subsets of these objects that are of special +interest to Schelog: @emph{goals} and @emph{predicates}. We +will first look at some simple goals. +@secref{predicates} will introduce predicates and ways +of making complex goals using predicates. + +A goal is an object whose truth or falsity we can check. A +goal that turns out to be true is said to succeed. +A goal that turns out to be false is said to +fail. + +Two simple goals that are provided in Schelog are: +@schemeblock[ +%true +%fail +] + +The goal @scheme[%true] succeeds. The goal @scheme[%fail] +always fails. + +(The names of all Schelog primitive objects +start with @litchar{%}. This is to avoid clashes with the names +of conventional Scheme objects of related meaning. +User-created objects in Schelog are not required to +follow this convention.) + +A Schelog user can @emph{query} a goal by wrapping it in a +@scheme[%which]-form. + +@schemeblock[ +(%which () %true) +] + +evaluates to @schemeresult[()], indicating success, whereas: + +@schemeblock[ +(%which () %fail) +] + +evaluates to @scheme[#f], indicating failure. + +Note 1: The second subexpression of the @scheme[%which]-form +is the empty list @schemeresult[()]. Later (@secref{solving-goals}), +we will see @scheme[%which]es +with other lists as the second subform. + +Henceforth, we will use the notation: + +@interaction[(eval:alts E 'F)] + +to say that @scheme[E] @emph{evaluates to} @scheme[F]. Thus, + +@interaction[#:eval schelog-eval (%which () %true)] + +@section[#:tag "predicates"]{Predicates} + +More interesting goals are created by applying a special +kind of Schelog object called a @emph{predicate} (or +@emph{relation}) to other +Schelog objects. Schelog comes with some primitive +predicates, such as the arithmetic operators +@scheme[%=:=] and @scheme[%<], +standing for arithmetic ``equal'' and ``less than'' +respectively. For example, the following are some goals +involving these predicates: + +@interaction[ + #:eval schelog-eval + (%which () (%=:= 1 1)) + (%which () (%< 1 2)) + (%which () (%=:= 1 2)) + (%which () (%< 1 1)) + ] + +Other arithmetic predicates are +@scheme[%>] (``greater than''), +@scheme[%<=] (``less than or equal''), +@scheme[%>=] (``greater than or equal''), and +@scheme[%=/=] (``not equal''). + +Schelog predicates are not to be confused with conventional +Scheme predicates (such as @scheme[<] and @scheme[=]). Schelog +predicates, when applied to arguments, produce goals +that +may either succeed or fail. Scheme predicates, when applied +to arguments, yield a boolean value. Henceforth, we will +use the term ``predicate'' to mean Schelog predicates. +Conventional predicates will be explicitly called ``Scheme +predicates''. + +@subsection[#:tag "facts"]{Predicates Introducing Facts} + +Users can create their own predicates using the Schelog form +@scheme[%rel]. For example, let's +define the predicate @scheme[%knows]: + +@schemeblock+eval[#:eval schelog-eval +(define %knows + (%rel () + [('Odysseus 'TeX)] + [('Odysseus 'Scheme)] + [('Odysseus 'Prolog)] + [('Odysseus 'Penelope)] + [('Penelope 'TeX)] + [('Penelope 'Prolog)] + [('Penelope 'Odysseus)] + [('Telemachus 'TeX)] + [('Telemachus 'calculus)])) +] + +The expression has the expected meaning. Each +@emph{clause} in the @scheme[%rel] establishes a @emph{fact}: +Odysseus +knows TeX, Telemachus knows calculus, &c. In general, if we +apply the predicate to the arguments in any one of its +clauses, we will get a successful goal. Thus, since +@scheme[%knows] has a clause that reads +@scheme[[('Odysseus 'TeX)]], the goal +@scheme[(%knows 'Odysseus 'TeX)] +will be true. + +We can now get answers for the following types of queries: + +@interaction[#:eval schelog-eval +(%which () + (%knows 'Odysseus 'TeX)) +(%which () + (%knows 'Telemachus 'Scheme)) +] + +@subsection[#:tag "rules"]{Predicates with Rules} + +Predicates can be more complicated than the above bald +recitation of facts. The predicate clauses can be @emph{rules}, eg, + +@schemeblock+eval[#:eval schelog-eval +(define %computer-literate + (%rel (person) + [(person) + (%knows person 'TeX) + (%knows person 'Scheme)] + [(person) + (%knows person 'TeX) + (%knows person 'Prolog)])) +] + +This defines the predicate +@scheme[%computer-literate] in +terms of the predicate @scheme[%knows]. In effect, a person is +defined as computer-literate if they know TeX and +Scheme, @emph{or} TeX and Prolog. + +Note that this use of +@scheme[%rel] employs a local @emph{logic variable} called @scheme[_person]. +In general, a @scheme[%rel]-expression can have a list of symbols +as its second subform. These name new logic variables that +can be used within the body of the @scheme[%rel]. + +The following query can now be answered: + +@interaction[#:eval schelog-eval +(%which () + (%computer-literate 'Penelope)) +] + +Since Penelope knows TeX and Prolog, she is computer-literate. + +@subsection[#:tag "solving-goals"]{Solving Goals} + +The above queries are yes/no questions. Logic programming +allows more: We can formulate a goal with @emph{uninstantiated} +logic variables and then ask the querying process to +provide, if possible, values for these variables that cause +the goal to succeed. For instance, the query: + +@interaction[#:eval schelog-eval +(%which (what) + (%knows 'Odysseus what)) +] + +asks for an instantiation of the logic variable @scheme[_what] +that satisfies the goal @scheme[(%knows 'Odysseus what)]. +In other words, we are asking, ``What does Odysseus know?'' + +Note that this use of @scheme[%which] --- like @scheme[%rel] +in the definition of @scheme[%computer-literate] --- +uses a local logic +variable, @scheme[_what]. In general, the second subform of +@scheme[%which] can be a list of local logic variables. The +@scheme[%which]-query returns an answer that is a list of +bindings, one for each logic variable mentioned in its +second subform. Thus, + +@interaction[#:eval schelog-eval +(%which (what) + (%knows 'Odysseus what)) +] + +But that is not all that wily Odysseus knows. Schelog +provides a zero-argument procedure (``thunk'') called +@scheme[%more] +that @emph{retries} the goal in the last +@scheme[%which]-query for a different solution. + +@interaction[#:eval schelog-eval +(%more) +] + +We can keep pumping for more solutions: + +@interaction[#:eval schelog-eval +(%more) +(%more) +(%more) +] + +The final @scheme[#f] shows that there are no more +solutions. This is because there are no more clauses in the +@scheme[%knows] predicate that list Odysseus as knowing anything +else. + +@subsection[#:tag "assert"]{Asserting Extra Clauses} + +We can add more clauses to a predicate after it has already +been defined with a @scheme[%rel]. Schelog provides the +@scheme[%assert] form for this purpose. Eg, + +@schemeblock+eval[#:eval schelog-eval +(%assert %knows () + [('Odysseus 'archery)]) +] + +tacks on a new clause at the end of the existing clauses +of the @scheme[%knows] +predicate. Now, the query: + +@interaction[#:eval schelog-eval +(%which (what) + (%knows 'Odysseus what)) +] + +gives TeX, Scheme, Prolog, and Penelope, as before, but +a subsequent @scheme[(%more)] yields a new result: +@interaction-eval[#:eval schelog-eval (begin (%more) (%more) (%more))] +@interaction[#:eval schelog-eval +(%more) +] + +The Schelog form @scheme[%assert-a] is similar to @scheme[%assert] but +adds clauses @emph{before} any of the current clauses. + +Both @scheme[%assert] and @scheme[%assert-a] assume that the variable +they are adding to already names a predicate (presumably +defined using @scheme[%rel]). +In order to allow defining a predicate entirely through +@scheme[%assert]s, Schelog provides an empty predicate value +@scheme[%empty-rel]. @scheme[%empty-rel] takes any number of arguments +and always fails. A typical use of the +@scheme[%empty-rel] and @scheme[%assert] combination: + +@schemeblock+eval[#:eval schelog-eval +(define %parent %empty-rel) + +(%assert %parent () + [('Laertes 'Odysseus)]) + +(%assert %parent () + [('Odysseus 'Telemachus)] + [('Penelope 'Telemachus)]) +] + +(Schelog does not provide a predicate for @emph{retracting} +assertions, since we can keep track of older versions of +predicates using conventional Scheme features (@scheme[let] and @scheme[set!]).) + +@subsection[#:tag "local-vars"]{Local Variables} + +The local logic variables of @scheme[%rel]- and +@scheme[%which]-expressions are in reality introduced by the +Schelog syntactic form called @scheme[%let]. (@scheme[%rel] and +@scheme[%which] are macros written using @scheme[%let].) + +@scheme[%let] introduces new lexically scoped logic variables. +Supposing, instead of + +@interaction[#:eval schelog-eval +(%which (what) + (%knows 'Odysseus what)) +] + +we had asked + +@interaction[#:eval schelog-eval +(%let (what) + (%which () + (%knows 'Odysseus what))) +] + +This query, too, succeeds five times, since +Odysseus knows five things. However, @scheme[%which] emits +bindings only for the local variables that @emph{it} +introduces. Thus, this query emits @schemeresult[()] five times before +@scheme[(%more)] finally returns @scheme[#f]. + +@section[#:tag "scheme-w-schelog"]{Using Conventional Scheme Expressions in Schelog} + +The arguments of Schelog predicates can be any Scheme +objects. In particular, composite structures such as lists, +vectors and strings can be used, as also Scheme expressions +using the full array of Scheme's construction and +decomposition operators. For instance, consider the +following goal: + +@schemeblock[ +(%member x '(1 2 3)) +] + +Here, @scheme[%member] is a predicate, @scheme[x] is a logic +variable, and @scheme['(1 2 3)] is a structure. Given a suitably +intuitive definition for @scheme[%member], the above goal +succeeds for @scheme[x] = @schemeresult[1], @schemeresult[2], and @schemeresult[3]. + +Now to defining predicates like @scheme[%member]: + +@schemeblock[ +(define %member + (%rel (x y xs) + [(x (cons x xs))] + [(x (cons y xs)) + (%member x xs)])) +] + +Ie, @scheme[%member] is defined with three local variables: +@scheme[x], @scheme[y], @scheme[xs]. It has two +clauses, identifying the two ways of determining membership. + +The first clause of @scheme[%member] states a fact: For any +@scheme[x], @scheme[x] is a member of a list whose head is also @scheme[x]. + +The second clause of @scheme[%member] is a rule: @scheme[x] is a +member of a list if we can show that it is a member of the +@emph{tail} of that list. In other words, the original +@scheme[%member] goal is translated into a @emph{sub}goal, which is also +a @scheme[%member] goal. + +Note that the variable @scheme[y] in the definition of +@scheme[%member] occurs only once in the second clause. As such, +it doesn't need you to make the effort of naming it. (Names +help only in matching a second occurrence to a first.) Schelog +lets you use the expression @scheme[(_)] to denote an anonymous +variable. (Ie, @scheme[_] is a thunk that generates a fresh +anonymous variable at each call.) The predicate @scheme[%member] can be +rewritten as + +@schemeblock[ +(define %member + (%rel (x xs) + [(x (cons x (_)))] + [(x (cons (_) xs)) + (%member x xs)])) +] + +@subsection[#:tag "constructors"]{Constructors} + +We can use constructors --- Scheme procedures for creating +structures --- to simulate data types in Schelog. For +instance, let's define a natural-number data-type where +@scheme[0] denotes zero, and @scheme[(succ x)] denotes the natural number +whose immediate predecessor is @scheme[x]. The constructor +@scheme[succ] can +be defined in Scheme as: + +@schemeblock+eval[#:eval schelog-eval +(define succ + (lambda (x) + (vector 'succ x))) +] + +Addition and multiplication can be defined as: + +@schemeblock+eval[#:eval schelog-eval +(define %add + (%rel (x y z) + [(0 y y)] + [((succ x) y (succ z)) + (%add x y z)])) + +(define %times + (%rel (x y z z1) + [(0 y 0)] + [((succ x) y z) + (%times x y z1) + (%add y z1 z)])) +] + +We can do a lot of arithmetic with this in place. For +instance, the factorial predicate looks like: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y y1) + [(0 (succ 0))] + [((succ x) y) + (%factorial x y1) + (%times (succ x) y1 y)])) +] + +@subsection[#:tag "is"]{@scheme[\%is]} + +The above is a very inefficient way to do arithmetic, +especially when the underlying language Scheme offers +excellent arithmetic facilities (including a comprehensive +number ``tower'' and exact rational arithmetic). One +problem with using Scheme calculations directly in Schelog +clauses is that the expressions used may contain logic +variables that need to be dereferenced. Schelog provides +the predicate @scheme[%is] that takes care of this. The goal + +@schemeblock[ +(%is _X _E) +] + +unifies @scheme[_X] with the value of @scheme[_E] considered as a +Scheme expression. @scheme[_E] can have logic variables, but +usually they should at least be bound, as unbound variables +may not be palatable values to the Scheme operators used in +@scheme[_E]. + +We can now directly use the numbers of Scheme to write a +more efficient @scheme[%factorial] predicate: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y x1 y1) + [(0 1)] + [(x y) (%is x1 (- x 1)) + (%factorial x1 y1) + (%is y (* y1 x))])) +] + +A price that this efficiency comes with is that we can +use @scheme[%factorial] only with its first argument already +instantiated. In many cases, this is not an unreasonable +constraint. In fact, given this limitation, there is +nothing to prevent us from using Scheme's factorial +directly: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y) + [(x y) + (%is y (scheme-factorial + x))])) +] + +or better yet, ``in-line'' any calls to @scheme[%factorial] with +@scheme[%is]-expressions calling @scheme[scheme-factorial], where the +latter is defined in the usual manner: + +@schemeblock+eval[#:eval schelog-eval +(define scheme-factorial + (lambda (n) + (if (= n 0) 1 + (* n (factorial + (- n 1)))))) +] + +@subsection[#:tag "lexical-scoping"]{Lexical Scoping} + +One can use Scheme's lexical scoping to enhance predicate +definition. Here is a list-reversal predicate defined using +a hidden auxiliary predicate: + +@schemeblock+eval[#:eval schelog-eval +(define %reverse + (letrec + ([revaux + (%rel (x y z w) + [('() y y)] + [((cons x y) z w) + (revaux y + (cons x z) w)])]) + (%rel (x y) + [(x y) (revaux x '() y)]))) +] + +@scheme[(revaux _X _Y _Z)] uses @scheme[_Y] as an accumulator for +reversing @scheme[_X] into @scheme[_Z]. (@scheme[_Y] starts out as @schemeresult[()]. +Each head of @scheme[_X] is @scheme[cons]ed on to @scheme[_Y]. Finally, when +@scheme[_X] has wound down to @schemeresult[()], @scheme[_Y] contains the reversed +list and can be returned as @scheme[_Z].) + +@scheme[revaux] is used purely as a helper predicate for +@scheme[%reverse], and so it can be concealed within a lexical +contour. We use @scheme[letrec] instead of @scheme[let] because +@scheme[revaux] is a recursive procedure. + +@subsection[#:tag "type-predicates"]{Type Predicates} + +Schelog provides a couple of predicates that let the user +probe the type of objects. + +The goal +@schemeblock[ +(%constant _X) +] + +succeeds if @scheme[_X] is an @emph{atomic} object, ie, not a +list or vector. + +The predicate @scheme[%compound], the negation of @scheme[%constant], +checks if its argument is indeed a list or a vector. + +The above are merely the logic-programming equivalents of +corresponding Scheme predicates. Users can use the +predicate @scheme[%is] and Scheme predicates to write more type +checks in Schelog. Thus, to test if @scheme[_X] is a string, the +following goal could be used: + +@schemeblock[ +(%is #t (string? _X)) +] + +User-defined Scheme predicates, in addition to primitive Scheme +predicates, can be thus imported. + +@section[#:tag "backtracking"]{Backtracking} + +It is helpful to go into the following evaluation (@secref{rules}) +in a +little detail: + +@schemeblock+eval[#:eval schelog-eval +(%which () + (%computer-literate 'Penelope)) +] + +The starting goal +is: + +@(define goal litchar) +@schemeblock[ +G0 = (%computer-literate Penelope) +] + +(I've taken out the quote because @schemeresult[Penelope] is the result +of evaluating @scheme['Penelope].) + +Schelog tries to match this with the head of the first +clause of @scheme[%computer-literate]. It succeeds, generating a +binding @scheme[[person Penelope]]. + +But this means it now has two new goals --- @emph{subgoals} +--- to solve. These are the goals in the body of the +matching clause, with the logic variables substituted by +their instantiations: + +@schemeblock[ +G1 = (%knows Penelope TeX) +G2 = (%knows Penelope Scheme) +] + +For @goal{G1}, Schelog attempts matches with the clauses of +@scheme[%knows], and succeeds at the fifth try. (There are no +subgoals in this case, because the bodies of these ``fact'' +clauses are empty, in contrast to the ``rule'' clauses of +@scheme[%computer-literate].) +Schelog then tries to solve @goal{G2} against the clauses of +@scheme[%knows], and since there is no clause stating that +Penelope knows Scheme, it fails. + +All is not lost though. Schelog now @emph{backtracks} to the +goal that was solved just before, viz., @goal{G1}. It +@emph{retries} @goal{G1}, ie, tries to solve it in a +different way. +This entails searching down the previously unconsidered +@scheme[%knows] +clauses for @goal{G1}, ie, the sixth onwards. Obviously, +Schelog fails again, because the fact that Penelope knows +TeX occurs only once. + +Schelog now backtracks to the goal before @goal{G1}, ie, +@goal{G0}. We abandon the current successful match with the +first clause-head of @scheme[%computer-literate], and try the +next clause-head. Schelog succeeds, again producing a binding +@scheme[[person Penelope]], and two new subgoals: + +@schemeblock[ +G3 = (%knows Penelope TeX) +G4 = (%knows Penelope Prolog) +] + +It is now easy to trace that Schelog finds both @goal{G3} and @goal{G4} to be +true. Since both of @goal{G0}'s subgoals are true, @goal{G0} is +itself considered true. And this is what Schelog reports. The +interested reader can now trace why the +following query has a different denouement: + +@interaction[#:eval schelog-eval +(%which () + (%computer-literate 'Telemachus)) +] + +@section[#:tag "unification"]{Unification} + +When we say that a goal matches with a clause-head, we mean +that the predicate and argument positions line up. Before +making this comparison, Schelog dereferences all already +bound logic variables. The resulting structures are then +compared to see if they are recursively identical. Thus, +@scheme[1] unifies with @scheme[1], and @scheme[(list 1 2)] with @scheme['(1 2)]; but @scheme[1] and +@scheme[2] do not unify, and neither do @scheme['(1 2)] and @scheme['(1 3)]. + +In general, there could be quite a few uninstantiated logic +variables in the compared objects. Unification will then +endeavor to find the most natural way of binding these +variables so that we arrive at structurally identical +objects. Thus, @scheme[(list _x 1)], where @scheme[_x] is an unbound logic +variable, unifies with @scheme['(0 1)], producing the +binding +@scheme[[_x 0]]. + +Unification is thus a goal, and Schelog makes the unification predicate +available to the user as @scheme[%=]. Eg, + +@interaction[#:eval schelog-eval +(%which (x) + (%= (list x 1) '(0 1))) +] + +Schelog also provides the predicate @scheme[%/=], the @emph{negation} of +@scheme[%=]. @scheme[(%/= _X _Y)] succeeds if and only if @scheme[_X] does +@emph{not} unify with @scheme[_Y]. + +Unification goals constitute the basic subgoals that all +Schelog goals devolve to. A goal succeeds because all the +eventual unification subgoals that it decomposes to in at +least one of its subgoal-branching succeeded. It fails +because every possible subgoal-branching was thwarted by the +failure of a crucial unification subgoal. + +Going back to the example in @secref{backtracking}, the goal +@scheme[(%computer-literate 'Penelope)] succeeds because +(a) it unified with +@scheme[(%computer-literate person)]; and then (b) with the binding +@scheme[[person Penelope]] in place, @scheme[(%knows person 'TeX)] +unified with @scheme[(%knows 'Penelope 'TeX)] and +@scheme[(%knows person 'Prolog)] unified with @scheme[(%knows 'Penelope 'Prolog)]. + +In contrast, the goal @scheme[(%computer-literate 'Telemachus)] +fails because, with @scheme[[person Telemachus]], +the subgoals @scheme[(%knows person 'Scheme)] and +@scheme[(%knows person 'Prolog)] have no facts they can +unify with. + +@subsection{The Occurs Check} + +A robust unification algorithm uses the @deftech{occurs check}, which ensures that a logic variable +isn't bound to a structure that contains itself. +Not performing the check can cause the unification +to go into an infinite loop in some cases. On the +other hand, performing the occurs check greatly +increases the time taken by unification, even in cases +that wouldn't require the check. + +Schelog uses the global parameter +@scheme[schelog-use-occurs-check?] to decide whether to +use the occurs check. By default, this variable is +@scheme[#f], ie, Schelog disables the occurs check. To +enable the check, + +@schemeblock[ +(schelog-use-occurs-check? #t) +] + +@section[#:tag "and-or"]{Conjuctions and Disjunctions} + +Goals may be combined using the forms @scheme[%and] +and @scheme[%or] +to form compound goals. (For @scheme[%not], see @secref{not}.) +Eg, + +@interaction[#:eval schelog-eval +(%which (x) + (%and (%member x '(1 2 3)) + (%< x 3))) +] + +gives solutions for @scheme[_x] that satisfy both the +argument goals of the @scheme[%and]. +Ie, @scheme[_x] should both be a member of @scheme['(1 2 3)] +@emph{and} be less than @scheme[3]. Typing @scheme[(%more)] gives another solution: + +@interaction[#:eval schelog-eval +(%more) +(%more) +] + +There are no more solutions, because @scheme[[x 3]] satisfies +the first but not the second goal. + +Similarly, the query + +@interaction[#:eval schelog-eval +(%which (x) + (%or (%member x '(1 2 3)) + (%member x '(3 4 5)))) +] + +lists all @scheme[_x] that are members of either list. + +@interaction[#:eval schelog-eval +(%more) +(%more) +(%more) +(%more) +(%more) +] + +(Yes, @scheme[([x 3])] is listed twice.) + +We can rewrite the predicate @scheme[%computer-literate] +from @secref{rules} using @scheme[%and] and @scheme[%or]: + +@schemeblock+eval[#:eval schelog-eval +(define %computer-literate + (%rel (person) + [(person) + (%or + (%and (%knows person + 'TeX) + (%knows person + 'Scheme)) + (%and (%knows person + 'TeX) + (%knows person + 'Prolog)))])) +] + +Or, more succinctly: + +@schemeblock+eval[#:eval schelog-eval +(define %computer-literate + (%rel (person) + [(person) + (%and (%knows person + 'TeX) + (%or (%knows person + 'Scheme) + (%knows person + 'Prolog)))])) +] + +We can even dispense with the @scheme[%rel] altogether: + +@schemeblock+eval[#:eval schelog-eval +(define %computer-literate + (lambda (person) + (%and (%knows person + 'TeX) + (%or (%knows person + 'Scheme) + (%knows person + 'Prolog))))) +] + +This last looks like a conventional Scheme predicate +definition, and is arguably +the most readable format for a Scheme programmer. + +@section[#:tag "lv-manip"]{Manipulating Logic Variables} + +Schelog provides special predicates for probing logic +variables, without risking their getting bound. + +@subsection[#:tag "var"]{Checking for Variables} + +The goal + +@schemeblock[ +(%== _X _Y) +] + +succeeds if @scheme[_X] and @scheme[_Y] are @emph{identical} objects. This +is not quite the unification predicate @scheme[%=], for @scheme[%==] +doesn't touch unbound objects the way @scheme[%=] does. Eg, +@scheme[%==] will not equate an unbound logic variable with a +bound one, nor will it equate two unbound logic variables +unless they are the @emph{same} variable. + +The predicate @scheme[%/==] is the negation of @scheme[%==]. + +The goal + +@schemeblock[ +(%var _X) +] + +succeeds if @scheme[_X] isn't completely bound --- ie, it has at +least one unbound logic variable in its innards. + +The predicate @scheme[%nonvar] is the negation of @scheme[%var]. + +@subsection[#:tag "freeze"]{Preserving Variables} + +Schelog lets the user protect a term with variables from +unification by allowing that term to be treated as a +(completely) bound object. The predicates provided for this +purpose are +@scheme[%freeze], +@scheme[%melt], @scheme[%melt-new], and @scheme[%copy]. + +The goal + +@schemeblock[ +(%freeze _S _F) +] + +unifies @scheme[_F] to the frozen version of @scheme[_S]. Any lack +of bindings in @scheme[_S] are preserved no matter how much you +toss @scheme[_F] about. + +The goal + +@schemeblock[ +(%melt _F _S) +] + +retrieves the object frozen in @scheme[_F] into @scheme[_S]. + +The goal + +@schemeblock[ +(%melt-new _F _S) +] + +is similar to @scheme[%melt], +except that when @scheme[_S] is made, the unbound variables in +@scheme[_F] are replaced by brand-new unbound variables. + +The goal + +@schemeblock[ +(%copy _S _C) +] + +is an abbreviation for @scheme[(%freeze _S _F)] +followed by @scheme[(%melt-new _F _C)]. + +@section[#:tag "cut"]{The Cut (@scheme[!])} + +The cut (called @scheme[!]) is a special goal that is used to +prune backtracking options. Like the @scheme[%true] goal, the +cut goal too succeeds, when accosted by the Schelog +subgoaling engine. However, when a further subgoal down the +line fails, and time comes to retry the cut goal, Schelog +will refuse to try alternate clauses for the predicate in +whose definition the cut occurs. In other words, the cut +causes Schelog to commit to all the decisions made from the +time that the predicate was selected to match a subgoal till +the time the cut was satisfied. + +For example, consider again the @scheme[%factorial] +predicate, as defined in @secref{is}: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y x1 y1) + [(0 1)] + [(x y) (%is x1 (- x 1)) + (%factorial x1 y1) + (%is y (* y1 x))])) +] + +Clearly, + +@interaction[#:eval schelog-eval +(%which () + (%factorial 0 1)) +(%which (n) + (%factorial 0 n)) +] + +But what if we asked for @scheme[(%more)] for either query? +Backtracking will try +the second clause of @scheme[%factorial], and sure enough the +clause-head unifies, producing binding @scheme[[x 0]]. +We now get three subgoals. Solving the first, we get @scheme[[x1 -1]], and then we have to solve @scheme[(%factorial -1 y1)]. It +is easy to see there is no end to this, as we fruitlessly +try to get the factorials of numbers that get more and more +negative. + +If we placed a cut at the first clause: + +@schemeblock[ +... +[(0 1) !] +... +] + +the attempt to find more solutions for @scheme[(%factorial 0 1)] is nipped in the bud. + +Calling @scheme[%factorial] with a @emph{negative} number would still cause an +infinite loop. To take care of that problem as well, we +use another cut: + +@schemeblock+eval[#:eval schelog-eval +(define %factorial + (%rel (x y x1 y1) + [(0 1) !] + [(x y) (%< x 0) ! %fail] + [(x y) (%is x1 (- x 1)) + (%factorial x1 y1) + (%is y (* y1 x))])) +] + +@interaction[#:eval schelog-eval +(%which () + (%factorial 0 1)) +(%more) +(%which () + (%factorial -1 1)) +] + +Using @emph{raw} cuts as above can get very confusing. For this +reason, it is advisable to use it hidden away in +well-understood abstractions. Two such common abstractions +are the conditional and negation. + +@subsection[#:tag "if-then-else"]{Conditional Goals} + +An ``if ... then ... else ...'' predicate can be defined +as follows + +@schemeblock+eval[#:eval schelog-eval +(define %if-then-else + (%rel (p q r) + [(p q r) p ! q] + [(p q r) r])) +] + +(Note that for the first time we have predicate arguments that +are themselves goals.) + +Consider the goal + +@schemeblock[ +G0 = (%if-then-else Gbool Gthen Gelse) +] + +We first unify @goal{G0} with the first clause-head, +giving +@scheme[[p Gbool]], @scheme[[q Gthen]], @scheme[[r Gelse]]. @goal{Gbool} can +now either succeed or fail. + +Case 1: If @goal{Gbool} fails, backtracking will cause the +@goal{G0} to unify with the second clause-head. @scheme[r] is bound +to @goal{Gelse}, and so @goal{Gelse} is tried, as expected. + +Case 2: If @goal{Gbool} succeeds, the cut commits to this +clause of the @scheme[%if-then-else]. We now try @goal{Gthen}. If +@goal{Gthen} should now fail --- or even if we simply retry for +more solutions --- we are guaranteed that the second +clause-head will not be tried. If it were not for the cut, +@goal{G0} would attempt to unify with the second clause-head, which will +of course succeed, and @goal{Gelse} @emph{will} be tried. + +@subsection[#:tag "not"]{Negation as Failure} + +Another common abstraction using the cut is @emph{negation}. +The negation of goal @goal{G} is defined as @scheme[(%not G)], where +the predicate @scheme[%not] is defined as follows: + +@schemeblock+eval[#:eval schelog-eval +(define %not + (%rel () + [(g) g ! %fail] + [(g) %true])) +] + +Thus, @scheme[g]'s negation is deemed a failure if @scheme[g] +succeeds, and a success if @scheme[g] fails. This is of course +confusing goal failure with falsity. In some cases, this +view of negation is actually helpful. + +@section[#:tag "set-of"]{Set Predicates} + +The goal + +@schemeblock[ +(%bag-of _X _G _Bag) +] + +unifies with @scheme[_Bag] the list of all instantiations of +@scheme[_X] for which @scheme[_G] succeeds. Thus, the following query +asks for all the things known --- ie, the collection of things +such that someone knows them: + +@interaction[#:eval schelog-eval +(%which (things-known) + (%let (someone x) + (%bag-of x (%knows someone x) + things-known))) +] + +This is the only solution for this goal: + +@interaction[#:eval schelog-eval +(%more) +] + +Note that some things --- eg, TeX --- are enumerated +more than once. This is because more than one person knows +TeX. To remove duplicates, use the predicate +@scheme[%set-of] +instead of @scheme[%bag-of]: + +@interaction[#:eval schelog-eval +(%which (things-known) + (%let (someone x) + (%set-of x (%knows someone x) + things-known))) +] + +In the above, the free variable @scheme[_someone] in the +@scheme[%knows]-goal is used as if it +were existentially quantified. In contrast, Prolog's +versions of +@scheme[%bag-of] and @scheme[%set-of] fix it for each solution of the +set-predicate goal. We can do it too with some additional +syntax that identifies the free variable. +Eg, + +@interaction[#:eval schelog-eval +(%which (someone things-known) + (%let (x) + (%bag-of x + (%free-vars (someone) + (%knows someone x)) + things-known))) +] + +The bag of things known by @emph{one} someone is +returned. That someone is Odysseus. The query can be +retried for more solutions, each listing the things known by +a different someone: + +@interaction[#:eval schelog-eval +(%more) +(%more) +(%more) +(%more) +] + +Schelog also provides two variants of these set predicates, +viz., @scheme[%bag-of-1] and @scheme[%set-of-1]. These act like @scheme[%bag-of] +and @scheme[%set-of] but fail if the resulting bag or set is empty. + +@section[#:tag "glossary"]{Glossary of Schelog Primitives} + +@; XXX any/c should be unifiable? +@; XXX logic-variable? goal? answer? + +@(define-syntax (defpred stx) + (syntax-case stx () + [(_ (id arg ...) pre ...) + (syntax/loc stx + (defproc (id arg ...) + goal? + pre ...))])) +@(define-syntax-rule (defgoal id pre ...) + (defthing id goal? pre ...)) + +@defpred[(%/= [E1 any/c] [E2 any/c])]{@scheme[%/=] is the negation of @scheme[%=]. +The goal @scheme[(%/= E1 E2)] succeeds if @scheme[E1] can not be unified +with @scheme[E2].} + +@defpred[(%/== [E1 any/c] [E2 any/c])]{ +@scheme[%/==] is the negation of @scheme[%==]. +The goal @scheme[(%/== E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are not +identical.} + +@defpred[(%< [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%< E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is less than @scheme[E2].} + +@defpred[(%<= [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%<= E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is less than or equal to @scheme[E2].} + +@defpred[(%= [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%= E1 E2)] succeeds if @scheme[E1] can be unified with +@scheme[E2]. Any resulting bindings for logic variables are kept.} + +@defpred[(%=/= [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%=/= E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is not equal to @scheme[E2].} + +@defpred[(%=:= [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%=:= E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is equal to @scheme[E2].} + +@defpred[(%== [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%== E1 E2)] succeeds if @scheme[E1] is @emph{identical} +to @scheme[E2]. They should be structurally equal. If containing +logic variables, they should have the same variables in the +same position. Unlike a @scheme[%=]-call, this goal will not bind +any logic variables.} + +@defpred[(%> [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%> E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is greater than @scheme[E2].} + +@defpred[(%>= [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%>= E1 E2)] succeeds if @scheme[E1] and @scheme[E2] are bound to +numbers and @scheme[E1] is greater than or equal to @scheme[E2].} + +@defform[(%and G ...) #:contracts ([G goal?])]{ +The goal @scheme[(%and G ...)] succeeds if all the goals +@scheme[G], ..., succeed.} + +@defpred[(%append [E1 any/c] [E2 any/c] [E3 any/c])]{ +The goal @scheme[(%append E1 E2 E3)] succeeds if @scheme[E3] is unifiable +with the list obtained by appending @scheme[E1] and @scheme[E2].} + +@defform[(%assert Pname (V ...) clause ...) + #:contracts ([Pname identifier?] + [V identifier?])]{ +Adds the clauses +@scheme[clauses], ..., to the @emph{end} of the predicate that is the value of +the Scheme variable @scheme[Pname]. The variables @scheme[V], ..., are +local logic variables for @scheme[clause], ....} + +@defform[(%assert-a Pname (V ...) clause ...) + #:contracts ([Pname identifier?] + [V identifier?])]{ +Like @scheme[%assert], but adds the new clauses to the @emph{front} +of the existing predicate.} + +@defpred[(%bag-of [E1 any/c] [G goal?] [E2 any/c])]{ +The goal @scheme[(%bag-of E1 G E2)] unifies with @scheme[E2] the @emph{bag} +(multiset) +of all the +instantiations of @scheme[E1] for which goal @scheme[G] succeeds.} + +@defpred[(%bag-of-1 [E1 any/c] [G goal?] [E2 any/c])]{ +Similar to @scheme[%bag-of], but fails if the bag is empty.} + +@defpred[(%compound [E any/c])]{ +The goal @scheme[(%compound E)] succeeds if @scheme[E] is a non-atomic +structure, ie, a vector or a list.} + +@defpred[(%constant [E any/c])]{ +The goal @scheme[(%compound E)] succeeds if @scheme[E] is an atomic +structure, ie, not a vector or a list.} + +@defpred[(%copy [F any/c] [S any/c])]{ +The goal @scheme[(%copy F S)] unifies with @scheme[S] a copy of the +frozen structure in @scheme[F].} + +@defpred[(%empty-rel [E any/c] ...)]{ +The goal @scheme[(%empty-rel E ...)] always fails. The @emph{value} +@scheme[%empty-rel] is used as a starting value for predicates +that can later be enhanced with @scheme[%assert] and @scheme[%assert-a].} + +@defgoal[%fail]{ +The goal @scheme[%fail] always fails.} + +@defform[(%free-vars (V ...) G) + #:contracts ([V identifier?] + [G goal?])]{ +Identifies +the occurrences of the variables @scheme[V], ..., in goal +@scheme[G] as free. It is used to avoid existential quantification +in calls to set predicates (@scheme[%bag-of], @scheme[%set-of], &c.).} + +@defpred[(%freeze [S any/c] [F any/c])]{ +The goal @scheme[(%freeze S F)] unifies with @scheme[F] a new frozen +version of the structure in @scheme[S]. Freezing implies that all +the unbound variables are preserved. @scheme[F] can henceforth be +used as @emph{bound} object with no fear of its variables +getting bound by unification.} + +@defpred[(%if-then-else [G1 goal?] [G2 goal?] [G3 goal?])]{ +The goal @scheme[(%if-then-else G1 G2 G3)] tries @scheme[G1] first: if it +succeeds, tries @scheme[G2]; if not, tries @scheme[G3].} + +@defform[(%is E1 E2)]{ +The goal @scheme[(%is E1 E2)] unifies with @scheme[E1] the result of +evaluating @scheme[E2] as a Scheme expression. @scheme[E2] may contain +logic variables, which are dereferenced automatically. +Fails if @scheme[E2] contains unbound logic variables.} + +@defform[(%let (V ...) expr ...) + #:contracts ([V identifier?])]{ +Introduces @scheme[V], ..., as +lexically scoped logic variables to be used in @scheme[expr], ...} + +@defpred[(%melt [F any/c] [S any/c])]{ +The goal @scheme[(%melt F S)] unifies @scheme[S] with the thawed +(original) form of the frozen structure in @scheme[F].} + +@defpred[(%melt-new [F any/c] [S any/c])]{ +The goal @scheme[(%melt-new F S)] unifies @scheme[S] with a thawed +@emph{copy} of the frozen structure in @scheme[F]. This means +new logic variables are used for unbound logic variables in +@scheme[F].} + +@defpred[(%member [E1 any/c] [E2 any/c])]{ +The goal @scheme[(%member E1 E2)] succeeds if @scheme[E1] is a member +of the list in @scheme[E2].} + +@defpred[(%nonvar [E any/c])]{ +@scheme[%nonvar] is the negation of @scheme[%var]. +The goal @scheme[(%nonvar E)] succeeds if @scheme[E] is completely +instantiated, ie, it has no unbound variable in it.} + +@defpred[(%not [G goal?])]{ +The goal @scheme[(%not G)] succeeds if @scheme[G] fails.} + +@defproc[(%more) answer?]{ +The thunk @scheme[%more] produces more instantiations of the +variables in the most recent @scheme[%which]-form that satisfy the +goals in that @scheme[%which]-form. If no more solutions can +be found, @scheme[%more] returns @scheme[#f].} + +@defform[(%or G ...) #:contracts ([G goal?])]{ +The goal @scheme[(%or G ...)] succeeds if one of @scheme[G], ..., tried +in that order, succeeds.} + +@defform/subs[(%rel (V ...) clause ...) + ([clause [(E ...) G ...]]) + #:contracts ([V identifier?] + [E expression?] + [G goal?])]{ +Creates a predicate object. +Each clause @scheme[C] signifies +that the goal created by applying the predicate object to +anything that matches @scheme[(E ...)] is deemed to succeed if all +the goals @scheme[G], ..., can, in their turn, be shown to succeed.} + +@defpred[(%repeat)]{ +The goal @scheme[(%repeat)] always succeeds (even on retries). +Used for failure-driven loops.} + +@defboolparam[schelog-use-occurs-check? on?]{ +If this is false (the default), +Schelog's unification will not use the occurs check. +If it is true, the occurs check is enabled.} + +@defpred[(%set-of [E1 any/c] [G goal?] [E2 any/c])]{ +The goal @scheme[(%set-of E1 G E2)] unifies with @scheme[E2] the @emph{set} +of all the +instantiations of @scheme[E1] for which goal @scheme[G] succeeds.} + +@defpred[(%set-of-1 [E1 any/c] [G goal?] [E2 any/c])]{ +Similar to @scheme[%set-of], but fails if the set is empty.} + +@defgoal[%true]{ +The goal @scheme[%true] succeeds. Fails on retry.} + +@defpred[(%var [E any/c])]{ +The goal @scheme[(%var E)] succeeds if @scheme[E] is not completely +instantiated, ie, it has at least one unbound variable in +it.} + +@defform[(%which (V ...) G ...) + #:contracts ([V identifier?] + [G goal?])]{ +Returns an instantiation +of the variables @scheme[V], ..., that satisfies all of @scheme[G], +... If @scheme[G], ..., cannot be satisfied, returns @scheme[#f]. +Calling the thunk @scheme[%more] produces more +instantiations, if available.} + +@defproc[(_) logic-variable?]{ +A thunk that produces a new logic variable. Can be +used in situations where we want a logic variable but +don't want to name it. (@scheme[%let], in contrast, introduces new +lexical names for the logic variables it creates.) +} + +@defgoal[!]{ +The cut goal, see @secref{cut}.} + +@bibliography[ + @bib-entry[#:key "sicp" + #:author "Harold Abelson and Gerald Jay Sussman with Julie Sussman" + #:title "Structure and Interpretation of Computer Programs (``SICP''), 2nd Edition" + #:url "http://mitpress.mit.edu/sicp/full-text/book/book.html" + #:date "1996" + #:location "MIT Press" + #:is-book? #t] + @bib-entry[#:key "aop" + #:author "Leon Sterling and Ehud Shapiro" + #:url "http://mitpress.mit.edu/book-home.tcl?isbn=0262193388" + #:title "The Art of Prolog, 2nd Edition" + #:location "MIT Press" + #:date "1994" + #:is-book? #t] + @bib-entry[#:key "tls" + #:author "Daniel P Friedman and Matthias Felleisen" + #:url "http://www.ccs.neu.edu/~matthias/BTLS" + #:title "The Little Schemer, 4th Edition" + #:location "MIT Press" + #:date "1996" + #:is-book? #t] + @bib-entry[#:key "tss" + #:author "Daniel P Friedman and Matthias Felleisen" + #:url "http://www.ccs.neu.edu/~matthias/BTSS" + #:title "The Seasoned Schemer" + #:location "MIT Press" + #:date "1996" + #:is-book? #t] + @bib-entry[#:key "eopl" + #:author "Daniel P Friedman and Mitchell Wand and Christopher T Haynes" + #:url "http://mitpress.mit.edu/book-home.tcl?isbn=0262061457" + #:title "Essentials of Programming Languages" + #:location "MIT Press, McGraw-Hill" + #:date "1992" + #:is-book? #t] + @bib-entry[#:key "bratko" + #:author "Ivan Bratko" + #:title "Prolog Programming for Artificial Intelligence" + #:location "Addison-Wesley" + #:date "1986" + #:is-book? #t] + @bib-entry[#:key "campbell" + #:author "J A Campbell (editor)" + #:title "Implementations of Prolog" + #:location "Ellis Horwood" + #:date "1984" + #:is-book? #t] + @bib-entry[#:key "ok:prolog" + #:author "Richard A O'Keefe" + #:url "http://mitpress.mit.edu/book-home.tcl?isbn=0262150395" + #:title "The Craft of Prolog" + #:location "MIT Press" + #:date "1990" + #:is-book? #t] + @bib-entry[#:key "logick" + #:author "Christopher T Haynes" + #:title "Logic continuations" + #:location "J Logic Program, vol 4, 157--176" + #:date "1987"] + @bib-entry[#:key "r5rs" + #:author "Richard Kelsey and William Clinger and Jonathan {Rees (eds)}" + #:url "http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs.html" + #:title "Revised^5 Report on the Algorithmic Language Scheme (``R5RS'')" + #:date "1998"] + @bib-entry[#:key "t-y-scheme" + #:author "Dorai Sitaram" + #:title "Teach Yourself Scheme in Fixnum Days" + #:url "http://www.ccs.neu.edu/~dorai/t-y-scheme/t-y-scheme.html"] + @bib-entry[#:key "mf:prolog" + #:author "Matthias Felleisen" + #:title "Transliterating Prolog into Scheme" + #:location "Indiana U Comp Sci Dept Tech Report #182" + #:date "1985"] + ] \ No newline at end of file diff --git a/collects/schelog/schelog.tex b/collects/schelog/schelog.tex deleted file mode 100644 index ce7f3b4f55..0000000000 --- a/collects/schelog/schelog.tex +++ /dev/null @@ -1,1572 +0,0 @@ -\magnification\magstephalf - -\input tex2page -\input btxmac -\texonly -%\input 2col - -\sidemargin 1.75 true in - -%\input defun - -% avoiding overfull boxes, without making -% paragraphs too bad - -\pretolerance -1 -\emergencystretch 5pt -\tolerance 3000 - -\hfuzz 1pt - -\hyphenpenalty -1000 -\exhyphenpenalty -1000 -\doublehyphendemerits -100000 -\finalhyphendemerits -100000 - -% ! is special char for makeindex -%\def\bang{!} - -\let\n\noindent - -\let\origverb\verb - -\def\verb{\def\verbatimhook{\parindent0pt \relax}\origverb} - -\def\p{\let\verbatimhook\relax\origverb} - -%sign for ``evaluates to'' -\def\y{$\Rightarrow$} - -%notation for true nil -\def\t{{\tt()}$^{\rm true}$} - -\overfullrule 0pt - - -\def\ar/#1{{\it/#1\/}} - -\hyphenation{sche-log} - -\let\ab\allowbreak - - -%that's all -%\input ptm - -\endtexonly - -\htmlonly -\def\defun#1#2{% -\evalh{(do-end-para)}% -\rawhtml
\endrawhtml -#2% -\rawhtml\endrawhtml{#1}% -\rawhtml
\endrawhtml -\evalh{(do-para)}} - -\def\t{()\rawhtmltrue\endrawhtml} -\def\y{{\tt =>}} - - -\endhtmlonly - -\let\byline\centerline - -\def\defproc{\defun{[{\it procedure}]}} -\def\defpred{\defun{[{\it predicate}]}} -\def\defmac{\defun{[{\it macro}]}} -\def\defgoal{\defun{[{\it goal}]}} -\def\defflag{\defun{[{\it flag}]}} - -\def\newsection{\htmlpagebreak\section} - -\let\q\scm -\let\sverbatim\scm - -\scmkeyword{%which %rel %assert %assert-a %let %and %or %is -! %free-vars -} - -\texonly -\def\t{()$^t$} -\def\y{$\Rightarrow$} -\endtexonly - -\title{Programming in Schelog} - -\byline{\urlh{http://www.ccs.neu.edu/~dorai}{Dorai -Sitaram}} -%\byline{\urlh{mailto:ds26@gte.com}{ds26@gte.com}} -\byline{\urlh{schelog.tar.gz}{\htmlonly Download -\endhtmlonly Version \input ./schelog-version }} -\htmlonly -\byline{\urlh{INSTALL}{Installation instructions}} -\endhtmlonly - -\bigskip - -\n Schelog is an {\em embedding} of -Prolog-style logic programming in Scheme. ``Embedding'' -means you don't lose Scheme: You can use Prolog-style and -conventional Scheme code fragments alongside each other. -Schelog contains the full repertoire of Prolog features, -including meta-logical and second-order (``set'') -predicates, leaving out only those features that could more -easily and more efficiently be done with Scheme -subexpressions. - -The Schelog implementation uses the approach to logic -programming described in Felleisen \cite{mf:prolog} and -Haynes \cite{logick}. In contrast to earlier Lisp simulations of -Prolog \cite{campbell}, -which used explicit continuation -arguments to store failure (backtrack) information, the -Felleisen and Haynes model uses the implicit reified -continuations of Scheme as provided by the operator -\q{call-with-current-continuation} (aka \q{call/cc}). This -allows Schelog to be an {\em embedding}, ie, logic -programming is not built as a new language on top of Scheme, -but is used alongside Scheme's other features. Both styles -of programming may be mixed to any extent that a project -needs. - -The Schelog user does not need to know about the -implementation mechanism or about \q{call/cc} and -continuations to get on with the business of -doing logic programming with Schelog. - -This text is a gentle introduction to Schelog syntax -and programming. It assumes a working knowledge of -Scheme and an awareness of, if not actual programming -experience with, Prolog. If you need assistance in -either language, you may consult -\cite{sicp,tls,tss,eopl,r5rs,t-y-scheme} for Scheme, and -\cite{bratko,ok:prolog,aop} for Prolog. -There are doubtless many other excellent books and -online documents available. - -\beginsection Contents - -\tableofcontents - -\newsection{Simple Goals and Queries} -\label{simple} - -Schelog objects are the same as Scheme objects. However, there -are two subsets of these objects that are of special -interest to Schelog: {\em goals} and {\em predicates}. We -will first look at some simple goals. -Section \ref{predicates} will introduce predicates and ways -of making complex goals using predicates. - -A goal is an object whose truth or falsity we can check. A -goal that turns out to be true is said to succeed. -A goal that turns out to be false is said to -fail. - -Two simple goals that are provided in Schelog are: - -\sverbatim{ -%true -%fail -} - -\n The goal \q{%true} succeeds. The goal \q{%fail} -always fails. - -(The names of all Schelog primitive objects -start with \q{%}. This is to avoid clashes with the names -of conventional Scheme objects of related meaning. -User-created objects in Schelog are not required to -follow this convention.) - -A Schelog user can {\em query} a goal by wrapping it in a -\q{%which}-form. - -\sverbatim{ -(%which () %true) -} - -\n evaluates to \q{()}, indicating success, whereas: - -\sverbatim{ -(%which () %fail) -} - -\n evaluates to \q{#f}, indicating failure. - -Note 1: The second subexpression of the \q{%which}-form -is the empty list \q{()}. Later (sec \ref{solving-goals}), -we will see \q{%which}es -with other lists as the second subform. - -Note 2: The distinction between successful and failing goals -depends on Scheme's distinguishing \q{#f} from -\q{()}. We will see later (sec \ref{false-vs-nil}) -what to do in Scheme dialects where \q{#f} and \q{()} are -identical. For the moment, we will use the annotation -\q{|t} to signal that \q{()} is being used as a true -value. - -Henceforth, we will use the notation: - -\sverbatim{ -E |y F -} - -\n to say that \q{E} {\em evaluates to} \q{F}. Thus, - -\sverbatim{ -(%which () %true) |y |t -} - -\newsection{Predicates} -\label{predicates} - -More interesting goals are created by applying a special -kind of Schelog object called a {\em predicate} (or -{\em relation}) to other -Schelog objects. Schelog comes with some primitive -predicates, such as the arithmetic operators -\q{%=:=} and \q{%<}, -standing for arithmetic ``equal'' and ``less than'' -respectively. For example, the following are some goals -involving these predicates: - -\sverbatim{ -(%which () (%=:= 1 1)) |y |t -(%which () (%< 1 2)) |y |t -(%which () (%=:= 1 2)) |y #f -(%which () (%< 1 1)) |y #f -} - -\n Other arithmetic predicates are -\q{%>} (``greater than''), -\q{%<=} (``less than or equal''), -\q{%>=} (``greater than or equal''), and -\q{%=/=} (``not equal''). - -Schelog predicates are not to be confused with conventional -Scheme predicates (such as \q{<} and \q{=}). Schelog -predicates, when applied to arguments, produce goals -that -may either succeed or fail. Scheme predicates, when applied -to arguments, yield a boolean value. Henceforth, we will -use the term ``predicate'' to mean Schelog predicates. -Conventional predicates will be explicitly called ``Scheme -predicates''. - -\subsection{Predicates Introducing Facts} -\label{facts} - -Users can create their own predicates using the Schelog form -\q{%rel}. For example, let's -define the predicate \q{%knows}: - -\sverbatim{ -(define %knows - (%rel () - [('Odysseus 'TeX)] - [('Odysseus 'Scheme)] - [('Odysseus 'Prolog)] - [('Odysseus 'Penelope)] - [('Penelope 'TeX)] - [('Penelope 'Prolog)] - [('Penelope 'Odysseus)] - [('Telemachus 'TeX)] - [('Telemachus 'calculus)])) -} - -\n The expression has the expected meaning. Each -{\em clause} in the \q{%rel} establishes a {\em fact}: -Odysseus -knows TeX, Telemachus knows calculus, \&c. In general, if we -apply the predicate to the arguments in any one of its -clauses, we will get a successful goal. Thus, since -\q{%knows} has a clause that reads -\q{[('Odysseus 'TeX)]}, the goal -\q{(%knows 'Odysseus 'TeX)} -will be true. - -(In the code in -this text, brackets have the same behavior as parentheses. -We use a mix of brackets and parentheses solely to improve -the readability of the code for humans.] - -We can now get answers for the following types of queries: - -\sverbatim{ -(%which () - (%knows 'Odysseus 'TeX)) -|y |t - -(%which () - (%knows 'Telemachus 'Scheme)) -|y #f -} - -\subsection{Predicates with Rules} -\label{rules} - -Predicates can be more complicated than the above bald -recitation of facts. The predicate clauses can be {\em rules}, eg, - -\sverbatim{ -(define %computer-literate - (%rel (person) - [(person) - (%knows person 'TeX) - (%knows person 'Scheme)] - [(person) - (%knows person 'TeX) - (%knows person 'Prolog)])) -} - -\n This defines the predicate -\q{%computer-literate} in -terms of the predicate \q{%knows}. In effect, a person is -defined as computer-literate if they know TeX and -Scheme, {\em or} TeX and Prolog. - -Note that this use of -\q{%rel} employs a local {\em logic variable} called \q{person}. -In general, a \q{%rel}-expression can have a list of symbols -as its second subform. These name new logic variables that -can be used within the body of the \q{%rel}. - -The following query can now be answered: - -\sverbatim{ -(%which () - (%computer-literate 'Penelope)) -|y |t -} - -\n Since Penelope knows TeX and Prolog, she is computer-literate. - -\subsection{Solving Goals} -\label{solving-goals} - -The above queries are yes/no questions. Logic programming -allows more: We can formulate a goal with {\em uninstantiated} -logic variables and then ask the querying process to -provide, if possible, values for these variables that cause -the goal to succeed. For instance, the query: - -\sverbatim{ -(%which (what) - (%knows 'Odysseus what)) -} - -\n asks for an instantiation of the logic variable \q{what} -that satisfies the goal \q{(%knows 'Odysseus what)}. -In other words, we are asking, ``What does Odysseus know?'' - -Note that this use of \q{%which} --- like \q{%rel} -in the definition of \q{%computer-literate} --- -uses a local logic -variable, \q{what}. In general, the second subform of -\q{%which} can be a list of local logic variables. The -\q{%which}-query returns an answer that is a list of -bindings, one for each logic variable mentioned in its -second subform. Thus, - -\sverbatim{ -(%which (what) - (%knows 'Odysseus what)) -|y ([what TeX]) -} - -\n But that is not all that wily Odysseus knows. Schelog -provides a zero-argument procedure (``thunk'') called -\q{%more} -that {\em retries} the goal in the last -\q{%which}-query for a different solution. - -\sverbatim{ -(%more) |y ([what Scheme]) -} - -\n We can keep pumping for more solutions: - -\sverbatim{ -(%more) |y ([what Prolog]) -(%more) |y ([what Penelope]) -(%more) |y #f -} - -\n The final \q{#f} shows that there are no more -solutions. This is because there are no more clauses in the -\q{%knows} predicate that list Odysseus as knowing anything -else. - -\subsubsection{A Note on {\tt\#f} vs {\tt()}} -\label{false-vs-nil} - -It is now clear why \q{|t} was the right choice for truth in -the previous yes/no \q{%which}-queries that had no logic -variables (sec \ref{simple}). \q{%which} returns a -list of bindings -for true -goals: the list is empty when there are no variables. - -For such Schemes as don't distinguish between \q{()} and -\q{#f}, we can still ask fruitful yes/no queries. Simply -use a dummy local -variable in the -\q{%which}-expression. Truth will give an (ignorable) -binding for the dummy variable, while falsity will, as -usual, produce \q{#f}. - -\sverbatim{ -(%which (bingo) - (%knows 'Odysseus 'TeX)) -|y ([bingo _]) - -(%which (bingo) - (%knows 'Odysseus 'calculus)) -|y #f -} - -\subsection{ Asserting Extra Clauses} -\label{assert} - -We can add more clauses to a predicate after it has already -been defined with a \q{%rel}. Schelog provides the -\q{%assert} form for this purpose. Eg, - -\sverbatim{ -(%assert %knows () - [('Odysseus 'archery)]) -} - -\n tacks on a new clause at the end of the existing clauses -of the \q{%knows} -predicate. Now, the query: - -\sverbatim{ -(%which (what) - (%knows 'Odysseus what)) -} - -\n gives TeX, Scheme, Prolog, and Penelope, as before, but -a subsequent \q{(%more)} yields a new result: \q{archery}. - -The Schelog form \q{%assert-a} is similar to \q{%assert} but -adds clauses {\em before} any of the current clauses. - -Both \q{%assert} and \q{%assert-a} assume that the variable -they are adding to already names a predicate (presumably -defined using \q{%rel}). -In order to allow defining a predicate entirely through -\q{%assert}s, Schelog provides an empty predicate value -\q{%empty-rel}. \q{%empty-rel} takes any number of arguments -and always fails. A typical use of the -\q{%empty-rel} and \q{%assert} combination: - -\sverbatim{ -(define %parent %empty-rel) - -(%assert %parent () - [('Laertes 'Odysseus)]) - -(%assert %parent () - [('Odysseus 'Telemachus)] - [('Penelope 'Telemachus)]) -} - -(Schelog does not provide a predicate for {\em retracting} -assertions, since we can keep track of older versions of -predicates using conventional Scheme features (\q{let} and \q{set!}).) - -\subsection{Local Variables} -\label{local-vars} - -The local logic variables of \q{%rel}- and -\q{%which}-expressions are in reality introduced by the -Schelog syntactic form called \q{%let}. (\q{%rel} and -\q{%which} are macros written using \q{%let}.) - -\q{%let} introduces new lexically scoped logic variables. -Supposing, instead of - -\sverbatim{ -(%which (what) - (%knows 'Odysseus what)) -} - -\n we had asked - -\sverbatim{ -(%let (what) - (%which () - (%knows 'Odysseus what))) -} - -\n This query, too, succeeds five times, since -Odysseus knows five things. However, \q{%which} emits -bindings only for the local variables that {\em it} -introduces. Thus, this query emits \q{|t} five times before -\q{(%more)} finally returns \q{#f}. - -\newsection{Using Conventional Scheme Expressions in Schelog} -\label{scheme-w-schelog} - -The arguments of Schelog predicates can be any Scheme -objects. In particular, composite structures such as lists, -vectors and strings can be used, as also Scheme expressions -using the full array of Scheme's construction and -decomposition operators. For instance, consider the -following goal: - -\sverbatim{ -(%member x '(1 2 3)) -} - -\n Here, \q{%member} is a predicate, \q{x} is a logic -variable, and \q{'(1 2 3)} is a structure. Given a suitably -intuitive definition for \q{%member}, the above goal -succeeds for \q{x} = \q{1}, \q{2}, and \q{3}. - -Now to defining predicates like \q{%member}: - -\sverbatim{ -(define %member - (%rel (x y xs) - [(x (cons x xs))] - [(x (cons y xs)) - (%member x xs)])) -} - -\n Ie, \q{%member} is defined with three local variables: -\q{x}, \q{y}, \q{xs}. It has two -clauses, identifying the two ways of determining membership. - -The first clause of \q{%member} states a fact: For any -\q{x}, \q{x} is a member of a list whose head is also \q{x}. - -The second clause of \q{%member} is a rule: \q{x} is a -member of a list if we can show that it is a member of the -{\em tail} of that list. In other words, the original -\q{%member} goal is translated into a {\em sub}goal, which is also -a \q{%member} goal. - -Note that the variable \q{y} in the definition of -\q{%member} occurs only once in the second clause. As such, -it doesn't need you to make the effort of naming it. (Names -help only in matching a second occurrence to a first.) Schelog -lets you use the expression \q{(_)} to denote an anonymous -variable. (Ie, \q{_} is a thunk that generates a fresh -anonymous variable at each call.) The predicate \q{%member} can be -rewritten as - -\sverbatim{ -(define %member - (%rel (x xs) - [(x (cons x (_)))] - [(x (cons (_) xs)) - (%member x xs)])) -} - -\subsection{Constructors} -\label{constructors} - -We can use constructors --- Scheme procedures for creating -structures --- to simulate data types in Schelog. For -instance, let's define a natural-number data-type where -\q{0} denotes zero, and \q{(succ x)} denotes the natural number -whose immediate predecessor is \q{x}. The constructor -\q{succ} can -be defined in Scheme as: - -\sverbatim{ -(define succ - (lambda (x) - (vector 'succ x))) -} - -\n Addition and multiplication can be defined as: - -\sverbatim{ -(define %add - (%rel (x y z) - [(0 y y)] - [((succ x) y (succ z)) - (%add x y z)])) - -(define %times - (%rel (x y z z1) - [(0 y 0)] - [((succ x) y z) - (%times x y z1) - (%add y z1 z)])) -} - -\n We can do a lot of arithmetic with this in place. For -instance, the factorial predicate looks like: - -\sverbatim{ -(define %factorial - (%rel (x y y1) - [(0 (succ 0))] - [((succ x) y) - (%factorial x y1) - (%times (succ x) y1 y)])) -} - -\subsection{\tt\%is} -\label{is} - -The above is a very inefficient way to do arithmetic, -especially when the underlying language Scheme offers -excellent arithmetic facilities (including a comprehensive -number ``tower'' and exact rational arithmetic). One -problem with using Scheme calculations directly in Schelog -clauses is that the expressions used may contain logic -variables that need to be dereferenced. Schelog provides -the predicate \q{%is} that takes care of this. The goal - -\sverbatim{ -(%is X E) -} - -\n unifies \q{X} with the value of \q{E} considered as a -Scheme expression. \q{E} can have logic variables, but -usually they should at least be bound, as unbound variables -may not be palatable values to the Scheme operators used in -\q{E}. - -We can now directly use the numbers of Scheme to write a -more efficient \q{%factorial} predicate: - -\sverbatim{ -(define %factorial - (%rel (x y x1 y1) - [(0 1)] - [(x y) (%is x1 (- x 1)) - (%factorial x1 y1) - (%is y (* y1 x))])) -} - -\n A price that this efficiency comes with is that we can -use \q{%factorial} only with its first argument already -instantiated. In many cases, this is not an unreasonable -constraint. In fact, given this limitation, there is -nothing to prevent us from using Scheme's factorial -directly: - -\sverbatim{ -(define %factorial - (%rel (x y) - [(x y) - (%is y (scheme-factorial - x))])) -} - -\n or better yet, ``in-line'' any calls to \q{%factorial} with -\q{%is}-expressions calling \q{scheme-factorial}, where the -latter is defined in the usual manner: - -\sverbatim{ -(define scheme-factorial - (lambda (n) - (if (= n 0) 1 - (* n (factorial - (- n 1)))))) -} - -\subsection{Lexical Scoping} -\label{lexical-scoping} - -One can use Scheme's lexical scoping to enhance predicate -definition. Here is a list-reversal predicate defined using -a hidden auxiliary predicate: - -\sverbatim{ -(define %reverse - (letrec - ([revaux - (%rel (x y z w) - [('() y y)] - [((cons x y) z w) - (revaux y - (cons x z) w)])]) - (%rel (x y) - [(x y) (revaux x '() y)]))) -} - -\n \q{(revaux X Y Z)} uses \q{Y} as an accumulator for -reversing \q{X} into \q{Z}. (\q{Y} starts out as \q{()}. -Each head of \q{X} is \q{cons}ed on to \q{Y}. Finally, when -\q{X} has wound down to \q{()}, \q{Y} contains the reversed -list and can be returned as \q{Z}.) - -\q{revaux} is used purely as a helper predicate for -\q{%reverse}, and so it can be concealed within a lexical -contour. We use \q{letrec} instead of \q{let} because -\q{revaux} is a recursive procedure. - -\subsection{Type Predicates} -\label{type-predicates} - -Schelog provides a couple of predicates that let the user -probe the type of objects. - -The goal - -\sverbatim{ -(%constant X) -} - -\n succeeds if \q{X} is an {\em atomic} object, ie, not a -list or vector. - -The predicate \q{%compound}, the negation of \q{%constant}, -checks if its argument is indeed a list or a vector. - -The above are merely the logic-program\-ming equivalents of -corresponding Scheme predicates. Users can use the -predicate \q{%is} and Scheme predicates to write more type -checks in Schelog. Thus, to test if \q{X} is a string, the -following goal could be used: - -\sverbatim{ -(%is #t (string? X)) -} - -\n User-defined Scheme predicates, in addition to primitive Scheme -predicates, can be thus imported. - -\newsection{Backtracking} -\label{backtracking} - -It is helpful to go into the following evaluation (sec \ref{rules}) -in a -little detail: - -\sverbatim{ -(%which () - (%computer-literate 'Penelope)) -|y |t -} - -\n The starting goal -is: - -\sverbatim{ -G0 = (%computer-literate Penelope) -} - -\n (I've taken out the quote because \q{Penelope} is the result -of evaluating \q{'Penelope}.) - -Schelog tries to match this with the head of the first -clause of \q{%computer-literate}. It succeeds, generating a -binding \q{[person Penelope]}. - -But this means it now has two new goals --- {\em subgoals} ---- to solve. These are the goals in the body of the -matching clause, with the logic variables substituted by -their instantiations: - -\sverbatim{ -G1 = (%knows Penelope TeX) -G2 = (%knows Penelope Scheme) -} - -\n For \q{G1}, Schelog attempts matches with the clauses of -\q{%knows}, and succeeds at the fifth try. (There are no -subgoals in this case, because the bodies of these ``fact'' -clauses are empty, in contrast to the ``rule'' clauses of -\q{%computer-literate}.) -Schelog then tries to solve \q{G2} against the clauses of -\q{%knows}, and since there is no clause stating that -Penelope knows Scheme, it fails. - -All is not lost though. Schelog now {\em backtracks} to the -goal that was solved just before, viz., \q{G1}. It -{\em retries} \q{G1}, ie, tries to solve it in a -different way. -This entails searching down the previously unconsidered -\q{%knows} -clauses for \q{G1}, ie, the sixth onwards. Obviously, -Schelog fails again, because the fact that Penelope knows -TeX occurs only once. - -Schelog now backtracks to the goal before \q{G1}, ie, -\q{G0}. We abandon the current successful match with the -first clause-head of \q{%computer-literate}, and try the -next clause-head. Schelog succeeds, again producing a binding -\q{[person Penelope]}, and two new subgoals: - -\sverbatim{ -G3 = (%knows Penelope TeX) -G4 = (%knows Penelope Prolog) -} - -\n It is now easy to trace that Schelog finds both \q{G3} and \q{G4} to be -true. Since both of \q{G0}'s subgoals are true, \q{G0} is -itself considered true. And this is what Schelog reports. The -interested reader can now trace why the -following query has a different denouement: - -\sverbatim{ -(%which () - (%computer-literate 'Telemachus)) -|y #f -} - -\newsection{Unification} -\label{unification} - -When we say that a goal matches with a clause-head, we mean -that the predicate and argument positions line up. Before -making this comparison, Schelog dereferences all already -bound logic variables. The resulting structures are then -compared to see if they are recursively identical. Thus, -\q{1} unifies with \q{1}, and \q{(list 1 2)} with \q{'(1 -2)}; but \q{1} and -\q{2} do not unify, and neither do \q{'(1 2)} and \q{'(1 -3)}. - -In general, there could be quite a few uninstantiated logic -variables in the compared objects. Unification will then -endeavor to find the most natural way of binding these -variables so that we arrive at structurally identical -objects. Thus, \q{(list x 1)}, where \q{x} is an unbound logic -variable, unifies with \q{'(0 1)}, producing the -binding -\q{[x 0]}. - -Unification is thus a goal, and Schelog makes the unification predicate -available to the user as \q{%=}. Eg, - -\sverbatim{ -(%which (x) - (%= (list x 1) '(0 1)) -|y ([x 0]) -} - -\n Schelog also provides the predicate \q{%/=}, the {\em negation} of -\q{%=}. \q{(%/= X Y)} succeeds if and only if \q{X} does -{\em not} unify with \q{Y}. - -Unification goals constitute the basic subgoals that all -Schelog goals devolve to. A goal succeeds because all the -eventual unification subgoals that it decomposes to in at -least one of its subgoal-branching succeeded. It fails -because every possible subgoal-branching was thwarted by the -failure of a crucial unification subgoal. - -Going back to the example in sec \ref{backtracking}, the goal -\q{(%computer-literate 'Penelope)} succeeds because -(a) it unified with -\q{(%computer-literate person)}; and then (b) with the binding -\q{[person Penelope]} in place, \q{(%knows person 'TeX)} -unified with \q{(%knows 'Penelope 'TeX)} and -\q{(%knows person 'Prolog)} unified with \q{(%knows 'Penelope -'Prolog)}. - -In contrast, the goal \q{(%computer-literate 'Telemachus)} -fails because, with \q{[person Telemachus]}, -the subgoals \q{(%knows person 'Scheme)} and -\q{(%knows person 'Prolog)} have no facts they can -unify with. - -\subsection{The Occurs Check} - -A robust unification algorithm uses the {\em -occurs check}, which ensures that a logic variable -isn't bound to a structure that contains itself. -Not performing the check can cause the unification -to go into an infinite loop in some cases. On the -other hand, performing the occurs check greatly -increases the time taken by unification, even in cases -that wouldn't require the check. - -Schelog uses the global variable -\q{*schelog-use-occurs-check?*} to decide whether to -use the occurs check. By default, this variable is -\q{#f}, ie, Schelog disables the occurs check. To -enable the check, - -\q{ -(set! *schelog-use-occurs-check?* #t) -} - -\newsection{Conjuctions and Disjunctions} -\label{and-or} - -Goals may be combined using the forms \q{%and} -and \q{%or} -to form compound goals. (For \q{%not}, see sec \ref{not}.) -Eg, - -\sverbatim{ -(%which (x) - (%and (%member x '(1 2 3)) - (%< x 3))) -} - -\n gives solutions for \q{x} that satisfy both the -argument goals of the \q{%and}. -Ie, \q{x} should both be a member of \q{'(1 2 3)} -{\em and} be less than \q{3}. The first -solution is - -\sverbatim{ -([x 1]) -} - -\n Typing \q{(%more)} gives another solution: - -\sverbatim{ -([x 2]) -} - -\n There are no more solutions, because \q{[x 3]} satisfies -the first but not the second goal. - -Similarly, the query - -\sverbatim{ -(%which (x) - (%or (%member x '(1 2 3)) - (%member x '(3 4 5)))) -} - -\n lists all \q{x} that are members of either list. - -\sverbatim{ - ([x 1]) -(%more) |y ([x 2]) -(%more) |y ([x 3]) -(%more) |y ([x 3]) -(%more) |y ([x 4]) -(%more) |y ([x 5]) -} - -\n (Yes, \q{([x 3])} is listed twice.) - -We can rewrite the predicate \q{%computer-literate} -from sec \ref{rules} using \q{%and} and \q{%or}: - -\sverbatim{ -(define %computer-literate - (%rel (person) - [(person) - (%or - (%and (%knows person - 'TeX) - (%knows person - 'Scheme)) - (%and (%knows person - 'TeX) - (%knows person - 'Prolog)))])) -} - -\n Or, more succinctly: - -\sverbatim{ -(define %computer-literate - (%rel (person) - [(person) - (%and (%knows person - 'TeX) - (%or (%knows person - 'Scheme) - (%knows person - 'Prolog)))])) -} - -\n We can even dispense with the \q{%rel} altogether: - -\sverbatim{ -(define %computer-literate - (lambda (person) - (%and (%knows person - 'TeX) - (%or (%knows person - 'Scheme) - (%knows person - 'Prolog))))) -} - -\n This last looks like a conventional Scheme predicate -definition, and is arguably -the most readable format for a Scheme programmer. - -\newsection{Manipulating Logic Variables} -\label{lv-manip} - -Schelog provides special predicates for probing logic -variables, without risking their getting bound. - -\subsection{Checking for Variables} -\label{var} - -The goal - -\sverbatim{ -(%== X Y) -} - -\n succeeds if \q{X} and \q{Y} are {\em identical} objects. This -is not quite the unification predicate \q{%=}, for \q{%==} -doesn't touch unbound objects the way \q{%=} does. Eg, -\q{%==} will not equate an unbound logic variable with a -bound one, nor will it equate two unbound logic variables -unless they are the {\em same} variable. - -The predicate \q{%/==} is the negation of \q{%==}. - -The goal - -\sverbatim{ -(%var X) -} - -\n succeeds if \q{X} isn't completely bound --- ie, it has at -least one unbound logic variable in its innards. - -The predicate \q{%nonvar} is the negation of \q{%var}. - -\subsection{Preserving Variables} -\label{freeze} - -Schelog lets the user protect a term with variables from -unification by allowing that term to be treated as a -(completely) bound object. The predicates provided for this -purpose are -\q{%freeze}, -\q{%melt}, \q{%melt-new}, and \q{%copy}. - -The goal - -\sverbatim{ -(%freeze S F) -} - -\n unifies \q{F} to the frozen version of \q{S}. Any lack -of bindings in \q{S} are preserved no matter how much you -toss \q{F} about. - -The goal - -\sverbatim{ -(%melt F S) -} - -\n retrieves the object frozen in \q{F} into \q{S}. - -The goal - -\sverbatim{ -(%melt-new F S) -} - -\n is similar to \q{%melt}, -except that when \q{S} is made, the unbound variables in -\q{F} are replaced by brand-new unbound variables. - -The goal - -\sverbatim{ -(%copy S C) -} - -\n is an abbreviation for \q{(%freeze S F)} -followed by \q{(%melt-new F C)}. - -\newsection{The Cut ({\tt!})} -\label{cut} - -The cut (called \q{!}) is a special goal that is used to -prune backtracking options. Like the \q{%true} goal, the -cut goal too succeeds, when accosted by the Schelog -subgoaling engine. However, when a further subgoal down the -line fails, and time comes to retry the cut goal, Schelog -will refuse to try alternate clauses for the predicate in -whose definition the cut occurs. In other words, the cut -causes Schelog to commit to all the decisions made from the -time that the predicate was selected to match a subgoal till -the time the cut was satisfied. - -For example, consider again the \q{%factorial} -predicate, as defined in sec \ref{is}: - -\sverbatim{ -(define %factorial - (%rel (x y x1 y1) - [(0 1)] - [(x y) (%is x1 (- x 1)) - (%factorial x1 y1) - (%is y (* y1 x))])) -} - -\n Clearly, - -\sverbatim{ -(%which () - (%factorial 0 1)) |y |t -(%which (n) - (%factorial 0 n)) |y ([n 1]) -} - -\n But what if we asked for \q{(%more)} for either query? -Backtracking will try -the second clause of \q{%factorial}, and sure enough the -clause-head unifies, producing binding \q{[x 0]}. -We now get three subgoals. Solving the first, we get \q{[x1 --1]}, and then we have to solve \q{(%factorial -1 y1)}. It -is easy to see there is no end to this, as we fruitlessly -try to get the factorials of numbers that get more and more -negative. - -If we placed a cut at the first clause: - -\sverbatim{ -... -[(0 1) !] -... -} - -\n the attempt to find more solutions for \q{(%factorial 0 -1)} is nipped in the bud. - -Calling \q{%factorial} with a {\em negative} number would still cause an -infinite loop. To take care of that problem as well, we -use another cut: - -\sverbatim{ -(define %factorial - (%rel (x y x1 y1) - [(0 1) !] - [(x y) (< x 0) ! %fail] - [(x y) (%is x1 (- x 1)) - (%factorial x1 y1) - (%is y (* y1 x))])) -} - -Using {\em raw} cuts as above can get very confusing. For this -reason, it is advisable to use it hidden away in -well-understood abstractions. Two such common abstractions -are the conditional and negation. - -\subsection{Conditional Goals} -\label{if-then-else} - -An ``if ... then ... else ...'' predicate can be defined -as follows - -\sverbatim{ -(define %if-then-else - (%rel (p q r) - [(p q r) p ! q] - [(p q r) r])) -} - -\n (Note that for the first time we have predicate arguments that -are themselves goals.) - -Consider the goal - -\sverbatim{ -G0 = (%if-then-else Gbool - Gthen Gelse) -} - -\n We first unify \q{G0} with the first clause-head, -giving -\q{[p Gbool]}, \q{[q Gthen]}, \q{[r Gelse]}. \q{Gbool} can -now either succeed or fail. - -Case 1: If \q{Gbool} fails, backtracking will cause the -\q{G0} to unify with the second clause-head. \q{r} is bound -to \q{Gelse}, and so \q{Gelse} is tried, as expected. - -Case 2: If \q{Gbool} succeeds, the cut commits to this -clause of the \q{%if-then-else}. We now try \q{Gthen}. If -\q{Gthen} should now fail --- or even if we simply retry for -more solutions --- we are guaranteed that the second -clause-head will not be tried. If it were not for the cut, -\q{G0} would attempt to unify with the second clause-head, which will -of course succeed, and \q{Gelse} {\em will} be tried. - -\subsection{Negation as Failure} -\label{not} - -Another common abstraction using the cut is {\em negation}. -The negation of goal \q{G} is defined as \q{(%not G)}, where -the predicate \q{%not} is defined as follows: - -\sverbatim{ -(define %not - (%rel () - [(g) g ! %fail] - [(g) %true])) -} - -\n Thus, \q{g}'s negation is deemed a failure if \q{g} -succeeds, and a success if \q{g} fails. This is of course -confusing goal failure with falsity. In some cases, this -view of negation is actually helpful. - -\newsection{Set Predicates} -\label{set-of} - -The goal - -\sverbatim{ -(%bag-of X G Bag) -} - -\n unifies with \q{Bag} the list of all instantiations of -\q{X} for which \q{G} succeeds. Thus, the following query -asks for all the things known --- ie, the collection of things -such that someone knows them: - -\sverbatim{ -(%which (things-known) - (%let (someone x) - (%bag-of x (%knows someone x) - things-known))) -|y ([things-known - (TeX Scheme Prolog - Penelope TeX Prolog - Odysseus TeX calculus)]) -} - -\n This is the only solution for this goal: - -\sverbatim{ -(%more) |y #f -} - -\n Note that some things --- eg, TeX --- are enumerated -more than once. This is because more than one person knows -TeX. To remove duplicates, use the predicate -\q{%set-of} -instead of \q{%bag-of}: - -\sverbatim{ -(%which (things-known) - (%let (someone x) - (%set-of x (%knows someone x) - things-known))) -|y ([things-known - (TeX Scheme Prolog - Penelope Odysseus calculus)]) -} - -\n In the above, the free variable \q{someone} in the -\q{%knows}-goal is used as if it -were existentially quantified. In contrast, Prolog's -versions of -\q{%bag-of} and \q{%set-of} fix it for each solution of the -set-predicate goal. We can do it too with some additional -syntax that identifies the free variable. -Eg, - -\sverbatim{ -(%which (someone things-known) - (%let (x) - (%bag-of x - (%free-vars (someone) - (%knows someone x)) - things-known))) -|y ([someone Odysseus] - [things-known - (TeX Scheme Prolog - Penelope)]) -} - -\n The bag of things known by {\em one} someone is -returned. That someone is Odysseus. The query can be -retried for more solutions, each listing the things known by -a different someone: - -\sverbatim{ -(%more) |y ([someone Penelope] - [things-known - (TeX Prolog - Odysseus)]) -(%more) |y ([someone Telemachus] - [things-known - (TeX calculus)]) -(%more) |y #f -} - -Schelog also provides two variants of these set predicates, -viz., \q{%bag-of-1} and \q{%set-of-1}. These act like \q{%bag-of} -and \q{%set-of} but fail if the resulting bag or set is empty. - -\newsection{Glossary of Schelog Primitives} -\label{glossary} - -This section lists, in ascii order, all the Schelog -primitives, with a brief explanation for each. Each entry is -identified -\texonly - --- on the right-hand side of its entry title --- -\endtexonly -as either {\em procedure}, {\em macro}, {\em predicate}, -{\em goal}, or {\em flag}. (Note that predicates and goals are also -procedures. We nevertheless use the more specific names -because of their importance to Schelog programming.) - -Following Prolog style, a predicate's arity is also noted in -its title. Thus, \q{%<}\ar/2 means that \q{%<} takes two -arguments. Variable-arity predicates use an asterisk -instead of a number, eg, \q{%and}\ar/*. - -\defpred{\q{%/=}\ar/2} - -\q{%/=} is the negation of \q{%=}. -The goal \q{(%/= E1 E2)} succeeds if \q{E1} can not be unified -with \q{E2}. - -\defpred{\q{%/==}\ar/2} - -\q{%/==} is the negation of \q{%==}. -The goal \q{(%/== E1 E2)} succeeds if \q{E1} and \q{E2} are not -identical. - -\defpred{\q{%<}\ar/2} - -The goal \q{(%< E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is less than \q{E2}. - -\defpred{\q{%<=}\ar/2} - -The goal \q{(%<= E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is less than or equal to \q{E2}. - -\defpred{\q{%=}\ar/2} - -The goal \q{(%= E1 E2)} succeeds if \q{E1} can be unified with -\q{E2}. Any resulting bindings for logic variables are kept. - -\defpred{\q{%=/=}\ar/2} - -The goal \q{(%=/= E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is not equal to \q{E2}. - -\defpred{\q{%=:=}\ar/2} - -The goal \q{(%=:= E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is equal to \q{E2}. - -\defpred{\q{%==}\ar/2} - -The goal \q{(%== E1 E2)} succeeds if \q{E1} is {\em identical} -to \q{E2}. They should be structurally equal. If containing -logic variables, they should have the same variables in the -same position. Unlike a \q{%=}-call, this goal will not bind -any logic variables. - -\defpred{\q{%>}\ar/2} - -The goal \q{(%> E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is greater than \q{E2}. - -\defpred{\q{%>=}\ar/2} - -The goal \q{(%>= E1 E2)} succeeds if \q{E1} and \q{E2} are bound to -numbers and \q{E1} is greater than or equal to \q{E2}. - -\defmac{\q{%and}\ar/*} - -The goal \q{(%and G ...)} succeeds if all the goals -\q{G}, ..., succeed. - -\defpred{\q{%append}\ar/3} - -The goal \q{(%append E1 E2 E3)} succeeds if \q{E3} is unifiable -with the list obtained by appending \q{E1} and \q{E2} - -\defmac{\q{%assert}} - -The form \q{(%assert Pname (V ...) C ...)} adds the clauses -\q{C}, ..., to the {\em end} of the predicate that is the value of -the Scheme variable \q{Pname}. The variables \q{V}, ..., are -local logic variables for \q{C}, ... - -\defmac{\q{%assert-a}} - -Like \q{%assert}, but adds the new clauses to the {\em front} -of the existing predicate. - -\defpred{\q{%bag-of}\ar/3} - -The goal \q{(%bag-of E1 G E2)} unifies with \q{E2} the {\em bag} -(multiset) -of all the -instantiations of \q{E1} for which goal \q{G} succeeds. - -\defpred{\q{%bag-of-1}\ar/3} - -Similar to \q{%bag-of}, but fails if the bag is empty. - -\defpred{\q{%compound}\ar/1} - -The goal \q{(%compound E)} succeeds if \q{E} is a non-atomic -structure, ie, a vector or a list. - -\defpred{\q{%constant}\ar/1} - -The goal \q{(%compound E)} succeeds if \q{E} is an atomic -structure, ie, not a vector or a list. - -\defpred{\q{%copy}\ar/2} - -The goal \q{(%copy F S)} unifies with \q{S} a copy of the -frozen structure in \q{F}. - -\defpred{\q{%empty-rel}\ar/*} - -The goal \q{(%empty-rel E ...)} always fails. The {\em value} -\q{%empty-rel} is used as a starting value for predicates -that can later be enhanced with \q{%assert} and \q{%assert-a}. - -\defgoal{\q{%fail}} - -The goal \q{%fail} always fails. - -\defmac{\q{%free-vars}} - -The form \q{(%free-vars (V ...) G)} identifies -the occurrences of the variables \q{V}, ..., in goal -\q{G} as free. It is used to avoid existential quantification -in calls to set predicates (\q{%bag-of}, \q{%set-of}, \&c.). - -\defpred{\q{%freeze}\ar/2} - -The goal \q{(%freeze S F)} unifies with \q{F} a new frozen -version of the structure in \q{S}. Freezing implies that all -the unbound variables are preserved. \q{F} can henceforth be -used as {\em bound} object with no fear of its variables -getting bound by unification. - -\defpred{\q{%if-then-else}\ar/3} - -The goal \q{(%if-then-else G1 G2 G3)} tries \q{G1} first: if it -succeeds, tries \q{G2}; if not, tries \q{G3}. - -\defpred{\q{%is}\ar/2} - -The goal \q{(%is E1 E2)} unifies with \q{E1} the result of -evaluating \q{E2} as a Scheme expression. \q{E2} may contain -logic variables, which are dereferenced automatically. -Fails if \q{E2} contains unbound logic variables. -(Note: Unlike other Schelog predicates, \q{%is} is implemented -as a macro and not a procedure.) - -\defmac{\q{%let}} - -The form \q{(%let (V ...) E ...)} introduces \q{V}, ..., as -lexically scoped logic variables to be used in \q{E}, ... - -\defpred{\q{%melt}\ar/2} - -The goal \q{(%melt F S)} unifies \q{S} with the thawed -(original) form of the frozen structure in \q{F}. - -\defpred{\q{%melt-new}\ar/2} - -The goal \q{(%melt-new F S)} unifies \q{S} with a thawed -{\em copy} of the frozen structure in \q{F}. This means -new logic variables are used for unbound logic variables in -\q{F} - -\defpred{\q{%member}\ar/2} - -The goal \q{(%member E1 E2)} succeeds if \q{E1} is a member -of the list in \q{E2}. - -\defpred{\q{%nonvar}\ar/1} - -\q{%nonvar} is the negation of \q{%var}. -The goal \q{(%nonvar E)} succeeds if \q{E} is completely -instantiated, ie, it has no unbound variable in it. - -\defpred{\q{%not}\ar/1} - -The goal \q{(%not G)} succeeds if \q{G} fails. - -\defproc{\q{%more}} - -The thunk \q{%more} produces more instantiations of the -variables in the most recent \q{%which}-form that satisfy the -goals in that \q{%which}-form. If no more solutions can -be found, \q{%more} returns \q{#f}. - -\defmac{\q{%or}\ar/*} - -The goal \q{(%or G ...)} succeeds if one of \q{G}, ..., tried -in that order, succeeds. - -\defmac{\q{%rel}} - -The form \q{(%rel (V ...) C ...)} creates a predicate object. -Each clause \q{C} is of the form \q{[(E ...) G ...]}, signifying -that the goal created by applying the predicate object to -anything that matches \q{(E ...)} is deemed to succeed if all -the goals \q{G}, ..., can, in their turn, be shown to succeed. - -\defpred{\q{%repeat}\ar/0} - -The goal \q{(%repeat)} always succeeds (even on retries). -Used for failure-driven loops. - -\defflag{\q{*schelog-use-occurs-check?*}} - -If the global flag -\q{*schelog-use-occurs-check?*} is false (the default), -Schelog's unification will not use the occurs check. -If it is true, the occurs check is enabled. - -\defpred{\q{%set-of}\ar/3} - -The goal \q{(%set-of E1 G E2)} unifies with \q{E2} the {\em set} -of all the -instantiations of \q{E1} for which goal \q{G} succeeds. - -\defpred{\q{%set-of-1}\ar/3} - -Similar to \q{%set-of}, but fails if the set is empty. - -\defgoal{\q{%true}} - -The goal \q{%true} succeeds. Fails on retry. - -\defpred{\q{%var}\ar/1} - -The goal \q{(%var E)} succeeds if \q{E} is not completely -instantiated, ie, it has at least one unbound variable in -it. - -\defmac{\q{%which}} - -The form \q{(%which (V ...) G ...)} returns an instantiation -of the variables \q{V}, ..., that satisfies all of \q{G}, -... If \q{G}, ..., cannot be satisfied, returns \q{#f}. -Calling the thunk \q{%more} produces more -instantiations, if available. - -\defproc{\q{_} ~~(underscore)} - -A thunk that produces a new logic variable. Can be -used in situations where we want a logic variable but -don't want to name it. (\q{%let}, in contrast, introduces new -lexical names for the logic variables it creates.) - -\newsection{References} -\label{references} - - -\bibliographystyle{plain} -\bibliography{schelog} - -\bye