Keywords

1 Introduction

Generation of lambda terms [1] has practical applications to testing compilers that rely on lambda calculus as an intermediate language, as well as in generation of random tests for user-level programs and data types. At the same time, several instances of lambda calculus are of significant theoretical interest given their correspondence with logic and proofs. Among them, simply-typed lambda terms [2, 3] enjoy a number of nice properties, among which strong normalization (termination for all evaluation-orders), a cartesian closed category mapping and a set-theoretical semantics. More importantly, via the Curry-Howard correspondence lambda terms that are inhabitants of simple types can be seen as proofs for tautologies in minimal logic which, in turn, correspond to the types. Extended with a fix-point operator, simply-typed lambda terms can be used as the intermediate language for compiling Turing-complete functional languages. Generation of large simply-typed lambda terms can also help with automation of testing and debugging compilers for functional programming languages [4].

Recent work on the combinatorics of lambda terms [5,6,7,8], relying on recursion equations, generating functions and techniques from analytic combinatorics [9] has provided counts for several families of lambda terms and clarified important properties like their asymptotic density. With the techniques provided by generating functions [9], it was possible to separate the counting of the terms of a given size for several families of lambda terms from their more computation intensive generation, resulting in several additions (e.g., A220894, A224345, A114851) to The On-Line Encyclopedia of Integer Sequences, [10].

On the other hand, the combinatorics of simply-typed lambda terms, given the absence of closed formulas, recurrence equations or grammar-based generators, due to the intricate interaction between type inference and the applicative structure of lambda terms, has left important problems open, including the very basic one of counting the number of closed simply-typed lambda terms of a given size. At this point, obtaining counts for simply-typed lambda terms requires going through the more computation-intensive generation process.

As a fortunate synergy, Prolog’s sound unification of logic variables, backtracking and definite clause grammars have been shown to provide compact combinatorial generation algorithms for various families of lambda terms [11,12,13,14].

For the case of simply-typed lambda terms, we have pushed (in the unpublished draft [15]) the counts in sequence A220471 of [10] to cover sizes 11 and 12, each requiring about one magnitude of extra computation effort, simply by writing the generators in Prolog. In this paper we focus on going two more magnitudes higher, while also integrating the results described in [15]. Using similar techniques, we achieve the same, for the special case of simply-typed normal forms.

The paper is organized as follows. Section 2 describes our representation of lambda terms and derives a generator for closed lambda terms. Section 3 defines generators for well-formed type formulas. Section 4 introduces a type inference algorithm and then derives, step by step, efficient generators for simply-typed lambda terms and simple types inhabited by terms of a given size. Section 5 defines generators for closed lambda terms in normal form and then replicates the derivation of an efficient generator for simply-typed closed normal forms. Section 6 aggregates our experimental performance data and Sect. 7 discusses possible extensions and future improvements. Section 8 overviews related work and Sect. 9 concludes the paper.

The paper is structured as a literate Prolog program. The code has been tested with SWI-Prolog 7.3.8 and YAP 6.3.4. It is also available as a separate file at http://www.cse.unt.edu/~tarau/research/2016/lgen.pro.

2 Deriving a Generator for Lambda Terms

Lambda terms can be seen as Motzkin trees [16], also called unary-binary trees, labeled with lambda binders at their unary nodes and corresponding variables at the leaves. We will thus derive a generator for them from a generator for Motzkin trees.

2.1 A Canonical Representation with Logic Variables

We can represent lambda terms [1] in Prolog using the constructors a/2 for applications, l/2 for lambda abstractions and v/1 for variable occurrences. Variables bound by the lambdas and their occurrences are represented as logic variables. As an example, the lambda term \(~\lambda a.(\lambda b.(a~(b~b)) ~ \lambda c.(a~(c~c)) )\) will be represented as l(A,a(l(B,a(v(A),a(v(B),v(B)))),l(C,a(v(A),a(v(C),v(C)))))). As variables share a unique scope (the clause containing them), this representation assumes that distinct variables are used for distinct scopes induced by the lambda binders in terms occurring in a given Prolog clause.

Lambda terms might contain free variables not associated to any binders. Such terms are called open. A closed term is such that each variable occurrence is associated to a binder.

2.2 Generating Motzkin Trees

Motzkin-trees (also called binary-unary trees) have internal nodes of arities 1 or 2. Thus they can be seen as a skeleton of lambda terms that ignores binders and variables and their leaves.

The predicate motzkin/2 generates Motzkin trees with S internal and leaf nodes.

figure a

Motzkin-trees, with leaves assumed of size 1 are counted by the sequence A001006 in [10]. Alternatively, as in our case, when leaves are assumed of size 0, we obtain binary-unary trees with S internal nodes, counted by the entry A006318 (Large Schröder Numbers) of [10].

Note the use of the predicate down/2, that assumes natural numbers in unary notation, with n s/1 symbols wrapped around 0 to denote \(n \in \mathbb {N}\). As our combinatorial generation algorithms will usually be tractable for values of n below 15, the use of unary notation is comparable (and often slightly faster) than the call to arithmetic built-ins. Note also that this leads, after the DCG translation, to “pure” Prolog programs made exclusively of Horn Clauses, as the DCG notation can be eliminated by threading two extra arguments controlling the size of the terms.

To more conveniently call these generators with the usual natural numbers we define the converter n2s as follows.

figure b

Example 1

Motzkin trees with 2 internal nodes.

figure c

2.3 Generating Closed Lambda Terms

We derive a generator for closed lambda terms by adding logic variables as labels to their binder and variable nodes, while ensuring that the terms are closed, i.e., that the function mapping variables to their binders is total.

The predicate lambda/2 builds a list of logic variables as it generates binders. When generating a leaf variable, it picks “nondeterministically” one of the binders among the list of binders available, Vs. As in the case of Motzkin trees, the predicate down/2 controls the number of internal nodes.

figure d

The sequence A220471 in [10] contains counts for lambda terms of increasing sizes, with size defined as the number of internal nodes.

Example 2

Closed lambda terms with 2 internal nodes.

figure e

3 A Visit to the Other Side: The Language of Types

As a result of the Curry-Howard correspondence, the language of types is isomorphic with that of minimal logic, with binary trees having variables at leaf positions and the implication operator (“-> ”) at internal nodes. We will rely on the right associativity of this operator in Prolog, that matches the standard notation in type theory.

The predicate type_skel/3 generates all binary trees with given number of internal nodes and labels their leaves with unique logic variables. It also collects the variables to a list returned as its third argument.

figure f

Type skeletons are counted by the Catalan numbers (sequence A000108 in [10]).

Example 3

All type skeletons for N = 3.

figure g

The next step toward generating the set of all type formulas is observing that logic variables define equivalence classes that can be used to generate partitions of the set of variables, simply by selectively unifying them.

The predicate mpart_of/2 takes a list of distinct logic variables and generates partitions-as-equivalence-relations by unifying them “nondeterministically”. It also collects the unique variables, defining the equivalence classes as a list given by its second argument.

figure h

To implement a set-partition generator, we will split a set repeatedly in subset+complement pairs with help from the predicate mcomplement_of/2.

figure i

To generate set partitions of a set of variables of a given size, we build a list of fresh variables with the equivalent of Prolog’s length predicate working in unary notation, len/2.

figure j

The count of the resulting set-partitions (Bell numbers) corresponds to the entry A000110 in [10].

Example 4

Set partitions of size 3 expressed as variable equalities.

figure k

We can then define the language of formulas in minimal logic, among which tautologies will correspond to simple types, as being generated by the predicate maybe_type/3.

figure l

Example 5

Well-formed formulas of minimal logic (possibly types) of size 2.

figure m

The sequence 2,10,75,728,8526,115764,1776060,30240210 counting these formulas corresponds to the product of Catalan and Bell numbers.

4 Merging the Two Worlds: Generating Simply-Typable Lambda Terms

