- 9.1 Introduction
- 9.2 Translations
- 9.3 Building Theory Interpretations
- 9.4 Translation of Defined Sorts and Constants
- 9.5 Reasoning and Formalization Techniques
- 9.6 Hints and Cautions

9. Theory Interpretations

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
and
be LUTINS theories. A *translation from
*
* to *
is a pair
,
where
is a
mapping from the atomic sorts of
to the sorts, unary
predicates (quasi-sorts), and indicators (sets) of
and is a mapping from the constants of
to the expressions of
,
satisfying certain syntactic conditions.
and
are called the *source theory* and *target theory* of ,
respectively. Given an expression *e* of
,
the
*translation* of *e* via ,
written ,
is an
expression of
defined from
and
in a manner that
preserves expression structure. In particular,
is a
sentence when *e* is a sentence.

When
maps an atomic sort
to a unary predicate *U*, the
variable binding constructors--,
,
,
and
--are ``relativized'' when they bind a variable of sort
.
For example,

Something very similar happens when maps an atomic sort to an indicator. The constructor

Let
be a translation from
to
.
is an
*interpretation of *
* in *
if
is a
theorem of
for each theorem
of
.
In other
words, an interpretation is a translation that maps theorems to
theorems. An *obligation* of
is a formula
where
is either:

- 1.
- a primitive axiom of
(
*axiom obligation*); - 2.
- a definition axiom of
(
*definition obligation*); - 3.
- a formula asserting that a particular primitive atomic sort of
is nonempty (
*sort nonemptiness obligation*); - 4.
- a formula asserting that a particular primitive constant of
is defined in its sort (
*constant sort obligation*); or - 5.
- a formula asserting that a particular primitive atomic sort of
is a subset of its enclosing sort (
*sort inclusion obligation*).

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

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

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
and
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

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

9.4 Translation of Defined Sorts and Constants

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

First, if the defined sort or constant is a member of one of the fixed theories of , 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 , 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
is a defined sort of
which is not mentioned
in the sort association list of .
Let *U* be the unary
predicate that was used to define .
If there is a atomic
sort
of
defined by a unary predicate *U*' such that
*U*' and
are alpha-equivalent, then
is translated
as if the pair
were in the sort association list of
.
Otherwise, it is translated as if the pair
were in the sort association list of .

Suppose *a* is a directly defined constant of
which is not
mentioned in the constant association list of .
Let *e* be the
expression that was used to define *a*. If there is a constant
*b* of
directly defined by an expression *e*' such that *e*'and
are alpha-equivalent, then *a* is translated to *b*.
Otherwise, *a* is translated to .

Suppose *a*_{i} is constant which is not mentioned in the constant
association list of ,
but which is a member of a list
of constants of
defined by recursion. Let
be the list of functionals that was used to define
.
If there is a list
of constants of
recursively defined by the list of functionals
such that
and
are alpha-equivalent for each *j* with
,
then *a*_{i} is translated to *b*_{i}. Otherwise, *a*_{i} is translated to
an iota-expression which denotes the *i*th component of the minimal
fixed point of
.

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

- 1.
- The translation of a theorem of
via an interpretation
of
in
can be installed in
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).

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

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 and holds everything else fixed in

(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

A list of definitions (atomic sort, directly defined constant or recursively
defined constant) can be transported from *T*_{1} to *T*_{2} via an interpretation
of
in
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

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

Let
be a LUTINS theory for *i*=1,2.
is an *extension* of
(and
is a
*subtheory* of
)
if
is a sublanguage of
and
.
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

(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 is an extension of that is obtained by adding to new constants and axioms relating the new constants of to the old constants of . Then each theorem of has a analogue in obtained by generalizing over the new constants of . This notion of generalization is performed automatically in IMPS with an appropriate interpretation of in .

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

Suppose
is an extension of
.
is a *model
conservative extension* of
if every model of
``expands'' to a model of
.
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

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

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

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.

If there is a theory interpretation from a theory
to a theory
,
then
is satisfiable (in other words, semantically
consistent) if
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**).

- 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 . From that point on, 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.