[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_7_Semantics
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Dec 13 11:52:52 PST 2010



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

      3. SYMBOL::=
        1. representation::#lexeme,
        2. type::Types,
        3. 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)::=$
        1. syntax::#lexeme,
        2. semantics::T.objects,
        3. For some p:meaning_in(T),
        4. syntax::=p.1st,
        5. semantics::=p.2nd.

      18. |-For p:@meaning_in(T),
      19. p in Syntax_semantics(T)(syntax)->(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

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    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_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. 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. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html


  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.