One can observe that per-size counts of both the sets of lambda terms and their potential types are very fast growing. There is an important difference, though, between computing the type of a given lambda term (if it exists) and computing an inhabitant of a type (if it exists). The first operation, called type inference is an efficient operation (linear in practice) while the second operation, called the inhabitation problem is P-space complete [17].

This brings us to design a type inference algorithm that takes advantage of operations on logic variables.

4.1 A Type Inference Algorithm

While in a functional language inferring types requires implementing unification with occurs-check, as shown for instance in [5], this operation is available in Prolog as a built-in predicate, optimized, for instance, in SWI-Prolog [18], to proceed incrementally, only checking that no new cycles are introduced during the unification step as such.

The predicate infer_type/3 works by using logic variables as dictionaries associating terms to their types. Each logic variable is then bound to a term of the form X:T where X will be a component of a fresh copy of the term and T will be its type. Note that we create this new term as the original term’s variables end up loaded with chunks of the partial types created during the type inference process.

As logic variable bindings propagate between binders and occurrences, this ensures that types are consistently inferred.

figure n

Example 6

illustrates typability of the term corresponding to the S combinator

\( \lambda x_0. \lambda x_1. \lambda x_2.((x_0~x_2)~(x_1~x_2))\)

and untypabilty of the term corresponding to the Y combinator

\( \lambda x_0.(\lambda x_1.(x_0~(x_1~x_1)) ~ ~\lambda x_2.(x_0~(x_2~x_2)) ) \).

figure o

By combining generation of lambda terms with type inference we have our first cut to an already surprisingly fast generator for simply-typable lambda terms, able to generate in a few hours counts for sizes 11 and 12 for sequence A220471 in [10].

figure p

Example 7

Lambda terms of size up to 3 and their types.

figure q

Note that, for instance, when one wants to select only terms having a given type, this is quite inefficient. Next, we will show how to combine size-bound term generation, testing for closed terms and type inference into a single predicate. This will enable more efficient querying for terms inhabiting a given type, as one would expect from Prolog’s multi-directional execution model, and more importantly for our purposes, to climb two orders of magnitude higher for counting simply-typed terms of size 13 and 14.

4.2 Combining Term Generation and Type Inference

We need two changes to infer_type to turn it into an efficient generator for simply-typed lambda terms. First, we need to add an argument to control the size of the terms and ensure termination, by calling down/2 for internal nodes. Second, we need to generate the mapping between binders and variables. We ensure this by borrowing the member/2-based mechanism used in the predicate lambda/4 generating closed lambda terms in Subsect. 2.3.

The predicate typed_lambda/3 does just that, with helper from DCG-expanded typed_lambda/5.

figure r

Like lambda/4, the predicate typed_lambda/5 relies on Prolog’s DCG notation to thread together the steps controlled by the predicate down. Note also the nondeterministic use of the built-in member/2 that enumerates values for variable:type pairs ranging over the list of available pairs Vs, as well as the use of unify_with_occurs_check to ensure that unification of candidate types does not create cycles.

Example 8

A simply-typed term of size 15 and its type.

figure s

We will discuss exact performance data later, but let’s note here that this operation brings down by an order of magnitude the computational effort to generate simply-typed terms. As expected, the number of solutions is computed as the sequence A220471 in [10]. Interestingly, by interleaving generation of closed terms and type inference in the predicate typed_lambda, the time to generate all the closed simply-typed terms is actually shorter than the time to generate all closed terms of the same size, e.g., 17.123 vs. 31.442 seconds for size 10 with SWI-Prolog. As, via the Curry-Howard isomorphism, closed simply typed terms correspond to proofs of tautologies in minimal logic, co-generation of terms and types corresponds to co-generation of tautologies and their proofs for proofs of given length.

4.3 One More Trim: Generating Inhabited Types

Let’s first observe that the actual lambda term does not need to be built, provided that we mimic exactly the type inference operations that one would need to perform to ensure it is simply-typed. It is thus safe to remove the first argument of typed_lambda/5 as well as the building of the fresh copy performed in the second argument. To further simplify the code, we can also make the DCG-processing of the size computations explicit, in the last two arguments.

