Experiments by María Alpuente, Santiago Escobar and Salvador Lucas.

We first give some examples with redundant arguments, borrowed from the literature and/or obtained by applying common transformation processes. Redundant arguments in these program examples are highlighted in red. Then we show the result of applying our Automatic Useless Argument Elimination System to these benchmarks. Finally, we present the improvement achieved by our system w.r.t. original examples by showing a table with runtimes of the original and optimized programs.

Examples with redundant arguments

data nat = Z | S nat

loop :: nat -> nat -> nat -> nat
loop a bogus Z     = loop (S a) (S bogus) (S Z)
loop a bogus (S x) = a

data nat = Z | S nat

f :: nat -> nat -> nat
f Z     y = Z
f (S x) y = f (f x y) y

data nat = Z | S nat

f :: nat -> nat
f Z         = S Z
f (S Z)     = S Z
f (S (S x)) = f (f (S x))

data Nat = 0 | S Nat

append::[Nat] -> [Nat] -> [Nat]
append nil    y = y
append (x:xs) y = x:(append xs y)

last::[Nat] -> Nat
last (x:nil)  = x
last (x:y:ys) = last (y:ys)

last (append xs (x:nil))

applast::[Nat] -> Nat -> Nat
applast nil    z = z
applast (x:xs) z = lastnew x xs z 

lastnew::Nat -> [Nat] -> Nat -> Nat
lastnew x nil    z = z
lastnew x (y:ys) z = lastnew y ys z

data nat = Z | S nat 

plus :: nat -> nat -> nat
plus Z     x = x
plus (S x) y = S (plus x y)

minus :: nat -> nat -> nat
minus x     Z     = x
minus (S x) (S y) = minus(X,Y)

minus (plus x y) x

minus_pe :: nat -> nat -> nat
minus_pe Z     y = y
minus_pe (S x) y = minus_pe x y

data nat = Z | S nat 

plus :: nat -> nat -> nat
plus Z     x = x
plus (S x) y = S (plus x y)

leq :: nat -> nat -> Bool
leq Z     x     = True
leq (S x) Z     = False
leq (S x) (S y) = leq x y

leq x (plus x y)

leq_pe :: nat -> nat -> Bool
leq_pe Z     x = True
leq_pe (S x) y = leq_pe x y

data nat = Z | S nat 

double :: nat -> nat
double Z     = Z
double (S x) = S (S (double x))

even :: nat -> Bool
even Z         = True
even (S Z)     = False
even (S (S x)) = even x

even (double x)

even_pe :: nat -> Bool
even_pe Z = True
even_pe (S x) = even_pe x

data nat = Z | S nat 

min :: nat -> nat -> nat
min Z     x     = Z
min (S x) Z     = Z
min (S x) (S y) = S (min x y)

minimal :: [nat] -> nat
minimal (x:nil)  = x
minimal (x:y:xs) = min x (minimal (y:xs))

append :: [Nat] -> [Nat] -> [Nat]
append nil    y = y
append (x:xs) y = x:(append xs y)

minimal (append (Z:nil) xs)

minimal_pe :: nat -> nat
minimal_pe nil = Z
minimal_pe (x:y) = Z

data nat = Z | S nat 

plus :: nat -> nat -> nat
plus Z     x = x
plus (S x) y = S (plus x y)

sum :: [nat] -> nat
sum nil    = Z
sum (x:xs) = plus x (sum xs)

allzeros :: [nat] -> [nat]
allzeros nil    = nil
allzeros (x:xs) = Z:(allzeros xs)

sum (allzeros x)

sum_pe :: [nat] -> nat
sum_pe nil    = Z
sum_pe (x:xs) = sum_pe xs

Experiments

Results of (automatically) performing the analysis and elimination of redundant arguments:
 

