Skip to main content
19 votes
Accepted

What does the leading turnstile operator mean?

On the left of the turnstile, you can find the local context, a finite list of assumptions on the types of the variables at hand. $$ x_1:T_1, \ldots, x_n:T_n \vdash e:T $$ Above, $n$ can be zero, ...
chi's user avatar
  • 14.6k
15 votes
Accepted

Why are computable functions continuous?

There are several ways to explain "computable implies continuous", I shall give here two such explanations. Turing machines compute continuous maps Suppose we have a Turing machine which ...
Andrej Bauer's user avatar
  • 30.9k
13 votes
Accepted

What questions can denotational semantics answer that operational semantics can't?

There is no real agreement what characterises denotational semantics (see also this article), except that it must be compositional. That means that if $\newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \...
Martin Berger's user avatar
10 votes
Accepted

What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?

I don't know why people didn't develop Hoare logics for lambda-calculi earlier. The first work to get this right was Honda et al's A Compositional Program Logic for Polymorphic Higher-Order Functions ...
Martin Berger's user avatar
9 votes

What is a predicate transformer?

The predicate transformer is just a formalization of the idea that you can produce a precondition given a program and its postcondition. For example, given a program ...
chepner's user avatar
  • 229
7 votes

What does the leading turnstile operator mean?

As a complement to the other answers, note that there are three levels of "implication" in typing derivations. And the same remark holds with logical derivations since there is actually a ...
Rodolphe Lepigre's user avatar
6 votes
Accepted

What's the difference between: operational, denotational and axiomatic semantics?

I think your examples show you do somehow understand the basic points of the several styles of semantics. Still, note that the whole point of having a semantics of a programming language is to have a ...
chi's user avatar
  • 14.6k
6 votes

What questions can denotational semantics answer that operational semantics can't?

I'll write $O(p,\sigma)$ for the only $\sigma'$ so that $\langle p, \sigma \rangle \to \sigma'$ (and $\bot$ if it doesn't exist) and $D(p)$ for the denotational semantics of $p$. Note that if you ...
xavierm02's user avatar
  • 1,255
4 votes

What does the leading turnstile operator mean?

In type checking systems, the ($\vdash$) represents the ternary relation over type environments, expressions and types: $\vdash \texttt Env \times \texttt Exp \times \texttt Typ$. In your example, the ...
mchar's user avatar
  • 141
4 votes

Why does the denotational semantics for a while loop have a existence quantifier?

The existential quantifier is misplaced. This is due to lack of reasonable notation for what needs to be expressed, namely: "if there is $i$ safisfying condition $C$, then use that $i$", where we make ...
Andrej Bauer's user avatar
  • 30.9k
3 votes

Why does the denotational semantics for a while loop have a existence quantifier?

The intuition is that the loop terminates at the $i$th iteration if the loop condition is false at that iteration but true at all earlier ones. If the loop condition is never false, then the loop ...
David Richerby's user avatar
3 votes

How is it that programs can be identified with partial functions for programming language semantics?

Partial functions from initial program states to final program states are a suitable model for deterministic sequential programs that do not interact with the environment while executing. Such ...
Kai's user avatar
  • 917
3 votes
Accepted

Why does the CwF definition require a set of types under a context rather than a class of types?

There is nothing special about types with respect to sizing, compared to what we already have in ordinary categories. A small category has a set of objects, and for each pair of objects, a set of ...
András Kovács's user avatar
2 votes
Accepted

Domain theory: Definition of isomorphisms

I think I have found an answer to my question, by proofing that the monotonicity of $f$ and $f^{-1}$ imply the continuity of $f$ and $f^{-1}$. Please correct me if I made a mistake – I will give you ...
user3389669's user avatar
2 votes

What is the definition of a redex and what are they for in programming languages literature?

A redex is an expressions on which we can perform a computation step, such as: fst (a, b) is a redex, it computes to a ...
Andrej Bauer's user avatar
  • 30.9k
2 votes

What is the semantics of a Turing machine?

The usual definitions of Turing machines are given in terms of formal semantics. For instance, the Wikipedia definition describes Turing machines in precise mathematical formalism. If you are looking ...
Andrej Bauer's user avatar
  • 30.9k
1 vote

What is the denotation for identifiers?

But I can't figure out what the type should be for the denotation for identifiers. That is because you are implicitly tracing the denotation function $⟦\_⟧$. It might get easier to see the type if ...
Apoorv's user avatar
  • 659

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