2
$\begingroup$

Some papers define an operational semantics of a programming language. That is nice, but what makes such a semantics fit for the purpose?

An idea is to have a progress theorem, i.e. well-formed expression is either a value or a reduction can take place

another is type preservation, that an reduction preserves the type of an expression.

What else is a test for the adequateness of a semantics? What should I prove about it?

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ Progress and type preservation only make sense for typed languages. $\endgroup$
    – Dave Clarke
    May 31 '16 at 12:32
  • $\begingroup$ I am interested in typed languages $\endgroup$
    – Gergely
    Jun 1 '16 at 12:45
  • 1
    $\begingroup$ Not to answer the question, but the operational semantics can be made executable and run against a test suite for the language – the paper "An Executable Formal Semantics of PHP" by Daniele Filaretti and Sergio Maffeis (ECOOP 2014) tests their extensive semantics of PHP against Zend PHP's test suite. $\endgroup$
    – Dave Clarke
    Jun 2 '16 at 7:38
4
$\begingroup$

I think you have it a bit backwards: proving type preservation is a good property of the type system with respect to the operational semantics, rather than the opposite.

Alternately: the whole point of a programing language is the ability to use it to perform some computational task. Because of this, the operational semantics is one of the requirements of having a programing language. The only real "fitness test" you need is

Can I write the programs I want using this language?

You might then want to prove that say, a compiler is correctly implemented by showing that the computational behavior of (well-behaved) code is equivalent in some sense to the operational semantics, but again, here I would take the semantics themselves to be primal rather than the opposite.

In certain fields of mathematics, notably in the area which studies the propositions-as-types correspondence, one might be more interested in the static semantics (the type system) and have the operational semantics more as an afterthought, where progress, preservation and termination have consequences on the type system as a logic (typically, that the logic is consistent).

But again, usually the operational semantics is primitive, and it is well-defined exactly when it enables the programmer to write the program she wishes to write (and possibly prevents some "bad" programs).

Improve this answer
$\endgroup$
10
  • $\begingroup$ I understand all the above, but is there any mathematical test on it? My idea is to formalise such a semantics in a theorem prover and then prove ... what? $\endgroup$
    – Gergely
    Jun 1 '16 at 12:35
  • $\begingroup$ What is your goal in performing such a formalization? An operational semantics is like a definition in Mathematics: not all that useful unless you have a motivation for it. If you're looking for suggestions, then I'd have to say that stackexchange is not really the right forum for this, though I'd suggest looking at some examples of such developments, e.g. this nice one here: cis.upenn.edu/~bcpierce/sf/current/Smallstep.html $\endgroup$
    – cody
    Jun 1 '16 at 14:04
  • $\begingroup$ I think this answer misses the point of what an operational semantics is for. It has nothing to do with how program-in-able a language is. $\endgroup$
    – Dave Clarke
    Jun 2 '16 at 5:09
  • $\begingroup$ My point is that an operational semantics is (the crucial part of) the definition of a programing language, and so is only useful insomuch as the programing language itself is useful. $\endgroup$
    – cody
    Jun 2 '16 at 11:51
  • $\begingroup$ The programming language may not be useful for programming, it may be for studying a particular aspect of concurrency or memory management or for demonstrating that a particular type system is sound. Also, most programming languages are not given an operational semantics (in the formal sense). Most operational semantics are defined independently of the language implementation. So in short, I completely disagree. $\endgroup$
    – Dave Clarke
    Jun 3 '16 at 5:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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