9. Theory Interpretations

9.1 Introduction

Theory Interpretations are translations which map the expressions from one theory to the expressions of another with the property that theorems are mapped to theorems. They serve as conduits to pass results from one theory to another. As such, they are an essential ingredient in the little theories version of the axiomatic method which IMPS supports (see Section 3.7). The IMPS notion of theory interpretation [5,7] is modeled on the standard approach to theory interpretation in first-order logic (e.g., see [2,19,24]).

Most of the various ways that interpretations are used in IMPS are described in the penultimate section of this chapter.

  
9.2 Translations

Let $\mbox{$\cal T$ }_1$ and $\mbox{$\cal T$ }_2$ be LUTINS theories. A translation from $\mbox{$\cal T$ }_1$ to $\mbox{$\cal T$ }_2$ is a pair $\Phi=(\mu,\nu)$, where $\mu$ is a mapping from the atomic sorts of $\mbox{$\cal T$ }_1$ to the sorts, unary predicates (quasi-sorts), and indicators (sets) of $\mbox{$\cal T$ }_2$ and $\nu$is a mapping from the constants of $\mbox{$\cal T$ }_1$ to the expressions of $\mbox{$\cal T$ }_2$, satisfying certain syntactic conditions. $\mbox{$\cal T$ }_1$ and $\mbox{$\cal T$ }_2$are called the source theory and target theory of $\Phi$, respectively. Given an expression e of $\mbox{$\cal T$ }_1$, the translation of e via $\Phi$, written $\Phi(e)$, is an expression of $\mbox{$\cal T$ }_2$ defined from $\mu$ and $\nu$ in a manner that preserves expression structure. In particular, $\Phi(e)$ is a sentence when e is a sentence.

When $\mu$ maps an atomic sort $\alpha$ to a unary predicate U, the variable binding constructors--$\lambda$, $\forall$, $\exists$, and $\iota$--are ``relativized'' when they bind a variable of sort $\alpha$. For example,

$$\Phi(\forall{x\mbox{:}\alpha}.\psi) = \forall{x\mbox{:}\beta}.U(x) \supset \Phi(\psi).$$

Something very similar happens when $\mu$ maps an atomic sort to an indicator. The constructor defined-in is also relativized when its second argument is $\alpha$. A translation is normal if it maps each atomic sort of the source theory to a sort of the target theory. Normal translations do not relativize constructors.

Let $\Phi$ be a translation from $\mbox{$\cal T$ }_1$ to $\mbox{$\cal T$ }_2$. $\Phi$ is an interpretation of $\mbox{$\cal T$ }_1$ in $\mbox{$\cal T$ }_2$ if $\Phi(\varphi)$ is a theorem of $\mbox{$\cal T$ }_2$ for each theorem $\varphi$ of $\mbox{$\cal T$ }_1$. In other words, an interpretation is a translation that maps theorems to theorems. An obligation of $\Phi$ is a formula $\Phi(\varphi)$where $\varphi$ is either:

1.

a primitive axiom of $\mbox{$\cal T$ }_1$ (axiom obligation);

2.

a definition axiom of $\mbox{$\cal T$ }_1$ (definition obligation);

3.

a formula asserting that a particular primitive atomic sort of $\mbox{$\cal T$ }_1$ is nonempty (sort nonemptiness obligation);

4.

a formula asserting that a particular primitive constant of $\mbox{$\cal T$ }_1$ is defined in its sort (constant sort obligation); or

5.

a formula asserting that a particular primitive atomic sort of $\mbox{$\cal T$ }_1$ is a subset of its enclosing sort (sort inclusion obligation).

The following theorem gives a sufficient condition for a translation to be an interpretation:

Theorem 9.2.1 (Interpretation Theorem)   A translation $\Phi$ from $\mbox{$\cal T$ }_1$ to $\mbox{$\cal T$ }_2$ is an interpretation if each of its obligations is a theorem of T₂.

See [5,7], for a more detailed discussion of theory interpretations in LUTINS.

9.3 Building Theory Interpretations

The most direct way for you to build an interpretation is with the def-translation form. However, there are also several ways interpretations can be built automatically by IMPS with little or no assistance from you.

Building an interpretation with def-translation is generally a two-step process. The first step is to build a translation by evaluating a def-translation form which contains a specified name, source theory, target theory, sort association list, and constant association list. These latter lists, composed of pairs, specify respectively the two functions $\mu$ and $\nu$ discussed in the previous section. Each pair in the sort association list consists of an atomic sort of the source theory and a specification of a sort, unary predicate, or indicator of the target theory. Each pair in the constant association list consists of a constant of the source theory and a specification of an expression of the target theory. There does not need to be a pair in the sort association list for each atomic sort in the source theory; missing primitive atomic sorts are paired with themselves and missing defined atomic sorts are handled in the special way described in the next section. A similar statement is true about the constant association list.

When the def-translation form is evaluated, IMPS does a series of syntactic checks to make sure that the form correctly specifies a translation. If all the checks are successful, IMPS builds the translation (or simply retrieves it if it had been built previously).

The second step is to verify that the translation is an interpretation. IMPS first generates the obligations of the translation that are not trivially theorems of the target theory. Next IMPS removes from this set those obligations which are instances of installed theorems of the target theory. If the line

   (theory-interpretation-check using-simplification)

is part of the def-translation form, IMPS will also remove obligations which are known to be theorems of the target theory by simplification. When IMPS is done working on the obligations, if there are none left the translation is marked as a theory interpretation. Otherwise, an error message is made that lists the outstanding obligations.

If there are outstanding obligations (and you believe that they are indeed theorems of the target theory), you will usually want to prove them in the target theory. Then, after installing them in the target theory, the def-translation form can be re-evaluated.

The following is a simple example of an interpretation built from a def-translation form:

   (def-translation MONOID-THEORY-TO-ADDITIVE-RR
     (source monoid-theory)
     (target h-o-real-arithmetic)
     (fixed-theories h-o-real-arithmetic)
     (sort-pairs
      (uu rr))
     (constant-pairs
      (e 0)
      (** +)
     (theory-interpretation-check using-simplification))

The purpose of the line

   (fixed-theories h-o-real-arithmetic)

is to speed up the construction of the interpretation by telling IMPS ahead of time that the theory h-o-real-arithmetic, which is a subtheory of monoid-theory, is fixed by the translation, i.e., each expression of h-o-real-arithmetic is mapped to itself.

   
9.4 Translation of Defined Sorts and Constants

Let $\Phi$ be a translation from $\mbox{$\cal T$ }_1$ to $\mbox{$\cal T$ }_2$. Translations have been implemented in IMPS so that the defined sorts and constants of $\mbox{$\cal T$ }_1$ are handled in an effective manner, even when they are defined after $\Phi$ is constructed. There are three possible ways that a defined sort or constant of $\mbox{$\cal T$ }_1$ can be translated.

First, if the defined sort or constant is a member of one of the fixed theories of $\Phi$, it is translated to itself. Second, if the defined sort or constant is mentioned (i.e., is the first component of a pair) in the sort or constant association list of $\Phi$, it is translated to the second component of the pair. In practice, most defined sorts and constants are not mentioned in the sort and constant association lists. And, third, if the defined sort or constant is not mentioned in the sort and constant association lists and is not a member of a fixed theory, it is translated on the basis of its definiens (unary predicate, expression, or list of functionals). This last way of translation requires some explanation.

Suppose $\alpha$ is a defined sort of $\mbox{$\cal T$ }_1$ which is not mentioned in the sort association list of $\Phi$. Let U be the unary predicate that was used to define $\alpha$. If there is a atomic sort $\beta$ of $\mbox{$\cal T$ }_2$ defined by a unary predicate U' such that U' and $\Phi(U)$ are alpha-equivalent, then $\alpha$ is translated as if the pair $(\alpha,\beta)$ were in the sort association list of $\Phi$. Otherwise, it is translated as if the pair $(\alpha,\Phi(U))$were in the sort association list of $\Phi$.

Suppose a is a directly defined constant of $\mbox{$\cal T$ }_1$ which is not mentioned in the constant association list of $\Phi$. Let e be the expression that was used to define a. If there is a constant b of $\mbox{$\cal T$ }_2$ directly defined by an expression e' such that e'and $\Phi(e)$ are alpha-equivalent, then a is translated to b. Otherwise, a is translated to $\Phi(e)$.

Suppose a_i is constant which is not mentioned in the constant association list of $\Phi$, but which is a member of a list $a_1,\ldots,a_n$ of constants of $\mbox{$\cal T$ }_1$ defined by recursion. Let $F_1,\ldots,F_n$ be the list of functionals that was used to define $a_1,\ldots,a_n$. If there is a list $b_1,\ldots,b_n$ of constants of $\mbox{$\cal T$ }_2$ recursively defined by the list of functionals $F^{\prime}_{1},\ldots,F^{\prime}_{n}$ such that $F^{\prime}_{j}$ and $\Phi(F_j)$ are alpha-equivalent for each j with $1 \leq j \leq n$, then a_i is translated to b_i. Otherwise, a_i is translated to an iota-expression which denotes the ith component of the minimal fixed point of $\Phi(F_1),\ldots,\Phi(F_n)$.

9.5 Reasoning and Formalization Techniques

This section briefly describes most of the ways interpretations are used in IMPS for formalizing mathematics and proving theorems.

9.5.1 Transporting Theorems

The most important use of theory interpretations is for transporting theorems from one theory to another. There are several ways that a theorem can be transported:

1.

The translation of a theorem of $\mbox{$\cal T$ }_1$ via an interpretation of $\mbox{$\cal T$ }_1$ in $\mbox{$\cal T$ }_2$ can be installed in $\mbox{$\cal T$ }_2$ using def-theorem with the modifier argument translation.

2.

In the course of a proof, the translation of a theorem can be added to the context of a sequent with the proof command assume-transported-theorem. Similarly, an instantiation of a translation of a theorem can be added with instantiate-transported-theorem. Both of these commands ask for the theory interpretation to be used. If no interpretation is given with the command instantiate-transported-theorem, IMPS will try to find or build an interpretation on its own using the information in the variable instances supplied by the user.

3.

When a transportable macete or transportable rewrite rule is applied, a theorem is effectively transported to the current theory (but it is not actually installed in the current theory).

Theorems are usually transported from an abstract theory to a more concrete theory.

9.5.2 Polymorphism

Constructors and quasi-constructors are polymorphic in the sense that they can be applied to expressions of several different types. This sort of polymorphism is not very useful unless we have results about constructors and quasi-constructors that could be used in proofs regardless of the actual types that are involved. For constructors, most of these ``generic'' results are coded in the form of the primitive inferences given in Chapter 19. Since quasi-constructors, unlike constructors, can be introduced by you, it is imperative that there is some way for you to prove generic results about quasi-constructors. This can be done by proving theorems about quasi-constructors in a theory of generic types, and then transporting these results as needed to theories where the quasi-constructor is used.

For example, consider the quasi-constructor m-composition defined by

   (def-quasi-constructor M-COMPOSITION
     "lambda(f:[ind_2,ind_3],g:[ind_1,ind_2], 
        lambda(x:ind_1, f(g(x))))"
     (language pure-generic-theory-3)
     (fixed-theories the-kernel-theory))

The basic properties about m-composition, such as associativity, can be proved in the theory pure-generic-theory-4, which has four base types but no constants, axioms, or other atomic sorts.

9.5.3 Symmetry and Duality

Theory interpretations can be used to formalize certain kinds of arguments involving symmetry and duality. For example, suppose we have proved a theorem in some theory and have noticed that some other conjecture follows from this theorem ``by symmetry.'' This notion of symmetry can frequently be made precise by creating a theory interpretation from the theory to itself which translates the theorem to the conjecture.

