On k-colored Lambda Terms and Their Skeletons

Abstract

The paper describes an application of logic programming to the modeling of difficult combinatorial properties of lambda terms, with focus on the class of simply typed terms.

Lambda terms in de Bruijn notation are Motzkin trees (also called binary-unary trees) with indices at their leaves counting up on the path to the root the steps to their lambda binder.

As a generalization of affine lambda terms, we introduce k-colored lambda terms obtained by labeling their lambda nodes with counts of the variables they bind. We define the skeleton of a k-colored lambda term as the Motzkin tree obtained by erasing the de Bruijn indices labeling its leaves. A new bijection between 2-colored skeletons and binary trees reveals their connection to the Catalan family of combinatorial objects.

After a statistical study of properties of k-colored lambda terms and their skeletons, we focus on the case of simply-typed closed k-colored lambda terms for which a new combinatorial generation algorithm is given and some interesting relations between maximal coloring, size of type expressions and typability are explored.

The paper is structured as a literate Prolog program to facilitate an easily replicable, concise and declarative expression of our concepts and algorithms.

1 Introduction

Lambda terms, in de Bruijn notation [1], can be seen as Motzkin-trees built of unary lambda nodes, binary application nodes and variables at their leaves, labeled with de Bruijn indices pointing toward their lambda binder. We call the skeleton of a lambda term the Motzkin tree obtained by erasing its de Bruijn indices.

A useful distinction can be made between lambda constructors that bind variables and those that do not. Among other benefits, distinguishing them makes the analysis of linear and affine terms simpler and puts their skeletons, the 2-colored Motzkin trees, in bijection with the well-known Catalan family of combinatorial objects.

More generally, can we classify lambda nodes by inverting the function from indices at the leaves to their binders?

This leads to the concept of k-colored lambda terms where colors classify binders depending on the number of variables they bind. It also brings us to the main focus of this paper, the interaction of k-coloring, skeletons and the class of simply-typed terms, starting with the easy case of always typable affine and linear terms and then empirically approaching some interesting observables for the notoriously difficult general case.

Despite the asymptotically vanishing density of simply-typed lambda terms [2], their all-term and random-term generation has been speeded-up significantly by the use of Prolog-based algorithms that interleave generation and type-inference steps [3, 4]. However, the structure of simply-typed lambda terms has so far escaped handling by analytical methods. Basic combinatorial properties like counts for terms of a given size have been obtained so far only by generating all terms, or, as in [4], by mimicking their exhaustive generation with a recursive structure that, while omitting the actual lambda terms, keeps the type-inference mechanism intact.

These difficulties are the main motivation of this paper, which suggests a fresh look at the structure of simply typed terms and their type expressions, via their relations to their k-colored skeletons, revealing insights on the structure of simply-typed closed lambda terms.

The paper is organized as follows. Section 2 describes a new bijection between binary trees and 2-colored Motzkin trees. Section 3 discusses the case of closed, linear and affine lambda terms. Section 4 focuses on the case of k-colored simply typed closed lambda terms and their statistical properties. Section 5 overviews related work and Sect. 6 concludes the paper.

The paper is structured as a literate Prolog program to facilitate an easily replicable, concise and declarative expression of our concepts and algorithms. The code extracted from the paper, together with some related code and utilities for visualization is available at: http://www.cse.unt.edu/~tarau/research/2017/padl18.pro, tested with SWI-Prolog [5] version 7.4.2.

2 A Bijection Between 2-colored Motzkin Trees and Binary Trees

A Motzkin tree (also called binary-unary tree) is a rooted ordered tree built from binary nodes, unary nodes and leaf nodes. A k-colored Motzkin tree is obtained by labeling its unary nodes with colors from a set of k elements.

As usual in Prolog, we denote, F/N a function symbol F of arity N. Given a set of such function symbols (that we will also call “constructors”) one can see the set of terms generated from them as a free algebra using the set of functors as its signature.

We define 2-colored Motzkin trees (shortly 2-Motzkin trees) as the free algebra generated by the constructors v/0, l/1, r/1 and a/2. An example of a Prolog term representing a 2-colored Motzkin tree is l(a(l(v),r(v))).

