# Relational Type Theory (All Proofs)

Aaron Stump  Computer Science
The University of Iowa
Iowa City, Iowa, 52242
Email<EMAIL_ADDRESS>Benjamin Delaware  Computer Science
Purdue University
West Lafayette, Indiana, 47907
Email<EMAIL_ADDRESS>Christopher Jenkins  Computer Science
The University of Iowa
Iowa City, Iowa, 52242
Email<EMAIL_ADDRESS>
###### Abstract

This paper introduces Relational Type Theory (RelTT), a new approach to type
theory with extensionality principles, based on a relational semantics for
types. The type constructs of the theory are those of System F plus relational
composition, converse, and promotion of application of a term to a relation. A
concise realizability semantics is presented for these types. The paper shows
how a number of constructions of traditional interest in type theory are
possible in RelTT, including $\eta$-laws for basic types, inductive types with
their induction principles, and positive-recursive types. A crucial role is
played by a lemma called Identity Inclusion, which refines the Identity
Extension property familiar from the semantics of parametric polymorphism. The
paper concludes with a type system for RelTT, paving the way for
implementation.

##  I Introduction

Modern constructive type theories have long wish lists of features, from
inductive and coinductive types, to type-specific extensionality principles,
quotient types, higher-order datatypes, and more. In tension with this, there
are excellent reasons to seek to keep the core type theory small and
trustworty. This has been done, in different ways, for Lean [1] and recently
Coq [2]. Both those systems implement (variants of) the Calculus of Inductive
Constructions, which lacks type-specific extensionality principles.

The present paper proposes Relational Type Theory (RelTT) for deriving
expressive type constructs, with type-specific extensionality principles, from
a formally small core theory. The approach followed is, to the authors’
knowledge, novel: RelTT is based a semantics for types as binary relations on
untyped terms. For example, the semantics for a function type $R\to
R^{\prime}$ makes it the set of pairs of terms $(t_{1},t_{2})$ that jointly
map inputs related by the meaning of $R$ to outputs related by the meaning of
$R^{\prime}$ (the semantics familiar from the field of logical relations). The
notion that a term “is” a function is expressed only by saying that it is
related to itself at function type. So relations between terms are the primary
concern of the theory, and expression of program behavior in isolation (i.e.,
traditional typing) is secondary.

This commitment to relational semantics leads us in an unexplored direction:
we extend the set of type constructs with relational constructs. We may use
these to express asymmetric relations, which are crucial for developing
reasoning principles, like induction principles, within the theory.
Interestingly, dependent types are unnecessary for this. The relational
semantics already gives us a form of dependency which is all we need for
inductive reasoning about terms. So RelTT is an extension, with relational
type constructs, of System F, not the Calculus of Constructions. Avoiding
dependent types notably simplifies the semantics. The power of System F is
needed because the terms that the theory (relationally) types are those of
pure lambda calculus, so we adopt impredicative lambda encodings to represent
inductive types.

The contributions of the paper are:

  * •

The syntax and semantics of relational types (Section II)

  * •

Basic properties of the semantics, crucially including $\beta\eta$-closure
(Section III)

  * •

Interesting derived type forms and examples (Section IV), and basic type-
specific extensionality principles (Section V).

  * •

Classes of types whose interpretations are proved to be, respectively,
symmetric (Section VI) and transitive (Section VII). The proof of transitivity
crucially relies on a novel theorem dubbed Identity Inclusion (Lemma 32). The
intricate proof of this makes use of duality between types where all
quantifiers occur only positively ($\forall^{+}$ types), and ones where they
occur only negatively.

  * •

Derivation of induction principles from types for Church-encodings (Section
X). This covers any inductive type definable by a type scheme which is
positive and, due to a critical use of Identity Inclusion, $\forall^{+}$.
Positive-recursive types are also derived (Section XI).

  * •

A proof system called RelPf (Section VIII) and type system RelTy (Section
XII), which are proven sound with respect to the semantics, and are intended
as the starting point for implementation of RelTT as a proof assistant.

We will reference lemmas and theorems by name, with the theorem number
following in braces (e.g., “$\beta\eta$-Closure {2}”). We will label
assumptions and proven local facts with numbers (e.g., “(1)”), and goals with
capital letters (e.g., “(A)”).

##  II Relational types and their semantics

$\begin{array}[]{lll}\textit{terms }t&::=&x\ |\ \lambda\,x.\,t\ |\
t\,t^{\prime}\\\ \textit{types }R&::=&X\ |\ R\to R^{\prime}\ |\
\forall\,X.\,R\ |\ R^{\cup}\ |\ R\cdot R^{\prime}\ |\ t\end{array}$ Figure 1:
Syntax for relational types ($X$ ranges over type variables)

The syntax of relational types $R$ is given in Figure 1. Terms $t$ are those
of pure untyped lambda calculus. Relational type constructs include those of
System F, plus $R^{\cup}$ for converse of a relation, $R\cdot R^{\prime}$ for
composition of relations, and promotion of terms $t$ to relations, to be
explained shortly. Usual parsing precedences from type theory are followed;
additionally, $R^{\cup}$ binds most tightly, $R\cdot R^{\prime}$ second most
tightly, and the other constructs after these. We also follow the usual
convention that distinct meta-variables ranging over variables denote distinct
variables (so $x$ and $y$ denote different variables), and treat terms and
types up to $\alpha$-equivalence. Capture-avoiding substitution of $R$ for $X$
in $R^{\prime}$ is denoted $[R/X]R^{\prime}$ (similarly $[t/x]t^{\prime}$ for
terms). The set of free variables of any syntactic entity $e$ is denoted
$\textit{FV}(e)$. The obvious definitions of these syntactic notions are
omitted.

######  Definition 1.

A relation $r$ on terms of pure untyped $\lambda$-calculus is
$\beta\eta$-closed iff $t_{1}\ [r]\ t_{2}$,
$t_{1}^{\prime}=_{\beta\eta}t_{1}$, and $t_{2}^{\prime}=_{\beta\eta}t_{2}$
imply $t_{1}^{\prime}\ [r]\ t_{2}^{\prime}$. Write $\mathcal{R}$ for the set
of all such relations, and use meta-variable $r$ to range over $\mathcal{R}$

The relational semantics of types is defined in Figure 2, where environment
$\gamma$ is a function mapping a finite set of type variables to elements of
$\mathcal{R}$. We use infix notation for application of a relation to a pair
of terms and, following [3], we sometimes put square brackets around the
relation for readability; for example, in the three equations at the bottom of
the figure. In those equations, operators like “$\to$” on the right-hand sides
have their standard meaning in the background meta-logic.

The interpretation $\llbracket R\rrbracket_{\gamma}$ is defined iff $\gamma$
is defined for all free type variables of $R$. When referencing $\llbracket
R\rrbracket_{\gamma}$ in theorems, we assume it is defined. The semantics
extends $\gamma$ from type variables to arbitrary types. Promotion of term $t$
is the graph of the meta-level operation mapping $t^{\prime}$ to $t\
t^{\prime}$. Many examples are below.

$\begin{array}[]{lll}\llbracket X\rrbracket_{\gamma}&=&\gamma(X)\\\ \llbracket
R\to R^{\prime}\rrbracket_{\gamma}&=&\llbracket
R\rrbracket_{\gamma}\to\llbracket R^{\prime}\rrbracket_{\gamma}\\\
\llbracket\forall\,X.\,R\rrbracket_{\gamma}&=&\bigcap_{r\in\mathcal{R}}\,\llbracket
R\rrbracket_{\gamma[X\mapsto r]}\\\ \llbracket
R^{\cup}\rrbracket_{\gamma}&=&\llbracket R\rrbracket_{\gamma}^{\cup}\\\
\llbracket R\cdot R^{\prime}\rrbracket_{\gamma}&=&\llbracket
R\rrbracket_{\gamma}\cdot\llbracket R^{\prime}\rrbracket_{\gamma}\\\
\llbracket\hat{t}\rrbracket_{\gamma}&=&\\{(t,t^{\prime})\ |\
\hat{t}\,t\,=_{\beta\eta}\,t^{\prime}\\}\\\ \\\
\lx@intercol\textit{where:}\hfil\lx@intercol\\\ t\,[r_{1}\to
r_{2}]\,t^{\prime}&=&\forall\,a.\,\forall\,a^{\prime}.\,a\,[r_{1}]\,a^{\prime}\to
t\,a\,[r_{2}]\,t^{\prime}\,a^{\prime}\\\
t\,[r^{\cup}]\,t^{\prime}&=&t^{\prime}\,[r]\,t\\\ t\,[r_{1}\cdot
r_{2}]\,t^{\prime}&=&\exists\,t^{\prime\prime}.\,t\,[r_{1}]\,t^{\prime\prime}\,\wedge\,t^{\prime\prime}\,[r_{2}]\,t^{\prime}\par\end{array}$
Figure 2: Semantics for relational types; relational operators $\to$, ∪, and
$\cdot$

While the semantics of universal types quantifies (at the meta-level) over all
relations in $\mathcal{R}$, we will restrict ourselves in all examples below
to instantiating such quantifiers only with definable relations (i.e., ones of
the form $\llbracket R\rrbracket_{\gamma}$). In Sections VIII and XII below,
we will consider deductive systems for RelTT where this restriction will be
enforced.

##  III Basic properties

######  Lemma 2 ($\beta\eta$-Closure).

$\llbracket R\rrbracket_{\gamma}\in\mathcal{R}$.

###### Proof.

The proof is by induction on $R$. Suppose $t_{1}=_{\beta\eta}t_{1}^{\prime}$
and $t_{2}=_{\beta\eta}t_{2}^{\prime}$, assume (1) $t_{1}\ \llbracket
R\rrbracket_{\gamma}\ t_{2}$, and show $t_{1}^{\prime}\ \llbracket
R\rrbracket_{\gamma}\ t_{2}^{\prime}$.

Case $X$: $\gamma(X)\in\mathcal{R}$ by specification of $\gamma$.

Case $R\to R^{\prime}$: assume (2) $a\ \llbracket R\rrbracket_{\gamma}\
a^{\prime}$, and show $t_{1}^{\prime}\ a\ \llbracket
R^{\prime}\rrbracket_{\gamma}\ t_{2}^{\prime}\ a^{\prime}$. From (1) and (2)
we have $t_{1}\ a\ \llbracket R^{\prime}\rrbracket_{\gamma}\ t_{2}\
a^{\prime}$. From this, the IH gives us the required conclusion, as $t_{1}\
a=_{\beta\eta}t_{1}^{\prime}\ a$ and $t_{2}\
a^{\prime}=_{\beta\eta}t_{2}^{\prime}\ a^{\prime}$.

Case $\forall\,X.\,R$: assume $r\in\mathcal{R}$, and show $t_{1}^{\prime}\
\llbracket R\rrbracket_{\gamma[X\mapsto r]}\ t_{2}^{\prime}$. By (1), we have
$t_{1}\ \llbracket R\rrbracket_{\gamma[X\mapsto r]}\ t_{2}$, from which the IH
then yields the desired conclusion.

Case $R^{\cup}$: this follows by the IH (using symmetry of $=_{\beta\eta}$).

Case $R\cdot R^{\prime}$: from (1), there exists $t$ such that $t_{1}\
\llbracket R\rrbracket_{\gamma}\ t$ and $t\ \llbracket
R^{\prime}\rrbracket_{\gamma}\ t_{2}$. By the IH, $t_{1}^{\prime}\ \llbracket
R\rrbracket_{\gamma}\ t$ and $t\ \llbracket R^{\prime}\rrbracket_{\gamma}\
t_{2}^{\prime}$. These imply the desired conclusion.

Case $t$: from (1), we have $t\ t_{1}=_{\beta\eta}t_{2}$; $t\
t_{1}^{\prime}=_{\beta\eta}t_{2}^{\prime}$ then follows.

∎

######  Lemma 3 (Symmetry Properties).

  1. 1.

$\llbracket(\forall\,X.\,R)^{\cup}\rrbracket_{\gamma}=\llbracket\forall\,X.\,R^{\cup}\rrbracket_{\gamma}$

  2. 2.

$\llbracket(R_{1}\to R_{2})^{\cup}\rrbracket_{\gamma}=\llbracket
R_{1}^{\cup}\to R_{2}^{\cup}\rrbracket_{\gamma}$

  3. 3.

$\llbracket(R_{1}\cdot R_{2})^{\cup}\rrbracket_{\gamma}=\llbracket
R_{2}^{\cup}\cdot R_{1}^{\cup}\rrbracket_{\gamma}$

###### Proof.

(1): assume $t\ \llbracket(\forall\,X.\,R)^{\cup}\rrbracket_{\gamma}\
t^{\prime}$, and hence $t^{\prime}\
\llbracket(\forall\,X.\,R)\rrbracket_{\gamma}\ t$. For any $r\in\mathcal{R}$,
$t^{\prime}\ \llbracket R\rrbracket_{\gamma[X\mapsto r]}\ t$, hence $t\
\llbracket R^{\cup}\rrbracket_{\gamma[X\mapsto r]}\ t^{\prime}$. From this,
$t\ \llbracket\forall\,X.\,R^{\cup}\rrbracket_{\gamma}\ t^{\prime}$ as
required. Conversely, assume $t\
\llbracket\forall\,X.\,R^{\cup}\rrbracket_{\gamma}\ t^{\prime}$, and
$r\in\mathcal{R}$. Then $t\ \llbracket R^{\cup}\rrbracket_{\gamma[X\mapsto
r]}\ t^{\prime}$, hence $t^{\prime}\ \llbracket R\rrbracket_{\gamma[X\mapsto
r]}\ t$. From this, $t^{\prime}\ \llbracket\forall\,X.\,R\rrbracket_{\gamma}\
t$, hence the required $t\
\llbracket(\forall\,X.\,R)^{\cup}\rrbracket_{\gamma}\ t^{\prime}$.

(2): Assume $t\ \llbracket(R_{1}\to R_{2})^{\cup}\rrbracket_{\gamma}\
t^{\prime}$ and $a\ \llbracket R_{1}^{\cup}\rrbracket_{\gamma}\ a^{\prime}$.
From these, $t^{\prime}\ \llbracket(R_{1}\to R_{2})\rrbracket_{\gamma}\ t$ and
$a^{\prime}\ \llbracket R_{1}\rrbracket_{\gamma}\ a$, which yield $t^{\prime}\
a^{\prime}\ \llbracket R_{1}\rrbracket_{\gamma}\ t\ a$. Thus, $t\ a\
\llbracket R_{1}^{\cup}\rrbracket_{\gamma}\ t^{\prime}\ a^{\prime}$ as
required. Conversely, assume $t\ \llbracket R_{1}^{\cup}\to
R_{2}^{\cup}\rrbracket_{\gamma}\ t^{\prime}$ and $a\ \llbracket
R_{1}\rrbracket_{\gamma}\ a^{\prime}$. From the latter, $a^{\prime}\
\llbracket R_{1}^{\cup}\rrbracket_{\gamma}\ a$, so $t\ a^{\prime}\ \llbracket
R_{2}^{\cup}\rrbracket_{\gamma}\ t^{\prime}\ a$. From this, $t^{\prime}\ a\
\llbracket R_{2}\rrbracket_{\gamma}\ t\ a^{\prime}$, as required.

(3): assume $t\ \llbracket(R_{1}\cdot R_{2})^{\cup}\rrbracket_{\gamma}\
t^{\prime}$, hence $t^{\prime}\ \llbracket R_{1}\cdot
R_{2}\rrbracket_{\gamma}\ t$. So there exists $t^{\prime\prime}$ with
$t^{\prime}\ \llbracket R_{1}\rrbracket_{\gamma}\ t^{\prime\prime}$ and
$t^{\prime\prime}\ \llbracket R_{2}\rrbracket_{\gamma}\ t$. From these,
$t^{\prime\prime}\ \llbracket R_{1}^{\cup}\rrbracket_{\gamma}\ t^{\prime}$ and
$t\ \llbracket R_{2}^{\cup}\rrbracket_{\gamma}\ t^{\prime\prime}$; thus, $t\
\llbracket R_{2}^{\cup}\cdot R_{1}^{\cup}\rrbracket_{\gamma}\ t^{\prime}$.
Conversely, assume $t\ \llbracket R_{2}^{\cup}\cdot
R_{1}^{\cup}\rrbracket_{\gamma}\ t^{\prime}$. So there exists
$t^{\prime\prime}$ with $t\ \llbracket R_{2}^{\cup}\rrbracket_{\gamma}\
t^{\prime\prime}$ and $t^{\prime\prime}\ \llbracket
R_{1}^{\cup}\rrbracket_{\gamma}\ t^{\prime}$. From these, $t^{\prime\prime}\
\llbracket R_{2}\rrbracket_{\gamma}\ t$ and $t^{\prime}\ \llbracket
R_{1}\rrbracket_{\gamma}\ t^{\prime\prime}$. So $t\ \llbracket(R_{1}\cdot
R_{2})^{\cup}\rrbracket_{\gamma}\ t^{\prime}$. ∎

######  Lemma 4 (Deapplication).

  1. 1.

$t_{1}\ \llbracket t\cdot R\rrbracket_{\gamma}\ t_{2}=t\ t_{1}\ \llbracket
R\rrbracket_{\gamma}\ t_{2}$

  2. 2.

$t_{1}\ \llbracket R\cdot t^{\cup}\rrbracket_{\gamma}\ t_{2}=t_{1}\ \llbracket
R\rrbracket_{\gamma}\ t\ t_{2}$

###### Proof.

