Also see Set Type and Quotient Types for supplementary material.


next up previous contents index
Next: Theories Up: Building Theories Previous: Definitions

Sets and Quotients

The quotient  type provides a powerful abstraction mechanism and puts a user--defined equality into the theory so that the rules for reasoning about equality  (the equality and substitution rules and all the intro rules for equality of noncanonical members) can be applied to it. The obverse of this is that if x is declared in a hypothesis list to be in a quotient type then any type T which appears as a later hypothesis or as the conclusion must be independent of the representation of x; that is, it must yield equal types when different but equal elements of the quotient type are substituted for x. For example, for t in T to be true under the assumption that x is in some quotient type, it is required that both t and T be independent of the representative for x (see the quotient--elim rule). Therefore, if we define the rational numbers to be the obvious quotient on pairs of integers whose second component is nonzero, then we will not be able to show that the following definition of less--than is a type:

  
     <x:Q> < <y:Q> in Q == 
        fst(<x>)*snd(<y>) < fst(<y>)*snd(<x>).
The difficulty here is that type equality in Nuprl is strong; two types are equal if they are structurally the same, and so there are types which have the same members but are not equal. In particular, two less--than types can be shown to be equal only if it can be shown that their corresponding components are equal as integers. Therefore, if we could show that the above were a type then for any pairs of integers <i,j>, <i',j'>, and <m,n> such that <i,j> and <i',j'> are equal as rational numbers, we would have
     ( i*n < m*j ) = ( i'*n < m*j' )  in U1
. In particular, we would have
     i*n = i'*n  in int,
which is not always true. Thus we cannot use the above definition of less--than over the quotient--type Q. However, we are only interested in the truth value of less--than, i.e., whether or not it is inhabited, and this property is independent of representatives. In this situation, we squash  the type. Define
 
     ||<T:type>|| == {0 in int|<T>}.
This squashes a type in the sense that given a type T, it produces a type which has one element if T is inhabited and is empty otherwise. For the less--than example, we define less--than to be the squash of what it was before, and the result is a type, since to show that two set  types are equal involves showing the proposition parts are equivalent instead of equal. (See the rule for equality of set types.) More specifically, to prove ||T|| = |||| in Ui , one only has to be able to prove T => and => T. In general, this use of the squash operator will often be required when one wishes to create a type which deals with the representations of objects from a quotient type.

Note that squashing does away with any computational content that the type might have had (this will be discussed further later in this section). If you are interested in that content and you cannot reformulate so as to bring out from under the squash operator the part you are interested in, you cannot use the quotient type and must treat the equality you want as you would any other defined relation. More precisely, suppose that Q is some quotient type and is some property of members of Q that one wishes to express in Nuprl . If, as above, one is interested only in the truth value of , i.e., whether or not its type representation is inhabited, and if the truth value respects the equality relation of Q, then the squash operator can be applied. Usually in this case the type resulting from a direct translation of according to the propositions--as--types principle will have at most one member, and that member will be known in advance (e.g., axiom), so one would lose nothing by squashing. Often, however, P will have some content of interest; for example, it might involve an assertion of the existence of some object, and one might wish to construct a function which takes a member x of Q satisfying to the object whose existence is asserted, but this may not be possible if the property has been squashed. What one has to do in this case is to separate into two pieces so that it can be expressed by a type z:T # ||||, or equivalently, {z:T|}, where T represents the computationally interesting part and represents the part of which only the truth value is interesting. This requires that the type T respect equality in x and that for any two representatives chosen for x the collection of computationally interesting objects be the same.

We illustrate the points raised above with an example. The usual formulation of the constructive real numbers is as a certain set of sequences of rational numbers with known convergence rates, where two such sequences are considered equal if they are the same in the limit. One crucial property of real numbers is that each one has a rational approximation to within any desired accuracy. Given a particular real number, obtaining such an approximation simply involves picking out an element suitably far along in the sequence, since the convergence rate is known. However, clearly one can have two different but equal real numbers for which this procedure gives two different answers, and in fact it is impossible constructively to come up with approximations in a way which respects equality. Since many computations over the real numbers involve approximations, one cannot bury the property of having a rational approximation under the squash operator. The upshot is that the constructive reals cannot be ``encapsulated'' as a quotient type; one must take the reals to be just the type of rational sequences and treat the equality relation separately. However, one can still use the quotient type to some extent in a situation such as this. For example, in the real number case one can still form the quotient type and use it to express the equality relation. Thus, although hypothetical real numbers will be members of the unquotiented version, one can express equality between reals as equality in the quotient type and so can use the equality rule, etc., to reason about it.