We define lambda terms in de Bruijn form as the free algebra generated by the constructors l/1, r/1 and a/2 with leaves labeled with natural numbers (and seen as wrapped with the constructor v/1 when convenient). When talking about lambda terms, we interpret l/1 constructors as lambda binders a/2 constructors as applications and v/1 constructors as de Bruijn index nodes.

Thus, we can see lambda terms in de Bruijn form as Motzkin trees with leaves labeled with natural numbers. We interpret the labels as pointing to their lambda binder on a path to the root of the tree. If each leaf reaches via its de Bruijn index at least one unary constructor, we call the term closed, otherwise we call it plain.

We observe that the constructors marking lambdas may have at least one de Bruijn index pointing to them or have none. We can think about these as 2-colored lambda terms. Thus, we classify our unary constructors into:

• binding lambdas, that are reached by at least one de Bruijn index (denoted l/1)

• free lambdas, that cannot be reached by any de Bruijn index (denoted r/1).

We define the 2-colored Motzkin skeleton of a lambda term (shortly skeleton) as the 2-Motzkin tree obtained by erasing the de Bruijn indices labeling their leaves.

It is well-known that 2-Motzkin trees are counted by the Catalan numbers and several bijections between them to members of the Catalan family of combinatorial objects have been identified in the past [6]. We will introduce here a new one that is defined inductively in a “compositional way”, based on a mapping between small tree components on the two sides. As an application, this allows one to use a uniform random binary tree generation algorithm like [7] to generate random 2-Motzkin trees.

We describe binary trees as the free algebra generated by the constructors e/0 and c/2. Binary trees are a well known member of the Catalan family of combinatorial objects. Our bijection can be seen as connecting any other member of this family to 2-colored Motzkin trees.

We define the bijection between non-empty binary trees and 2-Motzkin trees simply by encoding each of the nodes v/0, l/1, r/1 and a/2 by a unique small binary tree as shown by the reversible bidirectional predicate cat_mot/2, with the binary tree as its first argument and the 2-Motzkin tree as its second.

Proposition 1

The predicate cat_mot/2 defines a bijection between non-empty binary trees and 2-colored Motzkin trees.

Proof

It follows by structural induction by observing that the 4 clauses cover via disjoint unification patterns all the 4 possible tree shapes matched one-to-one on the two sides.

Example 1

We illustrate the bidirectional Prolog predicate cat_mot/2 with the two trees also shown in Fig. 1, together with two larger trees on the right side, “twinned” in a similar way, Motzkin-tree on the left, binary tree on the right.

Fig. 1.

The 2-colored Motzkin trees to non-empty binary trees bijection

As a first application, a linear-time random generator for binary trees (based on instance Rémy’s algorithm, [7]) can be “borrowed” in linear time in the size of the terms, to generate 2-colored Motzkin random motzkin trees via the bijection defined by the predicate cat_mot/2.

One can also “borrow” the simple binary tree generator cat(N,T) which, given a natural number N returns a tree X of size N, assuming a size definition that counts each internal node as 1.

Note the use of the bidirectional succ/2 built-in, which also tests for being larger than 0, when working as predecessor.

By using the generator cat/2 for binary trees, we derive a generator for 2-colored Motzkin trees via their bijection to non-empty binary trees as follows.

Given an enumeration of binary trees given by successor s/1 and predecessor p/1 (for instance the one in [8] that also provides more general arithmetic operations on them) one can define ranking and unranking operations on binary trees (bijections to/from the set of natural numbers).

Shifting the bijection from binary trees to Motzkin trees to include the empty binary tree is achieved with the predicates cat2mot/2 and mot2cat/2. Note the use of the s/1 and p/1 operations from [8], that are also given in the literate Prolog program associated in this paper.

This leads to ranking and unranking of 2-colored Motzkin trees via their bijection to binary trees, defined as

Unranking can then be defined as:

Note also the t/2 predicate mapping a natural number to a binary tree and the n/2 predicate mapping a tree its natural number correspondent. We refer to [8] for their definition and implementation, converting efficiently between binary representations of numbers to/from trees, also replicated in the literate code of this paper.

