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


14

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense. Structural operational semantics is not denotational, because it is not a compositional method of giving semantics to a programming language. However, you can build denotational models out of a structural operational semantics by using a ...


12

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


9

Amal Ahmed's very readable thesis dissertation could be a nice start.


8

I don't know what you mean by "practical", but confluence is very useful from the semantic point of view. Hopefully other people will be able to give you other answers from other points of view (for instance from the standpoint of abstract term rewriting, which is not my specialty). For instance, in $\lambda$-calculi and related languages, usually the ...


5

It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For instance, the computations do _ <- putStr "foo" return 42 and do _ <- putStr "bar" return 42 both "have" value 42 but are different, since one ...


5

The notion of "next" and "last" - prior to the idea of "expansion" and "reduction" - are essentially lost when we read a big-step operational semantics as an inductive definition, which is too bad because the way we usually prove things about big-step operational semantics is by reading it as an inductive definition! You can prove a "full expansion" ...


4

A compositional denotational semantics $[\![ {-} ]\!]$ of a programming language (a domain-theoretic or game-theoretic one, for instance) is adequate if semantically equal terms imply that they are observationally equivalent: $$[\![ t_1 ]\!] = [\![ t_2 ]\!] \implies t_1 \cong t_2.$$ It often happens that it is far easier to calculate denotations that to ...


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


3

We have been working on one for the last few years: Lem, a higher-order, typed language with backends for OCaml, Coq, Isabelle/HOL, HOL4, LaTeX and HTML. Lem has been used internally in the group to formalise various machine models (PowerPC, ARM, and so on), memory models (the C memory model, etc.), programming language semantics (OCaml Light), and so on.


2

This new version of the answer tries to take into account the changes in the question, and the information exchanged in the comments. This answer assumes that $S$ should be the set of variables that have a content that is used in some defined fragment of the program, rather than, at some point in the program, the variables with a content that will be ...


2

There is no standard notion of "fundamentalness". It's not clear that what you are looking for is meaningful or makes any sense. What is "fundamental" is a matter of perspective; I don't see any reason to privilege insert as more fundamental than splice, or vice versa. So, if you need a concept of "fundamental" for some reason, you'll need to define for ...


2

The domain and model theories of PTSes hasn't been explored all that much I'm afraid. One detailed source is Thomas Streicher's PhD work: Semantics of Type Theory. He gives category theoretic semantics for all PTS, though I'm not sure he addresses $\eta$-conversion.


1

I still don't quite understand what having a value means, but just considering the question of "can we give up the eta rule for monads", the answer is yes, this is an entirely reasonable thing to consider. As a rule of thumb, having the eta rule in the syntax corresponds to the uniqueness condition on a universal property. So if you want to add natural ...


1

I have not been following closely this area for many years, but I know systems have existed for a very long time to capture semantics or help translation. The first system for creating interpreters based on denotational semantics was SIS created by Peter Mosses around 1980. Around the same time, programmable structured editors and some multilanguage ...


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