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 = <Xs | sS>   with Xs"",s for all sS,  we can form a new S-sorted signature <S, (X)>   with
(X)w,sw,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

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.

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

Theorem:  Let  A be any <S, >-algebra,  then for any S-indexed family of mappings, = < s:Xs As | sS>  there is a unique homomorphism #:T[X] that extends  in the sense that if we let X be the S-indexed family of inclusion mappings X = < X,s:XsT[X]s | sS>   then #sX,sfor all s (i.e., for each xXsT[X]s#s(x) = = s(x)).

Proof: Given , extend A as a <S, (X)>-algebra, A+,  where for each sS and xXs xAs(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,sfor all sS.  The homomorphism is unique for if :T[X]  A with sX,ss   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.

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:XsT[X]s then  for any <S, >-algebra, A, and  S-indexed map :XU(A)  there is a unique homomorphism #:T[X] 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 tA, 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 = < hs:Xs As | sS> )  we define  tA(h) = h#(t).

Recall the Signature sigP in programming form:

 name: sigP

 sorts: {int}

 zero: -->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

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:XAint such that h(x1)=2, h(x2)=5 and h(x3)=7.

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:XA on the UA-calculator.   The function aitchFree takes three arguments:
  1. the name of the algebra
  2. an arrays of pairs of strings specifying the assignment of values to the variables
  3. 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:

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

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.

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(#) =  U(#) =   ()#Y which then implies that ## =   ()#

but then () = ( U(#)) =  U( #)( U(#)) = (U( #) U(#)) =  ()# = ()