We describe a Prolog-based combined lambda term generator and type-inferrer for closed well-typed terms of a given size, in de Bruijn notation. By taking advantage of Prolog's unique bidirectional execution model and sound unification algorithm, our generator can build “customized” closed terms of a given type. This relational view of terms and their types enables the discovery of interesting patterns about frequently used type expressions occurring in well-typed functional programs. Our study uncovers the most “popular” types that govern function applications among a about a million small-sized lambda terms and hints toward practical uses to combinatorial software testing. It also shows the effectiveness of Prolog as a meta-language for modeling properties of lambda terms and their types.
Properties of logic variables, unification with occurs-check and exploration of solution
spaces via backtracking facilitate compact algorithms for inferring types or generate terms
for various calculi. This holds in particular for lambda terms
While possibly one of the most heavily researched computational objects, lambda terms offer an endless stream of surprises to anyone digging just deep enough below their intriguingly simple surface.
This paper focuses on the synergy between combinatorial generation of lambda terms
and type inference, both favored by the use of Prolog as meta-language for representing
them. While we will take advantage of Prolog’s logic variables for type inference, we will
retain the “nameless” de Bruijn representation
Prolog’s ability to support “relational” queries enables us to easily explore the population of de Bruijn terms up to a given size and answer questions like the following: 1. How many distinct types occur for terms up to a given size? 2. What are the most popular types? 3. What are the terms that share a given type? 4. What is the smallest term that has a given type? 5. What smaller terms have the same type as this term?
The paper is organized as follows. Section 2 introduces the de Bruijn notation for lambda terms and describes a type inference algorithm working on them. Section 3 introduces a generator for lambda terms in de Bruijn form. Section 4 introduces an algorithm combining term generation and type inference. Section 5 uses our combined term generation and type inference algorithm to discover frequently occurring type patterns. Section 6 describes a type-directed algorithm for the generation of closed typable lambda terms. Section 7 discusses related work and section 8 concludes the paper.
The paper is structured as a literate Prolog program. The code, tested with SWI-Prolog 6.6.6 and YAP 6.3.4., is at http://www.cse.unt.edu/~tarau/research/2015/dbt.pro.
As lambda terms represent functions, inferring their types provides information on what
kind of argument(s) they can be applied to. For simple types, type inference is decidable
De Bruijn indices
For instance, the term l(A,a(l(B,a(A,a(B,B))),l(C,a(A,a(C,C))))) is represented as l(a(l(a(v(1),a(v(0),v(0)))),l(a(v(1),a(v(0),v(0)))))), given that v(1) is bound by the outermost lambda (two steps away, counting from 0) and the occurrences of v(0) are bound each by the closest lambda, represented by the constructor l/1.
One can define the size of a lambda expression in de Bruijn form as the number of its internal nodes, as implemented by the predicate dbTermSize. dbTermSize(v(_),0). isClosed(T):-isClosed1(T,0). isClosed1(v(N),D):-N<D. isClosed1(l(A),D):-D1 is D+1,
isClosed1(A,D1). isClosed1(a(X,Y),D):isClosed1(X,D), isClosed1(Y,D).
A lambda term is called closed if it contains no free variables. The predicate isClosed defines this property for de Bruijn terms.
Besides being closed, lambda terms interesting for functional languages and proof assistants, are also well-typed. We will start with an algorithm inferring types directly on the de Bruijn terms.
Simple types will be defined here also as binary trees built with the constructor “->/2” with
empty leaves, representing the unique primitive type “o”. Types can be seen as as a “binary
tree approximation” of lambda terms, centered around ensuring their safe and terminating
evaluation (strong normalization), as it is well-known (e.g.,
While in a functional language inferring types requires implementing unification with
occur check, as shown for instance in the appendix of
The predicate boundTypeOf/3 works by associating the same logical variable, denoting its type, to each of its occurrences. As a unique logic variable is associated to each leaf v/1 corresponding via its de Bruijn index to the same binder, types are consistently inferred. This is ensured by the use of the built-in nth0(I,Vs,V0) that unifies V0 with the I-th element of the type context Vs. Note that unification with occurs-check needs to be used to avoid cycles in the inferred type formulas. boundTypeOf(v(I),V,Vs):nth0(I,Vs,V0), unify_with_occurs_check(V,V0). boundTypeOf(a(A,B),Y,Vs):boundTypeOf(A,(X->Y),Vs), boundTypeOf(B,X,Vs). boundTypeOf(l(A),(X->Y),Vs):
boundTypeOf(A,Y,[X|Vs]).
At this point, most general types are inferred by boundTypeOf as fresh variables, similar to polymorphic types in functional languages, if one interprets logic variables as universally quantified.
Type inferred for the S combinator l x0: l x1: l x2:((x0 x2) (x1 x4)) in de Bruijn form. ?- X=l(l(l(a(a(v(2), v(0)), a(v(1), v(0)))))),boundTypeOf(X,T,0). X = l(l(l(a(a(v(2), v(0)), a(v(1), v(0)))))), T = ((A->B->C)-> (A->B)->A->C).
However, as we are only interested in simple types of closed terms with only one basic type, we will bind uniformly the leaves of our type tree to the constant “o” representing our only primitive type, by using the predicate bindType/1. boundTypeOf(A,T):-boundTypeOf(A,T0,[]),bindType(T0),!,T=T0. bindType(o):-!. bindType((A->B)):bindType(A), bindType(B).
Simple type inferred for the S combinator and failure to assign a type to the Y combinator l x0:( l x1:(x0 (x1 x2)) l x2:(x1 (x2 x2))). ?- boundTypeOf(l(l(l(a(a(v(2), v(0)), a(v(1), v(0)))))),T).
T = ((o-> (o->o))-> ((o->o)-> (o->o))). ?- boundTypeOf(l(a(l(a(v(1), a(v(0), v(0)))),
l(a(v(1), a(v(0), v(0)))))),T). false.
We can derive a generator for closed lambda terms in de Bruijn form by extending a Motzkin or unary-binary tree generator to keep track of the lambda binders. When reaching a leaf v/1, one of the available binders (expressed as a de Bruijn index) will be assigned to it nondeterministically.
The predicate genDBterm/4 generates closed de Bruijn terms with a fixed number of
internal (non-index) nodes, as counted by entry A220894 in
The range of possible indices is provided by Prolog’s built-in integer range generator between/3, that provides values from 0 to V0. Note also the use of down/2 abstracting away the predecessor operation and up/2 abstracting away the successor operation. Together, they control the amount of available nodes and the incrementing of de Bruijn indices at each lambda node.
Our generator of de Bruijn terms is exposed through two interfaces: genDBterm/2 that generates closed de Bruijn terms with exactly L non-index nodes and genDBterms/2 that generates terms with up to L non-index nodes, by not enforcing that exactly L internal nodes must be used. genDBterm(L,T):-genDBterm(T,0,L,0). genDBterms(L,T):-genDBterm(T,0,L,_).
Inserting a down operation in the first clause of genDBterm/4 will enumerate terms counted
by sequence A135501 instead of A220894, as this would imply assuming size 1 for
variables. in
Generation of terms with up to 2 internal nodes. ?- genDBterms(2,T).
T = l(v(0)) ; T = l(l(v(0))) ; T = l(l(v(1))) ; T = l(a(v(0), v(0))).
One could combine a generator for closed terms and a type inferrer in a “generate-and-test” style as follows: genTypedTerm1(L,Term,Type):genDBterm(L,Term), boundTypeOf(Term,Type).
Note that 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 efficient querying about what terms inhabit a given type, as one would expect from Prolog’s multi-directional execution model.
One can derive, from the type inferrer boundTypeOf, a more efficient generator for de Bruijn terms with a given number of internal nodes.
The predicate genTypedTerm/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 nth0 that enumerates values for both I and V ranging over the list of available variables Vs, as well as the use of unify with occurs check to ensure that unification of candidate types does not create cycles. genTypedTerm(v(I),V,Vs)--> { nth0(I,Vs,V0), unify_with_occurs_check(V,V0) }. genTypedTerm(a(A,B),Y,Vs)-->down, genTypedTerm(A,(X->Y),Vs), genTypedTerm(B,X,Vs). genTypedTerm(l(A),(X->Y),Vs)-->down,
genTypedTerm(A,Y,[X|Vs]). genTypedTerm(L,B,T):genTypedTerm(B,T,[],L,0), bindType(T). genTypedTerms(L,B,T):genTypedTerm(B,T,[],L,_), bindType(T).
Two interfaces are offered: genTypedTerm that generates de Bruijn terms of with exactly
L internal nodes and genTypedTerms that generates terms with L internal nodes or less.
As expected, the number of solutions, computed as the sequence 1, 2, 9, 40, 238, 1564,
11807, 98529, 904318, 9006364, 96709332, 1110858977 : : : for sizes 1; 2; 3; : : : ,12, : : :
matches entry A220471 in
Generation of well-typed closed de Bruijn terms of size 3. ?- genTypedTerm(3,Term,Type).
Term = a(l(v(0)), l(v(0))),Type = (o->o) ; Term = l(a(v(0), l(v(0)))),Type = (((o->o)->o)->o) ; Term = l(a(l(v(0)), v(0))),Type = (o->o) ; Term = l(a(l(v(1)), v(0))),Type = (o->o) ; Term = l(l(a(v(0), v(1)))),Type = (o-> ((o->o)->o)) ; Term = l(l(a(v(1), v(0)))),Type = ((o->o)-> (o->o)) ; Term = l(l(l(v(0)))),Type = (o-> (o-> (o->o))) ; Term = l(l(l(v(1)))),Type = (o-> (o-> (o->o))) ; Term = l(l(l(v(2)))),Type = (o-> (o-> (o->o))) . Size 1 2 3 4 5 6 7 8 9
Coming with Prolog’s unification and non-deterministic search, is the ability to make more specific queries by providing a type pattern, that selects only terms that match it, while generating terms and inferring their types.
The predicate queryTypedTerm finds closed terms of a given type of size exactly L. queryTypedTerm(L,QueryType,Term):genTypedTerm(L,Term,QueryType), boundTypeOf(Term,QueryType).
Similarly, the predicate queryTypedTerm finds closed terms of a given type of size L or less. queryTypedTerms(L,QueryType,Term):genTypedTerms(L,Term,QueryType), boundTypeOf(Term,QueryType).
Note that giving the query type ahead of executing genTypedTerm would unify with more general “false positives”, as type checking, contrary to type synthesis, proceeds bottom-up. This justifies filtering out the false positives simply by testing with the deterministic predicate boundTypeOf at the end. Despite the extra call to boundTypeOf, the performance improvements are significant, as shown in Figure 1. The figure also shows that when the slow generate-and-test predicate genTypedTerm1 is used, the result (in “logical-inferences-persecond”) does not depend on the pattern, contrary to the fast queryTypedTerm that prunes mismatching types while inferring the type of the terms as it generates them.
Terms of type o->o of size 4. ?- queryTypedTerm(3,(o->o),Term).
Term = a(l(v(0)), l(v(0))) ; Term = l(a(l(v(0)), v(0))) ; Term = l(a(l(v(1)), v(0))) . ?- queryTypedTerms(12,(o->o)->o,T). false.
Note that the last query, taking about a minute, shows that no closed terms of type (o->o)->o exist up to size 12. In fact, it is known that no such terms exist, as the corresponding logic formula is not a tautology in minimal logic.
Given a closed well-typed lambda term, we can ask what other terms of the same size or smaller share the same type. This can be interesting for finding possibly alternative implementations of a given function or for generation of similar siblings in genetic programming.
The predicate typeSiblingOf lists all the terms of the same or smaller size having the same type as a given term. typeSiblingOf(Term,Sibling):dbTermSize(Term,L), boundTypeOf(Term,Type), queryTypedTerms(L,Type,Sibling).
?- typeSiblingOf(l(l(a(v(0),a(v(0),v(1))))),T). T = l(l(a(v(0), v(1)))) ; % <= smaller sibling T = l(l(a(v(0), a(v(0), v(1))))) .
The ability to run “relational queries” about terms and their types extends to compute interesting statistics, giving a glimpse at their distribution.
As types can be seen as an approximation of their inhabitants, we expect them to be shared
among distinct terms. As we can enumerate all the terms for small sizes and infer their
types, we would like to know what are the most frequently occurring ones. This can be
meaningful as a comparison base for types that are used in human-written programs of
comparable size. In approaches like
Figure 2 describes counts for terms and their types for small sizes. It also shows the first two most frequent types with the count of terms they apply to.
Figure 3 shows the “most popular types” for the about 1 million closed well-typed terms up to size 9 and the count of their inhabitants.
We can observe that, like in some human-written programs, functions representing binary operations of type o->o->o are the most popular. Ternary operations o->o->o->o come third and unary operations o->o come fourth. Somewhat surprisingly, a higher order function type (o->o)->o->o applying a function to an argument to return a result comes second and multi-argument variants of it are also among the top 10. Term size 1 2 3 4 5 6 7 8 9
We can make use of our generator’s efficient specialization to a given type to explore empirical estimates for some types interesting to human programmers.
Contrary to the total absence of the type (o->o)->o among terms of size up to 12, “binary operations” of type o->(o->o) turn out to be quite frequent, giving, by increasing sizes, the sequence [0, 2, 0, 14, 12, 201, 445, 4632, 17789, 158271, 891635].
Transformers of type o->o, by increasing sizes, give the sequence [1, 0, 3, 3, 31, 78,
596, 2500, 18474, 110265]. While type (o->o)->o turns our to be absent up to size 12,
the type (o->o)->(o->o), describing transformers of transformers turns out to be quite
popular, as shown by the sequence [0, 0, 1, 1, 18, 52, 503, 2381, 19855, 125599]. The same
turns out to be true also for (o->o)->((o->o)->(o->o)), giving [0, 0, 0, 0, 2, 6, 96, 505,
5287, 36769] and ((o->o)->(o->o)) -> ((o->o)->(o->o)) giving [0, 0, 0, 0, 0, 6,
23, 432, 2450, 29924]. One might speculate that homotopy type theory
Another interface, generating closed simply-typed terms of a given size, restricted to have at most a given number of free de Bruijn indices, is implemented by the predicate genTypedWithSomeFree. genTypedWithSomeFree(Size,NbFree,B,T):between(0,NbFree,NbVs), length(FreeVs,NbVs), genTypedTerm(B,T,FreeVs,Size,0), bindType(T).
The first 9 numbers counting closed simply-typed terms with at most one free variable (not
yet in
Note that, as our generator performs the early pruning of untypable terms, rather than as a post-processing step, enumeration and counting of these terms happens in a few seconds.
In
We can organize in a similar way the interface of our combined generator and type inferrer.
The predicate genType generates binary trees representing simple types with a single base type ``o''.
It provides two interfaces, for generating types of exactly size N or up to size N. genType(o)-->[]. genType((X->Y))-->down, genType(X), genType(Y). genType(N,X):-genType(X,N,0). genTypes(N,X):-genType(X,N,_).
Type trees with up to 2 internal nodes (and up to 4 leaves). ?- genTypes(3,T). ?- genTypes(2,T).
T = o ; T = (o->o) ; T = (o->o->o) ; T = ((o->o)->o) .
Next, we will combine this type generator with the generator that efficiently produces terms matching each type pattern.
The predicate genByType first generates types (seen simply as binary trees) with genType and then uses the unification-based querying mechanism to generate all closed well-typed de Bruijn terms with fewer internal nodes then their binary tree type. genByType(L,B,T):genType(L,T), queryTypedTerms(L,T,B).
Enumeration of closed simply-typed de Bruijn terms with types of size 3 and terms of a given type with at most 3 internal nodes. ?- genByType(3,B,T).
B = l(l(l(v(0)))),T = (o->o->o->o) ; B = l(l(l(v(1)))),T = (o->o->o->o) ; B = l(l(l(v(2)))),T = (o->o->o->o) ; B = l(l(a(v(0), v(1)))),T = (o-> (o->o)->o) ; B = l(l(a(v(1), v(0)))),T = ((o->o)->o->o) ; B = l(a(v(0), l(v(0)))),T = (((o->o)->o)->o) .
Given that various constraints are naturally interleaved by our generator we obtain in a few seconds the sequence counting these terms having types up to size 8, [1, 2, 6, 18, 84, 376, 2344, 15327]. Intuitively this means that despite of their growing sizes, types have an increasingly large number of inhabitants of sizes smaller than their size. This is somewhat contrary to what we see in human-written code, where types are almost always simpler and smaller than the programs inhabiting them.
The classic reference for lambda calculus is
Originally introduced in
Combinatorics of lambda terms, including enumeration, random generation and
asymptotic behavior has seen an increased interest recently (see for instance
Of particular interest are the results of
We have described Prolog-based term and type generation and as well as type-inference algorithms for de Bruijn terms. Among the possible applications of our techniques we mention compilation and test generation for lambda-calculus based languages and proof assistants.
By taking advantage of Prolog’s unique bidirectional execution model and unification algorithm (including support for cyclic terms and occurs-check), we have merged generation and type inference in an algorithm that can build “customized closed terms of a given type”. This “relational view” of terms and their types has enabled the discovery of interesting patterns about the type expressions occurring in well-typed programs. We have uncovered the most “popular” types that govern function applications among a about a million small-sized lambda terms.
The paper has also introduced a number of algorithms that, at our best knowledge, are novel, at least in terms of their logic programming implementation, among which we mention the type inference for de Bruijn terms using unification with occurs-check in subsection 2.2 and the integrated generation and type inference algorithm for closed simply typed de Bruijn terms in section 4. Besides the ability to efficiently query for inhabitants of specific types, our algorithms also support a from of “query-by-example” mechanism, for finding (possibly smaller) terms inhabiting the same type as the query term.
We have also observed some interesting phenomena about frequently occurring types, that seem to be similar to those in human-written programs and we have computed growth sequences for the number of inhabitants of some “popular” types, for which we have not found any study in the literature.
While a non-strict functional language like Haskell could have been used for deriving similar algorithms, the synergy between Prolog’s non-determinism, DCG transformation and the availability of unification with occurs-check made the code embedded in the paper significantly simpler and arguably clearer.
This research has been supported by NSF grant 1423324.