The Semantics of LANG1

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  z  +2,147,483,647 } that takes "a" to 12, "b" to 3,  c" to 9 and is otherwise. undefined.
 

The Mathematical Semantics

The Signature PrimSyn in mathematical form:
 

 name: PrimSyn

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

 operations:
 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"}

[["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]"]
]

For example:  given elements a₁, a₂LANG1Sem(<ae>) ( recall then that this means that a_i:Stt --> Stt x Z for i=1,2,) and  a state Stt, we compute LANG1Sem(mult)(a_1, a₂)() by applying the function a₁ to  to get a  pair <', z>,   next we apply  the function a₂ 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

If the above "x" notation (as in (a₂ x id_Z), 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 )>

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

LANG1Sem(assign)( i, a )( )  = '

a( ) =  < ", v> 

Id, '( j )

ji

Compos: Given statements  s₁ :SttStt,  and s₂ :SttStt,  and a state Stt, what we want is

LANG1Sem(compos)( s₁, s₂ )( )  =  s₂(s₁())

b:SttStt x {true, false}

s₁ :SttStt

s₂ :SttStt

b( ) =  < ", v>

LANG1Sem( if )(b,  s₁,  s₂ )( ) = s₁(")

LANG1Sem( if )(b,  s₁,  s₂ )( ) = s₂(") 

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

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

 if b: SttSttx{true, false} in the image of   h_SEM,<be> then for every Stt then there exists v{true false} , such that b()  = <, v>

if a: SttSttxZ in the image of   h_SEM,<ae> then for every Stt then there exists vZ, such that a()  = <, v>

The Semantics in JavaScript

Id Z

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
}
 
 

         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

        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]])