Technical Communications of ICLP 2015. Copyright with the Authors. 1 On Type-directed Generation of Lambda Terms PAUL TARAU Department of Computer Science and Engineering (e-mail: tarau@cs.unt.edu) submitted April 29, 2015; accepted June 5, 2015 Abstract 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. KEYWORDS: lambda calculus, de Bruijn notation, type inference, generation of lambda terms, logic programming as a meta-language. 1 Introduction 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 (Barendregt 1984). Lambda terms provide a foundation to modern functional languages, type theory and proof assis- tants and have been lately incorporated into mainstream programming languages including Java 8, C# and Apple’s Swift. 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 in- triguingly 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 (de Bruijn 1972) for term generation as it provides a canonical representation to α-equivalent terms. We will also focus on closed terms (terms without free variables) as they are the ones used in lambda calculus based programming languages like Haskell and ML or proof assistants like Coq or Agda. 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: 2 Paul Tarau 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. 2 Type inference for lambda terms in de Bruijn notation 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 (Hindley and Seldin 2008) and it uses unification to recursively propagate type information between application sites of variable occurrences covered by a given lambda binder. We will describe next a type inference algorithm using de Bruijn indices in Prolog - a somewhat unusual choice, given that logic variables can play the role of lambda binders directly. One of the reasons we chose them is that they will be simpler to manipulate at meta-language level, as they handle object-level variables implicitly. At the same time this might be useful for other purposes, as we are not aware of any Prolog implementation of type inference with this representation of lambda terms. 2.1 De Bruijn Indices De Bruijn indices (de Bruijn 1972) provide a name-free representation of lambda terms. All closed terms that can be transformed by a renaming of variables (α-conversion) will share a unique representation. Variables following lambda abstractions are omitted and their occurrences are marked with positive integers counting the number of lambdas until the one binding them is found on the way up to the root of the term. We represent them using the constructor a/2 for application, l/1 for lambda abstractions (that we will call shortly binders) and v/1 for marking the integers corresponding to the 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 repre- sented 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 occur- rences 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). On Type-directed Generation of Lambda Terms 3 dbTermSize(l(A),R):- dbTermSize(A,RA), R is RA+1. dbTermSize(a(A,B),R):- dbTermSize(A,RA), dbTermSize(B,RB), R is 1+RA+RB. A lambda term is called closed if it contains no free variables. The predicate isClosed defines this property for de Bruijn terms. isClosed(T):-isClosed1(T,0). isClosed1(v(N),D):-N/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., (Barendregt 1991)) that lambda terms that have simple types are strongly normalizing. When a term X has a type T we say that the type T is inhabited by the term X. While in a functional language inferring types requires implementing unification with occur check, as shown for instance in the appendix of (Grygiel and Lescanne 2013), this is readily available in Prolog. 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]). 4 Paul Tarau 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 univer- sally quantified. Example 1 Type inferred for the S combinator λ x0 . λ x1 . λ 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). Example 2 Simple type inferred for the S combinator and failure to assign a type to the Y combinator λ x0 .( λ x1 .(x0 (x1 x2 )) λ 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. 3 Deriving a generator for lambda terms in de Bruijn form 3.1 Generation of de Bruijn terms 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 (Sloane 2014). genDBterm(v(X),V)--> {down(V,V0)}, {between(0,V0,X)}. genDBterm(l(A),V)-->down, {up(V,NewV)}, genDBterm(A,NewV). genDBterm(a(A,B),V)-->down, genDBterm(A,V), genDBterm(B,V). On Type-directed Generation of Lambda Terms 5 down(From,To):-From>0,To is From-1. up(K1,K2):-K2 is K1+1. 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 abstract- ing 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 vari- ables. in (Sloane 2014). Example 3 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))). 4 Combining term generation and type inference 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. 4.1 Generating closed well-typed terms of a given size 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 6 Paul Tarau 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]). 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. genTypedTerm(L,B,T):- genTypedTerm(B,T,[],L,0), bindType(T). genTypedTerms(L,B,T):- genTypedTerm(B,T,[],L,_), bindType(T). 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 (Sloane 2014). Note that the last 2 terms are not (yet) in the A220471 in (Sloane 2014) as the generate and filter method used in (Grygiel and Lescanne 2013) is limited by the super-exponential growth of the closed lambda terms among which the relatively few well-typed ones need to be found (e.g. more than 12 billion terms for size 12). Interestingly, by interleaving generation of closed terms and type inference in the predicate genTypedTerm the time to generate all the well-typed terms is actually shorter than the time to generate all closed terms of the same size, e.g.. 3.2 vs 4.3 seconds for size 9 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. Example 4 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))) . On Type-directed Generation of Lambda Terms 7 Size Slow o->o Slow o->o->o Fast o->o Fast o->o->o Fast o 1 39 39 38 27 15 2 126 126 60 109 36 3 552 552 240 200 88 4 3,108 3,108 634 1,063 290 5 21,840 21,840 3,213 3,001 1,039 6 181,566 181,566 12,721 19,598 4,762 7 1,724,131 1,724,131 76,473 81,290 23,142 8 18,307,585 18,307,585 407,639 584,226 133,554 9 213,940,146 213,940,146 2,809,853 3,254,363 812,730 Fig. 1. Number of logical inferences as counted by SWI-Prolog for our algorithms when querying generators with type patterns given in advance 4.2 Querying the generator for specific types 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 predi- cate boundTypeOf at the end. Despite the extra call to boundTypeOf, the performance im- provements 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-per- second”) 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. Example 5 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 8 Paul Tarau 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. 4.3 Same-type siblings 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 imple- mentations 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). Example 6 ?- 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))))) . 5 Discovering frequently occurring type patterns The ability to run “relational queries” about terms and their types extends to compute interesting statistics, giving a glimpse at their distribution. 5.1 The “Popular” type patterns 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 (Palka et al. 2011), where types are used to direct the generation of random terms, focusing on the most frequent types might help with genera- tion of more realistic random tests. 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 bi- nary 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. On Type-directed Generation of Lambda Terms 9 Term size Types Terms Ratio 1-st frequent 2-nd frequent 1 1 1 1.0 1: o->o 2 1 2 0.5 2: o->o->o 3 5 9 0.555 3: o->o->o->o 3: o->o 4 16 40 0.4 14: o->o->o 4: o->o->o->o->o 5 55 238 0.231 38: o->o->o->o 31: o->o 6 235 1564 0.150 201: o->o->o 80: o->o->o->o->o 7 1102 11807 0.093 732: o->o->o->o 596: o->o 8 5757 98529 0.058 4632: o->o->o 2500: o->o 9 33251 904318 0.036 20214: o->o->o->o 19855: (o->o)->o->o Fig. 2. Counts for terms and types for sizes 1 to 9 and the first two most frequent types Count Type 23095 o->o->o 22811 (o->o)->o->o 22514 o->o->o->o 21686 o->o 18271 o-> (o->o)->o 14159 (o->o)->o->o->o 13254 ((o->o)->o)-> (o->o)->o 12921 o-> (o->o)->o->o 11541 (o->o)-> ((o->o)->o)->o 10919 (o->o->o)->o->o->o Fig. 3. Most frequent types, out of a total of 33972 distinct types, of 1016508 terms up to size 9. 5.2 Growth sequences of some popular types 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 (The Univalent Foundations Program 2013), that focuses on such transformations and transformations of transformations etc. has a rich population of lambda terms from which to chose interesting inhabitants of such types! 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):- 10 Paul Tarau 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 (Sloane 2014)), are [3, 10, 45, 256, 1688, 12671, 105743, 969032, 9639606]. 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. 6 Generating closed typable lambda terms by types In (Palka et al. 2011) a “type-directed” mechanism for the generation of random terms is introduced, resulting in more realistic (while not uniformly random) terms, used success- fully in discovering some GHC bugs. We can organize in a similar way the interface of our combined generator and type inferrer. 6.1 Generating type trees The predicate genType generates binary trees representing simple types with a single base type ‘‘o’’. genType(o)-->[]. genType((X->Y))-->down, genType(X), genType(Y). It provides two interfaces, for generating types of exactly size N or up to size N. genType(N,X):-genType(X,N,0). genTypes(N,X):-genType(X,N,_). Example 7 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. 6.2 Generating lambda terms by increasing type sizes 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. On Type-directed Generation of Lambda Terms 11 genByType(L,B,T):- genType(L,T), queryTypedTerms(L,T,B). Example 8 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. 7 Related work The classic reference for lambda calculus is (Barendregt 1984). Various instances of typed lambda calculi are overviewed in (Barendregt 1991). Originally introduced in (de Bruijn 1972), the de Bruijn notation makes terms equivalent up to α-conversion and facilitates their normalization (Kamareddine 2001). Combinatorics of lambda terms, including enumeration, random generation and asymp- totic behavior has seen an increased interest recently (see for instance (David et al. 2009; Bodini et al. 2011; Grygiel and Lescanne 2013; David et al. 2010; Grygiel et al. 2013)), partly motivated by applications to software testing, given the widespread use of lambda terms as an intermediate language in compilers for functional languages and proof assis- tants. In (Palka et al. 2011; Fetscher et al. 2015), types are used to generate random terms for software testing. The same naturally “goal-oriented” effect is obtained in the generator/- type inferrer for de Bruijn terms in subsection 4.2, by taking advantage of Prolog’s ability to backtrack over possible terms, while filtering against unification with a specific pattern. In (Tarau 2015b) generation algorithms for several sub-families of lambda terms are given as well as a compressed deBruijn representation is introduced. In (Tarau 2015a) Rosser’s X-combinator trees (Fokker 1992) are used as a uniform representation via bijections top lambda terms in de Bruijn notation, types and a tree-based number representation. Of particular interest are the results of (Grygiel and Lescanne 2013) where recurrence relations and asymptotic behavior are studied for several families of lambda terms. Em- pirical evaluation of the density of closed simply-typed general lambda terms described in (Grygiel and Lescanne 2013) indicates extreme sparsity for large sizes. However, the problem of their exact asymptotic behavior is still open. 12 Paul Tarau 8 Conclusions 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 gen- eration 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 men- tion the type inference for de Bruijn terms using unification with occurs-check in sub- section 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. Acknowledgement This research has been supported by NSF grant 1423324. On Type-directed Generation of Lambda Terms 13 References BARENDREGT, H. P. 1984. The Lambda Calculus Its Syntax and Semantics, Revised ed. Vol. 103. North Holland. BARENDREGT, H. P. 1991. Lambda calculi with types. In Handbook of Logic in Computer Science. Vol. 2. Oxford University Press. B ODINI , O., G ARDY, D., AND G ITTENBERGER , B. 2011. Lambda-terms of bounded unary height. In ANALCO. SIAM, 23–32. DAVID , R., G RYGIEL , K., KOZIK , J., R AFFALLI , C., T HEYSSIER , G., AND Z AIONC , M. 2010. Asymptotically almost all λ -terms are strongly normalizing. Preprint: arXiv: math. LO/0903.5505 v3. DAVID , R., R AFFALLI , C., T HEYSSIER , G., G RYGIEL , K., KOZIK , J., AND Z AIONC , M. 2009. Some properties of random lambda terms. Logical Methods in Computer Science 9, 1. DE B RUIJN , N. G. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indagationes Mathemati- cae 34, 381–392. F ETSCHER , B., C LAESSEN , K., PALKA , M. H., H UGHES , J., AND F INDLER , R. B. 2015. Mak- ing random judgments: Automatically generating well-typed terms from the definition of a type- system. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 383–405. F OKKER , J. 1992. The systematic construction of a one-combinator basis for lambda-terms. Formal Aspects of Computing 4, 776–780. G RYGIEL , K., I DZIAK , P. M., AND Z AIONC , M. 2013. How big is BCI fragment of BCK logic. J. Log. Comput. 23, 3, 673–691. G RYGIEL , K. AND L ESCANNE , P. 2013. Counting and generating lambda terms. J. Funct. Pro- gram. 23, 5, 594–628. H INDLEY, J. R. AND S ELDIN , J. P. 2008. Lambda-calculus and combinators: an introduction. Vol. 13. Cambridge University Press Cambridge. K AMAREDDINE , F. 2001. Reviewing the Classical and the de Bruijn Notation for calculus and Pure Type Systems. Journal of Logic and Computation 11, 3, 363–394. PALKA , M. H., C LAESSEN , K., RUSSO , A., AND H UGHES , J. 2011. Testing an optimising com- piler by generating random lambda terms. In Proceedings of the 6th International Workshop on Automation of Software Test. AST’11. ACM, New York, NY, USA, 91–97. S LOANE , N. J. A. 2014. The On-Line Encyclopedia of Integer Sequences. Published electronically at https://oeis.org/. TARAU , P. 2015a. On a Uniform Representation of Combinators, Arithmetic, Lambda Terms and Types. In PPDP’15: Proceedings of the 17th international ACM SIGPLAN Symposium on Prin- ciples and Practice of Declarative Programming, E. Albert, Ed. ACM, New York, NY, USA, 244–255. TARAU , P. 2015b. On Logic Programming Representations of Lambda Terms: de Bruijn Indices, Compression, Type Inference, Combinatorial Generation, Normalization. In Proceedings of the Seventeenth International Symposium on Practical Aspects of Declarative Languages PADL’15, E. Pontelli and T. C. Son, Eds. Springer, LNCS 8131, Portland, Oregon, USA, 115–131. T HE U NIVALENT F OUNDATIONS P ROGRAM. 2013. Homotopy Type Theory. Institute of Advanced Studies, Princeton. http://homotopytypetheory.org/2013/06/20/the-hott-book/.