3 Closed, Affine and Linear Terms

We can see a lambda term in de Bruijn form as a Motzkin tree decorated with natural numbers at its leaves. With a size definition (assumed here) that gives 2 units to binary constructors, 1 unit to unary constructors and 0 units to the leaves of the tree, a lambda term and its skeleton can be, conveniently, seen as having the same size, in fact corresponding (up to a constant factor) to its heap representation in the runtime system of all programming languages we know of.

Semantically, the labels are understood as pointing to a unary node seen as a lambda binder on the path to the root, starting with 0 for the closest one.

Thus a lambda term is built with the constructors a/2 representing applications, l/1 and r/1 representing lambda nodes and natural numbers marking leaves (possibly wrapped as v/1 nodes, when convenient).

A 2-Motzkin tree is built with a/2 representing binary nodes, l/1 and r/1 representing unary nodes and v/0 standing for leaf nodes. Thus we compute a skeleton by replacing the de Bruijn indices at the leaves of a lambda term with the constant v/0.

When generating trees of a given size, with several node constructors, it makes sense to have separate counters for each. The predicate sum_to/3 maintains such counters for nodes of types l/1, r/1 and a/2.

The predicates (suggestively named) lDec/2, rDec/2 and aDec/2 define single steps consuming one available unit of size for each of the corresponding constructors. Note the use of the bidirectional built-in predicate succ/2 that computes in this case the predecessor of a natural number and fails after reaching 0.

We will start with generators for closed, affine and linear terms.

As analytic methods are known for computing counts for closed terms as well as closed affine and linear terms [9], we will focus here on some simple properties of their skeletons and on their efficient generators.

3.1 Closed Lambda Terms

A lambda term in de Bruijn form is closed, if for each of its de Bruijn indices, there is a lambda binder to which it points, on the path to the root of the tree representing the term. We call a Motzkin tree closable if it is the skeleton of at least one closed lambda term.

It immediately follows that:

Proposition 2

If a Motzkin tree is a skeleton of a closed lambda term, then it exists at least one lambda binder on each path from the leaf to the root.

There are slightly more unclosable Motzkin trees than closable ones as size grows:

number of closable skeletons of sizes 0,1,2,... :  

0,1,1,2,5,11,26,65,163,417,1086,2858,7599,20391,55127,150028,410719, ...

number of unclosable skeletons of sizes 0,1,2,... :

1,0,1,2,4,10,25,62,160,418,1102,2940,7912,21444,58507,160544,442748, ...

We refer to [10] for an analytic solution proving that asymptotically $\dfrac{1}{\sqrt{5}}$ of the skeletons are closable.

3.2 Closed Affine Lambda Terms

An affine lambda term has one or zero variables bound by each lambda constructor.

Proposition 3

If a 2-Motzkin tree with n binary nodes is a skeleton of an affine lambda term, then it has exactly $n+1$ unary l nodes, with at least one on each path from the root to its $n+1$ leaves.

This suggests generators that separate unary and binary node counts for the skeletons and enforce this constraint on their respective sizes.

The predicate afLam/2, follows closely the one described in detail in [11], except that it handles l/1 and r/1 as separate cases.

The predicate has_enough_lambdas/1 is used to express the constraint that the number of application nodes a/2 should be one less than the number of l/1 constructors (in bijection with the leaves they bind). The predicate afLinLam/4 is defined via Definite Clause Grammars (DCGs) that encapsulate the consumption of the size units¹. It uses the predicate subset_and_complement_of/3 to direct each lambda binder on either a left or a right path at an application node. Note also the use of the constructor l/2 holding as its first argument the actual variable that it binds.

Erasure of de Bruijn indices turns a 2-colored lambda term into a 2-colored Motzkin tree.

The predicates afSkelGen/2 and linSkelGen/2 transform the generator for lambda terms into generators for their skeletons.

The multiset of skeletons is trimmed to a set of unique skeletons using SWI-Prolog’s distinct/2 built-in.

3.3 Closed Linear Lambda Terms

