imperative state– oriented numerical computation symbolic data x:=E random access purely functional languages explicitly f(x) = x∗x+1 recursively f(x) = x=01x∗f(x−1) recursive data types tree = empty() | mktree(tree, tree) empty 0 mktree t_{1} t_{2} t_{1} t_{2} flow chart dynamic behaviour complex dynamic behaviours control flow define program f(e_{1}, …, e_{n}) evaluated

1

what how forms of definition

operational semantics inductively evaluation relation

EV

But usually implementations of functional languages also provide the facility of compiling your programs.

E evaluate V EV E V \underline{n} n numeral V_{1} = V_{2} EV_{1} EV_{2} determinstic E V E^{2} V EV E general recursion all

observational equality

E_{1} E_{2}

C[ ]

C[E_{1}]\underline{n} ⟺ C[E_{2}]\underline{n}

n ∈ E_{1} E_{2} E_{1} E_{2} observation E C[E]\underline{n}

C[ ] n test- ing

of programs

Denotational Semantics E σ E ∈ D_{σ} denotation meaning semantics E D_{σ} σ

3

Domain Theory

D_{σ} σ D_{=}∪

{⊥}

⊥ D ⊑ ⊥ D_{στ} D_{σ} D_{τ} D_{στ} ⊆

D_{τ}^{D_{σ}} = {f | f : D_{σ}D_{τ} }

D D D

∪{⊥} ⊑ but sets endowed with some additional structure D_{στ} structure preserving

D_{σ} D_{τ} στ σ D_{στ} ⊑ con- ti- nu-

For sake of completeness we will also present a “Small Step Semantics” for

as well as an abstract machine serving as an interpreter for . In particular, as we shall see they will not satisfy Hausdorff’s separation property reity^{4}

D_{στ} f ⊑ g

f(x) ⊑

g(x) x ∈ D_{σ}

extensional στ functions D_{σ} D_{τ} what how

P Q σ semantically denotationally equal

P = Q ∈

D_{σ} correct P V P V programs

P P = n P \underline{n}

n P \underline{n} P \underline{n} P = n complete

computationally ade-

quiring that for distinct points x and y there are disjoint open sets U and V containing x and y, respectively. which is in accordance with the usual topological notion of continuity when the domains D_{σ} and D_{τ} are endowed quate^{5}

P \underline{n} ⟺ P =n

P n

P Q

C[P] = C[Q] C[−]

compositional P = Q C[P] = C[Q] C[−]

P = Q

P Q

P = n = (\underline{n}) / (P \underline{n})

P \underline{n} ⇔ \underline{n}\underline{n} P \underline{n} \underline{n}\underline{n}

fully abstract a priori

P Q

C[P] C[Q] C[−]

… ()

parallel : 0 0 1 1 ⊥ relativity

E_{1} E_{2}

() C[−]

E_{1} E_{2}

[−]()

or

with the so– called Scott topology which is defined in terms of the information ordering One also might say that the operational semantics is computationally adequate w.r.t. the denotational semantics because the denotational semantics may be considered as conceptually prior to the operational semantics. One could enter an endless philosophical discussion on what comes first, the operational or the denotational semantics. The author of this course has a slight preference for the view that denotational semantics should be conceptually prior to operational semantics (the What comes before the How) being, however, aware of the fact that in practice opersequential domains the

game semantics not extensional

strongly stable domains

σ C_{σ} ⊆ D_{σ} computable A_{σ} C_{σ} all computable elements of the model do arise as denotations of closed terms universal^{7}

continuous existential quantifier

∃ : ()

∃(f) =

0 f(n) =

0 n ∈ ∃(f) =

1 f(⊥) =

1 ∃(f) =

⊥

∃ +

(D_{σ})_{σ∈}

ational semantics often comes before the denotational semantics. as for example in cryptology where the attacker is usually assumed to employ as strong weapons as possible Calling this property “universal” is in accordance with the common terminology where a programming language L is called “Turing universal” if all partial recursive functions on

can be implemented by programs of L. The property “universal”as defined above is stronger as it requires that computable elements of all types can be implemented within the language under consideration. But in both cases “universal” means that one has already got an implementation for all possible computable elements (of a