Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA natural counting of lambda terms
212
0
0.0
(
0
)
Added by
Pierre Lescanne
Publication date
2015
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We study the sequences of numbers corresponding to lambda terms of given sizes, where the size is this of lambda terms with de Bruijn indices in a very natural model where all the operators have size 1. For plain lambda terms, the sequence corresponds to two families of binary trees for which we exhibit bijections. We study also the distribution of normal forms, head normal forms and strongly normalizing terms. In particular we show that strongly normalizing terms are of density 0 among plain terms.
rate research
Read More
In a paper entitled Binary lambda calculus and combinatory logic, John Tromp presents a simple way of encoding lambda calculus terms as binary sequences. In what follows, we study the numbers of binary strings of a given size that represent lambda terms and derive results from their generating functions, especially that the number of terms of size n grows roughly like 1.963447954. .. n. In a second part we use this approach to generate random lambda terms using Boltzmann samplers.
We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagners counting hierarchy, but also that the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science.
We provide a characterisation of strongly normalising terms of the lambda-mu-calculus by means of a type system that uses intersection and product types. The presence of the latter and a restricted use of the type omega enable us to represent the particular notion of continuation used in the literature for the definition of semantics for the lambda-mu-calculus. This makes it possible to lift the well-known characterisation property for strongly-normalising lambda-terms - that uses intersection types - to the lambda-mu-calculus. From this result an alternative proof of strong normalisation for terms typeable in Parigots propositional logical system follows, by means of an interpretation of that system into ours.
Affine $lambda$-terms are $lambda$-terms in which each bound variable occurs at most once and linear $lambda$-terms are $lambda$-terms in which each bound variables occurs once. and only once. In this paper we count the number of closed affine $lambda$-terms of size $n$, closed linear $lambda$-terms of size $n$, affine $beta$-normal forms of size $n$ and linear $beta$-normal forms of ise $n$, for different ways of measuring the size of $lambda$-terms. From these formulas, we show how we can derive programs for generating all the terms of size $n$ for each class. For this we use a specific data structure, which are contexts taking into account all the holes at levels of abstractions.
In this note we describe a new method of counting the number of unordered factorizations of a natural number by means of a generating function and a recurrence relation arising from it, which improves an earlier result in this direction.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
