DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Useless-Code Elimination for (a small subset of) Caml

Examples

Unless explicitly stated the simplifications would be performed also without using e-type 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 e-type entailment)

  • Example E1
    fun f -> 
    fun u -> 
    
    (fun g -> (f g + g (u*u*u*u*u)))
         (fun z -> 3)
    ;;
    
  • Example E2
    fun f -> 
    fun u -> 
    fun v ->
    
    (fun g -> fun x -> (f g + g x + (fun y -> 1) u))
         (fun z -> 3)
         v 
    ;;
    

Examples involving conditional expressions

  • Example C1 (compare with Examples S2 and S3 above)
    fun b -> if b 
             then (fun x -> (fst (3,x))) 4
             else (fun f -> f 5) (fun x -> 6)
    ;;
    

Examples involving let-in expressions (with "MONOmorphic use" of the let-bound 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 let-bound 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 (z-1)
    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 (z-1)
    in
    f (fun v -> 7) 1 2 3
    ;;
    
  • Example R4

    This example is due to C. Paulin-Mohring. It is based on an instance of useless code that can arise in programs extracted from proofs (see [ Paulin-Mohring, 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 (n-1)))
                              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 (x-1) (x-1)
                         else x
    in
    f 5 5
    ;;
    
  • Example R6

    The following program cannot be simplified without using e-type entailment.

    let rec f = fun u -> fun x -> 
                if (x>0) then f (x-1) (x-1)
                         else x
    in
    f 
    ;;
    

Examples involving let-in expressions (with "POLYmorphic use" of the let-bound 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 useless-code that is NOT detected by this prototype

The useless-code elimination for let-polymorphically typed terms implemented by this prototype, carried on as part of the Master Thesis [ Esposito, 1999 ], is a strightforward-to-implement extension of the useless-code 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 let-polymorphically 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 let-bound 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 let-bound identifier (that is performed by using its principal type), and
  • the set of constraints produced by the analysis of the the body of the let-in (where the use of the let-bound 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 Lambda-Calculus [Boerio, 1994] or the type-based UCE for let-polymorphically 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 Lambda-Calculus. In Proceedings of ESOP'94, LNCS 788, pp. 30-45. Springer, 1994.
  • [Kobayashi, 2000] N. Kobayashi. Type-Based Useless-Variable Elimination. In: Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation 2000 (PEPM'00), pp. 84-93.
  • [Paulin-Mohring, 1989a] C. Paulin-Mohring. Extraction de Programme dans le Calcul des Constructions. PhD Thesis, Uviversité Paris VII.
  • [Paulin-Mohring, 1989b] C. Paulin-Mohring. 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. Control-Flow Analysis of Higher-Order Languages. Ph.D. Thesis, Carnegie-Mellon University.
  • [Wand and Siveroni, 1999] M. Wand and I. Siveroni. Constraint Systems for Useless-Variable Elimination. In: Proceedings of ACM SIGPLAN/SIGTACT Symposium on Principles of Programming Languages 1999 (POPL'99), pp. 291-302.


[Back]

Comments to: damiani[at]di[dot]unito[dot]it