Strong Normalisation of Cut Elimination that Simulates Reduction
15 pages
English

Strong Normalisation of Cut Elimination that Simulates Reduction

-

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

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

Informations

Publié par
Nombre de lectures 15
Langue English

Exrait

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],thefirstauthoridentifiedthroughaPrawitz-styletranslationasubsetofproofsinastandardsequentcalculusthatcorrespondtosimply-typedλ-terms,anddefinedareductionrelationonthoseproofsthatpreciselycorre-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,isconfluent.Thepresentpaperpresentsthefirstproofofstrongnormalisationofthecut-eliminationprocedurein[Kik07].Sincethecut-eliminationprocedurecansimulateβ-reductionofthesimply-typedλ-calculus,itsstrongnormalisationis
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents