De Bruijn's syntax and reductional equivalence of λ-terms

Fairouz Kamareddine, Roel Bloo, Rob Nederpelt

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 and we establish the desirable properties of our reduction modulo equivalence classes rather than single terms. Finally, we extend the cube consisting of eight type systems with class reduction and show that this extension satisfies all the desirable properties of type systems.

Original languageEnglish
Title of host publicationProceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
Pages16-27
Number of pages12
Publication statusPublished - 2001
EventProceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00) - Florence, Italy
Duration: 5 Sep 20017 Sep 2001

Conference

ConferenceProceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00)
CountryItaly
CityFlorence
Period5/09/017/09/01

Fingerprint

Notation
Equivalence
Canonical form
Type Systems
Term
Equivalence relation
Equivalence class
Regular hexahedron
Divides
Modulo
Calculus
Syntax
Class

Cite this

Kamareddine, F., Bloo, R., & Nederpelt, R. (2001). De Bruijn's syntax and reductional equivalence of λ-terms. In Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (pp. 16-27)
Kamareddine, Fairouz ; Bloo, Roel ; Nederpelt, Rob. / De Bruijn's syntax and reductional equivalence of λ-terms. Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 2001. pp. 16-27
@inproceedings{edb2c879a6c84fad84d299c36d8a2ec1,
title = "De Bruijn's syntax and reductional equivalence of λ-terms",
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 and we establish the desirable properties of our reduction modulo equivalence classes rather than single terms. Finally, we extend the cube consisting of eight type systems with class reduction and show that this extension satisfies all the desirable properties of type systems.",
author = "Fairouz Kamareddine and Roel Bloo and Rob Nederpelt",
year = "2001",
language = "English",
isbn = "158113388X",
pages = "16--27",
booktitle = "Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming",

}

Kamareddine, F, Bloo, R & Nederpelt, R 2001, De Bruijn's syntax and reductional equivalence of λ-terms. in Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. pp. 16-27, Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00), Florence, Italy, 5/09/01.

De Bruijn's syntax and reductional equivalence of λ-terms. / Kamareddine, Fairouz; Bloo, Roel; Nederpelt, Rob.

Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 2001. p. 16-27.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

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

AU - Kamareddine, Fairouz

AU - Bloo, Roel

AU - Nederpelt, Rob

PY - 2001

Y1 - 2001

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 and we establish the desirable properties of our reduction modulo equivalence classes rather than single terms. Finally, we extend the cube consisting of eight type systems with class reduction and show that this extension satisfies all the desirable properties of type systems.

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 and we establish the desirable properties of our reduction modulo equivalence classes rather than single terms. Finally, we extend the cube consisting of eight type systems with class reduction and show that this extension satisfies all the desirable properties of type systems.

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

M3 - Conference contribution

SN - 158113388X

SP - 16

EP - 27

BT - Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming

ER -

Kamareddine F, Bloo R, Nederpelt R. De Bruijn's syntax and reductional equivalence of λ-terms. In Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 2001. p. 16-27