<p>What I am writing is essentially contained in babou's answer. 
But I wanted to express it a bit differently 
emphasizing the point of defining formal semantics.</p>

<p>A formal semantics is a mapping from one class of mathematical structures $P$ 
(e.g. programs in a programming language) 
to another class of mathematical structure $S$ (e.g. domains):
$[[ \cdot]] : P \to S$.</p>

<p>Different conditions required from the mapping give different kinds of semantics.</p>

<p>What conditions should we require from the mapping? 
That depends on what we want to do with the semantics.
The required denotational properties depend on 
what your intention is in extending the language, 
a formal semantics might be wrong or right depending on that intention.</p>

<p>Let's step back for a second and look more generally why we define formal semantics.</p>

<blockquote>
  <p>The point of formal semantics is that 
  we take the class of mathematical structures that we want to study and 
  map it to another class of mathematical structures that we already know something about, and we use that knowledge to study the original class of structures. </p>
</blockquote>

<p>If you don't know what denotational properties you require from your denotational semantics of your language and have no use for it, 
what is the point of to providing a denotational semantics?
It will not add any confidence that your extended language will behave as you want.</p>

<p>On the other hand, 
if you know how the denotational semantics should be
based on your intuitive informal semantics and your intention in extending the language,
then you can use that to formally check that 
your programming language matches your intuitive semantics and 
will work as you intended 
(w.r.t. the requirements you had for your denotational semantics).</p>

