Hostname: page-component-8448b6f56d-jr42d Total loading time: 0 Render date: 2024-04-23T11:02:10.660Z Has data issue: false hasContentIssue false
  • English
  • Français

Structural recursion with locally scoped names

Part of: JFP Research Articles

Published online by Cambridge University Press:  27 May 2011

ANDREW M. PITTS
ANDREW M. PITTS*
Affiliation:
University of Cambridge Computer Laboratory, Cambridge CB3 0FD, UK (e-mail: Andrew.Pitts@cl.cam.ac.uk)
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.

This paper introduces a new recursion principle for inductively defined data modulo α-equivalence of bound names that makes use of Odersky-style local names when recursing over bound names. It is formulated in simply typed λ-calculus extended with names that can be restricted to a lexical scope, tested for equality, explicitly swapped and abstracted. The new recursion principle is motivated by the nominal sets notion of ‘α-structural recursion’, whose use of names and associated freshness side-conditions in recursive definitions formalizes common practice with binders. The new calculus has a simple interpretation in nominal sets equipped with name-restriction operations. It is shown to adequately represent α-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. The paper is a revised and expanded version of Pitts (Nominal System T. In Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 2010 (Madrid, Spain). ACM Press, pp. 159–170, 2010).

Type
Articles
Information
Journal of Functional Programming , Volume 21 , Issue 3 , May 2011 , pp. 235 - 286
Copyright
Copyright © Cambridge University Press 2011

References

