Abstract
Inspired by recent work on normalisation by evaluation for sums, we propose a normalising and confluent extensional rewriting theory for the simply-typed λ-calculus extended with sum types. As a corollary of confluence we obtain decidability for the extensional equational theory of simply-typed λ-calculus extended with sum types. Unlike previous decidability results, which rely on advanced rewriting techniques or advanced category theory, we only use standard techniques.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.: Normalization by evaluation for typed lambda calculus with coproducts. In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, MA, June 2001, pp. 303–310. IEEE Computer Society Press, Los Alamitos (2001)
Balat, V., Cosmo, R.D., Fiore, M.: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In: POPL 2004. 31st Symposium on Principles of Programming Languages, January 2004, pp. 64–76. ACM Press, New York (2004)
Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logics and the Foundations of Mathmatics, vol. 103. North Holland, Amsterdam (1984)
Berger, U., Eberl, M., Schwichtenberg, H.: Normalization by evaluation. In: Möller, B., Tucker, J.V. (eds.) Prospects for Hardware Foundations. LNCS, vol. 1546, pp. 117–137. Springer, Heidelberg (1998)
Ghani, N.: Beta-eta equality for coproducts. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 171–185. Springer, Heidelberg (1995)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)
Huet, G.P.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)
Lindley, S.: Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh (2005)
Lindley, S., Stark, I.: Reducibility and \({\top\top}\)-lifting for computation types. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 262–277. Springer, Heidelberg (2005)
Ohta, Y., Hasegawa, M.: A terminating and confluent linear lambda calculus. RTA, pp. 166–180 (2006)
Prawitz, D.: Ideas and results in proof theory. In: Proceedings of the 2nd Scandinavian Logic Symposium. Studies in Logics and the Foundations of Mathmatics, vol. 63, pp. 235–307. North Holland, Amsterdam (1971)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Lindley, S. (2007). Extensional Rewriting with Sums. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-73228-0_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73227-3
Online ISBN: 978-3-540-73228-0
eBook Packages: Computer ScienceComputer Science (R0)