Calculi of Meta-variables^{⋆}

Masahiko Sato^{1}, Takafumi Sakurai^{2}, Yukiyoshi Kameyama^{3}, and Atsushi Igarashi^{1}

1 Graduate School of Informatics, Kyoto University

            {masahiko,igarashi}@kuis.kyoto-u.ac.jp

2 Department of Mathematics and Informatics, Chiba University

                 sakurai@math.s.chiba-u.ac.jp

3 Institute of Information Sciences and Electronics, University of Tsukuba, and JST

                     kam@is.tsukuba.ac.jp

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 metavariable. 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 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.

Keywords: meta-variable, logical framework, context, λ-calculus

1 Introduction

The notion of meta-variable is a fundamental notion both in logic and computer science. It is because both logic and computer science mainly deal with linguistic objects such as formulas, proofs, programs etc., and whenever we make a general statement about these objects we use meta-variables to refer to these objects.

⋆ This is a revised version of the paper presetned at CSL’03. We have revised section 6, because we found a simple proof of strong normalizability.

For example, if we look at any book of logic, most variables we see are metavariables. Meta-variables are also known as metamathematical variables [7] and syntactical variables [12]. However, it seems that, so far, only a very few attempts have been made to formalize the notion of meta-variable. One reason for this may be that we have to go to metameta-level to do so.

In this paper, we present two new formalizations of the concept of the metavariable. These formalizations are based on our observations of the usages of meta-variables in text books and technical papers on logic.

The first observation is from Shoenfield [12] and Kleene [7]. In these books, we find the following sentence as one of the inductive clauses which define formulas. (We have slightly modified notations from the originals.)

If x is a variable and A is a formula, then ∃x A is a formula.

In the above sentence, both ‘x’ and ‘A’ are meta-variables, and when we use the sentence as a rule which is used to construct a concrete formula, we must instantiate these meta-variables by concrete linguistic objects of the object language. Thus, for example, we may instantiate x by a concrete variable x and A by a concrete formula x = x. Then, by applying the instantiated rule, we have that ∃x x = x is a formula. Here, it is important to remark that the process of instantiation we just described is a form of substitution, but, unlike ordinary substitutions, the variables being substituted are meta-variables. There is another subtle point in this substitution process. To see this, we analyze the above instantiation process in two steps. Namely, we assume that the meta-variable ‘x’ is first instantiated and then, in the second step, the meta-variable ‘A’ is instantiated. Then, after the first step, we get the following sentence.

If x is a variable and A is a formula, then ∃x A is a formula.

In the second step, we substitute x = x for A in the above sentence, and we get the fully instantiated sentence:

If x is a variable and x = x is a formula, then ∃xx = x is a formula.

We note here that, unlike ordinary substitution, we have substituted x = x for A in ∃x A without following the usual convention of renaming the name of the binding variable (x in this case) to avoid the capture of free variables.

The second observation we now make is also a very common one. Often in the literature, notation like A(x) is used to indicate a formula where free occurrences of x in A(x) is implicitly understood. Thus, if t is a term, then A(t) stands for a formula which is obtained from A(x) by substituting t for x in A(x). In this usage, ‘x’, ‘t’ and ‘A’ are all meta-variables and the first two meta-variables range over variables and terms in the object language. As for the third meta-variable ‘A’ it is possible to interpret its range in two ways.

The first interpretation is to regard ‘A’ as ranging over functions which, when applied to terms, will yield formulas. In this interpretation A(t) denotes the result of applying the meta-level function A to a term t. So, in this interpretation, A is a metameta-variable, since its denotation is not a linguistic object of the object language but it is a function in the meta language.

The second interpretation is to regard ‘A’ as ranging over abstracts of the object language which can be instantiated to formulas by supplying terms of the object language. This interpretation is possible only if the object language contains such abstracts as its formal entities. Higher-order abstract syntax employed by, e.g., Edinburgh LF [5] is based on this interpretation.

In this paper, we will introduce two typed calculi λM and λm, which are respectively designed based on the above two observations. In λM and λm, with each variable a non-negative integer, which we call the level of the variable, is associated. We consider level 0 as the object-level, level 1 as the meta-level, level 2 as the metameta-level and so on.

In these formalizations, we believe that we can take virtually any formal system as the object-level of our systems. However, for the sake of concrete presentation, we take as the object-level a system of symbolic expressions we introduced in Sato [10] which is simple but powerful enough to represent syntax of many of the commonly used formal systems such as the λ-calculus and predicate calculus. Both λM and λm will be constructed on top of this object-level system by adding higher-level structures, and we will show that these calculi enjoy nice properties such as confluence and strong normalizability. We will also show that the calculus λM can represent the notion of context naturally since a context, which is an expression containing some holes in it, is inherently a linguistic object in the meta-level and not in the object-level.

2 Informal Introduction to the Calculi

In this section we informally explain the two calculi λM and λm which we propose in this paper. We assume our object language contains constants, abstraction ((x)[M]), and pair (⟨M, N⟩). Abstraction and application in the meta-level are denoted by λX.M and MN. (We often use capital letters for meta-variables in examples, although both object- and meta-level variables belong to the same syntactic category in the formal definition.)

