Author name cluster

Laurent Regnier

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

TCS Journal 2008 Journal Article

Uniformity and the Taylor expansion of ordinary lambda-terms

Thomas Ehrhard
Laurent Regnier

We define the complete Taylor expansion of an ordinary lambda-term as an infinite linear combination–with rational coefficients–of terms of a resource calculus similar to Boudol’s lambda-calculus with multiplicities (or with resources). In our resource calculus, all applications are (multi)linear in the algebraic sense, i. e. commute with linear combinations of the function or the argument. We study the collective behaviour of the beta-reducts of the terms occurring in the Taylor expansion of any ordinary lambda-term, using, in a surprisingly crucial way, a uniformity property that they enjoy. As a corollary, we obtain (the main part of) a proof that this Taylor expansion commutes with Böhm tree computation, syntactically.

Details DOI

TCS Journal 2003 Journal Article

The differential lambda-calculus

Thomas Ehrhard
Laurent Regnier

We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus.

Details DOI

TCS Journal 1999 Journal Article

Reversible, irreversible and optimal λ-machines

Vincent Danos
Laurent Regnier

Lambda-calculus is the core of functional programming, and many different ways to evaluate lambda-terms have been considered. One of the nicest, from the theoretical point of view, is head linear reduction. We compare two ways of implementing that specific evaluation strategy: “Krivine's abstract machine” and the “interaction abstract machine”. Runs on those machines stand in a relation which can be accurately described using the call/return symmetry discovered by Asperti and Laneve.

Details DOI

CSL Conference 1998 Conference Paper

Timeless Games

Patrick Baillot
Vincent Danos
Thomas Ehrhard
Laurent Regnier

Abstract Two models of classical linear logic are set up. First our recent version of AJM games model which will be our source model. Then the target model, polarized pointed relations, a variant of the plain relational model which is constructed in two steps: first the model of pointed relations, then the additional polarization structure which yields a proper duality. Then the natural time-forgetting map is shown to generate a lax functor from the source to the target. Finally a further refinement of the target model using bipolarities is sketched, giving a closer link with the games model for the interpretation of syntax. Thus a bridge is constructed that goes from a dynamic model to a static model of evaluation.

Details

CSL Conference 1997 Conference Paper

Directed Virtual Reductions

Vincent Danos
Marco Pedicini
Laurent Regnier

Abstract This note defines a new graphical local calculus, directed virtual reductions. It is designed to compute Girard's execution formula EX, an invariant of closed functional evaluation obtained from the “geometry of interaction” interpretation of λ-calculus [5]. The calculus is obtained by synchronizing another graphical local calculus presented in “local and asynchronous beta-reduction”: virtual reductions [4]. This synchronization makes it easier to mechanize than general virtual reductions. In undirected virtual reductions the consistency of the computation is insured by an algebraic mechanism called the bar. This mechanism in general induces correction terms of any order. The directed virtual reduction has been designed to keep those terms at order one. A further synchronization, the combustion strategy will even wipe out first order correction terms. Applied to sharing graphs, the combustion strategy yields Lamping's optimal graphical calculus as presented in [1]. But more efficient optimal implementations of λ-calculus are expected. The paper is conceived as a follow-up of [4] and supposes a familiarity with virtual reduction.

Details

TCS Journal 1994 Journal Article

Une équivalence sur les lambda- termes

Laurent Regnier

Dans ce papier on définit une relation d'équivalence sur les lambda-termes, identifiant les termes qui ne diffèrent que par des permutations de radicaux: la σ-équivalence. On démontre qu'aucun des critères opérationnels standards de classification du lambda-calcul (e. g. la longueur de la plus longue normalisation) ne permet de distinguer deux termes σ-équivalents. Enfin, la σ-équivalence est utilisée pour démontrer une généralisation du théorème de la stratégie perpétuelle. In this paper an equivalence relation between lambda-terms is defined which identifies terms only differing by permutation of radices: the σ-equivalence. It is shown that none of the standard operational classification criteria on lambda-calculus (e. g. the length of the longest reduction) can separate two σ-equivalent terms. Finally, the σ-equivalence is used for proving a generalisation of the perpetual strategy theorem.

Details DOI