TY - GEN
T1 - Implementing λ-calculus reduction strategies in extended logic programming languages
AU - Hannan, John
N1 - Funding Information:
Acknowledgements. This work has been supported by a grant from the Danish Natural Science Research Council. I would like to thank the members of the programming language group at DIKU for discussions and comments that contributed to this work.
Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1992.
PY - 1992
Y1 - 1992
N2 - We study the implementation of four reduction strategies for the untyped λ-calculus in the logic programming language λProlog and restricted sublanguages. The higher-order features of these languages provide very natural methods for manipulating and substituting bound variables. Starting from clear and concise specifications of reduction in the full language we demonstrate how to make certain details in the implementations explicit as we restrict ourselves to the weaker sublanguages. We also show how to translate specifications in a higher-order language to a first-order one, such as Prolog, introducing closures as a replacement for substitutions. This process illustrates how a very high-level description of an implementation can be translated to lower-level ones by reasoning about the logic in which the descriptions are given. It also illustrates some basic methods for manipulating functional languages represented in a higher-order abstract syntax.
AB - We study the implementation of four reduction strategies for the untyped λ-calculus in the logic programming language λProlog and restricted sublanguages. The higher-order features of these languages provide very natural methods for manipulating and substituting bound variables. Starting from clear and concise specifications of reduction in the full language we demonstrate how to make certain details in the implementations explicit as we restrict ourselves to the weaker sublanguages. We also show how to translate specifications in a higher-order language to a first-order one, such as Prolog, introducing closures as a replacement for substitutions. This process illustrates how a very high-level description of an implementation can be translated to lower-level ones by reasoning about the logic in which the descriptions are given. It also illustrates some basic methods for manipulating functional languages represented in a higher-order abstract syntax.
UR - http://www.scopus.com/inward/record.url?scp=84947797651&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84947797651&partnerID=8YFLogxK
U2 - 10.1007/bfb0013609
DO - 10.1007/bfb0013609
M3 - Conference contribution
AN - SCOPUS:84947797651
SN - 9783540554981
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 193
EP - 219
BT - Extensions of Logic Programming - 2nd International Workshop, ELP 1991, Proceedings
A2 - Eriksson, Lars-Henrik
A2 - Hallnas, Lars
A2 - Schroeder-Heister, Peter
PB - Springer Verlag
T2 - 2nd International Workshop on Extensions of Logic Programming, ELP 1991
Y2 - 27 January 1991 through 29 January 1991
ER -