3
$\begingroup$

Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I understand correctly, the right way to do it is to develop a semantics for it, and then prove certain desirable properties such as soundness and consistency.

I've seen different approaches to this. Usually, a model in set theory is involved. But I believe that is not the only way to do it. Wouldn't, for example, an interpreter for that language on the untyped λ-calculus count as a semantics? So, my question is: what are the different ways to provide a semantics to language?

$\endgroup$
3
  • $\begingroup$ A reference request like yours is too broad for Stack Exchange -- you ask for a survey of a whole research area! You need to narrow your focus considerably before a question of reasonable scope appears. Try talking to your advisor(s), search with Google Scholar and check out this guide to better (re)searches on Academia. $\endgroup$
    – Raphael
    Jan 24, 2019 at 17:20
  • 2
    $\begingroup$ @Raphael I don't see how this question calls for a survey. chi's answer seems pretty satisfactory to me. If I had an objection to this question, it would be that it's pretty much calling for the Wikipedia article, but I don't think that particular article presents the information very well. $\endgroup$ Jan 24, 2019 at 23:01
  • $\begingroup$ @Gilles A short survey is still a survey, and better replaced by a textbook. But if you think otherwise, fair enough. $\endgroup$
    – Raphael
    Jan 25, 2019 at 14:16

1 Answer 1

5
$\begingroup$

There are many possible approaches. Here's a few "classic" styles.

  • Operational semantics (e.g. small step / reduction, or big step)
  • Denotational semantics (e.g. domain-theoretic, or category-theoretic)
  • Axiomatic semantics (e.g. hoare logic)

You can also define the semantics of a language through a translation to another language (already having its semantics). CPS transforms could also be mentioned here.

Also note that many languages admit several distinct semantics. Lazy & eager semantics of functional programs are possible, for instance. Prolog also has many different semantics (I recall someone stating "there's no such a thing as THE semantics of Prolog").

Further, concurrent languages like CCS or $\pi$-calculus have a LTS semantics. Game semantics is also used sometimes (but I don't know much about it).

I'm pretty sure there are many other kinds of semantics. I'd be surprised if in the future someone does not invent a new kind of semantics.

$\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.