how do you define functions with denotational semantics?

Denotational semantics are abstract functions that give meaning to statements of a programming language. They accept an expression and return a value. But how do you define denotational semantics for languages that define, for example, functions (and later use these functions), or global variables, and change some global state of the program? I think the simplest way to do it would be to define the semantics function so that it returns a pair of values and a "global state" instead of just a value. But is there a place I can read about it some more? I am sure someone have done something like that. For example, is there denotational semantics for languages like Java or C? It would be nice to find a book that focuses on denotational semantics for programming languages which are not necessarily purely functional (though I think functional languages, like LISP, can also change a global state).

asked Jun 16, 2013 at 15:10 31 2 2 bronze badges

$\begingroup$ Writing a denotational semantics for Lisp is a bit strange, as it is often implemented through a description in itself. I would not choose it as my first example. $\endgroup$

Commented Jun 16, 2013 at 16:17

$\begingroup$ @babou's answer below is very good. I'll just add that I'm aware of at least two textbooks that cover denotational semantics. Both cover semantics of languages with mutatable state. Carl Gunter; Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992. ISBN 978-0262071437. Franklyn Turbak, David Gifford; Design Concepts in Programming Languages, MIT Press, 2008. ISBN 978-0262201759. $\endgroup$

Commented Jun 17, 2013 at 2:12

2 Answers 2

$\begingroup$

People have been writing denotational semantics for all kinds of languages since the late seventies. The list must now be quite long, and include large real languages, but I never tried to check what is in it. The number of books is probably large too. What you want is to look at toy examples. Anything real is not a good idea for a start. Some are probably in (text)books.

There were some references to such examples in A simple programming language? You may try it . I did not check the answers.

In some cases people had to write a formal semantics because they wanted to prove correctness of the compiler. Still much research on this.

Denotational semantics are abstract functions that give meaning to statements of a programming language. They accept an expression and return a value.

Well, only in the sense that any well formed program fragment may be seen syntactically as an expression (a formula), and anything may be seen as a value in denotational semantics, including functions (values belong to domains . which you can understand approximately as types). Actually the semantics function takes a syntactic formula (you can read "formula" as "abstract syntax tree") and returns a function expressing what that formula is supposed to mean . or to do when run as (part of) a complete program.

How you write the semantics, and what domains you use is highly dependent on what kind of features exist in you language. For example, if you have exceptions, things may get a bit more complicated.

But just try toy examples to begin with. And then more.