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

Research output: Contribution to journalArticle

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

Fingerprint

Canonical form
Notation
Term
Equivalence class
Modulo
Calculus
Equivalence relation
Divides
Permutation
Syntax

Keywords

  • Canonical forms
  • Class reduction
  • Reductional behaviour

Cite this

@article{bfb7a4247ca54a0da884defdb5cd1195,
title = "De Bruijn's syntax and reductional behaviour of λ-terms: The untyped case",
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. {\circledC} 2004 Elsevier Inc. All rights reserved.",
keywords = "Canonical forms, Class reduction, Reductional behaviour",
author = "Fairouz Kamareddine and Roel Bloo",
year = "2005",
month = "1",
day = "1",
doi = "10.1016/j.jlap.2004.01.001",
language = "English",
volume = "62",
pages = "109--131",
journal = "Journal of Logic and Algebraic Programming",
issn = "1567-8326",
publisher = "Elsevier",
number = "1",

}

De Bruijn's syntax and reductional behaviour of λ-terms : The untyped case. / Kamareddine, Fairouz; Bloo, Roel.

In: Journal of Logic and Algebraic Programming, Vol. 62, No. 1, 01.01.2005, p. 109-131.

Research output: Contribution to journalArticle

TY - JOUR

T1 - De Bruijn's syntax and reductional behaviour of λ-terms

T2 - The untyped case

AU - Kamareddine, Fairouz

AU - Bloo, Roel

PY - 2005/1/1

Y1 - 2005/1/1

N2 - 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.

AB - 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.

KW - Canonical forms

KW - Class reduction

KW - Reductional behaviour

UR - http://www.scopus.com/inward/record.url?scp=10044243896&partnerID=8YFLogxK

U2 - 10.1016/j.jlap.2004.01.001

DO - 10.1016/j.jlap.2004.01.001

M3 - Article

VL - 62

SP - 109

EP - 131

JO - Journal of Logic and Algebraic Programming

JF - Journal of Logic and Algebraic Programming

SN - 1567-8326

IS - 1

ER -