De Bruijn's syntax and reductional behaviour of λ-terms: The typed case

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

In this paper, we consider the typed versions of the ?-calculus written in a notation which helps describe canonical forms more elegantly than the classical notation, and enables to divide terms into classes according to their reductional behaviour. In this notation, ß-reduction can be generalised from a relation on terms to one on equivalence classes. This class reduction covers many known notions of generalised reduction. We extend the Barendregt cube with our class reduction and show that the subject reduction property fails but that this is not unique to our class reduction. We show that other generalisations of reduction (such as the s -reduction of Regnier) also behave badly in typed versions of the ?-calculus. Nevertheless, solution is at hand for these generalised reductions by adopting the useful addition of definitions in the contexts of type derivations. We show that adding such definitions enables the extensions of type systems with class reduction and s -reduction to satisfy all the desirable properties of type systems, including subject reduction and strong normalisation. Our proposed typing relation ?c is the most general relation in the literature that satisfies all the desirable properties of type systems. We show that classes contain all the desirable information related to a term with respect to typing, strong normalisation, subject reduction, etc. © 2004 Elsevier Inc. All rights reserved.

Original languageEnglish
Pages (from-to)159-189
Number of pages31
JournalJournal of Logic and Algebraic Programming
Volume62
Issue number2
DOIs
Publication statusPublished - 1 Feb 2005

Keywords

  • Class reduction
  • Strong normalisation
  • Subject reduction
  • Type theory

Fingerprint Dive into the research topics of 'De Bruijn's syntax and reductional behaviour of λ-terms: The typed case'. Together they form a unique fingerprint.

  • Cite this