2.1 The Calculus λM

The first calculus λM is based on the first observation in Section 1. Let us consider the first observation again and assume that we have just completed the first step. Then, we have the expression ∃x A. We can represent this expression by ⟨′∃′, (x^{0})[A^{1}]⟩ using a constant ′∃′. On the shoulder of a variable, we write a natural number to indicate its level, although we often omit the level if it is clear from the context. So, we simply write x for x^{0} and it corresponds to the concrete object-level variable x. In λM, the instantiation process of the meta-variable A by the object-level formula x = x can be represented as the reduction process of the following β-redex:

(λA. ⟨′∃′, (x)[A]⟩)⟨′=′, ⟨x, x⟩⟩.

In the reduction, as pointed out in Section 1, non-standard substitution is performed and we get:

⟨′∃′, (x)[⟨′=′, ⟨x, x⟩⟩]⟩

which represents the formula ∃x x = x as expected. Note that the object-level variable x is captured through the substitution.

The non-standard (textual) substitution we have just introduced gives rise to the following two technical problems.

The first one is the non-confluence of the calculus. As argued in the literature on context calculi [8, 6, 11], calculi that have textual substitution cannot be confluent unless we restrict the evaluation order. For instance, let M be the term (λX^{2}. (λx^{1}. X^{2})y^{0})x^{1}. Depending on the evaluation-order, we will get different results y^{0} and x^{1}. Our solution to this problem is (roughly) that, a redex may not be reduced if it contains variables of higher levels than the level of the redex^{1}. In this example, the inner redex has level-1, so its reduction is postponed until the variable X^{2} disappears.

The second problem in formulating λM is that, since we restrict the evaluationorder, some reductions may get stuck. Consider the terms (λX^{2}. λx^{1}. X^{2})y^{0}z^{0}, and (λx^{1}. λX^{2}. X^{2})y^{0}z^{0}. The first term reduces to y^{0}, while the second term cannot be reduced. Since we do not consider terms like the second one meaningful, we introduce arities to rule out such terms. For instance, λx^{1}. X^{2} : 0 →_{1} 0 signifies that this term denotes a level-1 function from objects to objects. Similarly we have λX^{2}. λx^{1}. X^{2} : 0 →_{2} (0 →_{1} 0). On the other hand, λx^{1}. λX^{2}. X^{2} would have arity 0 →_{1} (0 →_{2} 0), and it would denote a level-1 function which returns a level-2 function. We will exclude such a term by defining arity properly, and show that the evaluation in λM does not get stuck (Theorem 4).

Although λM has non-standard substitution, we need the standard captureavoiding substitution as well, when the variable being substituted for and one being captured are of the same level. Let us see the following reduction:

(λX^{2}. λY^{2}. λz^{1}. X^{2})(Y^{2}z^{1}) → λW^{2}. λz^{1}. Y^{2}z^{1}

in which the variable z^{1} is captured, while the variable Y^{2} is not captured since its level is the same as that of the variable X^{2}.

2.2 The Calculus λm

The second calculus λm formalizes the first interpretation^{2} of the second observation in Section 1.

The formula A(t) can be represented as A^{2}(t^{1}) using the level-2 variable A^{2} of arity 0 →_{1} 0, and the level-1 variable t of arity 0 in λm. The existential formula ∃x A(x) is represented as:

⟨′∃′, (x^{0})[A^{2}(x^{0})]⟩),

1 The level of the redex (λX^{i}. M)N is i. 2 In this paper, we do not formalize the second interpretation in which A in A(t) ranges

over abstracts of the object language. It should be a straightforward extension of this work, but details are left for future work.

and the substitution of λx^{1} : 0. ⟨′=′, ⟨x^{1}, x^{1}⟩⟩ for A^{2} is realized by β-reduction, but this time we do not use the non-standard substitution. Hence, the term:

(λA^{2} : 0 →_{1} 0. ⟨′∃′, (x^{0})[A^{2}(x^{0})]⟩)(λx^{1} : 0. ⟨′=′, ⟨x^{1}, x^{1}⟩⟩)

reduces (using standard substitution) to

⟨′∃′, (x^{0})[⟨′=′, ⟨x^{0}, x^{0}⟩⟩]⟩

as expected.

3 The Calculus λM

In this section, we give a formal definition of the first calculus λM. The second calculus λm will be introduced in the next section.

3.1 Arities and Terms

We define arity (α) and its level (|α|) as follows:

1. 0 is an arity and |0| = 0.

2. If α and β are arities, 0 < i, |α| < i, and |β| ≤ i, then α →_{i} β is an arity and |α →_{i} β| = i.

Note that the side condition of the second clause reflects the intended notion of level introduced in Section 1. Intuitively, the arity α →_{i} β is for level-i functions from terms of arity α to terms of arity β, thus |α| < i and |β| < i must be satisfied. The restriction on β is relaxed to |β| ≤ i to allow currying.

We assume that, for each natural number i and arity α, there are infinitely many variables, and the sets of variables of each level and arity are mutually disjoint. For a variable x of level i and arity α, we sometimes write it as x^{i}. The set of all variables is denoted by V. A (variable) declaration is an expression of the form x^{i} : α, where α is an arity and either |α| < i or |α| = i = 0. We say the level of this declaration is i. A hypothesis sequence is a finite sequence of declarations. A judgment is an expression of the form Γ ⊢ M : α where Γ is a hypothesis sequence and α is an arity.

We have the following rules that are used to derive judgments.

The first rule introduces variables for each i and α, where we assume x is a variable of level i and arity α.

{x^{i} : α ∈ Γ \atop Γ ⊢ x^{i} : α} (var)

The next two rules introduce abstraction and application for level-i (i > 0).

\begin{matrix}Γ, x^{i} : α ⊢ M : β & |β| ≤ i \\ Γ ⊢ λx^{i}:α. M : α →_{i} β \end{matrix} (abs)  \begin{matrix}Γ ⊢ M : α →_{i} β & Γ ⊢ N : α \\ Γ ⊢ MN : β \end{matrix} (app)

Note that, in the rule (abs), the level of the variable x^{i} and that of the arity α →_{i} β should agree, and the side-condition |β| ≤ i is needed to form a (wellformed) arity α →_{i} β. Note also that we may not construct a term like λx^{1} :

0. λX^{2} : 0. X^{2}.

The last group of rules are those for the level-0, the object language.

c is a constant Γ ⊢ c : 0 (const0)  {Γ, x^{0} : 0 ⊢ M : 0 \atop Γ ⊢ (x^{0})[M] : 0} (abs0)

\begin{matrix}Γ ⊢ M : 0 & Γ ⊢ N : 0 \\ Γ ⊢ ⟨M, N⟩ : 0 \end{matrix} (pair0)

An expression M is said to be a term if a judgment of the form Γ ⊢ M : α is derivable for some Γ and α. We sometimes just write λx^{i}. M for λx^{i}:α. M when the arity α of x^{i} is irrelevant.

The scope of λx. and free occurrences of variables in a term are defined as usual. For a term M, the set of free variables in M is denoted by FV(M). The level of a term M, denoted by |M|, is the maximum level of variables in M, or 0 if there is no variable in M. Note that we take all variables (even variable occurrences in the scope of λ) into account—for instance, |(λx^{2}:α. x^{2})y^{1}| = 2. Note also that |M| is not necessarily equal to the level of its arity. The level of a hypothesis sequence Γ, denoted by |Γ |, is the maximum level of variables in Γ, or 0 if Γ is the empty sequence.

3.2 α-equivalence

In the calculus λM, we need special care to define α-equivalence: occurrences of a variable x in the scope of λx. – usually called bound occurrences – may or may not be subject to renaming since textual substitution does not commute with naive variable renaming. For instance, we may identify λx^{2}. y^{4}(λz^{2}. x^{2}z^{2}) with λx^{2}. y^{4}(λu^{2}. x^{2}u^{2}), but not with λw^{2}. y^{4}(λz^{2}. w^{2}z^{2}). To see its reason, let us substitute x^{2} for y^{4} in these terms. Since the level of y^{4} is higher than x^{2} and w^{2}, the textual substitution is used, and the first and the third terms become λx^{2}. x^{2}(λz^{2}. x^{2}z^{2}), and λw^{2}. x^{2}(λz^{2}. w^{2}z^{2}), resp., which do not have the same denotational meaning. Hence, we let an abstraction λx^{i}. e be α-convertible only when no variable at a level higher than i occurs in its scope.

We define the α-equivalence after a few auxiliary definitions. A renaming of variables is a partial function from V to V which is injective and satisfies |f(x^{i})| = i for all x^{i} in the domain of the partial function. For a partial function f, its domain is denoted by dom(f). For a renaming f and a variable x^{i} (which may not be in dom(f)), f ↓ x^{i} is a renaming of variables such that dom(f ↓ x^{i}) = dom(f) − {x^{i}}, and f ↓ x^{i} agrees with f on its domain.

For a renaming f and terms M and N in λM, we derive a judgment of the form f ⊢ M ≃ N by the following inference rules:

{f(x^{i}) = y^{i} \atop f ⊢ x^{i} ≃ y^{i}}  \begin{matrix}f ⊢ M ≃ M′ & f ⊢ N ≃ N′ \\ f ⊢ MN ≃ M′N′ \end{matrix}

{f ⊢ M ≃ M′ \atop f ⊢ λx^{i} : α. M ≃ λx^{i} : α. M′} (f(x^{i}) = x^{i})

{f ⊢ M ≃ M′ \atop g ⊢ λx^{i} : α. M ≃ λy^{i}. α.M′} ^{( \begin{matrix}|M| ≤ i, |M′| ≤ i, \\ f(x^{i}) = y^{i}, g ↓ x^{i} = f ↓ x^{i} \end{matrix} )}

The last rule can be applied only when both M and M′ are of level less than or equal to i. Otherwise, the term λx^{i}. M contains (not necessarily free) occurrences of meta-variables which have higher levels than i, and we cannot rename the bound variable x^{i}. In this case we can still apply the second last rule, since it does not rename the bound variable x^{i}. For brevity, we omit the inference rules for terms constructed by the rules (const0), (abs0), and (pair0), which are similarly defined. For instance, a term (x^{0})[M] has the same rules as the term λx^{i} : α. M.

