19

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, resulting in $\vdash e:T$. This means that no assumptions on variables are made. Usually, this means that $e$ is a closed term (without any free variables) having ...


11

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 \rbrack\!\rbrack} \SEMB{\cdot}$ is the semantic function, mapping programs to their meaning, something like the following must be the case for all $n$-ary program ...


10

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 There were some earlier attempts before this, but they didn't quite nail the problem, for example: how do you denote the value of a functional program? What ...


9

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 takes possibly infinite amount of input written down on an input tape. It writes the result on an output tape, where the output cells are write-once. There are workign ...


7

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 correspondence between the two (called the Curry-Howard's correspondance). The first implication is the arrow that appears in formulas, and it corresponds to logical ...


7

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 sqrt with the postcondition that sqrt(x) = y and y*y = x, what are some valid preconditions? x > 10 x > 20 x > 1 Some invalid preconditions would be x < 0 x > -10 One predicate P1 is ...


6

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 formal, mathematically rigorous description of the program behavior. That inherently involves math and several formulae -- one can't really do without math. ...


6

Can you come up with two different algebras, say, one where the domain is $\mathbb{N}$ and one where the domain is $\{0,1\}$ and in the former, suc and pred work as you would assume, and in the latter, they are modulo 2 operations? Then, try to come up with a homomorphism from one to another. Then, try to make an algebra, where the domain is $\{0, s0, ss0, ...


6

Your proposed alternate definition is no good. It tries to define $[[\text{while b do S}]]$ in terms of $[[\text{while b do S}]]$. That's a circular definition: you can't define something in terms of itself. "FIX" typically refers to the least fixpoint, and is a way of avoiding circularity. See your textbook for background on fixpoints and the precise ...


5

Since the question does not fully describe the language, I assume the simpler case when the $\texttt{++}$ operator applies only to variables given by an identifier, for example: $\texttt{foo++}$. Short of having more examples of the way you write denotational semantic, I have to improvise a bit. In particular, I avoid lambda notation since I do not know ...


4

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 define both semantics properly, you'll most likely have $O(p,\sigma)=D(p)(\sigma)$. I'll write $S(p)$ to mean either $\sigma\mapsto O(p,\sigma)$ or $D(p)$. Now ...


4

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 sure that at most one such $i$ exists. It would be better to write (and by the way, you might appreciate LaTeX's cases environment): $$ \mathcal F^{k}(\bot)(\...


3

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


3

Presumably you mean $\lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack$, which you can easily define using $\text{while}$ as follows. $$ \mathcal{S}_{\text{ds}} \lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack = \mathcal{S}_{\text{ds}} \lbrack\lbrack S ; \text{while } \lnot b \text{ do } S\rbrack\rbrack $$ Note that typically, a $\...


3

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 doesn't terminate and the denotation is $\bot$. However, it's written down wrongly. What it says is (and please pardon me for throwing away all the notation ...


3

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 programs just try to compute a result depending on what they find in their starting state. If program $P$'s attempted computation fails when starting from some initial ...


3

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 expression $t_2$ is typed at type $T_2$ wrt. to a type environment having a type assumption mapping $T_1$ to some type variable $x$ In this context, a type ...


2

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 some days to check my proof before I accept my own answer. Lemma: If a function $f \colon M \to N$ between two cpos is monotonic, the inequality $$\bigsqcup\{f(...


2

The Scheme specification (revision 4) has an extensive denotational semantics, specified in the appendix of Revised$^4$ Report on the Algorithmic Language Scheme. This is probably not the best starting point to learn denotational semantics. FYI, the most recent version, R6RS, has changed to use operational semantics.


2

The function $f$ computes the recurrence relation $$ f(x) = \begin{cases} 4 & x \leq 1, \\ f(x-1)^2 f(x-2)^4 & x > 1. \end{cases} $$ Taking $\ell = \log_2 \circ f$, we get $$ \ell(x) = \begin{cases} 2 & x \leq 1, \\ 2\ell(x-1) + 4\ell(x-2) & x > 1. \end{cases} $$ Now, modulo 10 we have $$ 2 \cdot 2 + 4 \cdot 2 = 12 \equiv 2 \pmod{10}. $$...


1

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 you explicitly trace the denotation function by tagging them appropriately. $⟦x + y⟧_{AExp}\sigma = ⟦x⟧_{AExp}\sigma + ⟦y⟧_{AExp}\sigma$. Similarly, if you ...


1

Hint: Here is one example $A($ a1 - a2$, s) = minus(A($ a1$,s),A($ a2$,s))$ or alternatively $A($ a1 - a2$) = \lambda s . minus(A($ a1$,s),A($ a2$,s))$ where $minus$ is the substraction in $\mathbb Z\cup\{\bot\}$


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