Initial Algebras

In this chapter we introduce the important concept of  an initial algebra and give some simple examples of its usefulness.  Most of the remaining chapters in Part I make use of initial algebras and provide evidence of the key importance of this concept.

Key Definitions and Results for Initial Algebras


Definition: An <S,>-algebra , A, is said to be an initial <S,>-algebra if for every  <S,>-algebra B there is exactly one  <S,>- homomorphism from A to B.  The unique homomorphism from an initial algebra A to an algebra B is sometimes refered to as the initial homomorphism  from A to B
end

Initial algebra have two particularly important properties that will concern us at this time.

  1.  For each signature there are initial algebras
  2. All initial algebras of a given signature are isomorphic.

Definition: Let <S,> be a signature then a <S,>-term is a string made up of operators from ,  parentheses and comma according to the following rules:
 
  1. if "",s for  sS  then "( )" is a  <S,>-term of sort s (such a term is called a constant term).
  2. if w,sfor wS* , sS,  and for each i=1,...,|w|,  ti  is a <S,>-term of sort wi,  then "(t1,...,t|w|)"  is a <S,>-term  of sort s.
end

Notes:

  • The first rule is really redundant (i.e., implied by the second line).
  • It is common practice to omit the parentheses on "constant terms", i.e., terms of form "( )" ,  we will not follow this practice.
  • What we have written above as "(t1,...,t|w|)"  is an informal presentation of the actual string which, in accordance with our formal, mathematical definition of string is a  mapping and not a sequence of symbols on a page (and in particular, not a sequence of symbols with an ellipsis "..." in the middle of it).  Given that for each i=1,...,|w|,  ti has length |ti |,  then the actual string is the mapping, s, from the set {1,..., 2+|t1|+...+|t|w||+ |w|} to the set consisting of the symbols in  plus left parenthesis, "(", and right parenthesis, ")" and comma, ",".such that

    •  
  • s(1) = 
  • s(2) = (  [left parenthesis]
  • s(2+j) = t1,j  for j=1,...,|t1|
  • s(2+|t1|+1) = ,  [comma]
  • s(2+|t1|+1+j ) = t2,j  for j = 1,...,|t2|
  • s(2+|t1|+1+|t2|+...+|t|w|-1|+1) = , [comma]
  • s(2+|t1|+1+|t2|+...+|t|w|-1 |+1+j)  = t|w|,j  for j=1,...,|t|w||
  • s(2+|t1|+|t2|+...+|t|w||+|w| = )  [right parenthesis]
    • Definition:  Given <S,>-terms t and t' we say that t is a subterm of t'  if, where t' = "(t1,...,t|w|)" that either t =t' or t is a subterm of one of the ti.  We say  t is a proper subterm of t'  if,  t is a subterm of t'  but tt'.
    end

    Example:  For the signature SigP:

    some typical SigP-terms are:
     
    "zero( )",
    "add(zero( ), succ(zero( )))"
    "mult(add(succ(zero( )), succ(zero( ))), succ(succ(zero( ))))"
    The term "zero( )"  is a subterm in all the examples.  The term "succ(zero( ))"  is a subterm of the last two examples.
    end

    Definition:For every signature <S,> the <S,>-terms  form a  <S,>-algebra  T, called the <S,>-term algebra,  where

    1. For each s in S, Ts, the carrier of sort s,   is the set of all <S,>-terms of sort s
    2. For each w,s and ti  for i=1,...,|w|, we define  T( t1,...,t|w|)  to be the string (t1,...,t|w|)    -- more formally,  T( t1,...,t|w|)  is the string that results from concatenating together the strings "(",  t1 , ",", t2, ",", ...,t|w|   and  ")" in the indicated order.
    end

    Theorem: The algebra T is an initial <S,>-algebra .

    Proof: What we must show is that for each  <S,>-algebra, A, there is one, and only one, homomorphism hA: TA.
    As a first step we define an S-ary function  h:U( T)U(A) by employing the above inductive definiton of the S-ary set of <S,. >-terms.

    Let t be an <S,>-term

    1. If   t = ( ) where (,s)  for some sS then define  h(t) = A
    2. If  t = (t1,...,tn) where (w,s),  n=|w| and h  is defined on each ti,  then define  h(t)= A (hw(1)(t1),...,hw(n)(tn))
    By inspection we see that end

    The algebra Tis not the only initial <S,>-algebra, indeed there are infinitely many.  However, as the following result show, they are all isomorphic and so may be said to be essentially the same except for notation.

    Theorem:  If  A and B are initial <S,>-algebras then they are isomorphic,  that is, there exist homomorphism  h:AB  and g:BA such that hg = 1B  and gh = 1A  where 1A :AA and 1B  :BB are the indicated identity homomorphisms.

    Proof: Since A is initial there must exist a unique morphism  h:AB.  Since B is initial there must exist a unique morphism g:BA.  But then   hg:BB and gh: AA.  But 1B :BB and so, by uniqueness of initial homomorphisms, we must have  hg = 1B   Similarly we get gh = 1A  .
    end
     

    Initial Homomorphisms on the UA-Calculators

    The UA-calculators have an JavaScript-function (i.e. value returning program) aitch(algname, term) which when applied to the name, algname, of a <S,>-algebra, and to a <S,>-term, term, gives the result of applying, to that term, the unique homomorphism from Tto the named algebra.   Try these examples: Try editing the examples by changing the algebra name to "alg_B", "alg_C", "alg_D" or "alg_E".

    These examples suggest that the result is that the given initial homomorphism from  T to the named algebra evaluates the term using the operations defined in the algebra.

    Some First Applications of Initality

    The significance of initial homomorphisms is that they provide a means for evaluating  <S,>-terms in any desired <S,>-algebra.  The process of evaluation is so simple and  uniform that we can implement it with the above program aitch(algname, term).   By choosing appropriate signatures and algebras we can define many significant functions.  The remaining chapters in Part I are largely dedicated to some especially significant examples of the use of initial homomorphisms.  The primary example is the description of the syntax, semantics and compilation of a simple programming language, LANG1, completely in terms of initial homomorphisms.   While we give many examples, see list below,  there are still many applications of initiality that we will not cover herein.  We close this section by showing how, for the signature, SigQ, we can describe many functions on SigQ terms using initial homomorphisms.

    Recall that, SigQ is the signature

    name: sigQ

     sorts: {int}

     operators:
     zero: -->int
     JSInt: -->int
     pred:int-->int
     succ:int-->int
     add:int.int-->int
     mult:int.int-->int

    End of signature sigQ.

    where JSInt(str) is a predicate (a JavaScript program) which determines whether or not a given string, str, corresponds to a (JavaScript) integer. What it actually does is determine whether or not the built-in JavaScript method parseInt(str)  converts str to an integer.

    Example:  The evaluation of SigQ-terms using the "obvious interpretation" of the operators can be done using alg_AA and the program aitch.For example, try performing aitch("alg_AA",  "add(3( ), mult(17( ), 5( )))") 
    Note that you can display the definition of the algebra named "alg_AA", by performing algDisplay("alg_AA")

    Example:  The set of constant operators occuring in a term.

    We claim that the desired SigQ-algebra is the algebra  alg_BB where
     

    the carrier of alg_BB is the set of all finite subsets of the set of JavaScript integers.

    alg_BB(zero) = {0}
    alg_BB(str) = {n} if  str is a string representing the JavaScript integers n.
    alg_BB(pred)(s) = s
    alg_BB(succ)(s) = s
    alg_BB(add)(s, s') = ss'
    alg_BB(mult)(s, s') = ss'

    We capture this algebra on the UA-Calculators with the algebra named "alg_BB" which is given as follows:

               The signature of alg_BB is: sigQ

     
    The carriers of alg_BB are:
       ["not specified"]
    // the carrier is the set of  JavaScript strings representing sets (e.g., "{1, 55, 70, 2}" is an element of the carrier  )

    The operations of the algebra alg_BB are:
       ["zero", "'{0}'"]
       [JSInt, mSet]
       ["succ", "arg[1]"]
       ["pred", "arg[1]"]
       ["add", "setUnion(arg[1],arg[2])"]
       ["mult", "setUnion(arg[1],arg[2])"]

    End of algebra alg_BB

    Note that this algebra actually has a different carrier (consisting of strings) than the algebra first proposed (which had  abstract sets of JavaScript integers in its carrier) -- this is because JavaScript does not have a data type whose elements are abstract sets so we have to make use of their syntactic counterpart.

    For example try the following on a UA-Calculator
     

    aitch("alg_BB",  "mult(add(13( ), succ(zero( ))), 3( ))")

    end

    Example:   The depth of a term.
    We claim that the desired SigQ-algebra is the algebra  alg_CCwhere
     
    the carrier of alg_CC is the set  of JavaScript integers.

    alg_CC(zero) = 1
    alg_CC(str) = 1 if  str is a string representing a JavaScript integer
    alg_CC(pred)(n) =  n+1
    alg_CC(succ)(s) = n+1
    alg_CC(add)(n, p) = 1+max(n, p)
    alg_CC(mult)(s, s') = 1+max(n, p)

    We capture this algebra on the UA-Calculators with the algebra named "alg_CC" which is given as follows:

              The signature of alg_CC is: sigQ

    The carriers of alg_CC are:
       [""]

    The operations of the algebra alg_CC are:
       ["zero", "1"]
       [JSInt, retOne]
       ["succ", "1+arg[1]"]
       ["pred", "1+arg[1]"]
       ["add", "1+Math.max(arg[1],arg[2])"]
       ["mult", "1+Math.max(arg[1],arg[2])"]

    End of algebra alg_CC

    where retOne is a function which always returns the integer 1.

    Example:  Alternative notations for expressions.
    To define our term algebras we used a particular definition of <S, >-term that employed a slight modification of what is usually called "prefix notation".  There are many other notations which work just as well but have a different appearance.  For example, here are five different notations for what is essentially the same term

    add(4( ),  mult( add(8( ),succ(3( ))), 7( )))  our prefix notation
    add(4,  mult( add(8,succ(3)), 7))        standard prefix notation
    (4+((8+succ(3))+7)                                            infix notation
    4 8 3 succ + 7 * +                              reverse polish notation
    (+ 4 (* 8 (succ3)) 7) )                            Cambridge notation

    The terms are "essentially the same"  in that we could have defined term algebra starting from any of these notations and have gotten an initial algebra that was isomorphic to the one we chose to use.  The initial homomorphisms from T to these these other initial algebras provide a translation from our system of notation for terms to these other systems of notation.  For example,  here is the algebra for reverse polish notation for Sig_Q-terms:

    the carrier of alg_DD is the set  of JavaScript strings

    alg_DD(zero) = "0"
    alg_DD(str) =str if  str is a string representing a JavaScript integer
    alg_DD(pred)(n) =  "s pred"
    alg_DD(succ)(s) = "s succ"
    alg_DD(add)(n, p) = s s' add
    alg_DD(mult)(s, s') = s s' mult


    The corresponding algebra for the UA-calculators is:
     

     The algebra alg_DD

    The signature of alg_DD is: sigQ

    The carriers of alg_DD are:
       [""]

    The operations of the algebra alg_DD are:
       ["zero", "1"]
       [JSInt, id]
       ["succ", "arg[1]+' succ'"]
       ["pred", "arg[1]+' pred'"]
       ["add", "arg[1]+' '+arg[2]+' +'"]
       ["mult", "arg[1]+' '+arg[2]+' *'"]

    End of algebra alg_DD

    end

    More Examples:  For further,  and more significant,  examples of the uses of initial algebras see: