Abstract
From a constructive proof of strong normalization plus uniqueness of the long beta-normal form for the simply typed lambda-calculus a normalization program is extracted using Kreisel's modified realizability interpretation for intuitionistic logic. The proof — which uses Tait's computability predicates — is not completely formalized: Induction is done on the meta level, and therefore not a single program but a family of program, one for each term is obtained. Nevertheless this may be used to write a short and efficient normalization program in a type free programming functional programming language (e.g. LISP) which has the interesting feature that it first evaluates a term r of type π to a functional ¦r¦ of type p and then collapses ¦r¦ to the normal form of r.
Preview
Unable to display preview. Download preview PDF.
References
U. Berger, H. Schwichtenberg, An Inverse of the Evaluation Functional for Typed λ-calculus, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, (1991) 203–211.
C. Coquand, A proof of normalization for simply typed lambda calculus written in ALF, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden (1992) 80–87.
S. Hayashi, PX: a system extracting programs from proofs, Kyoto University, Japan (1987).
V. Gaspes, J. S. Smith, Machine Checked Normalization Proofs for Typed Combinator Calculi, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden (1992) 168–192.
G. Kreisel, Interpretation of analysis by means of functionals of finite type, in Constructivity in Mathematics (1959) 101–128.
C. Paulin-Mohring, B. Werner, Synthesis of ML programs in the system Coq, Submitted to the Journal of Symbolic Computations (1992).
H. Schwichtenberg, Proofs as Programs, Leeds: Proof Theory '90 (P. Aczel, H. Simmons, Editors 1990).
W. W. Tait, Intensional Interpretation of Functionals of Finite Type I, Journal of Symbolic Logic 32(2) (1967) 198–212.
A. S. Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, SLNM 344 (1973).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berger, U. (1993). Program extraction from normalization proofs. In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037100
Download citation
DOI: https://doi.org/10.1007/BFb0037100
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56517-8
Online ISBN: 978-3-540-47586-6
eBook Packages: Springer Book Archive