# Tag Info

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

12

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

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}{\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 ...

8

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

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

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

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

5

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 The intuition is that the loop terminates at the ith 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 ... 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 \... 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 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}.$$...

2

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 morphisms between them; so morphisms are an indexed family of sets. We can immediately extend this definition to small CwFs, where for each context we have a set of ...

2

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 for something even more formal, have a look at this Coq formalization of Turing machines.

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