Let id be the identity function on V. If id ⊢ M ≃ N is derived by the rules above, we say M is α-equivalent to N (written by M ≡_{α} N). It is easy to show the relation ≡_{α} is a congruence on terms.

3.3 Substitution and Reduction

The notion of reduction in the calculus λM is the union of those in the object language (which we do not specify) and the following β-reduction:

(β) (λx^{i}. M)N → [x^{i} := N]M if |M| ≤ i and |N| ≤ i

in which [x^{i} := N]M denotes the (non-standard) substitution defined below. We write →^{∗} for the reflexive and transitive closure of →.

For a level i > 0, a level-i variable x^{i}, and terms M and N such that |M| ≤ i and |N| ≤ i, we define [x^{i} := N]M as follows:

1. [x^{i} := N]x^{i} =^{△} N

2. [x^{i} := N]y^{j} =^{△} y^{j} if y^{j} ≢ x^{i}

3. [x^{i} := N](M_{1}M_{2}) =^{△} ([x^{i} := N]M_{1})([x^{i} := N]M_{2})

4. [x^{i} := N](λy^{j}. M) =^{△} λy^{j}. [x^{i} := N]M if j < i

5. [x^{i} := N](λy^{i}. M) =^{△} λy^{i}. [x^{i} := N]M if y^{i} ∉ FV(N) and x^{i} ≢ y^{i}

6. [x^{i} := N]c =^{△} c

7. [x^{i} := N](y^{0})[M] =^{△} (y^{0})[[x^{i} := N]M]

8. [x^{i} := N]⟨M_{1}, M_{2}⟩ =^{△} ⟨[x^{i} := N]M_{1}, [x^{i} := N]M_{2}⟩

The first three clauses are standard. For the fourth line, if the level of y^{j} is strictly less than that of x^{i}, the substitution behaves like textual replacement, that is, free variables may get captured through this substitution. For the fifth line, the bound variable y^{i} has the same level as x^{i} that is being substituted, in which case the substitution is the standard capture-avoiding one, hence the side-conditions y^{i} ∉ FV(N) and x^{i} ≢ y^{i} must be satisfied. (The second sidecondition x ≢ y is not needed for the fourth clause because variables at different levels are assumed to be different.) This side-condition can be always satisfied by taking an α-equivalent term. The last three clauses deal with the level 0 in a straightforward manner, except textual substitution.

For brevity, we identify α-equivalent terms in the following. Under this convention, we simply have that [x^{i} := N]M is defined if and only if max(|M|, |N|) ≤ i.

The object-level may contain other redices than the β-redices in the above form, and to distinguish these two, we say that a redex (λx^{i} : α. M)N is a metaredex. A term is meta-normal if it does not have meta-redices and a reduction is called a meta-reduction if its redex is a meta-redex.

3.4 Replacing Level-0 Languages

Our level-0 language here is a simplest possible language, which has no notion of types or even computation. We have adopted such a language because it is simple but expressible enough to represent expressions that appear in typical logical systems. It would be possible, however, to adopt other languages such as untyped and simply typed λ-calculi as the level-0 language.

For example, for untyped λ-calculus, we could introduce another term constructor M_{1} · M_{2} by the rule

\begin{matrix}Γ ⊢ M : 0 & Γ ⊢ N : 0 \\ Γ ⊢ M · N : 0 \end{matrix} (app0)

and a reduction rule (x^{0})[M] · N → [x^{0} := N]M (if |M| = |N| = 0) where the level-0 substitution would be defined as expected. It would be also straightforward to substitute the simply typed λ-calculus for the level-0 language, by extending the base arities from 0 to the set of simple types.

4 The Calculus λm

As discussed in the previous sections, the second calculus λm is based on the second observation discussed in the introduction. It is obtained from λM by replacing the definition of substitution with the standard capture-avoiding one. Also, we need to use the standard definition of α-equivalence to identify λx^{1}.y^{2}(λz^{1}.x^{1}z^{1}) with λw^{1}.y^{2}(λz^{1}.w^{1}z^{1}), which are not α-equivalent in λM. Since the other definitions of arities, rules to derive judgments, β-reduction remain the same, we avoid repeating definitions and just show changes to be made.

For α-equivalence, we replace the third and fourth rules to derive f ⊢ M ≃ N with the following one:

{f ⊢ M ≃ M′ \atop g ⊢ λx^{i} : α.M ≃ λy^{i} : α.M′} (f(x^{i}) = y^{i}, g ↓ x^{i} = f ↓ x^{i})

Notice that there is no restriction on the levels of the bodies M and M′ of λ-abstraction. Similarly, the definition of substitution will be as follows.

For a level i > 0, a level-i variable x^{i}, and terms M and N such that |M| ≤ i and |N| ≤ i, [x^{i} := N]M is defined by:

1. [x^{i} := N]x^{i} =^{△} N

2. [x^{i} := N]y^{j} =^{△} y^{j} if y^{j} ≢ x^{i}