For the first fact: first, assume $t_{1}\ \llbracket t\cdot
R\rrbracket_{\gamma}\ t_{2}$. The semantics gives $t^{\prime}$ such that (1)
$t_{1}\ \llbracket t\rrbracket_{\gamma}\ t^{\prime}$ and (2) $t^{\prime}\
\llbracket R\rrbracket_{\gamma}\ t_{2}$. But (1) is equivalent to $t\
t_{1}=_{\beta\eta}t^{\prime}$. Applying $\beta\eta$-Closure {2}, $t\ t_{1}\
\llbracket R\rrbracket_{\gamma}\ t_{2}$ as required. Next, assume $t\ t_{1}\
\llbracket R\rrbracket_{\gamma}\ t_{2}$. Then there is a $t^{\prime}$, namely
$t\ t_{1}$, such that $t_{1}\ \llbracket t\rrbracket_{\gamma}\ t^{\prime}$ and
$t^{\prime}\ \llbracket R\rrbracket_{\gamma}\ t_{2}$. Hence $t_{1}\ \llbracket
t\cdot R\rrbracket_{\gamma}\ t_{2}$ as required.

For the second: assuming $t_{1}\ \llbracket R\cdot
t^{\cup}\rrbracket_{\gamma}\ t_{2}$, the semantics gives $t^{\prime}$ such
that (1) $t_{1}\ \llbracket R\rrbracket_{\gamma}\ t^{\prime}$ and (2)
$t^{\prime}\ \llbracket t^{\cup}\rrbracket_{\gamma}\ t_{2}$. But (2) is
equivalent to $t\ t_{2}=_{\beta\eta}t^{\prime}$. Applying $\beta\eta$-Closure
{2}, $t_{1}\ \llbracket R\rrbracket_{\gamma}\ t\ t_{2}$ as required. Next,
assume $t_{1}\ \llbracket R\rrbracket_{\gamma}\ t\ t_{2}$. Then there is a
$t^{\prime}$, namely $t\ t_{2}$, such that $t_{1}\ \llbracket
R\rrbracket_{\gamma}\ t^{\prime}$ and $t^{\prime}\ \llbracket
t^{\cup}\rrbracket_{\gamma}\ t_{2}$. Hence $t_{1}\ \llbracket R\cdot
t^{\cup}\rrbracket_{\gamma}\ t_{2}$ as required. ∎

We make use of a few definitions for terms in Figure 3.

$\begin{array}[]{lll}I&:=&\lambda\,x.\,x\\\
K&:=&\lambda\,x.\,\lambda\,y.\,x\\\ t\circ t^{\prime}&:=&\lambda\,x.\,t\
(t^{\prime}\ x)\end{array}$ Figure 3: Some standard definitions and notations
for terms, used below

######  Lemma 5 (Relational Laws).

  1. 1.

$\llbracket R_{1}\cdot(R_{2}\cdot
R_{3})\rrbracket_{\gamma}=\llbracket(R_{1}\cdot R_{2})\cdot
R_{3}\rrbracket_{\gamma}$

  2. 2.

$\llbracket(R^{\cup})^{\cup}\rrbracket_{\gamma}=\llbracket
R\rrbracket_{\gamma}$

  3. 3.

$\llbracket R\cdot I\rrbracket_{\gamma}=\llbracket I\cdot
R\rrbracket_{\gamma}=\llbracket R\rrbracket_{\gamma}$

###### Proof.

(1) follows from the semantics of $\cdot$ as relational composition, (2) from
the semantics of $\cup$ as relational converse, and (3) from Deapplication {4}
(applying also $\beta\eta$-Closure {2}). ∎

We may observe that Symmetry Properties {3} part (3) and Relational Laws {5}
validate the complement- and union-free axioms of the Calculus of Relations
(RelTT omits complement and union) [4].

######  Lemma 6 (Interpretation Over Substitution).

$\llbracket[R/X]R^{\prime}\rrbracket_{\gamma}=\llbracket
R^{\prime}\rrbracket_{\gamma[X\mapsto\llbracket R\rrbracket_{\gamma}]}$

###### Proof.

The proof is by induction on $R^{\prime}$. Let $\gamma^{\prime}$ denote
$\gamma[X\mapsto\llbracket R\rrbracket_{\gamma}]$.

Case $X$:

$\llbracket[R/X]X\rrbracket_{\gamma}=\llbracket
R\rrbracket_{\gamma}=\llbracket X\rrbracket_{\gamma^{\prime}}$

Case $Y$:

$\llbracket[R/X]Y\rrbracket_{\gamma}=\gamma(Y)=\llbracket
Y\rrbracket_{\gamma^{\prime}}$

Case $R_{1}\to R_{2}$:

$\begin{array}[]{l}\llbracket[R/X](R_{1}\to R_{2})\rrbracket_{\gamma}=\\\
\llbracket[R/X]R_{1}\rrbracket_{\gamma}\to\llbracket[R/X]R_{2}\rrbracket_{\gamma}=\\\
\llbracket R_{1}\rrbracket_{\gamma^{\prime}}\to\llbracket
R_{2}\rrbracket_{\gamma^{\prime}}=\\\ \llbracket R_{1}\to
R_{2}\rrbracket_{\gamma^{\prime}}\end{array}$

Case $\forall\,X.\,R_{1}$:

$\begin{array}[]{l}\llbracket[R/X]\forall\,X.\,R_{1}\rrbracket_{\gamma}=\\\
\bigcap_{r\in\mathcal{R}}\ \llbracket[R/X]R_{1}\rrbracket_{\gamma[X\mapsto
r]}\\\ \bigcap_{r\in\mathcal{R}}\ \llbracket
R_{1}\rrbracket_{\gamma^{\prime}[X\mapsto r]}\\\
\llbracket\forall\,X.\,R_{1}\rrbracket_{\gamma^{\prime}}\end{array}$

Case $R_{1}^{\cup}$:

$\begin{array}[]{l}\llbracket[R/X](R_{1}^{\cup})\rrbracket_{\gamma}=\\\
\llbracket[R/X]R_{1}\rrbracket_{\gamma}^{\cup}=\\\ \llbracket
R_{1}\rrbracket_{\gamma^{\prime}}^{\cup}=\\\ \llbracket
R_{1}^{\cup}\rrbracket_{\gamma^{\prime}}\end{array}$

Case $R_{1}\cdot R_{2}$:

$\begin{array}[]{l}\llbracket[R/X](R_{1}\cdot R_{2})\rrbracket_{\gamma}=\\\
\llbracket[R/X]R_{1}\rrbracket_{\gamma}\cdot\llbracket[R/X]R_{2}\rrbracket_{\gamma}=\\\
\llbracket R_{1}\rrbracket_{\gamma^{\prime}}\cdot\llbracket
R_{2}\rrbracket_{\gamma^{\prime}}=\\\ \llbracket R_{1}\cdot
R_{2}\rrbracket_{\gamma^{\prime}}\end{array}$

Case $\hat{t}$:

$\llbracket[R/X]\hat{t}\rrbracket_{\gamma}=\llbracket\hat{t}\rrbracket_{\gamma}=\llbracket\hat{t}\rrbracket_{\gamma^{\prime}}$

∎

######  Lemma 7 (Environment Extension).

  1. 1.

If $X\not\in\textit{FV}(R)$, then

$\llbracket R\rrbracket_{\gamma[X\mapsto r]}=\llbracket
R\rrbracket_{\gamma}=\llbracket[X/Y]R\rrbracket_{\gamma[X\mapsto\gamma(Y)]}$

  2. 2.

If $R$ is closed, then $\llbracket R\rrbracket_{\gamma}=\llbracket
R\rrbracket_{\gamma^{\prime}}$.

###### Proof.

The first fact is by an obvious induction on $R$. The second follows by
iterating the first one to shrink $\gamma$ to the empty environment, and then
build it back up to $\gamma^{\prime}$ (recall that environments map a finite
set of type variables). ∎

##  IV Basic examples and definitions

######  Lemma 8 (Identity).

$I\ \llbracket X\to X\rrbracket_{\gamma}\ I$

###### Proof.

Assume (1) $t\ [\gamma(X)]\ t^{\prime}$ and show $I\ t\ [\gamma(X)]\ I\
t^{\prime}$. But this follows from (1) by $\beta\eta$-Closure {2}. ∎

######  Definition 9.

  1. 1.

$[t]R:=(K\ t)\cdot R$

  2. 2.

$R[t]:=R\cdot(K\ t)^{\cup}$

We can express within the theory the property of being related to term $t$ by
$R$ with the relational types $[t]R$ and $R[t]$. In particular, this gives us
a form of internalized typing: for example, we may use the type
$[I]\forall\,X.\,X\to X[I]$ to express the property that $I$ has the expected
polymorphic type. These notations are to be parsed with highest precedence.

######  Lemma 10 (Internalized Typing).

  1. 1.

$t_{1}\ \llbracket[t]R\rrbracket_{\gamma}\ t_{2}=t\ \llbracket
R\rrbracket_{\gamma}\ t_{2}$

  2. 2.

$t_{1}\ \llbracket R[t]\rrbracket_{\gamma}\ t_{2}=t_{1}\ \llbracket
R\rrbracket_{\gamma}\ t$

###### Proof.

For (1), use $\beta\eta$-Closure {2}:

$(t_{1}\ \llbracket[t]R\rrbracket_{\gamma}\ t_{2})=(K\ t\ t_{1}\ \llbracket
R\rrbracket_{\gamma}\ t_{2})=(t\ \llbracket R\rrbracket_{\gamma}\ t_{2})$

For (2), use $\beta\eta$-Closure {2} and also Deapplication {4}:

$(t_{1}\ \llbracket R[t]\rrbracket_{\gamma}\ t_{2})=(t_{1}\ \llbracket
R\rrbracket_{\gamma}\ K\ t\ t_{2})=(t_{1}\ \llbracket R\rrbracket_{\gamma}\
t)$

∎

The following operations are reminiscent of conjugation in group theory:

######  Definition 11.

$t_{1}.R.t_{2}:=t_{1}\cdot R\cdot t_{2}^{\cup}$

######  Definition 12.

$t\mathbin{\ast}R:=t.R.t$

######  Lemma 13 (Conjugation).

  1. 1.

$t_{1}\ \llbracket t.R.t^{\prime}\rrbracket_{\gamma}\ t_{2}=t\ t_{1}\
\llbracket R\rrbracket_{\gamma}\ t^{\prime}\ t_{2}$.

  2. 2.

$t_{1}\ \llbracket t\mathbin{\ast}R\rrbracket_{\gamma}\ t_{2}=t\ t_{1}\
\llbracket R\rrbracket_{\gamma}\ t\ t_{2}$.

###### Proof.

Apply Deapplication {4}. ∎

We may internalize inclusion of relations as a type, using term promotions:

######  Definition 14.

$R\subseteq R^{\prime}:=(K\ I)\mathbin{\ast}(R\to R^{\prime})$

######  Lemma 15 (Subset).

$t_{1}\ \llbracket R\subseteq R^{\prime}\rrbracket_{\gamma}\ t_{2}$ iff
$\llbracket R\rrbracket_{\gamma}\subseteq\llbracket
R^{\prime}\rrbracket_{\gamma}$.

###### Proof.

Making use of Conjugation {13}, deduce

$\begin{array}[]{l}t_{1}\ \llbracket R\subseteq R^{\prime}\rrbracket_{\gamma}\
t_{2}=\\\ K\ I\ t_{1}\ \llbracket R\to R^{\prime}\rrbracket_{\gamma}\ K\ I\
t_{2}=\\\ I\ \llbracket R\to R^{\prime}\rrbracket_{\gamma}\ I\end{array}$

The semantics (Figure 2) states that this latter relational typing is true in
environment $\gamma$ iff for all $(x,x^{\prime})\in\llbracket
R\rrbracket_{\gamma}$, $(I\ x,I\ x^{\prime})\in\llbracket
R^{\prime}\rrbracket_{\gamma}$, which by $\beta\eta$-Closure {2} is equivalent
to $(x,x^{\prime})\in\llbracket R^{\prime}\rrbracket_{\gamma}$. ∎

Term promotions also enable us to derive implicit products [5]. In traditional
type theories, implicit products are used to express quantifications without
corresponding $\lambda$-abstractions in the subject. One may think of them as
describing specificational (or “ghost”) inputs to functions. In RelTT, we
express this by stating that the subject has a function type but erases its
input; i.e., it is of the form $K\,t$ for some $t$.

######  Definition 16.

$R\Rightarrow R^{\prime}:=K\mathbin{\ast}(R\to R^{\prime})$

Note in the following theorem the essential feature of implicit products: we
conclude by relating (with $R^{\prime}$) just $t_{1}$ and $t_{2}$, not their
applications to $x$ and $x^{\prime}$ respectively.

######  Lemma 17 (Implicit Product).

$t_{1}\ \llbracket R\Rightarrow R^{\prime}\rrbracket_{\gamma}\ t_{2}$ iff for
all $(x,x^{\prime})\in\llbracket R\rrbracket$, $t_{1}\ \llbracket
R^{\prime}\rrbracket_{\gamma}\ t_{2}$.

###### Proof.

$\begin{array}[]{l}t_{1}\ \llbracket R\Rightarrow
R^{\prime}\rrbracket_{\gamma}\ t_{2}=\\\ K\ t_{1}\ \llbracket R\to
R^{\prime}\rrbracket_{\gamma}\ K\ t_{2}\end{array}$

And the latter holds iff for all $(x,x^{\prime})\in\llbracket R\rrbracket$,
$K\ t_{1}\ x\ \llbracket R^{\prime}\rrbracket_{\gamma}\ K\ t_{2}\ x^{\prime}$.
By $\beta\eta$-Closure {2}, this is equivalent to $t_{1}\ \llbracket
R^{\prime}\rrbracket_{\gamma}\ t_{2}$. ∎

Finally, using internalized inclusion, we may neatly express equality of
relations as a type:

######  Definition 18.

$R\topdoteq R^{\prime}:=(R\subseteq R^{\prime})\cdot(R^{\prime}\subseteq R)$

######  Lemma 19 (Relational Equality).

$t_{1}\ \llbracket R\topdoteq R^{\prime}\rrbracket_{\gamma}\ t_{2}$ iff
$\llbracket R\rrbracket_{\gamma}=\llbracket R^{\prime}\rrbracket_{\gamma}$.

###### Proof.

First, suppose $t_{1}\ \llbracket R\topdoteq R^{\prime}\rrbracket_{\gamma}\
t_{2}$. Then by semantics of composition, there exists some $t$ such that

  * •

$t_{1}\ \llbracket R\subseteq R^{\prime}\rrbracket_{\gamma}\ t$, and

  * •

$t\ \llbracket R\subseteq R^{\prime}\rrbracket_{\gamma}\ t_{2}$.

Applying Subset {15}, these facts are equivalent to

  * •

$\llbracket R\rrbracket_{\gamma}\subseteq\llbracket
R^{\prime}\rrbracket_{\gamma}$, and

  * •

$\llbracket R^{\prime}\rrbracket_{\gamma}\subseteq\llbracket
R\rrbracket_{\gamma}$.

This proves the two relations are equal.

Next, suppose $\llbracket R\rrbracket_{\gamma}=\llbracket
R^{\prime}\rrbracket_{\gamma}$. Then similarly, applying Subset {15}, we may
arbitrarily choose $I$ for $t$ to satisfy

  * •

$t_{1}\ \llbracket R\subseteq R^{\prime}\rrbracket_{\gamma}\ t$, and

  * •

$t\ \llbracket R\subseteq R^{\prime}\rrbracket_{\gamma}\ t_{2}$.

which suffices, again by the semantics of composition. ∎

######  Lemma 20 (Substitutivity Of Relational Equality).

If $t_{1}\ \llbracket R\topdoteq R^{\prime}\rrbracket_{\gamma}\ t_{2}$, then
$\llbracket[R/X]R^{\prime\prime}\rrbracket_{\gamma}=\llbracket[R^{\prime}/X]R^{\prime\prime}\rrbracket_{\gamma}$

###### Proof.

The proof is by induction on $R^{\prime\prime}$, making use of Environment
Extension {7} as we induct on the bodies of universal types (in extended
environments). We omit the details, as all cases are obvious thanks to the
compositionality of the semantics (Figure 2). ∎

##  V Extensionality principles

We prove a few examples of standard type-specific extensionality principles.

######  Lemma 21 ($\eta$-Unit).

If $t\,\llbracket\forall\,X.\,X\to X\rrbracket_{\gamma}\,t^{\prime}$, then
$t\,\llbracket\forall\,X.\,X\to X\rrbracket_{\gamma}\,I$.

###### Proof.

Assume (1) $t\,\llbracket\forall\,X.\,X\to X\rrbracket_{\gamma}\,t^{\prime}$.
Next, assume $r\in\mathcal{R}$ with $y\,[r]\,y^{\prime}$. Instantiate (1) with
$\llbracket X[y^{\prime}]\rrbracket_{X\mapsto r}$ (note this is a definable
relation) to get

$t\,\llbracket X\to X\rrbracket_{\gamma[X\mapsto\llbracket
X[y^{\prime}]\rrbracket_{X\mapsto r}]}\,t^{\prime}$

Simplifying using Interpretation Over Substitution {6} and also Environment
Extension {7}, this gives us

$t\,\llbracket X[y^{\prime}]\to X[y^{\prime}]\rrbracket_{\gamma[X\mapsto
r]}\,t^{\prime}$

We may apply this to $y\,[X[y^{\prime}]]\,y^{\prime}$ which we have from (1)
by Internalized Typing {10}. This application yields

$t\,y\,\llbracket X[y^{\prime}]\rrbracket_{\gamma[X\mapsto
r]}\,t^{\prime}\,y^{\prime}$

Again applying Internalized Typing {10}, this gives us
$t\,y\,[r]\,y^{\prime}$, as required. ∎

######  Definition 22.

$\begin{array}[]{lll}R\times R^{\prime}&:=&\forall\,X.\,(R\to R^{\prime}\to
X)\to X\\\ \textit{pair}&:=&\lambda\,x.\,\lambda\,y.\,\lambda\,c.\,c\,x\,y\\\
(t,t^{\prime})&:=&\textit{pair}\ t\,t^{\prime}\\\ t.1&:=&t\
\lambda\,x.\,\lambda\,y.\,x\\\ t.2&:=&t\
\lambda\,x.\,\lambda\,y.\,y\end{array}$