It should not be concluded from the preceding discussion that one should never represent anything with the quotient type. There is a wide class of domains for which the quotient as a device for complete abstraction with respect to equality is a safe choice. This class consists of those domains where the desired equality is such that canonical representatives exist, i.e., where one can prove the existence of a function from the quotient type to its base type which takes equal members of the quotient type to the same member of the equivalence class in the base type. This will allow one to express properties which do not respect equality by having them refer to the canonical representative. An example of a common domain with this property is the rational numbers, where the canonical representative for a fraction is the fraction reduced to lowest terms.

The squash operation defined earlier is just one particular use of the information--hiding capability of the set  type. It can also be used to remove from the ``computational part'' of the theorem information whose computational content  is uninteresting and which would otherwise reduce the efficiency of the extracted code or information which would make the theorem weaker than one desired. As an example of the first kind of information, we could define the type of integers which are perfect squares two different ways:

    n:int # Some m:int. (n=m*m in int)
or
    { n:int | Some m:int. (n=m*m in int) }.
Suppose we had some variable declared in a hypothesis to be in one of the perfect square types. In each case we could eliminate it to get an integer which we know to be a perfect square. In the first case we could do another elimination to get our hands on the integer whose square is the first integer, and we could use this square root freely in the proof of the conclusion. However, this will not be allowed in the second case. The system will ensure that the proof that the number is a square is not used in the term which is built as the proof of the conclusion. On the other hand, if one is interested only in the integer which is a perfect square, and only needs the perfect square property to prove something about a program which does not need the square root, then the second version can be used to get a more efficient extracted object.

As an example of the second kind of information hiding referred to above, consider the specification of a function which is to search an array of integers for a given integer and return an index, where it is known in advance that the integer occurs in the array. If integer arrays  of length n are represented as functions from {1..n} to the integers, where {1..n} is defined to be the appropriate subset of the integers, a naive translation of the requirements for the search program into the Nuprl logic might be the following:

    All n:N. All a:{1..n}->int. All k:int.
      Some i:{1..n}. a(i)=k in int
      => Some i:{1..n}. a(i)=k in int
This specifies a trivial function which requires as an argument the answer which it is to produce, and so it does not capture the meaning of the informal requirements. This problem is solved by use of the set type to ``hide''  the proof of the fact that k occurs in the array. If we make the Nuprl definition
    All <x>:<T> where <P>. <P'> == 
      <x>: {<x>:<T>|<P>} -> <P'>
then we can give the correct specification as
    All n:N. All a:{1..n}->int. 
      All k:int where ( Some i:{1..n}. a(i)=k in int ) .
        Some i:{1..n}. a(i)=k in int
In a proof of this assertion, if one has done intro steps to remove the universal quantifiers and thus has n, a and k declared in the hypothesis list, then the type that k is in is a set type. The only way to get at the information about k (i.e., that it occurs in the array) is to use the elim rule on it. However, doing so will cause the desired information to be hidden (see the set elim rule), and it will not become unhidden until the proof has proceeded far enough so that the required function has been completely determined. Thus, the information can be used only to prove that the constructed function meets the specification, not to accomplish the construction itself.

The set type should be regarded primarily as an information--hiding  construct. It cannot be used as a general device for collecting together all objects (from some type) with a certain property, as it would in conventional mathematics. One of the reasons has just been discussed: if the set type is used to represent a subtype of a given type then being given a member of the subtype does not involve being given a proof of its membership; that is, the proof that the member is a member will be hidden, and in the Nuprl theory this means that information is irretrievably lost. Another reason is that for x a member of a type A the property of being a member of {x:A|B} cannot be expressed unless it is always true. This is because the type t in T is really a short form for t=t in T; it expresses an equality judgement and is well--formed only if t is a member of T. The problem remains of how to form the type which represents the power set of a given type. Bishop [Bishop 67] defines a subset of a given set S to be a set A together with an injection i from A into S. If one takes this definition and does the obvious translation into Nuprl then it turns out that the collection of such subsets (within some fixed universe Ui) of a given type T is equivalent to the function type T->Ui. This latter formulation, where we identify a subset with the predicate which ``identifies'' the members of the subset, is much simpler to deal with than Bishop's version. For example, the proposition that x (for x in T) is in a subset P is expressed just by P(x); the union of two subsets P and is just x.P(x)|(x). Notice that being given the fact that x is in a subset includes being given the proof that it is. Of course, one can still use the set type in this context to hide information when desired.



next up previous contents index
Next: Theories Up: Building Theories Previous: Definitions


Also see Set Type and Quotient Types for supplementary material.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995