3. [x^{i} := N](M_{1}M_{2}) =^{△} ([x^{i} := N]M_{1})([x^{i} := N]M_{2})

4. [x^{i} := N](λy^{j}. M) =^{△} λy^{j}. [x^{i} := N]M if y^{j} ∉ FV(N) and x^{i} ≢ y^{j}

5. [x^{i} := N]c =^{△} c

6. [x^{i} := N](y^{0})[M] =^{△} (y^{0})[[x^{i} := N]M] if y^{0} ∉ FV(N)

7. [x^{i} := N]⟨M_{1}, M_{2}⟩ =^{△} ⟨[x^{i} := N]M_{1}, [x^{i} := N]M_{2}⟩

Notice that the first three clauses are the same as before and the fourth clause is now a familiar one that avoids variable capturing.

5 Examples

In this section, we show a few examples of λM and λm.

5.1 Representing Formulas

In earlier sections, we informally explained how the formula x = x is substituted for the meta-variable A in ∃x A. Here we consider this process formally in λM.

The arity of the corresponding term is inferred in λM as follows:

\begin{matrix}\begin{matrix}x^{0} : 0, A^{1} : 0 ⊢ ′∃′ : 0 & {x^{0} : 0, A^{1} : 0, x^{0} : 0 ⊢ A^{1} : 0 \atop x^{0} : 0, A^{1} : 0 ⊢ (x^{0})[A^{1}] : 0} \\ x^{0} : 0, A^{1} : 0 ⊢ ⟨′∃′, (x^{0})[A^{1}]⟩ : 0 \end{matrix} ; x^{0} : 0 ⊢ λA^{1} : 0. ⟨′∃′, (x^{0})[A^{1}]⟩ : 0 →_{1} 0 & ⋮ . ; x^{0} : 0 ⊢ ⟨′=′, ⟨x^{0}, x^{0}⟩⟩ : 0 \\ x^{0} : 0 ⊢ (λA^{1} : 0. ⟨′∃′, (x^{0})[A^{1}]⟩)(⟨′=′, ⟨x^{0}, x^{0}⟩⟩) : 0 \end{matrix}

Note that, the variable x^{0} occurs free in the term of the conclusion, as indicated by the hypothesis sequence.

We can compute this term as:

(λA^{1} : 0. ⟨′∃′, (x^{0})[A^{1}]⟩)(⟨′=′, ⟨x^{0}, x^{0}⟩⟩)
→ [A^{1} := ⟨′=′, ⟨x^{0}, x^{0}⟩⟩]⟨′∃′, (x^{0})[A^{1}]⟩
≡ ⟨′∃′, [A^{1} := ⟨′=′, ⟨x^{0}, x^{0}⟩⟩](x^{0})[A^{1}]⟩
≡ ⟨′∃′, (x^{0})[⟨′=′, ⟨x^{0}, x^{0}⟩⟩]⟩

Note that non-standard (textual) substitution is applied in the last step, since the level of A^{1} is higher than that of x^{0}. As a result, the free occurrences of x^{0} get bound, and x^{0} does not occur free in the resulting term, which represents the formula ∃xx = x.

We also informally explained how the same example can be written in λm. Its formal counterpart can be written as follows^{3}:

\begin{matrix}\begin{matrix}A^{2} : 00 ⊢ ′∃′ : 0 & \begin{matrix}Γ ⊢ A^{2} : 00 & Γ ⊢ x^{0} : 0 \\ Γ ⊢ A^{2}(x^{0}) : 0 \end{matrix} ; A^{2} : 00 ⊢ (x^{0})[A^{2}(x^{0})] : 0 \\ A^{2} : 00 ⊢ ⟨′∃′, (x^{0})[A^{2}(x^{0})]⟩ : 0 \end{matrix} ; ⊢ λA^{2} : 00. ⟨′∃′, (x^{0})[A^{2}(x^{0})]⟩ : 00 →_{2} 0 & ⋮ . ; y^{1} : 0 ⊢ ⟨′=′, ⟨y^{1}, y^{1}⟩⟩ : 0 ; ⊢ λy^{1} : 0. ⟨′=′, ⟨y^{1}, y^{1}⟩⟩ : 00 \\ ⊢ (λA^{2} : 00. ⟨′∃′, (x^{0})[A^{2}(x^{0})]⟩)(λy^{1} : 0. ⟨′=′, ⟨y^{1}, y^{1}⟩⟩) : 0 \end{matrix}

where we put an arity 00 = 0 →_{1} 0 and Γ = A^{2} : 0 →_{1} 0, x^{0} : 0 Note that we replaced the meta-variable A^{1} in λM by an application term A(x), and to ensure this application is resolved in a meta-level, the arity of A should be 0 →_{1} 0, hence the level of the variable A must be 2 (or higher).

We omit the computation of the term here, since it is essentially the same as the standard β-reduction.

5.2 Representing Contexts

Contexts can be represented in λM using meta-variables naturally. Let M be a term, C be a context in the object language, i.e., a term with a hole [ ] in it, and C[M] be the result of the hole-filling operation. In λM, the context C is represented as a term \overline{C} ≡ (λX^{1}:0. C[X^{1}]), and C[M] as an application (\overline{C}M), which reduces to C[M] by the textual substitution in λM.