######  Lemma 23 (Surjective Pairing).

If $t\,\llbracket R\times R^{\prime}\rrbracket_{\gamma}\,t^{\prime}$, then

$(t.1,t.2)\,\llbracket R\times R^{\prime}\rrbracket_{\gamma}\,t^{\prime}$

###### Proof.

Assume (1) $t\,[R\times R^{\prime}]\,t^{\prime}$. Then assume
$r\in\mathcal{R}$ and (2) $c\,\llbracket R\to R^{\prime}\to
X\rrbracket_{\gamma[X\mapsto r]}\,c^{\prime}$, and show

$\textit{pair}\,(t.1)\,(t.2)\,c\,[r]\,t^{\prime}\,c^{\prime}$ (A)

Instantiate (1) with $\llbracket\lambda\,x.\,x\,c\cdot X\rrbracket_{[X\mapsto
r]}$ (note this is a definable relation). Then (A) follows from

$\textit{pair}\,\llbracket R\to R^{\prime}\to
X\rrbracket_{\gamma[X\mapsto\llbracket\lambda\,x.\,x\,c\cdot
X\rrbracket_{[X\mapsto r]}]}\,c^{\prime}$ (B)

Let us apply Environment Extension {7} implicitly to simplify environments. To
prove (B), assume (3) $r_{1}\,\llbracket R\rrbracket_{\gamma}\,r_{1}^{\prime}$
and (4) $r_{2}\,\llbracket R^{\prime}\rrbracket_{\gamma}\,r_{2}^{\prime}$, and
show

$\textit{pair}\ r_{1}\,r_{2}\llbracket\lambda\,x.\,x\,c\cdot
X\rrbracket_{[X\mapsto r]}\,c^{\prime}\,r_{1}^{\prime}\,r_{2}^{\prime}$

By Deapplication {4}, this is equivalent to

$\textit{pair}\
r_{1}\,r_{2}\,c\,[r]\,c^{\prime}\,r_{1}^{\prime}\,r_{2}^{\prime}$

By $\beta\eta$-Closure {2}, this is equivalent to

$c\,r_{1}\,r_{2}[r]\,c^{\prime}\,r_{1}^{\prime}\,r_{2}^{\prime}$

This follows from (2), (3), and (4) by the semantics. ∎

##  VI Symmetric types

######  Definition 24.

Call a type _symmetric_ iff it does not use $R\cdot R^{\prime}$, and every
occurrence of a promotion of a term $t$ either has $t=_{\beta\eta}I$ or occurs
as $t$ in subexpressions of the form $t\mathbin{\ast}R$. Use $S$ as a
metavariable for symmetric types.

######  Definition 25.

$\gamma^{\cup}(X)=(\gamma(X))^{\cup}$; i.e., the converse of relation
$\gamma(X)$.

######  Lemma 26.

$(\gamma^{\cup})^{\cup}=\gamma$.

######  Theorem 27 (Symmetric types).

$\llbracket S\rrbracket_{\gamma}=\llbracket S^{\cup}\rrbracket_{\gamma{\cup}}$

###### Proof.

The proof is by induction on $S$.

Case $X$: $\llbracket
X\rrbracket_{\gamma}=\gamma(X)=(\gamma^{\cup})^{\cup}(X)=\llbracket
X^{\cup}\rrbracket_{\gamma^{\cup}}$.

Case $S\to S^{\prime}$: assume $t\ \llbracket S\to
S^{\prime}\rrbracket_{\gamma}\ t^{\prime}$. To show $t^{\prime}\ \llbracket
S\to S^{\prime}\rrbracket_{\gamma^{\cup}}\ t$, assume $a\ \llbracket
S\rrbracket_{\gamma^{\cup}}\ a^{\prime}$. By the IH, $a^{\prime}\ \llbracket
S\rrbracket_{\gamma}\ a$, so $t\ a^{\prime}\ \llbracket
S^{\prime}\rrbracket_{\gamma}\ t^{\prime}\ a$. By the IH again, $t^{\prime}\
a\ \llbracket S^{\prime}\rrbracket_{\gamma^{\cup}}\ t\ a^{\prime}$, as
required. Conversely, assume $t\ \llbracket S\to
S^{\prime}\rrbracket_{\gamma^{\cup}}\ t^{\prime}$, and assume $a\ \llbracket
S\rrbracket_{\gamma}\ a^{\prime}$. By the IH, $a^{\prime}\ \llbracket
S\rrbracket_{\gamma^{\cup}}\ a$, so $t\ a^{\prime}\ \llbracket
S^{\prime}\rrbracket_{\gamma^{\cup}}\ t^{\prime}\ a$. By the IH again,
$t^{\prime}\ a\ \llbracket S^{\prime}\rrbracket_{\gamma}\ t\ a^{\prime}$, as
required.

