\begin{matrix}c \\ ◯ \end{matrix} Andreas Abel and Nicolai Kraus This work is licensed under the Creative Commons Attribution License.

A Lambda Term Representation Inspired by Linear Ordered Logic

Andreas Abel

Theoretical Computer Science Institut für Informatik Ludwig-Maximilians-Universität München, Germany

                   andreas.abel@ifi.lmu.de

Nicolai Kraus

Functional Programming Laboratory School of Computer Science University of Nottingham Nottingham, United Kingdom

                                                        ngk@cs.nott.ac.uk

We introduce a new nameless representation of lambda terms inspired by ordered logic. At a lambda abstraction, number and relative position of all occurrences of the bound variable are stored, and application carries the additional information where to cut the variable context into function and argument part. This way, complete information about free variable occurrence is available at each subterm without requiring a traversal, and environments can be kept exact such that they only assign values to variables that actually occur in the associated term. Our approach avoids space leaks in interpreters that build function closures.

In this article, we prove correctness of the new representation and present an experimental evaluation of its performance in a proof checker for the Edinburgh Logical Framework.

Keywords: representation of binders, explicit substitutions, ordered contexts, space leaks, Logical Framework.

1 Introduction

Type checking dependent types in languages like Agda [21] and Coq [14] or logical frameworks like Twelf [22] requires a large amount of evaluation, since types may depend on values. Such type checkers incorporate an interpreter for purely functional programs with free variables—at least, the λ-calculus— which is used to compute weak head normal forms of types. Efficiency of type checking is mostly identical with efficiency of evaluation^{1} (and, in case of type reconstruction, efficiency of unification), and remains a challenge as of today. In seminal work, Gregoire and Leroy [13] have sped up Coq type checking by compiling to byte-code instead of using an interpreter. Boespflug [6] has obtained further speed-ups by producing native code using stock-compilers.

While compilation approaches are successful on batch type checking fully explicit programs, they have not been attempted on type reconstruction using higher-order unification or on interactive program construction such as in Agda and Epigram [18]. These languages are involved and constantly evolving, and their implementations are prototypes and frequently modified and extended. Implementing a full compiler just to get type reconstruction going is deterring; furthermore, compilation has not (yet) proven its feasibility in minor evaluation tasks (like weak head evaluation) that dominate higher-order unification. At least for language prototyping, smart interpreters are, and may remain, competitive with compilation.

For instance, Twelf’s interpreter is sufficiently fast; it is inspired by a term representation with de Bruijn indices [7] and explicit substitutions [1]. In the context of functional programming, explicit substitutions are known as closures, consisting of the code of a function plus an environment, assigning values to the free variables appearing in the code. In typical implementations of interpreters [9], these environments are not precise; they assign values to all variables that are statically in scope rather than only to those that are actually referred to in the code. This bears potential for space-leaks: the environment of a closure might refer to a large value that is never used, but cannot be garbage collected. An obvious remedy to this threat is, when forming a closure, to restrict the environment to the actual free variables; however, this requires a traversal of the code. We explore a different direction: we are looking for a code representation that maintains information about the free variables at each node of the abstract syntax tree.

Submitted to:

LFMTP’11

1Evaluation is necessary to reduce types to weak head normal form and compare types for equality. Subtracting these operations, type checking has linear complexity.

A principal candidate is linear typing in Curry-Howard correspondence with Girard’s linear logic [12]; there, each variable in scope is actually referenced (more precisely, referenced exactly once). In other words, the free variables are exactly the variables in the typing context. Dropping types, we may talk of linear scoping. Yet we do not want to represent linear terms, but arbitrary λ-terms. Kesner and Lengrand [15] achieve this by introducing explicit term constructs for weakening and contraction. We pursue a different path: we incorporate information about variable use and multiplicity directly into abstraction and application.

In the context of linear λ-calculus, the free variables of a function application are the disjoint union of the free variables of the function and the free variables of the argument. If we want to maintain the set of free variables during a term traversal, at an application node we need to decide which variables go into the function part and which into the argument part. Thus, we would store at each application a set of variables that go into the, say, function part, all others would go to the argument part. Less information is needed if we switch to an ordered representation.

Ordered logic, also called non-commutative linear logic [23], refines linear logic by removing the structural rule exchange which restricts hypotheses to be used in the order they have been declared. Transferring this principle to ordered scoping this means that the scoping context lists the free variables in the order they occur in the term, from left to right. This allows pushing the context into an application with very little information: we just need to know how many variables appear in the function part so we can cut the context in two at the right position, splitting it into function context and argument context. This constitutes the central idea of our representation: at each application node of the syntax tree, we store a number denoting the number of free variable occurrences in the function part. During evaluation of an application in an environment, we can cut the environment into two, the environment needed for the evaluation of the function and the environment needed for the evaluation of the argument. Thus, our environments are precise and space leaks are avoided. In particular, a variable is always evaluated in a singleton environment assigning only a value to this variable. Following this observation, variables do not need a name, they are identified by their position; and environments are simply sequences of values.

Since we are not interested in proof terms of ordered logic per se, but only borrow the ordered context idea for our representation of untyped λ-calculus, we need to allow multiple occurrences of the same variable. In fact, the context shall list the variable occurrences in order. At a lambda abstraction, we bind all occurrences of the same variable. Thus, at an abstraction node we specify at which positions the bound variable should be inserted in the scoping context. This concludes the presentation of our idea.

In the rest of the paper, after an introductory example (Section 2) we formally define our term representation in Section 3. Interpreter and handling of environments are described in Section 4, followed by the translation between ordinary lambda terms and ordered terms (Section 5). Soundness of the interpreter is formally proven in Section 6, before we conclude with an experimental evaluation in Section 7.

This article summarizes the B.Sc. thesis of the second author [16].

2 An Example

To demonstrate the discussed risk of space-leaks during evaluation, we apply the term λx.λy.aby in basic syntax consecutively to the free variables g and f. A possible (and, if the mentioned closures are used, typical) sequence of reduction steps is given below. By writing t [s_{1}/x_{1},...,s_{n}/x_{n}], we want to express that in the term t, each occurrence of the variable x_{1} (x_{2},...,x_{n}) has to be replaced by the term s_{1} (resp. s_{2},...,s_{n}) simultaneously. Such a substitution list always applies only to the directly preceding term:

(λx.λy.aby)gf
−→  (λy.aby)[g/x] f
−→  (aby)[g/x,f/y]
−→ (ab)[g/x,f/y] y[g/x,f/y]
−→ a[g/x,f/y] b[g/x,f/y] f
−→  abf

Here, the substitution [g/x]could be dropped instantly and there is no need to apply the other substitution [f/y] to the term ab. However, the term representation used above comes along with the problem that such an evaluation algorithm does not have the required information in time. This is due to the fact that the binding information is always split between the λ and the actual variable occurrence, as they both carry the variable name. In contrast, using de Bruijn indices would make it possible to remove the piece of information from the λ. Our goal is to do it the other way round: We want the whole information to be available at the λ, thus making it possible to know the number and places of the bound variable occurrences without looking at the whole term.

3 Syntax

In this article, we only cover the core constructs of the lambda calculus as they are enough to make the approach clear. However, we do not see any limitations for common extensions. We first define ordered preterms :

ordered preterms ∋ t,u ::= x  free variable (named x)
| •  bound variable (nameless)
| t^{m}u application
| λk⃗.t abstraction

Free variables are denoted by their name like in the standard syntax. Bound variables, however, are just denoted by a dot •, which does not carry any information beside the fact that it is a bound variable. In the case of an application, there is a first term (the function part) and a second term (the argument) as usual. Furthermore, the application carries an integer m as an additional piece of information that will be important for the evaluation process and is explained in a moment. The most interesting part is the abstraction λk⃗.t. The vector k⃗= [k_{1},k_{2},...,k_{n}] is nothing else but a list of non-negative integers of length n. It determines which dots • are bound by the λ in the following way: Consider all • in the term t which are not bound in t itself. Now, the first k_{1} of these are not bound by the λ, the next one is, the following k_{2} are again not bound and so on (see examples below).

We denote the number of unbound • in an ordered preterm t by fV(t). Consequently, fV(·) is simply defined by:

fV(x) = 0, fV(•) = 1, fV(t^{m}u) = fV(t) + fV(u), fV(λ^{[k_{1},...,k_{n}]}.t) = fV(t) − n.

We call an ordered preterm u an ordered term iff each sub-preterm w of u fulfils the following condition: If w is an application t^{m}u, the equation m = fV(t) holds and if it is an abstraction λ^{[k_{1},...,k_{n}]}.t, then n+∑_{i}k_{i} ≤ fV(t) is satisfied. The latter condition states that if a λ in u binds a variable, this variable must actually exist while the first one just gives a meaning to the integer carried by an application. Clearly, any sub-preterm of an ordered term is again an ordered term. u is called closed if fV(t) = 0.

Here are some examples of closed terms. The S combinator

λx.λy.λz.xz (yz)

would be written as

λ^{[0]}.λ^{[1]}.λ^{[1,1]}.•^{1}•^{2} (•^{1}•)

Moreover, the term

(λx.λy.aby)gf

from Section 2 would be represented as

( λ^{[]}.λ^{[0]}.a^{0}b^{0}•) ^{0}f^{0}g

(note that applications are still left-associative). We can see that the first λ does not bind anything as it is annotated with the empty vector [], while this is less obvious when it is written as λx.

At this point, we hope to have clarified the intended meaning of our syntax. A formal definition will be given in Section 5.

4 Values and Evaluation

Before specifying values and evaluation formally, we want to give an example to demonstrate how the information carried by a lambda should be used and why we always have exactly the needed information. Suppose we have the term

( λ^{[0]}.λ^{[1]}.λ^{[1,1]}.•^{1}•^{2}(•^{1}•)) gf n

