Execises 2: Stable models of $λ$-calculus

Teacher: Paul-André Melliès

\[\newcommand\xto\xrightarrow \newcommand\xfrom\xleftarrow \newcommand{\Tr}{\mathop{\mathrm{Tr}}}\]

Stable models (dI-domains): 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 dI-domains).

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

  • well-defined, 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