Case $\forall\,X.\,S$: assume $t\ \llbracket\forall\,X.\,S\rrbracket_{\gamma}\
t^{\prime}$, and $r\in\mathcal{R}$. So $t\ \llbracket
S\rrbracket_{\gamma[X\mapsto r^{\cup}}\ t^{\prime}$, and by the IH,
$t^{\prime}\ \llbracket S\rrbracket_{\gamma^{\cup}[X\mapsto r]}\ t$, as
required. Conversely, assume $t\
\llbracket\forall\,X.\,S\rrbracket_{\gamma^{\cup}}\ t^{\prime}$, and
$r\in\mathcal{R}$. So $t\ \llbracket S\rrbracket_{\gamma^{\cup}[X\mapsto
r^{\cup}]}\ t^{\prime}$, and by the IH, $t^{\prime}\ \llbracket
S\rrbracket_{\gamma[X\mapsto r]}\ t$, as required.

Case $S^{\cup}$: assume $t\ \llbracket S^{\cup}\rrbracket_{\gamma}\
t^{\prime}$. By the IH, $t\ \llbracket S\rrbracket_{\gamma^{\cup}}\
t^{\prime}$ as required. Conversely, assume $t\ \llbracket
S\rrbracket_{\gamma^{\cup}}\ t^{\prime}$. Then by the IH, $t\ \llbracket
S^{\cup}\rrbracket_{\gamma}\ t^{\prime}$, as required.

Case $\hat{t}\mathbin{\ast}S$: assume $t\
\llbracket\hat{t}\mathbin{\ast}S\rrbracket_{\gamma}\ t^{\prime}$. By
Conjugation {13}, this is equivalent to $\hat{t}\ t\ \llbracket
S\rrbracket_{\gamma}\ \hat{t}\ t^{\prime}$. By the IH, $\hat{t}\ t^{\prime}\
\llbracket S\rrbracket_{\gamma}\ \hat{t}\ t$, which is then similarly
equivalent to the desired typing. The converse follows similarly, applying
Symmetry Properties {3} and Relational Laws {5}.

Case $\hat{t}=_{\beta\eta}I$:

$\begin{array}[]{l}(t\ \llbracket\hat{t}\rrbracket_{\gamma}\
t^{\prime})=(\hat{t}\
t=_{\beta\eta}t^{\prime})=(t=_{\beta\eta}t^{\prime})=(t=_{\beta\eta}\hat{t}\
t^{\prime})=\\\ (t^{\prime}\ \llbracket\hat{t}\rrbracket_{\gamma}\
t)\end{array}$

∎

##  VII Transitive types

######  Definition 28.

Use metavariable $p$ to range over the set $\\{-,+\\}$ of _polarities_.
$\bar{p}$ denotes the other polarity from $p$.

The following notion extends a similar one due to Krivine [6, Section 8.5],
put also to good use in other works like [7].

######  Definition 29 ($\forall^{p}$).

Define a property $\forall^{p}$ of types inductively by the following clauses.
Type variables $X$ are $\forall^{p}$. If $R$ is $\forall^{\bar{p}}$ and
$R^{\prime}$ is $\forall^{p}$, then $R\to R^{\prime}$ is $\forall^{p}$. If $R$
is $\forall^{+}$ then so is $\forall\,X.\,R$. If $R$ is $\forall^{p}$, then so
is $R^{\cup}$. If $t=_{\beta\eta}I$, then the promotion of $t$ to a type is
$\forall^{p}$. Note that $\forall^{p}$ types are symmetric types (Definition
24). We let $P$ range over $\forall^{+}$ types, and $N$ over $\forall^{-}$
types.

Recall the following fact from classical lambda calculus (e.g., Chapter 7 of
[8]).

######  Lemma 30 (Zeta).

If $t\ x=_{\beta\eta}t^{\prime}\ x$ and $x\not\in\textit{FV}(t\,t^{\prime})$,
then $t=_{\beta\eta}t^{\prime}$.

###### Proof.

From the assumption, deduce $\lambda\,x.\,t\
x=_{\beta\eta}\lambda\,x.\,t^{\prime}\ x$. The sides of this equation are
$\eta$-equal to $t$ and $t^{\prime}$, respectively. ∎

######  Definition 31.

Let $e$ denote the environment where $e(X)$ is the relation $=_{\beta\eta}$,
for all type variables $X$.

As discussed further in Section XIII, RelTT by design does not satisfy
Identity Extension (a property proposed originally by Reynolds [9]). The
following is a partial refinement:

######  Theorem 32 (Identity Inclusion).

  1. 1.

$\llbracket P\rrbracket_{e}\subseteq\ =_{\beta\eta}$.

  2. 2.

$=_{\beta\eta}\ \subseteq\llbracket N\rrbracket_{e}$.

###### Proof.

Proceed by induction on the assumption of $R$ in $\forall^{p}$.

Case $X\in\forall^{p}$: $\llbracket X\rrbracket_{e}=e(X)$, which is
$=_{\beta\eta}$.

Case $R\to R^{\prime}\in\forall^{+}$: assume (1) $t\ \llbracket R\to
R^{\prime}\rrbracket_{e}\ t^{\prime}$. By Zeta {30}, it suffices to prove $t\
x=_{\beta\eta}t^{\prime}\ x$. Since $R\in\forall^{-}$, the IH applies to
$x=_{\beta\eta}x$ to yield $x\ \llbracket R\rrbracket_{e}\ x$. Combining this
with (1) gives $t\ x\ \llbracket R^{\prime}\rrbracket_{e}\ t^{\prime}\ x$.
Then by the IH, $t\ x=_{\beta\eta}t^{\prime}\ x$, as required.

Case $R\to R^{\prime}\in\forall^{-}$: assume (1) $t=_{\beta\eta}t^{\prime}$
and (2) $a\ \llbracket R\rrbracket_{e}\ a^{\prime}$, and show $t\ a\
\llbracket R^{\prime}\rrbracket_{e}\ t^{\prime}\ a^{\prime}$. Since
$R\in\forall^{+}$, the IH applies to (2) yielding $a=_{\beta\eta}a^{\prime}$.
Combining this with (1) gives $t\ a=_{\beta\eta}t^{\prime}\ a^{\prime}$, from
which the IH yields $t\ a\ \llbracket R^{\prime}\rrbracket_{e}\ t^{\prime}\
a^{\prime}$.

Case $\forall\,X.\,R\in\forall^{+}$: assume (1) $t\
\llbracket\forall\,X.\,R\rrbracket_{e}\ t^{\prime}$, and show
$t=_{\beta\eta}t^{\prime}$. From (1), we have $t\ \llbracket
R\rrbracket_{e[X\mapsto\ =_{\beta\eta}]}\ t^{\prime}$. By the IH, this yields
$t=_{\beta\eta}t^{\prime}$, as required.

Case $R^{\cup}\in\forall^{+}$: assume $t\ \llbracket R^{\cup}\rrbracket_{e}\
t^{\prime}$, which implies $t^{\prime}\ \llbracket R\rrbracket_{e}\ t$. By the
IH, $t^{\prime}=_{\beta\eta}t$, hence $t=_{\beta\eta}t^{\prime}$ as required.

Case $R^{\cup}\in\forall^{-}$: assume $t=_{\beta\eta}t^{\prime}$, hence
$t^{\prime}=_{\beta\eta}t$. By the IH, $t^{\prime}\ \llbracket
R\rrbracket_{e}\ t$, which equals the required $t\ \llbracket
R^{\cup}\rrbracket_{e}\ t^{\prime}$.

Case $\hat{t}\in\forall^{p}$: $\llbracket\hat{t}\rrbracket_{e}$ is then just
$=_{\beta\eta}$.

∎

Using the terminology of [10], Identity Inclusion {32} identifies
$\forall^{+}$ types as _extensive_ (they are included in the equality
relation), and $\forall^{-}$ types as _parametric_ (the equality relation is
included in them).

######  Lemma 33 (Transitivity For $\forall^{+}$-Types).

$I\ \llbracket P\cdot P\to P\rrbracket_{e}\ I$.

###### Proof.

Assume (1) $x\ \llbracket R\rrbracket_{e}\ y$ and (2) $y\ \llbracket
R\rrbracket_{e}\ z$, and show $x\ \llbracket R\rrbracket_{e}\ z$. By Identity
Inclusion {32}, (1) implies $x\ =_{\beta\eta}\ y$. From this and (2),
$\beta\eta$-Closure {2} yields the desired conclusion. ∎

######  Corollary 34 ($\forall^{+}$ Per).

If $R$ is $\forall^{+}$ and closed, then $\llbracket R\rrbracket_{\gamma}$ is
a partial equivalence relation (i.e., symmetric and transitive; abbreviated
per).

###### Proof.

Since $R$ is closed, $\llbracket R\rrbracket_{\gamma}=\llbracket
R\rrbracket_{e}$ by Environment Extension {7}. Transitivity for
$\forall^{+}$-Types {33} then implies transitivity. Symmetry follows from
Symmetric Types {27}, since $\forall^{+}$ types are symmetric types
(Definition 24). ∎

######  Definition 35 (simple transitive types).

Simple transitive types $T$ are defined by the following grammar:

$T\ ::=\ P\ |\ P\to T\ |\ N\to T\ |\ t\mathbin{\ast}T$

######  Lemma 36 (transitivity for simple transitive types).

$I\ \llbracket T\cdot T\to T\rrbracket_{e}I$

###### Proof.

The proof is by induction on $T$, in each case assuming (1) $x\ \llbracket
T\rrbracket_{\gamma}\ y$ and (2) $y\ \llbracket T\rrbracket_{\gamma}\ z$.

Case $P$: Transitivity for $\forall^{+}$-Types {33}.

Case $P\to T$: assume (3) $a\ \llbracket P\rrbracket_{e}\ a^{\prime}$. By
Symmetric Types {27}, $a^{\prime}\ \llbracket P\rrbracket_{e}\ a$ (as
$e^{\cup}=e$). By Transitivity for $\forall^{+}$-Types {33}, this can be
combined with (3) to obtain $a\ \llbracket P\rrbracket_{e}\ a$. Using this
with (1), $x\ a\ \llbracket T\rrbracket_{e}\ y\ a$. Using (3) with (2), $y\ a\
\llbracket T\rrbracket_{e}\ z\ a^{\prime}$. By the induction hypothesis, $x\
a\ \llbracket T\rrbracket_{e}\ z\ a^{\prime}$ as required.

Case $N\to T$: assume (3) $a\ \llbracket N\rrbracket_{e}\ a^{\prime}$. By
Identity Inclusion {32}, since $N$ is $\forall^{-}$, $a\ \llbracket
N\rrbracket_{e}\ a$ (since $a=_{\beta\eta}a$). Using this with (1), $x\ a\
\llbracket T\rrbracket_{e}\ y\ a$. Then as in the previous case, we obtain $y\
a\ \llbracket T\rrbracket_{e}\ z\ a^{\prime}$ using (3) with (2), and the
required $x\ a\ \llbracket T\rrbracket_{e}\ z\ a^{\prime}$ by the induction
hypothesis.

Case $\hat{t}\mathbin{\ast}T$: by Conjugation {13}, it suffices to show
$\hat{t}\ x\ \llbracket T\rrbracket_{\gamma}\ \hat{t}\ z$. This follows by the
IH from assumptions (1) and (2), since these are equivalent to $\hat{t}\ x\
\llbracket T\rrbracket_{\gamma}\ \hat{t}\ y$ and $\hat{t}\ y\ \llbracket
T\rrbracket_{\gamma}\ \hat{t}\ z$ by Conjugation {13}. ∎

##  VIII A relational proof system

Figure 6 presents a proof system, RelPf, for judgments of the form
$\Gamma\vdash t\ [R]\ t^{\prime}$. (Here, the square brackets are part of the
syntax for the judgment; in our meta-language, we are using them for
application of a mathematical relation.) RelPf Soundness {40} below shows that
this system is sound with respect to the semantics of Figure 2 (extended for
contexts). In Section XII, we will develop a type theory based on RelPf, but
introduce the proof system here because the fragment for System F types will
be useful in Section X on inductive types. A few details:

  * •

typing contexts $\Gamma$ are described by the grammar

$\Gamma\ ::=\ \cdot\ |\ \Gamma,t\,[R]\,t^{\prime}$

We may elide $\cdot$ in examples.

  * •

There is an introduction and elimination rule for each connective.

  * •

The introduction rule for term promotions is the axiom $\Gamma\vdash
t\,[t^{\prime}]\,t^{\prime}\,t$. This states that $t$ is related to
$t^{\prime}\,t$ by the relation (i.e., term promotion) $t^{\prime}$.

  * •

The rule allowing to change the sides of the relational typing to
$\beta\eta$-equal terms is called _conversion_. While $\beta\eta$-equality is
undecidable in general, we may view the side conditions on conversion as
license for an implementation to check reductions to as deep a finite depth as
desired. So we view reduction as being implicitly bounded in applications of
this rule, making type-checking decidable. We do not formalize bounded
reduction.

$\Gamma\vdash
x\,[R]\,y^{\prime}\Gamma\vdash\textit{tt}\,x\,y\,[R]\,\textit{ff}\,x^{\prime}\,y^{\prime}\lx@proof@logical@and\Gamma\vdash\textit{tt}\,x\,[R\to
R]\,\textit{ff}\,x^{\prime}\,y^{\prime}\lx@proof@logical@and\Gamma\vdash\textit{tt}\,[R\to
R\to R]\,\textit{ff}\Gamma\vdash\textit{tt}\,[\textit{Bool}]\,\textit{ff}\
\Gamma\vdash x\,[R]\,x^{\prime}\ \Gamma\vdash y\,[R]\,y^{\prime}\ $ Figure 4:
Derivation of True Different From False {38}. The final inference is by the
conversion rule, noting $\textit{tt}\,x\,y=_{\beta\eta}x$ and
$\textit{ff}\,x^{\prime}\,y^{\prime}=_{\beta\eta}y^{\prime}$
$\begin{array}[]{ll}\Gamma\vdash
x:Tx:T\in\Gamma&\Gamma\vdash\lambda\,x.\,t:T\to T^{\prime}\Gamma,x:T\vdash
t:T^{\prime}\\\ \\\ \Gamma\vdash t\
t^{\prime}:T\lx@proof@logical@and\Gamma\vdash t:T^{\prime}\to T\Gamma\vdash
t^{\prime}:T^{\prime}&\Gamma\vdash
t:\forall\,X.\,T\lx@proof@logical@and\Gamma\vdash
t:TX\not\in\textit{FV}(\Gamma)\\\ \\\ \Gamma\vdash
t:[T^{\prime}/X]T\Gamma\vdash t:\forall\,X.\,T&\end{array}$ Figure 5: Typing
rules for Curry-style System F

$\begin{array}[]{lllll}\Gamma\vdash
t\,[R]\,t^{\prime}t\,[R]\,t^{\prime}\in\Gamma&&\Gamma\vdash\lambda\,x.\,t\,[R\to
R^{\prime}]\,\lambda\,x^{\prime}.\,t^{\prime}\lx@proof@logical@and\Gamma,x\,[R]\,x^{\prime}\vdash
t\,[R^{\prime}]\,t^{\prime}(*)&&\Gamma\vdash
t\,t_{1}\,[R^{\prime}]\,t^{\prime}\,t_{2}\lx@proof@logical@and\Gamma\vdash
t\,[R\to R^{\prime}]\,t^{\prime}\Gamma\vdash t_{1}\,[R]\,t_{2}\par\\\ \\\
\Gamma\vdash t\,[[R/X]R^{\prime}]\,t^{\prime}\Gamma\vdash
t\,[\forall\,X.\,R^{\prime}]\,t^{\prime}&&\Gamma\vdash
t\,[\forall\,X.\,R]\,t^{\prime}\lx@proof@logical@and\Gamma\vdash
t\,[R]\,t^{\prime}X\not\in\textit{FV}(\Gamma)\par&&\Gamma\vdash
t_{1}^{\prime}\,[R]\,t_{2}^{\prime}\lx@proof@logical@and\Gamma\vdash
t_{1}\,[R]\,t_{2}t_{1}=_{\beta\eta}t_{1}^{\prime}t_{2}=_{\beta\eta}t_{2}^{\prime}\par\\\
\\\ \Gamma\vdash t\,[R^{\cup}]\,t^{\prime}\Gamma\vdash
t^{\prime}\,[R]\,t&&\Gamma\vdash t^{\prime}\,[R]\,t\Gamma\vdash
t\,[R^{\cup}]\,t^{\prime}\par\ \ \ \ \par\Gamma\vdash
t\,[t^{\prime}]\,t^{\prime}\ t\
\par&&\Gamma\vdash[t^{\prime\prime}\,t/x]t_{1}\,[R]\,[t^{\prime\prime}\,t/x]t_{2}\lx@proof@logical@and\Gamma\vdash
t\,[t^{\prime\prime}]\,t^{\prime}\Gamma\vdash[t^{\prime}/x]t_{1}\,[R]\,[t^{\prime}/x]t_{2}\\\
\\\ \lx@intercol\Gamma\vdash
t_{1}\,[R^{\prime\prime}]\,t_{2}\lx@proof@logical@and\Gamma\vdash t\,[R\cdot
R^{\prime}]\,t^{\prime}\Gamma,t\,[R]\,x,x\,[R^{\prime}]\,t^{\prime}\vdash
t_{1}\,[R^{\prime\prime}]\,t_{2}(**)\hfil\lx@intercol&&\Gamma\vdash t\,[R\cdot
R^{\prime}]\,t^{\prime}\lx@proof@logical@and\Gamma\vdash
t\,[R]\,t^{\prime\prime}\Gamma\vdash
t^{\prime\prime}\,[R^{\prime}]\,t^{\prime}\par\end{array}$

Side condition (*) is $x\not\in\textit{FV}(\Gamma,R,R^{\prime})$.

Side condition (**) is
$x\not\in\textit{FV}(\Gamma,t_{1},t_{2},t,t^{\prime},R,R^{\prime},R^{\prime\prime})$.

Figure 6: Proof system for relational typing.

Here is an example in RelPf, deriving a form of inconsistency from an
assumption that different constructors of an inductive type are equal. It
states that if _tt_ and _ff_ are equal as booleans, then any relation $R$ is
trivial in the sense that $R=\textit{dom}(R)\times\textit{ran}(R)$.

######  Definition 37.

$\begin{array}[]{lll}\textit{Bool}&:=&\forall\,X.\,X\to X\to X\\\
\textit{tt}&:=&\lambda\,x.\,\lambda\,y.\,x\\\
\textit{ff}&:=&\lambda\,x.\,\lambda\,y.\,y\end{array}$

######  Lemma 38 (True Different From False).

For any type $R$, let $\Gamma$ be a context with the following assumptions:

  1. 1.

$\textit{tt}\,[\textit{Bool}]\,\textit{ff}$

  2. 2.

$x\,[R]\,x^{\prime}$

  3. 3.

$y\,[R]\,y^{\prime}$

Then $\Gamma\vdash x\,[R]\,y^{\prime}$.

###### Proof.

A derivation is in Figure 4. ∎

Turning now to meta-theory: let $\sigma$ range over term substitutions (finite
functions from term variables to terms). Denote capture-avoiding application
of a substitution $\sigma$ to a term $t$ as $\sigma\ t$. Apply substitutions
$\sigma$ to types $R$ by applying them to all terms contained in $R$. Now we
will define an interpretation of contexts $\Gamma$ as sets of substitutions
satisfying the contexts constraints.

######  Definition 39.

$\llbracket\Gamma\rrbracket_{\gamma}$ is defined by recursion on $\Gamma$:

$\begin{array}[]{lll}\sigma\in\llbracket\Gamma,t\,[R]\,t^{\prime}\rrbracket_{\gamma}&=&\sigma\in\llbracket\Gamma\rrbracket_{\gamma}\
\wedge\ \sigma t\,\llbracket\sigma R\rrbracket_{\gamma}\,\sigma t^{\prime}\\\
\sigma\in\llbracket\cdot\rrbracket_{\gamma}&=&\textit{True}\end{array}$

######  Theorem 40 (RelPf Soundness).

Suppose $\gamma$ is defined on all free type variables of $\Gamma$ and $R$. If
$\Gamma\vdash t\,[R]\,t^{\prime}$, and
$\sigma\in\llbracket\Gamma\rrbracket_{\gamma}$, then $\sigma\
t\,\llbracket\sigma\,R\rrbracket_{\gamma}\,\sigma\ t^{\prime}$.

###### Proof.

The proof is by induction on the RelPf derivation. In each case we assume
arbitrary $\sigma\in\llbracket\Gamma\rrbracket_{\gamma}$.

Case:

$\Gamma\vdash t\,[R]\,t^{\prime}t\,[R]\,t^{\prime}\in\Gamma$

From $t\,[R]\,t^{\prime}\in\Gamma$ we obtain the desired
$\sigma\,t\,\llbracket\sigma\,R\rrbracket_{\gamma}\sigma\,t^{\prime}$ from the
semantics of contexts.

Case:

$\Gamma\vdash\lambda\,x.\,t\,[R\to
R^{\prime}]\,\lambda\,x^{\prime}.\,t^{\prime}\lx@proof@logical@and\Gamma,x\,[R]\,x^{\prime}\vdash
t\,[R^{\prime}]\,t^{\prime}(*)$

Assume arbitrary $t_{1}$ and $t_{2}$ with (1)
$t_{1}\,\llbracket\sigma\,R\rrbracket_{\gamma}\,t_{2}$. Let $\sigma^{\prime}$
denote $\sigma[x\mapsto t_{1},x^{\prime}\mapsto t_{2}]$. By the IH,

$\sigma^{\prime}\,t\llbracket\sigma^{\prime}\,R^{\prime}\rrbracket_{\gamma}\,\sigma^{\prime}\,t^{\prime}$

By side condition (*), $\sigma^{\prime}\,R^{\prime}=\sigma\,R$. Applying then
$\beta\eta$-Closure {2}, we have

$(\sigma\,\lambda\,x.\,t)\,t_{1}\llbracket\sigma\,R^{\prime}\rrbracket_{\gamma}\,(\sigma\,\lambda\,x^{\prime}.\,t^{\prime})\,t_{2}$

By the semantics of arrow types, the fact that this holds for all $t_{1}$ and
$t_{2}$ satisfying (1) implies the desired
$\sigma\,\lambda\,x.\,t\,\llbracket\sigma\,(R\to
R^{\prime})\rrbracket_{\gamma}\,\sigma\,\lambda\,x^{\prime}.\,t^{\prime}$.

Case:

$\Gamma\vdash
t\,t_{1}\,[R^{\prime}]\,t^{\prime}\,t_{2}\lx@proof@logical@and\Gamma\vdash
t\,[R\to R^{\prime}]\,t^{\prime}\Gamma\vdash t_{1}\,[R]\,t_{2}$

By the IH, $\sigma\,t\,\llbracket R\to
R^{\prime}\rrbracket_{\gamma}\,\sigma\,t^{\prime}$ and
$\sigma\,t_{1}\,\llbracket R\rrbracket_{\gamma}\,\sigma\,t_{2}$. The semantics
of arrow types then gives the desired $\sigma\,(t\,t_{1})\,\llbracket
R^{\prime}\rrbracket_{\gamma}\,\sigma\,(t^{\prime}\,t_{2})$.

Case:

$\Gamma\vdash t\,[[R/X]R^{\prime}]\,t^{\prime}\Gamma\vdash
t\,[\forall\,X.\,R^{\prime}]\,t^{\prime}$

By the IH, we have (1)
$\sigma\,t\,\llbracket\sigma\,\forall\,X.\,R^{\prime}\rrbracket_{\gamma}\,\sigma\,t^{\prime}$.
By the condition on $\gamma$, $\llbracket R\rrbracket_{\gamma}$ is defined,
and we use it to instantiate (1). This gives

$\sigma\,t\,\llbracket\sigma\,R^{\prime}\rrbracket_{\gamma[X\mapsto\llbracket
R\rrbracket_{\gamma}]}\,\sigma\,t^{\prime}$

By Interpretation Over Substitution {6}, this implies the desired

$\sigma\,t\,\llbracket\sigma\,[R/X]R^{\prime}\rrbracket_{\gamma}\,\sigma\,t^{\prime}$

Case:

$\Gamma\vdash t\,[\forall\,X.\,R]\,t^{\prime}\lx@proof@logical@and\Gamma\vdash
t\,[R]\,t^{\prime}X\not\in\textit{FV}(\Gamma)$

Assume arbitrary $r\in\mathcal{R}$. Then by the IH,
$\sigma\,t\,\llbracket\sigma\,R\rrbracket_{\gamma[X\mapsto
r]}\,\sigma^{\prime}\,t^{\prime}$. The desired
$\sigma\,t\,\llbracket\sigma\,\forall\,X.\,R\rrbracket_{\gamma}\,\sigma^{\prime}\,t^{\prime}$
then follows by the semantics of universal quantification.

Case:

$\Gamma\vdash
t_{1}^{\prime}\,[R]\,t_{2}^{\prime}\lx@proof@logical@and\Gamma\vdash
t_{1}\,[R]\,t_{2}t_{1}=_{\beta\eta}t_{1}^{\prime}t_{2}=_{\beta\eta}t_{2}^{\prime}$

This case follows easily by the IH and $\beta\eta$-Closure {2}.

Case:

$\Gamma\vdash t\,[R^{\cup}]\,t^{\prime}\Gamma\vdash t^{\prime}\,[R]\,t$

By the IH, $\sigma\,t^{\prime}\llbracket R\rrbracket_{\gamma}\sigma\,t$. By
the semantics of converse, this implies the required $\sigma\,t\llbracket
R^{\cup}\rrbracket_{\gamma}\sigma\,t^{\prime}$.

Case:

$\Gamma\vdash t^{\prime}\,[R]\,t\Gamma\vdash t\,[R^{\cup}]\,t^{\prime}$

By the IH, $\sigma\,t\llbracket
R^{\cup}\rrbracket_{\gamma}\sigma\,t^{\prime}$. By the semantics of converse,
this implies the required $\sigma\,t^{\prime}\llbracket
R\rrbracket_{\gamma}\sigma\,t$.

Case:

$\Gamma\vdash t\,[t^{\prime}]\,t^{\prime}\ t\ $

The desired conclusion is equivalent to
$\sigma\,(t^{\prime}\,t)=_{\beta\eta}\sigma\,(t^{\prime}\ t)$, which holds.

Case:

$\Gamma\vdash[t^{\prime\prime}\,t/x]t_{1}\,[R]\,[t^{\prime\prime}\,t/x]t_{2}\lx@proof@logical@and\Gamma\vdash
t\,[t^{\prime\prime}]\,t^{\prime}\Gamma\vdash[t^{\prime}/x]t_{1}\,[R]\,[t^{\prime}/x]t_{2}$

By the IH, we have

  * •

$\sigma\,(t^{\prime\prime}\,t)=_{\beta\eta}\sigma\,t^{\prime}$

  * •

$\sigma\,[t^{\prime}/x]t_{1}\,\llbracket\sigma\,R\rrbracket_{\gamma}\,\sigma\,[t^{\prime}/x]t_{2}$

Using basic properties of $\beta\eta$-equivalence and substitution, these
facts imply the desired

$\sigma\,[t^{\prime\prime}\,t/x]t_{1}\,\llbracket\sigma\,R\rrbracket_{\gamma}\,\sigma\,[t^{\prime\prime}\,t/x]t_{2}$

Case:

$\Gamma\vdash
t_{1}\,[R^{\prime\prime}]\,t_{2}\lx@proof@logical@and\Gamma\vdash t\,[R\cdot
R^{\prime}]\,t^{\prime}\Gamma,t\,[R]\,x,x\,[R^{\prime}]\,t^{\prime}\vdash
t_{1}\,[R^{\prime\prime}]\,t_{2}(**)$

By the IH and semantics for composition we have that there exists
$t^{\prime\prime}$ such that

  * (1)

$\sigma\,t\,\llbracket\sigma\,R\rrbracket_{\gamma}\,t^{\prime\prime}$

  * (2)

$t^{\prime\prime}\,\llbracket\sigma\,R^{\prime}\rrbracket_{\gamma}\,\sigma\,t^{\prime}$

Let $\sigma^{\prime}$ denote $\sigma[x\mapsto t^{\prime\prime}]$. Using (1)
and (2), we may prove that $\sigma^{\prime}$ is in the interpretation of the
context in the right premise of the inference. Side condition (**) is used to
deduce that $\sigma^{\prime}$ satisfies the two constraints added to $\Gamma$
in that context, from (1) and (2) (where only $\sigma$ appears). Then by the
IH and (**), we have the required

$\sigma\,t_{1}\,\llbracket\sigma\,R^{\prime\prime}\rrbracket_{\gamma}\,\sigma\,t_{2}$

Case:

$\Gamma\vdash t\,[R\cdot
R^{\prime}]\,t^{\prime}\lx@proof@logical@and\Gamma\vdash
t\,[R]\,t^{\prime\prime}\Gamma\vdash
t^{\prime\prime}\,[R^{\prime}]\,t^{\prime}$

By the IH, we have

  * •

$\sigma\,t\,\llbracket\sigma\,R\rrbracket_{\gamma}\,\sigma\,t^{\prime\prime}$

  * •

$\sigma\,t^{\prime\prime}\,\llbracket\sigma\,R^{\prime}\rrbracket_{\gamma}\,\sigma\,t^{\prime}$

These imply the desired $\sigma\,t\,\llbracket\sigma\,(R\cdot
R^{\prime})\rrbracket_{\gamma}\,\sigma\,t^{\prime}$ by the semantics of
composition.

∎

##  IX Embedding System F

Similar to the Abstraction Theorem of Reynolds [9], we may prove that each
term typable in System F is related to itself by the relational interpretation
of its type. Figure 5 recalls the typing rules of Curry-style System F (also
known as $\lambda 2$-Curry [11]). We consider the set of types of System F a
subset of the set of relational types (Figure 1). We first show that typing
derivations in System F can be translated to RelTT in the obvious way. Then we
may appeal to RelTT Soundness {40}.

######  Definition 41.

Partition the set of variables by an injection $\dot{-}$. Assume $t$ does not
contain any variables of the form $\dot{x}$ with $x\in\textit{FV}(t)$. Then
let $\dot{t}$ be the term where every variable $x$ (free or bound) is renamed
to $\dot{x}$.

######  Definition 42.

Define $\ulcorner-\urcorner$ recursively on typing contexts $\Gamma$ of System
F by:

$\begin{array}[]{lll}\ulcorner\cdot\urcorner&=&\cdot\\\
\ulcorner\Gamma,x:T\urcorner&=&\ulcorner\Gamma\urcorner,x\,[T]\,\dot{x}\end{array}$

######  Theorem 43 (Soundness Of System F).

If $\Gamma\vdash t:T$ (in System F), then $\ulcorner\Gamma\urcorner\vdash t\
[T]\ \dot{t}$ (in RelPf), assuming $\dot{t}$ is defined.

###### Proof.

The proof is by induction on the typing derivation in System F.

Case:

$\Gamma\vdash x:Tx:T\in\Gamma$

From $x:T\in\Gamma$ we derive $x\,[T]\,\dot{x}\in\ulcorner\Gamma\urcorner$,
and conclude using the assumption rule of RelPf.

Case:

$\Gamma\vdash\lambda\,x.\,t:T\to T^{\prime}\Gamma,x:T\vdash t:T^{\prime}$

By the IH, we have

$\ulcorner\Gamma\urcorner,x\,[T]\,\dot{x}\vdash t\,[T^{\prime}]\,\dot{t}$

From this, use arrow introduction (of RelPf) to derive the desired

$\ulcorner\Gamma\urcorner\vdash\lambda\,x.\,t\,[T\to
T^{\prime}]\,\lambda\,\dot{x}.\,\dot{t}$

Case:

$\Gamma\vdash t\ t^{\prime}:T\lx@proof@logical@and\Gamma\vdash t:T^{\prime}\to
T\Gamma\vdash t^{\prime}:T^{\prime}$

By the IH we have

$\begin{array}[]{l}\ulcorner\Gamma\urcorner\vdash t\,[T^{\prime}\to
T]\,\dot{t}\\\ \ulcorner\Gamma\urcorner\vdash
t^{\prime}\,[T^{\prime}]\,\dot{t^{\prime}}\end{array}$

Use arrow elimination (of RelPf) to deduce the desired

$\ulcorner\Gamma\urcorner\vdash t\,t^{\prime}\,[T]\,\dot{t\,t^{\prime}}$

Case:

$\Gamma\vdash t:\forall\,X.\,T\lx@proof@logical@and\Gamma\vdash
t:TX\not\in\textit{FV}(\Gamma)$

By the IH, we have $\ulcorner\Gamma\urcorner\vdash t\,[T]\,\dot{t}$. Apply
forall introduction (of RelPf) to conclude the desired
$\ulcorner\Gamma\urcorner\vdash t\,[\forall\,X.\,T]\,\dot{t}$

Case:

$\Gamma\vdash t:[T^{\prime}/X]T\Gamma\vdash t:\forall\,X.\,T$

By the IH, we have $\ulcorner\Gamma\urcorner\vdash
t\,[\forall\,X.\,T]\,\dot{t}$. Apply forall elimination (of RelPf) to conclude
the desired $\ulcorner\Gamma\urcorner\vdash t\,[[T^{\prime}/X]T]\,\dot{t}$.

∎

######  Corollary 44 (Soundness Of System F For Closed Terms).

If $\cdot\vdash t:T$ (in System F), then $t\ \llbracket T\rrbracket_{\gamma}\
t$.

###### Proof.

Use Soundness of System F {43} (noting that $t=_{\alpha}\dot{t}$ since $t$
closed), and then RelTT Soundness {40}. ∎

Below we will also need this basic syntactic property:

######  Proposition 45 (Weakening for System F).

If $\Gamma_{1},\Gamma_{2}\vdash t:T$, then $\Gamma_{1},x:R,\Gamma_{2}\vdash
t:T$ where $x$ is not declared in $\Gamma_{1},\Gamma_{2}$.

##  X Inductive types

Following a relational, and functorial, generalization of [10], this section
shows how to derive a relational form of induction within RelTT. For this
section, except as noted in Section X-A, let $R$ be a type of System F,
possibly containing specified variable $X$ free. Under the usual requirement
of positivity, we prove equal the following two relational types, where in the
second one, we make use of our notation for internalized typing (Definition
9):

######  Definition 46.

  * •

$D_{\textit{param}}:=\forall\,X.\,(R\to X)\to X$

  * •

$D_{\textit{ind}}:=\forall\,X.\,([\textit{in}_{X,R}]\,(R\to
X)\,[\textit{in}_{X,R}])\Rightarrow X$

$\textit{in}_{X,R}$ represents the constructors of the inductive datatype in a
standard way, and is defined below (Definition 54).

###  X-A Variable Polarity and Monotonicity

The first step to proving equality of $D_{\textit{param}}$ and
$D_{\textit{ind}}$ is to extend the usual notion of a type variable’s
occurring free only positively or only negatively, to relational types (recall
Definition 28 for polarities $p$). For inductive types, our results hold only
for $\forall^{+}$ types of System F. For positive-recursive types, however
(Section XI), our derivation works for any relational type $R$. So we begin by
defining when a variable occurs only with polarity $p$ ($X\in^{p}R$) generally
for any relational type $R$:

######  Definition 47.

Define $X\in^{p}R$ inductively by the clauses:

  * •

$X\in^{+}X$

  * •

$X\in^{p}Y$

  * •

$X\in^{p}(R\to R^{\prime})$ iff $X\in^{\bar{p}}R$ and $X\in^{p}R^{\prime}$

  * •

$X\in^{p}\forall\,Y.\,R$ iff $X\in^{p}R$

  * •

$X\in^{p}(R\cdot R^{\prime})$ iff $X\in^{p}R$ and $X\in^{p}R^{\prime}$

  * •

$X\in^{p}(R^{\cup})$ iff $X\in^{p}R$

  * •

$X\in^{p}t$

(The intention is that $X\in^{+}R$ means $X$ occurs only positively in $R$,
and $X\in^{-}R$ only negatively.) The following form of monotonicity then
holds for any relational type. The statement of the lemma using a polarity
meta-variable $p$ consolidates many dual cases in the proof (cf. [12]).

######  Lemma 48 (Monotonicity).

Suppose $r_{+}$ and $r_{-}$ are in $\mathcal{R}$, with $r_{+}\subseteq r_{-}$.
If $X\in^{p}R$, then $\llbracket R\rrbracket_{\gamma[X\mapsto
r_{p}]}\subseteq\llbracket R\rrbracket_{\gamma[X\mapsto r_{\bar{p}}]}$.

###### Proof.

The proof is by induction on $X\in^{p}R$, assuming (1) $r_{+}\subseteq r_{-}$
and (2) $t_{1}\ \llbracket R\rrbracket_{\gamma[X\mapsto r_{p}]}\ t_{2}$.

Case $X\in^{+}X$: by (1).

Case $X\in^{p}Y$: by (2), as $\llbracket Y\rrbracket_{\gamma[X\mapsto
r_{p}]}=\llbracket Y\rrbracket_{\gamma}=\llbracket
Y\rrbracket_{\gamma[X\mapsto r_{\bar{p}}]}$.

Case $X\in^{p}(R_{1}\to R_{2})$: assume (3) $t_{a}\ \llbracket
R_{1}\rrbracket_{\gamma[X\mapsto r_{\bar{p}}]}\ t_{b}$. From this, the IH for
$R_{1}$ gives $t_{a}\ \llbracket R_{1}\rrbracket_{\gamma[X\mapsto r_{p}]}\
t_{b}$ (instantiating the quantified polarity in the IH with $\bar{p}$).
Combine this with (2) to obtain $t_{1}\ t_{a}\ \llbracket
R_{2}\rrbracket_{\gamma[X\mapsto r_{p}]}\ t_{2}\ t_{b}$. From this, the IH for
$R_{2}$ gives $t_{1}\ t_{a}\ \llbracket R_{2}\rrbracket_{\gamma[X\mapsto
r_{\bar{p}}]}\ t_{2}\ t_{b}$, as required.

Case $X\in^{p}\forall\,Y.\,R^{\prime}$: assume $r\in\mathcal{R}$, and
instantiate (2) with $r$. Then apply the IH to obtain the required $t_{1}\
\llbracket R^{\prime}\rrbracket_{\gamma[X\mapsto r_{\bar{p}},Y\mapsto r]}\
t_{2}$.

Case $X\in^{p}(R_{1}\cdot R_{2})$: (2) implies that there exists $t$ such that
$t_{1}\ \llbracket R_{1}\rrbracket_{\gamma[X\mapsto r_{P}]}\ t$ and $t\
\llbracket R_{2}\rrbracket_{\gamma[X\mapsto r_{p}]}\ t_{2}$. Applying the IH,
we obtain $t_{1}\ \llbracket R_{1}\rrbracket_{\gamma[X\mapsto r_{\bar{P}}]}\
t$ and $t\ \llbracket R_{2}\rrbracket_{\gamma[X\mapsto r_{\bar{p}}]}\ t_{2}$,
which suffices.

Case $X\in^{p}(R_{a}^{\cup})$: (2) implies $t_{2}\ \llbracket
R_{a}\rrbracket_{\gamma[X\mapsto r_{p}]}\ t_{1}$. From this, the IH gives
$t_{2}\ \llbracket R_{a}\rrbracket_{\gamma[X\mapsto r_{\bar{p}}]}\ t_{1}$,
which suffices.

Case $X\in^{p}t$: by (2), as $\llbracket t\rrbracket_{\gamma[X\mapsto
r_{p}]}=\llbracket t\rrbracket_{\gamma}=\llbracket
t\rrbracket_{\gamma[X\mapsto r_{\bar{p}}]}$.

∎

###  X-B Fmap, Fold, and In

Following a standard approach to derivation of inductive types (cf. [13]), we
will define operations $\textit{fmap}_{X,R}$, fold, and finally
$\textit{in}_{X,R}$, and prove relational typings about them. Because we will
be considering terms related to themselves, it is convenient to introduce
notation $t::r$:

######  Definition 49.

$(t::r):=t\ [r]\ t$

######  Definition 50.

Define a term $\textit{fmap}_{X,R}$ by recursion on types $R$ of System F
(also, recall Figure 3):

$\begin{array}[]{lll}\textit{fmap}_{X,X}&=&I\\\ \textit{fmap}_{X,Y}&=&K\ I\\\
\textit{fmap}_{X,R\to
R^{\prime}}&=&\lambda\,f.\,\lambda\,a.\,\textit{fmap}_{X,R^{\prime}}\ f\ \circ
a\circ\textit{fmap}_{X,R}\ f\\\
\textit{fmap}_{X,\forall\,Y.\,R}&=&\lambda\,f.\,\textit{fmap}_{X,R}\
f\end{array}$

Note that as we treat expressions up to $\alpha$-equivalence, we do not need a
case for $\textit{fmap}_{X,\forall\,X.\,R}$, as this will be handled as
$\textit{fmap}_{X,\forall\,Y.\,[Y/X]R}$.

######  Lemma 51 (Fmap (System F)).

Suppose $X_{+}$ and $X_{-}$ are type variables. Suppose
$X_{p}\not\in\textit{FV}(R)$, for all $p$. If $X\in^{p}R$, then in System F we
have

$\cdot\vdash\textit{fmap}_{X,R}:(X_{+}\to
X_{-})\to[X_{p}/X]R\to[X_{\bar{p}}/X]R$

###### Proof.

The proof is by induction on $X\in^{p}R$, implicitly applying Weakening for
System F {45}.

Case $X\in^{+}X$: the goal is

$\cdot\vdash I:(X_{+}\to X_{-})\to(X_{+}\to X_{-})$

which is derivable.

Case $X\in^{p}Y$: the goal is

$\cdot\vdash K\ I:(X_{+}\to X_{-})\to(Y\to Y)$

which is derivable.

Case $X\in^{p}(R_{1}\to R_{2})$: let $\Gamma$ be the context

$f:(X_{+}\to X_{-}),a:[X_{p}/X](R_{1}\to R_{2}),x:[X_{\bar{p}}/X]R_{1}$

Using the typing rules of System F, it suffices to show

$\Gamma\vdash\textit{fmap}_{X,R_{2}}\ f\ (a\ (\textit{fmap}_{X,R_{1}}\ f\
x)):[X_{\bar{p}}/X]R_{2}$

By the IH, since $X\in^{\bar{p}}R_{1}$, we have

$\cdot\vdash\textit{fmap}_{X,R_{1}}:(X_{+}\to
X_{-})\to([X_{\bar{p}}/X]R_{1}\to[X_{p}/X]R_{1}$

Hence we may derive

$\cdot\vdash(\textit{fmap}_{X,R_{2}}\ f\ x):[X_{p}/X]R_{1}$

and then $\cdot\vdash a\ (\textit{fmap}_{X,R_{2}}\ f\ x):[X_{p}/X]R_{2}$. From
this, using the IH with $X\in^{p}R_{2}$, we obtain the desired goal.

Case $X\in^{p}\forall\,Y.\,R$: by the IH we have

$\cdot\vdash\textit{fmap}_{X,R}:(X_{+}\to
X_{-})\to[X_{p}/X]R\to[X_{\bar{p}}/X]R$

From this we obtain

$f:(X_{+}\to X_{-})\vdash\textit{fmap}_{X,R}\ f:[X_{p}/X]R\to[X_{\bar{p}}/X]R$

Applying $\forall$-introduction, we get

$f:(X_{+}\to X_{-})\vdash\textit{fmap}_{X,R}\
f:\forall\,Y.\,[X_{p}/X]R\to[X_{\bar{p}}/X]R$

Applying $\to$-introduction gives the desired conclusion (note we needed the
$\eta$-expanded definition of $\textit{fmap}_{X,\forall\,Y.\,R}$).

∎

######  Definition 52 (Fold).

$\textit{fold}\ :=\ \lambda\,a.\,\lambda\,x.\,x\ a$

######  Lemma 53 (Fold).

Let $X$ be possibly free in $R$. Then in System F:

$\cdot\vdash\textit{fold}:\forall\,X.\,(R\to X)\to D_{\textit{param}}\to X$

###### Proof.

Let $\Gamma$ be the context $a:R\to X,x:D_{\textit{param}}$. It suffices to
prove $\Gamma\vdash x\ a:X$. Instantiating the type variable in
$D_{\textit{param}}$ with $X$, we obtain

$\Gamma\vdash x:(R\to X)\to X$

So applying $x$ to $a$ indeed has type $X$ in context $\Gamma$. ∎

######  Definition 54.

$\textit{in}_{X,R}\ :=\ \lambda\,x.\,\lambda\,a.\,a\ (\textit{fmap}_{X,R}\
(\textit{fold}\ a)\ x)$

######  Lemma 55 (In For $D_{\textit{param}}$ (System F)).

If $X\in^{+}R$ , then in System F we have

$\cdot\vdash\textit{in}_{X,R}:[D_{\textit{param}}/X]R\to D_{\textit{param}}$

###### Proof.

Let $\Gamma$ be the context $x:[D_{\textit{param}}/X]R,a:R\to X$. Applying
typing rules of System F, it suffices to show

$\Gamma\vdash a\ (\textit{fmap}_{X,R}\ (\textit{fold}\ a)\ x):X$

This holds if $\Gamma\vdash\textit{fmap}_{X,R}\ (\textit{fold}\ a)\ x:R$.
Using the assumption that $X\in^{+}R$, instantiate Fmap (System F) {51} with
$D_{\textit{param}}$ for $X_{+}$ and $X$ for $X_{-}$ to obtain:

$\cdot\vdash\textit{fmap}_{X,R}:(D_{\textit{param}}\to
X)\to[D_{\textit{param}}/X]R\to R$

The desired typing follows using $\Gamma\vdash\textit{fold}\
a:D_{\textit{param}}\to X$, which holds by Fold {53}. ∎

######  Lemma 56 (In For $D_{\textit{param}}$ (RelTT)).

If $X\in^{+}R$ , then

$\textit{in}_{X,R}::\llbracket[D_{\textit{param}}/X]R\to
D_{\textit{param}}\rrbracket_{\gamma}$

###### Proof.

Apply Soundness Of System F For Closed Terms {44} to In For
$D_{\textit{param}}$ (System F) {55}. ∎

We can prove a similar lemma about $\textit{in}_{X,R}$ and $D_{\textit{ind}}$,
but since $D_{\textit{ind}}$ is not a System F type we cannot use Soundness Of
System F {43}. We first need:

######  Lemma 57 ($D_{\textit{ind}}$ Containment).

If $\textit{in}_{X,R}::\llbracket R\to X\rrbracket_{\gamma[X\mapsto r]}$, then
$\llbracket D_{\textit{ind}}\rrbracket_{\gamma}\subseteq r$.

###### Proof.

Call the hypothesis of the lemma (1), and suppose also (2) $t\ \llbracket
D_{\textit{ind}}\rrbracket_{\gamma}\ t^{\prime}$. We must show $t\ [r]\
t^{\prime}$. Instantiating $X$ in $D_{\textit{ind}}$ with $r$, by Implicit
Product {17} (1) indeed implies $t\ [r]\ t^{\prime}$. ∎

######  Lemma 58 (In for $D_{\textit{ind}}$ (RelTT)).

If $X\in^{+}R$ , then

$\textit{in}_{X,R}::\llbracket[D_{\textit{ind}}/X]R\to
D_{\textit{ind}}\rrbracket_{\gamma}$

###### Proof.

Assume (1) $t\ \llbracket[D_{\textit{ind}}/X]R\rrbracket_{\gamma}\ t^{\prime}$
and show

$\textit{in}_{X,R}\ t\ \llbracket D_{\textit{ind}}\rrbracket_{\gamma}\
\textit{in}_{X,R}\ t^{\prime}$

Unfolding the definition of $D_{\textit{ind}}$ and applying Internalized
Typing {10} and Implicit Product {17}, it suffices to assume $r\in\mathcal{R}$
with

$\textit{in}_{X,R}\,\llbracket R\to X\rrbracket_{\gamma[X\mapsto
r]}\,\textit{in}_{X,R}$ (2)

and show

$\textit{in}_{X,R}\ t\ [r]\ \textit{in}_{X,R}\ t^{\prime}$

This will follow from (2) if we can show (A) $t\ \llbracket
R\rrbracket_{\gamma[X\mapsto r]}\ t^{\prime}$. To derive this, first
instantiate Monotonicity {48} with $D_{\textit{ind}}$ for $X_{+}$ and $r$ for
$X_{-}$. That tells us that if (B) $\llbracket
D_{\textit{ind}}\rrbracket_{\gamma}\subseteq r$, then also (applying
Interpretation Over Substitution {6})

$\llbracket[D_{\textit{ind}}/X]R\rrbracket_{\gamma}\subseteq\llbracket
R\rrbracket_{\gamma[X\mapsto r]}$

This together with (1) proves (A). And (B) follows from (2) by
$D_{\textit{ind}}$ Containment {57}. ∎

###  X-C Reflection

Next, we prove a property known as _reflection_ (cf. [14]). For the specific
case of natural numbers, a similar result is Proposition 14 of [10]. Recall
the definitions of fold and in from Section X-B.

######  Definition 59.

$\textit{rebuild}_{X,R}:=\textit{fold}\ \textit{in}_{X,R}$

######  Lemma 60 (Reflection).

If $X\in^{+}R$ , then

$\textit{rebuild}_{X,R}\ \llbracket D_{\textit{param}}\to
D_{\textit{param}}\rrbracket_{\gamma}\ I$

Before we can prove this, we need:

######  Lemma 61 (Fmap Fold).

Suppose $Y\not\in\textit{FV}(R)$. Let $r_{+}=\llbracket f\cdot
X\rrbracket_{\gamma}$ and $r_{-}=\gamma(X)$. If $X\in^{p}R$ , then, letting
$\gamma^{\prime}=\gamma[Y\mapsto r_{p},X\mapsto r_{\bar{p}}]$, we have

$\textit{fmap}_{X,R}\ f\ \llbracket[Y/X]R\to R\rrbracket_{\gamma^{\prime}}\ I$

###### Proof.

The proof is by induction on the derivation of $X\in^{p}R$. We simplify
implicitly using $\beta\eta$-Closure {2}.

Case $X\in^{+}X$: since $\textit{fmap}_{X,X}=I$, the goal becomes

$I\ f\ [r_{+}\to r_{-}]\ I$

So assume $t_{1}\ [r_{+}]\ t_{2}$, which is equivalent (by Deapplication {4})
to (1) $f\ t_{1}\ [\gamma(X)]\ t_{2}$; and show

$I\ f\ t_{1}\ [\gamma(X)]\ t_{2}$

but this simplifies to (1).

Case $X\in^{p}Z$: since $\textit{fmap}_{X,Z}=K\ I$, the goal becomes

$K\ I\ f\ \llbracket Z\to Z\rrbracket_{\gamma^{\prime}}\ I$

Further simplifying, it becomes

$I\ \llbracket Z\to Z\rrbracket_{\gamma^{\prime}}\ I$

which holds obviously (Identity {8}). Since $Y\not\in\textit{FV}(R)$ by
assumption, this concludes the variable cases.

Case $X\in^{p}(R_{1}\to R_{2})$: the goal becomes

$\lambda\,a.\,(\textit{fmap}_{X,R_{2}}\ f)\circ
a\circ(\textit{fmap}_{X,R_{1}}\ f)\ \llbracket[Y/X]R\to
R\rrbracket_{\gamma^{\prime}}\ I$

So assume (1) $a\,\llbracket[Y/X](R_{1}\to R_{2})\rrbracket_{\gamma^{\prime}}\
a^{\prime}$, and show

$(\textit{fmap}_{X,R_{2}}\ f)\circ a\circ(\textit{fmap}_{X,R_{1}}\ f)\
\llbracket R\rrbracket_{\gamma^{\prime}}\ a^{\prime}$

Next, assume (2) $b\,\llbracket
R_{1}\rrbracket_{\gamma^{\prime}}\,b^{\prime}$, and show

$\textit{fmap}_{X,R_{2}}\ f\ (a\ (\textit{fmap}_{X,R_{1}}\ f\ b)\ \llbracket
R_{2}\rrbracket_{\gamma^{\prime}}\ a^{\prime}\ b^{\prime}$

Since $X\in^{p}R_{2}$, this follows by the IH from

$a\ (\textit{fmap}_{X,R_{1}}\ f\ b)\
\llbracket[Y/X]R_{2}\rrbracket_{\gamma^{\prime}}\ a^{\prime}\ b^{\prime}$

In turn, this follows by (1) from

$\textit{fmap}_{X,R_{1}}\ f\
b\llbracket[Y/X]R_{1}\rrbracket_{\gamma^{\prime}}\ b^{\prime}$

Since $X\in^{\bar{p}}R_{1}$, this follows by the IH from (2).

Case $X\in^{+}\forall\,Z.\,R^{\prime}$: the goal becomes

$\textit{fmap}_{X,R^{\prime}}\ f\ \llbracket[Y/X]R\to
R\rrbracket_{\gamma^{\prime}}\ I$

So assume (1)
$a\,\llbracket\forall\,Z.\,[Y/X]R^{\prime}\rrbracket_{\gamma^{\prime}}\,a^{\prime}$,
and show

$\textit{fmap}_{X,R^{\prime}}\ f\ a\
\llbracket\forall\,Z.\,R^{\prime}\rrbracket_{\gamma^{\prime}}\ a^{\prime}$

For this, assume $r^{\prime}\in\mathcal{R}$, and show

$\textit{fmap}_{X,R^{\prime}}\ f\ a\ \llbracket
R^{\prime}\rrbracket_{\gamma^{\prime}[Z\mapsto r^{\prime}]}\ a^{\prime}$

Since $X\in^{p}R^{\prime}$, this follows by the IH from

$a\,\llbracket[Y/X]R^{\prime}\rrbracket_{\gamma^{\prime}[Z\mapsto
r^{\prime}]}\,a^{\prime}$

But this follows by instantiating (1) with $r^{\prime}$.

∎

We may now return to:

###### Proof of Reflection {60}.

Assuming (1) $t\ \llbracket D_{\textit{param}}\rrbracket_{\gamma}\
t^{\prime}$, it suffices (applying $\beta\eta$-Closure {2}) to show

$t\ \textit{in}_{X,R}\ \llbracket D_{\textit{param}}\rrbracket_{\gamma}\
t^{\prime}$

For this, assume $r\in\mathcal{R}$ and (2) $a\ \llbracket R\to
X\rrbracket_{\gamma[X\mapsto r]}\ a^{\prime}$, and show

$t\ \textit{in}_{X,R}\ a\ [r]\ t^{\prime}\ a^{\prime}$ (A)

The key idea (generalizing Wadler’s Proposition 14 already mentioned) is to
instantiate (1) with the asymmetric relation

$\llbracket\textit{fold}\ a\cdot X\rrbracket_{[X\mapsto r]}$

Let us call this $r_{a}$. (A) will follow from that instantiation if we can
prove

$\textit{in}_{X,R}\ \llbracket R\to X\rrbracket_{\gamma[X\mapsto r_{a}]}\
a^{\prime}$

So assume (3) $t_{1}\ \llbracket R\rrbracket_{\gamma[X\mapsto r_{a}]}\ t_{2}$,
and show

$\textit{in}_{X,R}\ t_{1}\ [r_{a}]\ a^{\prime}\ t_{2}$

This follows, by Deapplication {4} and $\beta\eta$-Closure {2}, from

$\textit{in}_{X,R}\ t_{1}\ a\ [r]\ a^{\prime}\ t_{2}$

Further applying $\beta\eta$-Closure {2}, this follows from

$a\ (\textit{fmap}_{X,R}\ (\textit{fold}\ a)\ t_{1})\ [r]\ a^{\prime}\ t_{2}$

By (2), this follows from

$(\textit{fmap}_{X,R}\ (\textit{fold}\ a)\ t_{1})\ \llbracket
R\rrbracket_{\gamma[X\mapsto r]}\ t_{2}$

which follows from (3) by Fmap Fold {61}, applying also Environment Extension
{7} to get the contexts and types in the required form; and using $X\in^{+}R$.

∎

###  X-D Equating $D_{\textit{param}}$ and $D_{\textit{ind}}$

######  Theorem 62 (Inductive Types).

Suppose $\textit{FV}(R)=\\{X\\}$ and $X\in^{+}R$ .

  1. i.

$t\,\llbracket D_{\textit{ind}}\subseteq
D_{\textit{param}}\rrbracket_{\gamma}\,t^{\prime}$

  2. ii.

If $R$ is $\forall^{+}$, then $t\,\llbracket D_{\textit{param}}\subseteq
D_{\textit{ind}}\rrbracket_{\gamma}\,t^{\prime}$

  3. iii.

If $R$ is $\forall^{+}$, then $t\,\llbracket D_{\textit{ind}}\topdoteq
D_{\textit{param}}\rrbracket_{\gamma}\ t^{\prime}$

###### Proof.

Recall the definitions:

$\begin{array}[]{lll}D_{\textit{param}}&:=&\forall\,X.\,(R\to X)\to X\\\
D_{\textit{ind}}&:=&\forall\,X.\,([\textit{in}_{X,R}]\,(R\to
X)\,[\textit{in}_{X,R}])\Rightarrow X\end{array}$

For this proof, let us apply Subset {15} implicitly. (iii) follows from (i)
and (ii). To show (i), assume $t\,\llbracket
D_{\textit{ind}}\rrbracket_{\gamma}\,t^{\prime}$, and instantiate $X$ in this
assumption with $D_{\textit{param}}$. This implies the required $t\,\llbracket
D_{\textit{param}}\rrbracket_{\gamma}\,t^{\prime}$, as long as (applying
Interpretation Over Substitution {6})

$\textit{in}_{X,R}\,\llbracket[D_{\textit{param}}/X]R\to
D_{\textit{param}}\rrbracket_{\gamma}\ \textit{in}_{X,R}$

But this is exactly In For $D_{\textit{param}}$ {56}.

To show (ii), assume (1) $t\,\llbracket
D_{\textit{param}}\rrbracket_{\gamma}\,t^{\prime}$, and instantiate $X$ in
this assumption with $D_{\textit{ind}}$ to get

$t\,\llbracket([D_{\textit{ind}}/X]R\to D_{\textit{ind}})\to
D_{\textit{ind}}\rrbracket_{\gamma}\ t^{\prime}$

(Here we again applied Interpretation Over Substitution {6}.) From this and In
For $D_{\textit{ind}}$ {58}, we obtain (2)

$t\,\textit{in}_{X,R}\ \llbracket D_{\textit{ind}}\rrbracket_{\gamma}\
t^{\prime}\ \textit{in}_{X,R}$

This is close to what we want. Applying Reflection {60} to (1), we obtain

$t\,\textit{in}_{X,R}\ \llbracket D_{\textit{param}}\rrbracket_{\gamma}\
t^{\prime}$

Since $\textit{FV}(R)=X$, $D_{\textit{param}}$ is closed, so we may change
$\gamma$ to $e$ here and in (1), by Environment Extension {7}. Then since $R$
is $\forall^{+}$, $D_{\textit{param}}$ is also, and we can apply Identity
Inclusion {32} to get:

$\begin{array}[]{l}t\,\textit{in}_{X,R}=_{\beta\eta}t^{\prime}\\\
t=_{\beta\eta}t^{\prime}\end{array}$

Using these facts with $\beta\eta$-Closure {2}, we may simplify (2) to the
desired $t\ \llbracket D_{\textit{ind}}\rrbracket_{\gamma}\ t^{\prime}$.

∎

In light of this result, we denote $D_{\textit{param}}$ for particular $X$ and
$R$ as $D_{X,R}$, and freely change between it and $D_{\textit{ind}}$ as long
as $R$ is $\forall^{+}$.

###  X-E Example: Nat

In this section, we consider the basic example of natural numbers. To express
this type using the parameter $R$ of $D_{X,R}$, we first need some standard
types (namely $A+B$ and $1$) and associated term definitions: for $A+B$,
constructors inl and inr, and eliminator $\langle n,m\rangle$; and for $1$,
constructor unit.

######  Definition 63.

$\begin{array}[]{lll}A+B&:=&\forall\,X.\,(A\to X)\to(B\to X)\to X\\\
1&:=&\forall\,X.\,X\to X\\\
\textit{inl}&:=&\lambda\,a.\,\lambda\,x.\,\lambda\,y.\,x\ a\\\
\textit{inr}&:=&\lambda\,b.\,\lambda\,x.\,\lambda\,y.\,y\ b\\\ \langle
n,m\rangle&:=&\lambda\,c.\,c\ n\ m\\\ \textit{unit}&:=&I\end{array}$

Now we define Nat and its constructors as expected, with addition as an
example operation:

######  Definition 64.

$\begin{array}[]{lll}\textit{Nat}&:=&D_{X,1+X}\\\
\textit{zero}&:=&\textit{in}_{X,1+X}\ (\textit{inl}\ \textit{unit})\\\
\textit{succ}&:=&\textit{in}_{X,1+X}\circ\textit{inr}\\\
\textit{add}&:=&\lambda\,n.\,\lambda\,m.\,n\ \langle
m,\textit{succ}\rangle\end{array}$

Thanks to Soundness of System F For Closed Terms {44} and the usual System F
typings of the above term definitions (including In For $D_{\textit{param}}$
(System F) {55}), we have the following relational typings:

######  Lemma 65 (Nat Operations).

$\begin{array}[]{lll}\textit{zero}&::&\llbracket\textit{Nat}\rrbracket_{\gamma}\\\
\textit{succ}&::&\llbracket\textit{Nat}\to\textit{Nat}\rrbracket_{\gamma}\\\
\textit{add}&::&\llbracket\textit{Nat}\to\textit{Nat}\to\textit{Nat}\rrbracket_{\gamma}\end{array}$

Following a very similar development as for Inductive Types {62}, we may also
equate $A+B$ and $1$ with inductive variants:

######  Definition 66.

$\begin{array}[]{lll}A+_{i}B&:=&\forall\,X.\,[\textit{inl}]\,(A\to
X)\,[\textit{inl}]\Rightarrow\\\ &&\ \ \ \ \ \ [\textit{inr}]\,(B\to
X)\,[\textit{inr}]\Rightarrow X\\\
1_{i}&:=&\forall\,X.\,[\textit{unit}]X[\textit{unit}]\Rightarrow X\end{array}$

Recall the notation $R\topdoteq R^{\prime}$ (Definition 18).

######  Proposition 67.

$\begin{array}[]{l}t_{1}\ \llbracket A+B\topdoteq A+_{i}B\rrbracket_{\gamma}\
t_{2}\\\ t_{1}\ \llbracket 1\topdoteq 1_{i}\rrbracket_{\gamma}\
t_{2}\end{array}$

Finally, let us prove a basic inductive property of add, as an example.

######  Lemma 68.

$\lambda\,n.\,\textit{add}\ n\ \textit{zero}\
\llbracket\textit{Nat}\to\textit{Nat}\rrbracket_{\gamma}\ I$

###### Proof.

For (i): Assume (1) $n\ \llbracket\textit{Nat}\rrbracket_{\gamma}\
n^{\prime}$, and show

$\textit{add}\ n\ \textit{zero}\ \llbracket\textit{Nat}\rrbracket_{\gamma}\
n^{\prime}$ (A)

Applying Inductive Types {62} to (1) allows us to reason inductively; we
instantiate the type variable $X$ in $D_{\textit{ind}}$ with the
interpretation of

$r:=\lambda\,n.\,\textit{add}\ n\ \textit{zero}\cdot\textit{Nat}$

We must show this is preserved by $\textit{in}_{X,1+X}$; that is

$\textit{in}_{X,1+X}::\llbracket(1+r)\to r\rrbracket_{\gamma}$ (B)

By Deapplication {4} this suffices for (A). For (B), assume (2) $v\ \llbracket
1+r\rrbracket_{\gamma}\ v^{\prime}$, and show

$\textit{in}_{X,1+X}v\ \llbracket r\rrbracket_{\gamma}\
\textit{in}_{X,1+X}v^{\prime}$

Switch to the inductive view of $1+r$ in (2), and induct using the
interpretation of

$r^{\prime}:=\textit{in}_{X,1+X}\mathbin{\ast}r$

By Deapplication {4}, this is sufficient for (B). We must prove

  * •

$\textit{inl}\ \textit{unit}::\llbracket r^{\prime}\rrbracket_{\gamma}$

  * •

$\textit{inr}::\llbracket r^{\prime}\to r^{\prime}\rrbracket_{\gamma}$

Unfolding definitions of $r^{\prime}$ and $r$ using Deapplication {4}, we
confirm the following using $\beta\eta$-Closure {2} and Nat Operations {65}

  * •

$\textit{add}\ (\textit{in}_{X,1+X}\ (\textit{inl}\ \textit{unit}))\
\textit{zero}\ \llbracket\textit{Nat}\rrbracket_{\gamma}\
(\textit{in}_{X,1+X}\ (\textit{inl}\ \textit{unit}))$

  * •

$\textit{add}\ (\textit{in}_{X,1+X}\ (\textit{inr}\ x))\ \textit{zero}\
\llbracket\textit{Nat}\rrbracket_{\gamma}\ (\textit{in}_{X,1+X}\
(\textit{inr}\ x^{\prime}))$ from $\textit{add}\ x\
\textit{zero}\llbracket\textit{Nat}\rrbracket_{\gamma}\ x^{\prime}$

∎

###  X-F Discussion

Wadler proves a result similar to Inductive Types {62} for the special case of
the natural numbers, in Section 5 of [10]. He shows, as a theorem of a second-
order logic, that being related by the relational interpretation of
$\textit{Nat}_{\textit{param}}$ is the same as being equal natural numbers
that satisfy a predicate of unary induction. The result here is more general,
covering any inductive datatype defined by a positive type scheme $R$. The
equivalence is expressed not in a second-order logic, but in RelTT. So the
proof is in terms only of binary relations, including a binary-relational form
of induction (instead of using unary induction). Another technical difference
is that the proof here relies on Identity Inclusion {32}. This does not show
up in Wadler’s proof, but only because he considers just the simple example of
natural numbers, with the type $\forall\,X.\,(X\to X)\to X\to X$. One may
confirm that a categorical version, as we consider here, would require an
analogous property for the proof of his Proposition 14 [10].

Thanks to Inductive Types {62}, we can transport properties between the
denotations of $D_{\textit{ind}}$ and $D_{\textit{param}}$. For a simple
example:

######  Lemma 69.

Suppose $R$ is $\forall^{+}$. Then $\llbracket D_{\textit{ind}}\rrbracket$ is
a per.

###### Proof.

If $R$ is $\forall^{+}$, then so is $D_{\textit{param}}$, and hence
$\llbracket D_{\textit{param}}\rrbracket_{\gamma}$ is a per by $\forall^{+}$
Per {34}. This implies $D_{\textit{ind}}$ is also a per, by Inductive Types
{62}. ∎

Proving this lemma directly is not hard, but using Inductive Types {62},
unnecessary. Richer examples are enabled thanks to Substitutivity Of
Relational Equality {20}.

##  XI Positive-recursive types

A very useful type form from standard type theory is the recursive type
$\textit{rec}\,X.\,R$, where $X$ is bound in $R$, and $X$ occurs only
positively in $R$. The type should be isomorphic to its unfolding
$[\textit{rec}\,X.\,R/X]R$, where we desire that the functions witnessing the
isomorphism are identity functions. (This form of recursive type can be seen
as unifying the standardly distinguished _isorecursive_ and _equirecursive_.)
This section shows how a relational version of this type can be derived in
RelTT. The development is a (nontrivial) adaptation of ideas from [15], to our
relational setting. It is built on the derivations of subset type and implicit
product from Section III, and makes crucial use of Montonicity {48}. Let us
assume that type $R$ may contain type variable $X$ free.

######  Definition 70.

$\textit{rec}\,X.\,R:=\forall\,X.\,(R\subseteq X)\Rightarrow X$

######  Lemma 71 (Rec Body).

If $\llbracket R\rrbracket_{\gamma[X\mapsto r]}\subseteq r$, then
$\llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}\subseteq r$.

###### Proof.

Assume (1) $t_{1}\ \llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}\ t_{2}$,
and instantiate this with $r$, to obtain

$t_{1}\ \llbracket(R\subseteq X)\Rightarrow X\rrbracket_{\gamma[X\mapsto r]}\
t_{2}$

From this, applying Subset {15} and Implicit Product {17}, we have the desired
$t_{1}\ r\ t_{2}$, as long as $\llbracket R\rrbracket_{\gamma[X\mapsto
r]}\subseteq r$. But the latter is a condition of the lemma. ∎

######  Lemma 72 (Rec Fold).

If $X\in^{+}R$, then $t_{1}\
\llbracket[\textit{rec}\,X.\,R/X]R\subseteq\textit{rec}\,X.\,R\rrbracket_{\gamma}\
t_{2}$.

###### Proof.

By Subset {15}, it suffices to show
$\llbracket\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}\subseteq\llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}$.
So assume (1) $t\ \llbracket[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}\
t^{\prime}$, and show $t\ \llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}\
t^{\prime}$. Applying the semantics, Implicit Product {17}, and Subset {15},
it suffices to assume $r\in\mathcal{R}$ and (2) $\llbracket
R\rrbracket_{\gamma[X\mapsto r]}\subseteq r$, and show $t_{1}\ [r]\ t_{2}$.
Applying Interpretation Over Substitution {6} to (1), we have (3) $t\
\llbracket
R\rrbracket_{\gamma[X\mapsto\llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}]}\
t^{\prime}$. By Rec Body {71} with (2),
$\llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}\subseteq r$. By Monotonicity
{48}, (3) implies $t\llbracket R\rrbracket_{\gamma[X\mapsto r_{\gamma}]}\
t^{\prime}$. Combining this with (2), we obtain the desired $t\ [r]\
t^{\prime}$.

