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 language | English |
---|---|
Pages (from-to) | 109-131 |
Number of pages | 23 |
Journal | Journal of Logic and Algebraic Programming |
Volume | 62 |
Issue number | 1 |
DOIs | |
Publication status | Published - 1 Jan 2005 |
Keywords
- Canonical forms
- Class reduction
- Reductional behaviour