CC BY-SA 3.0
2014-07-24T22:33:24.227Z
I disagree regarding the point of defining formal semantics, that you want to
emphasize. I develop my dissenting view at the end of my answer.  - -
- - - - - - - - - - Also, I guess everything can be seen as a mapping, but
this is not usually the way various formal semantics are presented,
though it is definitely the case for denotational semantics. Is your
intent actually to cover all formal definitions of semantics by the
statement in your second paragraph?
babou
CC BY-SA 3.0
2014-07-24T22:48:49.910Z
@babou, I read your view. _Mathematically_ there is no difference between meaning and syntax, considering one to be meaning is our informal intuition not mathematical. There is no mathematical way to show an informal concept matches a formal one (through we can gather evidence e.g. by considering different formalizations and showing they are compatible.) What you describe is a special case of what I wrote:we believe the semantics matches our intuitive intended meaning, and use this knowledge to show that syntax can be assigned meaning.
Kaveh
CC BY-SA 3.0
2014-07-24T23:18:45.850Z
Side notes: the view I expressed is partly based on Girard's writtings like [truth, modality, and intersubjectivity](http://iml.univ-mrs.fr/~girard/truth.pdf) and his "broccoli logic" joke. You can replace mapping with other kinds of relations between class of structures if you prefer, being a mapping is not essential for my points: there is no mathematical distinction between syntax and formal semantics, blindly defining a formal semantics for a language adds nothing. What I wrote does not imply the mathematical structure should be pre-existing.
Kaveh
CC BY-SA 3.0
2014-07-24T23:54:12.823Z
Sorry, I did not manage to parse your sentence beginning with
"Mathematically". So I cannot answer that usefully. Little point
discussing it since I do not know Girard's view. I can actually agree
with it if you consider relation, rather than map, because that is
clearly one of the thing we do with semantics, in order to construct
it (and revise beliefs). But, like the OP, I have used formal
semantics for practical work. And it has another major role, which is
accurate communication between people. It can be reduced to the
same. But then your statement is far too abstract.
babou
CC BY-SA 3.0
2014-07-25T03:31:55.373Z
I don't see what cofuses you, in any case it was restated in the following comment. The statements are not "far too abstract" at all. Btw, if you prefer that I don't refer to your answer let me and I will remove it.
Kaveh
CC BY-SA 3.0
2014-07-25T13:53:03.737Z
What confuses me is the syntactic role of "not mathematical" in that sentence.
I think I have some idea of what is intended by your 3 lines statement. I
still disagree on the way it was made, but I do not think discussing
it further will lead anywhere. I think the level of scientific discourse
should be adapted to its purpose, context and intended recipient. This
is actually a frequent problem on SE.
babou
CC BY-SA 3.0
2014-07-30T20:50:40.060Z
@Kaveh: I too couldn't understand in what sense you say is syntax is "mathematical".  In any case, syntax is always countable whereas semantic structures are rarely countable.  So, that is quite a precise mathematical difference that you can't brush off.
Uday Reddy
CC BY-SA 3.0
2014-07-30T22:46:04.743Z
@Uday, syntax can be uncountable (e.g. in model theory we deal with uncountable languages). My statement was not that syntax is mathematical, my statement is that referring to some mathematical structures as (formal) semantics is based on our _informal_ intuition, not a mathematical property of those structures. The moral take away is this: *don't blindly provide formal semantics just because others have provided formal semantics for their languages, having a formal semantics doesn't mean anything by itself, you have to know why you want a formal semantics.*
Kaveh
CC BY-SA 3.0
2014-07-30T22:46:35.860Z
I think Girard's broccoli logic example is illustrative: 1. add a new binary logical operator called broccoli and denoted by $\clubsuit$ to classical propositional logic, 2. consider an extension of Boolean algebra called broccoli algebras with a new broccoli operator satisfying suitable rules, 3. it is straight forward to show soundness and completeness of broccoli logic w.r.t. to free broccoli algebra semantics. But what is the point of providing this semantics and proving soundness and completeness?
Kaveh
CC BY-SA 3.0
2014-07-31T13:27:50.740Z
@Kaveh.  Ok you want to emphasize the "philosophical" aspect of what semantics is about.  That is perfectly fine.  However, note that broccoli semantics may not always be trivial.  For typed lambda calculus, for example, you can't show completeness for "broccoli algebras" but you can show it for "broccoli categories."  So, that says something fundamental about  the nature of typed lambda calculus!
Uday Reddy
CC BY-SA 3.0
2014-07-31T15:04:28.710Z
@Uday, my point is more practical than philosophical. It seems to me that they didn't know why they wanted a denotational semantics, and that was the root of their confusion. Sure, I mentioned boroccoli logic to demonstrate the point that one should not _blindly_ go for providing semantics, I am not saying algebraic semantics are not useful.
Kaveh
CC BY-SA 3.0
2014-07-31T15:30:18.113Z
Btw, I see Andrej and Neel made somewhat similr remarks regarding distinction between syntax and semantics: ["Of course, such a view requires one to differentiate between formal manipulation of syntax and "true" mathematics. This is necessarily a non-mathematical distinction."](http://cstheory.stackexchange.com/a/3588/) ["No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense."](http://cstheory.stackexchange.com/a/21543/)
Kaveh
CC BY-SA 3.0
2014-07-23T13:44:42.797Z
2014-07-23T13:44:42.797Z
Kaveh
<p>There are two aspects of correctness:</p>

<ul>
<li><p>one is internal consistency, so that whatever you define can be assigned a
proper meaning.  Typically, that is why you are told that the domains
you use must be CPO, so that you can have limits used to defined the
semantics of some looping/recursive construct, whether program or data.</p></li>
<li><p>the other is consistency with you intended semantics. This is a
general problem with specification of program, or languages or
anything else. When you design something, the correctness of your
design can only be checked with respect to some reference, and in
this case formal reference. I develop this second point.</p></li>
</ul>

<p>If a child ask you for a car with 4 wheels. You may buy him a small
automobile, and be in agreement with the specification. But what he
actually wanted was a new passenger car for his train, and the child
will be unhappy. The specification is incomplete (or incorrect) and as a consequence
the end result may not adequate.</p>

<p>So a specification may not exactly reflect your intent. You can prove
that your realisation of a car (or your compiler) is conformant with
specification, but you have no way to prove that your specification is
conformant with whatever intent is in your mind.</p>

<p>The denotational semantics of a language is a specification of the
language, and you have no way to prove that it conforms what is in
your mind, unless you can express that formally, which will just be
annother specification, of which you are not sure it conforms your
intent.</p>

<p>However, if you make your intent more precise in several different
ways, you can check that your various attempts at specifying what you
want are consistent, which will give you greater belief that what you
are doing conforms what you want. But there is no way to be certain.</p>

<p>For example, you can attempt to prove the consistency of your
denotational semantics with another formal specification or semantic
definition, as suggested in your question. These specifications do not
have to be complete specifications. It may only be a statement of some
property of your language.</p>

<p><strong>Consistency with previous version of the language</strong></p>

<p>Still, in your case, there is something that you may do, that you should do.</p>

<p>The language you are considering is an extension of another language,
that may have a formally defined semantics.</p>

<p>Then one thing that users will expect is that the extended language
will work like the original one when the new features are not used.</p>

<p>Hence, one thing you should prove is that any program of the original
language is given the same semantics in the new language.</p>

<p>It may be however that there has been some changes so that
programs have to be adapted for the new extended version of the language. Then
if you can formally defined how program P for the original language is
to be tranformed into another program P' in the extended language, then
you ideally should prove that this tranformation is semantics preserving.</p>

<p>If such a tranformation of programs to the new language version is necessary, and not clearly obvious, it may be worth defining semantics of the original language (if it does not exist yet) in order to prove the correctness of the transformation.</p>

<p><strong>Post-scriptum</strong></p>

<p>I have to disagree with <a href="https://cstheory.stackexchange.com/questions/25322#25325">Kaveh's answer</a> main statement that</p>

<blockquote>
  <p>The point of formal semantics is that we take the class of
    mathematical structures that we want to study and map it to another
    class of mathematical structures that we already know something
    about, and we use that knowledge to study the original class of
    structures. </p>
</blockquote>

<p>The problem is that, in general, we have no mathematical structure to
begin with. At best we have a syntax, defining sentences in a
language. <strong>The first point of formal semantics is to associate a
meaning with sentences (programs) following this syntax</strong>, and do it
formally so that we can study this meaning and prove properties about
it. So the semantics is indeed taking syntactic sentences to a class
of mathematical structures theat we are supposed to understand. But
<strong>We are not interested in studying the syntax</strong>, which is the only
original structure that is being mapped. We may have an intuitive
meaning in mind, but it can hardly be the domain of a mathematical
map.</p>

<p>We are indeed interested in studying our intended meaning for programs
though the mapping of the syntax that expresses them into semantics.
But the mapping applies only to the syntax, not to the intended
meaning we hope to study ... if the semantics we define does conform
our intent.</p>

<p>What we may do, though, is take two mapping from the same syntactic
structure into different classes of mathematical stuctures, and prove
the existence of a mapping between these structures, with properties
that represent some form of consistency of the two definitions.</p>

CC BY-SA 3.0
2014-07-23T12:21:54.547Z
2014-07-24T21:09:56.947Z
2017-04-13T12:32:28.167Z
babou
<p>We have a programming language and its denotational semantic, 
like Tony Hoare's <a href="https://en.wikipedia.org/wiki/Communicating_sequential_processes" rel="nofollow">CSP</a> with its syntax and denotational semantic 
e.g. stable failure and UTP. </p>

<p>We want to extend the language (its syntax and semantics) by
adding new operators to the language. 
After given an informal definition for each new operator, 
we want to provide a denotational semantic for the extended language.</p>

<p>We have been told that </p>

<ul>
<li>the denotational semantic must be a domain, </li>
<li>the denotational semantic must distinguish what your language want to distinguish intuitively, </li>
<li>the denotational semantic must be consistent with its operational semantic or algebraic semantic.</li>
</ul>

<p>What requirements should our denotational semantics for the extended language satisfy to be correct?
Are there any criteria to distinguish between correct and incorrect denotational semantic for a programming language? </p>

CC BY-SA 3.0
2014-07-27T02:23:58.213Z
1 Thank @Kaveh for your answers. Moreover thanks Kaveh for editing my poor English in my question statement.
zhuang
CC BY-SA 3.0
2014-07-27T02:24:26.667Z
2 Thank @babou for your answers.
zhuang
CC BY-SA 3.0
2014-07-27T02:29:16.187Z
3 This part is what I learned from babou, he tells me why the denotational semantic must be cpo or domain. and most important he show me what's the difference between the syntax, intuition and denotational semantic. As babou's answer, the intuition is used to comprehend the syntax, we can not prove the intuition is consistent with denotational semantic when the intuition can not stated formally. in some extent, the intuition  can be formally stated by operational semantic, and we can prove consistent between operational semantic and denotational semantic.
zhuang
CC BY-SA 3.0
2014-07-27T02:33:33.577Z
4 In Kaveh's answer,  I can use the denotational semantic to formally check that my programming language matches your intuitive semantics and will work as intended. Such checking give us an true response, then we can use the convenience of mathematical models to give more complicated laws or prove the relations between the two statement with different syntax. and the definition in second paragragh is the formalism of denotational semantics. The operational semantic is based on the labled transition systems, and the operational semantic is the sequence of execution labels on the arc.
zhuang
CC BY-SA 3.0
2014-07-27T02:37:28.807Z
5  The difference of denotational semantic and operational semantic may help us resolve the disagreement between Kaveh and babou.
zhuang
CC BY-SA 3.0
2014-07-27T02:38:02.797Z
6 The denotaional semantic is used for build the foundation of relations of different syntax,for example, two sequential programs x:=1;x:=2  and x:=3;x:=2 have the same denotational semantics [[x:=1;x:=2]]=(true, x=2)=[[x:=3;x:=2]] where (true, x=2) is an elements in the Cartesian product of predicate. the operational semantic is based on labeled transition system, it is by steps. for x:=1;x:=2, in operational semantic, the first step is x:=1, and the second step is x:=2. Then we can see that the deno semantic usually used for proof and operational semantic can be checked with model checking.
zhuang
CC BY-SA 3.0
2014-07-31T13:28:47.930Z
Please be sure to look at the previous questions on the topic that StackExchange shows you on the side bar, especially the thread "What constitutes denotational semantics?"
Uday Reddy
<pl.programming-languages><semantics><denotational-semantics>
What requirements should a denotational semantics for a programming language satisfy to be correct?
zhuang
# What requirements should a denotational semantics for a programming language satisfy to be correct?

(Asked by: username_0 on 2014-07-23)

We have a programming language and its denotational semantic,
like Tony Hoare's [CSP](https://en.wikipedia.org/wiki/Communicating_sequential_processes) with its syntax and denotational semantic
e.g. stable failure and UTP.

We want to extend the language (its syntax and semantics) by
adding new operators to the language.
After given an informal definition for each new operator,
we want to provide a denotational semantic for the extended language.

We have been told that

* the denotational semantic must be a domain,
* the denotational semantic must distinguish what your language want to distinguish intuitively,
* the denotational semantic must be consistent with its operational semantic or algebraic semantic.

What requirements should our denotational semantics for the extended language satisfy to be correct?
Are there any criteria to distinguish between correct and incorrect denotational semantic for a programming language?

**Tags:** pl.programming-languages, semantics, denotational-semantics

> **Comments:**
> **username_0**: 1 Thank @username_2 for your answers. Moreover thanks username_2 for editing my poor English in my question statement.  
> **username_0**: 2 Thank @username_3 for your answers.  
> **username_0**: 3 This part is what I learned from username_3, he tells me why the denotational semantic must be cpo or domain. and most important he show me what's the difference between the syntax, intuition and denotational semantic. As username_3's answer, the intuition is used to comprehend the syntax, we can not prove the intuition is consistent with denotational semantic when the intuition can not stated formally. in some extent, the intuition  can be formally stated by operational semantic, and we can prove consistent between operational semantic and denotational semantic.  
> **username_0**: 4 In username_2's answer,  I can use the denotational semantic to formally check that my programming language matches your intuitive semantics and will work as intended. Such checking give us an true response, then we can use the convenience of mathematical models to give more complicated laws or prove the relations between the two statement with different syntax. and the definition in second paragragh is the formalism of denotational semantics. The operational semantic is based on the labled transition systems, and the operational semantic is the sequence of execution labels on the arc.  
> **username_0**: 5  The difference of denotational semantic and operational semantic may help us resolve the disagreement between username_2 and username_3.  
> **username_0**: 6 The denotaional semantic is used for build the foundation of relations of different syntax,for example, two sequential programs x:=1;x:=2  and x:=3;x:=2 have the same denotational semantics [[x:=1;x:=2]]=(true, x=2)=[[x:=3;x:=2]] where (true, x=2) is an elements in the Cartesian product of predicate. the operational semantic is based on labeled transition system, it is by steps. for x:=1;x:=2, in operational semantic, the first step is x:=1, and the second step is x:=2. Then we can see that the deno semantic usually used for proof and operational semantic can be checked with model checking.  
> **username_1**: Please be sure to look at the previous questions on the topic that StackExchange shows you on the side bar, especially the thread "What constitutes denotational semantics?"  

---

## 2 answers

### Answer by username_2 on 2014-07-23. Score: 4

What I am writing is essentially contained in username_3's answer.
But I wanted to express it a bit differently
emphasizing the point of defining formal semantics.

A formal semantics is a mapping from one class of mathematical structures $P$
(e.g. programs in a programming language)
to another class of mathematical structure $S$ (e.g. domains):
$[[ \cdot]] : P \to S$.

Different conditions required from the mapping give different kinds of semantics.

What conditions should we require from the mapping?
That depends on what we want to do with the semantics.
The required denotational properties depend on
what your intention is in extending the language,
a formal semantics might be wrong or right depending on that intention.

Let's step back for a second and look more generally why we define formal semantics.

> The point of formal semantics is that
> we take the class of mathematical structures that we want to study and
> map it to another class of mathematical structures that we already know something about, and we use that knowledge to study the original class of structures.

If you don't know what denotational properties you require from your denotational semantics of your language and have no use for it,
what is the point of to providing a denotational semantics?
It will not add any confidence that your extended language will behave as you want.

On the other hand,
if you know how the denotational semantics should be
based on your intuitive informal semantics and your intention in extending the language,
then you can use that to formally check that
your programming language matches your intuitive semantics and
will work as you intended
(w.r.t. the requirements you had for your denotational semantics).

> **Comments:**
> **username_3**: I disagree regarding the point of defining formal semantics, that you want to emphasize. I develop my dissenting view at the end of my answer.  - - - - - - - - - - - - Also, I guess everything can be seen as a mapping, but this is not usually the way various formal semantics are presented, though it is definitely the case for denotational semantics. Is your intent actually to cover all formal definitions of semantics by the statement in your second paragraph?  
> **username_2**: @username_3, I read your view. _Mathematically_ there is no difference between meaning and syntax, considering one to be meaning is our informal intuition not mathematical. There is no mathematical way to show an informal concept matches a formal one (through we can gather evidence e.g. by considering different formalizations and showing they are compatible.) What you describe is a special case of what I wrote:we believe the semantics matches our intuitive intended meaning, and use this knowledge to show that syntax can be assigned meaning.  
> **username_2**: Side notes: the view I expressed is partly based on Girard's writtings like [truth, modality, and intersubjectivity](http://iml.univ-mrs.fr/~girard/truth.pdf) and his "broccoli logic" joke. You can replace mapping with other kinds of relations between class of structures if you prefer, being a mapping is not essential for my points: there is no mathematical distinction between syntax and formal semantics, blindly defining a formal semantics for a language adds nothing. What I wrote does not imply the mathematical structure should be pre-existing.  
> **username_3**: Sorry, I did not manage to parse your sentence beginning with "Mathematically". So I cannot answer that usefully. Little point discussing it since I do not know Girard's view. I can actually agree with it if you consider relation, rather than map, because that is clearly one of the thing we do with semantics, in order to construct it (and revise beliefs). But, like the OP, I have used formal semantics for practical work. And it has another major role, which is accurate communication between people. It can be reduced to the same. But then your statement is far too abstract.  
> **username_2**: I don't see what cofuses you, in any case it was restated in the following comment. The statements are not "far too abstract" at all. Btw, if you prefer that I don't refer to your answer let me and I will remove it.  
> **username_3**: What confuses me is the syntactic role of "not mathematical" in that sentence. I think I have some idea of what is intended by your 3 lines statement. I still disagree on the way it was made, but I do not think discussing it further will lead anywhere. I think the level of scientific discourse should be adapted to its purpose, context and intended recipient. This is actually a frequent problem on SE.  
> **username_1**: @username_2: I too couldn't understand in what sense you say is syntax is "mathematical".  In any case, syntax is always countable whereas semantic structures are rarely countable.  So, that is quite a precise mathematical difference that you can't brush off.  
> **username_2**: @Uday, syntax can be uncountable (e.g. in model theory we deal with uncountable languages). My statement was not that syntax is mathematical, my statement is that referring to some mathematical structures as (formal) semantics is based on our _informal_ intuition, not a mathematical property of those structures. The moral take away is this: *don't blindly provide formal semantics just because others have provided formal semantics for their languages, having a formal semantics doesn't mean anything by itself, you have to know why you want a formal semantics.*  
> **username_2**: I think Girard's broccoli logic example is illustrative: 1. add a new binary logical operator called broccoli and denoted by $\clubsuit$ to classical propositional logic, 2. consider an extension of Boolean algebra called broccoli algebras with a new broccoli operator satisfying suitable rules, 3. it is straight forward to show soundness and completeness of broccoli logic w.r.t. to free broccoli algebra semantics. But what is the point of providing this semantics and proving soundness and completeness?  
> **username_1**: @username_2.  Ok you want to emphasize the "philosophical" aspect of what semantics is about.  That is perfectly fine.  However, note that broccoli semantics may not always be trivial.  For typed lambda calculus, for example, you can't show completeness for "broccoli algebras" but you can show it for "broccoli categories."  So, that says something fundamental about  the nature of typed lambda calculus!  
> **username_2**: @Uday, my point is more practical than philosophical. It seems to me that they didn't know why they wanted a denotational semantics, and that was the root of their confusion. Sure, I mentioned boroccoli logic to demonstrate the point that one should not _blindly_ go for providing semantics, I am not saying algebraic semantics are not useful.  
> **username_2**: Btw, I see Andrej and Neel made somewhat similr remarks regarding distinction between syntax and semantics: ["Of course, such a view requires one to differentiate between formal manipulation of syntax and "true" mathematics. This is necessarily a non-mathematical distinction."](http://cstheory.stackexchange.com/a/3588/) ["No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense."](http://cstheory.stackexchange.com/a/21543/)  

---

### Answer by username_3 on 2014-07-23. Score: 1

There are two aspects of correctness:

* one is internal consistency, so that whatever you define can be assigned a
  proper meaning. Typically, that is why you are told that the domains
  you use must be CPO, so that you can have limits used to defined the
  semantics of some looping/recursive construct, whether program or data.
* the other is consistency with you intended semantics. This is a
  general problem with specification of program, or languages or
  anything else. When you design something, the correctness of your
  design can only be checked with respect to some reference, and in
  this case formal reference. I develop this second point.

If a child ask you for a car with 4 wheels. You may buy him a small
automobile, and be in agreement with the specification. But what he
actually wanted was a new passenger car for his train, and the child
will be unhappy. The specification is incomplete (or incorrect) and as a consequence
the end result may not adequate.

So a specification may not exactly reflect your intent. You can prove
that your realisation of a car (or your compiler) is conformant with
specification, but you have no way to prove that your specification is
conformant with whatever intent is in your mind.

The denotational semantics of a language is a specification of the
language, and you have no way to prove that it conforms what is in
your mind, unless you can express that formally, which will just be
annother specification, of which you are not sure it conforms your
intent.

However, if you make your intent more precise in several different
ways, you can check that your various attempts at specifying what you
want are consistent, which will give you greater belief that what you
are doing conforms what you want. But there is no way to be certain.

For example, you can attempt to prove the consistency of your
denotational semantics with another formal specification or semantic
definition, as suggested in your question. These specifications do not
have to be complete specifications. It may only be a statement of some
property of your language.

**Consistency with previous version of the language**

Still, in your case, there is something that you may do, that you should do.

The language you are considering is an extension of another language,
that may have a formally defined semantics.

Then one thing that users will expect is that the extended language
will work like the original one when the new features are not used.

Hence, one thing you should prove is that any program of the original
language is given the same semantics in the new language.

It may be however that there has been some changes so that
programs have to be adapted for the new extended version of the language. Then
if you can formally defined how program P for the original language is
to be tranformed into another program P' in the extended language, then
you ideally should prove that this tranformation is semantics preserving.

If such a tranformation of programs to the new language version is necessary, and not clearly obvious, it may be worth defining semantics of the original language (if it does not exist yet) in order to prove the correctness of the transformation.

**Post-scriptum**

I have to disagree with [username_2's answer](https://cstheory.stackexchange.com/questions/25322#25325) main statement that

> The point of formal semantics is that we take the class of
> mathematical structures that we want to study and map it to another
> class of mathematical structures that we already know something
> about, and we use that knowledge to study the original class of
> structures.

The problem is that, in general, we have no mathematical structure to
begin with. At best we have a syntax, defining sentences in a
language. **The first point of formal semantics is to associate a
meaning with sentences (programs) following this syntax**, and do it
formally so that we can study this meaning and prove properties about
it. So the semantics is indeed taking syntactic sentences to a class
of mathematical structures theat we are supposed to understand. But
**We are not interested in studying the syntax**, which is the only
original structure that is being mapped. We may have an intuitive
meaning in mind, but it can hardly be the domain of a mathematical
map.

We are indeed interested in studying our intended meaning for programs
though the mapping of the syntax that expresses them into semantics.
But the mapping applies only to the syntax, not to the intended
meaning we hope to study ... if the semantics we define does conform
our intent.

What we may do, though, is take two mapping from the same syntactic
structure into different classes of mathematical stuctures, and prove
the existence of a mapping between these structures, with properties
that represent some form of consistency of the two definitions.


---

