In this section we examine a fragment of group theory and discuss how the definition of algebraic structures can be cast in the Nuprl logic. Defining an algebraic structure involves identifying certain distinguished functions (the operators) and constants and stating the properties of the functions and constants. The properties one wishes to state are usually equational and thus correspond to Nuprl terms. Expressing inequations is slightly more tedious but does not present any fundamental difficulty.
We begin by discussing how some typical phrases that one might see in an algebra text are expressed in Nuprl . Suppose one wishes to make a statement of the following general form: `` where ''. In the first equation of such a statement the variable x serves as an abbreviation for the right--hand side of the second equation. The entire statement thus expresses whatever the first equation expresses with x appropriately instantiated. A natural way to express instantiation involves the application of a lambda term to another term. Thus we are led to the following Nuprl definition:
<t:term> where <x:var>=<tt:term> == (\ <x>.<t>)(<tt>).In algebra it is customary to write binary operators in infix form. In the Nuprl notation operators are just functions (lambda terms) expressed in curried form. The following definition thus allows one to use traditional algebraic syntax in discussing operators:
<x:arg> <op:operation> <y:arg> == <op>(<x>)(<y>).An important property of operators that one might wish to state is the property of associativity . Associativity is an equationally stated property; accordingly in Nuprl it is necessary to state associativity with respect to a particular type. One can use the definition for the universal quantifier in writing the definition of associativity to obtain the following definition.
<op:A->A->A> associative over <A:type>== All x,y,z:<A>. x <op> (y <op> z) = (x <op> y) <op> z in <A>During an instantiation of the last definition the template displayed in the library window will look like the following:
<A->A->A> associative over <A:type>.
With the definitions above, one can state the definition of a group. A group is just a type; accordingly the definition of a group will be a type expression in which the various components of the definition are pieced together. The complete definition is as follows:
Group == A:U1 # o:(A->A->A) # e:A # All x:A. x o e = e o x = x in A # All x:A. Some y:A. x o y = y o x = e in A # o associative over AIn the definition above, o is the group composition operator, e is the group identity, and the last three lines express the standard properties of a group. There are a number of different ways in which the definition can be used in stating theorems. One could, for example, state the type Group as a top--level goal. This would then assert that there exist groups. One could make a statement of the form B in Group; this would assert that B is a group. A proof of such a statement would of course be constructive and would involve displaying a procedure for computing inverses in B. A third way of using the definition of a group would be to state properties true of all groups with statements of the form
All G:Group. ... .
To be able to state interesting theorems about group theory it is necessary to be able to pull apart the constituents of a group. This is done using the spread operator, the elimination form of the product constructor. The following two definitions provide mnemonic access functions.
fst(<x:term>) == spread(<x>;u,v.u) snd(<x:term>) == spread(<x>;u,v.v)Now we can define notation that accesses the definition of a group and produces the underlying carrier set and operations. For example, the following definition defines the carrier set of a group.
|<G:Group>| == fst(<G>)We can access the composition operator and the identity of the group by using the following definitions.
op_of <G:Group> == fst(snd(<G>)) id_of <G:Group> == fst(snd(snd(<G>)))We conclude this section by stating a typical elementary theorem of group theory, namely that every equation of the form can be uniquely solved for x. In Nuprl this theorem would read
>> All G:Group. All a,b:|G|. Some x:|G|. (a o x = b in |G| & All c:|G|. a o c = b in |G| => c = x in |G| where o=op_of G )In the statement above, the fourth line states the uniqueness of the solution.