.Theory
1. SEMANTICS::=
   Net{

   1. lexeme::Sets. -- the words of the language
   2. values::Sets. -- the meanings to be attached to words, phrases and so on.

   3. SYMBOL::=
      Net{

      representation::#lexeme,
      1. type::Types,
      2. meaning::values
         }.

   4. symbols::@SYMBOL.

      
      

   5. |-For x:#lexeme, T:Types, m:T, symbol(x, T, m) iff (representation=>x, type=>T, meaning=>m) in symbols.
   6. [compare SERIAL.PARALLEL]

      
      

   7. (|- validity): For all x, T, 0..1 m (symbol(x, T, m)).

   8. references::=representation o symbol o /type,
      
   9. |-For T, references(T)={x:#lexeme || for some m:T ( symbol(x, T, m) )}.

   10. denotation::=the o meaning o symbol o /(representation, type).

   11. denotation::=The meaning of the symbols which have a given representation and type

       
       

   12. (validity) |- For x, T, denotation(x, T)=the m:T(symbol(x, T, m)).

       A syntactic-semantic pair is made up of a string and expression with a known type and defines the meaning of that string in that type,

   13. meaning_in::=(representation, meaning) o /type o symbols,
       
   14. (def) |- For T:Types, meaning_in(T)={(x:#lexeme, t:T.objects) || symbol(x, T, t)}.
       
   15. (def) |- For T:Types, meaning_in(T) ==> @#lexeme(any)-(0..1)T.objects

       
       

   16. (validity) |- For p:@meaning_in(T), p in p.1st->p.2nd.

   17. For T, Syntax_semantics(T)::=$
       Net{

       1. syntax::#lexeme, semantics::T.objects,
       2. For some p:meaning_in(T), syntax::=p.1st, semantics::=p.2nd.
          }

       
       

   18. |-For p:@meaning_in(T),
   19. p in Syntax_semantics(T)(syntax)->(semantics).

   
   }=::SEMANTICS.

   Semantic Equivalences

   Given that the semantics of a set of syntactic objects is given by a function:

2. denotation::syntax->semantics, then we say that two syntactic objects are semantically equivalent if they have the same semantics:
3. equivalent::Equivalence_relation(syntax)= (= mod denotation).

   A powerful tool fro the language definer is to supply the semantics for a part of the language and then provide a set of semantic equivalents. The MATHS definition form provides a natural way to do this:

4. For parameters, defined_form:: type = equivalent_expression

   Example in C

   This definition
5. For S:C.statement, a,b,c:C.expression, (for(a;b;c)S) ::C.statement= { a; while(b)S; c; }, means that C semantics does not have to define a for-loop. Similarly,
6. For a:C.pointer_expression, i:C.int_expression, a[i] ::= *(a+i). So, again K+R didn't have to give a formal definition of subscripts - See BCPL.

   The general syntax of such a definition is:

7. For T,T1,T2,...:Types, e(v1,...), f(v1,...): syntax(T), For v1:syntax(T1), v2: syntax(T2),... e(v1,v2,...) ::syntax(T)= f(v1,v2,...).

   See Transformational Grammars, Equivalence Relations, Types.Equality.

. . . . . . . . . ( end of section Semantics) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_2_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints, and give them a name. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents.

Notes on the Underlying Logic of MATHS

For a complete listing of pages by topic see [ home.html ]