.Theory
- SEMANTICS::=
Net{
- lexeme::Sets. -- the words of the language
- values::Sets. -- the meanings to be attached to words, phrases and so on.
- SYMBOL::=
- symbols::@SYMBOL.
- |-For x:#lexeme, T:Types, m:T, symbol(x, T, m) iff (representation=>x, type=>T, meaning=>m) in symbols.
- [compare SERIAL.PARALLEL]
- (|-validity): For all x, T, 0..1 m (symbol(x, T, m)).
- references::=representation o symbol o /type,
- |-For T, references(T)={x:#lexeme || for some m:T ( symbol(x, T, m) )}.
- denotation::=the o meaning o symbol o /(representation, type).
- denotation::=The meaning of the symbols which have a given representation and type
- (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,
- meaning_in::=(representation, meaning) o /type o symbols,
- (def)|-For T:Types, meaning_in(T)={(x:#lexeme, t:T.objects) || symbol(x, T, t)}.
- (def)|-For T:Types, meaning_in(T) ==> @#lexeme(any)-(0..1)T.objects
- (validity)|-For p:@meaning_in(T), p in p.1st->p.2nd.
- For T, Syntax_semantics(T)::=$
- |-For p:@meaning_in(T),
- p in Syntax_semantics(T)(syntax)->(semantics).
}=::
SEMANTICS.
Given that the semantics of a set of syntactic objects is given by a function:
- denotation::syntax->semantics,
then we say that two syntactic objects are semantically equivalent if they have the same semantics:
- 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:
- For parameters, defined_form:: type = equivalent_expression
This definition
- 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,
- 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:
- 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>>
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 ]
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
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
- 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).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- 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.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.