Tradeoffs in the intensional representation of lambda terms

Chuck Liang; Gopalan Nadathur

doi:10.1007/3-540-45610-4_14

Tradeoffs in the intensional representation of lambda terms

Chuck Liang, Gopalan Nadathur

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Scopus citations

Abstract

Higher-order representations of objects such as programs, specifications and proofs are important to many metaprogramming and symbolic computation tasks. Systems that support such representations often depend on the implementation of an intensional view of the terms of suitable typed lambda calculi. Refined lambda calculus notations have been proposed that can be used in realizing such implementations. There are, however, choices in the actual deployment of such notations whose practical consequences are not well understood. Towards addressing this lacuna, the impact of three specific ideas is examined:the de Bruijn representation of bound variables, the explicit encoding of substitutions in terms and the annotation of terms to indicate their independence on external abstractions. Qualitative assessments are complemented by experiments over actual computations. The empirical study is based on λProlog programs executed using suitable variants of a low level, abstract machine based implementation of this language.

Original language	English (US)
Title of host publication	Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings
Editors	Sophie Tison
Publisher	Springer Verlag
Pages	192-206
Number of pages	15
ISBN (Print)	3540439161, 9783540439165
DOIs	https://doi.org/10.1007/3-540-45610-4_14
State	Published - 2002
Externally published	Yes
Event	13th International Conference on Rewriting Techniques and Applications, RTA 2002 - Copenhagen, Denmark Duration: Jul 22 2002 → Jul 24 2002

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2378
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	13th International Conference on Rewriting Techniques and Applications, RTA 2002
Country/Territory	Denmark
City	Copenhagen
Period	7/22/02 → 7/24/02

Bibliographical note

Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.

Access

10.1007/3-540-45610-4_14

OpenUrl availability

Full text

Cite this

Liang, C., & Nadathur, G. (2002). Tradeoffs in the intensional representation of lambda terms. In S. Tison (Ed.), Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings (pp. 192-206). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2378). Springer Verlag. https://doi.org/10.1007/3-540-45610-4_14

Tradeoffs in the intensional representation of lambda terms. / Liang, Chuck; Nadathur, Gopalan.
Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings. ed. / Sophie Tison. Springer Verlag, 2002. p. 192-206 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2378).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Liang, C & Nadathur, G 2002, Tradeoffs in the intensional representation of lambda terms. in S Tison (ed.), Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2378, Springer Verlag, pp. 192-206, 13th International Conference on Rewriting Techniques and Applications, RTA 2002 , Copenhagen, Denmark, 7/22/02. https://doi.org/10.1007/3-540-45610-4_14

Liang C, Nadathur G. Tradeoffs in the intensional representation of lambda terms. In Tison S, editor, Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings. Springer Verlag. 2002. p. 192-206. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-45610-4_14

Liang, Chuck ; Nadathur, Gopalan. / Tradeoffs in the intensional representation of lambda terms. Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings. editor / Sophie Tison. Springer Verlag, 2002. pp. 192-206 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{c07b607c00854368b9a8b7d37251bcb3,

title = "Tradeoffs in the intensional representation of lambda terms",

abstract = "Higher-order representations of objects such as programs, specifications and proofs are important to many metaprogramming and symbolic computation tasks. Systems that support such representations often depend on the implementation of an intensional view of the terms of suitable typed lambda calculi. Refined lambda calculus notations have been proposed that can be used in realizing such implementations. There are, however, choices in the actual deployment of such notations whose practical consequences are not well understood. Towards addressing this lacuna, the impact of three specific ideas is examined:the de Bruijn representation of bound variables, the explicit encoding of substitutions in terms and the annotation of terms to indicate their independence on external abstractions. Qualitative assessments are complemented by experiments over actual computations. The empirical study is based on λProlog programs executed using suitable variants of a low level, abstract machine based implementation of this language.",

author = "Chuck Liang and Gopalan Nadathur",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2002.; 13th International Conference on Rewriting Techniques and Applications, RTA 2002 ; Conference date: 22-07-2002 Through 24-07-2002",

year = "2002",

doi = "10.1007/3-540-45610-4_14",

language = "English (US)",

isbn = "3540439161",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "192--206",

editor = "Sophie Tison",

booktitle = "Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings",

}

TY - GEN

T1 - Tradeoffs in the intensional representation of lambda terms

AU - Liang, Chuck

AU - Nadathur, Gopalan

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2002.

PY - 2002

Y1 - 2002

N2 - Higher-order representations of objects such as programs, specifications and proofs are important to many metaprogramming and symbolic computation tasks. Systems that support such representations often depend on the implementation of an intensional view of the terms of suitable typed lambda calculi. Refined lambda calculus notations have been proposed that can be used in realizing such implementations. There are, however, choices in the actual deployment of such notations whose practical consequences are not well understood. Towards addressing this lacuna, the impact of three specific ideas is examined:the de Bruijn representation of bound variables, the explicit encoding of substitutions in terms and the annotation of terms to indicate their independence on external abstractions. Qualitative assessments are complemented by experiments over actual computations. The empirical study is based on λProlog programs executed using suitable variants of a low level, abstract machine based implementation of this language.

AB - Higher-order representations of objects such as programs, specifications and proofs are important to many metaprogramming and symbolic computation tasks. Systems that support such representations often depend on the implementation of an intensional view of the terms of suitable typed lambda calculi. Refined lambda calculus notations have been proposed that can be used in realizing such implementations. There are, however, choices in the actual deployment of such notations whose practical consequences are not well understood. Towards addressing this lacuna, the impact of three specific ideas is examined:the de Bruijn representation of bound variables, the explicit encoding of substitutions in terms and the annotation of terms to indicate their independence on external abstractions. Qualitative assessments are complemented by experiments over actual computations. The empirical study is based on λProlog programs executed using suitable variants of a low level, abstract machine based implementation of this language.

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

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

U2 - 10.1007/3-540-45610-4_14

DO - 10.1007/3-540-45610-4_14

M3 - Conference contribution

AN - SCOPUS:84886715471

SN - 3540439161

SN - 9783540439165

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 192

EP - 206

BT - Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings

A2 - Tison, Sophie

PB - Springer Verlag

T2 - 13th International Conference on Rewriting Techniques and Applications, RTA 2002

Y2 - 22 July 2002 through 24 July 2002

ER -

Tradeoffs in the intensional representation of lambda terms

Abstract

Publication series

Other

Bibliographical note

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this