Name	Original Program	Redundant arguments found	Erased Program
bogus	loop :: nat -> nat -> nat -> nat loop a bogus Z     = loop (S a) (S bogus) (S Z) loop a bogus (S x) = a	loop: 2	loop' :: nat -> nat -> nat loop' a Z     = loop' (S a) (S Z) loop' a (S x) = a
applast	applast::[Nat] -> Nat -> Nat applast nil    z = z applast (x:xs) z = lastnew x xs z  lastnew::Nat -> [Nat] -> Nat -> Nat lastnew x nil    z = z lastnew x (y:ys) z = lastnew y ys z	applast: 1 lastnew: 1,2	applast' :: nat -> nat applast' z = z lastnew' :: Nat -> Nat lastnew' z = z
plus_minus	minus_pe :: nat -> nat -> nat minus_pe Z     y = y minus_pe (S x) y = minus_pe x y	minus_pe: 1	minus_pe' :: nat -> nat minus_pe' y = y
plus_leq	leq_pe :: nat -> nat -> Bool leq_pe Z     x = True leq_pe (S x) y = leq_pe x y	leq_pe: 1,2	leq_pe' :: Bool leq_pe' = True
double_even	even_pe :: nat -> Bool even_pe Z = True even_pe (S x) = even_pe x	even_pe: 1	even_pe' :: Bool even_pe' = True
minimal_append	minimal_pe :: [nat] -> nat minimal_pe nil = Z minimal_pe (x:y) = Z	minimal_pe: 1	minimal_pe' :: nat minimal_pe' = Z
sum_allzeros	sum_pe :: [nat] -> nat sum_pe nil    = Z sum_pe (x:xs) = sum_pe xs	sum_pe: 1	sum_pe' :: nat sum_pe' = Z
Mutual recursion 1	f :: nat -> nat -> nat f Z     y = Z f (S x) y = f (f x y) y	f: 1,2	f' :: nat f' = Z
Mutual recursion 2	f :: nat -> nat f Z         = S Z f (S Z)     = S Z f (S (S x)) = f (f (S x))	f: 1	f' :: nat f' = S Z

First, we execute the original and transformed programs in Curry.In the case of program bogus, no appreciable optimization is achieved by removing redundant arguments, since Curry is a lazy language and the redundant argument in bogus is a useless variable.

Runtimes have been measured in a Pentium III class machine running linux and using version 1.3.2 of the PAKCS Compiler under Sicstus Prolog 3.8.4.

Natural numbers are given by numbers 0, 1, 2, etc instead of the notation Z/S x. For bechmarking purposes, goals make use of the factorial function, defined in a usual way.
The number of elements of a list is indicated by a subindex. In the case of binary trees, the subindex indicates the depth of the tree.
 
 

Name	Call in original program	Time (ms)	Call in erased program	Time (ms)	Improvement
bogus	loop (fact 8) (fact 8) (fact 8)	260	loop' (fact 8) (fact 8)	260	0%
applast	applast [(fact 8)]1000 (fact 8)	340	applast' (fact 8)	260	20%
plus_minus	minus_pe (fact 8) (fact 8)	480	minus_pe' (fact 8)	270	40%
plus_leq	leq_pe (fact 8) (fact 8)	210	leq_pe'	0	100%
double_even	even_pe (fact 8)	210	even_pe'	0	100%
minimal_append	minimal_pe [(fact 8)]10000	5	minimal_pe'	0	100%
sum_allzeros	sum_pe [(fact 8)]10000	70	sum_pe'	0	100%
Mutual recursion 1	f (fact 8) (fact 8)	320	f'	0	100%
Mutual recursion 2	f (fact 8)	380	f'	0	100%

Finally, we run the programs in CiME 2, a system which uses an innermost rewriting strategy. Note that, in this case, significant optimizations are also measured for programs bogus, applast and plus_minus.
 

Name	Call in original program	Time (ms)	Call in erased program	Time (ms)	Improvement
bogus	loop (fact 6) (fact 6) (fact 6)	2820	loop' (fact 6) (fact 6)	1880	33%
applast	applast [(fact 6)]10 (fact 6)	2570	applast' (fact 6)	940	64%
plus_minus	minus_pe (fact 6) (fact 6)	7930	minus_pe' (fact 6)	960	87%
plus_leq	leq_pe (fact 6) (fact 6)	7970	leq_pe'	0	100%
double_even	even_pe (fact 6)	1930	even_pe'	0	100%
minimal_append	minimal_pe [(fact 6)]10	1070	minimal_pe'	0	100%
sum_allzeros	sum_pe [0]1000	1330	sum_pe'	0	100%
Mutual recursion 1	f (fact 6) (fact 6)	9580	f'	0	100%
Mutual recursion 2	f (fact 6)	2020	f'	0	100%

References

[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.

[Kob00] N. Kobayashi. Type-based useless variable elimination. In Proc. of PEPM-00, pages 84-93, ACM Press, 2000.

[WS99] M. Wand and I. Siveroni. Constraint systems for useless variable elimination. In Proc. of POPL'99, pages 291--302, ACM Press, 1999.
 

Please, send comments or suggestions to sescobar@dsic.upv.es. Any kind of contribution is welcome.