Hostname: page-component-745bb68f8f-cphqk Total loading time: 0 Render date: 2025-02-05T02:56:55.372Z Has data issue: false hasContentIssue false
  • English
  • Français

Efficient self-interpretation in lambda calculus

Part of: JFP Research Articles

Published online by Cambridge University Press:  07 November 2008

Torben Æ. Mogensen
Torben Æ. Mogensen
Affiliation:
DIKU, University of Copenhagen, Denmark
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We start by giving a compact representation schema for λ-terms, and show how this leads to an exceedingly small and elegant self-interpreter. We then define the notion of a self-reducer, and show how this too can be written as a small λ-term. Both the self-interpreter and the self-reducer are proved correct. We finally give a constructive proof for the second fixed point theorem for the representation schema. All the constructions have been implemented on a computer, and experiments verify their correctness. Timings show that the self-interpreter and self-reducer are quite efficient, being about 35 and 50 times slower than direct execution using a call-by-need reductions strategy

Type
Articles
Information
Journal of Functional Programming , Volume 2 , Issue 3 , July 1992 , pp. 345 - 364
Copyright
Copyright © Cambridge University Press 1992

References

Barendregt, H. 1984. The Lambda Calculus: Its Syntax and Semantics (revised edition). North-Holland.Google Scholar
Barendregt, H. 1991. Self-interpretation in lambda calculus. J. Functional Program., 1 (2): 229–33.Google Scholar
Berger, U. and Schwichtenberg, H. 1991. An Inverse of the Evaluation Functional for Typed λ-calculus. Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 203–211.Google Scholar
Dybvig, R. K. 1987. The Scheme Programming Language. Prentice-Hall.Google Scholar
Gomard, C. and Jones, N. D. 1991. A Partial Evaluator for the Untyped Lambda Calculus. J. Functional Program., 1 (1): 21–69.Google Scholar
Kleene, S. C. 1952. Introduction to Metamathematics. North-Holland.Google Scholar
Pfenning, F. and Elliot, C. 1988. Higher-Order Abstract Syntax. In Proc. ACM-SIGPLAN Conf. on Programming Language Design and Implementation, pp. 199–208. ACM Press.Google Scholar
Pfenning, F. and Lee, P. 1991. Metacircularity in the polymorphic λ-calculus. Theoretical Computer Science, 89: 137–159.Google Scholar
Reynolds, J. C. 1985. Three Approaches to Type Structure. Vol. 85 of Lecture Notes in Computer Science, pp. 97–138. Springer-Verlag.Google Scholar
Steensgaard-Madsen, J. 1989. Typed Representation of Objects by Functions. TOPLAS, 11 (1): 67–89.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.