Execises 2: Stable models of $λ$calculus
Teacher: PaulAndré Melliès
\[\newcommand\xto\xrightarrow \newcommand\xfrom\xleftarrow \newcommand{\Tr}{\mathop{\mathrm{Tr}}}\]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$.
\[f(u) = f\Big(\bigcup\limits_{u' ⊆_f u} u'\Big) \overset{\text{continuity}}{=} \bigcup\limits_{u' ⊆_f u} f(u')\]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.
\[Φ: \begin{cases} Cont(D_A,D_B) &⟶ Mon(!A, D_B) \\ f &⟼ f_{!A} \end{cases}\]and by the previous question:
\[Ψ ≝ Φ^{1}: \begin{cases} Mon(!A, D_B) &⟶ Cont(D_A,D_B)\\ f &⟼ \bigcup\limits_{u' ⊆_f \bullet} f(u') \end{cases}\]$\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 \rbrace\]We 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 ≤ x\]Indeed:
\[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
\[\Tr(f) ⊆ \, !A × B\]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$:
\[f(u) = \underbrace{\big\lbrace b ∈ B \; \mid \; ∃ \, v ∈ \, !A; \; v ≤_A u \text{ and } (v,b) ∈ \Tr(f)\big\rbrace}_{\text{denoted by } U}\] \[\begin{align*} f(u) & = f \bigg(\bigcup\limits_{v ⊆_f u} v\bigg) \\ & = \bigcup\limits_{v \, ⊆_f u} f(v) &&\text{ (continuity)}\\ & = \big\lbrace b ∈ B \; \mid \; ∃ \, v ∈ \, !A; \; v ≤_A u \text{ and } b ∈ f(v)\big\rbrace \end{align*}\]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
\[f: D_A ⟶ D_1 = \underbrace{\lbrace ∅ ≤ \lbrace \ast \rbrace}_{= Σ \text{ (Sierpinski)}}\rbrace\]Every monotone function $f: D_A ⟶ D_1$ is entirely described by the inverse image of $⊤$:
\[f^{1}(⊤) ⊆ D_A\]which is upper closed, because $f$ is monotone.
When the function is continuous, $f^{1}(⊤)$ is entirely described by $\Tr \, f$
\[\Tr f = \lbrace (u_i, \ast) \; \mid \; \ast \text{ is the unique element of } 1 = \lbrace\ast\rbrace \text{ and } f(u_i) = ⊤ \text{ and } ∀v \text{ strictly included in } u_i, \; f(v) = ⊥\rbrace\]NB: the $u_i$’s are finite elements
A continuous function
\[f: D_A ⟶ Σ = D_1\]is stable precisely when
\[∀i, j, \quad i ≠ j ⟹ u_i \# u_j\]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 ⟺ (∀ v ↑ u, \quad u ≤ v ⟺ b ∈ f(v))\]$⟹$: $(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$),
\[b ∈ f(v) ⟹ u ≤ v \text{, and } u = v\]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