that is, the S combinator applied to three free variables (we suppress the application indices 0 for better readability). We want to get rid of the beta redexes, so we start by eliminating the first one. The outermost λ is decorated with the vector [0] of length one. Now, the single variable bound by this λ should be replaced by g, so we start a substitution list and insert a single g:

( λ^{[1]}.λ^{[1,1]}.•^{1}•^{2}(•^{1}•)) [g] f n

The first remaining λ is λ^{[1]}, so it does not bind the first variable (thus g remains first in the substitution list), but the second one. Consequently, we add an f after the g:

( λ^{[1,1]}.•^{1}•^{2}(•^{1}•)) [g,f] n

Now the situation becomes more interesting. The only remaining λ is now decorated with the vector [1,1], so one n has to be inserted after the first entry (g) and another one must be placed after the subsequent entry (f):

(•^{1}•^{2}(•^{1}•))[g,n,f,n]

All λ have now been eliminated. The applications’ indices tell us how the substitution list should be divided between the terms:

(•^{1}•)[g,n] (•^{1}•)[f,n]

We do the same step once more:

•[g] •[n] (•[f] •[n])

The only thing left to be done is to apply the substitutions in the obvious way:

gn(f n)

Here, evaluation naturally leads to a term in beta normal form. This is not always the case: as an example, if we had tried to evaluate the above term without the n (i.e. S^{0}f^{0}g), we would have got stuck at (λ^{[1,1]}.•^{1}•^{2}(•^{1}•)) [g,f]. However, this would have been satisfactory as it would have shown that the term’s normal form is an abstraction. In other words, our evaluation results in weak head normal forms.

Consequently, we define values in the following way:

values ∋ v,w ::= xv⃗  large application
| (λk⃗.t)v⃗ closure

The large application^{2} consists of a variable x which is applied to a vector [v_{1},v_{2},...,v_{m}] of values. It is to be read as a left-associative application, i.e. as ((xv_{1})v_{2}...)v_{m}. Note that it is not necessarily “large”. Quite the contrary, it often only consists of the head (and the vector of values is empty).

A closure (λk⃗.t)v⃗ is the result of the evaluation process if the corresponding beta normal form of the term does not start with a free variable. The main part, λk⃗.t, is nothing other than a lambda abstraction in the syntax of ordered terms. In addition, we need the substitution list v⃗(which is simply a list of values) that satisfies length(v⃗) = fV(λk⃗.t). The idea is that the i^{th} unbound • is to be replaced by v_{i}. These substitution lists have already been used in the example above.

At this point, we want to introduce a notation for inserting a single item multiple times into a list. More precisely, if v⃗ = [v_{1},v_{2},...,v_{m}] is a list, k⃗ = [k_{1},k_{2},...,k_{n}] is a vector (i.e. also a list) of non-negative integers satisfying ∑ _{i=1}^{n} k_{i} ≤ m and w is a single item, we write v^{w/k⃗} for the list that is constructed by inserting w at each of the positions k_{1},k_{1} + k_{2},...,∑ _{i=1}^{n} k_{i} into v⃗, i.e. for the list [v_{1},v_{2},...,v_{k_{1}},w,v_{k_{1}+1},...,v_{k_{1}+k_{2}},w,v_{k_{1}+k_{2}+1} ,...,v_{m}] (of course, it is possible that v^{w/k⃗} starts or ends with w).

We are now able to define the evaluation function ⟦·⟧_{·} which takes an ordered term t as well as an ordered substitution list v⃗ and returns a value. The tuple must always satisfy the condition fV(t) = length(v⃗). In other words, the list carries neither too little nor redundant information. At the start of the evaluation, the ordered substitution list is empty. Additionally, we specify the application ·@· of two values, which also returns a value and does not need anything else. Our evaluation procedure uses a call-by-value strategy:

2 The argument vector v⃗ of a large application is sometimes called a spine [8]. Large applications xv⃗ also appear in the formulation of Böhm trees [4].

\begin{aligned}⟦x⟧_{[]} & = & x & (1) \\ ⟦•⟧_{[v_{1}]} & = & v_{1} & (2) \\ ⟦t^{k}u⟧_{[v_{1},...,v_{n}]} & = & ⟦t⟧_{[v_{1},...,v_{k}]}@⟦u⟧_{[v_{k+1} ,...,v_{n}]} & (3) \\ ⟦λk⃗.t⟧v⃗ & = & (λk⃗.t)v⃗ & (4) \\ (xv⃗)@w & = & x[v⃗,w] & (5) \\ (λk⃗.t)v⃗@w & = & ⟦t⟧_{}_{v^{w/k⃗}} & (6) \end{aligned}

First, if we want to evaluate a free variable (1), the substitution list must be empty because of the invariant mentioned above. Second, in the case of a • (2), the ordered list must have exactly one entry. This entry is the result of the evaluation. If we evaluate an application (3), we evaluate the left and the right term. The application’s index enables us to split the substitution list at the right position. Then, we have to apply the first result to the second. Evaluating an abstraction (4) is easy. We just need to keep the substitutions to build a closure.