As lambda binders in linear terms are in bijection with the (uniques) leaves they bind, the following holds.

Proposition 4

If a Motzkin tree with n binary nodes is a skeleton of a linear lambda term, then it has exactly $n+1$ unary nodes, with one on each path from the root to its $n+1$ leaves.

Note the use of the predicate has_no_unused/1 that expresses, quite concisely, the constraints that r/1 nodes should not occur in the term and that the set of l/1 nodes should be in a bijection with the set of leaves.

As (at most) one variable is associated to each binder, no type conflict can arise between occurrences. Thus, all closed affine and linear terms are well-typed. The unary nodes of the skeletons of affine term can be seen as having 2 colors, l/1 and r/1. This suggests to investigate next the general case of k-colored terms.

4 k-colored Simply-Typed Closed Lambda Terms

As a natural generalization derived from k-colored Motzkin trees, we define a k-colored lambda term having as its lambda constructor l/1 labeled with the number of variables that it binds. Thus an affine term is a 2-colored lambda term.

The predicate kColoredClosed/2 generates terms while partitioning lambda binders in k-colored classes. It works by incrementing the count of leaf variables a lambda binds, in a “backtrackable way”, by using successor arithmetic with the deepest node kept as a free logical variable at each step.

Note also the DCG-mechanism that controls the intended size of the terms via the (conveniently named) predicates l/2 and a/2 that decrement available size by 1 and respectively 2 units.

Example 2

3-colored lambda terms of size 3, exhibiting colors 0,1,2.

Given a tree with n application nodes, the counts for all k-colored lambdas in it must sum up to $n+1$. Thus we can generate a binary tree and then decorate it with lambdas satisfying this constraint. Note that the constraint holds for subtrees, recursively. We leave it as future work to find out if this mechanism can reduce the amount of backtracking and accelerate term generation.

4.1 Type Inference for k-colored Terms

The study of the combinatorial properties of simply-typed lambda terms is notoriously hard. The two most striking facts that one might notice when inferring types are:

• non-monotonicity, as crossing a lambda increases the size of the type, while crossing an application node trims it down

• agreement via unification (with occurs check) between the types of each variable under a lambda

Interestingly, to our best knowledge, no SAT or ASP algorithms exist in the literature that attack the combined type inference and combinatorial generation problem for lambda terms, most likely because of the complexity of emulating unification-with-occurs-check steps in propositional logic. Thus we will follow the interleaving of term generation, checking for closedness and type inference steps shown in [8], but enhance it to also identify variables covered by each lambda binder. In fact, given the surjective function $f:V \rightarrow L$ that associates to each leaf variable in a closed lambda term its lambda binder, one can compute the set $f^{-1}(l)$ for each $l \in L$, expressing which variables are mapped to each binder.

Example 3

We illustrate two 2-colored simply typed terms with lambda nodes shown as l/1 constructors marked with the labels of the variables they bind (if any). We place the inferred type as the right child of a “root” labeled with “:”.

As in [8], our type inference algorithm ensures that variables under the same binder agree on their type via unification with occurs check, to avoid formation of cycles in the types, represented as binary trees with internal nodes “->/2” and logic variables as leaves.

Note that addToBinder/2 adds each leaf under a binder to the open end of the list of variable/type pairs list, closed by closeBinder/1.

Fig. 2.

Counts of simply typed closed terms and affine closed terms by increasing sizes

Example 4

Some terms of size 5 generated by the predicate simplyTypedColored/3 and their types.

We are now ready to make some empirical observations on terms, colors and type sizes. We have noticed that both average and maximum number of colors of lambda terms grow very slowly with size. Figure 2 compares on a log-scale the growths of simply typed closed terms and their closed affine terms subset. As for de Bruijn terms, we can define the Motzkin skeletons of k-colored lambda terms by erasing the first argument of the l/2 and v/1 constructors. We can also define the k-colored Motzkin skeletons of these terms by replacing the variable lists in argument 1 of l/2 constructors by their length and by erasing the arguments of the v/1 constructors.

