A computational approach to reflective meta-reasoning about languages with bindings

ABSTRACT

We present a foundation for a computational meta-theory of languages with bindings implemented in a computer-aided formal reasoning environment. Our theory provides the ability to reason abstractly about operators, languages, open-ended languages, classes of languages, etc. The theory is based on the ideas of higher-order abstract syntax, with an appropriate induction principle parameterized over the language i.e. a set of operators) being used. In our approach, both the bound and free variables are treated uniformly and this uniform treatment extends naturally to variable-length bindings. The implementation is reflective, namely there is a natural mapping between the meta-language of the theorem-prover and the object language of our theory. The object language substitution operation is mapped to the meta-language substitution and does not need to be defined recursively. Our approach does not require designing a custom type theory; in this paper we describe the implementation of this foundational theory within a general-purpose type theory. This work is fully implemented in the MetaPRL theorem prover, using the pre-existing NuPRL-like Martin-Lof-style computational type theory. Based on this implementation, we lay out an outline for a framework for programming language experimentation and exploration as well as a general reflective reasoning framework. This paper also includes a short survey of the existing approaches to syntactic reflection.

REFERENCES

• 1: Eric Aaron , Stuart Allen, Justifying Calculational Logic by a Conventional Metalinguistic Semanti cs, Cornell University, Ithaca, NY, 1999
• 2: Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. Available from http://www.cis.upenn.edu/group/proj/plclub/mmm/, 2005.
• 3: William Aitken and Robert L. Constable. Reflecting on Nuprl : Lessons 1--4. Technical report, Cornell University, Computer Science Department, Ithaca, NY, 1992.
• 4: Stuart F. Allen , Robert L. Constable , Rich Eaton , Christoph Kreitz , Lori Lorigo, The Nuprl Open Logical Environment, Proceedings of the 17th International Conference on Automated Deduction, p.170-176, June 17-20, 2000
• 5: Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken. The semantics of reflected proof. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 95--197. IEEE Computer Society Press, June 1990.
• 6: Simon Ambler , Roy L. Crole , Alberto Momigliano, Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, p.13-30, August 20-23, 2002
• 7: S. J. Ambler , R. L. Crole , Alberto Momigliano, A definitional approach to primitivexs recursion over higher order abstract syntax, Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.1-11, August 26, 2003, Uppsala, Sweden [doi>10.1145/976571.976572]
• 8: William E. Aitken , Robert L. Constable , Judith L. Underwood, Metalogical Frameworks II: Developing a Reflected Decision Procedure, Journal of Automated Reasoning, v.22 n.2, p.171-221, February 1999 [doi>10.1023/A:1005929703675]
• 9: Stuart F. Allen. A Non-type-theoretic Definition of Martin-Löf's Types. In D. Gries, editor, Proceedings of the 2nd IEEE Symposium on Logic in Computer Science, pages 215--224. IEEE Computer Society Press, June 1987.
• 10: Stuart Frazier Allen, A non-type-theoretic semantics for type-theoretic language, 1987
• 11: Sergei N. Artëmov, On Explicit Reflection in Theorem Proving and Formal Verification, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.267-281, July 07-10, 1999
• 12: Sergei Artemov. Evidence-based common knowledge. Technical Report TR-2004018, CUNY Ph.D. Program in Computer Science Technical Reports, November 2004.
• 13: Eli Barzilay and Stuart Allen. Reflecting higher-order abstract syntax in Nuprl. In Victor A. Carreno, Cézar A. Munoz, and Sophiène Tahar, editors, Theorem Proving in Higher Order Logics; Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Hampton, VA, August 2002, pages 23--32. National Aeronautics and Space Administration, 2002.
• 14: Eli Barzilay, Stuart Allen, and Robert Constable. Practical reflection in Nuprl. Short paper presented at 18th Annual IEEE Symposium on Logic in Computer Science, June 22--25, Ottawa, Canada, 2003.
• 15: Eli Barzilay, Quotation and Reflection in Nuprl and Scheme, Cornell University, Ithaca, NY, 2001
• 16: Eli Barzilay. Implementing Reflection in Nuprl. PhD thesis, Cornell University, 2005. In preparation.
• 17: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 18: Lúis Crus-Filipe and Freek Weidijk. Hierarchical reflection. In Slind et al. phols2004, pages 66--81.
• 19: Robert L. Constable. Using reflection to explain and enhance type theory. In Helmut Schwichtenberg, editor, Proof and Computation, volume 139 of NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20-August 1, NATO Series F, pages 65--100. Springer, Berlin, 1994.
• 20: N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagaciones Mathematische, 34:381--392, 1972. This also appeared in the Proceedings of the Koninklijke Nederlandse Akademie van Wetenschappen, Amsterdam, series A, 75, No. 5.
• 21: Joëlle Despeyroux , Amy P. Felty , André Hirschowitz, Higher-Order Abstract Syntax in Coq, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, p.124-138, April 10-12, 1995
• 22: Joëlle Despeyroux , André Hirschowitz, Higher-Order Abstract Syntax with Induction in Coq, Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, p.159-173, July 16-22, 1994
• 23: James R. Davis , Daniel P. Huttenlocher, Shared annotation for cooperative learning, The first international conference on Computer support for collaborative learning, p.84-88, October 1995, Indiana Univ., Bloomington, Indiana, United States
• 24: Joëlle Despeyroux , Pierre Leleu, A Modal Lambda Calculus with Iteration and Case Constructs, Selected papers from the International Workshop on Types for Proofs and Programs, p.47-61, March 27-31, 1998
• 25: Joëlle Despeyroux , Pierre Leleu, Recursion over objects of functional type, Mathematical Structures in Computer Science, v.11 n.4, p.555-572, August 2001 [doi>10.1017/S0960129501003346]
• 26: Joëlle Despeyroux , Frank Pfenning , Carsten Schürmann, Primitive Recursion for Higher-Order Abstract Syntax, Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, p.147-163, April 02-04, 1997
• 27: Andrzej Ehrenfeucht and Jan Mycielski. Abbreviating proofs by adding new axioms. Bulletin of the American Mathematical Society, 77:366--367, 1971.
• 28: Solomon Feferman et al., editors. Kurt Gödel Collected Works, volume 1. Oxford University Press, Oxford, Clarendon Press, New York, 1986.
• 29: Marcelo Fiore , Gordon Plotkin , Daniele Turi, Abstract Syntax and Variable Binding, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.193, July 02-05, 1999
• 30: Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, July 1999
• 31: Andrew D. Gordon , Thomas F. Melham, Five Axioms of Alpha-Conversion, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, p.173-190, August 26-30, 1996
• 32: Jim Grundy, Tom Melham, and John O'Leary. A reflective functional language for hardware design and theorem proving. Technical Report PRG-RR-03-16, Oxford Univerity, Computing Laboratory, 2003.
• 33: Kurt Gödel. Über formal unentscheidbare sĂtze der principia mathematica und verwandter systeme I. Monatshefte für Mathematik und Physik, 38:173--198, 1931. English version in {59}.
• 34: K. Gödel. Über die Länge von beweisen. Ergebnisse eines mathematischen Kolloquiums, 7:23--24, 1936. English translation in {28}, pages 397--399.
• 35: F. Giunchiglia , Alan Smaill, Reflection in constructive and non-constructive automated reasoning, Meta-programming in logic programming, MIT Press, Cambridge, MA, 1989
• 36: Herman Geuvers , Freek Wiedijk , Jan Zwanenburg, Equational Reasoning via Partial Reflection, Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, p.162-178, August 14-18, 2000
• 37: Jason J. Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, and Xin Yu. A listing of MetaPRL theories. http://metaprl.org/theories.pdf.
• 38: J. Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-53, SRI International, Cambridge Computer Science Research Centre, Millers Yard, Cambridge, UK, February 1995.
• 39: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 40: Jason J. Hickey, Nuprl-Light: An Implementation Framework for Higher-Order Logics, Proceedings of the 14th International Conference on Automated Deduction, p.395-399, July 13-17, 1997
• 41: Jason Hickey, Fault-Tolerant Distributed Theorem Proving, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.227-231, July 07-10, 1999
• 42: Jason Jonathan Hickey , Robert L. Constable, The metaprl logical programming environment, 2000
• 43: Gérard P. Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31--55, 1978.
• 44: Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu. MetaPRL --- A modular logical environment. In David Basin and Burkhart Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of Lecture Notes in Computer Science, pages 287--303. Springer-Verlag, 2003
• 45: Jason J. Hickey, Aleksey Nogin, Alexei Kopylov, et al. MetaPRL home page. http://metaprl.org/.
• 46: Andrzej Mostowski. Sentences undecidable in formalized arithmetic: an exposition of the theory of Kurt Gödel. Amsterdam: North-Holland, 1952.
• 47: Aleksey Nogin , Jason Hickey, Sequent Schema for Derived Rules, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, p.281-297, August 20-23, 2002
• 48: Aleksey Nogin, Alexei Kopylov, Xin Yu, and Jason Hickey. A computational approach to reflective meta-reasoning about languages with bindings. Technical Report CaltechCSTR:2005.003, California Institure of Technology, 2005. Available at http://resolver.caltech.edu/CaltechCSTR:2005.003.
• 49: Michael Norrish. Recursive function definition for types with binders. In Slind et al. phols2004, pages 241--256.
• 50: R. Parikh. Existence and feasibility in arithmetic. The Journal of Symbolic Logic, 36:494--508, 1971.
• 51: Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1994.
• 52: F. Pfenning , C. Elliot, Higher-order abstract syntax, ACM SIGPLAN Notices, v.23 n.7, p.199-208, July 1988
• 53: F. Pfening, Elf: a language for logic definition and verified metaprogramming, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.313-322, June 1989, Pacific Grove, California, United States
• 54: Gordon Plotkin. An illative theory of relations. In R. Cooper, K. Mukai, and J. Perry, editors,Situation Theory and Its Applications, Volume 1, number 22 in CSLI Lecture Notes, pages 133--146. Centre for the Study of Language and Information, 1990.
• 55: L. Paulson and T. Nipkow. Isabelle tutorial and user's manual. Technical report, University of Cambridge Computing Laboratory, 1990.
• 56: Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), volume 3223 of Lecture Notes in Computer Science. Springer-Verlag, 2004.
• 57: Carsten Schürmann, Recursion for Higher-Order Encodings, Proceedings of the 15th International Workshop on Computer Science Logic, p.585-599, September 10-13, 2001
• 58: Brian Cantwell Smith, Reflection and semantics in LISP, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.23-35, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800513]
• 59: J. van Heijenoort, editor. From Frege to Gödel: A Source Book in Mathematical Logic, 1879--1931. Harvard University Press, Cambridge, MA, 1967.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

General Terms:
Languages, Theory, Verification

Keywords:
MetaPRL, Nuprl, experimentation, higher-order abstract syntax, languages with bindings, programming language, reflection, type theory