If we want to apply a large application to a value w (5) , we just append w to the vector of values (we write [v⃗,w] for [v_{1},...,v_{n},w]). The case of a closure (λk⃗.t)v⃗ (6) is less simple, but it is still quite clear what to do: k⃗ determines at which positions w should be inserted in the ordered substitution list, so we just construct the list v^{w/k⃗}. Then, t is evaluated.

Concerning substitution lists, we talk about “lists of values” for simplicity. More specifically, we want them to be lists of pointers to avoid the duplication of “real” values during constructing lists like v^{w/k⃗}. Instead of simple linked lists, we have also implemented these lists as dynamic functional arrays represented as binary trees. This reduces the asymptotic costs of list splitting—[v_{1},...,v_{n}] to ([v_{1},...,v_{k}],[v_{k+1},...,v_{n}])— and multi-insertion v^{w/k⃗} from linear to logarithmic time (in terms of the length of the list v⃗). For an experimental comparison of the two implementations see Section 7.

5 Parsing and Printing

In this section, we define how terms in normal syntax are translated into our ordered syntax (Parsing) and vice versa (Printing). To specify this, we need some notation. First of all, we write X for the set of variable names we want to use and T for the set of lambda terms in basic standard syntax (i.e. X ⊂ T, furthermore, x ∈ X together with t,u ∈ T implies t u ∈ T and λx.t ∈ T). Additionally, oT is the set of terms in our ordered syntax defined above, \overline{oT} the subset of closed ordered terms (fV(t) = 0) and V the set of values (defined in the previous section). Moreover, we write X⃗for the set of lists of variable names and V⃗ for the set of lists of values. For each set Γ of variable names (Γ ⊆ X), we denote the set of lists of elements of Γ by Γ⃗ and the ordered terms that do not contain any variable of Γ (as a free variable) by oT_{Γ}.

By writing oT ⊗ X⃗ (resp. oT ⊗ V⃗, oT_{Γ} ⊗ Γ⃗, ...), we mean the subset {(t,x⃗) | fV(t) = length(x⃗)} of oT × X⃗ (and analogous for the other cases).

For a finite set Γ of variable names, we define the correspondence relation · ◁ Γ ▷ ·[·]⊂ T × oT × X⃗ (pronounce: “corresponds in context Γ to”). The intuition is that M ◁ Γ ▷ u[x⃗]means: M is a term that corresponds to the ordered term u, where unbound •are replaced by the (not necessarily pairwise distinct) variables in the list x⃗. The set Γ can be seen as a filter that tells us which free variables do not occur in u but in x⃗instead.

\begin{matrix}x ∈ Γ \\ x ◁ Γ ▷ •[x] \end{matrix} (A)  M ◁ Γ ▷ t[x⃗] N ◁ Γ ▷ u[y⃗] length(x⃗) = m M N ◁ Γ ▷ (t^{m}u)[x⃗,y⃗] (B)

\begin{matrix}x ∉ Γ \\ x ◁ Γ ▷ x[] \end{matrix} (C)  \begin{matrix}M ◁ (Γ ∪ \{z\}) ▷ t[x^{z/k⃗}] z ∉ x⃗ \\ λz.M ◁ Γ ▷ (λk⃗.t)[x⃗] \end{matrix} (D)

It is important to note that M ◁ Γ ▷ u[x⃗]implies that each variable occurring in x⃗ is contained in Γ and each free variable occurring in u is not contained in Γ. This can be shown by induction on M (simultaneously for all sets Γ).

By the same argument, one can see that (for each M and Γ) there exists a unique tuple (u,x⃗) satisfying M ◁ Γ ▷ u[x⃗], so we can consider (◁Γ▷) a function T → oT_{Γ} ×Γ⃗. Furthermore, we note that M ◁ Γ ▷ u[x⃗] always implies fV(u) = length(x⃗).

This also works the other way round. For each Γ and each tuple (u,x⃗) ∈ oT_{Γ} ⊗Γ⃗, there is (by induction on u) a term M ∈ T satisfying M ◁ Γ ▷ u[x⃗]. Moreover, this term M is unique up to α equivalence. So, (◁Γ▷) is actually a bijection between T /α (the set of α equivalence classes of terms) and oT_{Γ} ⊗ Γ⃗. The inference rules above show how to apply this bijection or its inverse to a term or a tuple (in the last rule, any variable satisfying the condition can be chosen for z), so we have a computable bijection T /α ↔ oT_{Γ} ⊗Γ⃗ determined by the rules for (◁Γ▷).

Choosing Γ = ∅, we get a bijection T /α ↔ oT ⊗∅. As ∅ is only inhabited by the empty vector [], we naturally get the parse function ▷ which maps T /α bijectively on \overline{oT}.

The above construction also gives us a function \overline{oT}→ T, but this is not enough. We want to transform closures (elements of oT ⊗ V⃗) and values (elements of V) into basic terms T. Therefore, we define the two print functions ◁ ◁: oT ⊗ V⃗→ T /α and ◁: V → T /α simultaneously by recursion on the structure:

◁ ◁(x , [])  = x  (I)
◁ ◁(• , [v])  = ◁(v)  (II)
◁ ◁(t^{m}u , v⃗)  = ◁ ◁(t , v⃗_{start}) ◁ ◁(u , v⃗_{rest})  (III)

(split v⃗at position m to get v⃗_{start}and v⃗_{rest})

◁ ◁( λk⃗.t , v⃗) = λz.◁ ◁( t , v^{z/k⃗})  (IV)

where z is any variable that does not occur freely in t or v⃗

◁(xv_{1}v_{2} ... v_{n}) = x ◁(v_{1})◁(v_{2}) ... ◁(v_{n})  (V)

(a large application simply becomes an application of terms)

◁( (λk⃗.t)v⃗)  = ◁ ◁( λk⃗.t , v⃗)  (VI)

First, note that the printing functions are well-defined (i.e., they always terminate). This is because during evaluation of ◁ ◁(u , v⃗), we may safely assume that ◁ ◁(t , w⃗)is well-defined as long as t is a strict subterm of u and each value w′in w⃗ is either only a variable (so termination of ◁(w′) is clear) or also in v⃗. Similar, during evaluation of ◁(xv_{1} ...v_{n}), we may assume that ◁(v_{i})is defined for each i.

For all t ∈ \overline{oT},M ∈ T, we have ◁ ◁(t , [])= M if and only if M ◁ ∅ ▷ t[](which just means ▷t = M) as both judgements are defined identically in the case of closed ordered terms. This essentially (with implicit use of the bijection \overline{oT} ↔ oT ⊗∅) means ◁ ◁ ∘ ▷ = id_{T}, i.e. the composition of parsing and printing is the identity.

6 Correctness and Termination properties

We still have not shown that our evaluation algorithm given in Section 4 does not change the meaning of terms. The combination of parsing, evaluating and printing should never result in a term that is not beta equivalent to the original term. We also want to show a limited termination property. To keep our argument simple, we just sketch the proofs and hope that the ideas become clear.

First, we attend to the correctness question. We need to convince ourselves that rewriting according to the rules of the functions ⟦·⟧_{·}and @ does not cause an error. By rewriting, we mean one step of the normal or leftmost outermost evaluation. We have demonstrated this in the example at the beginning of Section 4. Printing should result in a term that is β equivalent to the term we get if we rewrite before printing. This basically means that, for each evaluation rule on the left hand side of the following table, we have to check that the equality on the right hand side holds:

\begin{aligned}⟦x⟧_{[]} & = & x & ◁ ◁(x , []) & =_{β} & ◁(x) & (1) \\ ⟦•⟧_{[v]} & = & v & ◁ ◁(• , v) & =_{β} & ◁(v) & (2) \\ ⟦t^{k}u⟧_{[v⃗,w⃗]} & = & ⟦t⟧v⃗@⟦u⟧w⃗ & ◁ ◁(t^{k}u , [v⃗,w⃗]) & =_{β} & ◁ ◁(t , v⃗)◁ ◁(u , w⃗) & (3) \\ ⟦λk⃗.t⟧v⃗ & = & (λk⃗.t)v⃗ & ◁ ◁( λk⃗.t , v⃗) & =_{β} & ◁( (λk⃗.t)v⃗) & (4) \\ (xv⃗)@w & = & x[v⃗,w] & ◁(xv⃗)◁(w) & =_{β} & ◁(x[v⃗,w]) & (5) \\ (λk⃗.t)v⃗@w & = & ⟦t⟧_{}_{v^{w/k⃗}} & ◁( (λk⃗.t)v⃗) ◁(w) & =_{β} & ◁ ◁( t , v^{w/k⃗}) & (6) \end{aligned}

Note that “rewriting using the evaluation rules” results in expressions which are, more or less, a mixture of elements of oT ⊗ V⃗ and V. To be precise, such an expression is either in oT ⊗ V⃗ or in V or a tuple (to read as simple application) of two expressions. The 1^{st}, 2^{nd} and 4^{th} rule turn an element of oT ⊗ V into a value, the 3^{rd} turns it in a tuple of two such elements, and the last two rules turn a tuple of two values into one value or element. Although we do not define it formally, it should be clear how those expressions can be printed by using the printing functions for ordered terms and values (if an expression is a tuple, just print the function part and the argument part separately). In fact, while the function ⟦·⟧_{·}is formulated as a big step evaluation, the rewriting process can be understood as the corresponding small step (or one step) evaluation.

In the first five rows of the table, we only have to look at the definitions of the printing functions to see that the printed terms are not only β equivalent but also equal. The very last rule (6) requires closer examination: By rule (IV), the term ◁( (λk⃗.t)v⃗) is equal to λz.◁ ◁( t , v^{z/k⃗}) for a (sufficiently) fresh variable z. Now, the definitions of the printing functions are “context free” in a way that guarantees that z occurs exactly length(k⃗) times (free) in ◁ ◁( t , v^{z/k⃗}). Furthermore, replacing those occurrences by ◁(w)

results in the term ◁ ◁( t , v^{w/k⃗}). This means that, starting with ◁( (λk⃗.t)v⃗) ◁(w), we have to use exactly

one β reduction step to get the term ◁ ◁( t , v^{w/k⃗}).

As we have already seen that the composition of parsing a term and printing it afterwards does not change anything (up to α equivalence), we can now conclude that parsing, evaluating (a finite number of rewriting steps) and printing is equivalent to a number of β reduction steps.

Now we discuss termination. Obviously, our evaluation function ⟦·⟧_{·}does not always terminate as some terms do not have a weak head normal form. However, ⟦·⟧_{·}terminates whenever it is applied to (▷t) if the usual β reduction is strongly normalizing on t. The main consequence of this is that evaluation terminates for all well-typed terms. To prove this statement, assume that there is such a term s_{0} ∈ T so that the evaluation of t_{0} := ▷s_{0} does not terminate. Then, we get an infinite sequence t_{0},t_{1},t_{2},... where t_{i+1} is the result of rewriting (a subexpression of) t_{i} using one of the evaluation rules. If we print t_{0},t_{1},t_{2},..., we get a sequence s_{0},s_{1},s_{2},... of terms in T, where s_{i+1} is either (α) equal to s_{i} or arises from s_{i} in exactly one β reduction step. If β reduction is strongly normalizing on s_{0}, the sequence has to become constant at some point, i.e. s_{N} = s_{N+1} = s_{N+2} = ... for some N. This implies that, after the first N rewriting steps, the second @ rule (which corresponds to the last line in the table) is not used anymore. Define the weight w(t) of an expression t to be 1, if the expression is just an element of oT ⊗ V, to be 2, if it is a value of the closure type, to be 1 + 2^{n}+ w(v_{1}) + w(v_{2}) + ...+ w(v_{n}) , if it is a value of the form xv_{1}v_{2}...v_{n} (i.e. a large application) and, if it is a tuple of two expressions, as the sum of both weights. Then, each of the rewritings that are induced by the first five lines in the table increase the weight of the expression, so we get w(t_{N}) < w(t_{N+1}) < w(t_{N+2}) < ...; however, as the total number of values (and tuples in oT ⊗ V) is bound by the length of the term we get after printing t_{N} (or any t_{N+i}), the sequence is bounded, resulting in the required contradiction.

7 Experiments and Results

The specified term representation and evaluation have been implemented in Haskell. They have been used by a type checker to check large files of dependently typed terms of the Edinburgh Logical Framework which were kindly provided by Andrew W. Appel (Princeton University). To make this possible, an extended syntax has been used that includes Π-types, constants and definitions. It is straightforward to expand our evaluation algorithm to the extended syntax—for details consult the Bachelor’s thesis of the second author [16]. The substitution lists have been implemented as simple Haskell lists, and also as balanced binary trees (following Adams [2]) for better asymptotic complexity. Both variants were evaluated for performance [referred to as Ordered (trees) and Ordered (lists)].

For comparison, the completely analogous algorithm for terms in extended basic syntax (i.e. T) has been used [Simple Closures]. Furthermore, we have tested a strategy that always evaluates completely (i.e. produces β normal forms) using Hereditary Substitution [Beta Normal Values] [25].

Our main test file w32 sig semant.elf with a size of approximately 21 megabytes contains a proof described in [3]. We also tested smaller parts of this file, more precisely, the first 6000, 10,000 and 12,000 lines without the rest (named 6000.elf and so on). Later terms tend to be larger, so the tests with fewer lines needed much less time.

All tests were executed on the same server baerentatze.cip.ifi.lmu.de working with a CPU of type AMD Phenom II X4 B95 (only one core used, 3 GHz) and 8 GB system memory. The measurements of space and time consumption are given in the following tables (rounded average values):

6000.elf (file size: 3.8 MB)

time (sec) space (MB)
Ordered (trees)  18.9  1111
Ordered (lists)  18.6  1114
Simple Closures  18.5  1152
Beta Normal Values  27.6  2034

10000.elf (file size: 12.9 MB)

time (sec) space (MB)
Ordered (trees)  61.0  3230
Ordered (lists)  60.6  3237
Simple Closures  60.0  3302
Beta Normal Values  98.7  5878

12000.elf (file size: 17.8 MB)

time (sec) space (MB)
Ordered (trees)  84.3  5096
Ordered (lists)  83.8  5103
Simple Closures  83.6  5226
Beta Normal Values  137.7  8513

Unsurprisingly, beta normal values perform significantly worse than each of the other possibilities. However, the difference is smaller than it could have been expected. This might be due to the fact that during type checking, total evaluation of a term is often necessary anyway, thereby reducing the hereditary substitution’s disadvantage.

Although none of the other strategies exhibited any shortcomings in the comparisons above, the following results for the complete file are remarkable. Here, implementing ordered substitutions as normal Haskell lists seems to be much more efficient than using tree structures:

w32 sig semant.elf (file size: 20.9 MB)