Altenkirch, T. & Chapman, J. (2009) Big-step normalisation. J. Funct. Prog. 19 (3–4), 311–333.CrossRefGoogle Scholar
Barendregt, H. P. (1984) The Lambda Calculus: Its Syntax and Semantics, Revised ed.North-Holland.Google Scholar
Cardelli, L. & Gordon, A. D. (2001) Logical properties of name restriction. In Proceedings of the 5th International Conference on Typed Lambda Calculus and Applications, Abramsky, S. (ed), Lecture Notes in Computer Science, vol. 2044. Berlin: Springer-Verlag, pp. 46–60.CrossRefGoogle Scholar
Cheney, J. (2005) Nominal logic and abstract syntax. ACM SIGACT News, Logic Column 36 (4), 47–69.Google Scholar
Cheney, J. (2009) A simple nominal type theory. In Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP 2008, Electronic Notes in Theoretical Computer Science, vol. 228. Elsevier B. V., pp. 37–52.CrossRefGoogle Scholar
Coquand, T. (1991) An algorithm for testing conversion in type theory., In Logical Frameworks, Huet, G. & Plotkin, G. D. (eds). New York, NY, USA: Cambridge University Press, pp. 255–228.CrossRefGoogle Scholar
Crary, K. & Harper, R. (2006) Higher-order abstract syntax: Setting the record straight. ACM SIGACT News, Logic Column 37 (3), 93–96.CrossRefGoogle Scholar
Fernández, M. & Gabbay, M. J. (2005) Nominal rewriting with name generation: Abstraction vs. locality. In Proceedings of the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming PPDP 2005. ACM Press, pp. 47–58.Google Scholar
Fiore, M. P., Plotkin, G. D. & Turi, D. (1999) Abstract syntax and variable binding. In Proceedings of the 14th Annual Symposium on Logic in Computer Science. Washington: IEEE Computer Society Press, pp. 193–202.Google Scholar
Friedman, H. (1975) Equality between functionals. In Logic Colloquium, Parikh, R. (ed), Lecture Notes in Mathematics, vol. 453. Berlin/Heidelberg: Springer, pp. 22–37.CrossRefGoogle Scholar
Gabbay, M. J. (2000) A Theory of Inductive Definitions with α-Equivalence: Semantics, Implementation, Programming Language, PhD thesis. University of Cambridge.Google Scholar
Gabbay, M. J. & Lengrand, S. (December 2009) The lambda-context calculus (extended version). Inform. comput. 207, 1369–1400.CrossRefGoogle Scholar
Gabbay, M. J. & Pitts, A. M. (2002) A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13, 341–363.CrossRefGoogle Scholar
Gacek, A., Miller, D. & Nadathur, G. (2008) Combining generic judgments with recursive definitions. In Proceedings of the 23rd IEEE Symposium on Logic in Computer Science, LICS 2008. IEEE Computer Society Press, pp. 33–44.Google Scholar
Gödel, K. (1958) Über eine bisher noch nicht benüzte Erweiterung des finiten Standpunktes. Dialectica 12, 280–287.CrossRefGoogle Scholar
Gordon, A. D. & Melham, T. (1996) Five axioms of alpha-conversion. In Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 1125. Springer-Verlag, pp. 173–191.CrossRefGoogle Scholar
Grégoire, B. & Leroy, X. (2002) A compiled implementation of strong reduction. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (Pittsburgh, PA, USA). ACM Press, pp. 235–246.CrossRefGoogle Scholar
Harper, R. & Pfenning, F. (2005) On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. 6, 61–101.CrossRefGoogle Scholar
Johnstone, P. T. (2002) Sketches of an Elephant, a Topos Theory Compendium, Vol. 1–2. Oxford Logic Guides, nos. 43–44. Oxford University Press.Google Scholar
Licata, D. R. & Harper, R. (2009) A universe of binding and computation. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009. ACM Press, pp. 123–134.Google Scholar
Licata, D. R., Zeilberger, N. & Harper, R. (2008) Focusing on binding and computation. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008 (Pittsburgh, PA, USA, 24–27 June 2008). IEEE Computer Society, pp. 241–252.Google Scholar
Miller, D. A. (1990) An extension to ML to handle bound variables in data structures. In Proceedings of the Logical Frameworks BRA Workshop, Technical Report MS-CIS-90-59. University of Pennsylvania.Google Scholar
Miller, D. A. & Tiu, A. (2005) A proof theory for generic judgments. ACM Trans. Comput. Log. 6 (4), 749–783.CrossRefGoogle Scholar
Milner, R. (1992) Functions as processes. Math. Struct. Comput. Sci. 2 (2), 119–141.CrossRefGoogle Scholar
Moggi, E. (1991) Notions of computation and monads. Inf. Comput., 93 (1), 55–92.CrossRefGoogle Scholar
Nordström, B., Petersson, K. & Smith, J. M. (1990) Programming in Martin-Löf's Type Theory. Oxford University Press.Google Scholar
Norrish, M. (2004) Recursive function definition for types with binders. In Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 3223. Springer-Verlag, pp. 241–256.CrossRefGoogle Scholar
Odersky, M. (1994) A functional theory of local names. In Proceedings of the Conference Record of the 21st Annual ACM Symposium on Principles of Programming Languages. ACM Press, pp. 48–59.Google Scholar
Pfenning, F. (2001) Logical frameworks. In Handbook of Automated Reasoning, Robinson, A. & Voronkov, A. (eds). Elsevier Science and MIT Press, Chapter 17, pp. 1063–1147.CrossRefGoogle Scholar
Pfenning, F. & Elliott, C. (1988) Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, pp. 199–208.Google Scholar
Pientka, B. (2008) A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008. ACM Press, pp. 371–382.Google Scholar
Pitts, A. M. (2003) Nominal logic, a first order theory of names and binding. Inf. Comput. 186, 165–193.CrossRefGoogle Scholar
Pitts, A. M. (2006) Alpha-structural recursion and induction. J. ACM 53, 459–506.CrossRefGoogle Scholar
Pitts, A. M. (2010) Nominal System T. In Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 2010 (Madrid, Spain). ACM Press, pp. 159–170.Google Scholar
Pitts, A. M. & Gabbay, M. J. (2000) A metalanguage for programming with bound names modulo renaming. In Proceedings of the 5th International Conference on Mathematics of Program Construction, MPC 2000, (Ponte De Lima, Portugal, July 2000), Backhouse, R. & Oliveira, J. N. (eds), Lecture Notes in Computer Science, vol. 1837. Heidelberg: Springer-Verlag, pp. 230–255.Google Scholar
Pitts, A. M. & Stark, I. D. B. (1993) Observable properties of higher order functions that dynamically create local names, or: What's new? In Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science (Gdańsk, 1993), Lecture Notes in Computer Science, vol. 711. Springer-Verlag, Berlin, pp. 122–141.CrossRefGoogle Scholar
Pitts, A. M. & Stark, I. D. B. (1998) Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics, Gordon, A. D. & Pitts, A. M. (eds), Publications of the Newton Institute. Cambridge University Press, pp. 227–273.Google Scholar
Poswolsky, A. & Schürmann, C. (2008) Practical programming with higher-order encodings and dependent types. In Proceedings of the European Symposium on Programming, ESOP 2008, Lecture Notes in Computer Science, vol. 4960. Springer-Verlag, pp. 93–107.Google Scholar
Pottier, F. (2007) Static name control for FreshML. In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007. Wroclaw, Poland: IEEE Computer Society Press, pp. 356–365.Google Scholar
Pouillard, N. & Pottier, F. (2010) A fresh look at programming with names and binders. In Proceedings of the Fifteenth ACM SIGPLAN International Conference on Functional Programming, ICFP 2010. ACM Press, pp. 217–228.Google Scholar
Schöpp, U. & Stark, I. D. B. (2004) A dependent type theory with names and binding. In Proceedings of the Computer Science Logic, CSL 2004 (Karpacz, Poland), Lecture notes in Computer Science, vol. 3210. Springer-Verlag, pp. 235–249.Google Scholar
Schürmann, C., Despeyroux, J. & Pfenning, F. (2001) Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. 266, 1–57.Google Scholar
Shinwell, M. R. & Pitts, A. M. (February 2005) Fresh Objective Caml User Manual, Techical Report UCAM-CL-TR-621. University of Cambridge Computer Laboratory.Google Scholar
Shinwell, M. R., Pitts, A. M. & Gabbay, M. J. (2003) FreshML: Programming with binders made simple. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003 (Uppsala, Sweden). ACM Press, pp. 263–274.Google Scholar
Tait, W. W. (1967) Intensional interpretation of functionals of finite type, I. J. Symb. Log. 32 (2), 198–212.CrossRefGoogle Scholar
Urban, C. (2008) Nominal reasoning techniques in Isabelle/HOL. J. Autom. Reason. 40 (4), 327–356.CrossRefGoogle Scholar
Urban, C. & Berghofer, S. (2006) A recursion combinator for nominal datatypes implemented in Isabelle/HOL. In Proceedings of the 3rd International Joint Conference on Automated Reasoning, IJCAR 2006 (Seattle, USA), Lecture Notes in Computer Science, vol. 4130. Springer-Verlag, pp. 498–512.Google Scholar
Urban, C., Cheney, J. & Berghofer, S. (2011) Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12 (15), 1–42.CrossRefGoogle Scholar
Urban, C., Pitts, A. M. & Gabbay, M. J. (2004) Nominal unification. Theor. Comput. Sci. 323, 473–497.CrossRefGoogle Scholar
Westbrook, E., Stump, A. & Austin, E. (2009) The calculus of nominal inductive constructions: An intensional approach to encoding name-bindings. In Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009 (Montreal, Canada), ACM International Conference Proceeding Series. ACM Press, pp. 74–83.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.