TY - JOUR
T1 - The suspension notation for lambda terms and its use in metalanguage implementations
AU - Nadathur, Gopalan
N1 - Copyright:
Copyright 2018 Elsevier B.V., All rights reserved.
PY - 2002/10
Y1 - 2002/10
N2 - Many metalanguages and logical frameworks have emerged in recent years that use the terms of the lambda calculus as data structures. A common set of questions govern the suitability of a representation for lambda terms in the implementation of such systems: α-convertibility must be easily recognizable, sharing in reduction steps, term traversal and term structure must be possible, comparison and unification operations should be efficiently supported and it should be possible to examine terms embedded inside abstractions. Explicit substitution notations for lambda calculi provide a basis for realizing such requirements. We discuss here the issues related to using one such notation - the suspension notation of Nadathur and Wilson - in this capacity. This notation has been used in two significant practical systems: the Standard ML of New Jersey compiler and the Teyjus implementation of λ-Prolog. We expose the theoretical properties of this notation, highlight pragmatic considerations in its use in implementing operations such as reduction and unification and discuss its relationship to other explicit substitution notations.
AB - Many metalanguages and logical frameworks have emerged in recent years that use the terms of the lambda calculus as data structures. A common set of questions govern the suitability of a representation for lambda terms in the implementation of such systems: α-convertibility must be easily recognizable, sharing in reduction steps, term traversal and term structure must be possible, comparison and unification operations should be efficiently supported and it should be possible to examine terms embedded inside abstractions. Explicit substitution notations for lambda calculi provide a basis for realizing such requirements. We discuss here the issues related to using one such notation - the suspension notation of Nadathur and Wilson - in this capacity. This notation has been used in two significant practical systems: the Standard ML of New Jersey compiler and the Teyjus implementation of λ-Prolog. We expose the theoretical properties of this notation, highlight pragmatic considerations in its use in implementing operations such as reduction and unification and discuss its relationship to other explicit substitution notations.
KW - Explicit substitution
KW - Logical framework
KW - Suspension notation
UR - http://www.scopus.com/inward/record.url?scp=18944389987&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=18944389987&partnerID=8YFLogxK
U2 - 10.1016/S1571-0661(04)80539-5
DO - 10.1016/S1571-0661(04)80539-5
M3 - Conference article
AN - SCOPUS:18944389987
SN - 1571-0661
VL - 67
SP - 35
EP - 48
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
T2 - WoLLIC'2002, 9th Workshop on Logic, Language, Information and Computation
Y2 - 30 July 2002 through 2 August 2002
ER -