∎

######  Lemma 73 (Rec Unfold).

If $X\in^{+}R$, then $t_{1}\
\llbracket\textit{rec}\,X.\,R\subseteq[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}\
t_{2}$.

###### Proof.

By Subset {15}, it suffices to show
$\llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}\subseteq\llbracket\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}$.
So assume (1) $t\ \llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}\
t^{\prime}$ and show $t\
\llbracket[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}\ t^{\prime}$.
Instantiate (1) with $\llbracket[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}$
to obtain

$t\ \llbracket(R\subseteq X)\Rightarrow
X\rrbracket_{\gamma[X\mapsto\llbracket[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}]}\
t^{\prime}$

Applying Interpretation Over Substitution {6}, this is equivalent to

$\begin{array}[]{l}t\
\llbracket([[\textit{rec}\,X.\,R/X]R/X]R\subseteq[\textit{rec}\,X.\,R/X]R)\Rightarrow\\\
\hskip 156.49014pt[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}\
t^{\prime}\end{array}$

By Implicit Product {17} and Subset {15}, this implies the desired typing as
long as

$\llbracket[[\textit{rec}\,X.\,R/X]R/X]R\rrbracket_{\gamma}\subseteq\llbracket[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}$

But this follows by Monotonicity {48} (since $X\in^{+}R$) from

