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