Let us take an example from Hashimoto and Ohori’s context calculus [6]. Consider the context C ≡ (λu. (λx. [ ])u + y)3 and the term M ≡ (λz. C[x + z])x in lambda calculus. They can be written in λM (using our notation for object language) as:

\overline{C} ≡ λX^{1}:0. (u^{0})[((x^{0})[X^{1}] · u^{0}) + y^{0}] · 3
\overline{M} ≡ (z^{0})[\overline{C} (x^{0} + z^{0})] · x^{0}

We can reduce \overline{M} as:

\overline{M} → (z^{0})[[X^{1} := x^{0} + z^{0}]((u^{0})[((x^{0})[X^{1}] · u^{0}) + y^{0}] · 3)] · x^{0}
≡ (z^{0})[(u^{0})[((x^{0})[x^{0} + z^{0}] · u^{0}) + y^{0}] · 3] · x^{0}
→^{∗} 3 + x^{0} + y^{0}

Note that, by the side-condition of the β-reduction, we cannot reduce the outermost level-0 redex first. If it would be reduced first, we would get 3+x^{0} +x^{0} as a result, so the Church-Rosser property would be broken. Hashimoto and Ohori’s context calculus has a similar restriction that the β-reduction is prohibited when the redex contains a hole.

3 We changed the level-1 variable x^{1} to y^{1} for readability. Formally this renaming is justified by the α-equivalence.

A good point of our representation of contexts is that, since contexts are functions, they can be composed, in other words, we can fill a context in another context. As a simple example, let C and D be the contexts λx. [ ] and λy. [ ] in lambda calculus, and consider hole-filling of D in C, i.e. C[D]. The contexts C and D are represented in λM as \overline{C} ≡ λX^{1}. (x^{0})[X^{1}] and \overline{D} ≡ λX^{1}. (y^{0})[X^{1}], then we can compose them in the same way as composition of two functions:

\overline{C} ∘ \overline{D} ≡ λX^{1}. \overline{C} (\overline{D} X^{1})

\overline{C} ∘ \overline{D} reduces to λX^{1}. (x^{0})[(y^{0})[X^{1}]] which represents the context λx. λy. [ ]. It should be noted that, in several existing context calculi including Hashimoto-Ohori’s and our previous work [11], contexts cannot be composed, since these calculi keep track of possible bound variables in a hole.

6 Properties of λM and λm

We have a number of desirable properties for the calculi λM and λm, that is, they enjoy subject reduction, confluence, and strong normalization properties. In the following, we focus on the properties of λM, but the modification for λm is straightforward.

We can prove the subject reduction property in the standard way.

Theorem 1 (Subject Reduction Property). If Γ ⊢ M : α is derived and M →^{∗} N, then Γ ⊢ N : α can be derived.

Note that even if Γ ⊢ (λx^{i}. M)N : α is derived, [x^{i} := N]M is not necessarily defined. But we can prove from Theorem 2 and 3 that if |Γ | ≤ i then there exist terms M′ and N′ such that M →^{∗} M′, N →^{∗} N′, and [x^{i} := N′]M′ is defined.

Lemma 1. Suppose Γ ⊢ M : α is derived and the highest level of the redices of M is i. Then, any reduction sequence that reduces only level-i redices leads to a term that does not have redices of level-i or higher.

Proof. (sketch) We can prove this lemma by reducing it to the strong normalizability of the simply typed λ-calculus. We translate λM to the simply typed λ-calculus by mapping a level-i abstraction λx^{i}. M to an abstract of the simply typed λ-calculus and a level-j (j < i) abstraction λx^{j}. M to a pair of x^{j} and M. ⊓ ⊔

Note that, we cannot simply map λ-abstractions of λM to those of the simply typed λ-calculus, since the textual substitution cannot be simulated by the capture-avoiding substitution in the standard calculi.

Theorem 2 (Strong Normalizability). If Γ ⊢ M : α is derived, then M is strongly normalizable with respect to the meta-reduction.

Proof. Suppose we have an infinite sequence of reductions starting from M. Let L_{1} → L_{2} → L_{3} be the first two consecutive reductions in the sequence such that the redex in L_{1} is (λx^{i}. M_{1})N_{1}, the redex in L_{2} is (λy^{j}. M_{2})N_{2}, and i < j. Since |[x^{i} := N_{1}]M_{1}| ≤ i < j = |(λy^{j}. M_{2})N_{2}|, (λy^{j}. M_{2})N_{2} cannot be a subterm of [x^{i} := N_{1}]M_{1} in L_{2}. Therefore, we have three cases.

1. [x^{i} := N_{1}]M_{1} is a subterm of M_{2}: Let M′_{2} be the term (in L_{1}) obtained by replacing [x^{i} := N_{1}]M_{1} in M_{2} with (λx^{i}. M_{1})N_{1}. Since (λx^{i}. M_{1})N_{1} cannot contain y^{j}, (λx^{i}. M_{1})N_{1} is unchagned by the reduction of (λy^{j}. M′_{2})N_{2}. Therefore, we can reduce (λy^{j}. M′_{2})N_{2} first and (λx^{i}. M_{1})N_{1} next. Then, we have L_{3}.