$\llbracket[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}\subseteq\llbracket\textit{rec}\,X.\,R\rrbracket_{\gamma}$

And this follows (by Subset {15}) directly from Rec Fold {72}. ∎

######  Theorem 74 (Recursive Types).

If $X\in^{+}R$, then $t_{1}\
\llbracket\textit{rec}\,X.\,R\topdoteq[\textit{rec}\,X.\,R/X]R\rrbracket_{\gamma}\
t_{2}$

###### Proof.

Using Relational Equality {19}, this follows from Rec Fold {72} and Rec Unfold
{73} ∎

##  XII A relational type system

Having considered now some of the expressive power of RelTT, in its ability to
derive types which are often taken as primitive – for example, inductive types
are derived here, but primitive for the Calculus of Inductive Constructions
[16] – let us turn to the question of an implementable type system for RelTT.
We follow the approach suggested by the Curry-Howard correspondence, to to
devise a system of proof terms for derivations in RelPf.

Figure 7 gives the syntax for contexts $\Gamma$ and proof terms $p$ of RelTy,
together with an erasure function mapping these back to pure
$\lambda$-calculus. Proof terms $(p,p^{\prime})$ and $\pi\,p-x.u.v.p^{\prime}$
are used for composition; the $\pi$-term is like an existential elimination.
Erasure will indeed treat proofs of relational typings by compositions as
pairs (Definition 22). The typing rules for RelTy are given in Figure 8.

