Rewrite Engines Competition

From FSL
Jump to: navigation, search

Contents

(Unconditional) Term Rewrite Systems

Permutations

Operations:

 z(0),suc(1),nil(0),cons(2),
 perm(1),insert0(2),insert1(2),map-cons(2),count(1)
The result of count should be built-in naturals.

Specification:

 append(P ; Ps,Ps') --> P ; append(Ps,Ps')
 append(nilP,Ps') --> Ps'
 perm(z) --> nil ; nilP
 perm(suc(z)) --> (suc(z),nil) ; nilP
 perm(suc(N)) --> insert1(suc(N), perm(N))
 insert1(N, (P ; Ps)) --> append(insert0(N,P) , insert1(N,Ps))
 insert1(N,nilP) --> nilP
 insert0(N, (M,P')) --> (N,M,P') ; map-cons(M, insert0(N,P'))
 insert0(N, nil) --> (N,nil) ; nilP
 map-cons(M, (P ; Ps)) --> (M, P) ; map-cons(M, Ps)
 map-cons(M, nilP) --> nilP
 count(nilP) --> 0
 count(P ; Ps) --> s(count(Ps))

Factorial

Operations (assume numbers (0, s, *) are already specified or built-in ):

fact(1)

Specification:

fact(0) --> s(0) 
fact(s(n)) --> s(n) * fact(n)

Fibbonaci

Operations (assume numbers (0, s, +) are already specified or built-in ):

fibb(1)

Specification:

fibb(0) --> s(0) 
fibb(1) --> s(0)
fibb(s(s(n))) --> fibb(s(n)) + fibb(n)

Merge-sort

Operations (assume integers with comaration predicates are specified of built-in):

nil,pair(2),cons(2),split(1),merge(2),mergesort(1)

Specification:

merge(nil,L) --> L 
merge(cons(x,Lx),cons(y,Ly)) --> cons(x,merge(Lx,cons(y,Ly))) if x < y
merge(cons(x,Lx),cons(y,Ly)) --> cons(y,merge(cons(x,Lx),Ly)) if x >= y
split(cons(x,cons(y,L))) --> pair(cons(x,Lx),cons(y,Ly)) 
 if split(L) --> pair(Lx,Ly)
split(nil) --> pair(nil,nil) 
split(cons(x,nil)) --> pair(cons(x,nil),nil)
mergesort(nil) --> nil 
mergesort(cons(x,nil)) --> cons(x,nil) 
mergesort(cons(x,cons(y,L))) -->   
  merge(mergesort(cons(x,Lx)),mergesort(cons(y,Ly))) 
  if split(L) --> pair(Lx,Ly)

Garbage collection test

Operations:

0,1,m,n,f(5) c(2)  : S S S S S -> S .

Specification:

1 --> s(0)
m --> s(s(s(s(0))))
n --> s(s(s(0)))
p --> s(s(s(s(s(0)))))
c(0,Y) --> Y 
c(s(X),Y) --> s(c(X,Y)) 
f(X,Y,s(Z),T,U) --> f(X,Y,Z,c(T,T),U) 
f(X,s(Y),0,T,U) --> f(X,Y,p,T,T) 
f(s(X),0,0,T,U) --> f(X,n,p,1,0) 
f(0,0,0,T,U) --> T 

Test: try to reduce a term of the form (definitions for m,n and p may be change to get relevant results

f(m,n,p,0,1) .

Rewriting modulo equations

(A) Permutations

Operations:

 z(0),suc(1),nil(0),cons(2),
 perm(1),insert0(2),insert1(2),map-cons(2),count(1)
Result of count should be built-in naturals

Specification:

 append(P ; Ps,Ps') --> P ; append(Ps,Ps')
 append(nilP,Ps') --> Ps'
 perm(z) --> nil ; nilP
 perm(suc(z)) --> (suc(z),nil) ; nilP
 perm(suc(N)) --> insert1(suc(N), perm(N))
 insert1(N, (P ; Ps)) --> append(insert0(N,P) , insert1(N,Ps))
 insert1(N,nilP) --> nilP
 insert0(N, (M,P')) --> (N,M,P') ; map-cons(M, insert0(N,P'))
 insert0(N, nil) --> (N,nil) ; nilP
 map-cons(M, (P ; Ps)) --> (M, P) ; map-cons(M, Ps)
 map-cons(M, nilP) --> nilP
 count(nilP) --> 0
 count(P ; Ps) --> s(count(Ps))

(AU) List Length

Operations (assumes built in natural numbers with 0 and successor s):

elt(1),cons(2),nil(0), length(1)

Specification: cons is associative with identity nil and

length(nil) --> 0
length(cons(elt(X),L)) --> s(length(L))

(AC) Satisfiability checker

Operations:

true(0),false(0),not(1), and(2), xor(2), or(2), implies(2)

Specification: and, or and xor are associative and commutative and

 and(true,A) --> A
 and(false,A) -->false
 and(A,A) --> A
 xor(false,A) --> A
 xor(A,A) --> false
 and(A,xor(B,C)) --> xor(and(A,B),and(A,C))
 not(A) --> xor(A,true)
 or(A,B) --> xor(xor(and(A,B),A),B)
 implies(A,B) --> not(xor(A,and(A,B)))

Conditional Term Rewrite Systems

Bubble-sort

Operations (assume built in integers with an less than (<) operator on them):

cons(2)

Specification:

cons(x,cons(y,L)) --> cons(y,cons(x,L)) if y < x

Odd/Even

Operations:

true,false,0,s(1),odd(1),even(1)

Specification:

odd(0) --> false
even(0) --> true
odd(s(x)) --> true if even(x) --> true
even(s(x)) --> true if odd(x) --> true
odd(s(x)) --> false if even(x) --> false
even(s(x)) --> false if odd(x) --> false

Quick-sort

Operations (assuming built in integers with comparation predicates on them):

pair(2), cons(2), split(2), qsort(1)

Specification:

split(x,cons(y,L)) --> pair(LTx,cons(y,GTx)) if x < y and split(x,L) --> pair(LTx,GTx)
split(x,cons(y,L)) --> pair(cons(y,LTx),GTx) if x >= y  and split(x,L) --> pair(LTx,GTx)
split(x,nil) --> pair(nil,nil) 
qsort(nil) = nil 
qsort(cons(x,L)) = append(qsort(LTx), cons(x,qsort(GTx)) if split(x,L) --> pair(LTx,GTx)

Marchiori

Operations:

a,b,c,d,e,k,l,m,A,B,f(1),h(2),g(3)

Specification:

a --> c
a --> d 
b --> c
b --> d 
c --> e
c --> l
d --> m
k --> l
k --> m 
A --> h(f(a),f(b)) 
g(d,x,x) --> B
h(x,x) --> g(x,x,f(k))
f(x) --> x if x --> e
B --> A

Test:

does A rewrites to B (implying non-termination)?

Confluence

Operations:

0,f(1),g(1)

Specification:

f(g(x)) --> x if x --> 0
g(g(x)) --> g(x)

Test:

Get all normal forms of f(g(g(0)))

Soundness of parallel engines

Operations:

0,f(1),g(1)

Specification:

f(g(x)) --> x if x --> s(0)
g(s(x)) --> g(x)

Test:

normal form for f(g(s(0)))

Search in conditions?

Operations:

 true,false,a,not(1)

Specification (order matters):

a --> true 
a --> false 
not(x) --> true if x --> false

Test:

does not(a) rewrites to true?

Termination, reachability?

Operations:

a,b,c

Specification (order matters):

a --> c if a --> b 
a --> b
b --> c

Test:

get a normal form for a
test whether a rewrites to b?

ASF/SDF Benchmark

We are grateful to professor Mark van der Brand for providing us this benchmark.

Informal specification

In the sequel, identifiers starting with capital letters denote variables. All other denote operations. Also, this benchmark assumes the rewrite engine supports a default strategy to handle otherwise untreated cases.

Boolean equations

or(true, Bool)   --> true
or(false, Bool)  --> Bool
and(true, Bool)  --> Bool
and(false, Bool) --> false
not ( false ) --> true
not ( true )  --> false

Normal operations on naturals

plus(X,z) --> X
plus(X,s(Y)) --> s(plus(X,Y))
mult(X,z) --> z
mult(X,s(Y)) --> plus(mult(X,Y),X)
exp(X,z) --> s(z)
exp(X,s(Y)) --> mult(X,exp(X,Y))
equal(X, X) --> true
[default] equal(X, Y) --> false
less(z, X) --> true
less(s(X),s(Y)) --> less(X,Y)
[default] less(X,Y) --> false

We are working modulo 17

succ17(s(s(s(s(s(s(s(s(s(s(s(s(
                  s(s(s(s(z))))))))))))))))) --> z
[default] succ17(X) --> s(X)
pred17(s(X)) --> X
pred17(z) --> s(s(s(s(s(s(s(s(s(s(s(s(
                  s(s(s(s(z))))))))))))))))

Operations on naturals modulo 17

plus17(X,z) --> X
plus17(X,s(Y)) --> succ17(plus17(X,Y))
mult17(X,z) --> z
mult17(X,s(Y)) --> plus17(X,mult17(X,Y))
[mod-7] exp17(X,z) --> succ17(z)
[mod-8] exp17(X,s(Y)) --> mult17(X,exp17(X,Y))

Complete evaluation of expressions

eval(exz) --> z
eval(exs(Xs)) --> s(eval(Xs))
eval(explus(Xs,Ys)) --> plus(eval(Xs), eval(Ys))
eval(exmult(Xs,Ys)) --> mult(eval(Xs), eval(Ys))
eval(exexp(Xs,Ys))  --> exp(eval(Xs), eval(Ys))

Fast evaluation modulo 17

eval17(exz) --> z
eval17(exs(Xs)) --> succ17(eval17(Xs))
eval17(explus(Xs,Ys)) --> plus17(eval17(Xs),eval17(Ys))
eval17(exmult(Xs,Ys)) --> mult17(eval17(Xs),eval17(Ys))
eval17(exexp(Xs,Ys))  --> exp17(eval17(Xs),eval(Ys))

Some symbolic natural constants

one --> exs(exz)
two --> exs(one)
three --> exs(two)
four --> exs(three)
five --> exs(four)
six --> exs(five)
seven --> exs(six)
eight --> exs(seven)
nine --> exs(eight)
ten --> exs(nine)
eleven --> exs(ten)
twelve --> exs(eleven)
thirteen --> exs(twelve)
fourteen --> exs(thirteen)
fifteen --> exs(fourteen)
sixteen --> exs(fifteen)
seventeen --> exs(sixteen)
eighteen --> exs(seventeen)
nineteen --> exs(eighteen)
twenty --> exs(nineteen)
twentyone --> exs(twenty)
twentytwo --> exs(twentyone)
twentythree --> exs(twentytwo)
twentyfour --> exs(twentythree)
twentyfive --> exs(twentyfour)
twentysix --> exs(twentyfive)
twentyseven --> exs(twentysix)
twentyeight --> exs(twentyseven)
twentynine --> exs(twentyeight)
thirty --> exs(twentynine)
thirtyone --> exs(thirty)
thirtytwo --> exs(thirtyone)
thirtythree --> exs(thirtytwo)
thirtyfour --> exs(thirtythree)
thirtyfive --> exs(thirtyfour)

Translation from naturals to symbolic naturals

nat2sym(z) --> exz
nat2sym(s(X)) --> exs(nat2sym(X))

Some natural constants

0 --> z
1 --> s(0)
2 --> s(1)
3 --> s(2)
4 --> s(3)
5 --> s(4)
6 --> s(5)
7 --> s(6)
8 --> s(7)
9 --> s(8)
10 --> s(9)
11 --> s(10)
12 --> s(11)
13 --> s(12)
14 --> s(13)
15 --> s(14)
16 --> s(15)
17 --> s(16)

Symbolic evaluation of expressions modulo 17

evalsym17(exz) --> z
evalsym17(exs(Xs)) --> succ17(evalsym17(Xs))
evalsym17(explus(Xs,Ys)) --> plus17(evalsym17(Xs),evalsym17(Ys))
evalsym17(exmult(Xs,exz)) --> z
evalsym17(exmult(Xs,exs(Ys))) -->
               evalsym17(explus(exmult(Xs,Ys),Xs))
evalsym17(exmult(Xs,explus(Ys,Zs))) -->
               evalsym17(explus(exmult(Xs,Ys),exmult(Xs,Zs)))
evalsym17(exmult(Xs,exmult(Ys,Zs))) -->
               evalsym17(exmult(exmult(Xs,Ys),Zs))
evalsym17(exmult(Xs,exexp(Ys,Zs))) -->
               evalsym17(exmult(Xs,dec(exexp(Ys,Zs))))
dec(exexp(Xs,exz)) --> exs(exz)
dec(exexp(Xs,exs(Ys))) --> exmult(exexp(Xs,Ys),Xs)
dec(exexp(Xs,explus(Ys,Zs))) -->
               exmult(exexp(Xs,Ys),exexp(Xs,Zs))
dec(exexp(Xs,exmult(Ys,Zs))) -->
               dec(exexp(exexp(Xs,Ys),Zs))
dec(exexp(Xs,exexp(Ys,Zs))) -->
               dec(exexp(Xs, dec(exexp(Ys,Zs))))
evalsym17(exexp(Xs,exz)) --> succ17(z)
evalsym17(exexp(Xs,exs(Ys))) -->
               evalsym17(exmult(exexp(Xs,Ys),Xs))
evalsym17(exexp(Xs,explus(Ys,Zs))) -->
               evalsym17(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))
evalsym17(exexp(Xs,exmult(Ys,Zs))) -->
               evalsym17(exexp(exexp(Xs,Ys),Zs))
evalsym17(exexp(Xs,exexp(Ys,Zs))) -->
               evalsym17(exexp(Xs,dec(exexp(Ys,Zs))))

Symbolic evaluation after expansion

evalexp17(Xs) --> eval17(expand(Xs))
expand(exz) --> exz
expand(exs(Xs)) --> explus(exs(exz),expand(Xs))
expand(explus(Xs2,Ys2)) --> explus(expand(Xs2),expand(Ys2))
expand(exmult(Xs,exz)) --> exz
expand(exmult(Xs,exs(exz))) --> expand(Xs)
expand(exmult(Xs,explus(Ys,Zs))) -->
               expand(explus(exmult(Xs,Ys),exmult(Xs,Zs)))
[default] expand(exmult(Xs1,Ys1)) --> 
               expand(exmult(Xs1,expand(Ys1)))
expand(exexp(Xs,exz)) --> exs(exz)
expand(exexp(Xs,exs(exz))) --> expand(Xs)
expand(exexp(Xs,explus(Ys,Zs))) -->
               expand(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))
[default] expand(exexp(Xs,Ys)) --> expand(exexp(Xs, expand(Ys)))

Tree benchmark

getval(leaf(Val)) --> Val
getval(node(Val,Max,Left,Right)) --> Val
getmax(leaf(Val)) --> Val
getmax(node(Val,Max,Left,Right)) --> Max
buildtree(z, Val) --> leaf(Val)
buildtree(s(X), Y) --> node(Val, Max, Left, Right) if
             Left <-- buildtree(X, Y),
             Max' <-- getmax(Left),
             Right <-- buildtree(X, succ17(Max')),
             Val' <-- getval(Left),
             Val <-- getval(Right),
             Val <-- plus17(Val', Val),
             Max <-- getmax(Right)
 calctree17(X) --> mult17(I,J) if
            I <-- exp17(s(s(z)), pred17(X)),
            J <-- pred17(exp17(s(s(z)),X))


Benchmark equations

bench-evalsym17(Xs) --> equal(eval17(Zs),evalsym17(Zs)) if
         Zs <-- exexp(two,Xs)
bench-evalexp17(Xs) --> equal(eval17(Zs),evalexp17(Zs)) if
         Zs <-- exexp(two,Xs)
bench-evaltree17(Xs) --> equal(calctree17(X),
         getval(buildtree(X, z))) if  X <-- eval(Xs)

Particular rewrite engines specifications

ASF/SDF Sources

SDF source
module Benchmark
imports Layout
exports
 sorts Nat SNat Bool Tree
 context-free syntax
   "true"                -> Bool
   "false"               -> Bool
   "or" "(" Bool "," Bool ")"       -> Bool
   "and" "(" Bool "," Bool ")"       -> Bool
   "not"  "("  Bool  ")"         -> Bool
   "z"                   -> Nat
   "s" "(" Nat ")"               -> Nat
   "equal" "(" Nat ","  Nat ")"      -> Bool
   "less" "(" Nat ","  Nat ")"       -> Bool
   "plus" "(" Nat ","  Nat ")"       -> Nat
   "mult" "(" Nat ","  Nat ")"       -> Nat
   "exp" "(" Nat ","  Nat ")"        -> Nat
   "succ17" "(" Nat ")"          -> Nat
   "pred17" "(" Nat ")"          -> Nat
   "plus17" "(" Nat ","  Nat ")"     -> Nat
   "mult17" "(" Nat ","  Nat ")"     -> Nat
   "exp17" "(" Nat ","  Nat ")"      -> Nat
   "exz"                   -> SNat  %% The constant 0
   "exs" "(" SNat ")"              -> SNat  %% successor
   "explus" "(" SNat ","  SNat ")"     -> SNat
   "exmult" "(" SNat ","  SNat ")"     -> SNat
   "exexp" "(" SNat ","  SNat ")"      -> SNat
   "leaf" "(" Nat ")"                   -> Tree
   "node" "(" Nat ","  Nat ","  Tree ","  Tree ")"  -> Tree
   "buildtree" "(" Nat ","  Nat ")"         -> Tree
   "calctree17" "(" Nat ")"             -> Nat
   "getmax" "(" Tree ")"                -> Nat
   "getval" "(" Tree ")"                -> Nat
   %% Several eval functions
   "eval" "(" SNat ")"            -> Nat
   "eval17" "(" SNat ")"          -> Nat
   "evalsym17" "(" SNat ")"       -> Nat
   "evalexp17" "(" SNat ")"       -> Nat
   %% The benchmarks
   "bench-evalsym17" "(" SNat ")"            -> Bool
   "bench-evalexp17" "(" SNat ")"            -> Bool
   "bench-evaltree17" "(" SNat ")"           -> Bool
   %% Some constants
   "zero"        -> SNat
   "one"         -> SNat
   "two"         -> SNat
   "three"       -> SNat
   "four"        -> SNat
   "five"        -> SNat
   "six"         -> SNat
   "seven"       -> SNat
   "eight"       -> SNat
   "nine"        -> SNat
   "ten"         -> SNat
   "eleven"      -> SNat
   "twelve"      -> SNat
   "thirteen"    -> SNat
   "fourteen"    -> SNat
   "fifteen"     -> SNat
   "sixteen"     -> SNat
   "seventeen"   -> SNat
   "eighteen"    -> SNat
   "nineteen"    -> SNat
   "twenty"      -> SNat
   "twentyone"   -> SNat
   "twentytwo"   -> SNat
   "twentythree" -> SNat
   "twentyfour"  -> SNat
   "twentyfive"  -> SNat
   "twentysix"   -> SNat
   "twentyseven" -> SNat
   "twentyeight" -> SNat
   "twentynine"  -> SNat
   "thirty"      -> SNat
   "thirtyone"   -> SNat
   "thirtytwo"   -> SNat
   "thirtythree" -> SNat
   "thirtyfour"  -> SNat
   "thirtyfive"  -> SNat
 %% Test constants
 "0"           -> Nat
 "1"           -> Nat
 "2"           -> Nat
 "3"           -> Nat
 "4"           -> Nat
 "5"           -> Nat
 "6"           -> Nat
 "7"           -> Nat
 "8"           -> Nat
 "9"           -> Nat
 "10"          -> Nat
 "11"          -> Nat
 "12"          -> Nat
 "13"          -> Nat
 "14"          -> Nat
 "15"          -> Nat
 "16"          -> Nat
 "17"          -> Nat
variables
   "Bool"[0-9\']* -> Bool
   "X"[0-9\']*    -> Nat
   "Y"[0-9\']*    -> Nat
   "Z"[0-9\']*    -> Nat
   "Xs"[0-9\']*   -> SNat
   "Ys"[0-9\']*   -> SNat
   "Zs"[0-9\']*   -> SNat
   "I"[0-9\']*    -> Nat
   "J"[0-9\']*    -> Nat
   "K"[0-9\']*    -> Nat
   "L"[0-9\']*    -> Nat
hiddens
 sorts NatPair
 context-free syntax
   "dec" "(" SNat ")"             -> SNat
   "expand" "(" SNat ")"          -> SNat
   "exone"               -> SNat
   "nat2sym" "(" Nat ")"  -> SNat
 variables
   "P"[0-9\']*    -> NatPair
   "P*"[0-9\']* -> NatPair*
   "Left"        -> Tree
   "Right"       -> Tree
   "Max"[\']*     -> Nat
   "Val"[\']*     -> Nat


ASF source
%% Boolean equations
[B1]   or(true, Bool)   = true
[B2]   or(false, Bool)  = Bool
[B3]   and(true, Bool)  = Bool
[B4]   and(false, Bool) = false
[B5]   not ( false ) = true
[B6]   not ( true )  = false
%% Normal operations on naturals
[nat-1] plus(X,z) = X
[nat-2] plus(X,s(Y)) = s(plus(X,Y))
[nat-3] mult(X,z) = z
[nat-4] mult(X,s(Y)) = plus(mult(X,Y),X)
[nat-5] exp(X,z) = s(z)
[nat-6] exp(X,s(Y)) = mult(X,exp(X,Y))
[nat-7] equal(X, X) = true
[default-8] equal(X, Y) = false
[nat-9] less(z, X) = true
[nat-10] less(s(X),s(Y)) = less(X,Y)
[default-9] less(X,Y) = false
%% We are working modulo 17
[mod-1] succ17(s(s(s(s(s(s(s(s(s(s(s(s(
                  s(s(s(s(z))))))))))))))))) = z
[default-mod-2] succ17(X) = s(X)
[pred-1] pred17(s(X)) = X
[pred-2] pred17(z) = s(s(s(s(s(s(s(s(s(s(s(s(
                  s(s(s(s(z))))))))))))))))
%% Operations on naturals modulo 17
[mod-3] plus17(X,z) = X
[mod-4] plus17(X,s(Y)) = succ17(plus17(X,Y))
[mod-5] mult17(X,z) = z
[mod-6] mult17(X,s(Y)) = plus17(X,mult17(X,Y))
[mod-7] exp17(X,z) = succ17(z)
[mod-8] exp17(X,s(Y)) = mult17(X,exp17(X,Y))
%% Complete evaluation of expressions
[eval-1] eval(exz) = z
[eval-2] eval(exs(Xs)) = s(eval(Xs))
[eval-3] eval(explus(Xs,Ys)) = plus(eval(Xs), eval(Ys))
[eval-4] eval(exmult(Xs,Ys)) = mult(eval(Xs), eval(Ys))
[eval-5] eval(exexp(Xs,Ys))  = exp(eval(Xs), eval(Ys))
%% Fast evaluation modulo 17
[mod17-1] eval17(exz) = z
[mod17-2] eval17(exs(Xs)) = succ17(eval17(Xs))
[mod17-3] eval17(explus(Xs,Ys)) = plus17(eval17(Xs),eval17(Ys))
[mod17-4] eval17(exmult(Xs,Ys)) = mult17(eval17(Xs),eval17(Ys))
[mod17-5] eval17(exexp(Xs,Ys))  = exp17(eval17(Xs),eval(Ys))
%% Some symbolic natural constants
[const-1] one = exs(exz)
[const-2] two = exs(one)
[const-3] three = exs(two)
[const-4] four = exs(three)
[const-5] five = exs(four)
[const-6] six = exs(five)
[const-7] seven = exs(six)
[const-8] eight = exs(seven)
[const-9] nine = exs(eight)
[const-10] ten = exs(nine)
[const-11] eleven = exs(ten)
[const-12] twelve = exs(eleven)
[const-13] thirteen = exs(twelve)
[const-14] fourteen = exs(thirteen)
[const-15] fifteen = exs(fourteen)
[const-16] sixteen = exs(fifteen)
[const-17] seventeen = exs(sixteen)
[const-18] eighteen = exs(seventeen)
[const-19] nineteen = exs(eighteen)
[const-20] twenty = exs(nineteen)
[const-21] twentyone = exs(twenty)
[const-22] twentytwo = exs(twentyone)
[const-23] twentythree = exs(twentytwo)
[const-24] twentyfour = exs(twentythree)
[const-25] twentyfive = exs(twentyfour)
[const-26] twentysix = exs(twentyfive)
[const-27] twentyseven = exs(twentysix)
[const-28] twentyeight = exs(twentyseven)
[const-29] twentynine = exs(twentyeight)
[const-30] thirty = exs(twentynine)
[const-31] thirtyone = exs(thirty)
[const-32] thirtytwo = exs(thirtyone)
[const-33] thirtythree = exs(thirtytwo)
[const-34] thirtyfour = exs(thirtythree)
[const-35] thirtyfive = exs(thirtyfour)
%% Translation from naturals to symbolic naturals
[n2s-0] nat2sym(z) = exz
[n2s-1] nat2sym(s(X)) = exs(nat2sym(X))
%% Some natural constants
[n-0] 0 = z
[n-1] 1 = s(0)
[n-2] 2 = s(1)
[n-3] 3 = s(2)
[n-4] 4 = s(3)
[n-5] 5 = s(4)
[n-6] 6 = s(5)
[n-7] 7 = s(6)
[n-8] 8 = s(7)
[n-9] 9 = s(8)
[n-10] 10 = s(9)
[n-11] 11 = s(10)
[n-12] 12 = s(11)
[n-13] 13 = s(12)
[n-14] 14 = s(13)
[n-15] 15 = s(14)
[n-16] 16 = s(15)
[n-17] 17 = s(16)
%% Symbolic evaluation of expressions modulo 17
[evalsym-1] evalsym17(exz) = z
[evalsym-2] evalsym17(exs(Xs)) = succ17(evalsym17(Xs))
[evalsym-3] evalsym17(explus(Xs,Ys)) = plus17(evalsym17(Xs),evalsym17(Ys))
[evalsym-4] evalsym17(exmult(Xs,exz)) = z
[evalsym-5] evalsym17(exmult(Xs,exs(Ys))) =
               evalsym17(explus(exmult(Xs,Ys),Xs))
[evalsym-6] evalsym17(exmult(Xs,explus(Ys,Zs))) =
               evalsym17(explus(exmult(Xs,Ys),exmult(Xs,Zs)))
[evalsym-7] evalsym17(exmult(Xs,exmult(Ys,Zs))) =
               evalsym17(exmult(exmult(Xs,Ys),Zs))
[evalsym-8] evalsym17(exmult(Xs,exexp(Ys,Zs))) =
               evalsym17(exmult(Xs,dec(exexp(Ys,Zs))))
[evalsym-9]  dec(exexp(Xs,exz)) = exs(exz)
[evalsym-10] dec(exexp(Xs,exs(Ys))) = exmult(exexp(Xs,Ys),Xs)
[evalsym-11] dec(exexp(Xs,explus(Ys,Zs))) =
               exmult(exexp(Xs,Ys),exexp(Xs,Zs))
[evalsym-11] dec(exexp(Xs,exmult(Ys,Zs))) =
               dec(exexp(exexp(Xs,Ys),Zs))
[evalsym-12] dec(exexp(Xs,exexp(Ys,Zs))) =
               dec(exexp(Xs, dec(exexp(Ys,Zs))))
[evalsym-13] evalsym17(exexp(Xs,exz)) = succ17(z)
[evalsym-14] evalsym17(exexp(Xs,exs(Ys))) =
               evalsym17(exmult(exexp(Xs,Ys),Xs))
[evalsym-15] evalsym17(exexp(Xs,explus(Ys,Zs))) =
               evalsym17(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))
[evalsym-16] evalsym17(exexp(Xs,exmult(Ys,Zs))) =
               evalsym17(exexp(exexp(Xs,Ys),Zs))
[evalsym-17] evalsym17(exexp(Xs,exexp(Ys,Zs))) =
               evalsym17(exexp(Xs,dec(exexp(Ys,Zs))))
%% Symbolic evaluation after expansion
[evalexp-1] evalexp17(Xs) = eval17(expand(Xs))
[expand-1] expand(exz) = exz
[expand-3] expand(exs(Xs)) = explus(exs(exz),expand(Xs))
[expand-6] expand(explus(Xs2,Ys2)) = explus(expand(Xs2),expand(Ys2))
[expand-7] expand(exmult(Xs,exz)) = exz
[expand-8] expand(exmult(Xs,exs(exz))) = expand(Xs)
[expand-9] expand(exmult(Xs,explus(Ys,Zs))) =
               expand(explus(exmult(Xs,Ys),exmult(Xs,Zs)))
[default-expand-9]
       expand(exmult(Xs1,Ys1)) = expand(exmult(Xs1,expand(Ys1)))
[expand-10] expand(exexp(Xs,exz)) = exs(exz)
[expand-11] expand(exexp(Xs,exs(exz))) = expand(Xs)
[expand-12] expand(exexp(Xs,explus(Ys,Zs))) =
               expand(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))
[default-expand-13]
       expand(exexp(Xs,Ys)) = expand(exexp(Xs, expand(Ys)))
%% Tree benchmark
[getval-1] getval(leaf(Val)) = Val
[getval-2] getval(node(Val,Max,Left,Right)) = Val
[getmax-1] getmax(leaf(Val)) = Val
[getmax-2] getmax(node(Val,Max,Left,Right)) = Max
[buildtree-1] buildtree(z, Val) = leaf(Val)
[buildtree-2] Left = buildtree(X, Y),
             Max' = getmax(Left),
             Right = buildtree(X, succ17(Max')),
             Val' = getval(Left),
             Val = getval(Right),
             Val = plus17(Val', Val),
             Max = getmax(Right)
             ================================================
             buildtree(s(X), Y) = node(Val, Max, Left, Right)
[calctree-1]
 I = exp17(s(s(z)), pred17(X)),
 J = pred17(exp17(s(s(z)),X))
 ============================
 calctree17(X) = mult17(I,J)
%% Benchmark equations
[bench-1] Zs = exexp(two,Xs)
         =====================================================
         bench-evalsym17(Xs) = equal(eval17(Zs),evalsym17(Zs))
[bench-2] Zs = exexp(two,Xs)
         =====================================================
         bench-evalexp17(Xs) = equal(eval17(Zs),evalexp17(Zs))
[bench-3] X = eval(Xs)
         =====================================================
         bench-evaltree17(Xs) = equal(calctree17(X),
                                      getval(buildtree(X, z)))


The Layout
%%%%
%%%% $Id: Layout.sdf2,v 1.1 2000/04/26 14:51:29 jurgenv Exp $
%%%%
%%%% This file is part of the specification
%%%%    "Box: Language, Laws and Formatters"
%%%%
%%%% Copyright (c) Mark van den Brand & Eelco Visser, 1995
%%%%
%%%% Programming Research Group, University of Amsterdam
%%%% Kruislaan 403, 1098 SJ Amsterdam, The Netherlands.
%%%% mail:markvdb@fwi.uva.nl http://adam.fwi.uva.nl/~markvdb/
%%%% mail:visser@fwi.uva.nl  http://adam.fwi.uva.nl/~visser/
%%%%
%% \module{Layout}
module Layout
exports
  lexical syntax
    [\ \t\n]         -> LAYOUT
    "%%" ~[\n]* "\n" -> LAYOUT
    "%" ~[\%\n]+ "%" -> LAYOUT
  context-free restrictions
    LAYOUT? -/- [\ \t\n\%]

Elan sources

ELN file
module benchmark
import global eq[Nat];
end
sort Bool Nat SNat Tree NatPair;
end
operators global
 'true'                : Bool;
 'false'               : Bool;
 'or' '(' @ ',' @ ')'  : (Bool Bool) Bool;
 'and' '(' @ ',' @ ')' : (Bool Bool) Bool;
 'not' '(' @ ')'       : (Bool) Bool;
 'zero'                  : Nat; 
 's' '(' @ ')'           : (Nat) Nat;
 'equal' '(' @ ',' @ ')' : (Nat Nat) Bool;
 'less' '(' @ ',' @ ')'  : (Nat Nat) Bool;

 'plus' '(' @ ',' @ ')'  : (Nat Nat) Nat;
 'mult' '(' @ ',' @ ')'  : (Nat Nat) Nat;
 'exp' '(' @ ',' @ ')'   : (Nat Nat) Nat;
 'succ17' '(' @ ')'        : (Nat) Nat;
 'pred17' '(' @ ')'        : (Nat) Nat;
 'plus17' '(' @ ',' @ ')'  : (Nat Nat) Nat;
 'mult17' '(' @ ',' @ ')'  : (Nat Nat) Nat;
 'exp17' '(' @ ',' @ ')'   : (Nat Nat) Nat;
 'exz'                    : SNat;
 'exs' '(' @ ')'          : (SNat) SNat;
 'explus' '(' @ ',' @ ')' : (SNat SNat) SNat;
 'exmult' '(' @ ',' @ ')' : (SNat SNat) SNat;
 'exexp' '(' @ ',' @ ')'  : (SNat SNat) SNat;
 'leaf' '(' @ ')'                   : (Nat) Tree;
 'node' '(' @ ',' @ ',' @ ',' @ ')' : (Nat Nat Tree Tree) Tree;
 'buildtree' '(' @ ',' @ ')'        : (Nat Nat) Tree;
 'calctree17' '(' @ ')'             : (Nat) Nat;
 'getmax' '(' @ ')'                 : (Tree) Nat;
 'getval'  '(' @ ')'                 : (Tree) Nat;
 'eval' '(' @ ')'      : (SNat) Nat;
 'eval17' '(' @ ')'    : (SNat) Nat;
 'evalsym17' '(' @ ')' : (SNat) Nat;
 'evalexp17' '(' @ ')' : (SNat) Nat; 
 'benchevalsym17' '(' @ ')'  : (SNat) Bool;
 'benchevalexp17' '(' @ ')'  : (SNat) Bool;
 'benchevaltree17' '(' @ ')' : (SNat) Bool; 
 'one'         : SNat;
 'two'         : SNat;
 'three'       : SNat;
 'four'        : SNat;
 'five'        : SNat;
 'six'         : SNat;
 'seven'       : SNat;
 'eight'       : SNat;
 'nine'        : SNat;
 'ten'         : SNat;
 'eleven'      : SNat;
 'twelve'      : SNat;
 'thirteen'    : SNat;
 'fourteen'    : SNat;
 'fifteen'     : SNat;
 'sixteen'     : SNat;
 'seventeen'   : SNat;
 'eighteen'    : SNat;
 'nineteen'    : SNat;
 'twenty'      : SNat;
 'twentyone'   : SNat;
 'twentytwo'   : SNat;
 'twentythree' : SNat;
 'twentyfour'  : SNat;
 'twentyfive'  : SNat;
 'twentysix'   : SNat;
 'twentyseven' : SNat;
 'twentyeight' : SNat;
 'twentynine'  : SNat;
 'thirty'      : SNat;
 'thirtyone'   : SNat;
 'thirtytwo'   : SNat;
 'thirtythree' : SNat;
 'thirtyfour'  : SNat;
 'thirtyfive'  : SNat; 
 '0'  : Nat;
 '1'  : Nat;
 '2'  : Nat;
 '3'  : Nat;
 '4'  : Nat;
 '5'  : Nat;
 '6'  : Nat;
 '7'  : Nat;
 '8'  : Nat;
 '9'  : Nat;
 '10' : Nat;
 '11' : Nat;
 '12' : Nat;
 '13' : Nat;
 '14' : Nat;
 '15' : Nat;
 '16' : Nat;
 '17' : Nat;
 'dec' '(' @ ')'    : (SNat) SNat;
 'expand' '(' @ ')' : (SNat) SNat;
 'exone'            : SNat;
 '<' @ ',' @ '>'                   : (Nat Nat) NatPair;
 'mod' '(' @ ',' @ ')'             : (Nat Nat) Nat;
 'mod' '(' @ ',' @ ',' @ ',' @ ')' : (Nat Nat Nat Nat) Nat;
 'nat2spoon' '(' @ ',' @ ',' @ ')' : (Nat Nat Nat) Nat;
 'nat2sym' '(' @ ')' : (Nat) SNat;
end
rules for Bool
 bool : Bool;
 X, x, y, x1, y1 : Nat;
 Xs, Ys, Zs : SNat;
 
 global
   [] or(true, bool)   => true end
   [] or(false, bool)  => bool end
   [] and(true, bool)  => bool end
   [] and(false, bool) => false end
   [] not(false) => true end
   [] not(true)  => false end
   [] equal(x,x) => true end 
   [] equal(x,y) => false end
   [] less(zero, y) => true end
   [] less(s(x), s(y)) => less(x,y) end 
   [] less(x, y) => false end 
   [] benchevalsym17(Xs) => equal(eval17(Zs),evalsym17(Zs))
      where Zs := ()exexp(two,Xs)
   end
   [] benchevalexp17(Xs) => equal(eval17(Zs),evalexp17(Zs))
      where Zs := ()exexp(two,Xs)
   end
   [] benchevaltree17(Xs) => equal(calctree17(X),getval(buildtree(X,zero)))
      where X := ()eval(Xs)
   end
 end
rules for Nat
 i, j, x, y, val, max : Nat;
 xs, ys : SNat;
 Xs, Ys, Zs : SNat;
 left, right : Tree;
 global
   [] plus(x,zero) => x end
   [] plus(x,s(y)) => s(plus(x,y)) end
   [] mult(x,zero) => zero end
   [] mult(x,s(y)) => plus(mult(x,y),x) end
   [] exp(x,zero) => s(zero) end
   [] exp(x,s(y)) => mult(x,exp(x,y)) end
   [] succ17(s(s(s(s(s(s(s(s(s(s(s(s(
                  s(s(s(s(zero))))))))))))))))) => zero end
   [] succ17(x) => s(x) end
   [] pred17(s(x)) => x end
   [] pred17(zero) => s(s(s(s(s(s(s(s(s(s(s(s(
                        s(s(s(s(zero)))))))))))))))) end
   [] plus17(x,zero) => x end
   [] plus17(x,s(y)) => succ17(plus17(x,y)) end
   [] mult17(x,zero) => zero end
   [] mult17(x,s(y)) => plus17(x,mult17(x,y)) end
   [] exp17(x,zero) => succ17(zero) end
   [] exp17(x,s(y)) => mult17(x,exp17(x,y)) end
   [] eval(exz) => zero end
   [] eval(exs(xs)) => s(eval(xs)) end
   [] eval(explus(xs,ys)) => plus(eval(xs), eval(ys)) end
   [] eval(exmult(xs,ys)) => mult(eval(xs), eval(ys)) end
   [] eval(exexp(xs,ys)) => exp(eval(xs), eval(ys)) end
   [] eval17(exz) => zero end
   [] eval17(exs(xs)) => succ17(eval17(xs)) end
   [] eval17(explus(xs,ys)) => plus17(eval17(xs), eval17(ys)) end
   [] eval17(exmult(xs,ys)) => mult17(eval17(xs), eval17(ys)) end
   [] eval17(exexp(xs,ys)) => exp17(eval17(xs), eval(ys)) end
   [] 0 => zero end
   [] 1 => s(0) end
   [] 2 => s(1) end
   [] 3 => s(2) end
   [] 4 => s(3) end
   [] 5 => s(4) end
   [] 6 => s(5) end
   [] 7 => s(6) end
   [] 8 => s(7) end
   [] 9 => s(8) end
   [] 10 => s(9) end
   [] 11 => s(10) end
   [] 12 => s(11) end
   [] 13 => s(12) end
   [] 14 => s(13) end
   [] 15 => s(14) end
   [] 16 => s(15) end
   [] 17 => s(16) end
   [] evalsym17(exz) => zero end
   [] evalsym17(exs(Xs)) => succ17(evalsym17(Xs)) end
   [] evalsym17(explus(Xs,Ys)) => plus17(evalsym17(Xs),evalsym17(Ys)) end
   [] evalsym17(exmult(Xs,exz)) => zero end
   [] evalsym17(exmult(Xs,exs(Ys))) =>
               evalsym17(explus(exmult(Xs,Ys),Xs)) end
   [] evalsym17(exmult(Xs,explus(Ys,Zs))) =>
               evalsym17(explus(exmult(Xs,Ys),exmult(Xs,Zs))) end
   [] evalsym17(exmult(Xs,exmult(Ys,Zs))) =>
               evalsym17(exmult(exmult(Xs,Ys),Zs)) end
   [] evalsym17(exmult(Xs,exexp(Ys,Zs))) =>
               evalsym17(exmult(Xs,dec(exexp(Ys,Zs)))) end
   [] evalsym17(exexp(Xs,exz)) => succ17(zero) end
   [] evalsym17(exexp(Xs,exs(Ys))) =>
               evalsym17(exmult(exexp(Xs,Ys),Xs)) end
   [] evalsym17(exexp(Xs,explus(Ys,Zs))) =>
               evalsym17(exmult(exexp(Xs,Ys),exexp(Xs,Zs))) end
   [] evalsym17(exexp(Xs,exmult(Ys,Zs))) =>
               evalsym17(exexp(exexp(Xs,Ys),Zs)) end
   [] evalsym17(exexp(Xs,exexp(Ys,Zs))) =>
               evalsym17(exexp(Xs,dec(exexp(Ys,Zs)))) end 
   [] evalexp17(Xs) => eval17(expand(Xs)) end
   [] eval17(exone) => s(zero) end
   [] getval(leaf(val)) => val end
   [] getval(node(val,max,left,right)) => val end
   [] getmax(leaf(val)) => val end
   [] getmax(node(val,max,left,right)) => max end
   [] calctree17(x) => mult17(i,j)
      where i := ()exp17(s(s(zero)),pred17(x))
      where j := ()pred17(exp17(s(s(zero)),x))
   end
 end
rules for SNat 
 x   : Nat;
 Xs, Ys, Zs : SNat;
 global
   [] one => exs(exz) end
   [] two => exs(one) end
   [] three => exs(two) end
   [] four => exs(three) end  
   [] five => exs(four) end  
   [] six => exs(five) end  
   [] seven => exs(six) end  
   [] eight => exs(seven) end  
   [] nine => exs(eight) end  
   [] ten => exs(nine) end  
   [] eleven => exs(ten) end  
   [] twelve => exs(eleven)  end  
   [] thirteen => exs(twelve) end  
   [] fourteen => exs(thirteen) end  
   [] fifteen => exs(fourteen) end  
   [] sixteen => exs(fifteen) end  
   [] seventeen => exs(sixteen) end  
   [] eighteen => exs(seventeen) end  
   [] nineteen => exs(eighteen) end  
   [] twenty => exs(nineteen) end  
   [] twentyone => exs(twenty) end  
   [] twentytwo => exs(twentyone) end  
   [] twentythree => exs(twentytwo) end  
   [] twentyfour => exs(twentythree) end  
   [] twentyfive => exs(twentyfour) end  
   [] twentysix => exs(twentyfive) end  
   [] twentyseven => exs(twentysix) end  
   [] twentyeight => exs(twentyseven) end  
   [] twentynine => exs(twentyeight) end          
   [] thirty => exs(twentynine) end  
   [] thirtyone => exs(thirty) end  
   [] thirtytwo => exs(thirtyone) end  
   [] thirtythree => exs(thirtytwo) end  
   [] thirtyfour => exs(thirtythree) end  
   [] thirtyfive => exs(thirtyfour) end 
   [] nat2sym(zero) => exz end
   [] nat2sym(s(x)) => exs(nat2sym(x)) end
   [] expand(exz) => exz end
   [] expand(exone) => exone end
   [] expand(exs(Xs)) => explus(exone,expand(Xs)) end
   [] expand(explus(Xs,Ys)) => explus(expand(Xs),expand(Ys)) end
   [] expand(exmult(Xs,exz)) => exz end
   [] expand(exmult(Xs,exone)) => expand(Xs) end
   [] expand(exmult(Xs,explus(Ys,Zs))) =>
               expand(explus(exmult(Xs,Ys),exmult(Xs,Zs))) end
   [] expand(exmult(Xs,Ys)) => expand(exmult(Xs,expand(Ys))) end
   [] expand(exexp(Xs,exz)) => exone end
   [] expand(exexp(Xs,exone)) => expand(Xs) end
   [] expand(exexp(Xs,explus(Ys,Zs))) =>
               expand(exmult(exexp(Xs,Ys),exexp(Xs,Zs))) end
   [] expand(exexp(Xs,Ys)) => expand(exexp(Xs, expand(Ys))) end
 end
rules for Tree
 x, y, val, val1, val2, max, max1 : Nat;
 left, right : Tree;
 global 
   [] buildtree(zero, val) => leaf(val) end
   [] buildtree(s(x), y) => node(val, max, left, right) 
      where left := ()buildtree(x, y)
      where max1 := ()getmax(left)
      where right := ()buildtree(x, succ17(max1))
      where val1 := ()getval(left)
      where val2 := ()getval(right)
      where val := ()plus17(val1,val2)
      where max := ()getmax(right)
   end
 end
end
LGI file
LPL benchmark description
  query of sort  Bool
  result of sort Bool
  import         benchmark
start with     ()benchevaltree17(twentyseven)
end

Maude sources

fmod BENCHMARK is
 sorts Boel Nat SNat Tree NatPair Boolean .
 op true : -> Boolean .
 op false : -> Boolean .
 op or  : Boolean Boolean -> Boolean .
 op and : Boolean Boolean -> Boolean .
 op neg : Boolean -> Boolean .
 op zero : -> Nat . 
 op s  : Nat -> Nat .
 op equal : Nat Nat -> Boolean .
 op less    : Nat Nat -> Boolean .

 op plus    : Nat Nat -> Nat .
 op mult    : Nat Nat -> Nat .
 op exp     : Nat Nat -> Nat .
 op succ17   : Nat -> Nat .
 op pred17   : Nat -> Nat .
 op plus17    : Nat Nat -> Nat .
 op mult17    : Nat Nat -> Nat .
 op exp17     : Nat Nat -> Nat .
 op exz : -> SNat .
 op exs : SNat -> SNat .
 op explus : SNat SNat -> SNat .
 op exmult : SNat SNat -> SNat .
 op exexp : SNat SNat -> SNat .
 op leaf   : Nat -> Tree .
 op node   : Nat Nat Tree Tree -> Tree .
 op buildtree   : Nat Nat -> Tree .
 op calctree17   : Nat -> Nat .
 op getmax   : Tree -> Nat .
 op getval    : Tree -> Nat .
 op eval   : SNat -> Nat .
 op eval17   : SNat -> Nat .
 op evalsym17   : SNat -> Nat .
 op evalexp17   : SNat -> Nat . 
 op benchevalsym17    : SNat -> Boolean .
 op benchevalexp17    : SNat -> Boolean .
 op benchevaltree17   : SNat -> Boolean . 
 op one         : -> SNat .
 op two         : -> SNat .
 op three       : -> SNat .
 op four        : -> SNat .
 op five        : -> SNat .
 op six         : -> SNat .
 op seven       : -> SNat .
 op eight       : -> SNat .
 op nine        : -> SNat .
 op ten         : -> SNat .
 op eleven      : -> SNat .
 op twelve      : -> SNat .
 op thirteen    : -> SNat .
 op fourteen    : -> SNat .
 op fifteen     : -> SNat .
 op sixteen     : -> SNat .
 op seventeen   : -> SNat .
 op eighteen    : -> SNat .
 op nineteen    : -> SNat .
 op twenty      : -> SNat .
 op twentyone   : -> SNat .
 op twentytwo   : -> SNat .
 op twentythree : -> SNat .
 op twentyfour  : -> SNat .
 op twentyfive  : -> SNat .
 op twentysix   : -> SNat .
 op twentyseven : -> SNat .
 op twentyeight : -> SNat .
 op twentynine  : -> SNat .
 op thirty      : -> SNat .
 op thirtyone   : -> SNat .
 op thirtytwo   : -> SNat .
 op thirtythree : -> SNat .
 op thirtyfour  : -> SNat .
 op thirtyfive  : -> SNat . 
 op 0  : -> Nat .
 op 1  : -> Nat .
 op 2  : -> Nat .
 op 3  : -> Nat .
 op 4  : -> Nat .
 op 5  : -> Nat .
 op 6  : -> Nat .
 op 7  : -> Nat .
 op 8  : -> Nat .
 op 9  : -> Nat .
 op 10 : -> Nat .
 op 11 : -> Nat .
 op 12 : -> Nat .
 op 13 : -> Nat .
 op 14 : -> Nat .
 op 15 : -> Nat .
 op 16 : -> Nat .
 op 17 : -> Nat .
 op dec      : SNat -> SNat .
 op expand   : SNat -> SNat .
 op exone    : -> SNat .
 op < _ , _ > : Nat Nat -> NatPair .
 op mod   : Nat Nat -> Nat .
 op mod   : Nat Nat Nat Nat -> Nat .
 op nat2spoon   : Nat Nat Nat -> Nat .
 op nat2sym   : Nat -> SNat .
*** some variables
var  Boolean : Boolean  .
vars X Y Val Max : Nat  .
vars Xs Ys Zs : SNat  .
vars Left Right : Tree  .
*** equations for boolean expressions
 
 eq or(true,Boolean) = true  .
 eq or(false,Boolean) = Boolean  .
 eq and(true, Boolean) = Boolean  .
 eq and(false, Boolean) = false  .
 eq neg(false) = true  .
 eq neg(true)  = false  .
*** toplevel benchmarks
eq benchevalsym17(Xs) = equal(eval17(exexp(two,Xs)),evalsym17(exexp(two,Xs))) .
eq benchevalexp17(Xs) = equal(eval17(exexp(two,Xs)),evalexp17(exexp(two,Xs))) .
eq benchevaltree17(Xs) = equal(calctree17(eval(Xs)),getval(buildtree(eval(Xs),zero))) .
*** equations for naturals modulo 17

   eq equal(X,X) = true  . 
   eq equal(X,Y) = false  .
   eq less(zero, Y) = true  .
   eq less(s(X), s(Y)) = less(X,Y)  .
   eq less(X, Y) = false  .
   eq plus(X,zero) = X  .
   eq plus(X,s(Y)) = s(plus(X,Y))  .
   eq mult(X,zero) = zero  .
   eq mult(X,s(Y)) = plus(mult(X,Y),X)  .
   eq exp(X,zero) = s(zero)  .
   eq exp(X,s(Y)) = mult(X,exp(X,Y))  .
   eq succ17(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(zero))))))))))))))))) = zero  .
   eq succ17(X) = s(X)  .
   eq pred17(s(X)) = X  .
   eq pred17(zero) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(zero))))))))))))))))  .
   eq plus17(X,zero) = X  .
   eq plus17(X,s(Y)) = succ17(plus17(X,Y))  .
   eq mult17(X,zero) = zero  .
   eq mult17(X,s(Y)) = plus17(X,mult17(X,Y))  .
   eq exp17(X,zero) = succ17(zero)  .
   eq exp17(X,s(Y)) = mult17(X,exp17(X,Y))  .
   eq eval(exz) = zero  .
   eq eval(exs(Xs)) = s(eval(Xs))  .
   eq eval(explus(Xs,Ys)) = plus(eval(Xs), eval(Ys))  .
   eq eval(exmult(Xs,Ys)) = mult(eval(Xs), eval(Ys))  .
   eq eval(exexp(Xs,Ys)) = exp(eval(Xs), eval(Ys))  .
   eq eval17(exz) = zero  .
   eq eval17(exs(Xs)) = succ17(eval17(Xs))  .
   eq eval17(explus(Xs,Ys)) = plus17(eval17(Xs), eval17(Ys))  .
   eq eval17(exmult(Xs,Ys)) = mult17(eval17(Xs), eval17(Ys))  .
   eq eval17(exexp(Xs,Ys)) = exp17(eval17(Xs), eval(Ys))  .
   eq 0 = zero  .
   eq 1 = s(0)  .
   eq 2 = s(1)  .
   eq 3 = s(2)  .
   eq 4 = s(3)  .
   eq 5 = s(4)  .
   eq 6 = s(5)  .
   eq 7 = s(6)  .
   eq 8 = s(7)  .
   eq 9 = s(8)  .
   eq 10 = s(9)  .
   eq 11 = s(10)  .
   eq 12 = s(11)  .
   eq 13 = s(12)  .
   eq 14 = s(13)  .
   eq 15 = s(14)  .
   eq 16 = s(15)  .
   eq 17 = s(16)  .
   eq evalsym17(exz) = zero  .
   eq evalsym17(exs(Xs)) = succ17(evalsym17(Xs))  .
   eq evalsym17(explus(Xs,Ys)) = plus17(evalsym17(Xs),evalsym17(Ys)) .
   eq evalsym17(exmult(Xs,exz)) = zero  .
   eq evalsym17(exmult(Xs,exs(Ys))) = evalsym17(explus(exmult(Xs,Ys),Xs))  .
   eq evalsym17(exmult(Xs,explus(Ys,Zs))) = evalsym17(explus(exmult(Xs,Ys),exmult(Xs,Zs)))  .
   eq evalsym17(exmult(Xs,exmult(Ys,Zs))) =  evalsym17(exmult(exmult(Xs,Ys),Zs))  .
   eq evalsym17(exmult(Xs,exexp(Ys,Zs))) =  evalsym17(exmult(Xs,dec(exexp(Ys,Zs))))  .
   eq evalsym17(exexp(Xs,exz)) = succ17(zero)  .
   eq evalsym17(exexp(Xs,exs(Ys))) =  evalsym17(exmult(exexp(Xs,Ys),Xs))  .
   eq evalsym17(exexp(Xs,explus(Ys,Zs))) =  evalsym17(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))  .
   eq evalsym17(exexp(Xs,exmult(Ys,Zs))) =  evalsym17(exexp(exexp(Xs,Ys),Zs))  .
   eq evalsym17(exexp(Xs,exexp(Ys,Zs))) =  evalsym17(exexp(Xs,dec(exexp(Ys,Zs))))  . 
   eq evalexp17(Xs) = eval17(expand(Xs))  .
   eq eval17(exone) = s(zero)  .
   eq getval(leaf(Val)) = Val  .
   eq getval(node(Val,Max,Left,Right)) = Val  .
   eq getmax(leaf(Val)) = Val  .
   eq getmax(node(Val,Max,Left,Right)) = Max  .
   eq calctree17(X) = mult17(exp17(s(s(zero)),pred17(X)), pred17(exp17(s(s(zero)),X))).
