\documentstyle[a4]{article}
%;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
%File: boyer.lhs
%Description: The Boyer benchmark
%Author: Bob Boyer
%Created: 05-Apr-1985 Bob Boyer?
%Modified: 10-Apr-1985 Bob Shaw
% 22-Jul-1987 Will Clinger
% 21-Jul-1992 Converted from Scheme to Haskell
%Language: Haskell
%Status: Public Domain
%Scheme version FTP'ed from anonymous@nexus.cs.yorku.ca:pub/scheme
%;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
\title{BOYER -- Logic programming benchmark}
\author{Bob Boyer \\
Converted from Scheme to Haskell by \\
Denis Howe {\tt <dbh\@doc.ic.ac.uk>} \\
Imperial College}
\begin{document}
\maketitle
\section{Introduction}
This is a Haskell version of the ``Boyer'' benchmark from the Gabriel
suite. It rewrites a given input term according to a given set of
lemmas in an attempt to produce the value @True@ meaning that the
original term was a valid theorem.
Terms are either variables or applications of functions to (all) their
arguments. Constants are represented as functions with no arguments.
Each function has an associated set of lemmas which specify how an
application of that function may be rewritten.
\begin{code}
module Main (main) where
data Term = Var Id |
Fun Id [Term] [Lemma]
instance Eq Term where
Var i1 == Var i2 = i1 == i2
Fun f1 ts1 _ == Fun f2 ts2 _ = f1 == f2 && ts1 == ts2
_ == _ = False
\end{code}
A lemma is a pair, @(LHS,RHS)@ representing two terms which are assumed
to be equal. It is used to rewrite a term matching the LHS into one
obtained by substituting for the variables in the RHS. It could in
fact be used either way round.
\begin{code}
type Lemma = (Term, Term)
\end{code}
In attempting to match the current term against the left hand side of
a lemma, a substitution is found which binds the lemma's variables to
parts of the term. This substitution is used as the binding
environment for variables in the right hand side.
\begin{code}
type Substitution = [(Id, Term)]
\end{code}
All variables and functions have an identifier of type @Id@.
\begin{code}
data Id = A | B | C | D | X | Y | Z | U | W |
ADD1 | AND | APPEND | CONS | CONSP | DIFFERENCE |
DIVIDES | EQUAL | EVEN | EXP | F | FALSE |
FOUR | GCD | GREATEREQP | GREATERP | IF | IFF |
IMPLIES | LENGTH | LESSEQP | LESSP | LISTP | MEMBER |
NIL | NILP | NLISTP | NOT | ODD | ONE | OR | PLUS |
QUOTIENT | REMAINDER | REVERSE | SUB1 | TIMES | TRUE |
TWO | ZERO | ZEROP
deriving Eq
\end{code}
\section{Unification}
Function @one_way_unify@ is used to match (part of) the term being
rewritten (@term1@) against (part of) the LHS of a lemma (@term2@).
It takes these two terms and returns @(True,subst)@ if they are
unifiable with substitution @subst@ or @(False,error)@ if they are
not.
If @term2@ is a variable and it is bound by the current substitution
then compare its bound value against @term1@. If it is an unbound
variable then bind it to @term1@ in the returned substitution. If
both terms are function applications then compare their functions and
attempt to unify their arguments.
The unification is ``one-way'' because only @term2@ (from the lemma)
can contain free variables, @term1@ (from the term being re-written)
cannot.
\begin{code}
one_way_unify :: Term -> Term -> (Bool, Substitution)
one_way_unify term1 term2 = one_way_unify1 term1 term2 []
one_way_unify1 :: Term -> Term -> Substitution -> (Bool, Substitution)
one_way_unify1 term1 term2@(Var vid2) subst
= if found
then (term1 == v2, subst)
else (True, (vid2,term1):subst)
where (found, v2) = find vid2 subst
{-
= case find vid2 subst of { (found, v2) ->
if found
then (term1 == v2, subst)
else (True, (vid2,term1):subst)
}
-}
one_way_unify1 (Fun f1 as1 _) (Fun f2 as2 _) subst
| f1 == f2
= one_way_unify1_lst as1 as2 subst
one_way_unify1 _ _ _ = (False, error "unify")
one_way_unify1_lst [] [] subst = (True, subst)
one_way_unify1_lst (t1:ts1) (t2:ts2) subst
= (hd_ok && tl_ok, subst'')
where (hd_ok, subst') = one_way_unify1 t1 t2 subst
(tl_ok, subst'') = one_way_unify1_lst ts1 ts2 subst'
one_way_unify1_lst _ _ _ = (False, error "unify_lst")
find :: Id -> Substitution -> (Bool, Term)
find vid [] = (False, error "find")
find vid1 ((vid2,val2):bs) = if vid1 == vid2
then (True, val2)
else find vid1 bs
\end{code}
\section{Variable substitution}
Once a substitution has been found which makes the LHS of a lemma
match a term then we apply it to the lemma's RHS to get a new term.
If the term is a variable then look up its @Id@ in the substitution.
If found, return the associated value else return the original term.
If the term is an application, apply the substitution to its
arguments.
\begin{code}
apply_subst :: Substitution -> Term -> Term
apply_subst subst term@(Var vid)
= if found then value else term
where (found, value) = find vid subst
apply_subst subst (Fun f args ls)
= Fun f (map (apply_subst subst) args) ls
\end{code}
\section{Term rewriting}
Lemmas concerning a particular function are stored as part of the
@Fun@ node representing the function application. Thus, to rewrite a
term, the lemmas associated with its top-level function are searched
until one is found whose LHS will unify with the term. The term is
then rewritten using that lemma's RHS, after first applying any
substitutions required by the unification. Rewriting recurses on the
new term until there are no matching lemmas.
\begin{code}
rewrite :: Term -> Term
rewrite term@(Var _)
= term
rewrite term@(Fun f args lemmas)
= rewrite_with_lemmas (Fun f (map rewrite args) lemmas) lemmas
rewrite_with_lemmas :: Term -> [Lemma] -> Term
rewrite_with_lemmas term []
= term
rewrite_with_lemmas term ((lhs, rhs):ls)
= if unified
then rewrite (apply_subst subst rhs)
else rewrite_with_lemmas term ls
where (unified, subst) = one_way_unify term lhs
\end{code}
\section{Theorem proving}
This term rewriting aparatus can be used to prove theorems by
attempting to rewrite them to the constant @True@. Terms whose
top-level function is an @IF@ are treated specially. An @IF@ term is
true if:
\begin{itemize}
\item its condition is true and its {\em then} part is true or
\item its condition is false and its {\em else} part is true or
\item its {\em then} is true if we assume the condition is true and
its {\em else} is true if we assume the condition is false.
\end{itemize}
The current assumptions are passed to recursive calls as @true_lst@
and @false_lst@ which are initially empty.
\begin{code}
tautp :: Term -> Bool
tautp x = tautologyp (rewrite x) [] []
tautologyp :: Term -> [Term] -> [Term] -> Bool
tautologyp x true_lst false_lst
| truep x true_lst = True -- trivially or assumed true
| falsep x false_lst = False -- trivially or assumed false
tautologyp (Fun IF [cond, t, e] ls) true_lst false_lst
| truep cond true_lst = tautologyp t true_lst false_lst
| falsep cond false_lst = tautologyp e true_lst false_lst
| otherwise = tautologyp t (cond:true_lst) false_lst
&& tautologyp e true_lst (cond:false_lst)
tautologyp _ _ _ = False
\end{code}
A term is true if it is the constant @TRUE@ or if it has been assumed
to be true. Similarly a term is false if it is the constant FALSE or
if it has been assumed to be false.
\begin{code}
truep :: Term -> [Term] -> Bool
truep (Fun TRUE _ _) _ = True
truep x l = x `elem` l
falsep :: Term -> [Term] -> Bool
falsep (Fun FALSE _ _) _ = True
falsep x l = x `elem` l
\end{code}
\section{Main function and top level theorem}
The top level theorem to prove and the environment binding its
variables are defined in one big mutually recursive definition along
with all the (Haskell) functions used as shorthand for @Var@ and
@Fun@ terms.
This theorem (translated directly from the Scheme version) seems
rather strange in that none of the values bound in @subst0@ are
actually relevant to the truth of the theorem. In fact none of them
can be rewritten in any interesting way.
\begin{code}
main = print test
test :: Bool
test = all test0 (take 20 (repeat (Var X)))
test0 xxxx = tautp (apply_subst subst0 theorem)
where
subst0 = [
(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)))
]
theorem = implies (and_ (implies xxxx y)
(and_ (implies y z)
(and_ (implies z u) (implies u w))))
(implies x w)
-- Variables
a = Var A
b = Var B
c = Var C
d = Var D
u = Var U
w = Var W
x = Var X
y = Var Y
z = Var Z
-- Constants
false = Fun FALSE [] []
nil = Fun NIL [] []
true = Fun TRUE [] []
zero = Fun ZERO [] []
-- Functions with their associated lemmas
add1 a = Fun ADD1 [a] []
and_ a b
= Fun AND [a,b] [
(and_ x y, if_ x (if_ y true false) false)]
append a b
= Fun APPEND [a,b] [
(append (append x y) z, append x (append y z))]
cons a b
= Fun CONS [a,b] []
consp a = Fun CONSP [a] [
(consp (cons x y), true)]
difference a b -- natural numbers
= Fun DIFFERENCE [a,b] [
(difference x x, zero),
(difference (plus x y) x, y),
(difference (plus y x) x, y),
(difference (plus x y) (plus x z), difference y z),
(difference (plus y (plus x z)) x, plus y z),
(difference (add1 (plus y z)) z, add1 y),
(difference (add1 (add1 x)) two, x)]
divides a b
= Fun DIVIDES [a,b] [
(divides x y, zerop (remainder y x))]
equal a b
= Fun EQUAL [a,b] [
(equal (plus x y) zero, and_ (zerop x) (zerop y)),
(equal (plus x y) (plus x z), equal y z),
(equal zero (difference x y), not_ (lessp y x)),
(equal x (difference x y), or_ (equal x zero)
(zerop y)),
(equal (times x y) zero, or_ (zerop x) (zerop y)),
(equal (append x y) (append x z), equal y z),
(equal y (times x y), or_ (equal y zero)
(equal x one)),
(equal x (times x y), or_ (equal x zero)
(equal y one)),
(equal (times x y) one, and_ (equal x one)
(equal y one)),
(equal (difference x y)
(difference z y), if_ (lessp x y)
(not_ (lessp y z))
(if_ (lessp z y)
(not_ (lessp y x))
(equal x z))),
(equal (lessp x y) z, if_ (lessp x y)
(equal true z)
(equal false z))]
even_ a = Fun EVEN [a] [
(even_ x, if_ (zerop x)
true
(odd_ (sub1 x)))]
exp_ a b
= Fun EXP [a,b] [
(exp_ x (plus y z), times (exp_ x y) (exp_ x z)),
(exp_ x (times y z), exp_ (exp_ x y) z)]
f a = Fun F [a] []
four = Fun FOUR [] [
(four, add1 (add1 two))]
gcd_ a b
= Fun GCD [a,b] [
(gcd_ x y, gcd_ y x),
(gcd_ (times x z) (times y z), times z (gcd_ x y))]
greatereqp a b
= Fun GREATEREQP [a,b] [
(greatereqp x y, not_ (lessp x y))]
greaterp a b
= Fun GREATERP [a,b] [
(greaterp x y, lessp y x)]
if_ a b c
= Fun IF [a,b,c] [
(if_ (if_ x y z) u w, if_ x (if_ y u w) (if_ z u w))]
iff a b = Fun IFF [a,b] [
(iff x y, and_ (implies x y)
(implies y x))]
implies a b
= Fun IMPLIES [a,b] [
(implies x y, if_ x (if_ y true false) true)]
length_ a
= Fun LENGTH [a] [
(length_ (reverse_ x), length_ x),
(length_ (cons x (cons y (cons z (cons u w)))),
plus four (length_
w))]
lesseqp a b
= Fun LESSEQP [a,b] [
(lesseqp x y, not_ (lessp y x))]
lessp a b
= Fun LESSP [a,b] [
(lessp (remainder x y) y, not_ (zerop y)),
(lessp (quotient x y) x, and_ (not_ (zerop x))
(lessp one y)),
(lessp (plus x y) (plus x z), lessp y z),
(lessp (times x z) (times y z),
and_ (not_ (zerop z))
(lessp x y)),
(lessp y (plus x y), not_ (zerop x))]
listp a = Fun LISTP [a] [
(listp x, or_ (nilp x) (consp x))]
member a b
= Fun MEMBER [a,b] [
(member x (append y z), or_ (member x y) (member x z)),
(member x (reverse_ y), member x y)]
nilp a = Fun NILP [a] [
(nilp x, equal x nil)]
nlistp a
= Fun NLISTP [a] [
(nlistp x, not_ (listp x))]
not_ a = Fun NOT [a] [
(not_ x, if_ x false true)]
odd_ a = Fun ODD [a] [
(odd_ x, even_ (sub1 x))]
one = Fun ONE [] [
(one, add1 zero)]
or_ a b = Fun OR [a,b] [
(or_ x y, if_ x true (if_ y true false))]
plus a b
= Fun PLUS [a,b] [
(plus (plus x y) z, plus x (plus y z)),
(plus (remainder x y)
(times y (quotient x y)), x),
(plus x (add1 y), add1 (plus x y))]
quotient a b
= Fun QUOTIENT [a,b] [
(quotient (plus x (plus x y))
two, plus x (quotient y two)),
(quotient (times y x) y, if_ (zerop y) zero x)]
remainder a b
= Fun REMAINDER [a,b] [
(remainder x one, zero),
(remainder x x, zero),
(remainder (times x y) x, zero),
(remainder (times x y) y, zero)]
reverse_ a
= Fun REVERSE [a] [
(reverse_ (append x y), append (reverse_ y)
(reverse_ x))]
sub1 a = Fun SUB1 [a] [
(sub1 (add1 x), x)]
times a b
= Fun TIMES [a,b] [
(times x (plus y z), plus (times x y) (times x z)),
(times (times x y) z, times x (times y z)),
(times x (difference y z), difference (times y x)
(times z x)),
(times x (add1 y), plus x (times x y))]
two = Fun TWO [] [
(two, add1 one)]
zerop a = Fun ZEROP [a] [
(zerop x, equal x zero)]
\end{code}
\section{Original Scheme version}
The source of the Scheme version is included here for comparison.
Many of the lemmas included here have not been translated to Haskell
because they are not used by the top-level expression.
The Scheme version uses property lists to associate lemmas with their
head Lisp symbol. The procedure @setup@ takes all the lemmas and adds
them to the appropriate symbols. This work is not included in the
time for the benchmark.
The main advantage of Lisp over Haskell evident from this translation
is the ability of Lisp to manipulate Lisp programs which means that it
is not necessary to invent a new syntax in which to write the terms we
are manipulating.
The main disadvantage of Lisp shown here is the incomprehensibility of
code which takes apart structured values using @car@, @cdr@, @cadr@,
@caddr@ etc.. This is made much clearer by Haskell's use of pattern
matching and user data types. It is sometimes unclear whether the
Lisp program is dealing with a list of terms, a single term, a number
or a truth value. Haskell's strong typing is a great bonus here.
\begin{verbatim}
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; File: boyer.sch
; Description: The Boyer benchmark
; Author: Bob Boyer
; Created: 5-Apr-85
; Modified: 10-Apr-85 14:52:20 (Bob Shaw)
; 22-Jul-87 (Will Clinger)
; Language: Scheme (but see note)
; Status: Public Domain
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Note: This benchmark uses property lists. The procedures that must
; be supplied are get and put, where (put x y z) is equivalent to Common
; Lisp's (setf (get x y) z).
; Note: The Common Lisp version of this benchmark returns the wrong
; answer because it uses the Common Lisp equivalent of memv instead of
; member in the falsep and truep procedures. (The error arose because
; memv is called member in Common Lisp. Don't ask what member is called,
; unless you want to learn about keyword arguments.) This Scheme version
; may run a few percent slower than it would if it were equivalent to
; the Common Lisp version, but it works.
;;; BOYER -- Logic programming benchmark, originally written by Bob Boyer.
;;; Fairly CONS intensive.
(define unify-subst 0)
(define temp-temp 0)
(define (add-lemma term)
(cond ((and (pair? term)
(eq? (car term)
(quote equal))
(pair? (cadr term)))
(put (car (cadr term))
(quote lemmas)
(cons term (get (car (cadr term)) (quote lemmas)))))
(else (error "ADD-LEMMA did not like term: " term))))
(define (add-lemma-lst lst)
(cond ((null? lst)
#t)
(else (add-lemma (car lst))
(add-lemma-lst (cdr lst)))))
(define (apply-subst alist term)
(cond ((not (pair? term))
(cond ((begin (set! temp-temp (assq term alist))
temp-temp)
(cdr temp-temp))
(else term)))
(else (cons (car term)
(apply-subst-lst alist (cdr term))))))
(define (apply-subst-lst alist lst)
(cond ((null? lst)
#f)
(else (cons (apply-subst alist (car lst))
(apply-subst-lst alist (cdr lst))))))
(define (falsep x lst)
(or (equal? x (quote (f)))
(member x lst)))
(define (one-way-unify term1 term2)
(begin (set! unify-subst #f)
(one-way-unify1 term1 term2)))
(define (one-way-unify1 term1 term2)
(cond ((not (pair? term2))
(cond ((begin (set! temp-temp (assq term2 unify-subst))
temp-temp)
(equal? term1 (cdr temp-temp)))
(else (set! unify-subst (cons (cons term2 term1)
unify-subst))
#t)))
((not (pair? term1))
#f)
((eq? (car term1)
(car term2))
(one-way-unify1-lst (cdr term1)
(cdr term2)))
(else #f)))
(define (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)))
(else #f)))
(define (rewrite term)
(cond ((not (pair? term))
term)
(else (rewrite-with-lemmas (cons (car term)
(rewrite-args (cdr term)))
(get (car term)
(quote lemmas))))))
(define (rewrite-args lst)
(cond ((null? lst)
#f)
(else (cons (rewrite (car lst))
(rewrite-args (cdr lst))))))
(define (rewrite-with-lemmas term lst)
(cond ((null? lst)
term)
((one-way-unify term (cadr (car lst)))
(rewrite (apply-subst unify-subst (caddr (car lst)))))
(else (rewrite-with-lemmas term (cdr lst)))))
(define (setup)
(add-lemma-lst
(quote ((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 a (intersect b c))
(and (member a b)
(member a c)))
(equal (nth (zero)
i)
(zero))
(equal (exp i (plus j k))
(times (exp i j)
(exp i k)))
(equal (exp i (times j k))
(exp (exp i j)
k))
(equal (reverse-loop x y)
(append (reverse x)
y))
(equal (reverse-loop x (nil))
(reverse x))
(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 (remainder x y)
y)
(not (zerop y)))
(equal (remainder x x)
(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 (plus b (plus a c))
a)
(plus b c))
(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)))))))
(define (tautologyp x true-lst false-lst)
(cond ((truep x true-lst)
#t)
((falsep x false-lst)
#f)
((not (pair? x))
#f)
((eq? (car x)
(quote 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))
(else (and (tautologyp (caddr x)
(cons (cadr x)
true-lst)
false-lst)
(tautologyp (cadddr x)
true-lst
(cons (cadr x)
false-lst))))))
(else #f)))
(define (tautp x)
(tautologyp (rewrite x)
#f #f))
(define (test)
(define ans #f)
(define term #f)
(set! term
(apply-subst
(quote ((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)))))
(quote (implies (and (implies x y)
(and (implies y z)
(and (implies z u)
(implies u w))))
(implies x w)))))
(set! ans (tautp term))
ans)
(define (trans-of-implies n)
(list (quote implies)
(trans-of-implies1 n)
(list (quote implies)
0 n)))
(define (trans-of-implies1 n)
(cond ((equal? n 1)
(list (quote implies)
0 1))
(else (list (quote and)
(list (quote implies)
(- n 1)
n)
(trans-of-implies1 (- n 1))))))
(define (truep x lst)
(or (equal? x (quote (t)))
(member x lst)))
(setup)
;;; make sure you've run (setup) then call: (test)
(run-benchmark "Boyer" (lambda () (test)))
\end{verbatim}
\end{document}
%Local Variables:
%mode:latex
%compile-command:"ghc -Rmax-heapsize 16M boyer.lhs"
%End:
|
