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

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

In this paper, a notation influenced by de Bruijn's syntax of the ?-calculus is used to describe canonical forms of terms and an equivalence relation which divides terms into classes according to their reductional behaviour. We show that this notation helps describe canonical forms more elegantly than the classical notation. We define reduction modulo equivalence classes of terms up to the permutation of redexes in canonical forms and show that this reduction contains other notions of reductions in the literature including the s -reduction of Regnier. We establish all the desirable properties of our reduction modulo equivalence classes for the untyped ?-calculus. © 2004 Elsevier Inc. All rights reserved.

Original languageEnglish
Pages (from-to)109-131
Number of pages23
JournalJournal of Logic and Algebraic Programming
Volume62
Issue number1
DOIs
Publication statusPublished - 1 Jan 2005

Keywords

  • Canonical forms
  • Class reduction
  • Reductional behaviour

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

  • Cite this