as Engeler’s model [39] and the same inequational theory as the filter model
defined by Ronchi Della Rocca in [76].

######  Theorem 5.8.

For $M,N\in\Lambda$ we have

$M\sqsubseteq_{\sf r}N\iff\mathcal{E}\models M\sqsubseteq N$

Therefore $\mathrm{Th_{\sqsubseteq}}(\mathcal{E})=\ \sqsubseteq_{\sf r}$ and
$\mathrm{Th}(\mathcal{E})=\mathcal{B}$.

######  Proof 5.9.

$(\Rightarrow)$ It follows immediately by Proposition 5.5.

$(\Leftarrow)$ Suppose, by the way of contradiction, that
$M\not\sqsubseteq_{\sf r}N$ but $\mathcal{E}\models M\sqsubseteq N$. Since
$\mathrm{Th_{\sqsubseteq}}(\mathcal{E})$ is sensible, Lemma 2.1 entails
$M\sqsubseteq_{\mathcal{H^{*}}}N$. By Lemma 5.7, there exists
$t\in\mathrm{BT}^{*}(M)$ and $\Gamma,\alpha$ such that $\Gamma\vdash t:\alpha$
while $\Gamma\not\vdash u:\alpha$ for all $u\in\mathrm{BT}^{*}(N)$. By the
Approximation Theorem, we have $(\Gamma,\alpha)\in\llbracket
M\rrbracket-\llbracket N\rrbracket$, which is impossible.

The above proof-technique could be suitably generalized to prove that all non-
extensional relational graph models induce the same inequational theory,
namely $\sqsubseteq_{\sf r}$.

######  Theorem 5.9.

The relation $\sqsubseteq_{\sf r}$ is the minimal inequational graph theory.
Similarly, $\mathcal{B}$ is the minimal relational graph theory.

###  5.3. A Semantic Characterization of Normalizability

We now show that in the model $\mathcal{E}$ $\beta$-normalizable
$\lambda$-terms have a simple semantic characterization. Indeed, since there
are no equations between atoms and arrow types, it makes sense to define
whether $\omega$ occurs in a type $\alpha$ with a certain _polarity_
$p\in\\{+,-\\}$.

######  Definition 5.10.

For all elements $\alpha$ of $\mathcal{E}$ the relations $\omega\in^{+}\alpha$
and $\omega\in^{-}\alpha$ are defined by mutual induction as follows (where
$p$ is a polarity and $\lnot p$ denotes the opposite polarity):

  1. (i)

$\omega\in^{-}a\to\beta$ if $a=\omega$;

  2. (ii)

if $\omega\in^{p}\beta$ then $\omega\in^{p}a\to\beta$;

  3. (iii)

if $\omega\in^{\neg p}\beta$ then $\omega\in^{p}([\beta]+a)\to\gamma$.

When $\omega\in^{+}\alpha$ (resp. $\omega\in^{-}\alpha$) holds we say that
$\omega$ _occurs positively_ (resp.  _negatively_) in $\alpha$. We write
$\omega\notin^{p}\alpha$ whenever $\omega$ does not occur in $\alpha$ with
polarity $p$.

These notions extend to multisets in the obvious way, that is,
$\omega\in^{p}[\alpha_{1},\dots,\alpha_{n}]$ whenever
$\omega\in^{p}\alpha_{i}$ for some index $i$. Similarly, $\omega\in^{p}\Gamma$
whenever there is $x\in\mathrm{Var}$ such that $\omega\in^{p}\Gamma(x)$.

######  Theorem 5.10.

Let $M\in\Lambda$. The following are equivalent:

  1. (1)

$M$ has a $\beta$-normal form,

  2. (2)

$\Gamma\vdash_{\mathcal{E}}M:\alpha$ for some environment $\Gamma$ and type
$\alpha$ such that $\omega\notin^{+}\alpha$ and $\omega\notin^{-}\Gamma$.

######  Proof 5.11.

(1 $\Rightarrow$ 2) Straightforward induction on the derivation of
$\Gamma\vdash\mathsf{nf}_{\mathtt{\beta}}(M):\alpha$.

(2 $\Rightarrow$ 1) We proceed by structural induction on the pair
$(\Gamma,\alpha)$. By Lemma 4.10, $M$ has a head normal form $\lambda
x_{1}\dots x_{n}.x_{i}M_{1}\cdots M_{k}$ having type $\alpha$ in the context
$\Gamma$, which entails $\alpha=a_{1}\to\cdots\to a_{n}\to\alpha^{\prime}$.
So, there exists a derivation of the form:

$\Gamma\vdash\lambda x_{1}\dots x_{n}.x_{i}M_{1}\cdots
M_{k}:\alpha=a_{1}\to\cdots\to
a_{n}\to\alpha^{\prime}\Gamma,x_{1}:a_{1},\dots,x_{n}:a_{n}\vdash
x_{i}M_{1}\cdots M_{k}:\alpha^{\prime}\lx@proof@logical@and\Gamma_{0}\vdash
x_{i}:b_{1}\to\cdots\to b_{k}\to\alpha^{\prime}\Gamma_{j\ell}\vdash
M_{j}:\beta_{j\ell}1\leq j\leq k1\leq\ell\leq k_{j}$

where $\Gamma_{0}=[x_{i}:b_{1}\to\cdots\to b_{k}\to\alpha^{\prime}]$, for all
$j\leq k$ we have $b_{j}=[\beta_{j1},\dots,\beta_{jk_{j}}]$ and
$\Gamma,x_{1}:a_{1},\dots,x_{n}:a_{n}=\Gamma_{0}+(\sum_{j=1}^{k}\sum_{\ell=1}^{k_{j}}\Gamma_{j\ell})$.
Since $\omega\notin^{+}\alpha$ and $\omega\notin^{-}\Gamma$ we get for each
$j\leq k$ that $b_{j}$ is non-empty, and moreover that
$\omega\notin^{+}\beta_{j\ell}$ and $\omega\notin^{-}\Gamma_{j\ell}$ for all
$\ell\leq k_{j}$. From the induction hypothesis, we get that all the $M_{i}$’s
have a $\beta$-normal form.

As proved in [67], Theorem 6 holds for every relational graph model
$\mathcal{D}$ _preserving $\omega$-polarities_ (in a technical sense). An
analogue of this theorem also holds for the usual intersection type systems
[8]. However, for an extensional relational graph model $\mathcal{D}$ this
lemma is enough to conclude
$\mathrm{Th_{\sqsubseteq}}(\mathcal{D})=\,\sqsubseteq_{\mathcal{H^{+}}}$,
while this is not the case for filter models. In other words, being
extensional and preserving $\omega$-polarities are sufficient conditions for a
relational graph model to be fully abstract for $\mathcal{H^{+}}$. We will now
provide conditions that are both necessary and sufficient.

##  6\. Characterizing Fully Abstract Relational Models of $\mathcal{H^{+}}$

In this section we provide a characterization of those relational graph models
that are (inequationally) fully abstract for $\mathcal{H}^{+}$. We first
introduce the notion of _$\lambda$ -König_ relational graph model (Definition
6.8), and show that a relational graph model $\mathcal{D}$ is extensional and
$\lambda$-König exactly when the induced inequational theory is the preorder
$\sqsubseteq_{\mathcal{H^{+}}}$ (Theorem 9).

Since our proof technique does not rely on the quantitative properties of
relational graph models, hereafter we rather prefer to use the categorical
interpretation.

###  6.1. Lambda König Relational Graph Models

Before entering into the technicalities we try to give the intuition behind
our condition. The main issue is to find suitable conditions for assuring that
if $M,N$ have the same interpretation in a relational graph model
$\mathcal{D}$ then $M=_{\mathcal{H^{+}}}\\!N$, equivalently that
$M\neq_{\mathcal{H^{+}}}\\!N$ implies
$|M|^{\mathcal{D}}\not=|N|^{\mathcal{D}}$. Now, the idea behind Theorem 2.3 is
that two $\lambda$-terms $M,N$ are equal in $\mathcal{H^{*}}$, but different
in $\mathcal{H}^{+}$, when there is a (possibly _virtual_ 888Intuitively, a
position $\sigma$ is virtual if it does not belong to $\mathrm{BT}(M)$, but
rather to one of its $\eta$-expansions. For more details we refer to [7,
§10.3]. ) position $\sigma\in{\rm Nature}^{<\omega}$ such that, say,
$\mathrm{BT}(M)_{\sigma}=x$ while $\mathrm{BT}(N)_{\sigma}$ is an infinite
$\eta$-expansion of $x$ following some $T\in\mathbb{T}^{\infty}_{\textrm{\sf
rec}}$. As a consequence of this fact, our models need to separate $x$ from
any ${\bf J}_{T}x$ for $T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$ in order
to be fully abstract for $\mathcal{H^{+}}$.

Notice now that in any extensional relational graph model $\mathcal{D}$, every
element $\alpha_{0}$ is equal to an arrow, so one can always try to unfold
$\alpha$ following a function $f$, starting with:

$\alpha_{0}=a_{0}\to\dots\to a_{f(0)}\to\beta$

If there is an $\alpha_{1}\in a_{f(0)}$, then one can keep unfolding:

$\alpha_{1}=a^{\prime}_{0}\to\dots\to a^{\prime}_{f(1)}\to\beta^{\prime}$

and so on. More generally, at level $\ell$ we have
$\alpha_{\ell}=b_{0}\to\dots\to b_{f(\ell)}\to\alpha^{\prime}$ for some
$b_{i}\in\mathcal{M}_{\mathrm{f}}(D)$ and $\alpha^{\prime}\in D$ and as long
as there exist an $\alpha_{\ell+1}\in a_{f(\ell)}$, we can keep unfolding it
at level $\ell+1$. There are now two possibilities.

  1. (1)

If this process continues indefinitely, then we consider that $\alpha$ can
actually be unfolded following $f$.

  2. (2)

Otherwise, if at some level $\ell$ we have $a_{f(\ell)}=\omega$, then the
process is forced to stop and we consider that $\alpha$ cannot be unfolded
following $f$.

Now, as $T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$ is a finitely branching
infinite tree, by König’s lemma there exists an infinite path $f$ in
$\mathrm{BT}({\bf J}_{T})$. Since the interpretation of ${\bf J}_{T}$ is
inductively defined (rather than coinductively), we will then have that
$[\alpha]\to\alpha\notin|{\bf J}_{T}|$ for any $\alpha$ whose unfolding can
actually follow $f$.

In some sense such an $\alpha$ is _witnessing within the model_ the existence
of an infinite path $f$ in $T$, and therefore in ${\bf J}_{T}$. The following
is a formal definition of such a witness.

Recall from Definition 1.3, that $\Pi(T)$ denotes the set of infinite paths of
a tree $T\in\mathbb{T}^{\infty}$.

######  Definition 6.1.

Let $\mathcal{D}$ be an rgm, $T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$ and
$f\in\Pi(T)$.

  * •

We coinductively define the set $\mathsf{W}_{\mathcal{D},f}(T)$ of all
_witnesses for $T$ (in $\mathcal{D}$) following $f$_. An element $\alpha\in D$
belongs to $\mathsf{W}_{\mathcal{D},f}(T)$ whenever there exist
$a_{0},\dots,a_{f(0)}\in\mathcal{M}_{\mathrm{f}}(\mathcal{D})$ and
$\alpha^{\prime}\in\mathcal{D}$ such that

