next up previous contents
Next: 12. The Proof System Up: 2. User's Guide Previous: 10. Quasi-Constructors


11. Theory Ensembles

11.1 Motivation

Much of mathematics deals with the study of structures such as monoids, fields, metric spaces, or vector spaces, which consist of an underlying set S, some distinguished constants in S, and one or more functions on S. In IMPS, an individual structure of this kind can be easily formalized as a theory. For example, the IMPS theory for monoids is specified by two def-forms:

   (def-language MONOID-LANGUAGE
     (embedded-languages h-o-real-arithmetic)
     (base-types uu)
      (e uu)
      (** (uu uu uu))))

   (def-theory MONOID-THEORY
     (component-theories h-o-real-arithmetic)
     (language monoid-language)
       "forall(z,y,x:uu, x**(y**z)=(x**y)**z)")
In the mathematical syntax, the sort uu is written U and the constants e, star* are written $e, \bullet.$

Notice that the theory of a monoid as presented here is suitable for concept formulation and proof in a single monoid. Here are some examples:

However, there is no way to talk about monoid homomorphisms between different monoids.

Nevertheless, it is possible to produce a suitable theory in IMPS in which a general notion of monoid homomorphism can be defined. To do so requires at the very least a theory with two possibly distinct monoids. In general, multiple instances of structures can be dealt with in IMPS in two ways:

In this section we explain the theory ensemble mechanism, which implements the second approach above. To illustrate how the machinery works in the case of a monoid, let us define a new theory, monoid-theory-1 obtained by renaming the sorts and constants of monoid-theory not in h-o-real-arithmetic by affixing the characters `` _1.''
   (def-language MONOID-LANGUAGE-1
     (embedded-languages h-o-real-arithmetic)
     (base-types uu_1)
       (e_1 uu_1)
       (**_1 (uu_1 uu_1 uu_1))))
   (def-theory MONOID-THEORY-1
     (component-theories h-o-real-arithmetic)
     (language monoid-language-1)
           x **_1 (y **_1 z)=(x **_1 y) **_1 z)")
       ("forall(x:uu_1,x **_1 e_1=x)")
       ("forall(x:uu_1,e_1 **_1 x=x)")))
Now define monoid-pair as the union of monoid-theory and monoid-theory-1:
   (def-theory MONOID-PAIR
     (component-theories monoid-theory monoid-theory-1))
The theory ensemble facility automates these steps and also provides several bookkeeping devices for keeping track of theories and interpretations in the ensemble.

11.2 Basic Concepts

A copy of a theory $\cal T$

11.3 Usage

There are four def-forms for building and manipulating theory ensembles.

11.4 Def-theory-ensemble

This is the def-form for building a theory ensemble from an IMPS theory. In the simplest version, the form requires only one argument, the name of the theory ensemble which is then identical to the name of the base theory. For example:
   (def-theory-ensemble METRIC-SPACES)
Evaluating the def-form builds a theory ensemble also named METRIC-SPACES. In general, three additional keyword arguments are allowed: Another example which utilizes the fixed-theories option is the theory ensemble of vector spaces over a field:
   (def-theory-ensemble VECTOR-SPACES 
     (fixed-theories fields))

When a theory ensemble def-form is evaluated, IMPS builds a number of tables, all of which are initially empty. The table will be filled as multiples are built. The tables are:

11.5 Def-theory-multiple

This form requires two arguments, the name of a theory ensemble and an integer n. For example,
   (def-theory-ensemble-multiple metric-spaces 2)
When this form is evaluated, IMPS builds a 2-multiple of the theory metric-spaces. IMPS automatically names this theory metric-spaces-2-tuples.

Once the theory metric-spaces-2-tuples is available several important concepts can be defined. For instance,

   (def-constant CONTINUOUS
          open(v) implies open(inv_image(f,v))))"
     (theory metric-spaces-2-tuples))

11.6 Def-theory-ensemble-instances

This form is used to build interpretations from selected theory multiples and to transport natively defined constants and sorts from these multiples using these interpretations. The syntax for this def-form is very elaborate, so we refer you to Chapter 17 for its general use.

As an example, suppose we wanted to consider the pair consisting of a normed linear space and the real numbers as a special case of the theory metric-spaces-2-tuples. One reason for doing this is to make all the mathematical machinery developed in the abstract theory metric-spaces-2-tuples available in the particular case. This machinery includes definitions (such as the definition of continuity for mappings) and theorems (such as the various characterizations of continuity.)

We would like to build a theory interpretation from metric-spaces-2-tuples to the union of normed-linear-spaces and h-o-real-arithmetic which is normed-linear-spaces itself, since normed-linear-spaces is a super-theory of h-o-real-arithmetic. Moreover, we would like IMPS to translate all the defined sorts and constants in metric-spaces-2-tuples to normed-linear-spaces.

This can be accomplished by evaluating the form

   (def-theory-ensemble-instances METRIC-SPACES
     (multiples 1 2)
     (sorts (pp uu rr))
        (dist "lambda(x,y:uu, norm(x-y))" 
              "lambda(x,y:rr, abs(x-y))")))
This does two things: First it builds an interpretation from metric-spaces-2-tuples into normed-linear-spaces in which Secondly, it translates all the natively defined constants in metric-spaces and metric-spaces-2-tuples into normed-linear-spaces.

11.7 Def-theory-ensemble-overloadings

This form takes the following arguments: Evaluation of the def-form causes IMPS to overload those constants natively defined in the theory multiples $\mbox{\it N}_1 \ldots {\it
N}_k.$ For example:
   (def-theory-ensemble-overloadings metric-spaces 1 2)

This form makes the theory ensemble mechanism manageable to the user. When the system transports a natively defined constant c from a theory multiple, it will often give the new constant an unappealing name. For instance, the name might be very long with several indices as suffixes. Ideally, one would like to use the same name for all instances of c, and this is usually possible if the constant is a function symbol which occurs as an operator of an application. In this case, the appropriate function symbol may be unambiguously determined from the sorts of the arguments.

11.8 Hints and Cautions

In principle, any theory can be used to build a theory ensemble. However, the theory ensemble facility is useful only if the following two conditions on the base theory are met:
There is a certain amount of overhead in building theory multiples. This overhead includes building and tabulating theory replicas and building canonical theory interpretations from the m-multiples to n-multiples, where m<n. Recall, that there is a canonical interpretation $\Phi_f: \mbox{$\cal U$ }_m \rightarrow
\mbox{$\cal U$ }_n$ for each injective map

\begin{displaymath}\{0, \ldots, m-1\} \rightarrow \{0, \ldots, n-1\}.\end{displaymath}

There are $n (n-1) \cdots (n-m+1)$ such mappings. This overhead can become forbidding when the multiples get too large. As a general rule, multiples of order greater than 4 should be avoided.
Before the system builds an n-multiple it checks whether all j-multiples for j<n already exist, building the missing multiples as needed.

next up previous contents
Next: 12. The Proof System Up: 2. User's Guide Previous: 10. Quasi-Constructors
System Administrator