Given a context $\Gamma$ and a proof term $p$, the rules may be read bottom-up
as an algorithm to compute the relational typing $t\,[T]\,t^{\prime}$ (if any)
proved by the proof term. Proofs are organized in natural-deduction style:
each type construct has introduction and elimination forms. For example, the
introduction form for an identity $t\,[t^{\prime}]\,t^{\prime}\,t$ is
$\iota\\{t,t^{\prime}\\}$. The elimination is more complicated, unfortunately,
as we must describe substitution, using a proven identity
$t\,[t^{\prime\prime}]\,t^{\prime}$, into the terms in some other relational
typing. The syntax for the elimination form uses a “guide”
$\\{x.t_{1},t_{2}\\}$ to give a mechanism for locating instances of $t$ in the
left and right terms of the relational typing, to be rewritten to
$t^{\prime}$. The variable $x$ in terms $t_{1}$ and $t_{2}$ marks these
locations.

By design, RelTy exactly follows the structure of RelPf. Define
$\llcorner\Gamma\lrcorner$ by

$\begin{array}[]{lll}\llcorner\cdot\lrcorner&=&\cdot\\\
\llcorner\Gamma,x:t\,[R]\,t^{\prime}\lrcorner&=&\llcorner\Gamma\lrcorner,t\,[R]\,t^{\prime}\end{array}$

This maps RelTy contexts to RelPf contexts. A reverse mapping
$\langle\Gamma\rangle$ can be defined as $\langle\Gamma\rangle_{k}$ where $k$
is the length of $\Gamma$, and the helper function is defined as follows,
using a canonical ordering $x_{1},x_{2},\ldots$ for assumption variables:

$\begin{array}[]{lll}\langle\cdot\rangle_{k}&=&\cdot\\\
\langle\Gamma,t\,[R]\,t^{\prime}\rangle_{k}&=&\langle\Gamma\rangle_{k-1},x_{k}:t\,[R]\,t^{\prime}\end{array}$

######  Theorem 75 (RelTy-RelPf Isomorphism).

  1. i.

If $\Gamma\vdash p:t\,[R]\,t^{\prime}$ in RelTy, then
$\llcorner\Gamma\lrcorner\vdash t\,[R]\,t^{\prime}$ in RelPf.

  2. ii.

If $\Gamma\vdash t\,[R]\,t^{\prime}$ in RelPf, then there exists $p$ such that
$\langle\Gamma\rangle\vdash p:t\,[R]\,t^{\prime}$ in RelTy.

###### Proof.

For (i): because RelTy just expands RelPf with proof terms, the proof amounts
to erasing all proof terms (including assumptions $u$ in contexts) from RelTy
derivations. For (ii): by design, RelTy has proof-term constructs
corresponding to all proof rules of RelPf, so the proof amounts to recursively
adding in those terms. ∎

If we project even further, we can map from RelTy to System F. Recall the
definition of pairs (Definition 22), which are used in projecting composition.

######  Definition 76.

Define $|R|$ recursively by:

$\begin{array}[]{lll}|X|&=&X\\\ |R\to R^{\prime}|&=&|R|\to|R^{\prime}|\\\
|\forall\,X.\,R|&=&\forall\,X.\,|R|\\\ |R^{\cup}|&=&|R|\\\ |R\cdot
R^{\prime}|&=&|R|\times|R^{\prime}|\\\ |t|&=&\forall\,X.\,X\to X\end{array}$

Extend this to contexts by recursively defining $|\Gamma|$:

$\begin{array}[]{lll}|\cdot|&=&\cdot\\\
|\Gamma,u:t\,[R]\,t^{\prime}|&=&|\Gamma|,u:|R|\end{array}$

######  Theorem 77 (RelTy Projection).

If $\Gamma\vdash p:t\,[R]\,t^{\prime}$ then $|\Gamma|\vdash|p|:|R|$ in System
F.

###### Proof.

The proof is by induction on the assumed RelTy derivation.

Case:

$\Gamma\vdash x:t\,[R]\,t^{\prime}x:t\,[R]\,t^{\prime}\in\Gamma$

From $x:t\,[R]\,t^{\prime}\in\Gamma$ we get $x:|R|\in\Gamma$ and hence the
desired conclusion.

Case:

$\Gamma\vdash\lambda\,u:R.\,p:\lambda\,x.\,t\,[R\to
R^{\prime}]\,\lambda\,x^{\prime}.\,t^{\prime}\lx@proof@logical@and\Gamma,u:x\,[R]\,x^{\prime}\vdash
p:t\,[R^{\prime}]\,t^{\prime}(*)$

By the IH we have $|\Gamma|,u:|R|\vdash p:|R^{\prime}|$, from which we deduce
the desired $|\Gamma|\vdash\lambda\,u.\,|p|:|R\to R^{\prime}|$.

Case:

$\Gamma\vdash
p_{1}\,p_{2}:t_{1}\,t_{2}\,[R^{\prime}]\,t_{1}^{\prime}\,t_{2}^{\prime}\lx@proof@logical@and\Gamma\vdash
p_{1}:t_{1}\,[R\to R^{\prime}]\,t_{1}^{\prime}\Gamma\vdash
p_{2}:t_{2}\,[R]\,t_{2}^{\prime}$

By the IH we have $|\Gamma|\vdash|p_{1}|:|R\to R^{\prime}|$ and
$|\Gamma|\vdash|p_{2}|:|R|$, from which we deduce the desired
$|\Gamma|\vdash|p_{1}\,p_{2}|:|R^{\prime}|$.

Case:

$\Gamma\vdash p\\{R\\}:t\,[[R/X]R^{\prime}]\,t^{\prime}\Gamma\vdash
p:t\,[\forall\,X.\,R^{\prime}]\,t^{\prime}$

By the IH we have $|\Gamma|\vdash|p|:\forall\,X.\,|R^{\prime}|$, from which
the desired $|\Gamma|\vdash|p|:|[R/X]R^{\prime}|$ follows.

Case:

$\Gamma\vdash\Lambda\,X.\,p:t\,[\forall\,X.\,R]\,t^{\prime}\lx@proof@logical@and\Gamma\vdash
p:t\,[R]\,t^{\prime}X\not\in\textit{FV}(\Gamma)$

By the IH we have $|\Gamma|\vdash|p|:|R|$, from which the desired
$|\Gamma|\vdash|p|:\forall\,X.\,|R|$ follows.

Case:

$\Gamma\vdash t_{1}^{\prime}\blacktriangleleft p\blacktriangleright
t_{2}^{\prime}:t_{1}^{\prime}\,[R]\,t_{2}^{\prime}\lx@proof@logical@and\Gamma\vdash
p:t_{1}\,[R]\,t_{2}t_{1}=_{\beta\eta}t_{1}^{\prime}t_{2}=_{\beta\eta}t_{2}^{\prime}$

The erasure of $t_{1}^{\prime}\blacktriangleleft p\blacktriangleright
t_{2}^{\prime}$ is $|p|$, so the desired conclusion is just
$|\Gamma|\vdash|p|:|R|$, which we have by the IH.

Case:

$\Gamma\vdash\cup_{e}\,p:t^{\prime}\,[R]\,t\Gamma\vdash
p:t\,[R^{\cup}]\,t^{\prime}$

Similar to the previous case.

Case:

$\Gamma\vdash\cup_{i}\,p:t^{\prime}\,[R^{\cup}]\,t\Gamma\vdash
p:t\,[R]\,t^{\prime}$

Similar to the previous case.

Case:

$\Gamma\vdash\iota\\{t,t^{\prime}\\}:t\,[t^{\prime}]\,t^{\prime}\,t\ $

$|\iota\\{t,t^{\prime}\\}|$ is $I$ and erasure of the term promotion
$t^{\prime}$ is $\forall\,X.\,X\to X$. So this inference translates to the
familiar typing of the identity function in System F.

Case:

$\Gamma\vdash\rho\\{x.t_{1},t_{2}\\}\ p-\
p^{\prime}:[t^{\prime}/x]t_{1}\,[R]\,[t^{\prime}/x]t_{2}\lx@proof@logical@and\Gamma\vdash
p:t\,[t^{\prime\prime}]\,t^{\prime}\Gamma\vdash
p^{\prime}:[t^{\prime\prime}\,t/x]t_{1}\,[R]\,[t^{\prime\prime}\,t/x]t_{2}$

By the IH we have $|\Gamma|\vdash|p^{\prime}|:|R|$. Since the $\rho$-proof
erases to just the erasure of its leftmost subproof, this suffices for the
desired conclusion.

Case:

$\Gamma\vdash\pi\,p-x.u.v.p^{\prime}:t_{1}\,[R^{\prime\prime}]\,t_{2}\begin{array}[]{c}\Gamma\vdash
p:t\,[R\cdot R^{\prime}]\,t^{\prime}\quad(**)\\\
\Gamma,u:t\,[R]\,x,v:x\,[R^{\prime}]\,t^{\prime}\vdash
p^{\prime}:t_{1}\,[R^{\prime\prime}]\,t_{2}\end{array}$

By the IH we have $|\Gamma|\vdash|p|:|R|\times|R^{\prime}|$ and
$|\Gamma|,u:|R|,v:|R^{\prime}|\vdash|p^{\prime}|:|R^{\prime\prime}|$. By the
definition of product types in System F, from these derivations we may easily
establish
$|\Gamma|\vdash|p|\,\lambda\,u.\,\lambda\,v.\,|p^{\prime}|:|R^{\prime\prime}|$,
which suffices since $|\pi\,p-x.u.v.p^{\prime}|=|p|\
\lambda\,u.\,\lambda\,v.\,|p^{\prime}|$.

Case:

$\Gamma\vdash(p,p^{\prime}):t\,[R\cdot
R^{\prime}]\,t^{\prime}\lx@proof@logical@and\Gamma\vdash
p:t\,[R]\,t^{\prime\prime}\Gamma\vdash
p^{\prime}:t^{\prime\prime}\,[R^{\prime}]\,t^{\prime}$

By the IH we have $|\Gamma|\vdash|p|:|R|$ and
$|\Gamma|\vdash|p^{\prime}|:|R^{\prime}|$. With these we may deduce
$|\Gamma|\vdash(|p|,|p^{\prime}|):|R|\times|R^{\prime}|$ by the definition of
product types in System F.

∎

This result is interesting, because it shows that any valid RelTy proof term
proves a property of its own erasure:

######  Proposition 78 (RelTy Self).

If $\Gamma\vdash p:t\,[R]\,t^{\prime}$, then $\Gamma\vdash p:|p|\,[R]\,|p|$.

###### Proof sketch.

From the assumed RelTy derivation we get to $\Gamma\vdash|p|\,[R]\,|p|$ using
RelTy Projection {77} and Soundness of System F {43}. We need then just a
somewhat more informative version of part (ii) of RelTy-RelPf Isomorphism
{75}, which maps RelPf derivations to particular proof terms $p$ (not just
showing that some such $p$ exists) in correspondence with the RelPf
derivations. ∎