The predicate toSkels/3 computes the (k-colored) Motzkin skeletons by measuring the length of the list of variables for each binder.

We obtain generators for skeletons and k-colored skeletons by combining the generator simplyTypedColored with toSkeleton.

We can generate the set of typable skeletons from the multiset of skeletons by using the built-in distinct/2 that trims duplicate solutions.

We define the type size of a simply typed term as the number of arrow nodes “->” its type contains, as computed by the predicate tsize/2.

Fig. 3.

Growth of colors and type sizes

Fig. 4.

Colors of a most colorful term vs. its maximum type size

Now that we can count, for a given term size, how many k-colored terms exists, one might ask if we can say something about the sizes of their types. This suggests an investigation of the relations between the complexity of type expressions and the number of colors.

Figure 3 shows the significantly slower growths of the average number of colors of colored terms vs. the average size of their types, with a possible log-scale correlation between them.

We call a most colorful term of a given size a term that reaches the maximum number of colors.

Figure 4 shows the relation between the number of colors of a most colorful term and a maximum size reached by the type of such a term.

Figure 5 shows the relation between the largest type sizes the most colorful terms of a given size can attain and the maximum possible type size of those terms.

We can observe that the largest most colorful terms reach the largest possible type size for a given term size, most of the time, but as Fig. 5 shows, there are exceptions.

We leave as an open problem to prove or disprove that there’s a term size such that for larger terms, the most colorful such terms reach the largest type size possible.

Fig. 5.

Largest type size of a most colorful term vs. largest type size

5 Related Work

Several papers exist that define bijections between 2-Motzkin trees and members of the Catalan family of combinatorial objects (e.g., in [6]), typically via depth-first walks in trees connected to Motzkin, Dyck or Schröder paths. However, we have not found any simple and intuitive bijection that connects components of the two families, or one that connects directly binary trees and 2-Motzkin trees, like the one shown in this paper.

The classic reference for lambda calculus is [12]. Various instances of typed lambda calculi are overviewed in [13]. The use of de Bruijn indices for the study of combinatorial properties of lambda terms is introduced in [14].

The combinatorics and asymptotic behavior of various classes of lambda terms are extensively studied in [15]. Distribution and density properties of random lambda terms are described in [16].

The generation and counting of affine and linear lambda terms is extensively covered in [9], with limits for counting larger than in this paper reachable using efficient recurrence formulas. Their asymptotic behavior, in relation with the BCK and BCI combinator systems, as well as bijections to combinatorial maps are studied in [17]. In [10] analytic models are used to solve the problem of the asymptotic density of closable skeletons and their subclass of uniquely closable skeletons.

Asymptotic density properties of simple types (corresponding to tautologies in minimal logic) have been studied in [18] with the surprising result that “almost all” classical tautologies are also intuitionistic ones.

6 Conclusions

The new, intuitive bijection between binary terms and 2-colored Motzkin terms, in combination with Rémy’s algorithm [7] for the generation of random binary trees, can also be used to produce large random simply-typed terms, with applications to testing functional programming languages and proof assistants using lambda calculus as their internal language.

The distinction between free and binding lambda constructors in 2-colored terms has helped design a simple and efficient algorithm for generating affine and linear terms.

Contrary to closed, linear and affine lambda terms (as well as several other classes of terms subject to similar constraints) the structure of simply-typed terms has so far escaped a precise characterization. While the focus of the paper is mostly empirical, it has unwrapped some new “observables” that highlight interesting statistical properties. The relations identified between colors and type sizes of lambda terms have led to some interesting (but possibly very hard) open problems.

In a way, our concepts involve abstraction mechanisms that “forget” properties of the difficult class of simply-typed closed lambda terms to reveal equivalence classes that are likely to be easier to grasp with analytic tools. Among them, k-colored terms subsume linear and affine terms and are likely to be usable to fine-tune random generators to more closely match “color-distributions” of lambda terms representing real programs.

Last but not least, we have shown that a language as simple as side-effect-free Prolog, with limited use of impure features and meta-programming, can handle elegantly complex combinatorial generation problems, when the synergy between sound unification, backtracking and DCGs is put at work.