2. [x^{i} := N_{1}]M_{1} is a subterm of N_{2}: Let N′_{2} be the term (in L_{1}) obtained by replacing [x^{i} := N_{1}]M_{1} in N_{2} with (λx^{i}. M_{1})N_{1}. Then, [y^{j} := N′_{2}]M_{2} may have 0 or more (λx^{i}. M_{1})N_{1}. By reducing these redices, we have L_{3}.

3. Otherwise: In this case, both (λx^{i}. M_{1})N_{1} and (λy^{j}. M_{2})N_{2} are subterms of L_{1} and one is not a subterm of the other. So, we can reduce (λy^{j}. M_{2})N_{2} first and (λx^{i}. M_{1})N_{1} next. Then, we have L_{3}.

By repeating this, we have an infinite reduction sequence such that the levels of the redices are decreasing. But this contradicts to Lemma 1. ⊓ ⊔

Proposition 1. If Γ ⊢ M : α, then |M| ≥ |α|.

Proof. By induction on the derivation of Γ ⊢ M : α. ⊓ ⊔

Theorem 3. If Γ ⊢ M : α is derived and M is meta-normal, then |M| ≤ max(|Γ |, |α|).

Proof. Suppose M is a meta-normal term. We prove the theorem by induction on M.

1. If M is x^{i}N_{1} ⋯ N_{n} for some i ≥ 0, x^{i}, n ≥ 0, N_{0}, ⋯, N_{n}, then the arity of x^{i} should be γ ≡ β_{1} →_{j_{1}} β_{2} →_{j_{2}} ⋯ →_{j_{n}} β_{n} →_{i} α where β_{k} is the arity of N_{k} for k = 1, ⋯, n. By induction hypothesis, |N_{k}| ≤ max(|Γ |, |β_{k}|), so we have:

|M| = max(i, |N_{1}|, ⋯, |N_{n}|)
≤ max(i, |Γ |, |β_{1}|, ⋯, |β_{n}|)
≤ max(i, |Γ |, |γ|)
= |Γ |

2. If M is (λx^{i}:β_{1}. N_{0})N_{1} ⋯ N_{n} for some i ≥ 0, x^{i}, β_{1}, n ≥ 0, N_{0}, ⋯, N_{n}, then the arity of N_{0} should be γ ≡ β_{2} →_{j_{2}} ⋯ →_{j_{n}} β_{n} →_{i} α where β_{k} is the arity of N_{k} for k = 2, ⋯, n. Since N_{0} is meta-normal, we have |N_{0}| ≤ max(|Γ |, i, |γ|) by induction hypothesis, and |γ| ≤ i by the side-condition of rule (abs). Therefore, we have

|λx^{i}:β_{1}. N_{0}| = max(i, |N_{0}|) ≤ max(i, |Γ |)

Now, we have two cases.

(a) n = 0. |M| ≤ max(i, |Γ |) = max(|β_{1} →_{i} γ|, |Γ |).

(b) n > 0. We have, by induction hypothesis, |N_{k}| ≤ max(|Γ |, |β_{k}|) for 1 ≤ k ≤ n. Hence |N_{1}| ≤ max(|Γ |, i). Since M is meta-normal, max(|N_{0}|, |N_{1}|) > i. Hence |Γ | > i. Since |γ| ≥ |β_{k}|, we have |N_{k}| ≤ |Γ | for 1 ≤ k ≤ n. Hence |M| ≤ |Γ |.

3. If M is a constant c, (x^{0})[N_{0}], or ⟨N_{0}, N_{1}⟩, the theorem can be proved easily by induction hypothesis. ⊓ ⊔

The following theorem ensures that meta-level evaluation in λM does not get stuck.

Theorem 4 (Normal Form Property). Suppose Γ ⊢ M : α is derived and M is meta-normal. (1) If |Γ | = |α| = 0, then |M| = 0. (2) If |Γ | < |α|, then M is a λ-abstraction.

Proof. (1) Clear from Theorem 3. (2) If M is not a λ-abstraction, then it must be of the form x^{i}N_{1}N_{2} ⋯ N_{n} or (λx^{i}:γ. N_{0})N_{1}N_{2} ⋯ N_{n} for n ≥ 0. In the former case, |α| ≤ |x^{i}| ≤ |Γ |. Contradiction. In the latter case, let β be the arity of N_{0}. From Theorem 3, |(λx^{i} : γ.N_{0})N_{1}| ≤ |β|. By the side-condition of rule (abs), |β| ≤ i. Hence |N_{0}| ≤ i and |N_{1}| ≤ i, which implies (λx^{i}:γ. N_{0})N_{1} is a redex. Contradiction. ⊓ ⊔

We can prove the confluence λM using the standard technique (parallel reduction).

Lemma 2 (Substitution Lemma). Let x^{i} and y^{i} be distinct variables, |M_{0}| ≤ i, |M_{1}| ≤ i, and |N| ≤ i. Then we have