$\begin{array}[]{lll}\Gamma&::=&\cdot\ |\ \Gamma,u:t\,[R]\,t^{\prime}\\\ \\\
\textit{proof terms }p&:=&u\ |\ \lambda\,u:T.\,p\ |\ p\ p^{\prime}\ |\\\
&&p\\{T\\}\ |\ \Lambda\,X.\,p\ |\\\ &&t\blacktriangleleft p\blacktriangleright
t^{\prime}\ |\\\ &&\cup_{i}\,p\ |\ \cup_{e}\,p\ |\\\
&&\iota\\{t,t^{\prime}\\}\ |\ \rho\\{x.t_{1},t_{2}\\}\ p-p^{\prime}\ |\\\
&&(p,p^{\prime})\ |\ \pi\,p-x.u.v.p^{\prime}\\\ \\\ |u|&=&u\\\
|\lambda\,u:T.\,p|&=&\lambda\,u.\,p\\\ |p\ p^{\prime}|&=&|p|\ |p^{\prime}|\\\
|p\\{T\\}|&=&|p|\\\ |\Lambda\,X.\,p|&=&|p|\\\ |t\blacktriangleleft
p\blacktriangleright t^{\prime}|&=&|p|\\\ |\cup_{i}\,p|&=&|p|\\\
|\cup_{e}\,p|&=&|p|\\\ |\iota\\{t,t^{\prime}\\}|&=&I\\\
|\rho\\{x.t_{1},t_{2}\\}\ p-p^{\prime}|&=&|p^{\prime}|\\\
|(p,p^{\prime})|&=&(|p|,|p^{\prime}|)\\\
|\pi\,p-x.u.v.p^{\prime}|&=&|p|\,\lambda\,u.\,\lambda\,v.\,|p^{\prime}|\end{array}$
Figure 7: Syntax for proof terms of RelTy, and erasure to pure
$\lambda$-calculus

$\begin{array}[]{lll}\Gamma\vdash
x:t\,[R]\,t^{\prime}x:t\,[R]\,t^{\prime}\in\Gamma&\Gamma\vdash\lambda\,x:R.\,p:\lambda\,x.\,t\,[R\to
R^{\prime}]\,\lambda\,x^{\prime}.\,t^{\prime}\lx@proof@logical@and\Gamma,p:x\,[R]\,x^{\prime}\vdash
p:t\,[R^{\prime}]\,t^{\prime}(*)&\Gamma\vdash
p_{1}\,p_{2}:t_{1}\,t_{2}\,[R^{\prime}]\,t_{1}^{\prime}\,t_{2}^{\prime}\lx@proof@logical@and\Gamma\vdash
p_{1}:t_{1}\,[R\to R^{\prime}]\,t_{1}^{\prime}\Gamma\vdash
p_{2}:t_{2}\,[R]\,t_{2}^{\prime}\par\\\ \\\ \Gamma\vdash
p\\{R\\}:t\,[[R/X]R^{\prime}]\,t^{\prime}\Gamma\vdash
p:t\,[\forall\,X.\,R^{\prime}]\,t^{\prime}&\Gamma\vdash\Lambda\,X.\,p:t\,[\forall\,X.\,R]\,t^{\prime}\lx@proof@logical@and\Gamma\vdash
p:t\,[R]\,t^{\prime}X\not\in\textit{FV}(\Gamma)&\Gamma\vdash
t_{1}^{\prime}\blacktriangleleft p\blacktriangleright
t_{2}^{\prime}:t_{1}^{\prime}\,[R]\,t_{2}^{\prime}\lx@proof@logical@and\Gamma\vdash
p:t_{1}\,[R]\,t_{2}t_{1}=_{\beta\eta}t_{1}^{\prime}t_{2}=_{\beta\eta}t_{2}^{\prime}\\\
\\\ \lx@intercol\Gamma\vdash\cup_{e}\,p:t^{\prime}\,[R]\,t\Gamma\vdash
p:t\,[R^{\cup}]\,t^{\prime}\par\ \ \ \ \
\Gamma\vdash\cup_{i}\,p:t^{\prime}\,[R^{\cup}]\,t\Gamma\vdash
p:t\,[R]\,t^{\prime}\par\ \ \ \ \
\Gamma\vdash\iota\\{t,t^{\prime}\\}:t\,[t^{\prime}]\,t^{\prime}\,t\
\hfil\lx@intercol&\Gamma\vdash\rho\\{x.t_{1},t_{2}\\}\ p-\
p^{\prime}:[t^{\prime}/x]t_{1}\,[R]\,[t^{\prime}/x]t_{2}\lx@proof@logical@and\Gamma\vdash
p:t\,[t^{\prime\prime}]\,t^{\prime}\Gamma\vdash
p^{\prime}:[t^{\prime\prime}\,t/x]t_{1}\,[R]\,[t^{\prime\prime}\,t/x]t_{2}\\\
\\\
\lx@intercol\Gamma\vdash\pi\,p-x.u.v.p^{\prime}:t_{1}\,[R^{\prime\prime}]\,t_{2}\lx@proof@logical@and\Gamma\vdash
p:t\,[R\cdot
R^{\prime}]\,t^{\prime}\Gamma,u:t\,[R]\,x,v:x\,[R^{\prime}]\,t^{\prime}\vdash
p^{\prime}:t_{1}\,[R^{\prime\prime}]\,t_{2}(**)\hfil\lx@intercol&\Gamma\vdash(p,p^{\prime}):t\,[R\cdot
R^{\prime}]\,t^{\prime}\lx@proof@logical@and\Gamma\vdash
p:t\,[R]\,t^{\prime\prime}\Gamma\vdash
p^{\prime}:t^{\prime\prime}\,[R^{\prime}]\,t^{\prime}\par\end{array}$

Side condition (*) is $x\not\in\textit{FV}(\Gamma,R,R^{\prime})$.

Side condition (**) is
$x\not\in\textit{FV}(\Gamma,t_{1},t_{2},t,t^{\prime},R,R^{\prime},R^{\prime\prime})$.

Figure 8: RelTy typing rules

##  XIII Related work

RelTT’s semantics (Figure 2) is a relational realizability semantics, where
realizers are terms of untyped lambda calculus (cf. [17, 18]). Relational
semantics for types has been studied extensively in the context of logical
relations; see Chapter 8 of [19]. An influential branch of this work was
initiated by Reynolds, on what is now called parametricity [9]. [20] frames
some recent results, using categorical semantics.

[21] proposes a similar realizabiliity semantics, for the Calculus of
Constructions plus an extensional equality type. The major difference is that
in RelTT, we propose a notation for asymmetric relations, which is lacking in
[21]. Instead, constructions based on the semantics are done at the meta-level
(where asymmetric relations can be described). Indeed, the denotable relations
of [21] are partial equivalences – albeit of a modified form due to basing the
semantics on “zig-zag complete” relations. In contrast, we have seen above
some families of types whose denotations are partial equivalences (unmodified)
in RelTT. But by design, not all types denote partial equivalences in RelTT,
since reasoning about terms generally involves asymmetric relations; an
important example we saw is Reflection {60}.

Observational Type Theory (OTT) is an approach to type-specific extensionality
principles in an intensional dependent type theory, based on a primitive
heterogeneous equality type and associated operators [22]. RelTT is similar in
deriving extensionality principles, but more radical in design: where OTT
extends a traditional (i.e., unary) type theory including $W$-types with an
extensional form of equality, RelTT takes a binary view of all types, and does
not use dependent types at all. The resulting system is hence formally quite a
bit simpler.

Unlike [9] and subsequent works like [23]), RelTT lacks Identity Extension.
This property states that when free type variables are interpreted by identity
relations, the relational meaning of a type $T$ is the identity relation on
the unary (or “object”) interpretation of $T$. This is a very strong property,
showing that the object interpretation of types gives canonical forms for the
equivalence defined by the relational interpretation of types. But it rules
out expression of asymmetric relations as types. RelTT preserves this
possibility, at the cost of weakening Identity Extension to Identity Inclusion
{32}.

In [24], Plotkin and Abadi introduce a second-order logic for reasoning about
(typable) terms of System F by quantification over relations, and using a
parametricity axiom. In contrast, RelTT uses relational types to express
relations in a more compact way. A parametricity axiom would not make sense
here, for there is no separate notion of unary typing from which relational
typing could be stated to follow. The only typings are relational.

RelTT may be compared with previous work of Stump et al. on Cedille [25, 26,
27]. Both systems aim at a minimalistic extension of a small pure type system
as a foundation for type theory. Cedille extends the Curry-style Calculus of
Constructions with dependent intersections, implicit products, and an equality
type over untyped terms. RelTT extends System F with three relational
operators based on a relational semantics. While the systems are roughly
equivalent in formal complexity – with RelTT having the simplifying advantage
of eschewing dependent types – RelTT delivers type-specific extensionality
principles, which Cedille lacks.

[28] considers how parametricity results can be embedded in constructive type
theory, by elaborating types into corresponding theorems in the logic of so-
called “reflective” pure type systems. Subsequent work built an extended PTS
internalizing these theorems [29]. These papers consider fairly rich Church-
style lambda calculi, in contrast to the more compact Curry-style calculus of
RelTT.

Finally, RelTT may be compared with Homotopy Type Theory (HoTT), a line too
active in recent years to summarize here [30]. Both theories support
functional extensionality. The two approaches have different origins: logical
relations and parametricity for RelTT, homotopy theory and higher category
theory for HoTT. A major point of difference is univalence: while RelTT allows
one to express and derive relational equalities within the theory, these are
based on semantic inclusions, not isomorphisms (as in univalence). Thus,
transporting results between isomorphic types as done in HoTT is not (in an
obvious way) directly possible in RelTT. Another point of comparison is the
compactness of the theory. RelTT is based on a very compact semantics for a
small number of relational type forms. In contrast, systems like, for one
notable example, Cubical Agda, are based on a larger array of primitives [31].
Whereas the free theorems provided by parametricity allows proofs to be
transported to observationally equivalent terms, HOTT uses explicit
equivalences between terms for this purpose. Only very recent work has
considered how to combine these two complementary approaches inside of
univalent type theories [32].

##  XIV Conclusion and future work

Based on a binary relational semantics, RelTT is a new minimalistic
extensional type theory, where inductive and positive-recursive types are
derivable. The theory does not have dependent types, and indeed, an indirect
conclusion of the paper is that type theory does not require dependent types
for reasoning about programs. Just passing from the traditional unary
semantics to a binary-relational one opens the possibility for formal
(extensional) reasoning about programs. Future work includes direct support
for existential types, for deriving coinductive types; the standard double-
negation encoding of existentials is problematic due to the requirement of
forall-positivity for Identity Inclusion {32}.

## Acknowledgments

We gratefully acknowledge NSF support under award 1524519, and DoD support
under award FA9550-16-1-0082 (MURI program). First author: St. Jer., AMDG.

## References

  * [1] L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer, “The Lean Theorem Prover (System Description),” in _Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings_ , ser. Lecture Notes in Computer Science, A. P. Felty and A. Middeldorp, Eds., vol. 9195. Springer, 2015, pp. 378–388. [Online]. Available: https://doi.org/10.1007/978-3-319-21401-6_26
  * [2] M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, and T. Winterhalter, “Coq coq correct! verification of type checking and erasure for coq, in coq,” _Proc. ACM Program. Lang._ , vol. 4, no. POPL, pp. 8:1–8:28, 2020. [Online]. Available: https://doi.org/10.1145/3371076
  * [3] C. Hermida, U. S. Reddy, and E. P. Robinson, “Logical relations and parametricity - A reynolds programme for category theory and programming languages,” _Electron. Notes Theor. Comput. Sci._ , vol. 303, pp. 149–180, 2014. [Online]. Available: https://doi.org/10.1016/j.entcs.2014.02.008
  * [4] S. Givant, “The calculus of relations as a foundation for mathematics,” _J. Autom. Reason._ , vol. 37, no. 4, p. 277–322, Nov. 2006. [Online]. Available: https://doi.org/10.1007/s10817-006-9062-x
  * [5] A. Miquel, “The Implicit Calculus of Constructions,” in _Typed Lambda Calculi and Applications_ , ser. Lecture Notes in Computer Science, vol. 2044\. Springer, 2001, pp. 344–359.
  * [6] J. Krivine, _Lambda-calculus, types and models_ , ser. Ellis Horwood series in computers and their applications. Masson, 1993, available from Krivine’s web page.
  * [7] P. Pistone, “On completeness and parametricity in the realizability semantics of system F,” _Log. Methods Comput. Sci._ , vol. 15, no. 4, 2019. [Online]. Available: https://doi.org/10.23638/LMCS-15(4:6)2019
  * [8] J. R. Hindley and J. P. Seldin, _Lambda-Calculus and Combinators: An Introduction_ , 2nd ed. USA: Cambridge University Press, 2008.
  * [9] J. C. Reynolds, “Types, Abstraction and Parametric Polymorphism,” in _Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983_ , R. E. A. Mason, Ed. North-Holland/IFIP, 1983, pp. 513–523.
  * [10] P. Wadler, “The Girard-Reynolds isomorphism (second edition),” _Theor. Comput. Sci._ , vol. 375, no. 1-3, pp. 201–226, 2007. [Online]. Available: https://doi.org/10.1016/j.tcs.2006.12.042
  * [11] H. P. Barendregt, “Lambda Calculi with Types,” in _Handbook of Logic in Computer Science (Vol. 2)_ , S. Abramsky, D. M. Gabbay, and S. E. Maibaum, Eds. New York, NY, USA: Oxford University Press, Inc., 1992, pp. 117–309.
  * [12] H. D. E. III, A. Stump, and R. McCleeary, “Dualized simple type theory,” _Log. Methods Comput. Sci._ , vol. 12, no. 3, 2016. [Online]. Available: https://doi.org/10.2168/LMCS-12(3:2)2016
  * [13] P. Wadler, “Recursive types for free!” 1990, available at https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt.
  * [14] T. Uustalu and V. Vene, “Primitive (Co)Recursion and Course-of-Value (Co)Iteration, Categorically,” _Informatica, Lith. Acad. Sci._ , vol. 10, no. 1, pp. 5–26, 1999. [Online]. Available: http://www.mii.lt/informatica/htm/INFO141.htm
  * [15] C. Jenkins and A. Stump, “Monotone recursive types and recursive data representations in cedille,” _CoRR_ , vol. abs/2001.02828, 2020, in second round of reviewing as of November, 2020. [Online]. Available: http://arxiv.org/abs/2001.02828
  * [16] B. Werner, “Une Théorie des Constructions Inductives,” Ph.D. dissertation, Université Paris-Diderot - Paris VII, 1994. [Online]. Available: https://tel.archives-ouvertes.fr/tel-00196524
  * [17] J. van Oosten, “Realizability: A historical essay,” _Math. Struct. Comput. Sci._ , vol. 12, no. 3, pp. 239–263, 2002. [Online]. Available: https://doi.org/10.1017/S0960129502003626
  * [18] A. Troelstra, “Chapter vi - realizability,” in _Handbook of Proof Theory_ , ser. Studies in Logic and the Foundations of Mathematics, S. R. Buss, Ed. Elsevier, 1998, vol. 137, pp. 407 – 473. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S0049237X98800219
  * [19] J. C. Mitchell, _Foundations for programming languages_ , ser. Foundation of computing series. MIT Press, 1996\.
  * [20] K. Sojakova and P. Johann, “A general framework for relational parametricity,” in _Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018_ , A. Dawar and E. Grädel, Eds. ACM, 2018, pp. 869–878.
  * [21] N. R. Krishnaswami and D. Dreyer, “Internalizing Relational Parametricity in the Extensional Calculus of Constructions,” in _Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy_ , ser. LIPIcs, S. R. D. Rocca, Ed., vol. 23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 432–451.
  * [22] T. Altenkirch, C. McBride, and W. Swierstra, “Observational equality, now!” in _Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007_ , A. Stump and H. Xi, Eds., 2007, pp. 57–68.
  * [23] R. Atkey, “Relational parametricity for higher kinds,” in _Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France_ , ser. LIPIcs, P. Cégielski and A. Durand, Eds., vol. 16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 46–61. [Online]. Available: http://drops.dagstuhl.de/opus/portals/extern/index.php?semnr=12009
  * [24] G. D. Plotkin and M. Abadi, “A Logic for Parametric Polymorphism,” in _Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings_ , ser. Lecture Notes in Computer Science, M. Bezem and J. F. Groote, Eds., vol. 664. Springer, 1993, pp. 361–375. [Online]. Available: https://doi.org/10.1007/BFb0037093
  * [25] A. Stump, C. Jenkins, S. Spahn, and C. McDonald, “Strong functional pearl: Harper’s regular-expression matcher in cedille,” _Proc. ACM Program. Lang._ , vol. 4, no. ICFP, pp. 122:1–122:25, 2020. [Online]. Available: https://doi.org/10.1145/3409004
  * [26] D. Firsov, R. Blair, and A. Stump, “Efficient mendler-style lambda-encodings in cedille,” in _Interactive Theorem Proving_ , J. Avigad and A. Mahboubi, Eds. Cham: Springer International Publishing, 2018, pp. 235–252.
  * [27] A. Stump, “From realizability to induction via dependent intersection,” _Ann. Pure Appl. Logic_ , vol. 169, no. 7, pp. 637–655, 2018.
  * [28] J.-P. Bernardy, P. Jansson, and R. Paterson, “Parametricity and dependent types,” in _Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming_ , ser. ICFP ’10. New York, NY, USA: Association for Computing Machinery, 2010, p. 345–356. [Online]. Available: https://doi.org/10.1145/1863543.1863592
  * [29] J.-P. Bernardy and G. Moulin, “A computational interpretation of parametricity,” in _Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science_ , ser. LICS ’12. USA: IEEE Computer Society, 2012, p. 135–144. [Online]. Available: https://doi.org/10.1109/LICS.2012.25
  * [30] T. Univalent Foundations Program, _Homotopy Type Theory: Univalent Foundations of Mathematics_. Institute for Advanced Study: https://homotopytypetheory.org/book, 2013.
  * [31] A. Vezzosi, A. Mörtberg, and A. Abel, “Cubical agda: a dependently typed programming language with univalence and higher inductive types,” _Proc. ACM Program. Lang._ , vol. 3, no. ICFP, pp. 87:1–87:29, 2019. [Online]. Available: https://doi.org/10.1145/3341691
  * [32] N. Tabareau, E. Tanter, and M. Sozeau, “The marriage of univalence and parametricity,” _J. ACM_ , vol. 68, no. 1, Jan. 2021. [Online]. Available: https://doi.org/10.1145/3429979