As an illustration, consider the theory interpretation defined by

   (def-translation MUL-REVERSE
     (source groups)
     (target groups)
     (fixed-theories h-o-real-arithmetic)
     (constant-pairs
      (mul "lambda(x,y:gg, y mul x)"))
     force-under-quick-load
     (theory-interpretation-check using-simplification))

This translation, which reverses the argument order of $\ast$ and holds everything else fixed in groups, maps the left cancellation law

   (def-theorem LEFT-CANCELLATION-LAW
     "forall(x,y,z:gg, x mul y = x mul z iff y=z)"
     (theory groups)
     (usages transportable-macete)
     (proof
      (...)))

to the right cancellation law

   (def-theorem RIGHT-CANCELLATION-LAW
     ;; "forall(x,y,z:gg, y mul x=z mul x iff y=z)"
     left-cancellation-law
     (theory groups)
     (usages transportable-macete)
     (translation mul-reverse)
     (proof existing-theorem))

Since this translation is in fact a theory interpretation, we need only prove the left cancellation law to show that both cancellation laws are theorems of groups.

9.5.4 Problem Transformation

Sometimes a problem is easier to solve if it is transformed into an equivalent, but more convenient form. For example, often geometry problems are easier to solve if they are transformed into algebra problems, and vice versa. Many problem transformations can be formalized as theory interpretations. The interpretation serves both as a means of transforming the problem and as a verification that the transformation is valid.

9.5.5 Definition Transportation

A list of definitions (atomic sort, directly defined constant or recursively defined constant) can be transported from T₁ to T₂ via an interpretation of $\mbox{$\cal T$ }_1$ in $\mbox{$\cal T$ }_2$ using def-transported-symbols.

For example, consider the following def-forms:

   (def-translation ORDER-REVERSE
     (source partial-order)
     (target partial-order)
     (fixed-theories h-o-real-arithmetic)
     (constant-pairs 
       (prec rev%prec)
       (rev%prec prec))
     (theory-interpretation-check using-simplification))

   (def-renamer FIRST-RENAMER
     (pairs
      (prec%majorizes prec%minorizes)
      (prec%increasing rev%prec%increasing)
      (prec%sup prec%inf)))

   (def-transported-symbols 
     (prec%majorizes prec%increasing prec%sup)
     (translation order-reverse)
     (renamer first-renamer))

The def-transported-symbols form installs three new definitions--prec%minorizes, rev%prec%increasing, and prec%inf--in partial-order. These new definitions are created by translating the definiens of prec%majorizes, prec%increasing, and prec%sup, respectively, via order-reverse.

9.5.6 Theory Instantiation

As argued by R. Burstall and J. Goguen (e.g., in [14,15]), a flexible notion of parametric theory can be obtained with the use of ordinary theories and theory interpretations. The key idea is that the primitives of a subtheory of a theory are a collection of parameters which can be instantiated as a group via a theory interpretation. In IMPS theories are instantiated using def-theory-instance; each subtheory of a theory can serve as a parameter of the theory.

For example, consider the following def-forms:

   (def-translation FIELDS-TO-RR
     (source fields)
     (target h-o-real-arithmetic)
     (fixed-theories h-o-real-arithmetic)
     (sort-pairs
      (kk rr))
     (constant-pairs
      (o_kk 0)
      (i_kk 1)
      (-_kk -)
      (+_kk +)
      (*_kk *)
      (inv "lambda(x:rr,1/x)"))
    (theory-interpretation-check using-simplification))

   (def-theory-instance VECTOR-SPACES-OVER-RR
     (source vector-spaces)
     (target h-o-real-arithmetic)
     (translation fields-to-rr)
     (renamer vs-renamer))

The last def-form creates a theory of an abstract vector space over the field of real numbers by instantiating a theory of an abstract vector space over an abstract field. The parameter theory is fields, a subtheory of vector-spaces and the source theory of fields-to-rr. For a detailed description of this technique, see [3,6].

9.5.7 Theory Extension