$\alpha=a_{0}\to\cdots\to a_{f(0)}\to\alpha^{\prime}$

and there is a $\beta\in a_{f(0)}$ belonging to
$\mathsf{W}_{\mathcal{D},f^{\geq{1}}}(T\upharpoonright_{\\!\langle
f(0)\rangle})$ where $f^{\geq{1}}$ maps $k\mapsto f(k+1)$.

  * •

We say that $\alpha$ is a _witness for $T$ in $\mathcal{D}$_ when there exists
an $f\in\Pi(T)$ such that $\alpha$ is a witness for $T$ in $\mathcal{D}$
following $f$.

  * •

We let $\mathsf{W}_{\mathcal{D}}(T)$ be the set of all witnesses for $T$ in
$\mathcal{D}$.

We formalize the intuition given above by showing that
$\mathsf{W}_{\mathcal{D}}(T)$ is constituted by those $\alpha\in D$ such that
$[\alpha]\to\alpha\notin|{\bf J}_{T}|$. We first prove the following technical
lemmas.

######  Lemma 6.2.

Let $\mathcal{D}$ be an rgm. For all $T\in\mathbb{T}^{\infty}_{\textrm{\sf
rec}}$ and $x\in\mathrm{Var}$ we have $|{\bf
J}_{T}x|^{\mathcal{D}}_{x}\subseteq|x|^{\mathcal{D}}_{x}$.

######  Proof 6.3.

Let $(a,\alpha)\in|{\bf J}_{T}x|_{x}$. By Theorem 3 there is
$t\in\mathrm{BT}^{*}({\bf J}_{T}x)$ such that ${(a,\alpha)\in|t|_{x}}$.
Proceeding by induction on $t$, we show that $a=[\alpha]$. The case $t=\bot$
is vacuous.

Consider $t=\lambda z_{0}\dots z_{T(\varepsilon)-1}.xt_{0}\cdots
t_{T(\varepsilon)-1}$ where $t_{i}\in\mathrm{BT}^{*}({\bf J}_{T\
\upharpoonright_{\\!\langle i\rangle}}z_{i})$. By Definition 3.4(2) we have
$(a,\alpha)\in|t|_{x}$ if and only if $\alpha=a_{0}\to\cdots\to
a_{T(\varepsilon)-1}\to\alpha^{\prime}$ for some
$a_{i}\in\mathcal{M}_{\mathrm{f}}(D)$ and $\alpha^{\prime}\in D$ such that
$((a,a_{0},\dots,a_{T(\varepsilon)-1}),\alpha^{\prime})\in|xt_{0}\cdots
t_{T(\varepsilon)-1}|_{x,z_{0},\dots,z_{T(\varepsilon)-1}}$. By Definition
3.4(1) and (3), we get $a=[b_{0}\to\cdots\to
b_{T(\varepsilon)-1}\to\alpha^{\prime}]$ where
$b_{i}=[\beta_{i,1},\dots,\beta_{i,k_{i}}]$ and there is a decomposition
$a_{i}=\sum_{j=1}^{k_{i}}a_{i,j}$ such that
$(a_{i,j},\beta_{i,j})\in|t_{i}|_{z_{i}}$. By the inductive hypothesis we have
$a_{i,j}=[\beta_{i,j}]$. Therefore
$a_{i}=[\beta_{i,1},\dots,\beta_{i,k_{i}}]=b_{i}$ which in its turn entails
$a=[b_{0}\to\cdots\to
b_{T(\varepsilon)-1}\to\alpha^{\prime}]=[a_{0}\to\cdots\to
a_{T(\varepsilon)-1}\to\alpha^{\prime}]=[\alpha].$

######  Lemma 6.4.

Let $\mathcal{D}$ be an rgm. For all $T\in\mathbb{T}^{\infty}_{\textrm{\sf
rec}}$, $\alpha\in\mathsf{W}_{\mathcal{D}}(T)$ and $t\in\mathrm{BT}^{*}({\bf
J}_{T}x)$ we have $([\alpha],\alpha)\notin|t|^{\mathcal{D}}_{x}$.

######  Proof 6.5.

We proceed by induction on the size ${\\#t}$ of $t$.

Case ${\\#t}=0$. This case is trivial since $t=\bot$ and
$|\bot|_{x}=\emptyset$.

Case ${\\#t}>0$. Then $t=\lambda z_{0}\dots z_{T(\varepsilon)-1}.xt_{0}\cdots
t_{T(\varepsilon)-1}$ where each $t_{i}\in\mathrm{BT}^{*}({\bf
J}_{T\,\,\upharpoonright_{\\!\langle i\rangle}}z_{i})$ is such that
${\\#t_{i}}<{\\#t}$. By Definition 3.4(2) we have
$([\alpha],\alpha)\in|t|_{x}$ if and only if $\alpha=a_{0}\to\cdots\to
a_{T(\varepsilon)-1}\to\alpha^{\prime}$ for some
$a_{i}=[\alpha_{i,1},\dots,\alpha_{i,k_{i}}]$ and
$(([\alpha],a_{0},\dots,a_{T(\varepsilon)-1}),\alpha^{\prime})\in|xt_{0}\cdots
t_{T(\varepsilon)-1}|_{x,z_{0},\dots,z_{T(\varepsilon)-1}}$. As
$|t_{i}|_{z_{i}}\subseteq|z_{i}|_{z_{i}}$ by Lemma 6.2, we obtain
$([\alpha_{i,j}],\alpha_{i,j})\in|t_{i}|_{z_{i}}$ for all $i\leq
T(\varepsilon)-1$ and $j\leq k_{i}$. Since
$\alpha\in\mathsf{W}_{\mathcal{D},f}(T)$ for some $f$, there exists a witness
$\alpha_{f(0),j}\in a_{f(0)}$ for $T\upharpoonright_{\\!\langle f(0)\rangle}$
following $f^{\geq{1}}$. By
$\alpha_{f(0),j}\in\mathsf{W}_{\mathcal{D}}(T\upharpoonright_{\\!\langle
f(0)\rangle})$ and the induction hypothesis we get
$([\alpha_{f(0),j}],\alpha_{f(0),j})\notin|t_{f(0)}|_{z_{f(0)}}$, which is a
contradiction.

By applying the Approximation Theorem we get the following characterization of
$\mathsf{W}_{\mathcal{D}}(T)$.

######  Proposition 6.6.

For any extensional rgm $\mathcal{D}$ and any tree
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$:

$\mathsf{W}_{\mathcal{D}}(T)=\\{\alpha\in D\ |\ ([\alpha],\alpha)\not\in|{\bf
J}_{T}x|_{x}\\}.$

######  Proof 6.7.

$(\subseteq)$ Follows immediately from the Approximation Theorem 3 and from
Lemma 6.4.

$(\supseteq)$ Let $\alpha\in D$ such that $([\alpha],\alpha)\not\in|{\bf
J}_{T}x|_{x}$. We coinductively construct a path $f$ such that
$\alpha\in\mathsf{W}_{f}(T)$. As $T$ is infinite we have ${\bf
J}_{T}x=_{\beta}\lambda z_{0}\dots z_{n}.x({\bf
J}_{T\,\,\upharpoonright_{\\!\langle 0\rangle}}z_{0})\cdots({\bf
J}_{T\,\,\upharpoonright_{\\!\langle n\rangle}}z_{n})$ and since $\mathcal{D}$
is extensional $\alpha=a_{0}\to\cdots\to a_{n}\to\alpha^{\prime}$. From
$([\alpha],\alpha)\not\in|{\bf J}_{T}x|_{x}$ and the soundness we get
$([\alpha],\alpha)\notin|\lambda z_{0}\dots z_{n}.x({\bf
J}_{T\,\,\upharpoonright_{\\!\langle 0\rangle}}z_{0})\cdots({\bf
J}_{T\,\,\upharpoonright_{\\!\langle n\rangle}}z_{n})|_{x}$. Therefore there
exist an index $k\leq n$ such that $a_{k}\neq\omega$ and an element $\beta\in
a_{k}$ such that $([\beta],\beta)\not\in|{\bf
J}_{T\,\,\upharpoonright_{\\!\langle k\rangle}}z_{k}|_{z_{k}}$. In particular,
this entails that the subtree $T\upharpoonright_{\\!\langle k\rangle}$ is
infinite because $([\beta],\beta)$ belongs to the interpretation of any finite
$\eta$-expansion of $z_{k}$. Therefore we set $f(0)=k$ and, for all $n\in{\rm
Nature}$, $f(n+1)=g(n)$ where $g$ is the function given by the coinductive
hypothesis and satisfying
$\beta\in\mathsf{W}_{\mathcal{D},g}(T\upharpoonright_{\\!\langle k\rangle})$.
By construction of $f$, we conclude that
$\alpha\in\mathsf{W}_{\mathcal{D},f}(T)$.

It should be now clear that a relational graph model $\mathcal{D}$, to be
fully abstract for $\mathcal{H^{+}}$, needs for every $\lambda$-definable
infinite $\eta$-expansion of the identity an element in $D$ witnessing its
infinite path, which exists by König’s lemma. This justifies the definition
below.

######  Definition 6.8 ($\lambda$-König models).

An rgm $\mathcal{D}$ is _$\lambda$ -König_ if for every
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$,
$\mathsf{W}_{\mathcal{D}}(T)\neq\emptyset$.

We will mainly focus on the $\lambda$-König condition, since the
extensionality is clearly necessary, as
$\boldsymbol{\lambda}\eta\subseteq\mathcal{H^{+}}$.

We start by showing that, if $\mathcal{D}$ is an extensional $\lambda$-König
relational graph model, then $\mathrm{Th_{\sqsubseteq}}(\mathcal{D})=\
\sqsubseteq_{\mathcal{H^{+}}}$. Indeed, since every
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$ has a non-empty set of witnesses
$\mathsf{W}_{\mathcal{D}}(T)$, by Proposition 6.6, there is an element
$\alpha\in\mathsf{W}_{\mathcal{D}}(T)$ such that $[\alpha]\to\alpha\notin|{\bf
I}|-|{\bf J}_{T}|$. Thus, $\mathcal{D}$ separates ${\bf I}$ from all the ${\bf
J}_{T}$’s for $T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$.

######  Theorem 6.8 (Inequational Full Abstraction).

Let $\mathcal{D}$ be an extensional $\lambda$-König rgm, then:

$M\sqsubseteq_{\mathcal{H^{+}}}N\iff\mathcal{D}\models M\sqsubseteq N$

######  Proof 6.9.

$(\Rightarrow)$ This follows directly from Corollary 4.18.

$(\Leftarrow)$ We assume, by the way of contradiction, that
$\mathcal{D}\models M\sqsubseteq N$ but $M\not\sqsubseteq_{\mathcal{H^{+}}}N$.
By the maximality of $\sqsubseteq_{\mathcal{H^{*}}}$ shown in Lemma 2.1 and
the fact that $|M|_{\vec{x}}\subseteq|N|_{\vec{x}}$ we must have
$M\sqsubseteq_{\mathcal{H^{*}}}N$. By Theorem 2.3 there exists a context
$C[-]$ such that $C[M]=_{\beta\eta}{\bf I}$ and $C[N]=_{\mathcal{B}}{\bf
J}_{T}$ for some $T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$. By monotonicity
of the interpretation $|-|$ and since
$\mathcal{B}\eta\subseteq\mathcal{H}^{+}\subseteq\mathrm{Th}(\mathcal{D})$ by
Corollary 4.18, we have $|{\bf I}|=|C[M]|\subseteq|C[N]|=|{\bf J}_{T}|$. We
derive a contradiction by applying Proposition 6.6.

We now show the converse, namely that if a relational graph model is
(inequationally) fully abstract for $\mathcal{H^{+}}$, then it is extensional
and $\lambda$-König.

######  Theorem 6.9.

Let $\mathcal{D}$ be an rgm. If $\mathrm{Th_{\sqsubseteq}}(\mathcal{D})=\
\sqsubseteq_{\mathcal{H^{+}}}$ or $\mathrm{Th}(\mathcal{D})=\mathcal{H^{+}}$
then $\mathcal{D}$ is extensional and $\lambda$-König.

######  Proof 6.10.

Obviously $\mathcal{D}$ must be extensional since $\mathcal{H^{+}}$ is an
extensional $\lambda$-theory. By contradiction, we suppose that it is not
$\lambda$-König. Then there is $T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$
such that $\mathsf{W}_{\mathcal{D}}(T)=\emptyset$ and, by Proposition 6.6, we
get $|{\bf I}|=|{\bf J}_{T}|$. This is impossible since ${\bf
I}\not\sqsubseteq_{\mathcal{H^{+}}}{\bf J}_{T}$.

From Theorem 7 and Theorem 8 we get the main result of this section.

######  Theorem 6.10.

For an rgm $\mathcal{D}$, the following are equivalent:

  1. (i)

$\mathcal{D}$ is extensional and $\lambda$-König,

  2. (ii)

$\mathcal{D}$ is inequationally fully abstract for
$\sqsubseteq_{\mathcal{H^{+}}}$,

  3. (iii)

$\mathcal{D}$ is fully abstract for $\mathcal{H^{+}}$.

In particular, the model $\mathcal{D}_{\star}$ induces the same inequational
and $\lambda$-theories as Coppo, Dezani-Ciancaglini and Zacchi’s filter model
[26], a result first appeared in [67].

######  Corollary 6.11.

The model $\mathcal{D}_{\star}$ of Example 3.3 is inequationally fully
abstract for Morris’s preorder $\sqsubseteq_{\mathcal{H^{+}}}$. In particular
$\mathrm{Th}(\mathcal{D}_{\star})=\mathcal{H^{+}}$.

##  7\. Characterizing Fully Abstract Relational Models of $\mathcal{H^{*}}$

In this section we provide a characterization of those relational graph models
that are (inequationally) fully abstract for $\mathcal{H^{*}}$. At this
purpose, we introduce the notion of _hyperimmune_ relational graph model
(Definition 7.12), which is in some sense dual to the notion of
$\lambda$-König. We prove that a relational graph model $\mathcal{D}$ is
extensional and hyperimmune exactly when the induced inequational theory is
the preorder $\sqsubseteq_{\mathcal{H^{*}}}$ (Theorem 11).

The technique in this section is Böhm-like tree oriented, therefore it is
convenient to fix some notations concerning Böhm-like trees and their
interpretation.

######  Notation 10.

We simply denote by ${\bf J}^{x}_{T}$ the tree $\mathrm{BT}({\bf J}_{T}x)$,
where $x$ is a fresh variable. Given a Böhm-like tree $V$, we write $V^{*}$
for the set $\\{t\in\mathrm{NF}_{\mathtt{\beta\bot}}\ |\ t\leq_{\bot}\\!V\\}$
of its finite approximants and we set $\llbracket
V\rrbracket^{\mathcal{D}}=\bigcup_{t\in V^{*}}\llbracket
t\rrbracket^{\mathcal{D}}$.

###  7.1. Decomposing Infinite $\eta$-Expansions

When considering Böhm trees of $\lambda$-terms, the infinite $\eta$-expansion
$\leq^{\eta}_{\infty}$ can be decomposed into the finitary one
$\,\leq^{\eta}\,$ followed by a more restricted infinite $\eta$-expansion
$\,\leq^{\eta}_{!}$ that only allows to $\eta$-expand variables (Lemma 7.5).

Remember that the difference between $\leq^{\eta}_{\infty}$ and $\leq^{\eta}$
lies in the fact that the former allows countably many possibly infinite
$\eta$-expansions, whereas the latter only countably many finite ones. As
first noticed by Severi and de Vries in their recent work on the infinitary
$\lambda$-calculus [84], in a way this difference only concerns
$\eta$-expansions of variables. Consider for instance
$yy\not\leq^{\eta}\lambda x.y{\bf J}^{y}{\bf J}^{x}$ and
$yy\leq^{\eta}_{\infty}\lambda x.y{\bf J}^{y}{\bf J}^{x}$. The tree $\lambda
x.y{\bf J}^{y}{\bf J}^{x}$ is an infinite $\eta$-expansion of $yy$, which is
not a variable. Nevertheless, one can narrow down to infinite
$\eta$-expansions of the variables $x$ and $y$, by noticing that
$yy\leq^{\eta}\lambda x.yyx\leq^{\eta}_{\infty}\lambda x.y{\bf J}^{y}{\bf
J}^{x}$.

######  Definition 7.1.

Let $\leq^{\eta}_{!}$ be the greatest relation between Böhm-like trees such
that $U\leq^{\eta}_{!}V$ entails that:

  * •

$U=V=\bot$,

  * •

or $U=x$ and $V={\bf J}^{x}_{T}\,$ for $T\in\mathbb{T}^{\infty}_{\textrm{\sf
rec}}$,

  * •

or $U=\lambda x_{1}\dots x_{n}.x_{i}U_{1}\cdots U_{k}$ and $V=\lambda
x_{1}\dots x_{n}.x_{i}V_{1}\cdots V_{k}$ (for some $i,k,n\in{\rm Nature}$)
where $U_{j}\leq^{\eta}_{!}V_{j}$ for all $j\leq k$.

${\bf U}$$\shortparallel$$\lambda
xy.x$$x$$x$$x$$\vdots$$y$$y$$y$$\leq^{\eta}_{!}$${\bf
V}$$\shortparallel$$\lambda xy.x$$x$$x$$x$$\vdots$$\lambda
z_{0}.y$$\lambda z_{1}.z_{0}$$\lambda z_{2}.z_{1}$$\vdots$$\lambda
z_{0}.y$$\lambda z_{1}.z_{0}$$\vdots$$\lambda z_{0}.y$$\vdots$ Figure 5. An
example of infinitely many $\eta!$-reductions.

######  Example 7.2.

We have $\lambda x.yyx\leq^{\eta}_{!}\lambda x.y{\bf J}^{y}{\bf J}^{x}$,
whereas $yy\not\leq^{\eta}_{!}\lambda x.y{\bf J}^{y}{\bf J}^{x}.$

Clearly $\leq^{\eta}_{!}$ is a subrelation of $\leq^{\eta}_{\infty}$, as it is
the case for $\leq^{\eta}$. Also notice that $\leq^{\eta}_{!}$ and
$\leq^{\eta}$ are completely orthogonal relations, in the sense that
$U\\!\leq^{\eta}\\!V$ and $U\\!\leq^{\eta}_{!}\\!V$ imply $U=V$.

For technical reasons we also need an _inductive_ version of the relation
$\leq^{\eta}_{!}$, that we denote by $\\!\,{}_{\eta!}\\!\\!\twoheadleftarrow$.
Intuitively $U\,_{\eta!}\\!\\!\twoheadleftarrow V$ means that $V$ is obtained
from $U$ by performing _finitely_ many infinite $\eta$-expansions of
variables. (The notation $\\!\,{}_{\eta!}\\!\\!\twoheadleftarrow$ is borrowed
from [84], although Severi and de Vrijes use the symbol for a more general
notion of $\eta!$-rule.)

As we will see, actually hyperimmune relational graph models cannot
distinguish between the relation $U\,_{\eta!}\\!\\!\twoheadleftarrow V$ and
its coinductive version $U\leq^{\eta}_{!}V,$ in the sense expressed by the
equivalence (iii$\iff$iv) in Proposition 7.14.

######  Definition 7.3.

Let $\\!\,{}_{\eta!}\\!\\!\twoheadleftarrow\,$ be the smallest relation
between Böhm-like trees closed under the following rules:

  * •

$U\,\,_{\eta!}\\!\\!\twoheadleftarrow U$ for $U\in\mathbb{BT}$,

  * •

$x\,\,_{\eta!}\\!\\!\twoheadleftarrow{\bf J}^{x}_{T}$ for
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$,

  * •

$\lambda x_{1}\dots x_{n}.x_{i}U_{1}\cdots
U_{k}\,\,{}_{\eta!}\\!\\!\twoheadleftarrow\lambda x_{1}\dots
x_{n}.x_{i}V_{1}\cdots V_{k}$ (for some $i,k,n\in{\rm Nature}$) and
$U_{j}\,{}_{\eta!}\\!\\!\twoheadleftarrow\\!V_{j}$ for all $j\leq k$.

Notice that this can be seen as the inductive version of the coinductive
Definition 7.1. Alternatively, one can define
$\twoheadrightarrow_{\mathtt{\eta!}}$ as the transitive-reflexive and
contextual closure of

$(\eta!)\qquad{\bf J}^{x}_{T}\rightarrow_{\mathtt{\eta!}}x\textrm{ \;\;for all
}T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}.$

######  Example 7.4.

Let ${\bf U}=\mathrm{BT}(\lambda xy.{\bf Y}(\lambda u.xyu))$ and ${\bf
V}=\mathrm{BT}(\lambda xy.{\bf Y}(\lambda u.x({\bf J}y)u))$. These two trees
are depicted in Figure 5. We have that ${\bf U}\leq^{\eta}_{!}{\bf V}$ while
${\bf U}\,_{\eta!}\\!\\!\twoheadleftarrow\\!\\!\\!\\!\\!\not\ \ {\bf V}$,
because ${\bf V}$ is obtained from ${\bf U}$ by performing an infinite amount
of $\eta!$-expansions of variables.

######  Lemma 7.5.

(Decomposition of $\leq^{\eta}_{\infty}$) Let $M,N\in\Lambda$. We have
$\mathrm{BT}(M)\leq^{\eta}_{\infty}\mathrm{BT}(N)$ if and only if there exists
a Böhm-like tree $W$ such that
$\mathrm{BT}(M)\leq^{\eta}W\leq^{\eta}_{!}\mathrm{BT}(N).$

######  Proof 7.6.

$(\Leftarrow)$ By transitivity of $\leq^{\eta}_{\infty}$, using the fact that
both $\leq^{\eta}$ and $\leq^{\eta}_{!}$ are contained in
$\leq^{\eta}_{\infty}$.

$(\Rightarrow)$ We construct $W$ coinductively.

In case $M$ and $N$ are unsolvable we just take $W=\bot$.

Otherwise, $M=_{\beta}\lambda\vec{x}.x_{i}M_{1}\cdots M_{k}$ and
$N=_{\beta}\lambda\vec{x}z_{1}\dots z_{m}.x_{i}N_{1}\cdots N_{k}P_{1}\cdots
P_{m}$ where $\mathrm{BT}(M_{j})\leq^{\eta}_{\infty}\mathrm{BT}(N_{j})$ for
all $j\leq k$ and $z_{\ell}\leq^{\eta}_{\infty}\mathrm{BT}(P_{\ell})$ for all
$\ell\leq m$. By the coinductive hypothesis, for all $j$ there exists $W_{j}$
such that
$\mathrm{BT}(M_{j})\leq^{\eta}W_{j}\leq^{\eta}_{!}\mathrm{BT}(N_{j})$. We then
set $W=\lambda\vec{x}z_{1}\dots z_{m}.x_{i}W_{1}\cdots W_{n}z_{1}\cdots
z_{m}.$ Clearly $\mathrm{BT}(M)\leq^{\eta}W$. In order to show that
$W\leq^{\eta}_{!}\mathrm{BT}(N)$ holds we have to prove, for all $\ell\leq m$,
that $\mathrm{BT}(P_{\ell})={\bf J}^{z_{\ell}}_{T_{\ell}}$ for some
$T_{\ell}\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$. Since
$z_{\ell}\leq^{\eta}_{\infty}\mathrm{BT}(P_{\ell})$, we conclude by
Proposition 2.2.

As shown in [84], the decomposition of $\leq^{\eta}_{\infty}$ could be
extended to all Böhm-like trees using possibly non-recursive infinite
$\eta$-expansions of $x$ in the definition of $\leq^{\eta}_{!}$. Since here we
use $\leq^{\eta}_{!}$ in connection with hyperimmune relational graph models
(Proposition 7.14), a semantic notion only concerning recursive trees, it is
crucial to use our restricted version.

######  Lemma 7.7.

Let $U,V$ be two Böhm-like trees such that $U\leq^{\eta}_{!}V$ and let $t\in
U^{*}$. Then there exists a Böhm-like tree $W$ such that
$U\leq^{\eta}_{!}W\,_{\eta!}\\!\\!\twoheadleftarrow V$ and $t\in W^{*}$.

######  Proof 7.8.

We proceed by induction on $t$.

  * •

If $t=\bot$ it suffices to take $W=V$.

  * •

If $t=U=x$ and $V={\bf J}^{x}_{T}$ we get the thesis by taking $W=U$.

  * •

If $t=\lambda\vec{x}.x_{i}t_{1}\cdots t_{k}$, then
$U=\lambda\vec{x}.x_{i}U_{1}\cdots U_{k}$ and
$V=\lambda\vec{x}.x_{i}V_{1}\cdots V_{k}$ where $t_{j}\in U_{j}^{*}$ and
$U_{j}\leq^{\eta}_{!}V_{j}$ for all $j\leq k$. By induction hypothesis for
each $j$ we get some $W_{j}$ such that
$U_{j}\leq^{\eta}_{!}W_{j}\,{}_{\eta!}\\!\\!\twoheadleftarrow V_{j}$ and
$t_{j}\leq_{\bot}\\!W_{j}$. We conclude by setting
$W=\lambda\vec{x}.x_{i}W_{1}\cdots W_{k}$.

######  Example 7.9.

Let ${\bf U},{\bf V}$ be the trees from Example 7.4 (and Figure 5) and let
$t=\lambda xy.xy\bot\in U^{*}$. A possible Böhm-like tree $W$ given by Lemma
7.7 is the following:

$W$$\shortparallel$$\lambda xy.x$$x$$x$$x$$\vdots$$y$$\lambda
z_{1}.y$$\lambda z_{2}.z_{1}$$\vdots$$\lambda z_{1}.y$$\vdots$

######  Lemma 7.10.

Let $U,V$ be two Böhm-like trees such that $U\leq^{\eta}_{\infty}V$ and let
$t\in V^{*}$. Then there exists a Böhm-like tree $W$ such that
$U\leq^{\eta}W\leq^{\eta}_{\infty}V$ and $t\in W^{*}$.

######  Proof 7.11.

We proceed by induction on $t$.

If $t=\bot$ we take $W=U$.

Let $t=\lambda\vec{x}z_{1}\dots z_{m}.x_{i}t_{1}\cdots
t_{k}t^{\prime}_{1}\dots
t^{\prime}_{m}\leq_{\bot}\\!V=\lambda\vec{x}z_{1}\dots z_{m}.x_{i}V_{1}\cdots
V_{k}V^{\prime}_{1}\cdots V^{\prime}_{m}$ and let
$U=\lambda\vec{x}.x_{i}U_{1}\cdots U_{k}$ be such that
$U_{j}\leq^{\eta}_{\infty}V_{j}$ for all $j\leq k$ and
$z_{\ell}\leq^{\eta}_{\infty}V^{\prime}_{\ell}$ for all $\ell\leq m$. For each
$j\leq k$, since $t_{j}\in V_{j}^{*}$, the induction hypothesis gives some
$W_{j}$ satisfying $U_{j}\leq^{\eta}W_{j}\leq^{\eta}_{\infty}V_{j}$ and
$t_{j}\in W^{*}_{j}$. We conclude by setting $W=\lambda\vec{x}z_{1}\dots
z_{m}.x_{i}W_{1}\cdots W_{k}z_{1}\dots z_{m}$.

###  7.2. Hyperimmune Relational Graph Models

In Section 6 we exploited the Morris Separation (Theorem 2.3) to reduce the
problem of being fully abstract for $\mathcal{H^{+}}$ to the property
$\llbracket x\rrbracket\neq\llbracket{\bf J}_{T}x\rrbracket$, namely
$\mathsf{W}_{\mathcal{D}}(T)=\llbracket x\rrbracket-\llbracket{\bf
J}_{T}x\rrbracket\not=\emptyset$, for every tree
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$. The notion of $\lambda$-König
relational graph model provided that. Here there is a similar phenomenon: we
exploit the decomposition seen above (Lemma 7.5) to reduce the full
abstraction for $\mathcal{H^{*}}$ to the property $\llbracket
x\rrbracket=\llbracket{\bf J}_{T}x\rrbracket$, namely
$\mathsf{W}_{\mathcal{D}}(T)=\llbracket x\rrbracket-\llbracket{\bf
J}_{T}x\rrbracket=\emptyset$, for every $T\in\mathbb{T}^{\infty}_{\textrm{\sf
rec}}$. This is the intuition behind the following definition, which is some
kind of dual of $\lambda$-König.

######  Definition 7.12 (Hyperimmune models).

An rgm $\mathcal{D}$ is _hyperimmune_ if for every
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$
$\mathsf{W}_{\mathcal{D}}(T)=\emptyset$.

The name refers to a standard concept in computability theory: a function
$f:{\rm Nature}\to{\rm Nature}$ is called _hyperimmune_ if it is not bounded
(upwardly) by any recursive function. One can prove that a relational graph
model $\mathcal{D}$ is hyperimmune exactly when it only admits witnesses that
follow hyperimmune functions. This observation justifies the choice of the
terminology. The notion of hyperimmunity first appeared in these terms in [16]
for Krivine’s models.

######  Example 7.13.

The model $\mathcal{D}_{\omega}$ of Example 3.3 is hyperimmune. As a matter of
fact, since the model is freely generated by the equation
$\star=\omega\to\star$, it is easy to verify that no element of
$\mathcal{D}_{\omega}$ can be a witness for any
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$ following any infinite path $f$.

In the hypothesis of extensionality, this notion admits some additional
characterizations.

######  Proposition 7.14.

Let $\mathcal{D}$ be an extensional rgm. The following statements are
equivalent:

  1. (i)

$\mathcal{D}$ is hyperimmune,

  2. (ii)

$\llbracket x\rrbracket\subseteq\llbracket{\bf J}_{T}x\rrbracket$ for all
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}},$

  3. (iii)

$U\,_{\eta!}\\!\\!\twoheadleftarrow V$ implies $\llbracket
U\rrbracket\subseteq\llbracket V\rrbracket$ for all Böhm-like trees $U,V,$

  4. (iv)

$U\leq^{\eta}_{!}V$ implies $\llbracket U\rrbracket\subseteq\llbracket
V\rrbracket$ for all Böhm-like trees $U,V.$

######  Proof 7.15.

(i $\iff$ ii) By Proposition 6.6 and Corollary 4.4 an extensional rgm
$\mathcal{D}$ is hyperimmune if and only if, for all
$T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$, we have that $\llbracket
x\rrbracket-\llbracket{\bf J}_{T}x\rrbracket=\\{\alpha\in D\ |\
x:[\alpha]\not\vdash{\bf
J}_{T}x:\alpha\\}=\mathsf{W}_{\mathcal{D}}(T)=\emptyset$. This is equivalent
to requiring that $\llbracket x\rrbracket\subseteq\llbracket{\bf
J}_{T}x\rrbracket$ for all $T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}$.

(ii $\Rightarrow$ iii) By a straightforward induction on the derivation of
$U\,_{\eta!}\\!\\!\twoheadleftarrow V$.

(iii $\Rightarrow$ ii) Trivial, as $x\,_{\eta!}\\!\\!\twoheadleftarrow{{\bf
J}_{T}x}$.

(iii $\Rightarrow$ iv) Suppose that there exist two Böhm-like trees $U,V$ such
that $U\leq^{\eta}_{!}V$ and $\llbracket U\rrbracket\not\subseteq\llbracket
V\rrbracket$. Since $\llbracket U\rrbracket=\bigcup_{t\in U^{*}}\llbracket
t\rrbracket$, there is a $t\in U^{*}$ such that $\llbracket
t\rrbracket\not\subseteq\llbracket V\rrbracket$. By Lemma 7.7 there exists
$W\,_{\eta!}\\!\\!\twoheadleftarrow V$ such that $t\in W^{*}$. Since
$\llbracket W\rrbracket=\bigcup_{t\in{W}^{*}}\llbracket t\rrbracket$, we get
$\llbracket W\rrbracket\not\subseteq\llbracket V\rrbracket$, whereas
$\llbracket W\rrbracket\subseteq\llbracket V\rrbracket$ by (iii).

(iv $\Rightarrow$ iii) Trivial, since the relation
$\,{}_{\eta!}\\!\\!\twoheadleftarrow\,$ is included in $\leq^{\eta}_{!}$.

######  Lemma 7.16.

Let $\mathcal{D}$ be an extensional rgm and let $U,V$ be two Böhm-like trees.
We have that $U\leq^{\eta}_{\infty}V$ implies $\llbracket
V\rrbracket\subseteq\llbracket U\rrbracket$.

######  Proof 7.17.

By Lemma 7.10, if $t\in V^{*}$ then $t\in W^{*}$ for some $U\leq^{\eta}W$. So
$\llbracket t\rrbracket\subseteq\llbracket W\rrbracket=\llbracket
U\rrbracket$, where the equality holds by extensionality. Since $\llbracket
V\rrbracket=\bigcup_{t\in V^{*}}\llbracket t\rrbracket$, we get $\llbracket
V\rrbracket\subseteq\llbracket U\rrbracket$.

In general, the hypothesis $U\leq^{\eta}_{\infty}V$ does not imply $\llbracket
U\rrbracket\subseteq\llbracket V\rrbracket$, even in presence of
extensionality. This implication only holds when the model is in addition
hyperimmune.

######  Lemma 7.18.

Let $\mathcal{D}$ be an extensional and hyperimmune rgm and let
$M,N\in\Lambda$. Then $\,\mathrm{BT}(M)\leq^{\eta}_{\infty}\mathrm{BT}(N)$
implies $\llbracket M\rrbracket\subseteq\llbracket N\rrbracket$.

######  Proof 7.19.

By Lemma 7.5 there exists a Böhm-like tree $W$ such that
$\mathrm{BT}(M)\leq^{\eta}W\leq^{\eta}_{!}\mathrm{BT}(N)$. Then we have
$\llbracket\mathrm{BT}(M)\rrbracket\subseteq\llbracket W\rrbracket$ by
extensionality and $\llbracket
W\rrbracket\subseteq\llbracket\mathrm{BT}(N)\rrbracket$ by the
characterization (iv) of hyperimmunity provided by Proposition 7.14. By
transitivity we obtain
$\llbracket\mathrm{BT}(M)\rrbracket\subseteq\llbracket\mathrm{BT}(N)\rrbracket$,
so we conclude $\llbracket M\rrbracket\subseteq\llbracket N\rrbracket$ by
Theorem 3.

The following theorem constitutes the main result of the section. It is
actually an adaptation to relational graph models of the characterization of
fully abstract Krivine’s models provided in [16, 17].

######  Theorem 7.19.

Let $\mathcal{D}$ be an rgm. The following statements are equivalent:

  1. (i)

$\mathcal{D}$ is extensional and hyperimmune,

  2. (ii)

$\mathcal{D}$ is inequationally fully abstract for
$\sqsubseteq_{\mathcal{H^{*}}}$,

  3. (iii)

$\mathcal{D}$ is fully abstract for $\mathcal{H^{*}}$.

######  Proof 7.20.

(i $\Rightarrow$ ii) We must prove that $M\sqsubseteq_{\mathcal{H^{*}}}\\!N$
if and only if $\llbracket M\rrbracket\subseteq\llbracket N\rrbracket$. The
right-to-left implication is true for all rgm’s, since they are sensible
(Corollary 4.16) and $\sqsubseteq_{\mathcal{H^{*}}}$ is the maximal sensible
inequational theory. Let us prove the left-to-right implication.

By Theorem 2 the hypothesis $M\sqsubseteq_{\mathcal{H^{*}}}\\!N$ means that
$\mathrm{BT}(M)\leq^{\eta}_{\infty}U\leq_{\bot}\\!V\geq^{\eta}_{\infty}\mathrm{BT}(N)$
for some Böhm-like trees $U$ and $V$. In particular $U$ can be taken of the
form $U=\mathrm{BT}(P)$ for some $P\in\Lambda$ (see [7, Ex. 10.6.7]). Then we
have

$\begin{array}[]{lcl@{\hspace{2cm}}r}\llbracket
M\rrbracket&\subseteq&\llbracket P\rrbracket\hfil\hskip 56.9055pt&\text{by
Lemma~{}\ref{lem:yeppa!hyper!} }\\\ &=&\llbracket U\rrbracket\hfil\hskip
56.9055pt&\text{by Theorem~{}\ref{thm:app} }\\\ &\subseteq&\llbracket
V\rrbracket\hfil\hskip 56.9055pt&\text{by def. \\!of $\llbracket-\rrbracket$
for B\"{o}hm-like trees }\\\
&\subseteq&\llbracket\mathrm{BT}(N)\rrbracket\hfil\hskip 56.9055pt&\text{by
Lemma~{}\ref{lem:yeppa!} }\\\ &=&\llbracket N\rrbracket\hfil\hskip
56.9055pt&\text{by Theorem~{}\ref{thm:app}.}\end{array}$

(ii $\Rightarrow$ iii) Trivial.

(iii $\Rightarrow$ i) The theory $\mathcal{H^{*}}$ is extensional, so that is
the case for any fully abstract rgm. Moreover, the theory $\mathcal{H^{*}}$
satisfies $x\sqsubseteq_{\mathcal{H^{*}}}\\!{{\bf J}_{T}x}\,$ for all
$\,T\in\mathbb{T}^{\infty}_{\textrm{\sf rec}}\,.$ So the model is hyperimmune
by the characterization (ii) of hyperimmunity provided by Proposition 7.14.

As a consequence, we get that the model $\mathcal{D}_{\omega}$ has the same
inequational and $\lambda$-theories as Scott’s $\mathcal{D}_{\infty}$ [81],
namely it is fully abstract for $\mathcal{H^{*}}$. Such a result first
appeared in [65].

######  Corollary 7.21.

The model $\mathcal{D}_{\omega}$ of Example 3.3 is inequationally fully
abstract for $\sqsubseteq_{\mathcal{H^{*}}}$. In particular
$\mathrm{Th}(\mathcal{D}_{\omega})=\mathcal{H^{*}}$.

##  8\. Conclusions

We have studied the class of the relational graph models living inside the
relational semantics of $\lambda$-calculus, and proved that they all enjoy the
Approximation Theorem. We exhibited a model inducing the minimum relational
(in)equational graph theory, and provided sufficient and necessary conditions
for a relational graph model to be fully abstract for $\mathcal{H^{+}}$ (resp.
$\mathcal{H^{*}}$). Actually such characterizations of full abstraction hold
more generally for all relational models, since these theories are extensional
and the class of extensional relational graph models coincide with the class
of extensional reflexive objects in MRel.

We conclude presenting some open problems that we consider interesting.

######  Problem 8.1.

It is well known that the $\lambda$-theory $\mathcal{H^{*}}$ satisfies the
$\omega$-rule [7, Def. 4.1.10], and the analogous result was recently proved
for $\mathcal{H^{+}}$ in [18]. Does every extensional graph model satisfy the
$\omega$-rule?

######  Problem 8.2.

Are all $\lambda$-theories in the interval $[\mathcal{H^{+}},\mathcal{H^{*}}]$
relational graph theories? If it is not the case, is it possible to provide a
characterization of the representable ones?

Acknowledgements. We would like to thank Henk Barendregt, Mariangiola Dezani,
Thomas Ehrhard, Jean-Jacques Lévy, Michele Pagani, Andrew Polonsky and Simona
Ronchi Della Rocca for many interesting discussions on relational models and
the $\lambda$-theory $\mathcal{H^{+}}$. We also wish to thank the anonymous
reviewers for their valuable comments and suggestions to improve the quality
of the paper.

## References

  * [1] A. Abel, B. Pientka, D. Thibodeau, and A. Setzer.  Copatterns: programming infinite structures by observations.  In R. Giacobazzi and R. Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, pages 27–38. ACM, 2013.
  * [2] S. Abramsky.  Domain theory in logical form.  Ann. Pure Appl. Logic, 51(1-2):1–77, 1991.
  * [3] R. Amadio and P.-L. Curien.  Domains and Lambda Calculi.  Cambridge tracts in theoretical computer science. Cambridge University Press, 1998.
  * [4] F. Aschieri and M. Zorzi.  Non-determinism, non-termination and the strong normalization of system T.  In M. Hasegawa, editor, Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013. Proceedings, volume 7941 of Lecture Notes in Computer Science, pages 31–47. Springer, 2013.
  * [5] A. Asperti and G. Longo.  Categories, types and structures: an introduction to category theory for the working computer scientist.  MIT Press, Cambridge, MA, 1991.
  * [6] H.P. Barendregt.  The type free lambda calculus.  In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 1091–1132. North-Holland, Amsterdam, 1977.
  * [7] H.P. Barendregt.  The lambda-calculus, its syntax and semantics.  Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1984.
  * [8] H.P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini.  A filter lambda model and the completeness of type assignment.  Journal of Symbolic Logic, 48:931–940, 1983.
  * [9] H.P. Barendregt, W. Dekkers, and R. Statman.  Lambda Calculus with Types.  Perspectives in logic. Cambridge University Press, 2013.
  * [10] C. Berline.  From computation to foundations via functions and application: The $\lambda$-calculus and its webbed models.  Theoretical Computer Science, 249(1):81–161, 2000.
  * [11] C. Berline, G. Manzonetto, and A. Salibra.  Effective lambda-models versus recursively enumerable lambda-theories.  Mathematical Structures in Computer Science, 19(5):897–942, 2009\.
  * [12] G. Berry.  Stable models of typed lambda-calculi.  In Proceedings of the Fifth Colloquium on Automata, Languages and Programming, volume 62 of LNCS, Berlin, 1978. Springer-Verlag.
  * [13] G. Bierman.  What is a categorical model of Linear Logic?  In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications ’95, volume 902 of Lecture Notes in Computer Science. Springer, April 1995.
  * [14] C. Böhm.  Alcune proprietà delle forme $\beta$-$\eta$-normali nel $\lambda$-$K$-calcolo.  INAC, 696:1–19, 1968.
  * [15] F. Breuvart.  The resource lambda calculus is short-sighted in its relational model.  In M. Hasegawa, editor, Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013. Proceedings, volume 7941 of Lecture Notes in Computer Science, pages 93–108. Springer, 2013.
  * [16] F. Breuvart.  On the characterization of models of $\mathcal{H}^{*}$.  In T. A. Henzinger and D. Miller, editors, Joint Meeting of the 23 EACSL Annual Conference on Computer Science Logic (CSL) and the 29 Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 24:1–24:10. ACM, 2014.
  * [17] F. Breuvart.  On the characterization of models of $\mathcal{H}^{*}$: the semantical aspect.  Logical Methods in Computer Science, 12(2), 2016.
  * [18] F. Breuvart, G. Manzonetto, A. Polonsky, and D. Ruoppolo.  New results on Morris’s observational theory.  In D. Kesner and B. Pientka, editors, Formal Structures for Computation and Deduction, volume 52 of LIPIcs, pages 15:1–15:18. Schloss Dagstuhl, 2016.
  * [19] A. Bucciarelli and T. Ehrhard.  Sequentiality and strong stability.  In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 138–145. IEEE Computer Society Press, 1991.
  * [20] A. Bucciarelli, T. Ehrhard, and G. Manzonetto.  Not enough points is enough.  In J. Duparc and T. A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007. Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 298–312. Springer, 2007.
  * [21] A. Bucciarelli, T. Ehrhard, and G. Manzonetto.  A relational semantics for parallelism and non-determinism in a functional setting.  Ann. Pure Appl. Logic, 163(7):918–934, 2012.
  * [22] A. Bucciarelli and A. Salibra.  Graph lambda theories.  Mathematical Structures in Computer Science, 18(5):975–1004, 2008\.
  * [23] A. Carraro, T. Ehrhard, and A. Salibra.  Exponentials with infinite multiplicities.  In A. Dawar and H. Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 170–184. Springer, 2010.
  * [24] A. Carraro and G. Guerrieri.  A semantical and operational account of call-by-value solvability.  In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 103–118. Springer, 2014.
  * [25] A. Church.  The calculi of lambda conversion.  Princeton Univ. Press, 1941.
  * [26] M. Coppo, M. Dezani, and M. Zacchi.  Type theories, normal forms and $\mathcal{D}_{\infty}$-lambda-models.  Inf. Comput., 72(2):85–116, 1987.
  * [27] M. Coppo, M. Dezani-Ciancaglini, F. Honsell, and G. Longo.  Extended type structures and filter lambda models.  In G. Longo G. Lolli and A. Marcja, editors, Logic Colloquium ’82, volume 112 of Studies in Logic and the Foundations of Mathematics, pages 241 – 262. Elsevier, 1984.
  * [28] M. Coppo, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca.  (Semi)-separability of finite sets of terms in Scott’s $\mathcal{D}_{\infty}$-models of the lambda-calculus.  In G. Ausiello and C. Böhm, editors, Automata, Languages and Programming, volume 62 of Lecture Notes in Computer Science, pages 142–164. Springer, 1978.
  * [29] D. de Carvalho.  Sémantiques de la logique linéaire et temps de calcul.  PhD thesis, Université Aix-Marseille II, 2007.  Thèse de Doctorat.
  * [30] D. de Carvalho.  Execution time of $\lambda$-terms via denotational semantics and intersection types.  Draft available at http://arxiv.org/abs/0905.4251, 2009.
  * [31] D. de Carvalho, M. Pagani, and L. Tortora de Falco.  A semantic measure of the execution time in linear logic.  Th. Comp. Sci., 412(20):1884–1902, 2011.
  * [32] U. de’Liguoro and A. Piperno.  Non deterministic extensions of untyped lambda-calculus.  Inf. Comput., 122(2):149–177, 1995.
  * [33] M. Dezani-Ciancaglini, U. de’Liguoro, and A. Piperno.  A filter model for concurrent lambda-calculus.  SIAM J. Comput., 27(5):1376–1419, 1998.
  * [34] A. Díaz-Caro, G. Manzonetto, and M. Pagani.  Call-by-value non-determinism in a linear logic type discipline.  In S. N. Artëmov and A. Nerode, editors, Logical Foundations of Computer Science, LFCS. Proceedings, volume 7734 of Lecture Notes in Computer Science, pages 164–178. Springer, 2013.
  * [35] T. Ehrhard.  Collapsing non-idempotent intersection types.  In P. Cégielski and A. Durand, editors, Computer Science Logic (CSL’12), 21st Annual Conference of the EACSL, CSL 2012, volume 16 of LIPIcs, pages 259–273. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012.
  * [36] T. Ehrhard and G. Guerrieri.  The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value.  In J. Cheney and G. Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pages 174–187. ACM, 2016.
  * [37] T. Ehrhard and L. Regnier.  The differential $\lambda$-calculus.  Th. Comp. Sci., 309(1):1–41, 2003.
  * [38] T. Ehrhard and L. Regnier.  Böhm trees, Krivine’s machine and the Taylor expansion of lambda-terms.  In CiE, volume 3988 of Lecture Notes in Computer Science, pages 186–197, 2006.
  * [39] E. Engeler.  Algebras and combinators.  Algebra Universalis, 13(3):389–392, 1981.
  * [40] M. Fiore, N. Gambino, M. Hyland, and G. Winskel.  The cartesian closed bicategory of generalised species of structures.  Journal of the London Mathematical Society, 77(1):203, 2008.
  * [41] P. Di Gianantonio, G. Franco, and F. Honsell.  Game semantics for untyped $\lambda\beta\eta$-calculus.  In TLCA’99, volume 1581 of Lecture Notes in Computer Science, pages 114–128. Springer, 1999.
  * [42] J.-Y. Girard.  Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur.  Thèse de doctorat, Université Paris 7, 1972.
  * [43] J.-Y. Girard.  Normal functors, power series and $\lambda$-calculus.  Ann. of Pure and App. Logic, 37(2):129–177, 1988.
  * [44] X. Gouy.  Étude des théories équationnelles et des propriétés algébriques des modèles stables du $\lambda$-calcul.  Thèse de doctorat, Université de Paris 7, 1995.
  * [45] F. Honsell and S. Ronchi Della Rocca.  An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus.  J. of Computer and System Sciences, 45:49–75, 1992.
  * [46] J.M.E. Hyland.  A survey of some useful partial order relations on terms of the $\lambda$-calculus.  In Lambda-Calculus and Comp. Sci. Th., volume 37 of Lecture Notes in Computer Science, pages 83–95. Springer, 1975.
  * [47] J.M.E. Hyland.  A syntactic characterization of the equality in some models for the $\lambda$-calculus.  J. London Math. Soc. (2), 12(3):361–370, 1976.
  * [48] J.M.E. Hyland.  Some reasons for generalising domain theory.  Mathematical Structures in Computer Science, 20(2):239–265, 2010\.
  * [49] J.M.E. Hyland, M. Nagayama, J. Power, and G. Rosolini.  A category theoretic formulation for Engeler-style models of the untyped $\lambda$-calculus.  Electr. Notes in TCS, 161:43–57, 2006.
  * [50] B. Intrigila, G. Manzonetto, and A. Polonsky.  Degrees of extensionality in the theory of Böhm trees and Sallé’s conjecture.  Submitted. CoRR abs/1802.07320.
  * [51] B. Intrigila, G. Manzonetto, and A. Polonsky.  Refutation of Sallé’s longstanding conjecture.  In D. Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, volume 84 of LIPIcs, pages 20:1–20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
  * [52] B. Jacobs and J. Rutten.  A tutorial on (co)algebras and (co)induction.  EATCS Bulletin, 62:62–222, 1997.
  * [53] S. C. Kleene.  $\lambda$-definability and recursiveness.  Duke Math. J., 2(2):340–353, 06 1936.
  * [54] C.P.J. Koymans.  Models of the lambda calculus.  Information and Control, 52(3):306–332, 1982.
  * [55] D. Kozen and A. Silva.  Practical coinduction.  Mathematical Structures in Computer Science, 27(7):1132–1152, 2017\.
  * [56] J.-L. Krivine.  Lambda-calculus, types and models.  Ellis Horwood, New York, 1993.  Translated from the ed. Masson, 1990, French original.
  * [57] J.-L. Krivine.  Realizability in classical logic.  In P.-L. Curien, H. Herbelin, J.-L. Krivine, and P.-A. Melliès, editors, Interactive models of computation and program behaviour, number 27 in Panoramas et synthèses. Société Mathématique de France, 2009\.
  * [58] J. Laird, G. Manzonetto, G. McCusker, and M. Pagani.  Weighted relational models of typed lambda-calculi.  In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pages 301–310. IEEE Computer Society, 2013.
  * [59] S. Lassen.  Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context.  Electr. Notes Theor. Comput. Sci., 20:346–374, 1999.
  * [60] J.-J. Lévy.  Le lambda calcul - notes du cours, 2005.  In French.
http://pauillac.inria.fr/~levy/courses/X/M1/lambda/dea-spp/jjl.pdf.

  * [61] P. B. Levy.  Call-by-push-value: Decomposing call-by-value and call-by-name.  Higher-Order and Symbolic Computation, 19(4):377–414, 2006.
  * [62] G. Longo.  Set-theoretical models of $\lambda$-calculus: theories, expansions, isomorphisms.  Ann. Pure Appl. Logic, 24(2):153–188, 1983.
  * [63] S. Lusin and A. Salibra.  The lattice of $\lambda$-theories.  J. Log. Comput., 14(3):373–394, 2004.
  * [64] G. Manzonetto.  Models and theories of lambda calculus.  Thèse de doctorat, Univ. Ca’Foscari (Venice) and Univ. Paris Diderot (Paris 7), 2008.
  * [65] G. Manzonetto.  A general class of models of $\mathcal{H}^{\star}$.  In Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009. Proceedings, volume 5734 of Lecture Notes in Computer Science, pages 574–586. Springer, 2009.
  * [66] G. Manzonetto.  What is a categorical model of the differential and the resource $\lambda$-calculi?  Mathematical Structures in Computer Science, 22(3):451–520, 2012\.
  * [67] G. Manzonetto and D. Ruoppolo.  Relational graph models, Taylor expansion and extensionality.  Electr. Notes Theor. Comput. Sci., 308:245–272, 2014.
  * [68] G. Manzonetto and A. Salibra.  Boolean algebras for lambda calculus.  In 21th IEEE Symposium on Logic in Computer Science (LICS 2006). Proceedings, pages 317–326. IEEE Computer Society, 2006.
  * [69] J.H. Morris.  Lambda calculus models of programming languages.  Phd, MIT, 1968.
  * [70] M. Pagani and S. Ronchi Della Rocca.  Linearity, non-determinism and solvability.  Fundam. Inform., 103(1-4):173–202, 2010.
  * [71] L. Paolini.  Parametric $\lambda$-theories.  Theoretical Computer Science, 398(1):51 – 62, 2008.
  * [72] L. Paolini, M. Piccolo, and S. Ronchi Della Rocca.  Essential and relational models.  Mathematical Structures in Computer Science, 27(5):626–650, 2017\.
  * [73] G.D. Plotkin.  A set-theoretical definition of application.  Technical Report MIP-R-95, School of artificial intelligence, 1971.
  * [74] G.D. Plotkin.  Set-theoretical and other elementary models of the $\lambda$-calculus.  Theoretical Computer Science, 121(1):351 – 409, 1993.
  * [75] J.C. Reynolds.  Types, abstraction and parametric polymorphism.  In IFIP Congress, pages 513–523, 1983.
  * [76] S. Ronchi Della Rocca.  Characterization theorems for a filter lambda model.  Information and Control, 54(3):201–216, 1982.
  * [77] S. Ronchi Della Rocca and L. Paolini.  The Parametric Lambda Calculus - A Metamodel for Computation.  Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004\.
  * [78] D. Ruoppolo.  Relational Graph Models and Morris’s Observability: resource-sensitive semantic investigations on the untyped $\lambda$-calculus.  Thése de doctorat, Université Paris 13, 2016.
  * [79] A. Salibra.  Nonmodularity results for lambda calculus.  Fundam. Inform., 45(4):379–392, 2001.
  * [80] S. Salvati, G. Manzonetto, M. Gehrke, and H. Barendregt.  Loader and Urzyczyn are logically related.  In A. Czumaj, K. Mehlhorn, A.M. Pitts, and R. Wattenhofer, editors, Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012. Proceedings, Part II, volume 7392 of Lecture Notes in Computer Science, pages 364–376. Springer, 2012.
  * [81] D. Scott.  Continuous lattices.  In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Math., pages 97–136. Springer, 1972.
  * [82] D.S. Scott.  Data types as lattices.  SIAM J. Comput., 5(3):522–587, 1976.
  * [83] P. Selinger.  The lambda calculus is algebraic.  J. Funct. Program., 12(6):549–566, 2002.
  * [84] P. Severi and F.-J. de Vries.  The infinitary lambda calculus of the infinite eta Böhm trees.  Mathematical Structures in Computer Science, 27(5):681–733, 2017\.
  * [85] W. Tait.  Intensional interpretations of functionals of finite type I.  J. Symb. Log., 32(2):198–212, 1967.
  * [86] P. Tranquilli.  Nets between Determinism and Nondeterminism.  Ph.D. thesis, Università Roma Tre/Université Paris Diderot (Paris 7), April 2009.
  * [87] A. M. Turing.  Computability and $\lambda$-definability.  J. Symb. Log., 2(4):153–163, 1937.
  * [88] C.P. Wadsworth.  The relation between computational and denotational properties for Scott’s $\mathscr{D}_{\infty}$-models of the lambda-calculus.  SIAM J. Comput., 5(3):488–521, 1976.
  * [89] C.P. Wadsworth.  Approximate reduction and lambda calculus models.  SIAM J. Comput., 7(3):337–356, 1978.


_The General Data Protection Regulation: An Opportunity for the CHI Community?
(CHI-GDPR 2018)_ , Workshop at ACM CHI’18, 22 April 2018, Montréal, Canada

# Some HCI Priorities for GDPR-Compliant Machine Learning

Michael Veale

Reuben Binns
Max Van Kleek

University College London  London, United Kingdom<EMAIL_ADDRESS>University of Oxford  Oxford, United Kingdom<EMAIL_ADDRESS>
<EMAIL_ADDRESS>
###### Abstract

In this short paper, we consider the roles of HCI in enabling the better
governance of consequential machine learning systems using the rights and
obligations laid out in the recent 2016 EU General Data Protection Regulation
(GDPR)—a law which involves heavy interaction with people and systems.
Focussing on those areas that relate to algorithmic systems in society, we
propose roles for HCI in legal contexts in relation to fairness, bias and
discrimination; data protection by design; data protection impact assessments;
transparency and explanations; the mitigation and understanding of automation
bias; and the communication of envisaged consequences of processing.

##  1 Introduction

The 2016 EU General Data Protection Regulation (GDPR) is making waves. With
all personal data relating to EU residents or processed by EU companies within
scope, it seeks to strengthen the rights of data subjects and the obligations
of data controllers (see definitions in the box overleaf) in an increasingly
data-laden society, newly underpinned with an overarching obligation of data
controller accountability as well as hefty maximum fines. Its articles
introduce new provisions and formalise existing rights clarified by the
European Court of Justice (the Court), such as the “right to be forgotten”, as
well as strengthening those already present in the 1995 Data Protection
Directive (DPD).

The GDPR has been turned to by scholars and activists as a tool for
“algorithmic accountability” in a society where machine learning (ML) seems to
be increasingly important. Machine learning models—statistical systems which
use data to improve their performance on particular tasks—are the approach of
choice to generate value from the ‘data exhaust’ of digitised human
activities. Critics, however, have framed ML as powerful, opaque, and with
potential to endanger privacy [3], equality [11] and autonomy [21]. While the
GDPR is intended to govern personal data rather than ML, there are a range of
included rights and obligations which might be useful to exert control over
algorithmic systems [15].

††margin:  Data Subjects & Controllers EU DP law applies whenever personal
data is processed either in the Union, or outside the Union relating to an EU
resident. Personal data is defined by how much it can render somebody
identifiable—going beyond email, phone number, etc to include dynamic IP
addresses, browser fingerprints or smart meter readings. The individual data
relates to is called the data subject. The organisation(s) who determine ‘the
purposes and means of the processing of personal data’ are data controllers.
Data subjects have rights over personal data, such as rights of access,
erasure, objection to processing, and portability of data elsewhere. Data
controllers are subject to a range of obligations, such as ensuring
confidentiality, notifying if data is breached, and undertaking risk
assessments. Additionally, they must only process data where they have a legal
ground—such as consent—to do so, for a specified and limited purpose, and a
limited period of storage.

Given that GDPR rights involve both individual data-subjects and data
controllers (see sidebar) interfacing with computers in a wide variety of
contexts, it strongly implicates another abbreviation readers will likely find
familiar: Human–Computer Interaction (HCI). In this short paper, we outline,
non-exhaustively of course, some of the crossovers between the GDPR
provisions, HCI and ML that appear most salient and pressing given current
legal, social, and technical debates. We group these in two broad categories:
those which primarily concern the building and training of models _before
deployment_ , and those which primarily concern the _post-deployment
application_ of models to data subjects in particular situations.

##  2 HCI, GDPR and Model Training

An increasing proportion of collected personal data111Note that the GDPR
defines personal data broadly—including things like dynamic IP addresses and
home energy data—as opposed to the predominantly American notion of personally
identifiable information (PII) [26]. is used to train machine learning
systems, which are in turn used to make or support decisions in a variety of
fields. As model training with personal data is considered data processing
(assuming data is not solidly ‘anonymised’), the GDPR does govern it to a
varying degree. In this section, we consider to what extent HCI might play a
role in promoting the governance of model training under the GDPR.

###  2.1 Fairness, discrimination and ‘special category’ data

Interest in unfair and/or illegal data-driven discrimination has concerned
researchers, journalists, pundits and policy-makers [18, 4], particularly as
the ease of transforming seemingly non-sensitive data into potentially
damaging, private insights has become clear [10]. Most focus on how to govern
data (both in Europe and elsewhere broadly [20]) has been centred on data
protection, which is not an anti-discrimination law and does not feature anti-
discrimination as a core concept. Yet the GDPR does contain provisions which
concern particularly sensitive attributes of data.

Several “special” types of data are given higher protection in the GDPR. The
1995 Data Protection Directive (art 8) prohibits processing of data
_revealing_ racial or ethnic origin, political opinions, religious or
philosophical beliefs and trade-union membership, in addition to data
concerning health or sex life. The GDPR (art 9(1)) adds genetic and biometric
data (the latter for the purposes of identification), as well as clarifying
sex life includes orientation, to create 8 ‘special categories’ of data. This
list is similar, but not identical, to the ‘protected characteristics’ in many
international anti-discrimination laws. Compared to the UK’s Equality Act
2010, the GDPR omits age, sex and marital status but includes political
opinions, trade union membership, and health data more broadly.

The collection, inference and processing of special category data triggers
both specific provisions (e.g. arts 9, 22) and specific responsibilities (e.g.
Data Protection Impact Assessments, art 35 and below), as well as generally
heightening the level of risk of processing and therefore the general
responsibilities of a controller (art 24). Perhaps the most important
difference is that data controllers cannot rely on their own _legitimate
interests_ to justify the processing of special category data, which usually
will mean they will have to seek explicit, specified consent for the type of
processing they intend—which they may not have done for their original data,
and may not be built into their legal data collection model.

Given that inferred special category data is also characterised as special
category data [29], there are important questions around how both controllers
and regulators recognise that such inference is or might be happening.
Naturally, if a data controller trains a supervised model for the purpose of
inferring a special category of data, this is quite a simple task (as long as
they are honest about it). Yet when they are using latent characteristics,
such as through principal components analysis, or features that are embedded
within a machine learning model, this becomes more challenging. In particular
it has been repeatedly demonstrated that biases connected to special category
data can appear in trained systems even where those special categories are not
present in the datasets being used [10].

The difficulty of this task is heightened by how the controller is unlikely to
possess ‘ground truth’ special category data in order to assess what it is
they are picking up. HCI might play an important role here in establishing
what has been described as ‘exploratory fairness analysis’ [28]. The task is
to understand potential patterns of discrimination, or to identify certain
unexpected but sensitive clusters, with only partial additional information
abut the participants. A similar proposal (and prototype of) a visual system,
albeit one assuming full information, has been proposed by discrimination-
aware data mining researchers concerned that the formal statistical criteria
for non-discrimination established by researchers may not connect with ideas
of fairness in practice [5, 6]. If we do indeed also know unfairness when we
see it, exploratory visual analysis may be a useful tool. A linked set of
discussions have been occurring in the information visualisation community
around desirable characteristics of feminist data visualisation, which
connects feminist principles around marginalisation and dominance in the
production of knowledge to information design [12]. Finally, visual tools
which help identify misleading patterns in data, such as instances of
Simpson’s paradox (e.g. [25]), may prove useful in confirming apparent
disparities between groups. Building and testing interfaces which help
identify sensitive potential correlations and ask critical questions around
bias and discrimination in the data is an important prerequisite to rigorously
meeting requirements in the GDPR.

###  2.2 Upstream provisions: Data Protection by Design (DPbD) and Data
Protection Impact Assessments (DPIAs)

The GDPR contains several provisions intended to move considerations of risks
to data subjects’ rights and freedoms upstream into the hands of designers.
Data Protection by Design (DPbD), a close cousin of privacy by design, is a
requirement under the GDPR and means that controllers should use
organisational and technical measures to imbue their products and processes
with data protection principles [9]. Data Protection Impact Assessments
(DPIAs) have a similar motivation [7]. Whenever controllers have reason to
believe that a processing activity brings high risks, they must undertake
continuous, documented analysis of these, as well as any measures they are
taking to mitigate.

The holistic nature of both DPbD and DPIAs is emphasised in both the legal
text and recent guidance. These are creative processes mixing anticipation and
foresight with best practice and documentation. Some HCI research has already
addressed this in particular. Luger et al. [24] use ideation cards to engage
designers with regulation and co-produce “data protection heuristics”.222The
cards are downloadable at https://perma.cc/3VBQ-VVPQ. Whether DPIA aides can
be built into existing systems and software in a user-centric way is an
important area for future exploration.

Furthermore, many risks within data, such as bias, poor representation, or the
picking up of private features, may be unknown to data controllers.
Identifying these is the point of a DPIA, but subtle issues are unlikely to
leap out of the page. In times like this, it has been suggested that a shared
knowledgebase [28] could be a useful resource, where researchers and data
controllers (or their modelling staff) could log risks and issues in certain
types of data from their own experiences, creating a resource which might
serve useful in new situations. For example, such a system might log found
biases in public datasets (particularly when linked to external data) or in
whole genres of data, such as Wi-Fi analytics or transport data. Such a system
might be a useful starting point for considering issues that may otherwise go
undetected, and for supporting low-capacity organisations in their responsible
use of analytics. From an HCI perspective though, the design of such a system
presents significant challenges. How can often nuanced biases be recorded and
communicated both clearly and in such a way that they generalise across
applications? How might individuals easily search a system for issues in their
own datasets, particularly when they might have a very large number of
variables in a combination the system has not seen previously? Making this
kind of knowledge accessible to practitioners seems promising, but daunting.

##  3 HCI, GDPR and Model Application

The GDPR, and data protection law in general, was not intended to
significantly govern decision-making. Already a strange law in the sense that
it poses transparency requirement that applies to the public and private
sectors alike, it is also a Frankenstein’s monster–style result culminating
from the melding of various European law and global principles that preceded
it [17].

###  3.1 Modes of Transparency

While transparency is generally spoken of as a virtue, the causal link between
it and better governance is rarely simple or clear. A great deal of focus has
been placed on the so-called “right to an explanation”, where a short paper at
a machine learning conference workshop [19] gained sudden notoriety,
triggering reactions from lawyers and technologists noting that the existence
and applicability of such a right was far from simple [30, 15]. Yet the
individualised transparency paradigm has rarely provided much practical use
for data subjects in their day-to-day lives (consider the burden of
‘transparent’ privacy policies). Consequently, HCI provides a useful place to
start when considering how to make the limited GDPR algorithmic transparency
provisions useful governance tools.

There are different places in which algorithmic transparency rights can be
found in the GDPR [30]. Each bring different important HCI challenges.

#### Meaningful information about the logic of processing

Articles 13–14 oblige data controllers to provide information at the time data
is collected around the logics of certain automated decision systems that
might be applied to this data. Current regulatory guidance [2] states that
there is no obligation to tailor this information to the specific situation of
a data subject (other than if they might be part of a vulnerable group, like
children, which might need further support to make the information
meaningful), although as many provisions in data protection law, the Court may
interpret this more broadly or narrowly when challenged. This points to an
important HCI challenge in making (or visualising) such general information,
but with the potential for specific relevance to individuals.

#### Right to be informed

In addition, there is a so-called ‘right to be informed’ of automated
decision-making [30]: how might an interface seamlessly flag to users when a
potentially legally relevant automated decision is being made? This is made
more challenging by the potential for adaptive interfaces or targeted
advertising to meet the criteria of a ‘decision’. In these cases, it is
unclear at what point the ‘decision’ is being made. Decisions might be seen in
the design process, or adaptive interfaces may be seen as ‘deciding’ which
information to provide or withold [15]. Exercise of data protection rights is
different in further ways in ambient environments [14], as smart cities and
ambient computing may bring significant challenges, if, for example, they are
construed as part of decision-making environments. Existing work in HCI has
focussed on the difficulties in identifying “moments of consent” in ubiquitous
computing [23, 22]. Not only is this relevant when consent is the legal basis
for an automated decision, but additional consideration will be needed in
relation to what equivalent “moments” of objection might look like. Given that
moments to object likely outnumber moments to consent, this might pose
challenges.

#### A right to an explanation?

An explicit “right to an explanation” of specific decisions, after they have
happened, sits in a non-binding recital in the GDPR [30], and thus its
applicability and enforceability depends heavily on regulators and the Court.
However, there is support for a parallel right in varying forms in certain
other laws, such as French administrative law or the Council of Europe
Convention 108 [16], and HCI researchers have already been testing different
explanation facilities proposed by machine learning researchers in qualitative
and quantitative settings to see how they compare in relation to different
notions of procedural justice [8]. Further research on explanation facilities
in-the-wild would be strongly welcome, given that most explanation facilities
to date have focussed on the user of a decision-support system rather than an
individual subject to an automated decision.

###  3.2 Mitigating Automation Bias

A key trigger condition for the automated decision-making provisions in the
GDPR (art 22) [15] centres on the degree of automation of the process.
Significant decisions “based solely on automated processing” require at least
consent, a contract or a basis in member state law. Recent regulatory guidance
indicates that there must be “meaningful” human input undertaken by somebody
with “authority and competence” who does not simply “routinely apply” the
outputs of the model in order to be able to avoid contestation or challenge
[29]. Automation bias has long been of interest to scholars of human factors
in computing [27, 13] and the GDPR provides two core questions for HCI in this
vein.

Firstly, this setup implies that systems that are expected to outperform
humans must always be considered “solely” automated [29]. If a decision-making
system is expected to legitimately outperform humans it makes meaningful input
very difficult. Any routine disagreement would be at best arbitrary and at
worst, harmful. This serves as yet another (legal) motivating factor to create
systems where human users can augment machine results. Even if this proves
difficult, when users contest an automated decision under the GDPR, they have
a right to human review. Interfaces need to ensure that even where models may
be complex and high-dimensional, decision review systems are rigorous and
themselves have “meaningful” human input—or else these reviewed decisions are
equally open to contestation.

Secondly, how might a data controller or a regulator understand whether
systems have “meaningful” human input or not, in order to either obey or
enforce the law? How might this input be justified and documented in a useful
and user-friendly way which could potentially be provided to the subject of
the decision? Recent French law does oblige this in some cases: in the case of
algorithmically-derived administrative decisions, information should be
provided to decision-subjects on the “the degree and the mode of contribution
of the algorithmic processing to the decision-making” [16]. Purpose-built
interfaces and increased knowledge from user studies both seem needed for the
aim of promoting meaningful, accountable input.

###  3.3 Communicating Envisaged Consequences

Where significant, automated decision-making using machine learning is
expected, the information rights in the GDPR (arts 13–15) provide that a data
subject should be provided with the “envisaged consequences” of such decision
for her. What this means is far from clear. Recent regulatory guidance
provides only the example of giving data subject applying for insurance
premiums an app to demonstrate the consequences of dangerous driving [2].
Where users are consenting to complex online personalisation which could
potentially bring significant effects to their life, such as content delivery
which might lead to echo chambers or “filter bubbles”, it is unclear how
complex “envisaged consequences” might be best displayed in order to promote
user autonomy and choice.

##  4 Concluding remarks

HCI is well-placed to help enable the regulatory effectiveness of the GDPR in
relation to algorithmic fairness and accountability. Here we have touched on
different points where governance might come into play—model training and
model application—but also different modes of governance. Firstly, HCI might
play a role in enabling creative, rigorous, problem solving practices within
organisations. Many mechanisms in the GDPR, such as data protection by design
and data protection impact assessments, will depend heavily on the
communities, practices and technologies that develop around them in different
contexts. Secondly, HCI might play a role in enabling controllers do
particular tasks better. Here, we discussed the potential for exploratory data
analysis tools, such as detecting special category data even when it was not
explicitly collected. Finally, it might help data subjects exercise their
rights better. It appears especially important to develop new modes and
standards for transparency, documentation of human input, and communication of
tricky notions such as “envisaged consequences”.

As the GDPR often defines data controllers’ obligations as a function of
“available technologies” and “technological developments”, it is explicitly
enabled and strengthened by computational systems and practices designed with
its varied provisions in mind. Many parts of the HCI community have already
been building highly relevant technologies and practices that could be applied
in this way. Further developing these with a regulatory focus might be
transformative in and of itself—and it is something we believe should be
promoted in this field and beyond.

## References

  * [1]
  * [2] Article 29 Data Protection Working Party. 2018.  Guidelines on Automated individual decision-making and Profiling for the purposes of Regulation 2016/679, wp251rev.01.
  * [3] Solon Barocas and Helen Nissenbaum. 2014.  Big Data’s End Run Around Procedural Privacy Protections.  Commun. ACM 57, 11 (2014), 31–33.
  * [4] Solon Barocas and Andrew D Selbst. 2016.  Big Data’s Disparate Impact.  California Law Review 104 (2016), 671–732.
  * [5] Bettina Berendt and Sören Preibusch. 2012.  Exploring discrimination: A user-centric evaluation of discrimination-aware data mining. In 12th IEEE International Conference on Data Mining Workshops (ICDMW). 344–351.
  * [6] Bettina Berendt and Sören Preibusch. 2014.  Better decision support through exploratory discrimination-aware data mining: Foundations and empirical evidence.  Artificial Intelligence and Law 22, 2 (2014), 175–209.
  * [7] Reuben Binns. 2017.  Data protection impact assessments: A meta-regulatory approach.  International Data Privacy Law 7, 1 (2017), 22–35.  DOI:http://dx.doi.org/10.1093/idpl/ipw027
  * [8] Reuben Binns, Max Van Kleek, Michael Veale, Ulrik Lyngs, Jun Zhao, and Nigel Shadbolt. 2018.  ‘It’s Reducing a Human Being to a Percentage’; Perceptions of Justice in Algorithmic Decisions.  In CHI’18.  DOI:http://dx.doi.org/10.1145/3173574.3173951
  * [9] Lee A Bygrave. 2017.  Data Protection by Design and by Default: Deciphering the EU’s Legislative Requirements.  Oslo Law Review 1, 02 (2017), 105–120.
  * [10] Toon Calders and Indrė Žliobaitė. 2012.  Why Unbiased Computational Processes Can Lead to Discriminative Decision Procedures.  In Discrimination and Privacy in the Information Society, Bart Custers, Toon Calders, Bart Schermer, and Tal Zarsky (Eds.). Springer, Berlin, Heidelberg, 43–59.
  * [11] Bart Custers. 2012.  Data Dilemmas in the Information Society: Introduction and Overview.  In Discrimination and Privacy in the Information Society, Bart Custers, Toon Calders, Bart Schermer, and Tal Zarsky (Eds.). Springer, 3–25.
  * [12] Catherine D’Ignazio and Lauren F Klein. 2016.  Feminist data visualization. In Workshop on Visualization for the Digital Humanities (VIS4DH), IEEE VIS 2016.
  * [13] Mary T Dzindolet, Scott A Peterson, Regina A Pomranky, Linda G Pierce, and Hall P Beck. 2003.  The role of trust in automation reliance.  International Journal of Human-Computer Studies 58, 6 (2003), 697–718.
  * [14] Lilian Edwards. 2016.  Privacy, security and data protection in smart cities: A critical EU law perspective.  Eur. Data Prot. L. Rev. 2 (2016), 28.  DOI:http://dx.doi.org/10.2139/ssrn.2711290
  * [15] Lilian Edwards and Michael Veale. 2017.  Slave to the Algorithm? Why a ‘Right to an Explanation’ is Probably Not The Remedy You Are Looking For.  Duke Law & Technology Review 16, 1 (2017), 18–84.  DOI:http://dx.doi.org/10.2139/ssrn.2972855
  * [16] Lilian Edwards and Michael Veale. 2018.  Enslaving the algorithm: From a ‘right to an explanation’ to a ‘right to better decisions’?  IEEE Security & Privacy (2018).  DOI:http://dx.doi.org/10.2139/ssrn.3052831
  * [17] Gloria González Fuster. 2014.  The emergence of personal data protection as a fundamental right of the EU.  Springer.
  * [18] Oscar H Gandy. 2009.  Coming to Terms with Chance: Engaging Rational Discrimination and Cumulative Disadvantage.  Routledge, London.
  * [19] Bryce Goodman and Seth Flaxman. 2016.  European Union regulations on algorithmic decision-making and a “right to explanation”.  In 2016 ICML Workshop on Human Interpretability in Machine Learning (WHI 2016), New York, NY.
  * [20] Graham Greenleaf. 2018.  ‘European’ Data Privacy Standards Implemented in Laws Outside Europe.  Privacy Laws & Business International Report 149 (2018), 21–23.
  * [21] Mireille Hildebrandt. 2008.  Defining Profiling: A New Type of Knowledge?  In Profiling the European Citizen: Cross-Disciplinary Perspectives, Mireille Hildebrandt and Serge Gutwirth (Eds.). Springer, 17–45.
  * [22] Ewa Luger and Tom Rodden. 2013a.  An Informed View on Consent for UbiComp. In UbiComp ’13. 529–538.  DOI:http://dx.doi.org/10.1145/2493432.2493446
  * [23] Ewa Luger and Tom Rodden. 2013b.  Terms of agreement: Rethinking consent for pervasive computing.  Interacting with Computers 25, 3 (2013), 229–241.
  * [24] Ewa Luger, Lachlan Urquhart, Tom Rodden, and Michael Golembewski. 2015\.  Playing the legal card: Using ideation cards to raise data protection issues within the design process.  457–466.  DOI:http://dx.doi.org/10.1145/2702123.2702142
  * [25] Justin Matejka and George Fitzmaurice. 2017.  Same stats, different graphs: generating datasets with varied appearance and identical statistics through simulated annealing. In CHI’17. 1290–1294.  DOI:http://dx.doi.org/10.1145/3025453.3025912
  * [26] Paul M Schwartz and Daniel J Solove. 2011.  The PII problem: Privacy and a new concept of personally identifiable information.  New York University Law Review 86 (2011), 1814.
  * [27] Linda J Skitka, Kathleen L Mosier, and Mark Burdick. 1999.  Does automation bias decision-making?  International Journal of Human-Computer Studies 51 (1999), 991–1006.  DOI:http://dx.doi.org/10.1006/ijhc.1999.0252
  * [28] Michael Veale and Reuben Binns. 2017.  Fairer machine learning in the real world: Mitigating discrimination without collecting sensitive data.  Big Data & Society 4, 2 (2017).  DOI:http://dx.doi.org/10.1177/2053951717743530
  * [29] Michael Veale and Lilian Edwards. 2018.  Clarity, Surprises, and Further Questions in the Article 29 Working Party Draft Guidance on Automated Decision-Making and Profiling.  Computer Law & Security Review 34, 2 (2018).  DOI:http://dx.doi.org/10.1016/j.clsr.2017.12.002
  * [30] Sandra Wachter, Brent Mittelstadt, and Luciano Floridi. 2017.  Why a right to explanation of automated decision-making does not exist in the General Data Protection Regulation.  International Data Privacy Law 7, 2 (2017), 76–99.