λ-calcul différentiel et logique classique : interactions calculatoires
Lionel Vaux · HAL (Le Centre pour la Communication Scientifique Directe) · 2007
We study the possible interactions between Ehrhard-Regnier's differential λ-calculus and pure calculi associated with classical logic : Parigot's λµ-calculus and Herbelin's λ-bar-µ-calculus. The impetus to this study is given by the respective decompositions of these calculi in particular extensions of Girard's linear logic. We first provide a unified framework for these extensions, as a variant of Lafont's interaction nets. We recall well known definitions and results, either from litterature or from folklore, rephrased in this setting : in particular, we explicit translations of λµ-calculus and λ-bar-µ-calculus into Laurent's polarized proof nets and a translation of the finitary fragment of differential λ-calculus into Ehrhard-Regnier's differential interaction nets. In a second part, we introduce polarized differential nets (PDN) : these are obtained as an extension of differential nets by a polarization scheme à la Laurent. The new reduction rules are justified by the properties of a denotational model of both polarized nets and differential nets. Last we proceed to the introduction of three pure term calculi, each corresponding to a readback from the dynamics of PDN, through a Curry-Howard-Girard decomposition : a differential λµ-calculus, which accounts for the union of polarized nets and interaction nets; an extension of λ-bar-µ-calculus involving a convolution product on stacks, which provides a computational meaning to the structure of bialgebra induced on polarized types by the reduction of PDN ; last, a differential λ-bar-µ-calculus encompassing all of the dynamics of PDN.