Let $\mbox {$\mathcal T$ }_i=(\mbox {$\mathcal L$ }_i,\Gamma_i)$ be a LUTINS theory for i=1,2. $\mbox{$\cal T$ }_2$ is an extension of $\mbox{$\cal T$ }_1$ (and $\mbox{$\cal T$ }_1$ is a subtheory of $\mbox{$\cal T$ }_2$) if $\mbox {$\mathcal L$ }_1$ is a sublanguage of $\mbox {$\mathcal L$ }_2$ and $\Gamma_1 \subseteq \Gamma_2$. A very useful reasoning technique is to (1) add machinery to a theory by means of a theory extension and (2) create one or more interpretations from the theory extension to the original theory. This setup allows one to prove results in a an enriched theory and then transport them back to the unenriched theory.

For example, many theorems about groups are more conveniently proved about groups actions because several group theorems may be just different instantiations of a particular group action theorem. The following def-forms show how group-actions is an extension of groups:

   (def-language GROUP-ACTION-LANGUAGE
     (embedded-language groups-language)
     (base-types uu)
     (constants
      (act "[uu,gg,uu]")))

   (def-theory GROUP-ACTIONS
     (language group-action-language)
     (component-theories groups)
     (axioms
      (act-id
       "forall(alpha:uu,g:gg, act(alpha,e) = alpha)"
       rewrite transportable-macete)
      (act-associativity
       "forall(alpha:uu,g,h:gg, 
          act(alpha,g mul h) = act(act(alpha,g),h))" 
       transportable-macete)))

There are many natural interpretations of group-actions in groups such as:

   (def-translation ACT->CONJUGATE
     (source group-actions)
     (target groups)
     (fixed-theories h-o-real-arithmetic)
     (sort-pairs
      (uu "gg"))
     (constant-pairs
      (act "lambda(g,h:gg, (inv(h) mul g) mul h)"))
     (theory-interpretation-check using-simplification))

Suppose $\mbox{$\cal T$ }_2$ is an extension of $\mbox{$\cal T$ }_1$ that is obtained by adding to $\mbox{$\cal T$ }_1$ new constants and axioms relating the new constants of $\mbox{$\cal T$ }_2$ to the old constants of $\mbox{$\cal T$ }_1$. Then each theorem of $\mbox{$\cal T$ }_2$has a analogue in $\mbox{$\cal T$ }_1$ obtained by generalizing over the new constants of $\mbox{$\cal T$ }_1$. This notion of generalization is performed automatically in IMPS with an appropriate interpretation of $\mbox{$\cal T$ }_2$ in $\mbox{$\cal T$ }_1$.

For example, the def-forms

   (def-language LCT-LANGUAGE
     (embedded-language groups)
     (constants
       (a "sets[gg]")
       (b "sets[gg]")))

   (def-theory LCT-THEORY
     (language lct-language)
     (component-theories groups)
     (axioms 
      (a-is-a-subgroup "subgroup(a)")
      (b-is-a-subgroup "subgroup(b)")))

   (def-theorem LITTLE-COUNTING-THEOREM
     "f_indic_q{gg%subgroup}
        implies
      f_card{a set%mul b}*f_card{a inters b} = 
      f_card{a}*f_card{b}"
     ;; "forall(b,a:sets[gg],
     ;;    subgroup(a) and subgroup(b) 
     ;;     implies 
     ;;    (f_indic_q{gg%subgroup}
     ;;     implies 
     ;;    f_card{a set%mul b}*f_card{a inters b} = 
     ;;    f_card{a}*f_card{b}))"
     (theory groups)
     (home-theory lct-theory)
     (usages transportable-macete)
     (proof (...)))

show that the ``little counting theorem'' is proved in an extension of groups, but is installed in groups by generalizing over the constants a and b.

9.5.8 Model Conservative Theory Extension