[x^{i} := N][y^{i} := M_{1}]M_{0} ≡ [y^{i} := [x^{i} := N]M_{1}][x^{i} := N]M_{0}

Theorem 5 (Confluence). The meta-reduction is confluent.

We remark that, for many object languages such as the simply typed lambda calculus, these theorems still hold if we replace the meta-reduction by the union of the meta-reduction and the reductions in the object language.

7 Related Work and Conclusion

We have proposed two formal systems λM and λm that formalize the notion of meta-variable, motivated by the observations how meta-variables are used in textbooks of logic.

Edinburgh Logical Framework (LF) [5] gives a typed framework by which we can define various logical systems as object calculi. Unlike LF and its descendants, we clearly distinguish the meta-levels from the object-level. The textual substitution in λM is another characteristic feature.

Geuvers and Jogjov [3] have introduced the notion of meta-variable into the proof assistant system, so that they can describe open proofs. Their motivation is similar to ours, so they have also encountered the problem that free variables are captured when a meta-variable is instantiated. Their solution to this problem is similar to the one in our work on the calculus of context [11].

Recently much effort has been devoted to formalize the notion of context in lambda calculi, and various calculi of context have been proposed. In the work of Talcott [13] and Mason [8], the notion of contexts are formalized outside of the object language, because contexts are meta-level objects in nature and should be characterized independently of the object language. In other work such as Dami [1], Hashimoto-Ohori [6], Sands [9], and Sato-Sakurai-Kameyama [11], contexts are built into the system, so that context manipulations and objectlevel calculations can be carried out in the same framework. By representing contexts in λM, we have integrated the two approaches.

It turns out that λm is similar to the calculi for binding-time analysis in offline partial evaluation with multiple computation stages [4, 2]. In those calculi, types are stratified like ours but, there, levels represent binding time—i.e., when certain expression can be computed. Reduction is similar to ours in that the order of computation is also determined by levels. Aside from the base language (for which they use typed or untyped λ-calculus), one subtle difference is that, in those calculi, variables can range over expressions of the same level, resulting in a relaxed condition on function types: α →_{i} β is a type if |α| ≤ i (not |α| < i), and |β| ≤ i.

Davies [2] also presents a reformulation λ^{◯} of the calculus for binding-time analysis and shows that it corresponds to a proof system of linear-time temporal logic with a modal operator. Actually, our earlier attempt to formalize metavariables [14] was done in a close style. In these calculi, terms are annotated with information that indicates levels of subexpressions, hence λm is a simpler calculus to formalize meta-variables.

As far as we know, the calculus λM is the first one which formalizes nonstandard (textual) substitution and is confluent and strongly normalizing. We believe that our calculi can be a basis of formalizing logical and computation systems naturally and directly, but their further development is left for future work.

Acknowledgements: We thank anonymous referees for helpful comments. The first author thanks Henk Barendregt and Jan Willem Klop for having discussions on metavariables with him. This work is supported in part by Grant-in-Aid for Scientific Research on Priority Areas Research No. 15017247 (Sato, Sakurai) and Grant-in-Aid for Young Scientists (B) No. 15700011 (Igarashi), from MEXT of Japan.

References

1. L. Dami. A Lambda-Calculus for Dynamic Binding. Theoretical Computer Science, 192:201–231, 1998.

2. R. Davies. A Temporal-Logic Approach to Binding-Time Analysis. In 11th Annual IEEE Symposium on Logic in Computer Science (LICS’96), pages 184–195, 1996.

3. H. Geuvers and G. Jojgov. Open Proofs and Open Terms: A Basis for Interactive Logic. In CSL 2002, LNCS 2471, pages 537–552, 2002.

4. R. Glück and J. Jørgensen. Efficient multi-level generating extensions for program specialization. In Programming Languages, Implementations, Logics and Programs (PLILP’95), LNCS 982, pages 259–278, 1995.

5. R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. Journal of the Association for Computing Machinery, 40(1):143–194, 1993.

6. M. Hashimoto and A. Ohori. A Typed Context Calculus. Theoretical Computer Science, 266(1-2):249–272, 2001.

7. S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952.

8. I. Mason. Computing with Contexts. Higher-Order and Symbolic Computation, 12:171–201, 1999.

9. D. Sands. Computing with Contexts - a Simple Approach. Electronic Notes in Theoretical Computer Science, 10, 1998.

10. M. Sato. Theory of Judgments and Derivations. In Discovery Science, LNAI 2281, pages 78–122, 2001.

11. M. Sato, T. Sakurai, and Y. Kameyama. A Simply Typed Context Calculus with First-Class Environments. Journal of Functional and Logic Programming, 2002(4):1–41, 2002.

12. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967.

13. C. Talcott. A Theory of Binding Structures and Applications to Rewriting. Theoretical Computer Science, 112(1):99–143, 1993.

14. K. Yamamoto, A. Okamoto, M. Sato, and A. Igarashi. A Typed Lambda Calculus with Quasi-quotation (in Japanese). In Informal Proceedings of the 4th JSSST Workshop on Programming and Programming Languages, pages 87–102, 2003.