This paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary lambda calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our result to analyze the characterisation of strong normalisability for three classes of intuitionistic terms: ordinary lambda terms, lambda-J terms (lambda terms with generalised application), and lambda-x terms (lambda terms with explicit substitution). We explain via our system why the type systems in the natural deduction format for lambda-J and lambda-x known from the literature contain extra, exceptional rules for typing generalised application or substitution; and we show a new characterisation of the beta-strongly normalising lambda terms, as a corollary to a PSN-result, relating the lambda calculus and the intuitionistic sequent calculus. Finally, we obtain variants of our characterisation by restricting the set of assignable types to sub-classes of intersection types, notably strict types. In addition, the known characterisation of the beta-strongly normalising lambda terms in terms of assignment of strict types follows as an easy corollary of our results.

Characterising Strongly Normalising Intuitionistic Terms

LIKAVEC, Silvia
2012-01-01

Abstract

This paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary lambda calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our result to analyze the characterisation of strong normalisability for three classes of intuitionistic terms: ordinary lambda terms, lambda-J terms (lambda terms with generalised application), and lambda-x terms (lambda terms with explicit substitution). We explain via our system why the type systems in the natural deduction format for lambda-J and lambda-x known from the literature contain extra, exceptional rules for typing generalised application or substitution; and we show a new characterisation of the beta-strongly normalising lambda terms, as a corollary to a PSN-result, relating the lambda calculus and the intuitionistic sequent calculus. Finally, we obtain variants of our characterisation by restricting the set of assignable types to sub-classes of intersection types, notably strict types. In addition, the known characterisation of the beta-strongly normalising lambda terms in terms of assignment of strict types follows as an easy corollary of our results.
2012
121
1-4
83
120
http://www.iospress.nl/journal/fundamenta-informaticae/
J. E. Santo; J. Ivetic; S. Likavec
File in questo prodotto:
File Dimensione Formato  
FI-esil.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 266.46 kB
Formato Adobe PDF
266.46 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/131550
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 5
social impact