Pierre Lescanne

TCS Journal 2013 Journal Article

On counting untyped lambda terms

• Pierre Lescanne

Despite λ -calculus is now three quarters of a century old, no formula counting λ -terms has been proposed yet, and the combinatorics of λ -calculus is considered a hard problem. The difficulty lies in the fact that the recursive expression of the numbers of terms of size n with at most m free variables contains the number of terms of size n − 1 with at most m + 1 variables. This leads to complex recurrences that cannot be handled by classical analytic methods. Here based on de Bruijn indices (another presentation of λ -calculus) we propose several results on counting untyped lambda terms, i. e. , on telling how many terms belong to such or such class, according to the size of the terms and/or to the number of free variables. We extend the results to normal forms.

TCS Journal 2008 Journal Article

Characterizing strong normalization in the Curien–Herbelin symmetric lambda calculus: Extending the Coppo–Dezani heritage

• Daniel J. Dougherty
• Silvia Ghilezan
• Pierre Lescanne

We develop an intersection type system for the λ ¯ μ μ ˜ calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves upon earlier type disciplines for λ ¯ μ μ ˜: in addition to characterizing the λ ¯ μ μ ˜ expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.

LPAR Conference 2005 Conference Paper

Strong Normalization of the Dual Classical Sequent Calculus

• Daniel J. Dougherty
• Silvia Ghilezan
• Pierre Lescanne
• Silvia Likavec

Abstract We investigate some syntactic properties of Wadler’s dual calculus, a term calculus which corresponds to classical sequent logic in the same way that Parigot’s λμ calculus corresponds to classical natural deduction. Our main result is strong normalization theorem for reduction in the dual calculus; we also prove some confluence results for the typed and untyped versions of the system.

I&C Journal 2004 Journal Article

Intersection types for explicit substitutions

• Stéphane Lengrand
• Pierre Lescanne
• Dan Dougherty
• Mariangiola Dezani-Ciancaglini
• Steffen van Bakel

We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are strongly normalizing. This system extends previous work on the natural generalization of the classical intersection types system, which characterized head normalization and weak normalization, but was not complete for strong normalization. An important role is played by the notion of available variable in a term, which is a generalization of the classical notion of free variable.

TCS Journal 1996 Journal Article

Valentin Antimirov (1961–1995)

• Gregory Kucherov
• Pierre Lescanne
• Peter Mosses

TCS Journal 1994 Journal Article

On termination of one rule rewrite systems

• Pierre Lescanne

The undecidability of the termination of rewrite systems is usually proved by reduction to the halting of Turing machines. In particular, Dauchet proves the undecidability of the termination of one rule rewrite systems by coding Turing machines into one rule rewrite systems. Rewrite systems are a very simple model of computation and one may expect proofs in this model to be more straightforward than those referring to the more complex model of Turing machines. In this paper we deduce the problem of termination of one rule rewrite systems to problems somewhat more related to rewrite systems namely to Post correspondence problems and to termination of semi-Thue systems. Proofs we obtain this way are shorter and we expect other interesting applications from these codings. In particular, the second part proposes a simulation of semi-Thue systems by one rule systems.

MFCS Conference 1991 Invited Paper

Rewrite Orderings and Termination of Rewrite Systems

• Pierre Lescanne

I&C Journal 1990 Journal Article

Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems

• Max Dauchet
• Thierry Heuillard
• Pierre Lescanne
• Sophie Tison

The aim of this paper is to propose an algorithm to decide the confluence of finite ground term rewrite systems. Actually a more general class of possibly infinite ground term rewrite systems is studied. It is well known that the confluence is not decidable for general term rewrite systems, but this paper proves it is for ground term rewrite systems following a conjecture made by Huet and Oppen in their survey. The result is also applied to the confluence of left-linear and right-ground term rewrite systems. We also sketch an algorithm for checking this property. This algorithm is based on tree automata and tree transducers. Here, we regard them as rewrite systems and specialists in automata theory would translate that easily in their language.

I&C Journal 1990 Journal Article

Tools for proving inductive equalities, relative completeness, and ω-completeness

• Azeddine Lazrek
• Pierre Lescanne
• Jean-Jacques Thiel

Inductive theorems are properties valid in the initial algebra. A now popular tool for proving them in equational theories or abstract data types is based on proof by consistency. This method uses a completion procedure and requires two essential properties of the specification, namely relative completeness and ω-completeness. This paper investigates ways of proving them. For the first one, the complement algorithm is presented. It is based on unification and computation of coverings and complements. For the second one, a technique based on discrimination of pairs of normal forms is explained and illustrated through examples.

TCS Journal 1989 Journal Article

Editorial

• Pierre Lescanne