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

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


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
Issue number1
Publication statusPublished - 1 Jan 2005


  • Canonical forms
  • Class reduction
  • Reductional behaviour


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