The Semantics of LANG1

The Mathematical Semantics
The Semantics In Java Script
Some Examples of LANG1 Semantics

Earlier we showed how the translation from the abstract syntax of LANG1 to the concrete syntax of LANG1 was given by a homomorphism.  That homomorphism was the unique homomorphism from the initial LANG1Syn-algebra, alg_LANG1Abs, to the LANG1Syn-algebra, alg_LANG1Conc.   The semantics of LANG1 is  given by  the unique homomorphism  from  alg_LANG1Abs to an appropriate LANG1Syn-algebra alg_LANG1Sem.  While the carriers of alg_LANG1Conc were strings, the carriers in alg_LANG1Sem, of sorts <ae>, <be> and <st> are functions!

     alg_LANG1Sem(<id>) =     Id = { "a", "b", ..., "z"}

     Let  Stt be the set of all total mappings from  Id = { "a", "b", ..., "z"} to Z = {...-1,0,1,...}  (the "set of integers")

     alg_LANG1Sem(<ae>) = the set of all partial mappings  SttSttxZ

     alg_LANG1Sem(<be>) = the set of all partial mappings SttStt x {true, false}

     alg_LANG1Sem(<st>) = the set of all partial mappings SttStt

In what follows below we will present a somewhat more restricted semantics that is compatible with the limitations of JavaScript and thus possible to exercise using our programs that implement algebras and free constructions.   For this implementation we will take Z to be the set of all integers between, and including,  -2,147,483,648  and + 2,147,483,647.   We will implement the states as JavaScript arrays such as [["a", 12], ["b", 3], ["c",9]],  which corresponds to the partial function from { "a", "b", ..., "z"} to Z = {z |   -2,147,483,648  +2,147,483,647 } that takes "a" to 12, "b" to 3,  c" to 9 and is otherwise. undefined.

The Mathematical Semantics

  It is convenient to present the semantics by first defining the semantics of the "primitives" of the language and then using this as a basis for defining the algebra alg_LANG1Sem.   The primitives are given by the following sub-signature, PrimSyn, of  LANG1Syn:

The Signature PrimSyn in mathematical form:

 name: PrimSyn

 sorts: {<id>, <be>, <ae>, <st>}

 PrimSyn(<id>) = {LANG1var}
 PrimSyn(<be>) = {tr, fa}
 PrimSyn(<ae>) = {LANG1Int}
 PrimSyn(<be>, <be>) = {not}
 PrimSyn(<be>.<be>,<be>) = {and}
 PrimSyn(<ae>.<ae>,<be>) = {eq, leq}
 PrimSyn(<ae>,<ae>) = {succ, pred}
 PrimSyn(<ae>.<ae>,<ae>) = {add, mult}

End of signature LANG1PrimSyn.

The "obvious" semantics of these is the algebra alg_LANG1Prim in which we take the carriers to be

alg_Prim<be> = {"true", "false"}
alg_Prim<ae> =  Z
alg_Prim<id>  = {"a", "b",...,"z"}
then we take the operations to be the familiar ones,
[["tr", "true"],
["fa", "false"],
[LANG1Int(str),  str2num],
["not", "!arg[1]"],
["and", "arg[1] && arg[2]"],
["eq", "arg[1]==arg[2]"],
["leq", "arg[1]<=arg[2]"],
["succ", "arg[1]+1"],
["pred", "arg[1]-1"],
["add", "arg[1]+arg[2]"],
["mult", "arg[1]*arg[2]"]
All these operations can be "lifted" in a straight forward manner to operations on the carriers of alg_LANG1Sem.

For example:  given elements a1, a2LANG1Sem(<ae>) ( recall then that this means that ai:Stt --> Stt x Z for i=1,2,) and  a state Stt, we compute LANG1Sem(mult)(a1, a2)() by applying the function a1 to  to get a  pair <', z>,   next we apply  the function a2 to '  get a pair <'', z'>  finally we pair "  with the product  alg_Prim(mult)(z, z') = z * z'  to get the final result <'',  z * z'>.

This can be expressed more succinctly and mathematicaly as

    LANG1Sem(mult)(a1, a2) =  ((idStt x alg_Prim( mult))(a2xidZ)a1:SttStt x Z

If the above "x" notation (as in (a2 x idZ), etc.) is unfamiliar then click here for an explanation.

Lifting takes care of the semantics of all boolean and arithmetic operators (i.e., operators of sort <be> or <ae>)  with the excepton of id2ae. What is wanted there is a function from Id = { "a", "b", ..., "z"} to { f:SttSttxZ}. Clearly the desired function is such that for any iId, and Stt

 LANG1Sem(id2ae)( i )( )  =  <( i )>
It remains then to give the semantics for the statements (i.e., the operators of sort <st>), namely, assign, compos, if and wdo (while-do).

Assign:  Given an identifier   iId,  an arithmetic expression  a:SttStt x Z and a state Stt, what we want is

LANG1Sem(assign)( i, a )( )  = '
where , if  a( ) =  < ", v>  then , for each jId, '( j ) equals v if  j = i  and equals "( j ) if  ji.

Compos: Given statements  s1 :SttStt,  and s2 :SttStt,  and a state Stt, what we want is

LANG1Sem(compos)( s1, s2 )( )  =  s2(s1())
if:  Given  a boolean expression, b:SttStt x {true, false}, :statements  s1 :SttStt,  and s2 :SttStt,  and a state Stt, what we want is that, if   b( ) =  < ", v>, then, LANG1Sem( if )(b,  s1,  s2 )( ) = s1(") if  v = true, while LANG1Sem( if )(b,  s1,  s2 )( ) = s2(")  if v = false.

wdo: Given  a boolean expression, b:SttStt x {true, false}, a statement s1 :SttStt,  and a state Stt, what we want is that  if b( ) =  < ", v>, then,  LANG1Sem(wdo)(b,  s1 )( )   = LANG1Sem(wdo)(b,  s1 )( s1)) if  v = true, while LANG1Sem(wdo)(b,  s1 )( )   =  if v = false.

Theorem: Let hSEM:alg_LANG1Abs   alg_LANG1Sem be the indicated initial homomorphism.   Then every element in the image of   hSEM,<be>   and hSEM,<ae> is a total function  "without side effects",  that is,

  •  if b: SttSttx{true, false} in the image of   hSEM,<be> then for every Stt then there exists v{true false} , such that b()  = <, v>
  • if a: SttSttxZ in the image of   hSEM,<ae> then for every Stt then there exists vZ, such that a()  = <, v>
  • end

    The Semantics in JavaScript

    To program the semantics of LANG1 in JavaScript is is convenient to represent the states (the elements of Stt) as arrays of  identifier/value pairs rather than as functions.   Furthermore, in order to avoid having to write out long arrays we will only require that pairs be given for non-zero values.   Thus, for example, the array  [["a", 22], ["b", 3]]  can be viewed as an abbreviation for the mapping :Id Z such that ("a") = 22, ("b") = 3  and (i) = 0 for all other identifiers.

    We make use of three specially defined functions on identifier/value pairs:

               function apG(arr, arg)    //  returns the value in the last pair in array arr with first element arg
               {var apGout = 0;
               for (var i=0; i<arr.length; i++) if (arr[i][0]==arg) apGout=arr[i][1];
               return apGout

    function repG(arr, key, val)   // modifies the array  arr  so that it contains the pair [key, val] (replacing any earlier pair starting with key)
    { var tst = true
      for (var i=0; i<arr.length; i++)  if (arr[i][0]==key) {arr[i][1]=val; tst=false}
      if (tst) arr[arr.length]=[key, val]
      return arr

    function chgG(arr, arg, val)  // appends a pair  [key, val] to the end of the array arr
    {arr[arr.length]=[arg, val]
    return arr

    Then, using the above special functions,  we implement the mathematical semantics of LANG1  almost directly in JavaScript using the following JavaScript functions

             function numout(itgr) { return new Function("return new Function('ff', 'return [ff, "+itgr+"]')"))( ) }

              function varout(item){return "'"+item+"'"}

              trueout = new Function("return Function('ff', 'return [ff, true]')")

              falseout = new Function("return Function('ff', 'return [ff, false]')")

              function notout(be)
              {  return Function("ff", "var zz = "+be+"(ff); return [zz[0], !zz[1]]") }

              function andout(be1, be2)
              {  return Function("ff", "var zz = "+be1+"(ff); var ww  = "+be2+"(zz[0]); return  [ww[0], zz[1] && ww[1]]") }

              function addout(ae1, ae2)
              {  return Function("ff", "var zz = "+ae1+"(ff); var ww = "+ae2+"(zz[0]); return  [ww[0], parseInt(zz[1]) + parseInt(ww[1])]") }

              function multout(ae1, ae2)
              {  return Function("ff", "var zz = "+ae1+"(ff); var ww = "+ae2+"(zz[0]); return  [ww[0], parseInt(zz[1]) * parseInt(ww[1])]") }

              function id2aeout(id)
             {  return Function("ff", "return [ff, apG(ff, '"+id+"')] ") }

              function assignout(id, ae)
              {  return Function("ff", "return repG(ff, '"+id+"',  "+ae+"(ff)[1])") }

              function assignTrace(id, ae)
              {  return Function("ff", "return chgG(ff, '"+id+"',  "+ae+"(ff)[1])") }

              function composout(st1, st2)
              {  return Function("ff", "zz = "+st1+"(ff); ww = "+st2+"(zz); return ww") }

              function condout(be, st1, st2)
              {  return Function("ff",  "var zz = "+be+"(ff); if (zz[1]) "+st1+"(ff) else "+st2+"(ff)")}

              function wdoout(be, st)
              {  return Function("ff", "if ("+be+"(ff)[1])  {return wdoout("+be+", "+st+")("+st+"(ff))} else {return ff}")

    The resulting algebra is then the following.

         UAObj_alg_LANG1Sem = new Algebra("LANG1syn",
              [numQ, numout ],    // note that numout is not quoted
              [LANG1Var, varout],  //recall that this is an identity function on Id (the set of identifiers)
              ["tr", "trueout( )"],
              ["fa", "falseout( )"],
              ["not", "notout(arg[1])"],
              ["and", "andout(arg[1], arg[2])"],
              ["eq", "eqout(arg[1], arg[2])"],
              ["leq", "leqout(arg[1], arg[2])""],
              ["id2ae", "id2aeout(arg[1])"],
              ["neg", "negout(arg[1])"],
              ["succ", "succout(arg[1])"],
              ["pred", "predout(arg[1])"],
              ["add", "addout(arg[1], arg[2])"],
              ["mult", "multout(arg[1], arg[2])"],
              ["assign", "assignout(arg[1], arg[2])"],
              ["assignT", "assignTrace(arg[1], arg[2])"],   // see note below
              ["compos", "composout(arg[1], arg[2])"],
              ["if", "condout(arg[1], arg[2], arg[3])"],
              ["wdo", "wdoout(arg[1], arg[2])"]
              ] )

         Note there are two different versions of the semantics for the assignment statement: assignout and assignTrace.  In the former the state just consists of the current values of the variables while in the latter the state is a sequential listing of the initial state followed by the sequence of all changes to the state.  Thus they actually correspond to two different definitions of the concept of state.

    Some Examples of  LANG1 semantics

    For the sake of brevity, we will allow partial states and write states as JavaScript arrays:   Thus,  a state in which  the only interesting variables are "a", "b" and "c" with respective values  10, 46, and 12, will be written as  [["a", 10], ["b", 46],  ["c", 12]] (or as a permutation of this array such as  [ ["b", 46], ["a", 10],  ["c", 12]] or  [ ["c", 12], ["a", 10], ["b", 46] ] ).   For convenience, the UA-calculator has a built-in state

            samplestt [["a", 10], ["b", 3],  ["c", 77]]

    Example:  The meaning of the expression "tr( )" should be a function which, given a state, s,   returns the  pair  [s, true].   To see that this is the case, use the UA-calculator to evaluate the expression   The problem here (pedagogical) is that the state is a finFunct and thus full of irrelevant material.

            aitch("alg_LANG1Sem", "tr()")(samplestt)

    Example:  Recall that the LANG1Syn-expression

         "compos(assign(b( ), 1( )), wdo(leq(1( ), id2ae(a( ))), compos(assign(b( ), mult(id2ae(a( )), id2ae(b( )))), assign(a( ), pred(id2ae(a( )))))))"

    Is the abstract syntax of the LANG1 program with concrete syntax  b:=1 ; While (1 <= a) do b:=(a * b) ; a:=(a-1) od., that is, it is "the usual program" for the factorial function .Thus, starting from the above state,  [["a", 10], ["b", 3],  ["c", 77]],  it should terminate in the state  [["a", 0], ["b", 3628800],  ["c", 77] (since 10! = 3628800).    The complete text to perform is:

     aitch("alg_LANG1Sem", "compos(assign(b( ), 1( )), wdo(leq(1( ), id2ae(a( ))), compos(assign(b(), mult(id2ae(a( )), id2ae(b( )))), assign(a( ), pred(id2ae(a( )))))))")(samplestt)

    It is not necessary to use the variable samplestt,  that is, you can get the same result using the expression:

    aitch("alg_LANG1Sem", "compos(assign(b( ), 1( )), wdo(leq(1( ), id2ae(a( ))), compos(assign(b(), mult(id2ae(a( )), id2ae(b( )))), assign(a( ), pred(id2ae(a( )))))))")( [["a", 10], ["b", 3],  ["c", 77]])
    The value of "a" can be modified in the state  [["a", 10], ["b", 3],  ["c", 77]], and the program can be run again to compute other factorials.   However,  the answer will be incorrect for  values of "a" greater than 21.  This is because 22! is too big -- it is not an integer according to the semantics we have given to LANG1 (which only has integers in the range from  - 2,147,483,648  to   + 2,147,483,647  -- this choice being made to make it compatible with the limitations of JavaScript).  The program will also fail for values of "a" less than 1.