Free Algebras, Derived Operations and Substitution

In the section on initial algebras we introduced the concept of an <S,

>-term (reference). Those terms, sometimes called ground terms, contain only symbols from

. We now want to extend that concept to the idea of <S,

>-terms with variables. To do this we introduce the important concept of a free <S,

>-algebra generated by an S-indexed set of sets,X

The essential theoretical core is the following

Given an S-sorted signature <S,> and an S-indexed set X = <X_s | sS>   with X_s"",s= for all sS, we can form a new S-sorted signature <S, (X)>   with
(X)_"",s = _sX_s
(X)_w,s = _w,s,   for all w"".

Let T(X) be the initial <S, (X)>-algebra. We can view T(X) as an <S, >-algebra, T[X], by simply not viewing the elements from X as new constant operators but keeping everything else the same, that is we take:
        T[X]_s = T(X)_s
and
_T[X] = _T(X).
for all .

Definition: The <S,

>-algebra T

[X] is called "the" <S,

>-algebra freely generated by X. The <S,

(X)>-terms that make up the carriers of T

[X] , are called derived operators.
end

The <S, >-algebra freely generated by X has the following important property.

Theorem: Let A be any <S, >-algebra, then for any S-indexed family of mappings, = < _s:X_s A_s | sS> there is a unique homomorphism ^#:T[X] A that extends in the sense that if we let _X be the S-indexed family of inclusion mappings _X = < _X,s:X_sT[X]_s| sS> then ^#_sX,s = _sfor all sS (i.e., for each xX_sT[X]_s , ^#_s(x) = = _s(x)).

Proof: Given , extend A as a <S, (X)>-algebra, A+, where for each sS and xX_s, x_A = _s(x). Then, since T(X) is the initial (X)-algebra there exists a unique homomorphism h:T(X)A+. But since T[X] is just T(X) with the elements of X no longer treated as operators, it follows that U(h) also gives us a <S, >-homomorphism ^# :T[X] A with the property that ^#_sX,s = _sfor all sS. The homomorphism is unique for if :T[X] A with _sX,s = _s for all sS, then U() would give us a homomorphism h":T(X)A+ which implies h" = h, by the initiality of h, but then U() = U(h) = U() so= .
end

The statement of the above theorem can be done a little more neatly if , for any <S, >-algebra A, we define U(A) to be the corresponding S-indexed set of its carriers and for any homomorphism h:AB we define U(h) to be the S-indexed mapping U(h)=< hs:AsBs | sS> used to define the homomorphism h. Given this additional notation we can state the theorem as follows:

Let X be an S-indexed set of variables and let _X be the S-indexed family of inclusion mappings _X = < _X,s:X_sT[X]_sthen for any <S, >-algebra, A, and S-indexed map :XU(A) there is a unique homomorphism ^#:T[X] A such that ^#_X = h. This equality can be expressed by the following commuting diagram

We now turn to the applications of the above result:

Given a signature <S,>, an S-sorted set of variables X and an <S,> -algebra A the above result provides a precise meaning of what it means to interpret a derived operator as a function .

Definition: Given a derived operator t (i.e., an <S, (X)>-term t) then for any <S,> -algebra A, we define the derived operation, t_A, to be the function such that, for any assignment, h, of values in A to the elements of X (i.e., any any S-indexed family of mappings, h = < h_s:X_s A_s | sS> ) we define t_A(h) = h^#(t).
end

Example:
Recall the Signature sigP in programming form:

name: sigP
sorts: {int}
operators:
zero: -->int
pred:int-->int
succ:int-->int
add:int.int-->int
mult:int.int-->int
End of signature sigP.

There is only one sort in this signature. So let X be the 1-sorted set X = {x1, x2, x3}. Then a typical <1, SigP(X)>-term, t, would be the following:

t = "add(pred(x2( )), succ( succ(x1( ))))".

Note, that we are treating the variables (the elements of X) as <1, SigP(X)>-terms and are thus writing "x1( )" rather than just "x1".

Now say we want to interpret this term in the algebra alg_A where

A_int = Z
zero_A = 0
pred_A(z) = z-1
succ_A(z) = z+1
add_A(z, z') = z+z'
mult_A(z, z') = z*z'

Then we claim that evaluating (interpreting) the above term, t, with x1 = 2, x2= 5, and x3=7 is exactly the same as taking h^#(t) for h:X

A_int such that h(x1)=2, h(x2)=5 and h(x3)=7.
end

Performing Derived Operators on the UA-Calculators

Just as we were able to use the function aitch to compute the unique homomorphism from an initial <S,

>-algebras to an arbitrary <S,

>-algebra on the UA-calculator, so can we can use the function aitchFree to compute the unique homomorphism h^# for a combination of the <S,

>-algebra generated by X and an assignment h:X

A on the UA-calculator. The function aitchFree takes three arguments:

the name of the algebra
an arrays of pairs of strings specifying the assignment of values to the variables
the term-with-variables to be evaluated

Try the following example:

To convince yourself that everything is on the up-and-up, try some variations:

make modifications on the term and perform it again
try other algebras with the same signature ( the algebras "alg_B", "alg_C", "alg_D" and "alg_E" with signature SigP are built into the calculator, click here to review their descriptions). Note that the above expression will not evaluate in algebras alg_D and alg_E since these algebras don't have numerical carriers.

The algebra alg_D has the booleans as its carrier -- try evaluating the expression:

aitchFree("alg_D", [["x1", "'true'"], ["x2", "'false'"], ["x3", "'true'"]], "add(pred(x2( )), succ(succ(x1( ))))")

The algebra alg_E has strings on the set {a,b,...,x,A,B,...,Z} as its carrier -- try evaluating the expression

aitchFree("alg_E", [["x1", "'abc'"], ["x2", "'ed'"], ["x3", "'uvw'"]], "add(pred(x2( )), succ(succ(x1( ))))")

Note

that in both examples the values in the assignment are written using both a double and a single quote -- the double quotes are used for all assignments, the single quotes indicate that the value is a string.

Derived Operators and Substitution

Substitution of terms within terms is a very common operation within many areas in computer science. Despite this, it is often treated extremely informally and this makes it difficult to prove even seemingly obvious results such as that substitution is associative. However, by using the idea of free algebras we can give a rigorous definition of substitution and prove the associativity of substitution by applying the above theorem.

Definition: Given an <S, (X)>-term t and an assignment, , of <S, (Y)>-terms to the elements of X, that is, an S-indexed mapping :X U(T[Y]), we define the result of substituting(x) for x in t , for all xX, to be the <S, (Y)>-term ^#(t). [this is a direct application of the above theorem but with in place of h].
end

Clearly we can follow one substitution with another, which is to say, we can compose compositions. The above framework leads us to the following formal definition of composition.

Definition: Given an <S, (X)>-term t , an assignment, , of <S, (Y)>-terms to the elements of X, and an assignment, , of <S, (Z)>-terms to the elements of Y, then we define their composite, denoted , to be the assignment U(^#):X U(T[Z]), where "" denotes the composition for S-indexed mappings.
end

Note: We could use just one symbol for both composition of assignments and composition of S-indexed mappings and write=U(^#), since the two uses can be distinguished by context. Such overloading is commonly used in mathematical treatments for the sake of brevity, but it comes at a price.

Proposition: The above composition is associative. that is, given an assignment , of <S, (Y)>-terms to the elements of X, an assignment, , of <S, (Z)>-terms to the elements of Y, and an assignment, , of <S, (W)>-terms to the elements of Z, then () = ().
Proof: Consider the following diagram:

From the theorem on free algebras and the definition of the composite of assignmnents it follows that

U(^#)U(^#)_Y = U(^#) = ()^#_Y which then implies that ^#^# = ()^#

but then () = ( U(^#)) = U( ^#)( U(^#)) = (U( ^#) U(^#)) = ()^# = ()
end