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

Q1: There are many notions of program equivalence (trace equivalence, contextual equivalence, observational equivalence, bisimilarity) which may or may not take into account things such as time, resource usage, nondeterminism, termination. A lot of work has been done on finding usable notions of program equivalence. For example: Operationally-Based Theories ...


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


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


15

The other extreme is to say two programs are equivalent iff they compute the same function (or show the same observable behavior in similar environments). But these are not good: not all programs checking primality are the same. We can add a line of code with no effect on the result and we would still consider it the same program. This is not an extreme: ...


13

Comparing two programming languages is difficult is a difficult problem, and far from being solved. The key issue is that there are many different ways languages can be compared, and none of them is compelling. The most widely used approach, coming from logic, is to consider translations between the languages to be compared. The general idea is as ...


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


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


11

A semantics of a program is a model of its behavior which, like any scientific model, ignores aspects that you don't want to study. An extremely detailed model of the execution of a program would model the physical behavior of the computer that executes it, including the execution time, power consumption, electromagnetic radiation, etc. Such aspects are ...


11

Here is one possibility, but other people might use different words. I will use first-order logic as a running example. Language The language is a collection of expressions, which are syntactic entities, i.e., finite configurations without any a priori meaning. A language is described by the grammar, which determines which finite configurations are valid ...


11

No, to my knowledge there has been no work on formalizing TeX of the kind you are interested in. (What follows is a subjective and personal commentary). I think it is an intriguing and well-posed idea, and your motivation of using it to perform optimizations sounds reasonable -- another related question is whether you could define a bytecode format for it ...


10

You'll need to modernize the notation, but McCarthy and Painter's Correctness of a Compiler for Arithmetic Expressions is simple and good, and also of historical interest (since to the best of my knowledge it's the first paper on the subject).


10

I do not know of good tutorial material, but there are papers that are sufficiently elementary for a grad student (like me). The first might be what you are looking for (emphasis is mine). Simple relational correctness proofs for static analyses and program transformations, Nick Benton. 2004. We show how some classical static analyses for imperative ...


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


10

There is a naive algorithm for programs with bounded-size inputs: enumerate all programs in order of increasing length (or execution time, which is a bounded function of the length). If you can prove that the program is equivalent to the original, stop; otherwise keep searching. This algorithm is sound. In order for it to be complete, you need to be able to ...


10

The practical reason is that it is very convenient to include also the case "zero steps" in the definition of "many steps" (millennia of mathematical experience have taught us that it is usually a good thing to have a 0 around in our set of natural numbers). One possible technical exemplification of this (but there are probably dozens more, perhaps more ...


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


9

The answer is complicated, for two reasons. Different people in Computer Science interpret the term "object" differently. One is that an object consists of some data and operations packaged together. The other is that an object is all that but also has "state," i.e., it is some form of a changeable entity. There are deep philosophical issues to do with ...


9

(With apologies for a long answer that goes in a direction different from the scope of the site: frankly I was surprised to see the question here in the first place….) TeX was designed for typesetting, not for programming; so it is at best “weird” when considered as a programming language. — Donald Knuth, Digital Typography, page 235 I have read a ...


8

A reduction strategy is a function on Lambda that picks one redex (reducible expression) from all possible redexes -- depending on what you define as a redex. Informally, an evaluation strategy is the order in which a language evaluates its arguments. A parameter-passing strategy is what the language hands to the function. To understand the connection ...


8

Obviously there is an operational semantics of Ltac by Jedynak et al.


8

I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's The Use of Machines to Assist in Rigorous Proof.


7

Perhaps not the simplest example, but Xavier Leroy has done a lot of work in this area, such as a formally verified C compiler. He gave a summer school presentation using a small imperative language IMP, which is an accessible introduction to the more advanced work.


7

Graham Hutton has a small example in his book "Programming in Haskell" which is a great place to start. I also have a few mechanised proofs (various logics) of the McCarthy-Painter compiler in a report I did for my PhD.


7

Adam Chlipala's A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language seems to be a good example of a simple compiler correctness proof using denotational methods, with the added advantage of having been formalized completely in a proof assistant.


7

Landin's SECD machine, originally described in The mechanical evaluation of expressions in 1964, is a transition system in the form of an abstract machine, later inspiring lots of of other abstract machines such as the CESK machine.


7

I essentially agree with Martin's comment, I can elaborate on that to make a tentative answer, knowing that there is no general formal definition of calculus or abstract machine and that what I am going to describe cannot possibly cover the meaning of all instances of these two words found in the literature. In brief: a calculus usually gives you the ...


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


7

Non-termination can be considered an algebraic effect up to a point. It's an exception that cannot be handled. More precisely, we may introduce a nullary operation (constant) $\bot$ which signifies non-termination, but then we disallow handling it, as that would allow us to implement the Halting oracle. Such treatment of non-termination is a bit naive. A ...


6

I don't know how you can define the informal semantics as accurately as possibly, but there does exist machinery for defining semantics that is purely, well, semantic. Your semantics could be based on mathematical functions, relations, or domains. Indeed, the style of semantics known as Denotational Semantics builds upon these (and other) semantic notions ...


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