This gives the predicate inhabited_type/4 and then inhabited_type/2, that generates all types having inhabitants of a given size, but omits the inhabitants as such.

figure t

Clearly the multiset of generated types has the same count as the set of their inhabitants and this brings us an additional 1.5x speed-up.

figure u

One more (easy) step, giving a 3x speed-up, makes reaching counts for sizes 13 and 14 achievable: using a faster Prolog, with a similar unify_with_occurs_check built-in, like YAP [19], with the last value computed in less than a day.

Example 9

The sequence A220471 completed up to N = 14

figure v

5 Doing It once More: Generating Closed Simply-Typed Normal Forms

We will devise similar methods for an important subclass of simply-typed lambda terms.

5.1 Generating Normal Forms

Normal forms are lambda terms that cannot be further reduced. A normal form should not be an application with a lambda as its left branch and, recursively, its subterms should also be normal forms. The predicate normal_form/2 uses normal_form/4 to define them inductively and generates all normal forms with S internal nodes.

figure w

Example 10

Illustrates closed normal forms with 2 internal nodes.

figure x

The number of solutions of our generator replicates entry A224345 in [10] that counts closed normal forms of various sizes.

The predicate nf_with_type applies the type inference algorithm to the generated normal forms of size S.

figure y

5.2 Merging in Type Inference

Like in the case of the set of simply-typed lambda terms, we can define the more efficient combined generator and type inferrer predicate typed_nf/2.

figure z

It works by calling the DCG-expended typed_nf/4 predicate, with the last two arguments enforcing the size constraints.

figure aa

Example 11

Simply-typed normal forms up to size 3.

figure ab

We are now able to efficiently generate counts for simply-typed normal forms of a given size.

Example 12

Counts for closed simply-typed normal forms up to N=14.

figure ac

Note that if we would want to just collect the set of types having inhabitants of a given size, the preservation of typability under \(\beta \) -reduction property [3] would allow us to work with the (smaller) set of simply-typed terms in normal form.

6 Experimental Data

Figure 1 gives the number of logical inferences as counted by SWI-Prolog. This is a good measure of computational effort except for counting operations like unify_with_occurs_check as a single step, while its actual complexity depends on the size of the terms involved. Therefore, Fig. 2 gives actual timings for the same operations above N=5, where they start to be meaningful.

The “closed \(\lambda \) -terms” column gives logical inferences and timing for generating all closed lambda terms of size given in column 1. The column “gen, then infer” covers the algorithm that first generates lambda terms and then infers their types. The column “gen + infer” gives performance data for the significantly faster algorithm that merges generation and type inference in the same predicate. The column “inhabitants” gives data for the case when actual inhabitants are omitted in the merged generation and type inference process. The column “typed normal form” shows results for the fast, merged generation and type inference for terms in normal form.

As moving from a size to the next typically adds one order of magnitude of computational effort, computing values for N=15 and N=16 is reachable with our best algorithms for both simply typed terms and their normal form subset.

Fig. 1.
figure 1

Number of logical inferences used by our generators, as counted by SWI-Prolog

Full size image
Fig. 2.
figure 2

Timings (in seconds) for our generators up to size 10 (on a 2015 MacBook, with 1.3 GHz Intel Core M processor)

Full size image

7 Discussion

An interesting open problem is if this can be pushed significantly farther. We have looked into term_hash based indexing and tabling-based dynamic programming algorithms, using de Bruijn terms. Unfortunately as subterms of closed terms are not necessarily closed, even if de Bruijn terms can be used as ground keys, their associated types are incomplete and dependent on the context in which they are inferred.

While it only offers a constant factor speed-up, parallel execution is a more promising possibility. However, given the small granularity of the generation and type inference process, the most useful parallel execution mechanism would simply split the task of combined generation and inference process into a number of disjoint sets, corresponding to the number of available processors. A way to do this, is by using unranking functions (bijections originating in \(\mathbb {N}\)) to the sets of combinatorial objects involved, and then, for k processors, assign work on successive numbers belonging to the same equivalence class modulo k. Another way is to first generate Motzkin trees and then launch threads to “flesh them up” with logic variables, run the type inference steps and collect success counts atomically.

