Hostname: page-component-8448b6f56d-m8qmq Total loading time: 0 Render date: 2024-04-16T19:10:10.741Z Has data issue: false hasContentIssue false
  • English
  • Français

Big-step normalisation

Part of: JFP Research Articles

Published online by Cambridge University Press:  01 July 2009

THORSTEN ALTENKIRCH  and
JAMES CHAPMAN
THORSTEN ALTENKIRCH
Affiliation:
School of Computer Science, University of Nottingham, Jubilee Campus, Wollaton Road, Nottingham NG8 1BB, UK (e-mail: txa@cs.nott.ac.uk)
JAMES CHAPMAN
Affiliation:
Institute of Cybernetics at Tallinn University of Technology, Akadeemia tee 21, EE-12618 Tallinn, Estonia (e-mail: james@cs.ioc.ee)
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.

Traditionally, decidability of conversion for typed λ-calculi is established by showing that small-step reduction is confluent and strongly normalising. Here we investigate an alternative approach employing a recursively defined normalisation function which we show to be terminating and which reflects and preserves conversion. We apply our approach to the simply typed λ-calculus with explicit substitutions and βη-equality, a system which is not strongly normalising. We also show how the construction can be extended to system T with the usual β-rules for the recursion combinator. Our approach is practical, since it does verify an actual implementation of normalisation which, unlike normalisation by evaluation, is first order. An important feature of our approach is that we are using logical relations to establish equational soundness (identity of normal forms reflects the equational theory), instead of the usual syntactic reasoning using the Church–Rosser property of a term rewriting system.

Type
Articles
Information
Journal of Functional Programming , Volume 19 , Issue 3-4 , July 2009 , pp. 311 - 333
Copyright
Copyright © Cambridge University Press 2009

References

Abadi, M., Cardelli, L., Curien, P.-L. & Lèvy, J.-J. (1990) Explicit substitutions. In Conference Record of 17th Annual ACM Symposium on Principles of Programming Languages, POPL '90 (San Francisco, CA, Jan. 1990). ACM Press, pp. 31–46.Google Scholar
Altenkirch, T. & Chapman, J. (2006) Tait in one big step. In Proceedings of the Workshop on Mathematically Structured Functional Programming, MSFP 2006 (Kuressaare, July 2006), McBride, C. & Uustalu, T. (eds), Electronic Workshops in Computing. BCS, article 4.Google Scholar
Altenkirch, T., Dybjer, P., Hofmann, M. & Scott, P. (2001) Normalization by evaluation for typed lambda calculus with coproducts. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS '01. Boston, MA.Google Scholar
Altenkirch, T., Hofmann, M. & Streicher, T. (1995) Categorical reconstruction of a reduction free normalization proof. In Proceedings of the 6th International Confernece on Category Theory and Computer Science, CTCS '95 (Cambridge, August 1995), Pitt, D., Rydeheard, D. E. & Johnstone, P. (eds), Lecture Notes in Computer Science, vol. 953. Springer, pp. 182–199.Google Scholar
Balat, V. (2002) Une étude des sommes fortes: isomorphismes et formes normales. PhD thesis, Université Denis Diderot.Google Scholar
Berger, U. & Schwichtenberg, H. (1991) An inverse of the evaluation functional for typed λ–calculus. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, LICS '91 (Amsterdam, July 1991). IEEE CS Press, pp. 203–211.Google Scholar
Bove, A. & Capretta, V. (2001) Nested general recursion and partiality in type theory. In Proceedings of the 14th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2001 (Edinburgh, September 2001), Boulton, R. J., & Jackson, P. B. (eds), Lecture Notes in Computer Science, vol. 2152. Springer, pp. 121–135.Google Scholar
Chapman, J. (2007) Formalisation of big-step normalisation for system T [online]. Available at http://cs.ioc.ee/~james/BSN.html (Accessed 4 May 2009).Google Scholar
Chapman, J., McBride, C. & Altenkirch, T. (2007) Epigram reloaded: a standalone typechecker for ETT. In Trends in Functional Programming 6, van Eekelen, M. (ed). Intellect, pp. 79–94.Google Scholar
Coquand, C. (2002) A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions, Higher-Order Symb. Comput., 15 (1): 57–90.CrossRefGoogle Scholar
Coquand, T. (1991) An algorithm for testing conversion in type theory. In Logical Frameworks, Huet, G. & Plotkin, G. (eds). Cambridge University Press, pp. 255–279.CrossRefGoogle Scholar
Coquand, T. & Dybjer, P. (1997) Intuitionistic model constructions and normalization proofs, Math. Struct. Comput. Sci., 7 (1): 75–94.CrossRefGoogle Scholar
David, R. (2001) Normalization without reducibility, Ann. Pure Appl. Logic, 107 (1–3): 121–130.CrossRefGoogle Scholar
Ghani, N. (1995) Beta–eta equality for coproducts. In Proceedings of the 2nd International Conference on Typed Lambda Calculi and Applications, TLCA '95 (Edinburgh, April 1995), Dezani-Ciancaglini, M. & Plotkin, G. (eds), Lecture Notes in Computer Science, vol. 902. Springer, pp. 171–185.CrossRefGoogle Scholar
Girard, J.-Y., Lafont, Y. & Taylor, P. (1989) Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press.Google Scholar
Hofmann, M. (1997) Syntax and semantics of dependent types. Semantics and logics of computation, vol. 14, Pitts, A. M. & Dybjer, P. (eds). Cambridge University Press, pp. 79–130.CrossRefGoogle Scholar
Jay, C. B. & Ghani, N. (1995) The virtues of eta-expansion, J. Funct. Program., 5 (2): 135–154.CrossRefGoogle Scholar
Levy, P. B. (2001) Call-by-Push-Value. PhD thesis, Queen Mary, University of London.Google Scholar
Lindley, S. (2007) Extensional rewriting with sums. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, TLCA 2007 (Paris, June 2007), Ronchi Della Rocca, S. (ed), Lecture Notes in Computer Science, vol. 4583. Springer, pp. 255–271.Google Scholar
Martin-Löf, P. (1984) Intuitionistic Type Theory. Bibliopolis.Google Scholar
McBride, C. (2005a) Epigram [online]. Available at http://www.e-pig.org/ (Accessed 4 May 2009).Google Scholar
McBride, C. (2005b) Epigram: practical programming with dependent types. In Revised Lectures from 5th International School on Advanced Functional Programming, AFP 2004 (Tartu, August 2004), Vene, V. & Uustalu, T. (eds), Lecture Notes in Computer Science, vol. 3622. Springer, pp. 130–170.Google Scholar
McBride, C. & McKinna, J. (2004) The view from the left, J. Funct. Program., 14 (1): 69–111.CrossRefGoogle Scholar
Melliès, P.-A. (1995) Typed lambda-calculi with explicit substitutions may not terminate. In Proceedings of the 2nd International Conference on Typed Lambda Calculi and Applications, TLCA '95 (Edinburgh, April 1995), Dezani-Ciancaglini, M. & Plotkin, G. (eds), Lecture Notes in Computer Science, vol. 902. Springer, pp. 328–334.CrossRefGoogle Scholar
Nordström, B., Petersson, K. & Smith, J. (1990) Programming in Martin-Löf's Type Theory: An Introduction. Oxford University Press.Google Scholar
Norell, U. (2007a) Agda 2 [online]. Available at http://www.cs.chalmers.se/~ulfn/.Google Scholar
Norell, U. (2007b) Towards a Practical Programming Language Based on Dependent Type theory. PhD thesis, Chalmers University of Technology.Google Scholar
Tait, W. W. (1967) Intensional interpretations of functionals of finite type, J. Symb. Logic, 32 (2): 198–212.CrossRefGoogle Scholar
Watkins, K., Cervesato, I., Pfenning, F. & Walker, D. (2004) A concurrent logical framework: the propositional fragment. In Revised Selected Papers from 3rd Internationa; Workshop on Types for Proofs and Programs, TYPES 2003 (Torino, April/May 2003), Berardi, S., Coppo, M. & Damiani, F. (eds), Lecture Notes in Computer Sci., vol. 3085. Springer, pp. 355–377.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.