Strong Normalisation of Cut Elimination that Simulates Reduction

Stéphane Lengrand2

Description

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

Sujets

• Tohoku University
• Calculus

Informations

• Publié par: chaeh
• Nombre de lectures: 15
• Langue: English

Extrait

StrongNormalisationofCut-Elimination thatSimulatesβ-Reduction KentaroKikuchi 1 andStéphaneLengrand 2 1 RIEC,TohokuUniversity,Japan 2 CNRS,Laboratoired’Informatiquedel’EcolePolytechnique,France AbstractThispaperisconcernedwithstrongnormalisationofcut- eliminationforastandardintuitionisticsequentcalculus.Thecut- eliminationprocedureisbasedonarewritesystemforproof-termswith cut-permutationrulesallowingthesimulationofβ-reduction.Strongnor- malisationofthetypedtermsisinferredfromthatofthesimply-typed λ-calculus,usingthenotionsofsafeandminimalreductionsaswell asasimulationinNederpelt-Klop’sλI-calculus.Itisalsoshownthat thetype-freetermsenjoythepreservationofstrongnormalisation(PSN) propertywithrespecttoβ-reductioninanisomorphicimageofthetype- freeλ-calculus. 1Introduction Itisnowestablishedthatcut-eliminationproceduresinsequentcalculushavea computationalmeaning(seee.g.[Her94,CH00,UB99,San00]),inthesamesense asthatofprooftransformationsinnaturaldeduction.Theparadigmofthe Curry-Howardcorrespondenceisthenillustratednotonlyby(intuitionisticim- plicational)naturaldeductionandthesimply-typedλ-calculus[How80],butalso byatypedhigher-ordercalculuscorrespondingtothe(intuitionisticimplica- tional)sequentcalculus. In[Kik06],thefirstauthoridentifiedthroughaPrawitz-styletranslationa subsetofproofsinastandardsequentcalculusthatcorrespondtosimply-typed λ-terms,anddefinedareductionrelationonthoseproofsthatpreciselycorre- spondstoβ-reductionofthesimply-typedλ-calculus.Thereductionrelation wasshowntobesimulatedbyacut-eliminationprocedure,sothesystemof proof-termsforthesequentcalculusisaconservativeextensionoftheλ-calculus inbothterm-structureandreduction.Sincethecorrespondenceholdsalsofor thetype-freecase,therewritesystemin[Kik06]cansimulateβ-reductionof thetype-freeλ-calculus,whichmeansthatitisstrongenoughtorepresentall computablefunctions.Itwasalsoshownin[Kik07]thatarestrictionofthe rewritesystemin[Kik06],whichisstillstrongenoughtosimulateβ-reduction, isconfluent. Thepresentpaperpresentsthefirstproofofstrongnormalisationofthe cut-eliminationprocedurein[Kik07].Sincethecut-eliminationprocedurecan simulateβ-reductionofthesimply-typedλ-calculus,itsstrongnormalisationis