We have not seen any obvious way to improve these results using constraint programing systems, partly because the “inner loop” computation is unification with occurs check with computations ranging over Prolog terms rather than being objects of a constraint domain. On the other hand, for a given size, exploring grounding to propositional formulas or answer-set programming seems worth exploring as a way to take advantage of today’s fast SAT-solvers.

Several concepts of size have been used in the literature, for reasons ranging from simplifying evaluation procedures, to matching the structure of the terms naturally occurring in practical programs [20]. As a byproduct, some size definitions also result in better convergence conditions of formal series in analytic combinatorics [21]. Our techniques can be easily adapted to a different size definition like the ones in [20, 21] where variables in de Bruijn notation have a size proportional to the distance to their binder. We have not discussed here the use of similar techniques to improve the Boltzmann samplers described to [22], but clearly interleaving type checking with the probability-driven building of the terms would improve their performance, by excluding terms with ill-typed subterms as early as possible, during the large number of retries needed to overcome the asymptotically 0-density of simply-typed terms in the set of closed terms [6].

8 Related Work

The classic reference for lambda calculus is [1]. Various instances of typed lambda calculi are overviewed in [3].

The combinatorics and asymptotic behavior of various classes of lambda terms are extensively studied in [5, 8]. Distribution and density properties of random lambda terms are described in [6].

Generation of random simply-typed lambda terms and its applications to generating functional programs from type definitions is covered in [23].

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

In [4] a “type-directed” mechanism for the generation of random terms is introduced, resulting in more realistic (while not uniformly random) terms, used successfully in discovering some bugs in the Glasgow Haskell Compiler (GHC). A statistical exploration of the structure of the simple types of lambda terms of a given size in [14] gives indications that some types frequent in human-written programs are among the most frequently inferred ones.

Generators for closed simply-typed lambda terms, as well as their normal forms, expressed as functional programming algorithms, are given in [5], derived from combinatorial recurrences. However, they are significantly more complex than the ones described here in Prolog, and limited to terms up to size 10.

In the unpublished draft [15] we have collected several lambda term generation algorithms written in Prolog and covering mostly de Bruijn terms and a compressed de Bruijn representation. Among them, we have covered linear, affine linear terms as well as terms of bounded unary height and in binary lambda calculus encoding. In [15] type inference algorithms are also given for SK and Rosser’s X-combinator expressions. A similar (but slower) program for type inference using de Bruijn notation is also given in the unpublished draft [15], without however describing the step-by-step derivation steps leading to it, as done in this paper.

In [25] a general constraint logic programming framework is defined for size-constrained generation of data structures as well as a program-transformation mechanism. While our fine-tuned interleaving of term generation and type inference directly provides the benefits of a CLP-based scheme, the program transformation techniques described in [25] are worth exploring for possible performance improvements. In [26] a general Haskell-based framework for generating enumerable structures is introduced. While clearly useful for arbitrary free structures, the fine-grained interleaving of generation and type inference of this paper do not seem to be embeddable in it with similar performance gains.

9 Conclusion

We have derived several logic programs that have helped solve the fairly hard combinatorial counting and generation problem for simply-typed lambda terms, 4 orders of magnitude higher than previously published results.

This has put at test two simple but effective program transformation techniques naturally available in logic programming languages: (1) interleaving generators and testers by integrating them in the same predicate and (2) dropping arguments used in generators when used simply as counters of solutions, as in this case their role can be kept implicit in the recursive structure of the program. Both have turned out to be effective for speeding up computations without changing the semantics of their intended application. We have also managed (after a simple DCG translation) to work within in the minimalist framework of Horn Clauses with sound unification, showing that non-trivial combinatorics problems can be handled without any of Prolog’s impure features.

Our techniques, combining unification of logic variables with Prolog’s backtracking mechanism and DCG grammar notation, recommend logic programming as a convenient meta-language for the manipulation of various families of lambda terms and the study of their combinatorial and computational properties.