Abstract We investigate the asymptotic densities of theorems provable in Zermelo–Fraenkel set theory zf and its extension zfc including the axiom of choice. Assuming a canonical De Bruijn representation of formulae, we construct asymptotically large sets of sentences unprovable within zf, yet provable in zfc. Furthermore, we link the asymptotic density of zfc theorems with the provable consistency of zfc itself. Consequently, if zfc is consistent, it is not possible to refute the existence of the asymptotic density of zfc theorems within zfc. Both these results address a recent question by Zaionc regarding the asymptotic equivalence of zf and zfc.

λν is an extension of the λ-calculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of λν focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for λν-terms and famous Catalan numbers. As a by-product, we establish effective sampling schemes for random λν-terms. We show that typical λν-terms represent, in a strong sense, non-strict computations in the classic X-calculus. Moreover, typically almost all substitutions are in fact suspended, i.e. unevaluated, under closures. Consequently, we argue that λν is an intrinsically non-strict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in λν and investigate the quantitative contribution of various substitution primitives.

Abstract A natural approach to software quality assurance consists in writing unit tests securing programmer-declared code invariants. Throughout the literature, a great body of work has been devoted to tools and techniques automating this labour-intensive process. A prominent example is the successful use of randomness, in particular, random typable λ-terms, in testing functional programming compilers such as the Glasgow Haskell Compiler. Unfortunately, due to the intrinsically difficult combinatorial structure of typable λ-terms, no effective uniform sampling method is known, setting it as a fundamental open problem in the random software testing approach. In this paper, we combine the framework of Boltzmann samplers, a powerful technique of random combinatorial structure generation, with today's Prolog systems offering a synergy between logic variables, unification with occurs check and efficient backtracking. This allows us to develop a novel sampling mechanism able to construct uniformly random closed simply typed λ-terms of up size 120. We apply our techniques to the generation of uniformly random closed simply typed normal forms and design a parallel execution mechanism pushing forward the achievable term size to 140.

Abstract We present an algorithm which, for given n , generates an unambiguous regular tree grammar defining the set of combinatory logic terms, over the set {S, K} of primitive combinators, requiring exactly n normal-order reduction steps to normalize. As a consequence of Curry and Feys's standardization theorem, our reduction grammars form a complete syntactic characterization of normalizing combinatory logic terms. Using them, we provide a recursive method of constructing ordinary generating functions counting the number of SK -combinators reducing in n normal-order reduction steps. Finally, we investigate the size of generated grammars giving a primitive recursive upper bound.

We consider combinatorial aspects of |$\lambda$|-terms in the model based on de Bruijn indices where each building constructor is of size one. Surprisingly, the counting sequence for |$\lambda$|-terms corresponds also to two families of binary trees, namely black-white trees and zigzag-free ones. We provide a constructive proof of this fact by exhibiting appropriate bijections. Moreover, we identify the sequence of Motzkin numbers with the counting sequence for neutral |$\lambda$|-terms, giving a bijection which, in consequence, results in an exact-size sampler for the latter based on the exact-size sampler for Motzkin trees of Bodini et alli. Using the powerful theory of analytic combinatorics, we state several results concerning the asymptotic growth rate of |$\lambda$|-terms in neutral, normal, and head normal forms. Finally, we investigate the asymptotic density of |$\lambda$|-terms containing arbitrary fixed subterms showing that, inter alia, strongly normalising or typeable terms are asymptotically negligible in the set of all |$\lambda$|-terms.

We present a quantitative basis-independent analysis of combinatory logic. Using a general argument regarding plane binary trees with labelled leaves, we generalize the results of David et al. (see [11]) and Bendkowski et al. (see [6]) to all Turing-complete combinator bases proving, inter alia, that asymptotically almost no combinator is strongly normalizing nor typeable. We exploit the structure of recently discovered normal-order reduction grammars (see [3]) showing that for each positive |$n$|⁠, the set of |$\mathbf{S} \mathbf{K}$|-combinators reducing in |$n$| normal-order reduction steps has positive asymptotic density in the set of all combinators. Our approach is constructive, allowing us to systematically find new asymptotically significant fractions of the set of normalizing combinators. We show that the density of normalizing combinators cannot be less than |$34\%$|⁠, improving the previously best lower bound of approximately |$3\%$| (see [6]). Finally, we present some super-computer experimental results, conjecturing that the density of the set of normalizing combinators is close to |$85\%$|⁠.