? σ do- main D_{σ} x_{1} : σ_{1}, …, x_{n} :

σ_{n} ⊢ M : σ x_{1} : σ_{1}, …, x_{n} : σ_{n} ⊢ M : σ : D_{σ_{1}}×…×D_{σ_{n}}D_{σ}

M n=0 ⊢ M : σ : 1D_{σ} 1 ⟨⟩

not D_{στ} all D_{σ} D_{τ} σ f ∈

D_{σσ} f

D_{σ} D_{σ} f

σ(f) ∈ D_{σ} σ(f) = f(_{σ}(f)) f

D_{σ} D_{σ} D_{στ} D_{σ} D_{τ} σ σ σ σ M_{σ}N N M

N ∪{⊥}

⊥ nontermination divergence σ Ω_{σ} ≡_{σ} (λx:σ.x)

Ω_{σ}_{σ}M M ∈_{σ} D_{σ} ⊥_{D_{σ}} 1

P στ f ∈

D_{στ} M_{στ} N

M(P)N(P)

P σ D_{στ} f ⊑ g

∀d∈D_{σ}. f(d) ⊑ g(d)

≤ f :: n ↦ n+1 D f :

DD μ(f)

⊥ ⊑ f(⊥) ⊑ f^{2}(⊥) ⊑ … ⊑ f^{n}(⊥) ⊑ …

μ(f) f f f(⨆_{n} f^{n}(⊥)) = ⨆_{n} f(f^{n}(⊥)) = ⨆_{n} f^{n}(⊥) μ(f)

least f

d = f(d)

f^{n}(⊥) ⊑

d n ∈ μ(f) ⊑

which still has to be proved but may well serve the purpose of motivation!