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$

Tags:

Updated: