UselessCode Elimination for (a small subset of) Caml
Examples
Unless explicitly stated
the simplifications would be performed also without using etype entailment.
Examples about simply typed programs

Example S1
(fun x > 1) 2
;;

Example S2
(fun x > (fst (3,x))) 4
;;

Example S3
(fun f > f 5) (fun x > 6)
;;

Example S4
fun a >
fun b >
(fun swap > (fst (swap (a,b))))
(fun p > ((snd p), (fst p)))
;;
Examples about simply typed programs
(where
the simplifications would NOT be performed by the
system without etype entailment)
Examples involving conditional expressions
Examples involving letin expressions
(with "MONOmorphic use" of the letbound identifier)

Example L1 (compare with Example S1 above)
let x = 2
in
1
;;

Example L2 (compare with Example S2 above)
let x = 4
in
(fst (3,x))
;;

Example L3 (compare with Example S3 above)
let f = fun x > 6
in
f 5
;;

Example L3' (compare with Example S3 above)
let p = (fun f > f 5) in
let q = (fun x > 6) in
p q
;;

Example L4 (compare with Example S4 above)
fun a >
fun b >
let swap = fun p > ((snd p), (fst p))
in
(fst (swap (a,b)))
;;

Example L5 (compare with Example E1 above)
fun f >
fun u >
let g = fun z > 3 in
f g + g (u*u*u*u*u)
;;

Example L5' (compare with Example E1 above)
fun f >
fun u >
let p = fun g > (f g + g (u*u*u*u*u)) in
let q = (fun z > 3) in
p q
;;

Example L6
fun x >
let y = (fst x)
in
x
;;
Examples involving recursive definitions
(with "MONOmorphic use" of the letbound identifier)

Example R1
This example is taken from
[Wand and Siveroni, 1999]
and originally comes from
[Shivers, 1991].
fun f >
fun x >
let rec loop = fun a > fun bogus > fun j >
if (j>100) then a else loop (f(a,j)) (bogus+2) (j+1)
in
loop x 3 1
;;

Example R2
let rec f = fun g > fun x > fun z >
if (z=0) then g x
else f g x (z1)
in
f (fun v > 7) 1 2
;;

Example R3
let rec f = fun g > fun x > fun y > fun z >
if (z=0) then g x
else f g y x (z1)
in
f (fun v > 7) 1 2 3
;;

Example R4
This example is due to C. PaulinMohring.
It is based on an instance of useless code that can arise in
programs extracted from proofs (see
[
PaulinMohring, 1989a
]
for an introduction to the subject).
A detailed presentation of the example can be found in Section 2.2 of
[
Berardi et al, 2000
].
fun e1 >
fun e2 >
fun h1 >
fun h2 >
( fun recursor > fun g > fun x > ( fst (recursor (e1,e2) g x) )
)
( fun a > fun f > let rec r = fun n > if (n=0)
then a
else (f n (r (n1)))
in r
)
( fun m > fun p > ((h1 (fst p)), (h2 (fst p ) (snd p)))
)
;;

Example R5
let rec f = fun u > fun x >
if (x>0) then f (x1) (x1)
else x
in
f 5 5
;;

Example R6
The following program cannot be simplified without using etype entailment.
let rec f = fun u > fun x >
if (x>0) then f (x1) (x1)
else x
in
f
;;
Examples involving letin expressions
(with "POLYmorphic use" of the letbound identifier)

Example P1
let k = (fun x > fun y > x)
in
((k 3 (fun u > u))=2) && ((k (fun v >true) 7) false)
;;

Example P2
fun x >
fun a >
fun b >
let c = fun y > x
in
c ((a+1),(not b))
;;

Example P3
fun z >
fun a >
let id = fun x > x
in
id (fun y > z) (a+1)
;;

Example P4
fun z >
fun a >
fun b >
let id = fun x > x
in
id (fun y > z) ((a+1), (not b))
;;
Examples of uselesscode that is NOT detected by this prototype
The uselesscode elimination
for
letpolymorphically typed terms
implemented by this prototype,
carried on as part of the Master Thesis
[
Esposito, 1999
],
is a strightforwardtoimplement extension of
the uselesscode elimination
for
simply typed terms
described in
[
Damiani and Giannini, 2000
].
It is quite efficient (e.g., no constraint copying). However,
it is not completely satisfactory.
In fact,
as illustrated by the following examples,
it is not
able to perform a certain class of simplifications
on letpolymorphically typed terms.
A more effective extension of the technique that overcomes this
limitation is currently under investigation.

Example N1
Both the expressions
(fun x > x) (fun z > 3) 5
;;
and
(fst ((fun x > x) (1,2)))
;;
can be simplified.
However,
if we rewrite them by introducing a polymorphic use of a letbound
identifier, we have
the expression
let id = (fun x > x) in
id (fun z > 3) 5
;;
can be still simplified, while
the following expession cannot.
let id = (fun x > x) in
(fst (id (1,2)))
;;
Roughly speaking,
this "odd" behaviour is due to the "naive"
technique used for connecting

the set of constraints produced by
the analysis of the definition of the letbound
identifier (that is performed by using its principal type),
and

the set of constraints produced by the analysis of the
the body of the letin
(where the use of the letbound identifier has a type that is
a specialization of the type used to analized its
definition).
Instead, the above expression can be simplified by using the
type based UCE for the
Polymorphic Second Order LambdaCalculus
[Boerio, 1994]
or the
typebased UCE for letpolymorphically typed terms described in
[Kobayashi, 2000].
Another example of expression that is not simplified by the
prototype is the following
(Example 3.4 of [Kobayashi, 2000]).

Example N2
The
expression
let f = fun u > (fst u) (snd u)
in
f ( (fun v > (fst v)), (1,2) )
+
f ( (fun v > (fst v) + (snd v)), (2,3) )
;;
might be simplified to
let f = fun u > (fst u) (snd u)
in
f ( (fun v > v), 1 )
+
f ( (fun v > (fst v) + (snd v)), (2,3) )
;;
However,
no simplification is performed by this prototype.
BIBLIOGRAPHY

[Boerio, 1994]
L. Boerio.
Extending Pruning Thechniques to Polymorphic Second Order LambdaCalculus.
In Proceedings of ESOP'94, LNCS 788, pp. 3045. Springer, 1994.

[Kobayashi, 2000]
N. Kobayashi.
TypeBased UselessVariable Elimination.
In:
Proceedings of ACM SIGPLAN Workshop on Partial Evaluation
and SemanticsBased Program Manipulation 2000 (PEPM'00),
pp. 8493.

[PaulinMohring, 1989a]
C. PaulinMohring.
Extraction de Programme dans le Calcul des Constructions.
PhD Thesis, Uviversité Paris VII.

[PaulinMohring, 1989b]
C. PaulinMohring.
Extracting F_omega's Programs from Proofs in the Calculus of Construnctions.
In:
Proceedings of ACM SIGPLAN/SIGTACT Symposium on
Principles of Programming Languages 1989 (POPL'89).

[Shivers, 1991]
O. Shivers.
ControlFlow Analysis of HigherOrder Languages.
Ph.D. Thesis, CarnegieMellon University.

[Wand and Siveroni, 1999]
M. Wand and I. Siveroni.
Constraint Systems for UselessVariable Elimination.
In:
Proceedings of ACM SIGPLAN/SIGTACT Symposium on
Principles of Programming Languages 1999 (POPL'99),
pp. 291302.
