Execises 2: Stable models of $λ$calculus
Teacher: PaulAndré Melliès
Stable models (dIdomains): by Gérard Béry, at the same time (in the 80’s), Girard introduced dilators (models of system F).
In this problem, we call a graph $A ≝ (V, E)$ a set $V$ of vertices equipped with a reflexive and symmetric relation $E ⊆ V × V$ describing the edges.
 A clique of a graph $A$:

is defined a a subset $u ⊆ V$ such that ∀a,a' ∈ u, \quad (a,a') ⊆ E
One recalls that a continuous function is monotonic by definition.
Q1. Show that the set of cliques of $A$ ordered by inclusion defines a domain $(D_A, ≤_A)$
It is a DCPO:
 It is a partial order

Let $D$ be a directed set of cliques. The union $\bigcup D$ of these cliques

is still a clique: indeed, let $a, b ∈ \bigcup D$. There exist two cliques $u_a, u_b$ such that a ∈ u_a \qquad \text{ and } \qquad b ∈ u_b But as $D$ is directed, there exists a clique $v \supset u_a, u_b$, so as $a, b ∈ v$, $(a,b) ⊆ E$.

and clearly it is the lub of $D$

It has a smallest element: the empty clique.
NB: We will interpret every type of ST $λ$calculus (and even linear logic) as such a domain: a coherence space (introduced by Girard, subcategory of dIdomains).
Q2. Show that
a continuous function f: D_A ⟶ D_B is entirely described by its restriction !A \hookrightarrow D_A \xto f D_B
to the set (noted $!A$) of the finite cliques of the graph $A$.
because ℱ_u ≝ \lbrace u' ∈ !A \; \mid \; u' ⊆ u\rbrace is clearly a filter, so $f$ commutes with its lub.
Q3. From this, deduce the existence of a bijection between the set of continuous functions from $D_A$ to $D_B$ and the set of monotonic functions from $!A$ to $D_B$, and describe how the bijection works.
and by the previous question:
$\bigcup\limits_{u’ ⊆_f \bullet} f(u’)$ is indeed

welldefined, as $\lbrace f(u’) \; \mid \; u’ ⊆_f u \rbrace$ is a filter for every clique $u$, since $f$ is monotonic

continuous: if $D$ is a directed set of $D_A$:
\begin{align*} \bigcup\limits_{u' ⊆_f \bigvee D} f(u') & = \bigcup\limits_{∃ \, u ∈ D; \, u' ⊆_f u} f(u') &&\text{(as } \bigvee D = \bigcup\limits_{u ∈ D} u \text{ and finite cliques are compact element)}\\ & = \bigcup\limits_{u ∈ D} \bigcup\limits_{u' ⊆_f u} f(u') \\ & = \bigvee\limits_{u ∈ D} \bigcup\limits_{u' ⊆_f u} f(u') \end{align*}
$Ψ(g)$ is monotone:

$x ≤ y$ then $ℱ_x ⊆ ℱ_y$, hence
\bigvee g (ℱ_x) ≤ \bigvee g(ℱ_y)because $\bigvee g (ℱ_y)$ is an upper bound of $g(ℱ_y)$, hence of $g(ℱ_x)$ and $\bigvee g (ℱ_x)$ is the least upper bound of $g(ℱ_x)$
$Ψ(g)$ is continuous:

By monotonicity:
\underbrace{\bigvee Ψ(g)(ℱ)}_{\bigvee \lbrace g(u) \; \mid \; ∃x ∈ ℱ; u ≤ x \rbrace} ≤ Ψ(g)\Big(\bigvee ℱ\Big)Now,
Ψ(g)\Big(\bigvee ℱ\Big) = \bigvee g(ℱ_{\bigvee ℱ}) \overset{?}{≤} \bigvee \lbrace g(u) \; \mid \; ∃x ∈ ℱ; u ≤ x \rbraceWe reduced the problem to the question: for every element $v ∈ ℱ_{\bigvee ℱ}$, every finite clique $v ⊆ \bigvee ℱ$, does there exist an element $x ∈ ℱ$ such that $v ⊆ x$?
For every filter $ℱ$:
v ≤ \bigvee ℱ ⟹ ∃ x ∈ ℱ; v ≤ xIndeed:
v ≤ \bigvee ℱ = \bigcup\limits_{x ∈ ℱ} x ⟹ ∀ a_i ∈ v ≝ \lbrace a_i \rbrace_{1 ≤ i ≤ n}, \; ∃ x_i ∈ ℱ; \; a_i ∈ x_i\\ v ⊆ \bigvee_{1 ≤ i ≤ n} x_i \quad\text{ (filter)}
##
Q4. For every continuous function $f: D_A → D_B$, one defines the set
of elements $(u,b)$ satisfying the two properties below:
 $b ∈ f(u)$
 $b ∉ f(v)$ for every clique $v ∈ D_A$ stricly included in $u$
Show that, for all clique $u$ of $A$:
So clearly $U ⊆ f(u)$, and conversely: $f(u) ⊆ U$:

indeed, for all $b ∈ f(u)$: as $\lbrace v’ ∈ \, !A \; \mid \; v’ ≤_A u \text{ and } b ∈ f(v’) \rbrace ≠ ∅$, by setting
v \, ≝ \, \bigcap\limits_{v' ∈ !A; \; v' ≤_A u \text{ and } b ∈ f(v')} v'$v$ is still a finite clique included in $u$ containing $b$, and by minimality of $v$: $(v, b) ∈ \Tr(f)$, hence $b ∈ U$
Therefore: $f(u) = U$.
Q5.
In order to understand the meaning of “stability”, it is good to consider the special case of a stable function
Every monotone function $f: D_A ⟶ D_1$ is entirely described by the inverse image of $⊤$:
which is upper closed, because $f$ is monotone.
When the function is continuous, $f^{1}(⊤)$ is entirely described by $\Tr \, f$
NB: the $u_i$’s are finite elements
A continuous function
is stable precisely when
where $u # v$ means that there does not exist any $w$ such that $u, v ≤ w$
In other words, the $u_i$’s are pairwise incompatible.
cf picture “parallel or”: not stable (it cannot be implemented by a $λ$term: Béry’s model was a proof of that)
NB: Syntax ≃ Existential (there exists a $λ$term that implements…) VS Model ≃ Universal (for all $λ$term, it does not implement…)
Every $λ$term can be interpreted by a stable function: for any computation, there exists a minimal amount of information that led to this output. Stability: you also have uniqueness of this minimal piece of information (look at parallel or: if $True$ is returned, you don’t know which branch ($⊤⊥$ or $⊥⊤$) triggered it)
$⟹$: $(u,b) ∈ \Tr f$. For $v ↑ u$,
 If $u ≤ v$, then $b ∈ f(u) ⊆ f(v)$ as $f$ is monotone
 If $b ∈ f(v)$: $u ≤ v$ because $u ↑ v$ and $f$ is stable: $b ∈ f(u) ∩ f(v) = f(u ∩ v)$ hence $u ∩ v = u$ and $u ≤ v$
$⟸$: Suppose ∀ v ↑ u, \quad u ≤ v ⟺ b ∈ f(v)
For all $v$ included in $u$ compatible with $u$ ($v ↑ u$),
hence $(u,b) ∈ \Tr f$
Q6.
$f: D_A ⟶ D_B$ linear ⟺ every element in the trace is of the form $(\lbrace a\rbrace, b)$
Leave a comment