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

Fairouz Kamareddine; Roel Bloo; Rob Nederpelt

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

Fairouz Kamareddine, Roel Bloo, Rob Nederpelt

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
Pages	16-27
Number of pages	12
Publication status	Published - 2001
Event	Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00) - Florence, Italy Duration: 5 Sept 2001 → 7 Sept 2001

Conference

Conference	Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00)
Country/Territory	Italy
City	Florence
Period	5/09/01 → 7/09/01

Cite this

@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",

note = "Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00) ; Conference date: 05-09-2001 Through 07-09-2001",

}

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.

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

T2 - Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00)

Y2 - 5 September 2001 through 7 September 2001

ER -

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

Abstract

Conference

Other files and links

Fingerprint

Cite this