f(x,y)=x+y==z
look up x is 1, and z is 3, find y is 2:
substraction
what are all the triples (x,y,z) such that
x+y==z
no notion of inputs/outputs
is (x=1,y=2,z=3) in the table? consistency check
if x is 2, for which values of y is z==1? no solution
any non negative integers x,y
now infinite table
notion of laziness to control enumeration
search control
- depth first search is incomplete for infinite domain
- default search for Prolog
- complete search: eventually enumerate all these values
- breadth-first search
- iterative deepening
- interleaved search
infinite table constructed lazily
with infinite search to construct any tuple
all the triples where z is 5
finitely many if we don't allow negatives
how to guarantee finitely many?
enumerate with monotonically increasing z
undecidable problems
Intro to the language
Scheme
((lambda (x) (+ x 1)) 2)
Unification
first-order syntactic unification
two-way pattern matching
(run 1 (q) (== 'cat q))
(run 1 (q) (== 'cat 'dog))
(run 1 (q) (== 'cat 'cat))
(run 1 (x y) (== 'cat 'cat))
(run 1 (x y) (== x y))
(run 1 (x y) (== x y) (== x 'bat))
(run 1 (x y) (== x 'bat) (== x y))
(run 1 (x y) (== x 'bat) (== y x))
conde
(run* (q)
(conde
((== q 'dog))
((== q 'cat))))
fresh
(run* (q)
(fresh (x y)
(== q (list x x y))
(== x 'cat)))
appendo
first, functional
(append '(a b c) '(d e))
(letrec ((append (lambda (l s)
(if (null? l)
s
(cons (car l)
(append (cdr l) s))))))
(append '(a b c) '(d e)))
relational
(define (appendo l s ls)
(conde
((== l '()) (== s ls))
((fresh (a d r)
(== l (cons a d))
(== ls (cons a r))
(appendo d s r)))))
(define (appendo2 l s ls)
(conde
((== l '()) (== s ls))
((fresh (a d r)
(== l (cons a d))
(appendo2 d s r)
(== ls (cons a r))))))
(run* (q)
(appendo '(a b c) '(e d) q))
(run* (x y)
(appendo x y '(a b c d e)))
'((() (a b c d e))
((a) (b c d e))
((a b) (c d e))
((a b c) (d e))
((a b c d) (e))
((a b c d e) ()))
(run 6 (x y)
(appendo2 x y '(a b c d e)))
(run 7 (x y)
(appendo2 x y '(a b c d e)))
Simple Relational Interpreter
(defrel (evalo exp val)
(eval-expo exp '() val))
(defrel (eval-expo exp env val)
(conde
((fresh (v)
(== `(quote ,v) exp)
(not-in-envo 'quote env)
(absento 'closure v)
(== v val)))
((fresh (a*)
(== `(list . ,a*) exp)
(not-in-envo 'list env)
(absento 'closure a*)
(proper-listo a* env val)))
((symbolo exp) (lookupo exp env val))
((fresh (rator rand x body env^ a)
(== `(,rator ,rand) exp)
(eval-expo rator env `(closure ,x ,body ,env^))
(eval-expo rand env a)
(eval-expo body `((,x . ,a) . ,env^) val)))
((fresh (x body)
(== `(lambda (,x) ,body) exp)
(symbolo x)
(not-in-envo 'lambda env)
(== `(closure ,x ,body ,env) val)))))
(defrel (not-in-envo x env)
(conde
((fresh (y v rest)
(== `((,y . ,v) . ,rest) env)
(=/= y x)
(not-in-envo x rest)))
((== '() env))))
(defrel (proper-listo exp env val)
(conde
((== '() exp)
(== '() val))
((fresh (a d t-a t-d)
(== `(,a . ,d) exp)
(== `(,t-a . ,t-d) val)
(eval-expo a env t-a)
(proper-listo d env t-d)))))
(defrel (lookupo x env t)
(fresh (rest y v)
(== `((,y . ,v) . ,rest) env)
(conde
((== y x) (== v t))
((=/= y x) (lookupo x rest t)))))
(run 1 (q)
(evalo '((lambda (x) x) 'cat) q))
(run 1 (q)
(evalo '(list 'I 'love 'programming) q))
(run 1 (expr val)
(== val '(I love programming))
(evalo expr val))
(run 2 (e)
(evalo e '(I love programming)))
((lambda (x) '(I love programming)) 'foo)
(run 99 (e)
(evalo e '(I love programming)))
quine
(run 1 (e)
(evalo e e))
((lambda (_.0) (list _.0 (list 'quote _.0)))
'(lambda (_.0) (list _.0 (list 'quote _.0))))
((lambda (x) (list x (list 'quote x)))
'(lambda (x) (list x (list 'quote x))))
Full Relational Interpreter
(load "full-interp.scm")
letrec version of append
(run 1 (q)
(evalo
`(letrec ((append (lambda (l s)
(if (null? l)
s
(cons (car l)
(append (cdr l) s))))))
(append '(a b c) '(d e)))
q))
(run 1 (q)
(evalo
`(letrec ((append (lambda (l s)
(if (null? l)
s
(cons (car l)
(append (cdr l) s))))))
(append ,q '(d e)))
'(a b c d e)))
(run 2 (q)
(evalo
`(letrec ((append (lambda (l s)
(if (null? l)
s
(cons (car l)
(append (cdr l) s))))))
(append ,q '(d e)))
'(a b c d e)))
(run 2 (q)
(evalo
`(letrec ((append (lambda (l s)
(if (null? l)
s
(cons (car l)
(append (cdr l) s))))))
(append ',q '(d e)))
'(a b c d e)))
(run 2 (q)
(evalo
`(letrec ((append (lambda (l s)
(if (null? l)
s
(cons ,q
(append (cdr l) s))))))
(append '(a b c) '(d e)))
'(a b c d e)))
