3
$\begingroup$

We have a programming language and its denotational semantic, like Tony Hoare's CSP 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?

Improve this question
$\endgroup$
7
  • $\begingroup$ 1 Thank @Kaveh for your answers. Moreover thanks Kaveh for editing my poor English in my question statement. $\endgroup$
    – zhuang
    Commented Jul 27, 2014 at 2:23
  • $\begingroup$ 2 Thank @babou for your answers. $\endgroup$
    – zhuang
    Commented Jul 27, 2014 at 2:24
  • $\begingroup$ 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. $\endgroup$
    – zhuang
    Commented Jul 27, 2014 at 2:29
  • $\begingroup$ 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. $\endgroup$
    – zhuang
    Commented Jul 27, 2014 at 2:33
  • $\begingroup$ 5 The difference of denotational semantic and operational semantic may help us resolve the disagreement between Kaveh and babou. $\endgroup$
    – zhuang
    Commented Jul 27, 2014 at 2:37

2 Answers 2

Reset to default
4
$\begingroup$

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.

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).

Improve this answer
$\endgroup$
12
  • $\begingroup$ 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? $\endgroup$
    – babou
    Commented Jul 24, 2014 at 22:33
  • $\begingroup$ @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. $\endgroup$
    – Kaveh
    Commented Jul 24, 2014 at 22:48
  • $\begingroup$ Side notes: the view I expressed is partly based on Girard's writtings like truth, modality, and intersubjectivity 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. $\endgroup$
    – Kaveh
    Commented Jul 24, 2014 at 23:18
  • $\begingroup$ 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. $\endgroup$
    – babou
    Commented Jul 24, 2014 at 23:54
  • 1
    $\begingroup$ @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. $\endgroup$
    – Uday Reddy
    Commented Jul 30, 2014 at 20:50
1
$\begingroup$

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 Kaveh's answer 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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.