Calculi of meta-variables

Abstract

The notion of meta-variable plays a fundamental role when we define formal systems such as logical and computational calculi. Yet it has been usually understood only informally as is seen in most textbooks of logic. Based on our observations of the usages of meta-variables in textbooks, we propose two formal systems that have the notion of meta-variable.In both calculi, each variable is given a level (non-negative integer), which classifies variables into object variables (level 0), meta-variables (level 1), metameta-variables (level 2) and so on. Then, simple arity systems are used to exclude meaningless terms like a meta-level function operating on the metameta-level. A main difference of the two calculi lies in the definitions of substitution. The first calculus uses textual substitution, which can often be found in definitions of quantified formulae: when a term is substituted for a meta-variable, free object-level variables in the term may be captured. The second calculus is based on the observation that predicates can be regarded as meta-level functions on object-level terms, hence uses capture-avoiding substitution.We show that both calculi enjoy a number of properties including Church-Rosser and Strong Normalization, which are indispensable when we use them as frameworks to define logical systems.

References

1. Kleene S C Introduction to metamathematics. North-Holland 1952
2. Shoenfield J R Mathematical logic. Addison-Wesley 1967
3. Harper R Honsell F Plotkin G A framework for defining logicsJournal of the Association for Computing Machinery 1993 40(1)143194
4. Sato M Theoryof judgments and derivationsDiscovery Science, LNAI 2281, 2001 78122
5. Sato M Sakurai T Kameyama Y Calculi of meta-variablesProceedingsof CSL 2003, LNCS 2803, 2003 484497
6. Mason I Computingwith contextsHigher-Order and SymbolicComputation 1999 12171201
7. Hashimoto M Ohori A A typed context calculusTheoretical Computer Science 2001 266(1–2)249272
8. Sato M Sakurai T Kameyama Y A simply typed context calculus with first-class environmentsJournal of Functional and Logic Programming 2002 4141
9. Takahashi M Parallelreductions in λ-calculusJournalof Symbolic Computation 1989 7113123
10. Geuvers H Jojgov G Open proofs and open terms:a basis for interactive logicProceedingsof CSL 2002, LNCS 2471, 2002 537552
11. Talcott C A theoryof binding structures and applications to rewritingTheoretical Computer Science 1993 112(1)99143
12. Dami L A lambda-calculusfor dynamic bindingTheoretical ComputerScience 1998 192201231
13. Sands D Computingwith contexts - a simple approachElectronicNotes in Theoretical Computer Science10 1998
14. Glück R Jørgensen J Efficient multi-level generatingextensions for program specializationProceedingsof Programming Languages, Implementations, Logics and Programs (PLILP'95), LNCS 982, 1995 259278
15. Davies R A temporal-logicapproach to binding-time analysisIn: 11thAnnual IEEE Symposium on Logic in Computer Science (LICS'96) 1996 184195
16. Yuse Y Igarashi A A modal type system for multi-levelgenerating extensions with persistent codeProceedings of PPDP 2006 201212
17. Yamamoto K Okamoto A Sato M A typed lambda calculus with quasi-quotation (in Japanese)Informal Proceedings of the 4th JSSST Workshop onProgramming and Programming Languages 2003 87102
18. Nanevski A Pfenning F Pientka B Contextual modal type theoryTransactions onComputational Logic, to appear
19. Pfenning F Davies R A judgmental reconstructionof modal logicMathematical Structure inComputer Science 2001 11(4)511540
20. Gabbay M J ANEW calculus for contextsProceedings of7th Int. ACM SIGPLAN Conf. on Principles and Practice of DeclarativeProgramming 2005 94105
21. Hamana M Free Σ-Monoids:a higher-order syntax with metavariablesProceedings of APLAS 2004 348363