*** equations for SNat
   eq one = exs(exz)  .
   eq two = exs(one)  .
   eq three = exs(two)  .
   eq four = exs(three)  .  
   eq five = exs(four)  .  
   eq six = exs(five)  .  
   eq seven = exs(six)  .  
   eq eight = exs(seven)  .  
   eq nine = exs(eight)  .  
   eq ten = exs(nine)  .  
   eq eleven = exs(ten)  .  
   eq twelve = exs(eleven)   .  
   eq thirteen = exs(twelve)  .  
   eq fourteen = exs(thirteen)  .  
   eq fifteen = exs(fourteen)  .  
   eq sixteen = exs(fifteen)  .  
   eq seventeen = exs(sixteen)  .  
   eq eighteen = exs(seventeen)  .  
   eq nineteen = exs(eighteen)  .  
   eq twenty = exs(nineteen)  .  
   eq twentyone = exs(twenty)  .  
   eq twentytwo = exs(twentyone)  .  
   eq twentythree = exs(twentytwo)  .  
   eq twentyfour = exs(twentythree)  .  
   eq twentyfive = exs(twentyfour)  .  
   eq twentysix = exs(twentyfive)  .  
   eq twentyseven = exs(twentysix)  .  
   eq twentyeight = exs(twentyseven)  .  
   eq twentynine = exs(twentyeight)  .          
   eq thirty = exs(twentynine)  .  
   eq thirtyone = exs(thirty)  .  
   eq thirtytwo = exs(thirtyone)  .  
   eq thirtythree = exs(thirtytwo)  .  
   eq thirtyfour = exs(thirtythree)  .  
   eq thirtyfive = exs(thirtyfour)  . 
   eq nat2sym(zero) = exz  .
   eq nat2sym(s(X)) = exs(nat2sym(X))  .
   eq expand(exz) = exz  .
   eq expand(exone) = exone  .
   eq expand(exs(Xs)) = explus(exone,expand(Xs))  .
   eq expand(explus(Xs,Ys)) = explus(expand(Xs),expand(Ys))  .
   eq expand(exmult(Xs,exz)) = exz  .
   eq expand(exmult(Xs,exone)) = expand(Xs)  .
   eq expand(exmult(Xs,explus(Ys,Zs))) =
               expand(explus(exmult(Xs,Ys),exmult(Xs,Zs)))  .
   eq expand(exmult(Xs,Ys)) = expand(exmult(Xs,expand(Ys)))  .
   eq expand(exexp(Xs,exz)) = exone  .
   eq expand(exexp(Xs,exone)) = expand(Xs)  .
   eq expand(exexp(Xs,explus(Ys,Zs))) =
               expand(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))  .
   eq expand(exexp(Xs,Ys)) = expand(exexp(Xs, expand(Ys)))  .
*** equations for trees
   eq buildtree(zero, Val) = leaf(Val)  .
   eq buildtree(s(X),Y) = node(plus17(getval(buildtree(X,Y)),
                   getval(buildtree(X,succ17(getmax(buildtree(X,Y)))))),
                   getmax(buildtree(X,succ17(getmax(buildtree(X,Y))))),
                   buildtree(X,Y),
                   buildtree(X,succ17(getmax(buildtree(X,Y))))) .
endfm
Personal tools
Namespaces

Variants
Actions
Navigation