Searcharxiv⌕ Search

arXiv subjects

René David

Publications and source records attributed to René David.

13 recordsLinked to original sources
arXiv2014

About the range property for H

Recently, A. Polonsky has shown that the range property fails for H. We give here some conditions on a closed term that imply that its range has an infinite cardinality.

math.LO↗
arXiv2013

Asymptotically almost all λ-terms are strongly normalizing

We present quantitative analysis of various (syntactic and behavioral) properties of random λ-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term. Surprisingly, in combinatory logic (the translation of the λ-calculus into combinators), the result is exactly opposite. We show that almost all terms are not strongly normalizing. This is due to the fact that any fixed combinator almost always appears in a random combinator.

math.LO↗
arXiv2009

Strong normalization results by translation

We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system.

math.LO↗
arXiv2009

Counting proofs in propositional logic

We give a procedure for counting the number of different proofs of a formula in various sorts of propositional logic. This number is either an integer (that may be 0 if the formula is not provable) or infinite.

math.LO↗
arXiv2009

An arithmetical proof of the strong normalization for the $λ$-calculus with recursive equations on types

We give an arithmetical proof of the strong normalization of the $λ$-calculus (and also of the $λμ$-calculus) where the type system is the one of simple types with recursive equations on types. The proof using candidates of reducibility is an easy extension of the one without equations but this proof cannot be formalized in Peano arithmetic. The strength of the system needed for such a proof was not known. Our proof shows that it is not more than Peano arithmetic.

math.LO↗
arXiv2009

Arithmetical proofs of strong normalization results for the symmetric $λμ$-calculus

The symmetric $λμ$-calculus is the $λμ$-calculus introduced by Parigot in which the reduction rule $\m'$, which is the symmetric of $μ$, is added. We give arithmetical proofs of some strong normalization results for this calculus. We show (this is a new result) that the $μμ'$-reduction is strongly normalizing for the un-typed calculus. We also show the strong normalization of the $βμμ'$-reduction for the typed calculus: this was already known but the previous proofs use candidates of reducibility where the interpretation of a type was defined as the fix point of some increasing operator and thus, were highly non arithmetical.

math.LO↗
arXiv2009

Arithmetical proofs of strong normalization results for symmetric lambda calculi

We give arithmetical proofs of the strong normalization of two symmetric $λ$-calculi corresponding to classical logic. The first one is the $\barλμ\tildeμ$-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric $λμ$-calculus. It is the $λμ$-calculus introduced by Parigot in which the reduction rule $μ'$, which is the symmetric of $μ$, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.

math.LO↗