Cours 16: PCF: Logical Relations to show Adequacy

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*}\]

What about completeness?

Is is true that

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

NO!!! Indeed, recall that:

  • $Ω_ι ≝ Y \; (λx^ι.x^ι) ⟶ (λx.x) Ω ⟶ Ω ⟶ ⋯$$
  • \[S_ι ≝ Y \; (λx^ι. succ \; x^ι)\]

And

\[⟦Ω_ι⟧ = ⟦S_ι⟧ = ⊥\]

(since $⊥$ is a fixed-point thereof)

But

\[Ω_ι ≠_{β(η)} S_ι\]

Let’s try to find out the “meaning” of $⟦M⟧ = ⟦N⟧$ then!

Adequacy

Th (ADEQUACY): Let $M$ be a PCF program, then

\[⟦M⟧ = n ⟺ M ⟶^\ast \underline{n}\]

Corollary:

\[⟦M⟧ = ⟦N⟧ ⟺ \begin{cases} \text{ if } M ⟶^\ast \underline{n} ⟺ N ⟶^\ast \underline{n} \\ \text{ or else } M \text{ and } N \text{ diverge } \end{cases}\]

i.e.

\[⟦M⟧ = ⟦N⟧ ⟺ (∀n, M ⟶^\ast \underline{n} ⟺ N ⟶^\ast \underline{n})\]

NB:

  1. one can replace $n$ by a boolean $b: \omicron$, it stands for any ground type (but we can express the boolean as integers, so let’s restrict ourselves to integers).

  2. it’s not true anymore for types which are not ground

Proof:

$⟸$: is a trivial consequence of the soundness theorem: it follows that $⟦M⟧ = ⟦n⟧ = \underline{n}$

$⟹$: we will try to “lift” the statement to a higher order, so as to have more powerful induction hypothesis.

Let’s define

\[(ℛ^A)_{A ∈ Types} ⊆ ⟦A⟧ × Terms_A\]

  • $ℛ^ι$:

    \[\underbrace{v}_{ ∈ ⟦ι⟧} \; ℛ^ι \; \underbrace{M}_{⊢ M: ι} ⟺ (v=n ⟹ M ⟶^\ast \underline{n})\]

    NB: so that the relation $⟦M⟧ \; ℛ^ι \; M$ gives us exactly what we want to show.

    In fact, we have:

    \[∀f ≤ ⟦M⟧, f \; ℛ^ι \; M\]

  • $ℛ^{A ⇒ B}$

    \[f \; ℛ^{A ⇒ B} \; M ⟺ ∀v \; ℛ^A \; N, f(v) \, ℛ^B \; MN\]

Problem: In, $⟦M⟧ \; ℛ^ι \; M$, the type will be complexified, and the term will not always be close in the proof.

Key Lemma (of the Logical Relation):

$∀ x_1:A_1, ⋯, x_n: A_n ⊢ M:B, ∀ v_i \; ℛ^{A_i} \; N_i \quad (i ≤ n)$:

\[⟦x_1:A_1, ⋯, x_n: A_n ⊢ M:B⟧ \, (v_1, ⋯, v_n) \; ℛ^B \; M \lbrace N_1/x_1, ⋯, N_n/x_n \rbrace\]

Proof: By induction on a derivation of $x_1:A_1, ⋯, x_n: A_n ⊢ M:B$

  • $M = x_j$:

    \[\underbrace{⟦\vec{x_i}: \vec{A_i} ⊢ M⟧ \, \vec{v_i}}_{= v_j} \; ℛ^{A_j} \; \underbrace{N_j}_{= M \lbrace N_i/x_i \rbrace}\]

  • $M = \underline{n}$:

    \[\underbrace{⟦Γ ⊢ M⟧ \, \vec{v_i}}_{= ⟦\underline{n}⟧ = n} \; ℛ^{A_j} \; \underbrace{\underline{n}}_{= M \lbrace N_i/x_i \rbrace}\]

  • $M = \texttt{if } P^\omicron \texttt{ then } Q^ι \texttt{ else } L^ι$:

    \[⟦Γ ⊢ M⟧ \, \vec{v_i} = \begin{cases} ⟦Γ ⊢ Q⟧ \, \vec{v_i} &&\text{ si } ⟦Γ ⊢ P^\omicron⟧ \, \vec{v_i} = true \\ ⟦Γ ⊢ L⟧ \, \vec{v_i} &&\text{ si } ⟦Γ ⊢ P^\omicron⟧ \, \vec{v_i} = false \\ ⊥ &&\text{ sinon si } ⟦Γ ⊢ P^\omicron⟧ \, \vec{v_i} = ⊥ \end{cases}\]

    WARNING! THE DEFINITION HAS CHANGED, SO THIS PART OF THE PROOF IS NO LONGER VALID: Let’s consider the third case: then $⊥ \; ℛ^\omicron \; P \lbrace N_i/x_i \rbrace$ by IH, so that $P \lbrace N_i/x_i \rbrace$ diverges by definition, and $M \lbrace N_i/x_i \rbrace$ as well. Therefore: $⟦Γ ⊢ M⟧ \, \vec{v_i} \; ℛ^ι \; M \lbrace N_i/x_i \rbrace$ by definition.

    Now, the first case (the second one will be analogous): then $⟦Γ ⊢ M⟧ \, \vec{v_i} = ⟦Γ ⊢ Q⟧ \, \vec{v_i}$, and as by IH: $⟦Γ ⊢ Q⟧ \, \vec{v_i} \; ℛ^\omicron \; Q \lbrace N_i/x_i \rbrace$. But $M \lbrace N_i/x_i \rbrace ⟶^\ast Q \lbrace N_i/x_i \rbrace$, so the result is clear, since $v \; ℛ^ι _$ is clearly closed under anti-reduction.

  • $M = λy^C. L^D$ ($B = C ⇒ D$):

    Let’s show $⟦Γ ⊢ λy^C. L^D⟧ \, \vec{v_i} \; ℛ^B \; λy^C. L^D \lbrace N_i/x_i \rbrace$:

    Let $u \; ℛ^C \; P$: let’s show that

    \[\underbrace{⟦Γ ⊢ λy^C. L^D⟧ \, \vec{v_i}\, u}_{= ⟦y:C, Γ ⊢ L^D⟧ (u, \vec{v_i})} \; ℛ^D \; \underbrace{(λy^C. L^D) \, P \, \lbrace N_i/x_i \rbrace}_{⟶ L^D \lbrace N_i/x_i \rbrace \lbrace P/y \rbrace \text{ since } P \text{ is closed}}\]

    But by IH:

    \[⟦y:C, Γ ⊢ L^D⟧ (u, \vec{v_i}) \; ℛ^D \; L^D \lbrace N_i/x_i \rbrace \lbrace P/y \rbrace\]

    so

    \[⟦Γ ⊢ λy. L^D⟧ \vec{v_i} \, u \; ℛ^D \; L^D \lbrace N_i/x_i \rbrace \lbrace P/y \rbrace\]

    and by closure under anti-reduction:

    \[⟦Γ ⊢ λy. L^D⟧ \vec{v_i} \, u \; ℛ^D \; (λy. L^D \lbrace N_i/x_i \rbrace) \, P = (λy. L^D P) \lbrace N_i/x_i \rbrace = M \lbrace N_i/x_i \rbrace\]

  • $M = L^{C ⇒ B} Q^C$:

    By IH:

    \[\begin{cases} ⟦L⟧ \, \vec{v_i} \; ℛ^{C ⇒ B} \; L \lbrace N_i/x_i \rbrace \\ ⟦Q⟧ \, \vec{v_i} \; ℛ^{C ⇒ B} \; Q \lbrace N_i/x_i \rbrace \end{cases}\]

    So one concludes by definition of $ℛ^{C ⇒ B}$

  • $M = Y \; L^{B ⇒ B}$:

    \[⟦YL⟧ \, \vec{v_i} \; ℛ^B \; YL \lbrace N_i/x_i \rbrace\]

    • By the lemma 2: \(⊥ \lbrace \vec{v_i} \rbrace \; ℛ^B \; YL \lbrace N_i/x_i \rbrace\)

    • \[⟦L⟧ \, (\vec{v_i}) \, (⊥ \, \vec{v_i}) \; ℛ^B \; YL \lbrace N_i/x_i \rbrace\]

      Since by IH,

      \[⟦L⟧ \, \vec{v} \; ℛ^{B ⇒ B} \; L \lbrace N_i/x_i \rbrace\]

      that is:

      \[⟦L⟧ \, \vec{v} \, (⊥ \, \vec{v}) \; ℛ^B \; L \lbrace N_i/x_i \rbrace (Y L \lbrace N_i/x_i \rbrace)\]

      Therefore we conclude, by closure by anti-reduction

Lemma (Closure) 1: $v \; ℛ^A _$ is closed under anti-reduction, i.e.:

\[v \; ℛ^A \; M \text{ and } M ⟶^\ast N ⟹ v \; ℛ^A \; N\]

Reminder:

  • $v \; ℛ^ι \; M$ ssi $(v = n ⟹ M ⟶^\ast \underline{n})$

  • $v \; ℛ \; M$ ssi $∀ n \; ℛ^A \; N, \quad v n \; ℛ^B \; MN$

A type is of the form

\[A = A_1 ⟹ ⋯ ⟹ A_n ⟹ ι\]

Let’s assume that

\[n_1 \; ℛ^{A_1} \; N_1, ⋯, n_n \; ℛ^{A_n} \; N_n\]

Show that

\[v n_1 ⋯ n_n ℛ^ι M N_1 ⋯ N_n\]

i.e. if $v n_1 ⋯ n_n = k$, then $M N_1 ⋯ N_n ⟶^\ast \underline{k}$.

As $M ⟶ N$, it follows that

\[M N_1 ⋯ N_n ⟶ N N_1 ⋯ N_n\]

By hyp: $v \; ℛ^A \; N$, so

\[N N_1 ⋯ N_n ⟶^\ast \underline{k}\]

And we conclude.

Lemma 2:

  • $⊥ \; ℛ^A \; M$
  • if $v_0 ≤ v_1 ≤ ⋯$ s.t. $∀i, v_i \; ℛ^A \; M$: then \(\bigvee_i v_i \; ℛ^A \; M\)

Outline of the proof:

  • Induction step: to show that $⊥ n_1 ⋯ n_n \; ℛ^ι \; M N_1 ⋯ N_n$, it suffices to show that $⊥ \; ℛ^ι \; M N_1 ⋯ N_n$ (base step), since the functions are orderes pointwise.
  • we use the fact that if $(\bigvee_i v_i) \, n_1 ⋯ n_n \; ℛ^ι \; M \, N_1 ⋯ N_n$, then $(\bigvee_i v_i \, n_1 ⋯ n_n) \; ℛ^ι \; M \, N_1 ⋯ N_n$ (since functions are ordered pointwise: $(\bigvee_i f_i)(x) ≝ \bigvee_i f_i (x)$)

Leave a comment