Cours 17: Fully abstract models

Th: Let $M$ be a PCF program, then

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

Corollary:

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

Now: what happens if we consider arbitrarily compicated terms?

Ex: If $⊢ M, N: A_1 ⟹ ⋯ ⟹ A_n ⟹ ι$, what can we say of $⟦M⟧ = ⟦N⟧$?

If $⊢ M, N: A_1 ⟹ ⋯ ⟹ A_n ⟹ ι$ and $⟦M⟧ = ⟦N⟧$,

then for any context $C[_]: ι$, for any $n ∈ ℕ$,

\[C[n] ⟶^\ast \underline{n} \text{ iff } C[N] ⟶^\ast \underline{n}\]
Contexts:

A term with a “hole”:

\[[\;^A] \mid MC[] \mid C[] N \mid λx. C[] \\ \texttt{ if } C[] \texttt{ then } M \texttt{ else } P \mid \texttt{ if } M \texttt{ then } C[] \texttt{ else } P\]

NB: It means that if two subprograms share the same semantic, then you can interchange them.

Proof:

Given that $⟦M⟧ = ⟦N⟧$, show that $⟦C[M]⟧ = ⟦C[N]⟧$ by structural induction on $C$.

Ex: if $C[M] ← (λx. C[x]) M$:

\[⟦C[M]⟧ = ⟦λx. C[x]⟧ ⟦M⟧ = ⟦λx. C[x]⟧ ⟦N⟧ = ⟦C[N]⟧\]

In fact, we have to show that the lemma holds even if $M, N$ have free variables: $Γ ⊢ M, N: A$

NB: During substitution, no free variable is bouns, while when applying a context, it can happen.

Fully abstract models

A model $⟦_⟧$ is fully abstract with respect to $\sim$:
\[\text{ iff } ⟦M⟧ = ⟦N⟧ ⟺ M \sim N\]

In our case: let $Γ ⊢ M, N: A$.

$\quad M \sim N$:
\[\text{ iff }∀C [{}^{Γ ⊢ A}]: ι, ∀n, C[M] ⟶^\ast \underline{n} \text{ iff } C[N] ⟶^\ast \underline{n}\]

Equationally fully abstract models

Same as before, but for preorder relations:

$M ≼ N$:
\[\text{ iff } ∀C [{}^{Γ ⊢ A}]: ι, ∀n, \text{ if } C[M] ⟶^\ast \underline{n} \text{ then } C[N] ⟶^\ast \underline{n}\]

NB: $N$ can be seen as “better-defined” than $M$

For these previously defined $\sim$ and $≼$, we have:

\[⟦M⟧ ≤ ⟦N⟧ ⟺ M ≼ N\\ ⟦M⟧ = ⟦N⟧ ⟺ M \sim N\]

$CPO$ is not fully abstract

$CPO$ is not fully abstract wrt $\sim$ ! We have some counter-examples such that:

\[M \sim N \text{ but } ⟦M⟧ ≠ ⟦N⟧\]

$M, N: (\omicron ⟶ \omicron ⟶ \omicron) ⟶ \omicron$

We have to find a term $por$ such that

\[\not\exists P; \; ⟦P⟧ = por\]

Indeed: if

\[⟦M⟧ \; por ≠ ⟦N⟧ \; por \text{ and } M \sim N \text{ and } \exists P; \; ⟦P⟧ = por\]

then as $MP \sim NP$ and $MP, NP$ are of ground type:

\[⟦M⟧ ⟦P⟧ = ⟦MP⟧ = ⟦NP⟧ = ⟦N⟧ ⟦P⟧\]

Counter-example: parallel or: $por$

\[por ≝ \begin{cases} ⟦\omicron⟧ × ⟦\omicron⟧ ⟶ ⟦\omicron⟧ \\ ⊥, tt &⟼ tt\\ tt, ⊥ &⟼ tt \\ ⊥, ⊥ &⟼ ⊥\\ ff, ff &⟼ ff\\ \end{cases}\]

$por$ is a monotonous function that extends the previous definition.

$⟦i⟧ =$

digraph {
rankdir=BT;
⊥ -> tt, ff;
}

    M ≝ λp.
        if p Ω tt:
            if p tt Ω:
                if p ff:
                    Ω
                else:
                    tt
            else:
                Ω
        else:
            Ω

and

N ≝ λp. Ω

cf. Gordon Plotkin (1970’s)

What about $Coh$?

Recall: we have seen $Set$, $CPO$, $Coh$.

In this category, the previous counter-example doesn’t work (it is no longer a counter-example).

But there is indeed another example: Gustav function, which shows that $Coh$ is not fully abstract.

The equational theory on finitary types (such as booleans) IS undecidable (result by Loader).

So as long as $⟦\omicron⟧ × ⟦\omicron⟧ ⟶ ⟦\omicron⟧$ is interpreted by finite functions, it the semantic cannot be fully abstract.

There exist fully abstract semantics: Game Semantics

\[A = (\vert A \vert, \sim_A)\]

where $\sim_A$ is a binary relation reflexive and symmetric.

Cliques

\[Cl(A) ≝ \lbrace x ⊆ \vert A \vert \mid ∀a, a' ∈ x, a \sim_A a'\rbrace\]

Clique properties:

  • $∅ ∈ Cl(A)$

  • $x ⊆ y ∈ Cl(A), x ∈ Cl(A)$

  • \[∀ \lbrace a, a' \rbrace ⊆ x, \lbrace a, a' \rbrace ∈ Cl(A), \text{ then } x ∈ Cl(A)\]

  • $(Cl(A), ⊆)$ is a CPO

    • the sup is the union of cliques

    • it’s even a Scott-domain

$⟦\underbrace{\omicron}_{= 1 \oplus 1}⟧ =$

  digraph {
    rankdir=TB;
    tt; ff;
  }

$Cl(⟦\omicron⟧) =$

  digraph {
    rankdir=BT;
    ∅ -> "{tt}", "{ff}";
  }

$⟦ \underbrace{ι}_{= 1 \oplus ι} ⟧ =$

  digraph {
    rankdir=TB;
    1; 2; 3; ⋯[shape=none];
  }

$Cl(⟦ι⟧) =$

  digraph {
    rankdir=BT;
    ∅ -> "{1}", "{2}", ⋯;
  }

Categories whose objects are coherent spaces:

  • Coh spaces, linear functions ($!$: comonad)

⇓ Kleisli

  • Coh spaces, stable functions
Stable function $f: A ⟶ B$:

$f$ is a function from $Cl(A)$ to $Cl(B)$ s.t.

  1. Monotonous: $∀ x ⊆ y ∈ Cl(A), f(x) ⊆ f(y)$

  2. Preserve the sup: \(∀ \lbrace x_i \rbrace \Uparrow ⊆ Cl(A), \quad f\Big( \bigcup_i x_i \Big) = \bigcup_i f(x_i)\)

  3. \[∀x ∪ y ⊆ Cl(A), \quad f(x ∩ y) = f(x) ∩ f(y)\]

NB:

  • the first two properties (Scott-continuity) enable us to define the fixed point

  • the perservation of the intersection eliminates the “parallel or” from stable functions: $(⊥, tt) ∩ (tt, ⊥) = (⊥, ⊥)$, but \(por((⊥, ⊥)) = ⊥ ≠ \underbrace{por((⊥, tt))}_{tt} ∩ \underbrace{por((tt, ⊥))}_{tt} = tt\)

Leave a comment