Strong Normalisation of Cut Elimination that Simulates Reduction

pages

English

Documents

Écrit par
Stéphane Lengrand2

Publié par
chaeh

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

chaeh

Nombre de lectures

Langue

English

Niveau: Supérieur
Strong Normalisation of Cut-Elimination that Simulates ?-Reduction Kentaro Kikuchi1 and Stéphane Lengrand2 1 RIEC, Tohoku University, Japan 2 CNRS, Laboratoire d'Informatique de l'Ecole Polytechnique, France Abstract This paper is concerned with strong normalisation of cut- elimination for a standard intuitionistic sequent calculus. The cut- elimination procedure is based on a rewrite system for proof-terms with cut-permutation rules allowing the simulation of ?-reduction. Strong nor- malisation of the typed terms is inferred from that of the simply-typed ?-calculus, using the notions of safe and minimal reductions as well as a simulation in Nederpelt-Klop's ?I-calculus. It is also shown that the type-free terms enjoy the preservation of strong normalisation (PSN) property with respect to ?-reduction in an isomorphic image of the type- free ?-calculus. 1 Introduction It is now established that cut-elimination procedures in sequent calculus have a computational meaning (see e.g. [Her94,CH00,UB99,San00]), in the same sense as that of proof transformations in natural deduction. The paradigm of the Curry-Howard correspondence is then illustrated not only by (intuitionistic im- plicational) natural deduction and the simply-typed ?-calculus [How80], but also by a typed higher-order calculus corresponding to the (intuitionistic implica- tional) sequent calculus.

then ? ?g3

cut- elimination procedure

means usual implicit

g1 ?

calculus untouched

both term-structure

local proof

?g3-terms

calculus

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

Tohoku University Calculus

StrongNormalisationofCut-EliminationthatSimulatesβ-ReductionKentaroKikuchi1andStéphaneLengrand21RIEC,TohokuUniversity,Japan2CNRS,Laboratoired’Informatiquedel’EcolePolytechnique,FranceAbstractThispaperisconcernedwithstrongnormalisationofcut-eliminationforastandardintuitionisticsequentcalculus.Thecut-eliminationprocedureisbasedonarewritesystemforproof-termswithcut-permutationrulesallowingthesimulationofβ-reduction.Strongnor-malisationofthetypedtermsisinferredfromthatofthesimply-typedλ-calculus,usingthenotionsofsafeandminimalreductionsaswellasasimulationinNederpelt-Klop’sλI-calculus.Itisalsoshownthatthetype-freetermsenjoythepreservationofstrongnormalisation(PSN)propertywithrespecttoβ-reductioninanisomorphicimageofthetype-freeλ-calculus.1IntroductionItisnowestablishedthatcut-eliminationproceduresinsequentcalculushaveacomputationalmeaning(seee.g.[Her94,CH00,UB99,San00]),inthesamesenseasthatofprooftransformationsinnaturaldeduction.TheparadigmoftheCurry-Howardcorrespondenceisthenillustratednotonlyby(intuitionisticim-plicational)naturaldeductionandthesimply-typedλ-calculus[How80],butalsobyatypedhigher-ordercalculuscorrespondingtothe(intuitionisticimplica-tional)sequentcalculus.In[Kik06],theﬁrstauthoridentiﬁedthroughaPrawitz-styletranslationasubsetofproofsinastandardsequentcalculusthatcorrespondtosimply-typedλ-terms,anddeﬁnedareductionrelationonthoseproofsthatpreciselycorre-spondstoβ-reductionofthesimply-typedλ-calculus.Thereductionrelationwasshowntobesimulatedbyacut-eliminationprocedure,sothesystemofproof-termsforthesequentcalculusisaconservativeextensionoftheλ-calculusinbothterm-structureandreduction.Sincethecorrespondenceholdsalsoforthetype-freecase,therewritesystemin[Kik06]cansimulateβ-reductionofthetype-freeλ-calculus,whichmeansthatitisstrongenoughtorepresentallcomputablefunctions.Itwasalsoshownin[Kik07]thatarestrictionoftherewritesystemin[Kik06],whichisstillstrongenoughtosimulateβ-reduction,isconﬂuent.Thepresentpaperpresentstheﬁrstproofofstrongnormalisationofthecut-eliminationprocedurein[Kik07].Sincethecut-eliminationprocedurecansimulateβ-reductionofthesimply-typedλ-calculus,itsstrongnormalisationis

Voir