18

"Meaning" is used in a broader way than denotation is. The original dichotomy, inherited from logic and philosophy, is between "sense" and "denotation" (which philosophers call "reference"). This distinction can be illustrated by Frege's original example. He noted that phrases "the morning star" and "the evening star" referred to the same object --- the ...


18

How do type classes fit in this model? The short answer is: they don't. Whenever you introduce coercions, type classes, or other mechanisms for ad-hoc polymorphism into a language, the main design issue you face is coherence. Basically, you need to ensure that typeclass resolution is deterministic, so that a well-typed program has a single ...


16

I am happy with Adrej's answer, but I would like to drill down further. To start with, denotational semantics wants to say something like "the meaning of this notation is that". A real semanticist would want to imagine that the meanings are what exist in our mind and the notations are just a way of expressing those meanings. The requirement that ...


16

I would divide the books on programming language semantics into two classes: those that focus on modelling programming language concepts and those that focus on the foundational aspects of semantics. There is no reason a book can't do both. But, usually, there is only so much you can put into a book, and the authors also have their own predispositions ...


12

Unfortunately, there are too many things are going on here. So, it is easy to mix things up. The use of "full" in "full completeness" and "full abstraction" refer to completely different ideas of fullness. But, there is also some vague connection between them. So, this is going to be a complicated answer. Full completeness: "Sound and complete" is a ...


12

[One more answer. It is probably uncool to pile up several answers. But, hey, this is a deep issue.] I said that I agreed with Andrej's answer, but it seems that I don't agree entirely. There is a difference. I said that a denotational semantics has to say "the meaning of this notation is that". What I meant is that notations must be assigned meanings, ...


11

In this answer, I'll take "expressible" to mean "macro-expressible" in the sense of Felleisen 1991, On The Expressive Power of Programming Languages. (Intuitively, a language feature is macro-expressible if you can define it as a local source transformation, without using a whole-program transformation.) With this definition, the answer is no: delimited ...


10

The following is an extended comment, it does not answer your question in the terms you posed it but does give a semantics for higher-order probabilistic calculi which you may find of interest. In the past few years there has been a very active line of research around so-called quantitative denotational semantics of linear logic, based on the idea (...


10

[Hopefully, this is my last answer to this question!] Ohad's original question was about how denotational semantics differs from structural operational semantics. He thought that both of them were compositional. Actually, that is untrue. Structural operational semantics is given as sequences of steps. Each step is expressed compositionally (and it is ...


9

This additional response is to amplify the point that denotational semantic models are designed to "explain" computational phenomena. I will give a series of examples from the semantics of imperative programming languages (also called "Algol-like" languages). First there was the semantic model formulated by Scott and Strachey. (Cf. Gordon: Denotational ...


8

Makoto Takeyama and I sent the following to data-refinement@etl.go.jp on Jan 5, 1996: Subject: what is a data refinement relation? Dear all: anyone still interested in data refinement? Recently Mak and I have been looking again at an idea we considered many months ago. The motivation is to characterize the logical relations relevant to ...


7

(Gosh, Neel, that was a tough question.) The "folk model" of linear logic is definitely the coherent spaces model, discussed in Girard's Linear Logic paper (and also in "Proofs and Types"). This is not degenerate in the sense you describe. Whether this semantics throws any light on how a linear functional language can be implemented, I am not sure. When ...


7

Most people avoid giving precise descriptions of what a syntactic category is, because if you do it properly with all the details, the ratio of insight to necessary mathematical sophistication ends up being very, very low. John Reynolds' book Theories of Programming Languages has one of the more comprehensive explanations in its chapter 1, as does Robert ...


6

I don't know about the field of semantics, but the concept you mention is crucial in the complexity of counting. I have not seen a relation $R$ called a difunctional relation before, but it is equivalent to $R$ having some Mal'tsev operation as a polymorphism, a concept from universal algebra. An operation $m$ is a Mal'tsev operation if $m(x,y,y) = m(y,y,x) ...


6

The second paragraph of Plotkin's 1973 Memo on Lambda-definability and Logical Relations says this: "The definition of logical [relation] is derived from a corresponding one of M. Gordon for the typed λ-calculus." This doesn't say explicitly that the term was coined by Gordon. But, given that the memo is titled "Lambda-definability and logical ...


6

The only natural condition I can think of is Berry's "I condition" ([1], Sect. 12.3): (I) each compact element dominates finitely many elements. The above condition is the defining property of Berry's dI-domains, which are distributive (that's what the "d" stands for) algebraic domains satisfying condition I. This is a widely known and well studied class ...


5

Summary: full completeness means that the interpretation function is not just complete, but also surjective on programs. Full abstraction has no requirement for surjectivity. $\newcommand{\semb}[1]{[\![ #1 ]\!]}$ Details: The detailed meaning of full abstraction and full completeness depends on the nature of what/where/how you are interpreting. Here is a ...


4

The textbook that might be most relevant to your question is Principles of Program Analysis by Nielson, Nielson and Hankin. It does cover dataflow analysis and its relationship to denotational semantics. It does not deal with axiomatic semantics though.


4

With only flat domains, you cannot define limits to construct "infinite" structures, such as looping structures, for data or for programs. Fixpoint constructions in denotational semantics (since you used that tag) use non flat domains. Maybe you should give examples of domains that are taken as flat, while it would be better to do differently. Many problems ...


4

The comment below is correct, but it's important to understand the meaning of "finite" or "compact" elements of a domain. These are the denotations of objects computable in finite time, so their appearance in a semantic model is not for proof-theoretic convenience - they represent the strong connection between the model and actual computation.


4

[My apologies for writing this as an answer, despite the fact that it is basically just a comment to the previous answer. But I am not allowed to post a comment up there, since I do not have enough "reputation"] The previous answer is not correct. Linear logic (as well as any of its substructural systems: MLL, MALL, MELL, ALL, whatever you want...) is ...


4

Non-monotonic logic is kind of a wide area -- do you have any particular logics in mind? Anyway, defeasibly assuming :) that you are interested in any logic in which the principle of monotony fails, and you want a categorical semantics in the sense of categorical proof theory (rather than, say, a hyperdoctrine semantics), then one answer is that you can ...


4

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]] : ...


4

I would like to add two books not found on the answers given up to now: Aaron Stump, Programming Language Foundations David Schmidt, Denotational Semantics: A Methodology for Language Development Stump's book is concise but very clear.


4

I never found an explicit definition either, but I have inferred the folowing. As I understand, you split the language into syntactic domains; with the addition that syntactic domains must be fully generated by single different symbols, when you write down the grammar. So a syntactic domain is a subset of your language, and each domain is generated by one ...


3

For a complete beginner studying operational semantics, I would suggest Programming Languages and Operational Semantics by Maribel Fernández. Everything is explained in a very simple manner which is easy to understand. http://www.springer.com/computer/swe/book/978-1-4471-6367-1


3

For what concerns the use of non-flat domains, babou already gave examples. I can add that sometimes it may even be useful to see integers as streams: there's ⊥, above which there are 0 and S⊥, above the latter there are S0 and SS⊥, and so on. I know that in the early 90s Loïc Colson worked on models using the above interpretation of integers, although I ...


3

(This is an extended comment). I may be misreading your definitions, but it seems to me that the relation you introduce, let us call it $\simeq$, is not an equivalence relation because it is not transitive. If $V_1,V_2$ are two distinct closed normal forms (values), then obviously $V_1\not\simeq V_2$. On the other hand, the genericity lemma (Proposition ...


2

Restating the definition to make the quantifiers easier to understand: A molecule is a finite stable approximable mapping, such that there exists a largest pair $(a,p) \in m$, such that for all other pairs $(b,q) \in m$ we have $b \subseteq a$ and $\{p\} \vdash q$. In other words, a molecule is a mapping that closes off neatly, having a largest pair.


2

Well, Mislove's quote already contains a positive answer: the category of dcpos is carteisan closed and also closed under the probabilistic powerdomain. It can indeed be used to give a denotational semantics to higher-order probabilistic computation. However, dcpos fail to satisfy the "usual approximation assumptions" that every element can be approximated ...


Only top voted, non community-wiki answers of a minimum length are eligible