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