From: ····@svax.UUCP
Subject: Wanted: a copy of the Boyer Lisp benchmark program
Date:
Message-ID: <1468@svax.cs.cornell.edu>
Robert Boyer wrote a benchmark theorem proving program for Lisp
systems which is described in Richard Gabriel's book on the
performance and evaluation of Lisp systems. Does anybody have an
on-line copy of the program they could send me, post, or give
me access to. The program is listed in Gabriel's book, but I would
prefer to not have to type it in.
Thanks,
Bill Pugh
····@svax.cs.cornell.edu
From: William Pugh
Subject: Re: Wanted: a copy of the Boyer Lisp benchmark program
Date:
Message-ID: <1471@svax.cs.cornell.edu>
Thanks everyone, I received a copy of it...
Bill Pugh
From: William Pugh
Subject: Re: Wanted: a copy of the Boyer Lisp benchmark program
Date:
Message-ID: <1473@svax.cs.cornell.edu>
I received a number of requests from others for copies of the benchmark
so I am posting it. I received a couple of copies - if for some reason this
version is not suitable for you, mail me and I can check the other versions I
received.
Bill Pugh
>>Here is a copy of the boyer theorem proving benchmark that I used
>>to benchmark Lucid Common Lisp, Data General Common Lisp and Kyoto
>>Common Lisp. If you are not using Common Lisp you should find it
>>no problem to translate to the dialect of your choice (watch out for
>>the :test in calls to assoc and the :test in calls to member).
>>
>> Hope this helps.
>>
>>Greg Frascadore (········@umn-cs.arpa)
>>
>> PS. To run the benchmark:
>> (load "boyer")
>> (setup)
>> (test) ;; The call to test is what you want to time
>> ;; If you have CommonLisp you could (time (test))
>>
----------------------------------cut here-----------------------------
(defvar unify-subst nil)
(defvar temp-temp nil)
;;;
(defun add-lemma (term)
(cond ((and (not (atom term))
(eq (car term) 'equal)
(not (atom (cadr term))) )
(setf (get (car (cadr term)) 'lemmas)
(cons term (get (car (cadr term))
'lemmas )) ) )
(t
(error "%ADD-LEMMA did not like the term:" term) ) ) )
;;;
(defun add-lemma-lst (lst)
(cond ((null lst) t)
(t
(add-lemma (car lst))
(add-lemma-lst (cdr lst)) ) ) )
;;;
(defun apply-subst (alist term)
(cond ((atom term)
(cond ((setq temp-temp (assoc term alist :test #'eq))
(cdr temp-temp) )
(t term) ) )
(t
(cons (car term)
(apply-subst-lst alist (cdr term)) ) ) ) )
;;;
(defun apply-subst-lst (alist lst)
(cond ((null lst) nil)
(t
(cons (apply-subst alist (car lst))
(apply-subst-lst alist (cdr lst)) ) ) ) )
;;;
(defun falsep (x lst)
(or (equal x '(f))
(member x lst :test #'equal) ) )
;;;
(defun one-way-unify (term1 term2)
(progn
(setq unify-subst nil)
(one-way-unify1 term1 term2) ) )
;;;
(defun one-way-unify1 (term1 term2)
(cond ((atom term2)
(cond ((setq temp-temp (assoc term2 unify-subst :test #'eq))
(equal term1 (cdr temp-temp)) )
(t (setq unify-subst (cons (cons term2 term1)
unify-subst) )
t ) ) )
((atom term1) nil)
((eq (car term1) (car term2))
(one-way-unify1-lst (cdr term1) (cdr term2)) )
(t nil) ) )
;;;
(defun one-way-unify1-lst (lst1 lst2)
(cond ((null lst1) t)
((one-way-unify1 (car lst1) (car lst2))
(one-way-unify1-lst (cdr lst1) (cdr lst2)) )
(t nil) ) )
;;;
(defun rewrite (term)
(cond ((atom term) term)
(t
(rewrite-with-lemmas (cons (car term)
(rewrite-args (cdr term)) )
(get (car term) 'lemmas) ) ) ) )
;;;
(defun rewrite-args (lst)
(cond ((null lst) nil)
(t
(cons (rewrite (car lst))
(rewrite-args (cdr lst)) ) ) ) )
;;;
(defun rewrite-with-lemmas (term lst)
(cond ((null lst) term)
((one-way-unify term (cadr (car lst)))
(rewrite (apply-subst unify-subst (caddr (car lst)))) )
(t
(rewrite-with-lemmas term (cdr lst)) ) ) )
;;;
(defun setup ()
(add-lemma-lst
'(
(equal (compile form)
(reverse (codegen (optimize form) (nil))) )
(equal (eqp x y)
(equal (fix x) (fix y)) )
(equal (greaterp x y)
(lessp y x))
(equal (lesseqp x y)
(not (lessp y x)))
(equal (greatereqp x y)
(not (lessp x y)))
(equal (boolean x)
(or (equal x (t))
(equal x (f)) ) )
(equal (iff x y)
(and (implies x y)
(implies y x) ) )
(equal (even1 x)
(if (zerop x) (t) (odd (1- x))) )
(equal (countps- l pred)
(countps-loop l pred (zero)) )
(equal (fact- i)
(fact-loop i 1) )
(equal (reverse- x)
(reverse-loop x (nil)) )
(equal (divides x y)
(zerop (remainder y x)) )
(equal (assume-true var alist)
(cons (cons var (t)) alist) )
(equal (assume-false var alist)
(cons (cons var (f)) alist) )
(equal (tautology-checker x)
(tautologyp (normalize x) (nil)) )
(equal (falsify x)
(falsify1 (normalize x) (nil)) )
(equal (prime x)
(and (not (zerop x))
(not (equal x (add1 (zero))))
(prime1 x (1- x)) ) )
(equal (and p q)
(if p (if q (t) (f)) (f)) )
(equal (or p q)
(if p (t) (if q (t) (f)) (f)) )
(equal (not p)
(if p (f) (t)) )
(equal (implies p q)
(if p (if q (t) (f)) (t)) )
(equal (fix x)
(if (numberp x) x (zero)) )
(equal (if (if a b c) d e)
(if a (if b d e) (if c d e)) )
(equal (zerop x)
(or (equal x (zero))
(not (numberp x)) ) )
(equal (plus (plus x y) z)
(plus x (plus y z)) )
(equal (equal (plus a b) (zero))
(and (zerop a) (zerop b)) )
(equal (difference x x)
(zero) )
(equal (equal (plus a b) (plus a c))
(equal (fix b) (fix c)) )
(equal (equal (zero) (difference x y))
(not (lessp y x)) )
(equal (equal x (difference x y))
(and (numberp x)
(or (equal x (zero))
(zerop y) ) ) )
(equal (meaning (plus-tree (append x y)) a)
(plus (meaning (plus-tree x) a)
(meaning (plus-tree y) a) ) )
(equal (meaning (plus-tree (plus-fringe x)) a)
(fix (meaning x a)) )
(equal (append (append x y) z)
(append x (append y z)) )
(equal (reverse (append a b))
(append (reverse b) (reverse a)) )
(equal (times x (plus y z))
(plus (times x y) (times x z)) )
(equal (times (times x y) z)
(times x (times y z)) )
(equal (equal (times x y) (zero))
(or (zerop x) (zerop y)) )
(equal (exec (append x y) pds envrn)
(exec y (exec x pds envrn) envrn) )
(equal (mc-flatten x y)
(append (flatten x) y) )
(equal (member x (append a b))
(or (member x a)
(member x b) ) )
(equal (member x (reverse y))
(member x y) )
(equal (length (reverse x))
(length x) )
(equal (member z (intersect b c))
(and (member a b)
(member a c) ) )
(equal (nth (zero) i)
(zero) )
(equal (exp i (plus j k))
(times (exp i h)
(exp i k) ) )
(equal (exp i (times j k))
(exp (exp i j) k) )
(equal (reverse-loop x y)
(append (reverse x) y) )
(equal (count-list z (sort-lp x y))
(plus (count-list z x)
(count-list z y) ) )
(equal (equal (append a b) (append a c))
(equal b c) )
(equal (plus (remainder x y) (times y (quotient x y)))
(fix x) )
(equal (power-eval (big-plus1 l i base) base)
(plus (power-eval l base) i ) )
(equal (power-eval (big-plus x y i base) base)
(plus i (plus (power-eval x base)
(power-eval y base) )) )
(equal (remainder y 1)
(zero) )
(equal (lessp (quotient i j) i)
(and (not (zerop i))
(or (zerop j)
(not (equal j 1)) ) ) )
(equal (lessp (remainder x y) x)
(and (not (zerop y))
(not (zerop x))
(not (lessp x y)) ))
(equal (power-eval (power-rep i base) base)
(fix i) )
(equal (power-eval (big-plus (power-rep i base)
(power-rep j base)
(zero)
base )
base )
(plus i j) )
(equal (gcd x y)
(gcd y x) )
(equal (nth (append a b) i)
(append (nth a i)
(nth b (difference i (length a))) ) )
(equal (difference (plus x y) x)
(fix y) )
(equal (difference (plus y x) x)
(fix y) )
(equal (difference (plus x y) (plus x z))
(difference y z) )
(equal (times x (difference c w))
(difference (times c x)
(times w x) ) )
(equal (remainder (times x z) z)
(zero) )
(equal (difference (add1 (plus y z)) z)
(add1 y) )
(equal (lessp (plus x y) (plus x z))
(lessp y z) )
(equal (lessp (times x z) (times y z))
(and (not (zerop z))
(lessp x y) ) )
(equal (lessp y (plus x y))
(not (zerop x)) )
(equal (gcd (times x z) (times y z))
(times z (gcd x y)) )
(equal (value (normalize x) a)
(value x a) )
(equal (equal (flatten x) (cons y (nil)))
(and (nlistp x)
(equal x y) ) )
(equal (listp (gopher x))
(listp x) )
(equal (samefringe x y)
(equal (flatten x)
(flatten y) ) )
(equal (equal (greatest-factor x y) (zero))
(and (or (zerop y)
(equal y 1) )
(equal x (zero)) ) )
(equal (equal (greatest-factor x y) 1)
(equal x 1) )
(equal (numberp (greatest-factor x y))
(not (and (or (zerop y)
(equal y 1) )
(not (numberp x)) ) ) )
(equal (times-list (append x y))
(times (times-list x)
(times-list y) ))
(equal (prime-list (append x y))
(and (prime-list x)
(prime-list y) ))
(equal (equal z (times w z))
(and (numberp z)
(or (equal z (zero))
(equal w 1) ) ) )
(equal (greatereqpr x y)
(not (lessp x y)) )
(equal (equal x (times x y))
(or (equal x (zero))
(and (numberp x)
(equal y 1 ) ) ) )
(equal (remainder (times y x) y)
(zero) )
(equal (equal (times a b) 1)
(and (not (equal a (zero)))
(not (equal b (zero)))
(numberp a)
(numberp b)
(equal (1- a) (zero))
(equal (1- b) (zero)) ) )
(equal (lessp (length (delete x l)) (length l))
(member x l) )
(equal (sort2 (delete x l))
(delete x (sort2 l)) )
(equal (dsort x)
(sort2 x) )
(equal (length
(cons
x1
(cons
x2
(cons
x3
(cons
x4
(cons
x5
(cons x6 x7) ) ) ) ) ) )
(plus 6 (length x7)) )
(equal (difference (add1 (add1 x)) 2)
(fix x) )
(equal (quotient (plus x (plus x y)) 2)
(plus x (quotient y 2)) )
(equal (sigma (zero) i)
(quotient (times i (add1 i)) 2) )
(equal (plus x (add1 y))
(if (numberp y)
(add1 (plus x y))
(add1 x) ) )
(equal (equal (difference x y)
(difference z y) )
(if (lessp x y)
(not (lessp y z))
(if (lessp z y)
(not (lessp y x))
(equal (fix x)
(fix z) ) ) ) )
(equal (meaning (plus-tree (delete x y)) a)
(if (member x y)
(difference (meaning (plus-tree y) a)
(meaning x a) )
(meaning (plus-tree y) a) ))
(equal (times x (add1 y))
(if (numberp y)
(plus x (times x y))
(fix x) ) )
(equal (nth (nil) i)
(if (zerop i)
(nil)
(zero) ) )
(equal (last (append a b))
(if (listp b)
(last b)
(if (listp a)
(cons (car (last a)) b)
b ) ) )
(equal (equal (lessp x y) z)
(if (lessp x y)
(equal t z)
(equal f z) ) )
(equal (assignment x (append a b))
(if (assignedp x a)
(assignment x a)
(assignment x b) ) )
(equal (car (gopher x))
(if (listp x)
(car (flatten x))
(zero) ) )
(equal (flatten (cdr (gopher x)))
(if (listp x)
(cdr (flatten x))
(cons (zero)
(nil) ) ) )
(equal (quotient (times y x) y)
(if (zerop y)
(zero)
(fix x) ) )
(equal (get j (set i val mem))
(if (eqp j i)
val
(get j mem) ) )
) ) )
;;;
(defun tautologyp (x true-lst false-lst)
(cond ((truep x true-lst) t)
((falsep x false-lst) nil)
((atom x) nil)
((eq (car x) 'if)
(cond ((truep (cadr x) true-lst)
(tautologyp (caddr x) true-lst false-lst) )
((falsep (cadr x) false-lst)
(tautologyp (cadddr x) true-lst false-lst) )
(t
(and (tautologyp (caddr x)
(cons (cadr x) true-lst)
false-lst )
(tautologyp (cadddr x)
true-lst
(cons (cadr x) false-lst) ) ) ) ) )
(t nil) ) )
;;;
(defun tautp (x)
(tautologyp (rewrite x) nil nil) )
;;;
(defun test ()
(tautp (apply-subst
'((x f (plus (plus a b)
(plus c (zero)) ) )
(y f (times (times a b)
(plus c d) ) )
(z f (reverse (append (append a b) (nil))))
(u equal (plus a b)
(difference x y) )
(w lessp (remainder a b)
(member a (length b)) ) )
'(implies (and (implies x y)
(and (implies y z)
(and (implies z u)
(implies u w) ) ) )
(implies x w) ) ) ) )
;;;
(defun truep (x lst)
(or (equal x '(t))
(member x lst :test #'equal) ) )
;;;
From: Mike Clarkson
Subject: Re: Wanted: a copy of the Boyer Lisp benchmark program
Date:
Message-ID: <498@yetti.UUCP>
In article <····@svax.cs.cornell.edu> ····@svax.cs.cornell.edu (William Pugh) writes:
>I received a number of requests from others for copies of the benchmark
>so I am posting it.
I have a complete set of the Gabriel Benchmarks in Common Lisp, kindly
provided to me by Stan Shebs at Utah. If there is sufficient
demand, say 10-15 requests and not too many nays, I'd be happy to
post them. Let me know *by mail* if you want/don't want me to post them.
decvax!utzoo!yetti!mike or seismo!mnetor!yetti!mike or ······@YUSOL.BITNET
--
Mike Clarkson, ...!allegra \ BITNET: ····@YUYETTI or
CRESS, York University, ...!decvax \ ······@YUSOL
4700 Keele Street, ...!ihnp4 > !utzoo!yetti!mike
North York, Ontario, ...!linus /
CANADA M3J 1P3. ...!watmath / Phone: +1 (416) 736-2100 x 7767
"...the most inevitable business communications system on the planet."
- ROLM magazine advertisement
which planet?