.Open Semantics
.Theory
SEMANTICS::=Net{
lexeme:: Sets. -- the words of the language
values:: Sets. -- the meanings to be attached to words, phrases and so on.
SYMBOL::=Net{
representation::#lexeme,
type::Types,
meaning::values
}.
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) ::=$ Net{
syntax::#lexeme,
semantics::T.objects,
For some p:meaning_in(T),
syntax::=p.1st,
semantics::=p.2nd.
}
|- For p:@meaning_in(T),
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:
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
. Example in C
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.
.Close Semantics