time (sec) space (MB)
Ordered (trees)  108.4  8877
Ordered (lists)  94.8  4948
Simple Closures  94.3  5068
Beta Normal Values  169.8  9044

Our Simple Closures are still on the same level as Ordered Representation with lists, but the trees are far behind. In comparison, the type checker of the Twelf project, Twelf r1697 (written in Standard ML and compiled with MLton’s whole program optimizations [11]) does the job nearly five times faster while using only 2720 megabytes of memory.

8 Related Work and Conclusions

Our term representation is inspired by intuitionistic implicational linear logic in natural deduction style which has explicit operations for weakening and contraction [5]. With explicit weakening and contraction, one easily maintains complete information about the free variables of a term at each node [15]. Our term representation incorporates weakening and contraction into lambda abstraction. By using inspiration from ordered logic, we reduce the stored information at application nodes to a minimum, namely an integer; further, our variable nodes need to carry no information at all.

Another means to maintain information about free variables are director strings by Sinot [24]. Application nodes come with a map that tell for each variable whether it appears in the left or the right subterm or in both. Our term representation can be seen as an optimized version of director strings, however, we have no experimental comparison. Sinot et. al. [10] present some performance results of director strings; however, it is restricted to evaluation of some specific big lambda-terms. There is no study on their relative performance in a realistic application—yet that is our concern.

An alternative to explicit substitutions is Nadathur’s suspension calculus [19], which, in a refinement, also maintains information about closedness of subterms. In this refinement, the suspension calculus maintains at least partial information about the free variables of a subterm. As the basis of an implementation of λ-Prolog [20], Nadathur has proven the efficiency of his term representation not only for normalization and equality checking, but also for higher-order unification.

Building on the suspension calculus, Liang, Nadathur, and Qi [17] have evaluated different term representations in the context of λProlog, a study that compares to our study of term representations for the Edinburgh Logical Framework. They have tested different combinations of features, confirming our result that lazy substitution is preferable to eager substitution [Beta Normal Forms], even more so when several substitutions are gathered into one traversal [Closures, Ordered]. They also test a variant where each term is equipped with an annotation, a flag telling whether this term is open, i. e., has free variables, or closed, i. e., has no free variables. In their experimental evaluation, these annotations pay off greatly for the poorly behaving eager substitution, yet give negligible advantage for explicit substitutions. It is hypothesized that in a combined substitution, each subterm will mention at least one variable with a high probability, so the traversal has to run over most of the whole term—this is certainly different in the substitution for a single variable.

To summarize, we have presented a new term representation for the lambda-calculus inspired by ordered linear logic, and experimentally compared it with well-known representations (closures, normal forms) in a prototypical implementation of a type checker for the Edinburgh Logical Framework. The experiments were carried out on large realistic proof terms, constructed manually and mechanically.

The results were not significantly in favor of our new representation. This might be due to the application domain, LF signature checking. For one, LF-definitions are closed, which means that substitutions never need to traverse a definition body when the definition is expanded, and this optimization is shared by all the term representations we compared. Secondly, we only tested type checking, not type reconstruction via unification. During type checking, where equality tests are expected to succeed, full normal forms are always computed, and closures are very short-lived in memory. More space leaks are to be expected in applications such as logic programming or type reconstruction, where unification is needed, which is not expected to always succeed. In constraint-based unification, unsolvable constraints might be postponed, keeping closures alive for longer. In such situations, the benefits of our representation might be more noticeable, more experiments are required.

In the future, we plan to investigate further term representations such as term graphs, and perform more experiments. The literature on experimentally successful term representations is sparse, our work contributes to close this gap. Our long term goal is to find a term representation which speeds up Agda’s type reconstruction.

12 A Lambda Term Representation Inspired by Linear Ordered Logic

Acknowledgements The idea for the here presented ordered term representation was planted in a discussion with Christophe Raffalli who invited the first author to Chambery in February 2010. He mentioned to me that in his library bindlib formation of closures restricts the environment to the variables actually occurring free in the code. I also benefited from discussions with Brigitte Pientka and Stefan Monnier.

Thanks to Gabriel Scherer for comments on a draft version of this paper and pointers to related work. The final version of this paper was stylistically improved with the highly appreciated help of Neil Sculthorpe.

References

[1] Martín Abadi, Luca Cardelli, Pierre-Louis Curien & Jean-Jacques Lévy (1991): Ex-

plicit Substitutions.  Journal of Functional Programming 1(4), pp. 375–416.  Available at

http://dx.doi.org/10.1017/S0956796800000186.

[2] Stephen Adams (1993): Efficient Sets - A Balancing Act. Journal of Functional Programming 3(4), pp.

553–561. Available at http://dx.doi.org/10.1017/S0956796800000885.

[3] Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan & Daniel C. Wang (2010): Semantic foundations for typed assembly languages. ACM Transactions on Programming Languages

and Systems 32(3). Available at http://doi.acm.org/10.1145/1709093.1709094.

[4] Henk Barendregt (1984): The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam.

[5] Nick Benton, Gavin M. Bierman, Valeria de Paiva & Martin Hyland (1993): A Term Calculus for Intuitionistic Linear Logic. In: Marc Bezem & Jan Friso Groote, editors: Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, Lecture Notes in Computer Science 664, Springer-Verlag, pp. 75–90. Available at

http://dx.doi.org/10.1007/BFb0037099.

[6] Mathieu Boespflug (2010): Conversion by Evaluation. In: Manuel Carro & Ricardo Peña, editors: Practical Aspects of Declarative Languages, 12th International Symposium, PADL 2010, Madrid, Spain, January 18-19, 2010. Proceedings, Lecture Notes in Computer Science 5937, Springer-Verlag, pp. 58–72. Available at

http://dx.doi.org/10.1007/978-3-642-11503-5_7.

[7] N. G. de Bruijn (1972): Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, pp. 381–392.

[8] Iliano Cervesato & Frank Pfenning (2003): A Linear Spine Calculus. Journal of Logic and Computation

13(5), pp. 639–688. Available at http://dx.doi.org/10.1093/logcom/13.5.639.

[9] Thierry Coquand (1996): An Algorithm for Type-Checking Dependent Types. In: Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17–21, 1995, Kloster Irsee, Germany), Science of Computer Programming 26, Elsevier, pp.

167–177. Available at http://www.cs.chalmers.se/~{}coquand/type.html.

[10] Maribel Fernández, Ian Mackie & François-Régis Sinot (2005): Lambda-Calculus with Director Strings. Applicable Algebra in Engineering, Communication and Computing 15(6), pp. 393–437. Available at

http://dx.doi.org/10.1007/s00200-005-0169-9.

[11] Matthew Fluet & Stephen Weeks (2001): Contification Using Dominators. In: Proceedings of the sixth ACM SIGPLAN International Conference on Functional Programming (ICFP 2001), pp. 2–13. Available at

http://doi.acm.org/10.1145/507635.507639.

[12] Jean-Yves Girard (1987): Linear Logic. Theoretical Computer Science 50, pp. 1–102.

[13] Benjamin Grégoire & Xavier Leroy (2002): A compiled implementation of strong reduction. In: Proceedings of the seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh,

Andreas Abel and Nicolai Kraus 13

Pennsylvania, USA, October 4-6, 2002, SIGPLAN Notices 37, ACM Press, pp. 235–246. Available at

http://doi.acm.org/10.1145/581478.581501.

[14] INRIA (2010): The Coq Proof Assistant Reference Manual. INRIA, version 8.3 edition. Available at http://coq.inria.fr/. http://coq.inria.fr/.

[15] Delia Kesner & Stéphane Lengrand (2007): Resource operators for lambda-calculus. Information and Com-

putation 205(4), pp. 419–473. Available at http://dx.doi.org/10.1016/j.ic.2006.08.008.

[16] Nicolai Kraus (2011): A Lambda Term Representation Based on Linear Ordered Logic. Bachelor’s thesis, Department of Computer Science, Ludwig-Maximilians-University Munich.

[17] Chuck Liang, Gopalan Nadathur & Xiaochu Qi (2005): Choices in representation and reduction strategies for lambda terms in intensional contexts. Journal of Automated Reasoning 33(2), pp. 89–132. Available at

http://dx.doi.org/10.1007/s10817-004-6885-1.

[18] Conor McBride & James McKinna (2004): The view from the left. Journal of Functional Programming 14(1),

pp. 69–111. Available at http://dx.doi.org/10.1017/S0956796803004829.

[19] Gopalan Nadathur (1999): A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations. Journal of Functional and Logic Programming 1999(2). Available at

http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-02/A99-02.html.

[20] Gopalan Nadathur (2001): The Metalanguage lambda-Prolog and Its Implementation. In: Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Pro-

ceedings, pp. 1–20. Available at http://dx.doi.org/10.1007/3-540-44716-4_1.

[21] Ulf Norell (2007): Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden.

[22] Frank Pfenning & Carsten Schürmann (1999): System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Harald Ganzinger, editor: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, Lecture Notes in Computer Science 1632, Springer-Verlag, pp. 202–206. Available at

http://dx.doi.org/10.1007/3-540-48660-7_14.

[23] Jeff Polakow & Frank Pfenning (1999): Natural Deduction for Intuitionistic Non-communicative Linear Logic. In: Jean-Yves Girard, editor: Typed Lambda Calculi and Applications, 4th International Conference, TLCA’99, L’Aquila, Italy, April 7-9, 1999, Proceedings, Lecture Notes in Computer Science 1581, Springer-

Verlag, pp. 295–309. Available at http://dx.doi.org/10.1007/3-540-48959-2_21.

[24] François-Régis Sinot (2005): Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting. Journal of Logic and Computation 15(2), pp. 201–218.

Available at http://dx.doi.org/10.1093/logcom/exi010.

[25] Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2003): A concurrent logical framework I: Judgements and properties. Technical Report, School of Computer Science, Carnegie Mellon University, Pittsburgh.