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

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

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

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

Thu Sep 14 08:45:18 EDT 1995