Strategies for the Representation and Reduction of Lambda Terms and their Impact

Chuck Liang, Gopalan Nadathur and Xiaochu Qi

Area of Concern: Efficient Implementation Techniques for Supporting Higher-Order Abstract Syntax.

Goal: Reduce redundant term traversals and term creations during substitution and normalization.

Available Tools:

• Debruijn Representation of terms (factored out for now)

• Graph-based representation allows sharing

• An explicit-substitution system. Simplified representation of a suspension structure:

[[t; Env]]

where t is a term and Env an environment with possibly multiple substitutions:

Env = (s_{1}/x_{1}, s_{2}/x_{2}, …, s_{n}/x_{n})

Merging Multiple Substitutions

New form of beta-contraction merges substitutions:

(λx.[[T; E]])S → [[T; (S/x) :: E]]

• Potential benefits have been well argued

• What is the best way to take advantage of this ability?

Eager versus Laziness in Substitution and Reduction

Full or head normalization?

Should suspended substitutions persist in term structures?

Possible to use new β rule implicitly (eager substitution)

Lazy substitution allows combining of substitutions across computational steps:

eval (let A λx. let B λy. C) :

The two β-redexes are not contracted at once, but substitution work can still be combined with an explicit embedding of suspension terms:

let [[B; (A′/x)]] [[λy. C; (A′/x)]] → → [[C; (B′/y, A′/x)]]

Potential Disadvantage: Backtracking may require substitution work to be redone.

Principal strategies to consider:

1. Lazy Reduction, Eager Substitution: head normalization with no outstanding substitutions

2. Eager Reduction and Substitution: full normalization

3. Lazy Reduction and Substitution: head normalization with suspended substitutions in terms

4. Some compromise approach?

Platform for experimentation: Teyjus Lambda Prolog

Examples Suite of Programs

• Reduction Only

SKI Object-level head-normalization of random combinations of S, K and I. Meta-level representation restricted to second order, using abs : (i → i) → i and app : i → i → i.

Church Calculations using large Church numerals and arithmetic combinators. Combinators are represented as third-order terms at the meta-level.

• L-lambda Unification (higher-order pattern unification)

Typeinf An expensive algorithm for inferring principal type schemes. Compiler An experimental compiler using higher-order abstract syn-

tax and continuation-passing style.

• Higher-order Unification

Hilbert Solving diophantine equations with higher-order unification.

Generates flexible-flexible constraints. Funtrans A collection of transformations for functional programs.

1. Head Normalization with Eager Substitution Disadvantages:

• substitutions cannot be combined across computational steps.

• Embedded Redexes:

λx_{1} … λx_{n}. (h t_{1} … t_{n})

The terms t_{1} … t_{n} may also contain redexes.

• Origins of embedded redexes:

1. Third (and higher) order reductions: (λx.λy.h (x y)) λz.t → λy.h (λz.t)y

2. exacerbated by η-expansion λu ((λx λy λz (y (x z))) u) λu ((λx λy λz (y (x z))) λw (u λv (w v))). λu (λy λz (y (λw (u λv (w v))) z)).

3. Most Common Cause of embedded redices:

higher-order unification procedure.

flexible-rigid pair:

⟨λx_{1} … λx_{l} (F t_{1} … t_{n}), λx_{1} … λx_{l} (c s_{1} … s_{m})⟩

{⟨F, λw_{1} … λw_{n} (h (H_{1} w_{1} … w_{n}) … (H_{o} w_{1} … w_{n}))⟩}

H_{1} … H_{n} will also be bound to abstractions

Possible to eliminate redexes caused by flex-rigid pairs by annotating the dependency of terms as open/closed 2. Full Normalization

• Eagerness in both reduction and substitution.

• Terms are always reduced to λ-normal form.

• No redices left embedded.

• Much redundancy in structural traversal.

• Loss of ability to combine substitutions across computational steps.

3. Head Normalization with Lazy Substitution

• Embedded redices do not cause extra structural taversal

λ … λ. h … [[(λx.t) s; env]] … → →

[[t; (s/x) :: env]]

• Backtracking may cause redundant substitutions:

Common cause: Occurs-Check Failure: does x appear free in A?

• Application may call for substitution reduction anyway (printing terms for user-interaction)

Formulation of New Head-Normalization Strategy: Contract all redexes encountered while applying substitutions eagerly

• Does not re-visit terms already in normal form.

• Does not leave embedded redexes in head normal forms

• Cannot combine substitutions across computational steps.

• Avoids redundancy created by backtracking.

Peformance of lazy and enhanced eager-head normalization are comparable.

Typical, simplified L-lambda Program:

copy (app A B) (app C D) :- copy A C, copy B D.

copy (abs A) (abs B) :- ∀v(copy v v ⊃ copy (A v) (B v)).

Terms to be considered consists of n abstractions and m applications:

abs λx_{1}…. abs λx_{n}. app A_{1} (app … (app A_{m}B))

Types of goals:

• copy A A where A is a ground term (reduction only).

• copy A U where A is ground but U is a logic variable: unification procedure generates embedded redexes when instantiating U.

• copy A U, copy U V where only A is ground: embedded redexes in U are involved in further reductions Effect of backtracking

copy (let E (λx T)) T’ :- copy T T’.

copy (let E T) (let E’ T’) :- copy E E’, ∀v (copy v v ⊃ copy (T v) (T’ v)). Goal: copy A U where A contains no vacuous abstractions will cause backtracking and the undoing of substitutions. Advantage of lazy substitution nullified in this case The De Bruijn Representation of Bound variables Advantage: Simplifies α-equivalence. Potential Disadvantage: Need to renumber indices after contraction:

λx ((λy λz y x) (λw x))

λ ((λ λ #2 #3) (λ #2))
λ λ ((λ #3) #2)
λ λ #2

Observation: combined substitutions also combines renumbering steps:

(λ λ A) B C

[[A, 2, 0, (C, 0) :: (B, 0)]]

The free indices of B,C never needed to be renumbered.

Potential Loss of Sharing

(λ #1 (λ #2)) T → T (λ T)

The two instances of T cannot be shared after renumbering. How significant is this effect? Alternative: Contract T in [[T, 0, NL, nil]] before renumbering T preserves the sharing of reduction. This can be measured Data indicates no significant difference in practice Summary

• The ability to combine substitutions during reduction is an important enhancement.

• Full reduction to λ-normal form is costly due to redundant term traversals.

• The phenomenon of embedded redices in head normal forms occurs commonly, and has a significant effect on performance

• Head normalization with lazy substitution using suspension terms avoids redundancy caused by embedded redices

• The ability to suspend substitutions across computational steps is somewhat offset by the possibility of redundancy upon backtracking

• A new strategy can be formulated that specifically targets these tradeoffs: eliminate embedded redices eagerly during substitution.

• The de Bruijn representation of λ-terms is preferable to a name-based scheme.