Suppose $\mbox{$\cal T$ }_2$ is an extension of $\mbox{$\cal T$ }_1$. $\mbox{$\cal T$ }_2$ is a model conservative extension of $\mbox{$\cal T$ }_1$ if every model of $\mbox{$\cal T$ }_1$``expands'' to a model of $\mbox{$\cal T$ }_2$. Model conservative extensions are safe extensions since they add new machinery without compromising the old machinery. For instance, a model conservative extension preserves satisfiability. The most important model conservative extensions are definitional extensions which introduce new symbols that are defined in terms of old vocabulary. (Logically, IMPS definitions create definitional extensions.) Many natural methods of extending theories correspond to a class or type of model conservative extensions. For instance the theories created with the def-bnf are always model conservative extensions of the starting theory.

IMPS supports a general technique, based on theory interpretation and theory instantiation, for building safe theory extension methods. The idea is that a model conservative extension type can be formalized as an abstract theory with a distinguished subtheory. The theory can be shown to be a model conservative extension of the subtheory using

Theorem 9.5.1 (Model Conservative Verification Theorem)   Let $\mbox{$\cal T$ }_2$ be an extension of $\mbox{$\cal T$ }_1$. $\mbox{$\cal T$ }_2$ is a model conservative extension of $\mbox{$\cal T$ }_1$ if there is an interpretation of $\mbox{$\cal T$ }_2$ in $\mbox{$\cal T$ }_1$ which fixes $\mbox{$\cal T$ }_1$.

Then instances of the model conservative extension type are obtained by instantiating the theory. Each such instance is guaranteed to be a model conservative extension by

Theorem 9.5.2 (Model Conservative Instantiation Theorem)   Let $\mbox{$\cal T$ }^{\prime}_{1}$ be a model conservative extension of $\mbox{$\cal T$ }_1$, and let $\mbox{$\cal T$ }^{\prime}_{2}$ be an instance of $\mbox{$\cal T$ }^{\prime}_{1}$ under the an interpretation of $\mbox{$\cal T$ }_1$ in $\mbox{$\cal T$ }_2$. Then $\mbox{$\cal T$ }^{\prime}_{2}$ is a model conservative extension of $\mbox{$\cal T$ }_2$.

For a detailed description of this technique, see [6].

9.5.9 Theory Ensembles

A theory ensemble consists of a base theory, copies of the base theory called replicas, and unions of copies of the base theory called theory multiples. The constituents of a theory ensemble are related to each other by theory interpretations. They allow you to make a definition or prove a theorem in just one place, and then transport the definition or theorem to other members of the theory ensemble as needed. They are used in a similar way to relate a theory multiple to one of its ``instances.'' See Chapter 11 for a detailed description of the IMPS theory ensemble mechanism.

9.5.10 Relative Satisfiability

If there is a theory interpretation from a theory $\mbox{$\cal T$ }_1$ to a theory $\mbox{$\cal T$ }_2$, then $\mbox{$\cal T$ }_1$ is satisfiable (in other words, semantically consistent) if $\mbox{$\cal T$ }_2$ is satisfiable. Thus, theory interpretations provide a mechanism for showing that one theory is satisfiable relative to another. One consequence of this is that IMPS can be used as a foundational system. In this approach, whenever one introduces a theory, one shows it to be satisfiable relative to a chosen foundational theory (such as, perhaps, h-o-real-arithmetic).

9.6 Hints and Cautions

1.

The application of a nonnormal translation to an expression containing quasi-constructors will often result in a devastating explosion of quasi-constructors. One way of avoiding this problem is to ``normalize'' the translation by defining new atomic sorts in the translation's target theory to replace the unary predicates used in the translation.

2.

Suppose a defined atomic sort or constant a is transported to a new atomic sort or constant b via a theory interpretation $\Phi$. From that point on, $\Phi$ will map a to b.

3.

Translations must be updated to take advantage of new definitions (see Section 9.4 above). The updating is called translation enrichment and it performed periodically by IMPS. For example, enrichment is done when a translation is evaluated and when the macete help mechanism is called. In rare occasions, IMPS will not work as expected because some interpretation has not been enriched. This may happen, for example, when a transportable macete is applied directly without using the macete help mechanism. In some cases, you can get around the problem by re-evaluating a relevant def-translation form.