# Rappels

• $CPO$ category:

• completely partially ordered sets
• Scott-
• $⟦i⟧ =$

digraph {
rankdir=BT;
⊥ -> 0, 1, 2, ⋯;
}

• $⟦A ⇒ B⟧ = \lbrace f: ⟦A⟧ ⟶ ⟦B⟧ \mid f \text{ Scott-continuous} \rbrace$

• $⟦x_1:A_1, ⋯, x_n:A_n ⊢ M:B⟧: ⟦A_1⟧ × ⋯ × ⟦A_n⟧ ⟶ ⟦B⟧$

• $⟦Y \; M⟧ \; \vec{g} = \underbrace{\bigvee_n (⟦M⟧ \, \vec{g})^n (⊥)}_{\text{what we can’t do in } Set}$

Question: what does $⟦M⟧ = ⟦N⟧$ mean? (eg: when it comes to Friedman, this is tantamount to $βη$-equivalence)

Prop (Soundness of denotational semantics): If $M ⟶ N$ then $⟦M⟧ = ⟦N⟧$

Proof: Use the properties of CCC for $β$-reduction

Interesting case:

⟦Γ ⊢ Y \; M⟧ \overset{?}{=} ⟦Γ ⊢ M \, (Y \; M)⟧

To show that the functions are equal, show that they take the same values, i.e. for any $\vec{g}$:

\underbrace{⟦Γ ⊢ Y \; M⟧ \; \vec{g}}_{= \bigvee_n (⟦M⟧ \, \vec{g})^n (⊥)} \overset{?}{=} \underbrace{⟦Γ ⊢ M \, (Y \; M)⟧ \; \vec{g}}_{= ⟦M⟧ \, \vec{g} (⟦Y \, M⟧ \, \vec{g})}

But:

\begin{align*} ⟦M⟧ \, \vec{g} (⟦Y \, M⟧ \, \vec{g}) & = ⟦M⟧ \, \vec{g} \left(\bigvee_n (⟦M⟧ \, \vec{g})^n (⊥)\right) \\ & = \bigvee_n ⟦M⟧ \, \vec{g} (⟦M⟧ \, \vec{g})^n (⊥) &&\text{by Scott-continuity} \\ & = \bigvee_n (⟦M⟧ \, \vec{g})^n (⊥) \end{align*}

Is is true that

⟦M⟧ = ⟦N⟧ \overset{?}{⟹} M =_{β(η)} N

NO!!! Indeed, recall that:

Tags:

Updated: