Experiments by María Alpuente, Santiago Escobar and Salvador Lucas.
We give some benchmark programs to demonstrate the practicality of our on-demand prototype interpreter OnDemandOBJ and our program transformation tool for removing negative annotations TransformNeg.
Program pi
This program codifies the well-known infinite series expansion to approximate the pi number: pi/4=1 - 1/3 + 1/5 - 1/7 + .... To make the program terminating and complete, the strategy for symbol cons must include annotation -2. The rest of strategy annotations are positive since termination of the whole program is ensured. Note that the auxiliary functions plus, times and square for natural numbers are also included.
|
|
obj PI is sorts Nat LNat Recip LRecip . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op posrecip : Nat -> Recip [strat (1)] . op negrecip : Nat -> Recip [strat (1)] . op nil : -> LNat . op cons : Nat LNat -> LNat [strat (1 -2)] . op rnil : -> LRecip . op rcons : Recip LRecip -> LRecip [strat (1 2)] . op from : Nat -> LNat [strat (1 0)] . op 2ndspos : Nat LNat -> LRecip [strat (1 2 0)] . op 2ndsneg : Nat LNat -> LRecip [strat (1 2 0)] . op pi : Nat -> LRecip [strat (1 0)] . op plus : Nat Nat -> Nat [strat (1 2 0)] . op times : Nat Nat -> Nat [strat (1 2 0)] . op square : Nat -> Nat [strat (1 0)] . vars N X Y : Nat . var Z : LNat . eq from(X) = cons(X,from(s(X))) . eq 2ndspos(0,Z) = rnil . eq 2ndspos(s(N),cons(X,cons(Y,Z))) = rcons(posrecip(Y),2ndsneg(N,Z)) . eq 2ndsneg(0,Z) = rnil . eq 2ndsneg(s(N),cons(X,cons(Y,Z))) = rcons(negrecip(Y),2ndspos(N,Z)) . eq pi(X) = 2ndspos(X,from(0)) . eq plus(0,Y) = Y . eq plus(s(X),Y) = s(plus(X,Y)) . eq times(0,Y) = 0 . eq times(s(X),Y) = plus(Y,times(X,Y)) . eq square(X) = times(X,X) . endo |
Transformed program pi_noneg
The application of the program transformation for removing negative annotations TransformNeg to the program pi produces the following program (this is obtained automatically by the implementation of the program transformation). Note that annotation (0) for symbol cons is necessary due to problems in Maude for representing and interpreting an empty strategy.
|
|
obj PI4 is sorts Nat LNat Recip LRecip . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op posrecip : Nat -> Recip [strat (1)] . op negrecip : Nat -> Recip [strat (1)] . op nil : -> LNat . op cons : Nat LNat -> LNat [strat (0)] . op rnil : -> LRecip . op rcons : Recip LRecip -> LRecip [strat (1 2)] . op from : Nat -> LNat [strat (1 0)] . op 2ndspos : Nat LNat -> LRecip [strat (1 2 0)] . op 2ndsneg : Nat LNat -> LRecip [strat (1 2 0)] . op pi : Nat -> LRecip [strat (1 0)] . op plus : Nat Nat -> Nat [strat (1 2 0)] . op times : Nat Nat -> Nat [strat (1 2 0)] . op square : Nat -> Nat [strat (1 0)] . op cons-root : Nat LNat -> LNat [strat (1 0)] . op cons-pos : Nat LNat -> LNat [strat (1)] . op cons-pos-+2 : Nat LNat -> LNat [strat (1 2)] . vars N X Y : Nat . var Z : LNat . eq from(X) = cons-root(X,from(s(X))) . eq 2ndspos(0,Z) = rnil . eq 2ndspos(s(N),cons(X,Z)) = 2ndspos(s(N),cons-pos(X,Z)) . eq 2ndspos(s(N),cons-pos(X,Z)) = 2ndspos(s(N),cons-pos-+2(X,Z)) . eq 2ndspos(s(N),cons-pos-+2(X,cons(Y,Z))) = rcons(posrecip(Y),2ndsneg(N,Z)) . eq 2ndsneg(0,Z) = rnil . eq 2ndsneg(s(N),cons(X,Z)) = 2ndsneg(s(N),cons-pos(X,Z)) . eq 2ndsneg(s(N),cons-pos(X,Z)) = 2ndsneg(s(N),cons-pos-+2(X,Z)) . eq 2ndsneg(s(N),cons-pos-+2(X,cons(Y,Z))) = rcons(negrecip(Y),2ndspos(N,Z)) . eq pi(X) = 2ndspos(X,from(0)) . eq plus(0,Y) = Y . eq plus(s(X),Y) = s(plus(X,Y)) . eq times(0,Y) = 0 . eq times(s(X),Y) = plus(Y,times(X,Y)) . eq square(X) = times(X,X) . eq cons-root(X,Z) = cons(X,Z) . endo |
Program msquare_eager
This program uses functions minus, square, times, and plus over natural numbers; they are common to several examples included here. The key point of this program is that it is terminating using only positive annotations and including the indices of all symbols.
|
|
obj MINUS-SQUARE is sort Nat . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op plus : Nat Nat -> Nat [strat (1 2 0)] . op times : Nat Nat -> Nat [strat (1 2 0)] . op square : Nat -> Nat [strat (1 0)] . op minus : Nat Nat -> Nat [strat (1 2 0)] . vars M N : Nat . eq plus(0,N) = N . eq plus(s(M),N) = s(plus(M,N)) . eq times(0,N) = 0 . eq times(s(M),N) = plus(N,times(M,N)) . eq square(N) = times(N,N) . eq minus(0,N) = 0 . eq minus(s(M),0) = s(M) . eq minus(s(M),s(N)) = minus(M,N) . endo |
Program msquare_apt
This program is identical to msquare_eager but only the annotations which are necessary to make the program complete are included, i.e. we use only canonical positive strategies.
|
|
obj MINUS-SQUARE is sort Nat . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op plus : Nat Nat -> Nat [strat (1 0)] . op times : Nat Nat -> Nat [strat (1 0)] . op square : Nat -> Nat [strat (0)] . op minus : Nat Nat -> Nat [strat (1 2 0)] . vars M N : Nat . eq plus(0,N) = N . eq plus(s(M),N) = s(plus(M,N)) . eq times(0,N) = 0 . eq times(s(M),N) = plus(N,times(M,N)) . eq square(N) = times(N,N) . eq minus(0,N) = 0 . eq minus(s(M),0) = s(M) . eq minus(s(M),s(N)) = minus(M,N) . endo |
Program msquare_neg
This program is identical to msquare_apt but negative annotations are included, i.e. we consider canonical arbitrary strategies.
|
|
obj MINUS-SQUARE is sort Nat . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op plus : Nat Nat -> Nat [strat (1 0)] . op times : Nat Nat -> Nat [strat (1 0)] . op square : Nat -> Nat [strat (0)] . op minus : Nat Nat -> Nat [strat (1 -2 0)] . vars M N : Nat . eq plus(0,N) = N . eq plus(s(M),N) = s(plus(M,N)) . eq times(0,N) = 0 . eq times(s(M),N) = plus(N,times(M,N)) . eq square(N) = times(N,N) . eq minus(0,N) = 0 . eq minus(s(M),0) = s(M) . eq minus(s(M),s(N)) = minus(M,N) . endo |
Transformed program msquare_neg_noneg
The application of the program transformation for removing negative annotations TransformNeg to the program msquare_neg produces the following program. Note that annotation 0 in strategy for symbol s is necessary due to problems in Maude for representing and interpreting an empty strategy.
|
|
obj MINUS-SQUARE is sort Nat . op 0 : -> Nat . op s : Nat -> Nat [strat (0)] . op s-root : Nat -> Nat [strat (1 0)] . op s-pos : Nat -> Nat [strat (1)] . op plus : Nat Nat -> Nat [strat (1 0)] . op times : Nat Nat -> Nat [strat (1 0)] . op square : Nat -> Nat [strat (0)] . op minus : Nat Nat -> Nat [strat (1 0)] . op minus-+2 : Nat Nat -> Nat [strat (1 2 0)] . vars M N : Nat . eq plus(0,N) = N . eq plus(s(M),N) = plus(s-pos(M),N) . eq plus(s-pos(M),N) = s-root(plus(M,N)) . eq times(0,N) = 0 . eq times(s(M),N) = times(s-pos(M),N) . eq times(s-pos(M),N) = plus(N,times(M,N)) . eq square(N) = times(N,N) . eq minus(0,N) = 0 . eq minus(s(M),N) = minus(s-pos(M),N) . eq minus(s-pos(M),N) = minus-+2(s-pos(M),N) . eq minus-+2(s-pos(M),0) = s-root(M) . eq minus-+2(s-pos(M),s(N)) = minus(M,N) . eq s-root(N) = s(N) . endo |
Program quicksort
This program is borrowed from Example 3.11 of [AG01]. Note that auxiliary functions from and take for constructing lists are included, as well as two predicates nfLNat and nfNat to normalize terms, and the connective and. The term used for evaluation is: nfLNat(quicksort(take(10,from(0)))).
|
|
obj Quicksort is sorts Nat LNat Bool2 . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op nil : -> LNat . op cons : Nat LNat -> LNat [strat (1)] . op true2 : -> Bool2 . op false2 : -> Bool2 . op le : Nat Nat -> Bool2 [strat (1 -2 0)] . op app : LNat LNat -> LNat [strat (1 0)] . op low : Nat LNat -> LNat [strat (2 0)] . op high : Nat LNat -> LNat [strat (2 0)] . op ifLNat : Bool2 LNat LNat -> LNat [strat (1 0)] . op quicksort : LNat -> LNat [strat (1 0)] . op and : Bool2 Bool2 -> Bool2 [strat (1 0)] . op nfLNat : LNat -> Bool2 [strat (1 0)] . op nfNat : Nat -> Bool2 [strat (1 0)] . op from : Nat -> LNat [strat (0)] . op take : Nat LNat -> LNat [strat (1 -2 0)] . vars X Y : Nat . vars Z W : LNat . vars A B : Bool2 . eq le(0,Y) = true2 . eq le(s(X),0) = false2 . eq le(s(X),s(Y)) = le(X,Y) . eq app(nil,Z) = Z . eq app(cons(X,Z),W) = cons(X,app(Z,W)) . eq low(X,nil) = nil . eq low(X,cons(Y,Z)) = ifLNat(le(Y,X),cons(Y,low(X,Z)),low(X,Z)) . eq high(X,nil) = nil . eq high(X,cons(Y,Z)) = ifLNat(le(Y,X),high(X,Z),cons(Y,high(X,Z))) . eq ifLNat(true2,Z,W) = Z . eq ifLNat(false2,Z,W) = W . eq quicksort(nil) = nil . eq quicksort(cons(X,Z)) = app(quicksort(low(X,Z)),cons(X,quicksort(high(X,Z)))) . eq from(X) = cons(X,from(s(X))) . eq take(0,Z) = nil . eq take(s(X),cons(Y,Z)) = cons(Y,take(X,Z)) . eq nfLNat(nil) = true2 . eq nfLNat(cons(X,Z)) = and(nfNat(X),nfLNat(Z)) . eq nfNat(0) = true2 . eq nfNat(s(X)) = nfNat(X) . eq and(true2,A) = A . eq and(false2,A) = false2 . endo |
Program minsort
This program is borrowed from Example 3.10 of [AG01]. The call considered for evaluation is: nfLNat(minsort(take(10,from(0)),nil)).
|
|
obj Minsort is sorts Nat LNat Bool2 . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op nil : -> LNat . op cons : Nat LNat -> LNat [strat (1 -2)] . op true2 : -> Bool2 . op false2 : -> Bool2 . op le : Nat Nat -> Bool2 [strat (1 2 0)] . op app : LNat LNat -> LNat [strat (1 0)] . op rm : Nat LNat -> LNat [strat (2 0)] . op min : LNat -> Nat [strat (1 0)] . op eqNat : Nat Nat -> Bool2 [strat (1 2 0)] . op ifNat : Bool2 Nat Nat -> Nat [strat (1 0)] . op ifLNat : Bool2 LNat LNat -> LNat [strat (1 0)] . op and : Bool2 Bool2 -> Bool2 [strat (1 0)] . op minsort : LNat LNat -> LNat [strat (1 2 0)] . op nfLNat : LNat -> Bool2 [strat (1 0)] . op nfNat : Nat -> Bool2 [strat (1 0)] . op take : Nat LNat -> LNat [strat (1 2 0)] . op from : Nat -> LNat [strat (0)] . vars X Y : Nat . vars Z W : LNat . vars A B : Bool2 . eq le(0,Y) = true2 . eq le(s(X),0) = false2 . eq le(s(X),s(Y)) = le(X,Y) . eq app(nil,Z) = Z . eq app(cons(X,Z),W) = cons(X,app(Z,W)) . eq rm(X,nil) = nil . eq rm(X,cons(Y,Z)) = ifLNat(eqNat(X,Y),rm(X,Z),cons(Y,rm(X,Z))) . eq min(cons(X,nil)) = X . eq min(cons(X,cons(Y,Z))) = ifNat(le(Y,X),min(cons(Y,Z)),min(cons(X,Z))) . eq eqNat(0,0) = true2 . eq eqNat(s(X),0) = false2 . eq eqNat(0,s(X)) = false2 . eq eqNat(s(X),s(Y)) = eqNat(X,Y) . eq ifLNat(true2,Z,W) = Z . eq ifLNat(false2,Z,W) = W . eq ifNat(true2,X,Y) = X . eq ifNat(false2,X,Y) = Y . eq minsort(nil,nil) = nil . eq minsort(cons(X,Z),W) = ifLNat(eqNat(X,min(cons(X,Z))),cons(X,minsort(app(rm(X,Z),W),nil)),minsort(Z,cons(X,W))) . eq from(X) = cons(X,from(s(X))) . eq take(0,W) = nil . eq take(s(X),cons(Y,Z)) = cons(Y,take(X,Z)) . eq nfLNat(nil) = true2 . eq nfLNat(cons(X,Z)) = and(nfNat(X),nfLNat(Z)) . eq nfNat(0) = true2 . eq nfNat(s(X)) = nfNat(X) . eq and(true2,A) = A . eq and(false2,A) = false2 . endo |
Program mod
This program is borrowed from Example 3.5 of [AG01]. Auxiliary functions for natural numbers are included, namely fact, times, and plus. The call considered for evaluation is: mod(fact(fact(3)),2).
|
|
obj MOD is sorts Nat Bool2 . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op true2 : -> Bool2 . op false2 : -> Bool2 . op minus : Nat Nat -> Nat [strat (1 -2 0)] . op mod : Nat Nat -> Nat [strat (1 -2 0)] . op le : Nat Nat -> Bool2 [strat (1 -2 0)] . op ifNat : Bool2 Nat Nat -> Nat [strat (1 0)] . op plus : Nat Nat -> Nat [strat (1 0)] . op times : Nat Nat -> Nat [strat (1 0)] . op fact : Nat -> Nat [strat (1 0)] . vars M N : Nat . eq le(0,M) = true2 . eq le(s(N),0) = false2 . eq le(s(N),s(M)) = le(N,M) . eq minus(0,N) = 0 . eq minus(s(M),0) = s(M) . eq minus(s(M),s(N)) = minus(M,N) . eq mod(0,M) = 0 . eq mod(s(N),0) = 0 . eq mod(s(N),s(M)) = ifNat(le(M,N),mod(minus(N,M),s(M)),s(N)) . eq ifNat(true2,N,M) = N . eq ifNat(false2,N,M) = M . eq plus(0,N) = N . eq plus(s(M),N) = s(plus(M,N)) . eq times(0,N) = 0 . eq times(s(M),N) = plus(N,times(M,N)) . eq fact(0) = s(0) . eq fact(s(N)) = times(s(N),fact(N)) . endo |
Program mod'
This program is similar to program mod but positive annotations are provided for symbols times and plus in order to avoid differences due to sharing of variables. The call considered for evaluation is: mod(fact(fact(3)),2).
|
|
obj MOD is sorts Nat Bool2 . op 0 : -> Nat [strat ()] . op s : Nat -> Nat [strat (1)] . op true2 : -> Bool2 . op false2 : -> Bool2 . op minus : Nat Nat -> Nat [strat (1 -2 0)] . op mod : Nat Nat -> Nat [strat (1 -2 0)] . op le : Nat Nat -> Bool2 [strat (1 -2 0)] . op ifNat : Bool2 Nat Nat -> Nat [strat (1 0)] . op plus : Nat Nat -> Nat [strat (1 2 0)] . op times : Nat Nat -> Nat [strat (1 2 0)] . op fact : Nat -> Nat [strat (1 0)] . vars M N : Nat . eq le(0,M) = true2 . eq le(s(N),0) = false2 . eq le(s(N),s(M)) = le(N,M) . eq minus(0,N) = 0 . eq minus(s(M),0) = s(M) . eq minus(s(M),s(N)) = minus(M,N) . eq mod(0,M) = 0 . eq mod(s(N),0) = 0 . eq mod(s(N),s(M)) = ifNat(le(M,N),mod(minus(N,M),s(M)),s(N)) . eq ifNat(true2,N,M) = N . eq ifNat(false2,N,M) = M . eq plus(0,N) = N . eq plus(s(M),N) = s(plus(M,N)) . eq times(0,N) = 0 . eq times(s(M),N) = plus(N,times(M,N)) . eq fact(0) = s(0) . eq fact(s(N)) = times(s(N),fact(N)) . endo |
Program average
This program is borrowed from Example 3.15 of [AG01]. Auxiliary functions for natural numbers are included, namely fact, times, and plus. The call considered for evaluation is: average(square(square(4)),square(square(4))).
|
|
obj AVERAGE is sort Nat . op 0 : -> Nat . op s : Nat -> Nat [strat (1)] . op average : Nat Nat -> Nat [strat (-1 -2 0)] . op plus : Nat Nat -> Nat [strat (1 0)] . op times : Nat Nat -> Nat [strat (1 0)] . op fact : Nat -> Nat [strat (1 0)] . op square : Nat -> Nat [strat (1 0)] . vars M N : Nat . eq average(0,0) = 0 . eq average(0,s(0)) = 0 . eq average(0,s(s(0))) = s(0) . eq average(s(M),N) = average(M,s(N)) . eq average(M,s(s(s(N)))) = s(average(s(M),N)) . eq plus(0,N) = N . eq plus(s(M),N) = s(plus(M,N)) . eq times(0,N) = 0 . eq times(s(M),N) = plus(N,times(M,N)) . eq square(N) = times(N,N) . eq fact(0) = s(0) . eq fact(s(N)) = times(s(N),fact(N)) . endo |
Experiments
The following three tables
show the runtimes
and the number of rewrite steps
of the benchmarks for the different OBJ-family systems.
Each runtime is the average of 10 executions measured in a Pentium III machine running
redhat 7.2.
The
OnDemandOBJ
interpreter is our on-demand prototype interpreter.
CafeOBJ
is developed in Lisp at the Japan Advanced Inst. of Science and Technology (JAIST).
OBJ3,
also written in Lisp,
is maintained by the University of California at San Diego.
Maude
is developed in C++ and maintained by the Computer Science Lab at SRI
International.
OBJ3
and
Maude
provide only computations with
positive annotations whereas
CafeOBJ
and
OnDemandOBJ
provide computations with
negative annotations as well.
Note that
CafeOBJ
and
OBJ3
implement sharing of variables
whereas
Maude
and
OnDemandOBJ do not.
The following table compares the evaluation of expression
pi(square(square(3))) using pi and pi_noneg. It
witnesses that negative annotations are extremely useful
in practice and that the program transformation enables the execution of
negatively annotated programs in all OBJ implementations.
This table also
evidences that the implementation of the on-demand evaluation strategy of [AEGL02]
in other systems is really interesting.
On the other hand, the following table illustrates the interest of
using negative annotations to improve the behavior of programs.
There, for instance, program msquare_neg runs in less time and
requires a smaller number of rewrite steps than
msquare_eager or msquare_apt, which do not
include negative annotations.
Moreover, note that the program transformation is also
very useful since execution of the expression
minus(0,square(square(5))) is improved.
Finally, the following table compares the execution
of typical functional programs with canonical
arbitrary strategies in
OnDemandOBJ
and in
CafeOBJ,
and demonstrates that there are
clear advantages in using our implementation
of the
on-demand evaluation of [AEGL02].
[AEGL02]
M. Alpuente, S. Escobar, B. Gramlich, and S. Lucas.
Improving on-demand strategy annotations.
In Matthias Baaz and Andrei Voronkov, editors, Proc. 9th Int.
Conf. on Logic for Programming, Artificial Intelligence, and Reasoning
(LPAR'02), Lecture Notes in Computer Science, Tbilisi, Georgia, October
2002. Springer-Verlag.
[AG01] T. Arts and J. Giesl.
A
collection of examples for termination of term rewriting using dependency
pairs. Technical Report AIB-2001-09 RWTH Aachen, 2001.
Please, send comments or suggestions
to
sescobar@dsic.upv.es. Any
kind of contribution is welcome.
Last update Feb 2002 # sescobar@dsic.upv.es