Calculi of meta-variables

doi:10.1007/s11704-008-0011-1

Front. Comput. Sci.

2008, Vol. 2

Issue (1) : 12-21 https://doi.org/10.1007/s11704-008-0011-1

Calculi of meta-variables

SATO Masahiko¹, IGARASHI Atsushi¹, SAKURAI Takafumi², KAMEYAMA Yukiyoshi³

1.Graduate School of Informatics, Kyoto University; 2.Department of Mathematics and Informatics, Chiba University; 3.Department of Computer Science, University of Tsukuba

Download: PDF(168 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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.

Issue Date: 05 March 2008

Cite this article:

SATO Masahiko,SAKURAI Takafumi,KAMEYAMA Yukiyoshi, et al. Calculi of meta-variables[J]. Front. Comput. Sci., 2008, 2(1): 12-21.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-008-0011-1
https://academic.hep.com.cn/fcs/EN/Y2008/V2/I1/12

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

Viewed

Full text

Abstract

Cited

Shared

Discussed