==== TABLE OF CONTENTS ====
Weak-and-strong-normalization-in-pure-type-systems//paper.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/channels.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/erasure.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/introduction.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/metatheory.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/observation-bounds.inc.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/observation-free-spaces.inc.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/observations.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/profiles.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/relational.tex
Weak-and-strong-normalization-in-pure-type-systems//sections/wrappers.tex
Weak-and-strong-normalization-in-pure-type-systems//references.bib
===========================
==== BEGIN Weak-and-strong-normalization-in-pure-type-systems//paper.tex ====
\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{microtype}
\usepackage{enumitem}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning}
\usepackage{placeins}
\usepackage{needspace}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={Weak and strong normalization in pure type systems},
pdfauthor={OpenAI}}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{claim}{Claim}
\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]
\newtheorem{remark}{Remark}[section]
\newtheorem{example}{Example}[section]
\setlist{itemsep=2pt,topsep=4pt}
\title{Weak and strong normalization in pure type systems}
\author{OpenAI}
\date{September 25, 2026}
\begin{document}
\maketitle
\begin{abstract}
We prove that every weakly $\beta$-normalizing pure type system is strongly
$\beta$-normalizing. Both properties quantify over all legal expressions
in all valid contexts, and reduction acts inside type annotations.
No functionality hypothesis is required. This resolves the
$\beta$-Barendregt--Geuvers--Klop conjecture.
\end{abstract}
\setcounter{tocdepth}{1}
\tableofcontents
\clearpage
\input{sections/introduction}
\input{sections/metatheory}
\input{sections/profiles}
\input{sections/observations}
\input{sections/wrappers}
\input{sections/channels}
\input{sections/relational}
\input{sections/erasure}
\bibliographystyle{plain}
{\small
\bibliography{references}
}
\end{document}
==== END Weak-and-strong-normalization-in-pure-type-systems//paper.tex ====
==== BEGIN Weak-and-strong-normalization-in-pure-type-systems//sections/channels.tex ====
\section{Typed data channels}
\label{chan-section}
We retain the labelled proof and data fragment, its fixed ambient context,
the proof-formula constructors, and the data-path wrappers constructed
above. In particular, a formula is a stable data type sorted at the logic
vertex $b$; its proofs have mode $\mathsf p$. All data introduced in this
section have mode $\mathsf d$. Saying that a type is \emph{sorted at a
vertex} means that it is typed at every sort belonging to that vertex. This
asserts the indicated typings, and does not assert that the vertex is its
exact profile.
The aim is to construct a common type of probes that works with different
choices of a data type and a data parameter. We first build observations
and predicates for one type, then query objects and a bundle that retains
the chosen parameter. These give a probe type independent of those
choices and a second observation channel on that type. The permitted
logical quantifier domains are recorded at the end of the section.
For reference, an even data path $\rho$ from a vertex at which $T$ is sorted
has the operations
\[
\operatorname{pack}_{\rho}(t):W_{\rho}(T),\qquad
\operatorname{use}_{\rho}(w;x.\Phi),
\]
where $t:T$, $w:W_{\rho}(T)$, and $\Phi$ is a formula under $x:T$.
An odd data path has the operations
\[
\operatorname{mk}_{\rho}(x.\Phi):W_{\rho}(T),\qquad
\langle w,t\rangle_{\rho}.
\]
The last expressions in both displays are formulas. We use the proof
builders of Lemma~\ref{lem:enc-data-cancellation} in the following form:
\begin{equation}
\begin{aligned}
\operatorname{use}_{\rho}(\operatorname{pack}_{\rho}(t);x.\Phi)
&\leftrightarrow \Phi[x:=t] &&(\rho\text{ even}),\\
\langle\operatorname{mk}_{\rho}(x.\Phi),t\rangle_{\rho}
&\leftrightarrow \Phi[x:=t] &&(\rho\text{ odd}).
\end{aligned}
\label{chan-cancellation}
\end{equation}
These are logical biconditionals with typed proof terms, rather than
equations permitting replacement inside data. Subscripts may name a
particular resulting type instead of its fixed path. Even when paths are
reused, their source type and their role are fixed by that subscript.
\subsection{The required paths and the first channel}
Assume the configuration to be excluded: $C$ is a plain active strongly
connected component of the secondary graph, it has an internal negative
edge, and
\begin{equation}
\begin{gathered}
(I,J,k)\text{ is a profile triple},\qquad J,k,d=\{s\}\in C,\\
\operatorname{Ax}(s)\ne\varnothing,\qquad
\operatorname{Ax}(s)\longrightarrow I
\text{ by a primary positive path}.
\end{gathered}
\label{chan-configuration}
\end{equation}
The logic component $S$ has its odd closed walk and all-$S$ triple, as in
the preceding construction. We do not assume that $C$ itself has an odd
closed walk.
\begin{lemma}[Choice of paths]
\label{chan-paths}
There is a retained negative edge associated to a triple $(p,n,g)$, with
$p,g\in C$, and there are fixed secondary paths
\[
\alpha:k\longrightarrow p\quad\text{odd},\qquad
\beta:p\longrightarrow k\quad\text{odd},\qquad
\kappa:g\longrightarrow J\quad\text{even},
\]
all inside $C$. There are also fixed secondary paths
\[
\lambda:k\longrightarrow j\quad\text{odd},\qquad
\theta:k\longrightarrow h\quad\text{even},
\]
where $j$ and $h$ are direct vertices. In particular,
$\eta=\beta\theta:p\longrightarrow h$ is odd.
\end{lemma}
\begin{proof}
If $C$ has an odd closed walk, between any two of its vertices there are
paths of both parities: choose paths to and from the base of that walk,
and insert the walk once to change parity. Choose any internal retained
negative $(p,n,g)$ and then choose the three required parities for
$\alpha$, $\beta$, and $\kappa$.
Suppose instead that every closed walk in $C$ is even. Color its vertices
by the parity of a path from a fixed vertex. The color is well defined:
appending a fixed return path to two such paths shows that their parities
are equal. A positive edge preserves color and a negative edge changes
it. The positive edge $J\longrightarrow k$ of the triple in
\eqref{chan-configuration} is retained, since $J,k\in C\subseteq H$;
hence $J$ and $k$ have the same color. There is a negative edge entering
this color. Indeed, take any internal negative. If it enters the other
color, follow a directed return path to its source; that path must contain
a negative edge entering the color of $k$. Choose such an edge
$p\longrightarrow g$, with its retained triple $(p,n,g)$. Thus $g$ has
the color of $J,k$, and $p$ has the opposite color. Connectivity now gives
$\kappa$ even and $\alpha,\beta$ odd.
Finally, $k$ is plain. By the definition of plainness it has an odd path
to a direct vertex $j$ and an even path to a direct vertex $h$. They need
not have the same endpoint and need not stay inside $C$. Choose them as
$\lambda$ and $\theta$. Concatenating $\beta$ with $\theta$ gives the
claimed odd path $\eta$.
\end{proof}
Fix also a path $\delta:d\longrightarrow k$ inside $C$, with no parity
condition. We use $\delta$ only to form a type. Work for the moment under
the data declaration $A:s$. This is a valid declaration because
$\operatorname{Ax}(s)$ is nonempty. Define
\begin{equation}
\begin{aligned}
B(A)&=W_{\delta}(A),&
L_c(A)&=W_{\alpha}(B(A)),\\
L(A)&=W_{\lambda}(B(A)),&
\mathsf P_L(A)&=W_{\eta}(L_c(A)).
\end{aligned}
\label{chan-basic-types}
\end{equation}
When $A$ is fixed, omit it from the notation. The sort ledger is
\[
\begin{array}{c|c|l}
\text{data type}&\text{sorted at}&\text{support}\\ \hline
A&d=\{s\}&A:s\\
B(A)&k&\delta:d\longrightarrow k\\
L_c(A)&p&\alpha:k\longrightarrow p\text{ odd}\\
L(A)&j&\lambda:k\longrightarrow j\text{ odd}\\
\mathsf P_L(A)&h&\eta:p\longrightarrow h\text{ odd}
\end{array}
\]
Each line follows from the corresponding data-path formation lemma.
For instance, $\operatorname{mk}_{L}(t.\Phi)$ binds $t:B(A)$, whereas
$\operatorname{mk}_{\mathsf P_L}(c.\Phi)$ binds $c:L_c(A)$. These
different sources will be important below.
\begin{definition}[Logical and raw channel values]
\label{chan-raw-log}
For $y:L$, $c:L_c$, and $P:\mathsf P_L$, put
\[
\begin{aligned}
\operatorname{Raw}(y)
&=\operatorname{mk}_{L_c}(t.\langle y,t\rangle_L):L_c,\\
\operatorname{Log}(c)
&=\operatorname{mk}_{L}(t.\langle c,t\rangle_{L_c}):L,\\
\operatorname{Round}(y)&=\operatorname{Log}(\operatorname{Raw}(y)):L,\\
P@y&=\langle P,\operatorname{Raw}(y)\rangle_{\mathsf P_L}.
\end{aligned}
\]
For a formula $\Phi$ under $x:L$, define
\[
\operatorname{pred}(x.\Phi)
=\operatorname{mk}_{\mathsf P_L}
(c.\Phi[x:=\operatorname{Log}(c)]):\mathsf P_L.
\]
Here $t:B(A)$ and $c:L_c(A)$ in their respective callbacks.
\end{definition}
\begin{lemma}[Rounding and predicate evaluation]
\label{chan-rounding}
There are proof builders, for $y:L$ and $t:B(A)$, of
\begin{equation}
\langle\operatorname{Round}(y),t\rangle_L
\leftrightarrow\langle y,t\rangle_L.
\label{chan-primitive-round}
\end{equation}
For every formula $\Phi$ under $x:L$ and every $w:L$, there is a proof of
\begin{equation}
\operatorname{pred}(x.\Phi)@w
\leftrightarrow\Phi[x:=\operatorname{Round}(w)].
\label{chan-predicate-evaluation}
\end{equation}
\end{lemma}
\begin{proof}
For \eqref{chan-primitive-round}, cancellation for $\operatorname{Log}$
gives the comparison with
$\langle\operatorname{Raw}(y),t\rangle_{L_c}$, and cancellation for
$\operatorname{Raw}$ compares this with $\langle y,t\rangle_L$.
Apply $\mathsf{pl}$ to these two biconditionals. For
\eqref{chan-predicate-evaluation}, expand $@$ and cancel
$\operatorname{mk}_{\mathsf P_L}$ at the exact argument
$c=\operatorname{Raw}(w)$. Its callback becomes
$\Phi[x:=\operatorname{Log}(\operatorname{Raw}(w))]$, which is the
displayed formula by definition.
\end{proof}
\subsection{Bits stored by pairs of odd wrappers}
Two odd wrappers store one bit while retaining formula observations of
the original input. Iterating this construction will distinguish the
finite query markers.
\begin{definition}[A double wrapper]
\label{chan-double}
Let $T_1=W_{\rho}(T)$ and $T_2=W_{\sigma}(T_1)$ for two odd data paths.
Use subscripts $1$ and $2$ for their respective constructors and
evaluations. For $t:T$ define two data embeddings
\[
\operatorname{emb}_1(t)
=\operatorname{mk}_2(f.\langle f,t\rangle_1),\qquad
\operatorname{emb}_0(t)
=\operatorname{mk}_2(f.\neg\langle f,t\rangle_1),
\qquad f:T_1.
\]
Both have type $T_2$. Set
\[
\operatorname{if}(G;H,H')=(G\land H)\lor(\neg G\land H'),
\]
and, for $v:T_2$ and a formula $\Phi$ under $u:T$, set
\[
\begin{aligned}
\operatorname{bit}(v)
&=\langle v,\operatorname{mk}_1(u.\top)\rangle_2,\\
\operatorname{rec}(v;u.\Phi)
&=\operatorname{if}\bigl(\operatorname{bit}(v);
\langle v,\operatorname{mk}_1(u.\Phi)\rangle_2,
\neg\langle v,\operatorname{mk}_1(u.\Phi)\rangle_2\bigr).
\end{aligned}
\]
\end{definition}
\begin{lemma}[Canonical bit and recovery proofs]
\label{chan-double-laws}
For $\epsilon\in\{0,1\}$ there are proofs of the signed bit
\[
\begin{cases}
\operatorname{bit}(\operatorname{emb}_1(t)),&\epsilon=1,\\
\neg\operatorname{bit}(\operatorname{emb}_0(t)),&\epsilon=0,
\end{cases}
\]
and a proof of
\[
\operatorname{rec}(\operatorname{emb}_{\epsilon}(t);u.\Phi)
\leftrightarrow\Phi[u:=t].
\]
\end{lemma}
\begin{proof}
Cancel the second wrapper, then the first. Evaluation of
$\operatorname{emb}_1(t)$ against $\operatorname{mk}_1(u.\Phi)$ is
biconditional to $\Phi[u:=t]$; evaluation of
$\operatorname{emb}_0(t)$ against the same value is biconditional to
$\neg\Phi[u:=t]$. Each comparison follows by $\mathsf{pl}$ from the two
cancellation proofs. With $\Phi=\top$, the proof of $\top$ and these
comparisons give the signed bits. If $\epsilon=1$, the definition of
$\operatorname{rec}$ then selects the positive comparison. If
$\epsilon=0$, it selects the negation of the negative comparison. The
propositional double-negation equivalence is available from
$\mathsf{pl}$ by Lemma~\ref{lem:enc-propositional}, since the logical
constructors and classical proof builders have already been derived in
the labelled fragment. Thus
$\mathsf{pl}$ gives the recovery biconditional in both cases.
\end{proof}
To record the iteration explicitly, begin with $T_0=L_c$ and define, for
$1\le r\le4$,
\[
T_{2r-1}=W_{\beta}(T_{2r-2}),\qquad
T_{2r}=W_{\alpha}(T_{2r-1}),\qquad
\operatorname{Big}=T_8.
\]
The even-indexed types are sorted at $p$ and the odd-indexed types at $k$.
Let $\operatorname{emb}^{(r)}$, $\operatorname{bit}_r$, and
$\operatorname{rec}_r$ refer to the $r$th pair. For a string
$\epsilon=(\epsilon_1,\ldots,\epsilon_r)$ put
\[
E_0(c)=c,\qquad
E_r(c;\epsilon)=\operatorname{emb}^{(r)}_{\epsilon_r}
(E_{r-1}(c;\epsilon_1,\ldots,\epsilon_{r-1})).
\]
The bit observations at level $r$ are the formulas
\[
\begin{aligned}
H_{r,r}(v)&=\operatorname{bit}_r(v),\\
H_{r,a}(v)&=\operatorname{rec}_r(v;u.H_{r-1,a}(u))
&&(1\le a=stealth,baseline=(current bounding box.center)]
\node (I) at (0,1.1) {$I=\pi(D)$};
\node (L) at (-1.4,-.5) {$L\supseteq J$};
\node (J) at (1,-.5) {$J=\pi(E)$};
\node (K) at (4,.45) {$K=\pi(\Pi x:D.E)$};
\draw[->] (I) -- node[above] {$-$} (K);
\draw[->] (J) -- node[below right] {$+$} (K);
\draw[->] (L) -- node[above] {$+$} (J);
\end{tikzpicture}
\caption{The domain and open codomain point to their product. An
instantiated codomain has profile $L\supseteq J$ and also has a
positive path to the product. The edge $L\to J$ is omitted if $L=J$.}
\label{fig:profile-dependencies}
\end{figure}
Order the strongly connected components so that every predecessor
component is processed first. At a given stage let $S$ be the current
component and $U$ the union of the already processed components.
Thus $U$ is predecessor-closed, and every predecessor of $S$ lies in
$U\cup S$. The graph immediately gives the following facts:
\begin{enumerate}
\item the domain and open codomain of an $S$ product have profiles
in $U\cup S$;
\item every instantiated codomain of that product has profile in
$U\cup S$;
\item any feasible enlargement of a profile in $S$ lies in $U\cup S$;
\item any feasible enlargement of a profile in $U$ lies in $U$.
\end{enumerate}
All statements also hold after valid thinning or context conversion.
\subsection{Application tests and candidates}
Use the saturated context $\Omega$ from the preliminaries. A judgment
over $\Omega$ means a judgment over some finite prefix; finitely many
judgments may always be thinned to a common prefix. Profile invariance
makes their profiles independent of this choice. An \emph{actual
type} is a normal sorted expression over $\Omega$, or a literal sort.
For such a type put
\[
\operatorname{Ty}(T)=\{h:\Omega\vdash h:T\},\qquad
\top_T=\operatorname{Ty}(T)\cap\operatorname{SN}_\beta.
\]
Here and below strong normalization includes reduction in annotations.
A \emph{tested stack at $T$} is a finite list defined inductively.
The empty list is always a tested stack. If $T=\Pi x:D.E$,
$n\in\top_D$, and $\vec m$ is a tested stack at
\[
T_n=(E[x:=n])^\#,
\]
then $(n,\vec m)$ is a tested stack at $T$. This definition follows
these exact successive types; it does not range over alternative
typings of a term. Define
\[
G_T=\{h\in\operatorname{Ty}(T):
h\,\vec n\in\operatorname{SN}_\beta
\text{ for every tested stack }\vec n\text{ at }T\}.
\]
We shall establish, component by component, the invariant
\begin{equation}
G_T=\top_T\qquad(\pi(T)\in U).
\label{eq:processed-invariant}
\end{equation}
\begin{lemma}[Elementary properties of the tests]
\label{lem:test-properties}
For every actual type $T$, $G_T\subseteq\top_T$. If $T$ is a literal
sort, equality holds. Every variable typed at $T$ belongs to $G_T$.
If $T=\Pi x:D.E$, $h\in G_T$, and $n\in\top_D$, then
$h\,n\in G_{T_n}$.
\end{lemma}
\begin{proof}
The empty stack gives the inclusion; at a literal sort it is the only
stack. A variable followed by finitely many strongly normalizing
arguments is strongly normalizing: its head never contracts, and a
reduction decreases the sum of the arguments' reduction heights.
This proves the assertion for variables. For propagation, append any
tested stack at $T_n$ to $n$ and apply the definition of $G_T$.
Application and conversion give the required exact typing at $T_n$.
\end{proof}
\begin{lemma}[Head expansion for strong normalization]
\label{lem:sn-head-expansion}
Suppose that $D,P,n,m_1,\ldots,m_k$ are strongly normalizing and that
\[
P[x:=n]m_1\cdots m_k
\]
is strongly normalizing. Then
$(\lambda x:D.P)n m_1\cdots m_k$ is strongly normalizing.
\end{lemma}
\begin{proof}
Every strongly normalizing expression has a finite maximal reduction
length. Indeed, reduction is finitely branching; if lengths were
unbounded, at least one immediate reduct would again have unbounded
lengths, and iterating this choice would give an infinite reduction.
Write $\ell(Q)$ for this maximal length and induct on
\[
\ell(D)+\ell(P)+\ell(n)+\sum_{i=1}^k\ell(m_i).
\]
The head reduct is strongly normalizing by hypothesis. Every other
immediate reduct changes one displayed component and strictly lowers
this sum. Its head contractum is either unchanged or is a reduct of
the old head contractum. For a step in $n$, contract the corresponding
step in each of its finitely many copies in $P[x:=n]$; there may be
zero copies. For a step in the annotation, the contractum is unchanged.
Thus the new contractum is strongly normalizing, and the induction
applies. Every immediate reduct is strongly normalizing, which proves
the claim.
\end{proof}
\begin{definition}[Candidate at an actual type]
\label{def:candidate}
A candidate at $T$ is a set $C$ satisfying
$G_T\subseteq C\subseteq\top_T$ and the following head-expansion
property: if
\[
r=(\lambda x:D.P)n\,\vec m\in\operatorname{Ty}(T),
\]
all displayed components $D,P,n,\vec m$ are strongly normalizing, and
$P[x:=n]\vec m\in C$, then $r\in C$. Denote the candidates at $T$
by $\mathcal C(T)$.
\end{definition}
Reduction closure is not part of this definition. All subsequent
candidate arguments use only the properties just stated.
This is a local variant of the reducibility-candidate method
\cite[Chapters~6 and~14]{Girard1989}; the next lemma proves its required
lattice and product closure directly.
\begin{lemma}[Candidate lattice and product tests]
\label{lem:candidate-lattice}
The inclusion-ordered set $\mathcal C(T)$ is a complete lattice with
largest element $\top_T$. Write $\bot_T$ for its least element.
For an actual product $T=\Pi x:D.E$, choose a set
$A\subseteq\top_D$. For each $n\in A$ choose any family of candidates
$C_{n,a}\in\mathcal C(T_n)$ indexed by a set $Q_n$. Then
\begin{equation}
\{h\in\top_T:\text{for every }n\in A\text{ and }a\in Q_n,
\ h n\in C_{n,a}\}
\label{eq:product-test-candidate}
\end{equation}
is a candidate at $T$.
\end{lemma}
\begin{proof}
Lemma~\ref{lem:sn-head-expansion} shows that $\top_T$ is a candidate.
Intersections of candidates preserve all three requirements of
Definition~\ref{def:candidate}; take the empty intersection to be
$\top_T$. Therefore every family has a meet, and its join is the
intersection of its common upper bounds. This family of upper bounds
is nonempty because it contains $\top_T$. In particular, the least
candidate is the intersection of all candidates.
For \eqref{eq:product-test-candidate}, a term in $G_T$ passes every
test by Lemma~\ref{lem:test-properties} and the containment
$G_{T_n}\subseteq C_{n,a}$. Suppose a head contractum belongs to
\eqref{eq:product-test-candidate} and its expansion has strongly
normalizing components. Lemma~\ref{lem:sn-head-expansion} gives the
expansion's membership in $\top_T$. Append a prescribed $n\in A$ to
its spine. The enlarged head contractum lies in $C_{n,a}$ for every
$a$, and all enlarged components are strongly normalizing. Head
expansion in $C_{n,a}$ gives the required membership of the enlarged
spine. This proves every test, without using reduction closure of a
candidate.
\end{proof}
At profiles in $U$, the invariant
\eqref{eq:processed-invariant} forces every candidate to equal
$\top_T$. This is why previously processed types need no further
choices.
\subsection{The interface for one component}
\label{subsec:candidate-interface}
We now specify exactly what a component construction must supply.
The context $\Gamma$ and its syntax will be called \emph{generic};
a typed substitution $\xi:\Gamma\to\Omega$ supplies raw actual
images. An environment also contains auxiliary parameters $\theta$
for the declarations. Each construction below specifies their sets.
Require an empty parameter environment and compatible parameter
extensions along every typed context extension. Restrictions to
preceding declarations are understood when interpreting declaration
types.
For each normal generic expected type $T$ with
$\pi_\Gamma(T)\in S$, the construction supplies a candidate
\[
R_{\Gamma,T}(\xi,\theta)
\in\mathcal C\bigl((T\xi)^\#\bigr).
\]
For any other normal generic expected type use the convention
\[
R_{\Gamma,T}(\xi,\theta)=\top_{(T\xi)^\#}.
\]
When no ambiguity arises write simply $R_T$. Actual profiles obtained
from generic profiles in $S$ lie in $U\cup S$, and an actual profile
in $U$ makes the candidate equal to top.
The required properties are the following.
\begin{enumerate}
\item\label{item:interface-invariance}
\emph{Invariance.} Valid thinning, context conversion, and pointwise
convertible actual images preserve the candidates on old syntax when
the old parameters are unchanged. Capture-avoiding renaming of generic declared and bound variables preserves
the interpretation, with the substitution and parameter environment reindexed
on declared variables and all actual images and parameter values unchanged.
\item\label{item:interface-product}
\emph{Product equality.} Let $T=\Pi x:D.E$ have generic profile in
$S$ and actual profile in $S$. For each $n\in R_D$, specify a
nonempty collection $Q_{T,n}$ of compatible parameter extensions to
$\Gamma,x:D$ with substitution $\xi[x\mapsto n]$. Then $R_T$
equals the following product-test candidate. Its members are exactly
the $h\in\top_{(T\xi)^\#}$ such that, for every $n\in R_D$:
\begin{itemize}
\item if the actual type $(E(\xi[x\mapsto n]))^\#$ has profile
in $S$, then $h n\in R_E(\xi[x\mapsto n],\theta')$ for
every $\theta'\in Q_{T,n}$;
\item if that actual profile lies in $U$, then $h n$ is strongly
normalizing at that exact normal type.
\end{itemize}
Application is well typed because the actual domain of the normal
product $(T\xi)^\#$ is $(D\xi)^\#$; substitution and normalization
identify its instantiated codomain with the displayed actual type.
The generic domain profile belongs to $U\cup S$, so $R_D$ is the
candidate supplied by the construction or the prescribed top in $U$.
\item\label{item:interface-specialization}
\emph{Specialization.} In the product situation, if
$\Gamma\vdash N:D$, $N\xi\in R_D$, and $h\in R_T$, then
\begin{equation}
h(N\xi)\in
R_{\Gamma,(E[x:=N])^\#}(\xi,\theta).
\label{eq:interface-specialization}
\end{equation}
It is enough to find one of the tested parameter extensions for which
the codomain candidate is contained in the candidate on the right.
If the actual codomain profile is in $U$, this follows directly from
the strong-normalization test.
\end{enumerate}
Both directions of the product-equality requirement are required: the lambda case uses its
introduction direction and application uses its elimination direction.
A typed environment $(\xi,\theta)$ is \emph{admissible} if, for each
declaration $x:B$ of $\Gamma$, its image satisfies the following
condition, evaluated over the preceding declarations:
\[
\begin{cases}
\xi(x)\in R_{B^\#},&\pi(B)\in S,\\
\xi(x)\in\operatorname{SN}_\beta,&\pi(B)\in U,\\
\xi(x)\in G_{(B\xi)^\#},&\pi(B)\notin U\cup S.
\end{cases}
\]
The exact typings in these conditions follow from typed substitution
and conversion. Admissibility imposes no separate restriction on the
auxiliary parameters.
\begin{lemma}[Transport of strongly normalizing terms]
\label{lem:sn-fundamental}
Assume \eqref{eq:processed-invariant} and an implementation of
the three interface requirements in Section~\ref{subsec:candidate-interface}
for $S$. If $\Gamma\vdash M:A$, the expression $M$ is strongly
normalizing, and $(\xi,\theta)$ is admissible, then
\begin{equation}
M\xi\in R_{\Gamma,A^\#}(\xi,\theta).
\label{eq:sn-fundamental}
\end{equation}
\end{lemma}
\begin{proof}
Induct lexicographically on $(\ell(M),|M|)$, where $|M|$ is syntax
size including annotations. The induction is simultaneous over all
typings, contexts, and admissible environments. A proper subexpression
has no larger reduction height and smaller size; a beta reduct has
strictly smaller height. Typed substitution gives all required actual
typings throughout.
We shall repeatedly use a fresh-variable extension. If a binder has
raw generic annotation $B$, then $B\xi$ is sorted over a finite
prefix of $\Omega$. Saturation supplies a fresh variable $z$ declared
at that raw type, beyond a common prefix for the finite expressions
in question. Choose $z$ outside the free names of all other images.
It belongs to $G_{(B\xi)^\#}$ by
Lemma~\ref{lem:test-properties}, and hence satisfies whichever of
the three admissibility conditions applies. Any allowed parameter
extension can be used. Invariance retains the assumptions on old
variables. If the induction proves the body with $x$ sent to $z$
strongly normalizing, renaming $z$ back to a bound $x$ proves strong
normalization of the open substituted body.
For a sort, $M\xi=M$ is normal, and its expected normal type is a
literal sort. At a literal sort $G$ equals top, so this suffices for
membership in any candidate. For a product, apply the induction to
its domain and to its open codomain under a fresh-variable extension.
The two substituted components are strongly normalizing, so the
product is strongly normalizing. Its expected normal type is again
a literal sort, giving the conclusion.
Let $M=\lambda x:B.P$. The induction on $B$, and on $P$ under a
fresh-variable extension, proves strong normalization of the actual
annotation and open body. Hence $M\xi$ is strongly normalizing.
This already proves the conclusion unless both the generic and the
actual normalized expected types have profiles in $S$. In the latter
case write $A^\#=\Pi x:D.E$. Generation and product compatibility
identify $D$ with the normal form of $B$ and identify $E$ with the
normal body type, after context conversion under the binder.
Context-convert the generic body judgment to
$\Gamma,x:D\vdash P:E$. Take an arbitrary $n\in R_D$ and arbitrary
prescribed parameter extension in $Q_{A^\#,n}$. Convert $n$ to the
actualized type $D\xi$ and extend this context's substitution by
$x\mapsto n$. This is admissible:
the generic domain profile is in $U\cup S$, and the test condition is
exactly the required candidate or SN condition. Apply the induction
to the context-converted judgment for $P$ in this very extension.
It gives the required codomain candidate for the head contractum of
$(M\xi)n$. The actual annotation, open body and $n$ are strongly
normalizing. Head expansion in that codomain candidate proves the
test. If the actual codomain profile is in $U$, use any compatible
parameter extension, the body's strong normalization, and
Lemma~\ref{lem:sn-head-expansion}. We have verified every product
test; the introduction direction of
the product-equality requirement proves the conclusion.
For an application, inspect its entire left-associated spine. If its
head is a lambda, write
\[
M=(\lambda x:B.P)N\,\vec L.
\]
Contract its first redex generically to $M'$. Subject reduction gives
$\Gamma\vdash M':A$ and $\ell(M')<\ell(M)$, so the induction gives
$M'\xi\in R_{A^\#}$. The components $B,P,N,\vec L$ are proper
subexpressions. Their inductions, using a fresh-variable extension for
the open $P$, give strong normalization of every component after
substitution. Substitution commutes with the displayed contraction up
to alpha conversion. Head expansion in $R_{A^\#}$ therefore proves
the result. This step does not invoke reduction closure of a candidate.
The remaining case is a neutral spine $xN_1\cdots N_k$, including
$k=0$. Starting at the normal form of the declaration type of $x$,
generation and neutral uniqueness determine its successive normal
expected types. Whenever a next argument occurs, the preceding type
is a product; convert that argument to its normalized domain and take
the normalized instantiated codomain as the next type. The induction
applied to each $N_i$ at this exact domain gives its candidate
membership and, in particular, strong normalization after substitution.
Typed substitution and confluence identify the actual successive
types with the normal forms of the corresponding generic types.
Track membership along the spine. A $G$ prefix propagates by
Lemma~\ref{lem:test-properties}. If the head declaration has profile
in $U$, admissibility and profile growth put it in actual top in $U$,
hence in $G$ by \eqref{eq:processed-invariant}. If a prefix has generic
profile in $S$, an actual profile in $U$ likewise gives $G$. Otherwise
its candidate product test applies to the next argument, and
\eqref{eq:interface-specialization} gives the next candidate. That
next generic profile lies in $U\cup S$ by the positive codomain path;
on reaching $U$ its membership is again in $G$. A head declaration
outside $U\cup S$ starts in $G$ by admissibility and requires no
further restriction on profiles. Thus the final prefix belongs either
to the desired candidate or to its subset $G$. No other spine head
can type as an application. This completes the induction.
\end{proof}
\begin{proposition}[Advancing one component]
\label{prop:advance-component}
Under the hypotheses of Lemma~\ref{lem:sn-fundamental},
\eqref{eq:processed-invariant} also holds for every actual type with
profile in $S$.
\end{proposition}
\begin{proof}
Fix $h\in\top_T$ with $\pi(T)\in S$ and any tested stack
$(n_1,\ldots,n_k)$ at $T$. Choose a common finite prefix $\Gamma$
of $\Omega$ supporting the relevant exact typings and use the
identity substitution. Choose parameters successively; all variable
images lie in $G$ and therefore the environment is admissible.
Apply Lemma~\ref{lem:sn-fundamental} separately to $h$ and to each
$n_i$ at its exact successive domain. Each is strongly normalizing
by hypothesis or by the definition of a tested stack.
Start with the resulting candidate membership of $h$ and iterate the
product tests and specialization along the stack. Each encountered
type has profile in $U\cup S$. In $S$ specialization supplies the
next candidate membership; in $U$ the invariant supplies $G$, which
propagates across every remaining frame. Thus $h n_1\cdots n_k$ is
strongly normalizing. The argument never assumes strong normalization
of an intermediate generic application and never applies the
fundamental lemma to such an application. Since the stack was
arbitrary, $h\in G_T$. The reverse inclusion is
Lemma~\ref{lem:test-properties}.
\end{proof}
\begin{proposition}[Completion of the interface argument]
\label{prop:interfaces-imply-sn}
If the interface can be implemented at every strongly connected
component, then every legal expression of the PTS is strongly
normalizing.
\end{proposition}
\begin{proof}
Process the finitely many components and apply
Proposition~\ref{prop:advance-component}. At the end, $G_T=\top_T$
for every actual type with nonempty profile. Empty-profile actual
types are literal sorts, for which this equality already holds by
Lemma~\ref{lem:test-properties}.
Suppose a typable expression is not strongly normalizing and choose
one of least syntax size, among all valid contexts and typings. Its
proper syntactic children are typable in the corresponding contexts,
including under binders, and so are strongly normalizing. A variable
or sort is normal; a product or lambda with strongly normalizing
children is strongly normalizing. The expression must therefore be
an application $f n$, with $f,n$ strongly normalizing. Generation
types $f$ at a product and $n$ at its domain. Normalize that product,
convert these typings, and embed the finite context into $\Omega$.
The resulting normal product is an actual type with nonempty profile:
it is sorted by correctness of types and cannot be a literal sort.
The equality $G_T=\top_T$ and its one-frame test now give strong
normalization of $f n$, a contradiction. This also handles an empty
feasible-profile graph, since the hypothetical application would
itself produce a feasible product profile.
Finally, every legal expression is typable by validity and correctness
of types, or is a literal sort. Literal sorts are normal. Hence the
conclusion holds with the full legal-expression and open-context scope.
\end{proof}
The remaining task is to construct the interface. We now do so in two
cases using only the profile graph. The other components require the
additional semantic construction developed later.
Figure~\ref{fig:component-contracts} separates the construction of an
interface from its use in the normalization induction. For the third
case, the observation construction has an additional graph hypothesis.
The typed obstruction proves that hypothesis from system-wide weak
normalization, independently of the candidate interpretation. Thus the
third branch, like the first two, supplies the full interface before
the processed invariant is advanced.
\begin{figure}[ht]
\centering
\begin{tikzpicture}[>=Stealth,
contract/.style={draw,rounded corners,align=center,font=\small,
inner sep=6pt,text width=4.2cm}]
\node[contract,text width=11.8cm] (input) at (0,0)
{Finite specification and system-wide weak normalization;\\
current component $S$, processed predecessors $U$, and $G_T=\top_T$ on $U$};
\node[contract] (simple) at (-3.2,-2.25)
{No odd closed walk, or no all-$S$ profile triple\\
Propositions~\ref{prop:signed-component} and~\ref{prop:one-child-component}};
\node[contract] (remaining) at (3.2,-2.25)
{Remaining components: observation construction and typed exclusion\\
Propositions~\ref{obs:interface-theorem} and~\ref{prop:enc-exclusion}};
\node[contract,text width=10.7cm] (interface) at (0,-4.25)
{Candidate interface for $S$ (Section~\ref{subsec:candidate-interface}):\\
invariance, product equality in both directions, and specialization};
\node[contract,text width=10.7cm] (advance) at (0,-5.85)
{$G_T=\top_T$ also on $S$ (Proposition~\ref{prop:advance-component});\\
after all components, strong normalization (Proposition~\ref{prop:interfaces-imply-sn})};
\draw (input.south) -- (0,-.95);
\draw[->] (0,-.95) -| (simple.north);
\draw[->] (0,-.95) -| (remaining.north);
\draw (simple.south) -- (-3.2,-3.45) -- (0,-3.45);
\draw (remaining.south) -- (3.2,-3.45) -- (0,-3.45);
\draw[->] (0,-3.45) -- (interface.north);
\draw[->] (interface) -- (advance);
\end{tikzpicture}
\caption{The contracts of one component step. The right branch combines
the conditional observation construction with the independent proof of
its graph hypothesis. The arrows to the interface assert the complete
three-part contract, before any use of component advancement.}
\label{fig:component-contracts}
\end{figure}
\FloatBarrier
\section{Two component constructions}
\label{sec:simple-components}
Keep a current component $S$ and the invariant on its processed
predecessors $U$. The first construction uses signs to compensate for
the opposite variances of domain and codomain. The second uses a
single chain in each normal type when its two product children cannot
both remain in $S$.
\subsection{Components without an odd closed walk}
\begin{proposition}[The signed fixed-point construction]
\label{prop:signed-component}
If $S$ has no odd closed walk, it admits the candidate interface.
\end{proposition}
\begin{proof}
Choose a vertex of $S$. Assign to each vertex the parity of any path
from the chosen vertex to it. This is well defined: append a return
path to two proposed paths; different parities would produce an odd
closed walk. Give even vertices sign $+$ and odd vertices sign $-$.
Every internal positive edge preserves sign, and every internal
negative edge reverses sign.
Let $\mathcal T_S$ be the set of actual types with profile in $S$.
It is a set, since these are finite syntax over the countable context
$\Omega$. On
\[
\mathcal L=
\prod_{T\in\mathcal T_S}\mathcal C(T)
\]
use inclusion in coordinates with sign $+$ and reverse inclusion in
coordinates with sign $-$. This is a complete lattice by
Lemma~\ref{lem:candidate-lattice}. Extend a vector $v$ to actual
types in $U$ by $v_T=\top_T$.
Define an operator $F:\mathcal L\to\mathcal L$. At a nonproduct
type set $F(v)_T=\top_T$. At $T=\Pi x:D.E$, let
\[
F(v)_T=\{h\in\top_T:\text{for every }n\in v_D,
\ h n\in v_{(E[x:=n])^\#}\}.
\]
All indices belong to $U\cup S$ by the dependency graph, and this
is a candidate by Lemma~\ref{lem:candidate-lattice}.
The operator is monotone in the mixed order. In the usual inclusion
order its product clause is antitone in the domain coordinate and
monotone in every instantiated-codomain coordinate. An internal domain
has the opposite sign to $T$ by its negative edge. An instantiated
codomain in $S$ has the same sign as $T$ by its positive path through
the open codomain: the intermediate vertex must also lie in $S$,
since a vertex in $U$ has all its predecessors in $U$. Coordinates
in $U$ are constant. These observations
give exactly the required coordinatewise monotonicity, in either sign
of the output.
Tarski's fixed-point theorem \cite[Theorem~1]{Tarski1955} gives a fixed
point. We recall its short existence proof, which needs no continuity
assumption. Let $a$ be the supremum of all
$v$ satisfying $v\le F(v)$. For every such $v$, monotonicity gives
$v\le F(v)\le F(a)$, so $a\le F(a)$. Then
$F(a)\le F(F(a))$, making $F(a)$ one of the elements whose supremum
is $a$; hence $F(a)\le a$. Fix such a vector $a$.
No auxiliary parameters are needed. For a generic normal type $T$
with profile in $S$, define $R_T=a_{(T\xi)^\#}$ if its actual
profile is in $S$, and top otherwise. At a generic product with
actual profile in $S$, its actual normalized domain and all actual
instantiated codomains are exactly the indices in the operator clause.
Thus the fixed-point equality gives the required product equality,
with the unique parameter extension.
The actual normalized type determines the candidate, so thinning,
context conversion and pointwise convertible images preserve it.
For specialization the two actual type expressions
\[
E(\xi[x\mapsto N\xi])
\quad\hbox{and}\quad ((E[x:=N])^\#)\xi
\]
are convertible by substitution composition and normalization.
Their normal forms are identical. The two candidates are consequently
equal when that profile is in $S$, and both are top in $U$. A generic
child in $U$ remains there under substitution, so no additional case
arises. This proves all interface requirements.
\end{proof}
\subsection{Components with at most one internal product child}
Suppose now that there is no profile triple $(I,J,K)$ with
$I,J,K\in S$. For a normal type $T$ of profile in $S$, start at its
root. At a product continue to its child of profile in $S$, if it has
one; there is at most one. Stop at a nonproduct or at a product with
no such child. This is a finite path in the syntax tree.
If the path ends at a neutral expression whose head $y$ is free in
the starting context of $T$, define the \emph{support} of $T$ to be
$y$. Define its \emph{polarity} to be $+$ or $-$ according to whether
the path takes an even or odd number of domain steps. In every other
case the support is empty. Also declare support empty at a generic
profile outside $S$. In particular a head bound strictly inside
$T$ is not its support. The support of a codomain, considered in its
own extended context, may of course be its immediately preceding
binder.
Assign each declaration of a generic context a bit $0$ or $1$;
these are the parameters $\theta$. At a neutral we use the candidate
extremum selected by its head's bit, with $0$ selecting bottom and $1$
selecting top. Define candidates recursively on normal generic types
as follows. At an actual profile in $U$ use top. At a generic profile
outside $S$ also use top, as in the interface. Otherwise:
\begin{itemize}
\item at a sort use top;
\item at a neutral with head $y$ use
$\bot_{(T\xi)^\#}$ or $\top_{(T\xi)^\#}$ according to
$\theta(y)$;
\item at a product $T=\Pi x:D.E$ use the product-test candidate
in Section~\ref{subsec:candidate-interface}. There is one prescribed
bit for $x$: use $0$ if the support of $E$ is $x$ with positive
polarity, $1$ if it is $x$ with negative polarity, and $1$ if
$x$ is not supported. If $E$ has profile in $U$, its bit is
irrelevant and we again choose $1$.
\end{itemize}
Every recursive child is smaller syntax; candidate existence follows
from Lemma~\ref{lem:candidate-lattice}. Context variables can always
be assigned bits, and the prescribed extension is nonempty.
\begin{lemma}[Dependence on support]
\label{lem:support-dependence}
For fixed typed actual images, the candidate of an $S$ type depends
on the bits of its starting context only through its support, if any.
Valid thinning and context conversion preserve the support, its
polarity, and the candidates. Pointwise convertible actual images
preserve the candidates when old bits agree.
\end{lemma}
\begin{proof}
Induct on the normal type. Sorts and actual-$U$ cases do not use
bits. A neutral uses only its head bit. At a product, any child in
$U$ is interpreted as top; only the unique $S$ child can depend on
old bits. Its support is propagated to the parent unless it is the
product's own binder, whose bit is fixed by the displayed rule.
This proves the dependence assertion. Profile invariance preserves
the same product path and its domain parity under thinning and
context conversion. In those operations and under convertible images,
the actual normal types agree. The recursive product tests then have
identical domains, codomains and prescribed bits, proving the stated
invariances.
\end{proof}
Use the notation $A\preceq_+B$ for $A\subseteq B$ and
$A\preceq_-B$ for $A\supseteq B$. Regard signs as $+1$ and $-1$
when multiplying them.
\begin{lemma}[Comparison after generic substitution]
\label{lem:support-substitution}
Let $\Gamma,y:B,\Delta$ be valid, let $\Gamma\vdash N:B$, and
let $T$ be a normal type of profile in $S$ in that context. Put
\[
\Gamma'=\Gamma,\Delta[y:=N],\qquad
T'=(T[y:=N])^\#.
\]
Take typed substitutions of the two contexts into $\Omega$ whose
images are compatible with composition: the pre-substitution image
of $y$ is convertible to the actual image of $N$, and the other
images agree up to conversion. Equip the substitutions with bits
$\theta,\theta'$. Fix a comparison sign $\delta\in\{+,-\}$ and
assume:
\begin{enumerate}
\item the bits agree on any variable supported by both $T$ and $T'$;
\item if $y$ supports $T$ with polarity $\varepsilon$, then its
pre-substitution bit is $0$ when $\delta\varepsilon=+$ and
$1$ when $\delta\varepsilon=-$.
\end{enumerate}
Then, at their common actual normal type,
\[
R_T(\xi,\theta)
\preceq_\delta R_{T'}(\xi',\theta').
\]
\end{lemma}
\begin{proof}
Induct on the pre-substitution syntax of $T$. The actual normal
types agree by substitution composition and confluence. If their
profile lies in $U$, both candidates are top. Otherwise that profile
lies in $S$, and so does the generic profile of $T'$: profile growth
puts it in $U\cup S$, and a generic profile in $U$ could only have
actual profile in $U$.
A sort is unchanged. A neutral whose head is not $y$ remains a
neutral with the same head after substitution and normalization; if
its actual profile is in $S$, the supported head is common and its
bit agrees. At a neutral headed by $y$, its polarity is positive and
the prescribed bit chooses the least candidate for forward inclusion,
or the greatest candidate for reverse inclusion. This compares it
with every possible candidate of $T'$. In particular we do not
recurse into the possibly larger normal expression obtained by
substituting for $y$.
Let $T=\Pi x:D.E$, choosing $x$ fresh for $N$ and for the
substitution data. The post-substitution type is again a product,
with its two substituted components normalized. Context-convert the
open codomain to the normalized post domain. To compare the product
test candidates in direction $\delta$, compare their domain
candidates in direction $-\delta$. On each common test compare their
codomain candidates in direction $\delta$, extending the actual
images by that same raw test and using the respective prescribed
bits for $x$. For example, for forward inclusion every post domain
test must be a pre domain test, and its pre codomain candidate must
be contained in its post codomain candidate.
If a pre child is in $U$, its generic substitute remains in $U$ and
both actual child candidates are top. If its generic substitute
grows into $U$, the common actual child profile is again in $U$,
with the same conclusion. In all other required child comparisons,
both generic child profiles are in $S$. Such a post child must be
the same unique $S$ child as before substitution: a pre off-path
child in $U$ cannot grow into $S$. Every common supported variable
other than the new binder $x$ therefore inherits the agreement
condition from the parent. If $y$ supports the child, the prescribed
extremum condition is also inherited: a domain step reverses both
the comparison direction and the support polarity, and a codomain
step reverses neither.
It remains to check the bits of $x$ when it is supported in both
open codomains. The pre support path ends at a neutral with head
$x$, which substitution for $y$ cannot change. Every product on
that path persists. The post support path must follow the same
positions: a pre off-path child remains in $U$, while truncation
of the path into $U$ would prevent the post codomain from being
supported by $x$. Thus both paths have the same number of domain
steps, their polarities agree, and the prescribed bits of $x$
agree. If substitution exposes $x$ through a neutral headed by
$y$, that portion of the induction instead stops at the extremum
case already proved; it imposes no further shared-support condition.
All hypotheses of the child inductions now hold. Their inclusions
give the desired product inclusion by the universal test definition,
in either direction. This completes the induction.
\end{proof}
\begin{proposition}[The one-child construction]
\label{prop:one-child-component}
If no profile triple has all three vertices in $S$, then the
bit-parametrized candidates above implement the candidate interface.
\end{proposition}
\begin{proof}
Candidate existence and product equality follow from the recursion.
Lemma~\ref{lem:support-dependence} gives the required invariances.
To verify specialization, let
$T=\Pi x:D.E$, take $\Gamma\vdash N:D$ with $N\xi\in R_D$,
and let $h\in R_T$. Its product test gives
\[
h(N\xi)\in R_E(\xi[x\mapsto N\xi],\theta_x)
\]
when the actual codomain profile lies in $S$; here $\theta_x$ is
the prescribed binder extension. Apply
Lemma~\ref{lem:support-substitution} to substitution for $x$ in
$E$, with comparison direction $+$. All old bits agree. The
prescribed bit of $x$ is exactly $0$ for positive support and $1$
for negative support, as that lemma requires. It follows that the
last candidate is contained in
$R_{(E[x:=N])^\#}(\xi,\theta)$, proving specialization. At an
actual codomain profile in $U$, the strong-normalization test gives
specialization directly. Arbitrary bits are allowed on the starting
context, and every prescribed or arbitrary binder extension exists.
All interface requirements are satisfied.
\end{proof}
Consequently, only components having both an odd closed walk and a
profile triple entirely inside the component remain. The next
construction will provide their interface under a stated graph
exclusion. Once that exclusion is proved from system-wide weak
normalization, Proposition~\ref{prop:interfaces-imply-sn} completes
the normalization argument.
==== END Weak-and-strong-normalization-in-pure-type-systems//sections/profiles.tex ====
==== BEGIN Weak-and-strong-normalization-in-pure-type-systems//sections/relational.tex ====
\section{Relational coding of the diagonal argument}
\label{rel-section}
We continue with the fixed labelled wrappers, their data cancellation law
(Lemma~\ref{lem:enc-data-cancellation}), and their predicate evaluation laws
\eqref{chan-predicate-evaluation} and \eqref{chan-x-evaluation}.
In particular, for either of the
predicate spaces under consideration,
\[
\operatorname{pred}(y.\Phi)@w
\ \leftrightarrow\ \Phi[\operatorname{Round}w/y].
\]
Until a specialization is explicitly made, \(A:s\) and \(m:M(A)\) are
open data parameters. Write \(L=L(A)\). The variables \(y,z,w,a\)
range over \(L\), \(P,P'\) over \(\mathsf P_L\), \(x,x'\) over \(X\),
and \(i,i'\) over \(\mathsf P_X\). The spaces \(V,X,\mathsf P_X\)
are independent of \(A,m\). All displayed quantifiers use the fixed
direct-vertex annotations: \(j\) for \(L,X\) and \(h\) for
\(\mathsf P_L,\mathsf P_X\). The other parameters are parameters of
term builders, not additional logical quantifiers.
The operations \(\mathsf{pl}\), \(\mathsf{All}\), \(\mathsf{Ex}\),
\(\mathsf{Gd}\), \(\operatorname{to}\), and
\(\operatorname{back}\) have the typed expansions already constructed.
For clarity, when a proof below says that specified proofs yield a
formula by \(\mathsf{pl}\), that formula is its target. Quantifiers
are treated as propositional atoms until explicitly introduced or
instantiated. An existential is eliminated only into the displayed
target, which is independent of its locally opened witnesses.
Our goal is a proof of the terminal formula $F_b$ in the ambient labelled
context. First we construct relations and probes for open parameters
$A,m$. Next we choose $A_0,m_0$ and prove admissibility. At that
specialization, three tagged copies turn the query formulas into class
and pairing laws. Section~\ref{rel-diagonal} then uses these laws to
construct the terminal proof.
\subsection{Generic relations and probes}
\begin{definition}[Admissible queries and observational equivalence]
\label{rel-admissible}
Define
\[
\begin{aligned}
P\approx P'&=\forall y.\,(P@y\leftrightarrow P'@y),\\
i\approx i'&=\forall x.\,(i@x\leftrightarrow i'@x),\\
\operatorname{Adm}
&=\neg D(m)\land
\bigwedge_{t\ {\rm structural}}\forall P,P'.\,
\bigl(P\approx P'\Rightarrow
(\operatorname{qry}_t(m,P)\leftrightarrow
\operatorname{qry}_t(m,P'))\bigr),\\
\operatorname{Good}(P)
&=\bigl(\forall y.\,(P@y\leftrightarrow
P@\operatorname{Round}y)\bigr)
\land\operatorname{qry}_G(m,P),\\
y\sim z&=\forall P.\,
\bigl(\operatorname{Good}(P)\Rightarrow
(P@y\leftrightarrow P@z)\bigr).
\end{aligned}
\]
The finite Boolean operations have fixed bracketing. From
\(ad:\operatorname{Adm}\) obtain \(d_m:\neg D(m)\) by projection.
For each structural \(t\), projection followed by two instantiations
and application defines
\[
\operatorname{qr}_t(e):
\operatorname{qry}_t(m,P)\leftrightarrow
\operatorname{qry}_t(m,P')
\qquad(e:P\approx P').
\]
\end{definition}
\begin{lemma}[Equivalence and rounding]
\label{rel-equivalence}
The relation \(\sim\) has reflexivity, symmetry, and transitivity
builders. There is a builder
\(\operatorname{RoundRel}(y):y\sim\operatorname{Round}y\).
For \(e:a\sim a'\) and \(f:c\sim c'\) there is a builder
\[
\operatorname{cong}(e,f):
(a\sim c)\leftrightarrow(a'\sim c').
\]
These builders require no admissibility assumption.
\end{lemma}
\begin{proof}
Reflexivity is
\(\Lambda P.\lambda^*h.\mathsf{pl}_{P@y\leftrightarrow P@y}()\).
For symmetry, under \(e:y\sim z\), introduce \(P,h\), instantiate
\(e[P]\cdot h\), and apply \(\mathsf{pl}\) to reverse its
biconditional. For transitivity, under
\(e:y\sim z\) and \(f:z\sim w\), introduce \(P,h\) and apply
\(\mathsf{pl}_{P@y\leftrightarrow P@w}\) to
\(e[P]\cdot h,f[P]\cdot h\).
For rounding introduce \(P,h\), project
\(\forall w.(P@w\leftrightarrow P@\operatorname{Round}w)\)
from \(h:\operatorname{Good}(P)\), and instantiate it at \(y\).
Write these builders as \(\operatorname{refl}\),
\(\operatorname{sym}\), and \(\operatorname{trans}\).
The two components of the last biconditional are
\[
\begin{aligned}
&\lambda^*u.\operatorname{trans}
(\operatorname{sym}(e),\operatorname{trans}(u,f)),\\
&\lambda^*u.\operatorname{trans}
(e,\operatorname{trans}(u,\operatorname{sym}(f))).
\end{aligned}
\]
In the first line \(u:a\sim c\), and in the second
\(u:a'\sim c'\), so the endpoints are respectively
\(a'\sim c'\) and \(a\sim c\).
\end{proof}
\begin{definition}[Class, union, and pairing predicates]
\label{rel-pair-definition}
Put
\[
\begin{aligned}
c_y&=\operatorname{pred}(w.w\sim y),\\
u_{yz}&=\operatorname{pred}(w.(w\sim y)\lor(w\sim z)),\\
\operatorname{Is}_t(y)&=\operatorname{qry}_{C_t}(m,c_y)
&&(t=0,\ell,r),\\
T_t(y,z)&=\operatorname{Is}_0(y)\land
\operatorname{Is}_t(z)\land
\operatorname{qry}_{E_t}(m,u_{yz})
&&(t=\ell,r),\\
\operatorname{form}(P,a,z)
&=\bigl(\exists y.\,(T_\ell(y,z)\land P@y)\bigr)
\lor T_r(a,z),\\
\operatorname{Pair}(P,a)&=
\operatorname{pred}(z.\operatorname{form}(P,a,z)).
\end{aligned}
\]
These are data definitions, independent of any proof of
\(\operatorname{Adm}\).
\end{definition}
\begin{lemma}[Congruence of the relational predicates]
\label{rel-pair-congruence}
There are unrounded evaluation proofs
\[
c_y@w\leftrightarrow(w\sim y),\qquad
u_{yz}@w\leftrightarrow((w\sim y)\lor(w\sim z)).
\]
Equivalent parameters give \(c_y\approx c_{y'}\) and
\(u_{yz}\approx u_{y'z'}\). Under \(ad:\operatorname{Adm}\),
the predicates \(\operatorname{Is}_t,T_t\) respect \(\sim\).
Moreover, still under \(ad\), and under \(P\approx P'\),
\(a\sim a'\), and \(z\sim z'\)
there are proofs of
\[
\operatorname{form}(P,a,z)\leftrightarrow
\operatorname{form}(P',a',z'),
\]
and, under the first two of these assumptions, of
\(\operatorname{Pair}(P,a)\approx\operatorname{Pair}(P',a')\).
In particular, under \(ad\) there is
\[
\operatorname{pv}(P,a,z):
\operatorname{Pair}(P,a)@z
\leftrightarrow\operatorname{form}(P,a,z).
\]
\end{lemma}
\begin{proof}
Predicate evaluation first gives
\[
c_y@w\leftrightarrow(\operatorname{Round}w\sim y).
\]
Apply relation congruence with
\(\operatorname{RoundRel}(w)\) and \(\operatorname{refl}(y)\);
propositional chaining gives the first displayed evaluation.
For the union do this separately for \(y\) and \(z\), then chain
their disjunctions. For \(e:y\sim y'\), congruence with
\(\operatorname{refl}(w),e\), together with the two class
evaluations, gives \(c_y@w\leftrightarrow c_{y'}@w\).
Introduce \(w\) to obtain the class comparison. For the union
use the two parameter congruences inside the disjunction before
introducing \(w\).
Apply \(\operatorname{qr}_{C_t}\) to the class comparison to
obtain the \(\operatorname{Is}_t\) comparison. For \(T_t\),
combine the two resulting \(\operatorname{Is}\) comparisons and
\(\operatorname{qr}_{E_t}\) applied to the union comparison.
For \(\operatorname{form}\), fix \(y\). The \(T_\ell\)
comparison with its first argument unchanged, together with
\((P\approx P')[y]\), gives
\[
(T_\ell(y,z)\land P@y)\leftrightarrow
(T_\ell(y,z')\land P'@y).
\]
Apply \(\mathsf{Ex}_y\), then combine its result with the
\(T_r(a,z)\leftrightarrow T_r(a',z')\) comparison by
\(\mathsf{pl}\). Predicate evaluation for \(\operatorname{Pair}\)
has right side
\(\operatorname{form}(P,a,\operatorname{Round}z)\).
The just-proved form congruence, with \(P,a\) unchanged and
\(\operatorname{RoundRel}(z)\), gives \(\operatorname{pv}\).
Finally fix \(z\), combine both \(\operatorname{pv}\) proofs
with form congruence at unchanged \(z\), and introduce \(z\).
\end{proof}
\begin{definition}[Lifts and uniform probes]
\label{rel-lifts}
Define data, still with open \(A,m\), by
\[
\begin{aligned}
\operatorname{Part}(v)&=\operatorname{pred}(y.v\diamond_m y),\\
\operatorname{sb}(v,m,a)&=\operatorname{qry}_R
(m,\operatorname{Pair}(\operatorname{Part}(v),a)),\\
\operatorname{lift}_m(a)&=\operatorname{mk}_X(v.\operatorname{sb}(v,m,a)).
\end{aligned}
\]
For \(i:\mathsf P_X\), define \(z_i:V\) by the following data
lambda. At \(z:Z\), pack along the even path \(g\to J\) the
data function
\[
\lambda^{\mathsf d,\mathsf d}w:
\operatorname{Single}(z^\downarrow).
\operatorname{send}_n
\bigl(\operatorname{Access}
(w;o,y.i@\operatorname{lift}_o(y))\bigr),
\]
where all channel types and the lift in its body use
\(A=z^\downarrow\). This defines the body of
\(\lambda^{\mathsf d,\mathsf d}z:Z.\,\cdots\).
The variable \(o\) is the data parameter supplied by
\(\operatorname{Access}\). Thus \(z_i\) has no free \(A,m\).
Put
\[
\begin{aligned}
\operatorname{le}(i,x)&=[x z_i],\\
x\simeq x'&=\forall i.\,(\operatorname{le}(i,x)\leftrightarrow \operatorname{le}(i,x')),\\
\operatorname{Valid}(x)&=\forall i,i'.\,
\bigl(i\approx i'\Rightarrow
(\operatorname{le}(i,x)\leftrightarrow \operatorname{le}(i',x))\bigr),\\
\operatorname{Ext}(i)&=\forall x,x'.\,
\bigl(x\simeq x'\Rightarrow(i@x\leftrightarrow i@x')\bigr),\\
\operatorname{Resp}(v)&=\forall y,z.\,
\bigl(y\sim z\Rightarrow
(v\diamond_m y\leftrightarrow v\diamond_m z)\bigr).
\end{aligned}
\]
\end{definition}
\begin{lemma}[Evaluation, validity, and response]
\label{rel-lift-properties}
The relation \(\simeq\) is an equivalence relation, with the
congruence builder of Lemma~\ref{rel-equivalence}, and
\[
\operatorname{RoundRel}_X(x):x\simeq\operatorname{Round}_Xx.
\]
Data cancellation supplies
\[
\operatorname{LP}(i,a):
\operatorname{le}(i,\operatorname{lift}_m a)\leftrightarrow \operatorname{sb}(z_i,m,a).
\]
Under \(ad:\operatorname{Adm}\) there are builders
\begin{align}
z_i\diamond_m y&\leftrightarrow
i@\operatorname{lift}_m(\operatorname{Round}y),
\label{rel-probe-rounded}\\
\operatorname{LC}(e)&:
\operatorname{lift}_m(a)\simeq\operatorname{lift}_m(a')
\qquad(e:a\sim a'), \label{rel-lift-congruence}\\
&\operatorname{Valid}(\operatorname{lift}_m a). \label{rel-lift-valid}
\end{align}
If also \(ex:\operatorname{Ext}(i)\), then
\begin{equation}
z_i\diamond_m y\leftrightarrow i@\operatorname{lift}_m y
\quad\hbox{and}\quad \operatorname{Resp}(z_i).
\label{rel-probe-exact}
\end{equation}
If \(h:\operatorname{Resp}(v)\), then
\begin{equation}
\operatorname{Part}(v)@y\leftrightarrow v\diamond_m y.
\label{rel-part-exact}
\end{equation}
\end{lemma}
\begin{proof}
For \(\simeq\), introduce \(i\) and use propositional
reflexivity, symmetry, or transitivity of the instantiated
biconditionals. Its congruence builder is the pair displayed
in Lemma~\ref{rel-equivalence}, with the relation replaced by
\(\simeq\). Primitive \(X\)-evaluation is preserved by
\(\operatorname{Round}_X\). Apply this preservation at \(z_i\)
and introduce \(i\) to obtain \(\operatorname{RoundRel}_X\).
Cancellation of \(\operatorname{mk}_X\) gives \(\operatorname{LP}\)
at the exact input \(z_i\).
For \eqref{rel-probe-rounded}, the application \(z_iA^\uparrow\)
beta-reduces to the same pack and data lambda at \(A\), since
\((A^\uparrow)^\downarrow=_\beta A\) and the wrapper choices
are fixed. The pack/use cancellation leaves the read of that
function applied to \(\operatorname{Bundle}(m,y)\).
After its raw beta contraction, read/send cancellation leaves
\[
\operatorname{Access}
(\operatorname{Bundle}(m,y);o,w.i@\operatorname{lift}_o(w)).
\]
The Access builder, applied to \(d_m\), compares this with
\(i@\operatorname{lift}_m(\operatorname{Round}y)\).
Chain these three biconditionals by \(\mathsf{pl}\).
To obtain \(\operatorname{LC}(e)\), introduce \(i\).
Pair congruence applied to the reflexive comparison of
\(\operatorname{Part}(z_i)\) and to \(e\), followed by
\(\operatorname{qr}_R\), compares \(\operatorname{sb}(z_i,m,a)\) and
\(\operatorname{sb}(z_i,m,a')\). Combine it with the two \(\operatorname{LP}\)
proofs and introduce \(i\).
For validity introduce \(i,i'\) and \(e:i\approx i'\).
There is a comparison
\(\operatorname{Part}(z_i)\approx\operatorname{Part}(z_{i'})\):
at \(y\), predicate evaluation gives the two expressions
\(z_i\diamond_m\operatorname{Round}y\) and
\(z_{i'}\diamond_m\operatorname{Round}y\).
Apply \eqref{rel-probe-rounded} at precisely
\(\operatorname{Round}y\), and use
\[
e[\operatorname{lift}_m
(\operatorname{Round}(\operatorname{Round}y))].
\]
These proofs propositionally entail the required evaluation
comparison; introduce \(y\). Apply Pair congruence with \(a\)
unchanged, then \(\operatorname{qr}_R\), and finally the two
\(\operatorname{LP}\) proofs. Introducing \(i,i',e\) proves
\eqref{rel-lift-valid}.
For \eqref{rel-probe-exact}, apply \(ex\) at
\(\operatorname{lift}_m y,\operatorname{lift}_m(\operatorname{Round}y)\)
to \(\operatorname{LC}(\operatorname{RoundRel}(y))\).
Combine its result with \eqref{rel-probe-rounded}. Under
\(e:y\sim z\), apply \(ex\) at the two lifts to
\(\operatorname{LC}(e)\), and combine this with the exact
probe evaluations at \(y,z\). Introducing \(y,z,e\) proves
\(\operatorname{Resp}(z_i)\).
Finally predicate evaluation gives
\(\operatorname{Part}(v)@y\leftrightarrow
v\diamond_m\operatorname{Round}y\).
Combine it with \(h[y][\operatorname{Round}y]\cdot
\operatorname{RoundRel}(y)\) to obtain \eqref{rel-part-exact}.
\end{proof}
\subsection{The laws needed for the diagonal argument}
\label{rel-target-laws}
The relations and uniform probes are now defined. Before choosing
$A$ and $m$, we identify the laws their specialization must provide.
For $i:\mathsf P_X$, define
\begin{equation}
\operatorname{Ind}(i)=
\forall x:X.\bigl(\operatorname{Valid}(x)\Rightarrow
(\operatorname{le}(i,x)\Rightarrow i@x)\bigr).
\label{rel-ind-definition}
\end{equation}
This formula says that $i$ contains every valid $x$ for which
$\operatorname{le}(i,x)$ holds. The name records its role in the
well-foundedness diagonal; it does not assume a pre-existing order on $X$.
We shall construct data operations $x\mapsto\delta x:X$ and
$i\mapsto Si:\mathsf P_X$, and a data term
$\operatorname{WF}:X$. Their required properties are
\begin{align*}
&\operatorname{Valid}(\delta x),\qquad
\operatorname{Valid}(\operatorname{WF}),\\
&\operatorname{Ext}(i)\ \Longrightarrow\
\operatorname{Ext}(Si)\ \text{ and }\
(Si@x\leftrightarrow i@\delta x),\\
&\operatorname{Ext}(i),\ \operatorname{Valid}(x)
\ \Longrightarrow\
\bigl(\operatorname{le}(i,\delta x)
\leftrightarrow\operatorname{le}(Si,x)\bigr),\\
&\operatorname{Ext}(i)\ \Longrightarrow\
\bigl(\operatorname{le}(i,\operatorname{WF})
\leftrightarrow\operatorname{Ind}(Si)\bigr).
\end{align*}
Here the outer implication signs describe proof builders with the
displayed inputs, as elsewhere in the construction. We also require
$x\simeq x'$ to imply $\delta x\simeq\delta x'$.
The logical binders introduced in the final diagonal proof range only
over $X$ or $\mathsf P_X$; it also uses the previously proved laws at
their original domains.
These laws already explain the intended role of $\operatorname{WF}$.
For an extensional $i$, a proof of $\operatorname{Ind}(i)$ gives a
proof of $\operatorname{Ind}(Si)$: apply the proof of
$\operatorname{Ind}(i)$ at
the valid point $\delta x$, using the predecessor comparison to turn
$\operatorname{le}(Si,x)$ into $\operatorname{le}(i,\delta x)$.
The shift evaluation then gives the required conclusion $Si@x$.
The last displayed law then gives
$\operatorname{le}(i,\operatorname{WF})$, so validity of
$\operatorname{WF}$ gives $i@\operatorname{WF}$. Section~\ref{rel-diagonal}
uses this consequence with a specified negative predicate to derive
$\bot$; it will prove the construction with every guard in place.
To obtain the predecessor comparison, we will encode three distinguishable
copies of $X$ in $L$. The class and edge queries will identify the
corresponding elements of those copies. Observations of the pairing
predicate on one copy will be equivalent to the evaluations of the
represented predicate; observations on another will identify the point
of evaluation up to $\simeq$. The $R$ query can then express
$\operatorname{le}$ at that point. Its validity guard is essential:
it permits transport between the corresponding
$\operatorname{le}$ formulas for the represented and original predicates.
The next two subsections build
these copies and queries before the guarded diagonal uses them.
\subsection{Three tagged copies and one admissible parameter}
The types $V,X,\mathsf P_X$ and the probes $z_i$ were constructed
uniformly, before any choice of $A,m$. We now use them to choose
$A_0$ and then $m_0$. The observations defining $m_0$ may use those
already constructed probes; they never use $m_0$ itself. This order
will allow us to prove admissibility after defining the data term.
We now choose a fixed \(A_0:s\). Choose the secondary path
\(k\to d\), inside \(C\), so that its concatenation with the
previously fixed \(d\to k\) has even parity and at least four
negative edges, and put \(A_0=W_{k\to d}(V)\).
For completeness, in a component with an odd closed walk a
detour changes the parity if necessary; in a component with a
consistent two-coloring the return paths already have matching
parities. A closed detour through an internal negative exists
by strong connectivity. Inserting it twice preserves parity
and increases the number of negatives. Repeating this insertion
gives the claimed choice.
Split the resulting wrapper from \(V\) to \(B(A_0)\) into
four odd segments \(\rho_1,\ldots,\rho_4\). This is possible
by cutting after the first, second, and third negative;
the remaining number of negatives is odd. Let \(T_0=V\) and
\(T_a=W_{\rho_a}(T_{a-1})\), so \(T_4=B(A_0)\).
The fixed odd path \(k\to j\), denoted \(\rho_5\) here, gives
\(T_5=L(A_0)\). The first odd wrapper defines
\[
y_1(x)=\operatorname{mk}_{\rho_1}(v.[xv]):T_1.
\]
Use the double-embedding construction of Definition~\ref{chan-double}
and Lemma~\ref{chan-double-laws} on \((\rho_2,\rho_3)\)
and on \((\rho_4,\rho_5)\). Denote their signed embeddings
by \(E^{(1)}_\epsilon:T_1\to T_3\) and
\(E^{(2)}_\epsilon:T_3\to T_5\), their bit observations by
\(B_1,B_2\), and their recovery formula builders by
\(\mathcal R_1,\mathcal R_2\). These are notation for the
previous data macros, not logical function spaces.
Fix distinct strings, for example
\[
(b_1(0),b_2(0))=(0,0),\quad
(b_1(\ell),b_2(\ell))=(1,0),\quad
(b_1(r),b_2(r))=(0,1),
\]
and define
\[
\begin{aligned}
x^t&=E^{(2)}_{b_2(t)}(E^{(1)}_{b_1(t)}(y_1(x))),\\
H_2(y)&=B_2(y),\\
H_1(y)&=\mathcal R_2(y;c.B_1(c)),\\
O_i(y)&=\mathcal R_2
(y;c.\mathcal R_1(c;u.\langle u,z_i\rangle_{\rho_1})).
\end{aligned}
\]
Here \(\langle u,z_i\rangle_{\rho_1}\) uses the first odd
wrapper, whose input type is \(V\).
\begin{lemma}[Tagged observations]
\label{rel-tags}
For \(t=0,\ell,r\) there are proofs of the signed bits
\(H_a(x^t)\) if \(b_a(t)=1\), and \(\neg H_a(x^t)\) if
\(b_a(t)=0\), and proofs
\[
O_i(x^t)\leftrightarrow \operatorname{le}(i,x).
\]
Each \(H_a\) and \(O_i\) is invariant, by biconditional, under
\(y\mapsto\operatorname{Round}y\).
Define
\[
\operatorname{Ae}(y,z)=
\bigwedge_{a=1,2}(H_a(y)\leftrightarrow H_a(z))
\land\bigl(\forall i.\,(O_i(y)\leftrightarrow O_i(z))\bigr).
\]
Then \(\operatorname{Ae}\) is an equivalence relation and
there is \(\operatorname{AeRound}(y):
\operatorname{Ae}(y,\operatorname{Round}y)\).
For each tag \(t\), its restriction compares exactly \(\simeq\):
\[
\operatorname{Ae}(x^t,x'^{\,t})\leftrightarrow x\simeq x'.
\]
For distinct tags \(t,u\) there is a proof of
\(\neg\operatorname{Ae}(x^t,x'^{\,u})\).
\end{lemma}
\begin{proof}
The two double-embedding builders give their signed bits and
recover each callback at its exact input. Apply them successively
to \(B_1\) and to \(u\mapsto\langle u,z_i\rangle_{\rho_1}\).
For the latter, first-wrapper cancellation gives
\(\langle y_1(x),z_i\rangle_{\rho_1}\leftrightarrow[xz_i]\).
Propositional chaining gives all the asserted canonical
evaluations. For a general \(y\), the outer bit and every
outer recovery are Boolean combinations of primitive
\(L\)-evaluations at arguments independent of \(y\).
Primitive Round preservation at those arguments, followed
by \(\mathsf{pl}\), therefore gives each invariance proof.
Reflexivity of \(\operatorname{Ae}\) pairs the propositional
bit reflexivities with
\(\Lambda i.\mathsf{pl}_{O_i(y)\leftrightarrow O_i(y)}()\).
For symmetry, project both bit comparisons and the observation
universal, reverse the former by \(\mathsf{pl}\), instantiate
the latter at \(i\), reverse it, and introduce \(i\).
For transitivity perform these projections on both premises,
compose the bit comparisons, and at each \(i\) compose the
two observation comparisons before introducing \(i\).
Reassemble the conjunctions by \(\mathsf{pl}\).
The invariance proofs supply the two bit components of
\(\operatorname{AeRound}\) and, after introduction of \(i\),
its observation component. The congruence builder for
\(\operatorname{Ae}\) is the explicit two-component
transitivity construction of Lemma~\ref{rel-equivalence}.
Given \(e:x\simeq x'\), the canonical signed bits imply
the two same-tag bit comparisons. At \(i\), combine \(e[i]\)
with both canonical \(O_i\) evaluations, then introduce \(i\).
This proves \(\operatorname{Ae}(x^t,x'^{\,t})\).
Conversely project its observation universal, instantiate at
\(i\), and chain the two canonical evaluations to obtain
\(\operatorname{le}(i,x)\leftrightarrow \operatorname{le}(i,x')\); introduce \(i\).
For \(t\ne u\), choose a coordinate where their fixed strings
differ. The two signed-bit proofs contradict the comparison
at that coordinate projected from an assumed
\(\operatorname{Ae}(x^t,x'^{\,u})\).
Abstract that assumption to obtain the negation.
\end{proof}
\begin{definition}[The specialized query object]
\label{rel-specialized-object}
At \(A_0\), for \(P:\mathsf P_L\), define
\[
\begin{aligned}
\mathcal P_G(P)&=\forall y,z.\,
\bigl(\operatorname{Ae}(y,z)\Rightarrow(P@y\leftrightarrow P@z)\bigr),\\
\mathcal P_{C_t}(P)&=\exists x.\forall w.\,
(P@w\leftrightarrow\operatorname{Ae}(w,x^t)),\\
\mathcal P_{E_t}(P)&=\exists x.\forall w.\,
\bigl(P@w\leftrightarrow
(\operatorname{Ae}(w,x^0)\lor\operatorname{Ae}(w,x^t))\bigr),\\
i_P&=\operatorname{pred}_X(x.P@(x^\ell)),\\
\mathcal P_R(P)&=\operatorname{Ext}(i_P)\Rightarrow
\forall x.\bigl(\operatorname{Valid}(x)\Rightarrow
(P@(x^r)\Rightarrow \operatorname{le}(i_P,x))\bigr).
\end{aligned}
\]
Here \(C_t\) has \(t=0,\ell,r\) and \(E_t\) has \(t=\ell,r\).
Define
\[
m_0=\operatorname{mk}_M
\left(bp.\bigvee_{t\ {\rm structural}}
\bigl(\operatorname{Mark}_t(bp)\land
\mathcal P_t(\operatorname{Dec}(bp))\bigr)\right).
\]
The formulas \(\mathcal P_t\) use \(z_i\), tags, and observations
already defined independently of \(m_0\); this is a data term
with no recursive occurrence of itself.
\end{definition}
\begin{lemma}[Respect and admissibility]
\label{rel-query-realization}
For \(d:i\approx i'\) there is a builder
\[
\operatorname{ExtC}(d):
\operatorname{Ext}(i)\leftrightarrow\operatorname{Ext}(i').
\]
For \(e:P\approx P'\), every structural \(t\) has a builder
\(\mathcal P_t(P)\leftrightarrow\mathcal P_t(P')\).
Consequently there are proofs
\[
q_t(P):\operatorname{qry}_t(m_0,P)\leftrightarrow\mathcal P_t(P)
\quad(t\ {\rm structural}),\qquad
ad:\operatorname{Adm}\big|_{A=A_0,m=m_0}.
\]
\end{lemma}
\begin{proof}
Under \(x,x'\), the evaluations \(d[x],d[x']\) propositionally
entail
\[
(x\simeq x'\Rightarrow(i@x\leftrightarrow i@x'))
\leftrightarrow
(x\simeq x'\Rightarrow(i'@x\leftrightarrow i'@x')).
\]
Apply \(\mathsf{All}_{x,x'}\) to obtain
\(\operatorname{ExtC}(d)\).
For \(G\), under \(y,z\), apply \(\mathsf{pl}\) to
\(e[y],e[z]\) with target the comparison of the two implications
whose common antecedent is \(\operatorname{Ae}(y,z)\);
then apply \(\mathsf{All}_{y,z}\).
For \(C_t\), under \(x,w\), the proof \(e[w]\) compares
\[
P@w\leftrightarrow\operatorname{Ae}(w,x^t)
\quad\hbox{with}\quad
P'@w\leftrightarrow\operatorname{Ae}(w,x^t).
\]
Apply \(\mathsf{All}_w\) and then \(\mathsf{Ex}_x\).
For \(E_t\), use exactly the same two typed operations, with
their common right side now
\(\operatorname{Ae}(w,x^0)\lor\operatorname{Ae}(w,x^t)\).
For \(R\), predicate evaluation at \(x\) for \(i_P,i_{P'}\)
has right sides
\[
P@((\operatorname{Round}_Xx)^\ell)
\quad\hbox{and}\quad P'@((\operatorname{Round}_Xx)^\ell).
\]
Combine these evaluations with
\(e[(\operatorname{Round}_Xx)^\ell]\) and introduce \(x\),
obtaining \(d:i_P\approx i_{P'}\).
The proof \(\operatorname{ExtC}(d)\) compares the two
antecedents of \(\mathcal P_R\).
Under \(x,v:\operatorname{Valid}(x)\), combine
\[
e[x^r],\qquad v[i_P][i_{P'}]\cdot d
\]
with target
\[
(P@(x^r)\Rightarrow \operatorname{le}(i_P,x))
\leftrightarrow(P'@(x^r)\Rightarrow \operatorname{le}(i_{P'},x)).
\]
Apply \(\mathsf{Gd}_{v:\operatorname{Valid}(x)}\), then
\(\mathsf{All}_x\). This compares the consequents of
\(\mathcal P_R\). Combine it propositionally with
\(\operatorname{ExtC}(d)\). In particular, the change of
predicate in \(le\) has used its explicit validity guard.
Data cancellation at \(\operatorname{Enc}_t(P)\) compares
\(\operatorname{qry}_t(m_0,P)\) with the defining disjunction
evaluated there. The signed marker proofs eliminate every
disjunct except \(t\), and give a comparison with
\(\mathcal P_t(\operatorname{Dec}(\operatorname{Enc}_t(P)))\).
Introduce \(y\) in the decoder evaluation comparison to get
\[
\operatorname{Dec}(\operatorname{Enc}_t(P))\approx P.
\]
Use the property-respect builder just proved and chain to
obtain \(q_t(P)\). Cancellation at \(bp_\bot\) and the
negations of all its structural markers give \(\neg D(m_0)\).
For each structural \(t\), form
\[
\Lambda P,P'.\lambda^*e.\,
\mathsf{pl}\bigl(q_t(P),q_t(P'),
\text{property-respect}_t(e)\bigr)
\]
with target
\(\operatorname{qry}_t(m_0,P)\leftrightarrow
\operatorname{qry}_t(m_0,P')\).
Together with \(\neg D(m_0)\), these are exactly the
conjuncts of the displayed admissibility formula.
\end{proof}
From this point onward \(A=A_0\), \(m=m_0\), and \(ad\) is
the proof just constructed.
\subsection{Pairing laws at the fixed specialization}
\begin{lemma}[The coded equivalence is the observation equivalence]
\label{rel-observation-equivalence}
There are proofs
\[
\operatorname{GA}(P):
\operatorname{Good}(P)\leftrightarrow\mathcal P_G(P),
\qquad
\operatorname{SA}(y,z):
(y\sim z)\leftrightarrow\operatorname{Ae}(y,z).
\]
For each \(t\), there are builders
\[
\operatorname{Tag}_t(e):x^t\sim x'^{\,t}
\quad(e:x\simeq x'),\qquad
\operatorname{TagBack}_t(f):x\simeq x'
\quad(f:x^t\sim x'^{\,t}).
\]
For \(t\ne u\) there is
\(\operatorname{diff}_{t,u}:\neg(x^t\sim x'^{\,u})\).
\end{lemma}
\begin{proof}
The proof \(q_G(P)\) identifies the second conjunct of
\(\operatorname{Good}(P)\). Its property implies the first:
the builder
\[
\lambda^*g.\Lambda y.\,
g[y][\operatorname{Round}y]\cdot\operatorname{AeRound}(y)
\]
has that implication as type. Combining these by
\(\mathsf{pl}\) gives \(\operatorname{GA}(P)\).
For an observation \(\Phi\) equal to \(H_1,H_2\), or \(O_i\)
with \(i\) temporarily free, put
\(P_\Phi=\operatorname{pred}(w.\Phi(w))\).
Predicate evaluation and Round invariance give, at every \(u\),
an evaluation proof \(P_\Phi@u\leftrightarrow\Phi(u)\).
Under \(a:\operatorname{Ae}(u,w)\), project the relevant bit
comparison, or project and instantiate its observation
universal at the free \(i\). Combine it with the two evaluations
to get \(P_\Phi@u\leftrightarrow P_\Phi@w\).
Introducing \(u,w,a\) proves \(\mathcal P_G(P_\Phi)\);
apply \(\operatorname{back}(\operatorname{GA}(P_\Phi),-)\)
to get \(\operatorname{Good}(P_\Phi)\).
Under \(e:y\sim z\), the proof
\(e[P_\Phi]\cdot\operatorname{Good}(P_\Phi)\), combined
with the two evaluations, gives \(\Phi(y)\leftrightarrow\Phi(z)\).
Take the two bit instances. For \(O_i\), introduce \(i\)
after obtaining this comparison. Their conjunction proves
\(\operatorname{Ae}(y,z)\). Conversely, under
\(a:\operatorname{Ae}(y,z)\), the term
\[
\Lambda P.\lambda^*g.\,
\bigl(\operatorname{to}(\operatorname{GA}(P),g)\bigr)
[y][z]\cdot a
\]
proves \(y\sim z\). Abstract the two premises and pair the
directions to obtain \(\operatorname{SA}\).
Given \(e:x\simeq x'\), use the same-tag direction of
Lemma~\ref{rel-tags}, then \(\operatorname{back}(\operatorname{SA},-)\).
Given \(f:x^t\sim x'^{\,t}\), use
\(\operatorname{to}(\operatorname{SA},f)\) and the reverse
same-tag direction. For distinct tags, introduce
\(f:x^t\sim x'^{\,u}\), map it forward through
\(\operatorname{SA}\), and apply the negation from
Lemma~\ref{rel-tags}. These define the three asserted builders.
\end{proof}
\begin{lemma}[Class and edge witnesses]
\label{rel-witnesses}
For \(t=0,\ell,r\) there is a proof
\[
\operatorname{Is}_t(y)\leftrightarrow
\exists x.\,(y\sim x^t).
\]
For \(t=\ell,r\) there is a proof
\[
T_t(y,z)\leftrightarrow
\exists x.\,((y\sim x^0)\land(z\sim x^t)).
\]
\end{lemma}
\begin{proof}
For the first forward implication, take
\(h:\operatorname{Is}_t(y)\), apply
\(\operatorname{to}(q_{C_t}(c_y),h)\), and open the result
as \(x,p\), where
\[
p:\forall w.\,(c_y@w\leftrightarrow\operatorname{Ae}(w,x^t)).
\]
The class evaluation and reflexivity prove \(c_y@y\).
Apply \(p[y]\) forward and \(\operatorname{SA}(y,x^t)\)
backward to obtain \(y\sim x^t\). Witness the opened \(x\)
in the target existential. The target contains no free
occurrence of either local witness.
For the reverse, open \(x,e:y\sim x^t\).
At \(w\), the class evaluation, congruence with
\(\operatorname{refl}(w),e\), and
\(\operatorname{SA}(w,x^t)\) yield
\(c_y@w\leftrightarrow\operatorname{Ae}(w,x^t)\).
Introduce \(w\), witness \(x\) in \(\mathcal P_{C_t}(c_y)\),
and apply \(q_{C_t}(c_y)\) backward.
For the edge forward implication, take \(h:T_t(y,z)\).
Project both \(\operatorname{Is}\) conjuncts and its query.
Use the first equivalence and open their witnesses as
\[
a,e_a:y\sim a^0,\qquad
b',e_{b'}:z\sim b'^{\,t}.
\]
Map the query forward through \(q_{E_t}(u_{yz})\) and
open its witness as \(x,p\), with
\[
p:\forall w.\,
\bigl(u_{yz}@w\leftrightarrow
(\operatorname{Ae}(w,x^0)\lor\operatorname{Ae}(w,x^t))\bigr).
\]
The union evaluation and reflexivity prove \(u_{yz}@y\)
and \(u_{yz}@z\). Apply \(p\) at each of these points and
the comparisons \(\operatorname{SA}\); the resulting proofs
have types
\[
(y\sim x^0)\lor(y\sim x^t),\qquad
(z\sim x^0)\lor(z\sim x^t).
\]
The term
\[
\lambda^*f.\operatorname{diff}_{0,t}\cdot
\operatorname{trans}(\operatorname{sym}(e_a),f)
\]
negates \(y\sim x^t\). The corresponding term
\[
\lambda^*f.\operatorname{diff}_{t,0}\cdot
\operatorname{trans}(\operatorname{sym}(e_{b'}),f)
\]
negates \(z\sim x^0\). Propositional elimination gives
\(y\sim x^0\) and \(z\sim x^t\); pair them and witness \(x\).
All three openings have the original target existential.
For the reverse, open \(x,e\) and project
\(e_0:y\sim x^0\), \(e_t:z\sim x^t\).
Witness \(x\) with \(e_0\) or \(e_t\) in the first
equivalence backward to obtain the two \(\operatorname{Is}\)
conjuncts. At \(w\), the union evaluation and congruences
along \(e_0,e_t\) compare \(u_{yz}@w\) with
\((w\sim x^0)\lor(w\sim x^t)\). Use the two
\(\operatorname{SA}\) proofs and introduce \(w\), obtaining
the property required for the witness \(x\) in
\(\mathcal P_{E_t}(u_{yz})\). Apply \(q_{E_t}(u_{yz})\)
backward and conjoin the three results.
\end{proof}
\begin{lemma}[The two pairing laws]
\label{rel-pair-laws}
Under \(h:\operatorname{Resp}(v)\), let
\(P_x=\operatorname{Pair}(\operatorname{Part}(v),x^0)\).
For every \(x':X\) there are proofs
\begin{align}
P_x@(x'^{\,\ell})&\leftrightarrow
v\diamond_m(x'^{\,0}), \label{rel-pair-left}\\
P_x@(x'^{\,r})&\leftrightarrow x\simeq x'. \label{rel-pair-right}
\end{align}
\end{lemma}
\begin{proof}
For \eqref{rel-pair-left} forward, first negate
\(T_r(x^0,x'^{\,\ell})\). Given such a proof, map it
forward through Lemma~\ref{rel-witnesses} and open its
witness \(u\) into \(\bot\). Its second conjunct is
\(x'^{\,\ell}\sim u^r\), contradicted by
\(\operatorname{diff}_{\ell,r}\).
Given \(p:P_x@(x'^{\,\ell})\), use
\(\operatorname{pv}\) and this negation to extract
\[
\exists y.\,
(T_\ell(y,x'^{\,\ell})\land\operatorname{Part}(v)@y).
\]
Open it as \(y,q\), and open the edge witness from the
first conjunct as \(u,q_0,q_\ell\), where
\[
q_0:y\sim u^0,\qquad q_\ell:x'^{\,\ell}\sim u^\ell.
\]
The proof \(\operatorname{TagBack}_\ell(q_\ell)\) is
\(x'\simeq u\). Symmetrize it and apply
\(\operatorname{Tag}_0\), then compose with \(q_0\),
to get \(e:y\sim x'^{\,0}\).
From the second conjunct of \(q\), the unrounded Part
evaluation gives \(v\diamond_m y\).
Apply \(h[y][x'^{\,0}]\cdot e\) forward to obtain the
target \(v\diamond_m(x'^{\,0})\). Each opening uses this
fixed target.
For the left reverse implication, a proof of
\(v\diamond_m(x'^{\,0})\) gives
\(\operatorname{Part}(v)@(x'^{\,0})\) by
\eqref{rel-part-exact} backward. Witness \(x'\) with
the two reflexivities in the edge equivalence backward
to get \(T_\ell(x'^{\,0},x'^{\,\ell})\).
Pair these, witness \(y=x'^{\,0}\), inject the resulting
existential into \(\operatorname{form}\), and apply
\(\operatorname{pv}\) backward.
For \eqref{rel-pair-right} forward, negate
\(\exists y.(T_\ell(y,x'^{\,r})\land\operatorname{Part}(v)@y)\).
Open an assumed existential into \(\bot\), open its
\(T_\ell\) witness, and contradict its second conjunct
\(x'^{\,r}\sim u^\ell\) with \(\operatorname{diff}_{r,\ell}\).
Thus \(\operatorname{pv}\) maps a proof of
\(P_x@(x'^{\,r})\) to \(T_r(x^0,x'^{\,r})\).
Open its witness \(u\), with
\(x^0\sim u^0\) and \(x'^{\,r}\sim u^r\).
The two same-tag converses give \(x\simeq u\) and
\(x'\simeq u\). Compose the first with the symmetry of
the second to prove \(x\simeq x'\).
For the reverse, given \(e:x\simeq x'\), witness \(x\)
in the edge equivalence with reflexivity at \(x^0\) and
\(\operatorname{Tag}_r(\operatorname{sym}(e)):
x'^{\,r}\sim x^r\). This gives \(T_r(x^0,x'^{\,r})\);
inject it into \(\operatorname{form}\), then apply
\(\operatorname{pv}\) backward.
Abstract each input proof and pair the two directions.
\end{proof}
\section{The guarded diagonal argument}
\label{rel-diagonal}
The pairing laws are now available at the fixed specialization. We use
them to compare a probe with a predicate on $X$, and then derive a proof
of $F_b$.
The construction below adapts the well-foundedness paradox of Hurkens
\cite{Hurkens1995}, as presented by Geuvers~\cite[Section~2]{Geuvers2007}.
We prove each identity with the validity and extensionality hypotheses
required by the present encoding.
We retain the specialization $A=A_0$, $m=m_0$ and the constructed
proof $ad:\operatorname{Adm}$. Thus every relation and every occurrence
of $\diamond_m$ below uses this fixed specialization. We use the Pair
laws of Lemma~\ref{rel-pair-laws}, the query comparison $q_R$, and the
previously constructed lift and tag builders. All displayed proof
builders are in the labelled fragment. In particular, $\Lambda$ and
$\lambda^*$ denote the established logical introduction rules, and
$\mathsf{pl}_F$ denotes the established propositional proof builder
with target formula $F$. Its use to construct a biconditional supplies
both implication directions; it never replaces a data expression by
a logically equivalent expression. The data parameters $v:V$ used
below are open parameters, not additional logical quantifier domains.
\begin{lemma}[The predicate represented by a response]
\label{rel-response-predicate}
For every data parameter $v:V$, define
\[
i_v=\operatorname{pred}_X(x'.\,v\diamond_m(x'^{\,0}))
:\mathsf P_X.
\]
This data definition requires no proof hypothesis. Given
$h:\operatorname{Resp}(v)$, there are builders
\[
E_h(x):i_v@x\leftrightarrow v\diamond_m(x^0),
\qquad ex_v:\operatorname{Ext}(i_v).
\]
Moreover, for $x:X$ and $u:\operatorname{Valid}(x)$, there is a builder
\begin{equation}
\operatorname{SB}(v,h,x,u):
\operatorname{sb}(v,m,x^0)\leftrightarrow
\operatorname{le}(i_v,x).
\label{rel-sb-law}
\end{equation}
\end{lemma}
\begin{proof}
The predicate evaluation law gives
\[
i_v@x\leftrightarrow
v\diamond_m((\operatorname{Round}_Xx)^0).
\]
On the other hand,
\[
h[x^0][(\operatorname{Round}_Xx)^0]\cdot
\operatorname{Tag}_0(\operatorname{RoundRel}_X(x))
:v\diamond_m(x^0)\leftrightarrow
v\diamond_m((\operatorname{Round}_Xx)^0).
\]
Applying $\mathsf{pl}$ to these two biconditionals at the stated
target gives $E_h(x)$. For $e:x\simeq x'$, put
\[
ex_v=\Lambda x,x'.\lambda^*e.\,
\mathsf{pl}_{\,i_v@x\leftrightarrow i_v@x'}
\bigl(E_h(x),E_h(x'),
h[x^0][x'^{\,0}]\cdot\operatorname{Tag}_0(e)\bigr).
\]
The final premise has type
$v\diamond_m(x^0)\leftrightarrow v\diamond_m(x'^{\,0})$,
so this is a proof of $\operatorname{Ext}(i_v)$.
Fix $x:X$ and write
\[
P_x=\operatorname{Pair}(\operatorname{Part}(v),x^0),
\qquad
i_{P_x}=\operatorname{pred}_X(x'.\,P_x@(x'^{\,\ell})).
\]
The Pair laws, under the present hypothesis $h$, supply
\begin{align*}
L_h(x')&:P_x@(x'^{\,\ell})
\leftrightarrow v\diamond_m(x'^{\,0}),\\
R_h(x')&:P_x@(x'^{\,r})\leftrightarrow x\simeq x'.
\end{align*}
At an arbitrary $x':X$, denote the two predicate evaluation proofs by
\begin{align*}
r_{P_x}(x')&:i_{P_x}@x'
\leftrightarrow P_x@((\operatorname{Round}_Xx')^\ell),\\
r_v(x')&:i_v@x'
\leftrightarrow v\diamond_m((\operatorname{Round}_Xx')^0).
\end{align*}
Using $L_h(\operatorname{Round}_Xx')$ between them gives
\[
d=\Lambda x'.\,
\mathsf{pl}_{\,i_{P_x}@x'\leftrightarrow i_v@x'}
(r_{P_x}(x'),r_v(x'),
L_h(\operatorname{Round}_Xx'))
:i_{P_x}\approx i_v.
\]
Consequently
\[
ex_P=\operatorname{back}(\operatorname{ExtC}(d),ex_v)
:\operatorname{Ext}(i_{P_x}).
\]
We first construct both directions of
\begin{equation}
\mathcal P_R(P_x)\leftrightarrow\operatorname{le}(i_v,x),
\label{rel-r-property-law}
\end{equation}
where, by the definition of $\mathcal P_R$,
\[
\mathcal P_R(P_x)=\operatorname{Ext}(i_{P_x})\Rightarrow
\forall x':X.\bigl(\operatorname{Valid}(x')\Rightarrow
(P_x@(x'^{\,r})\Rightarrow\operatorname{le}(i_{P_x},x'))\bigr).
\]
For the forward direction, assume $g:\mathcal P_R(P_x)$ and put
\[
p_x=\operatorname{back}(R_h(x),\operatorname{refl}(x))
:P_x@(x^r).
\]
Then
\[
(g\cdot ex_P)[x]\cdot u\cdot p_x
:\operatorname{le}(i_{P_x},x),
\qquad
u[i_{P_x}][i_v]\cdot d:
\operatorname{le}(i_{P_x},x)\leftrightarrow
\operatorname{le}(i_v,x).
\]
Thus the forward builder is
\[
\lambda^*g.\,
\operatorname{to}\bigl(u[i_{P_x}][i_v]\cdot d,
(g\cdot ex_P)[x]\cdot u\cdot p_x\bigr).
\]
For the reverse direction, assume $l:\operatorname{le}(i_v,x)$.
Introduce $ex':\operatorname{Ext}(i_{P_x})$, $x':X$,
$u':\operatorname{Valid}(x')$, and $p:P_x@(x'^{\,r})$.
The proof $ex'$ need not be used. Set
\[
e=\operatorname{to}(R_h(x'),p):x\simeq x'.
\]
Here $e[i_v]:\operatorname{le}(i_v,x)\leftrightarrow
\operatorname{le}(i_v,x')$, whereas
\[
u'[i_{P_x}][i_v]\cdot d:
\operatorname{le}(i_{P_x},x')\leftrightarrow
\operatorname{le}(i_v,x').
\]
The required proof of $\operatorname{le}(i_{P_x},x')$ is therefore
\[
\operatorname{back}\bigl(u'[i_{P_x}][i_v]\cdot d,
\operatorname{to}(e[i_v],l)\bigr).
\]
Abstracting, in order, over $p,u',x',ex',l$ gives the reverse
direction of \eqref{rel-r-property-law}; pairing the directions gives
the displayed biconditional.
Finally, by definition,
$\operatorname{sb}(v,m,x^0)=\operatorname{qry}_R(m,P_x)$.
The query comparison is
\[
q_R(P_x):\operatorname{qry}_R(m,P_x)
\leftrightarrow\mathcal P_R(P_x).
\]
Composing its forward direction with the forward direction of
\eqref{rel-r-property-law}, and composing the two reverse directions
in the reverse order, gives \eqref{rel-sb-law}.
\end{proof}
\begin{lemma}[The shift and its predecessor comparison]
\label{rel-shift}
Define the data operations
\[
\delta x=\operatorname{lift}_m(x^0):X,
\qquad
Si=\operatorname{pred}_X(x.\,i@\delta x):\mathsf P_X.
\]
For every $x:X$ there is a proof
$V_\delta(x):\operatorname{Valid}(\delta x)$, and for
$e:x\simeq x'$ there is a proof
$\operatorname{DeltaC}(e):\delta x\simeq\delta x'$.
For $ex:\operatorname{Ext}(i)$ there are builders
\begin{align}
s_{ex}(x)&:Si@x\leftrightarrow i@\delta x,
\label{rel-shift-evaluation}\\
\operatorname{ExtS}(i,ex)&:\operatorname{Ext}(Si),
\label{rel-shift-extensionality}\\
d_s&:i_{z_i}\approx Si. \label{rel-shift-comparison}
\end{align}
For the additional input $u:\operatorname{Valid}(x)$ there is a builder
\begin{equation}
a_{ex,u}:\operatorname{le}(i,\delta x)
\leftrightarrow\operatorname{le}(Si,x).
\label{rel-shift-predecessor}
\end{equation}
\end{lemma}
\begin{proof}
The established validity proof for a lift, applied to $x^0$, is
$V_\delta(x)$. Congruence is the composite
\[
\operatorname{DeltaC}(e)
=\operatorname{LC}(\operatorname{Tag}_0(e)).
\]
Neither construction requires $x$ to be valid or any predicate to
be extensional.
The predicate evaluation law gives
$Si@x\leftrightarrow i@\delta(\operatorname{Round}_Xx)$.
The proof
\[
ex[\delta x][\delta(\operatorname{Round}_Xx)]\cdot
\operatorname{DeltaC}(\operatorname{RoundRel}_X(x))
:i@\delta x\leftrightarrow
i@\delta(\operatorname{Round}_Xx)
\]
and that evaluation give $s_{ex}(x)$ by $\mathsf{pl}$ at the target
in \eqref{rel-shift-evaluation}. Set
\[
\operatorname{ExtS}(i,ex)=
\Lambda x,x'.\lambda^*e.\,
\mathsf{pl}_{\,Si@x\leftrightarrow Si@x'}
\bigl(s_{ex}(x),s_{ex}(x'),
ex[\delta x][\delta x']\cdot\operatorname{DeltaC}(e)\bigr).
\]
This has the type in \eqref{rel-shift-extensionality}.
From $ex$, the earlier response builder gives
$h_i:\operatorname{Resp}(z_i)$, and the earlier exact evaluation
gives, for every $y:L$, a proof
\[
Z_{ex}(y):z_i\diamond_m y\leftrightarrow
i@\operatorname{lift}_m(y).
\]
In particular, at $y=x^0$ the right-hand side is $i@\delta x$.
Together with $E_{h_i}(x)$ and $s_{ex}(x)$ this gives
\[
d_s=\Lambda x.\,
\mathsf{pl}_{\,i_{z_i}@x\leftrightarrow Si@x}
\bigl(E_{h_i}(x),Z_{ex}(x^0),s_{ex}(x)\bigr).
\]
Now assume $u:\operatorname{Valid}(x)$. The three available
biconditionals, with their exact endpoints, are
\begin{align*}
\operatorname{LP}(i,x^0)&:
\operatorname{le}(i,\delta x)
\leftrightarrow\operatorname{sb}(z_i,m,x^0),\\
\operatorname{SB}(z_i,h_i,x,u)&:
\operatorname{sb}(z_i,m,x^0)
\leftrightarrow\operatorname{le}(i_{z_i},x),\\
u[i_{z_i}][Si]\cdot d_s&:
\operatorname{le}(i_{z_i},x)
\leftrightarrow\operatorname{le}(Si,x).
\end{align*}
The forward direction of $a_{ex,u}$ is
\[
\lambda^*t.\,
\operatorname{to}\bigl(u[i_{z_i}][Si]\cdot d_s,
\operatorname{to}\bigl(\operatorname{SB}(z_i,h_i,x,u),
\operatorname{to}(\operatorname{LP}(i,x^0),t)\bigr)\bigr).
\]
Its reverse direction is
\[
\lambda^*t.\,
\operatorname{back}\bigl(\operatorname{LP}(i,x^0),
\operatorname{back}\bigl(\operatorname{SB}(z_i,h_i,x,u),
\operatorname{back}(u[i_{z_i}][Si]\cdot d_s,t)\bigr)\bigr).
\]
Pairing them proves \eqref{rel-shift-predecessor}. The only use of
$u$ is in the response comparison and in transport at the fixed
argument $x$; no unconditional replacement of $i_{z_i}$ by $Si$
inside $\operatorname{le}$ has been made.
\end{proof}
\begin{lemma}[Induction respects predicate equivalence]
\label{rel-ind-congruence}
For $d:i\approx i'$ there is a builder
\[
\operatorname{IndC}(d):
\operatorname{Ind}(i)\leftrightarrow\operatorname{Ind}(i').
\]
This builder needs no extensionality hypothesis on either predicate.
\end{lemma}
\begin{proof}
For $x:X$ and $u:\operatorname{Valid}(x)$ put
\[
c_u=u[i][i']\cdot d:
\operatorname{le}(i,x)\leftrightarrow\operatorname{le}(i',x).
\]
The two directions, paired in the displayed order, are
\begin{align*}
&\lambda^*l.\Lambda x.\lambda^*u.\lambda^*t'.\,
\operatorname{to}\bigl(d[x],
l[x]\cdot u\cdot\operatorname{back}(c_u,t')\bigr),\\
&\lambda^*l'.\Lambda x.\lambda^*u.\lambda^*t.\,
\operatorname{back}\bigl(d[x],
l'[x]\cdot u\cdot\operatorname{to}(c_u,t)\bigr).
\end{align*}
In the first line $l:\operatorname{Ind}(i)$ and
$t':\operatorname{le}(i',x)$; in the second
$l':\operatorname{Ind}(i')$ and $t:\operatorname{le}(i,x)$.
Thus every application has the exact antecedent required by
\eqref{rel-ind-definition}.
\end{proof}
\begin{lemma}[A valid induction object]
\label{rel-wf}
Define, without proof hypotheses,
\[
\operatorname{WF}=\operatorname{mk}_X(v.\,\operatorname{Ind}(i_v)):X.
\]
There is a proof $V_{\operatorname{WF}}:
\operatorname{Valid}(\operatorname{WF})$. For
$ex:\operatorname{Ext}(i)$ there is a builder
\begin{equation}
w_{ex}:\operatorname{le}(i,\operatorname{WF})
\leftrightarrow\operatorname{Ind}(Si).
\label{rel-wf-evaluation}
\end{equation}
Finally, from $i:\mathsf P_X$, $ex:\operatorname{Ext}(i)$ and
$l:\operatorname{Ind}(i)$ there is a builder
\begin{equation}
b(i,ex,l):i@\operatorname{WF}.
\label{rel-induction-builder}
\end{equation}
\end{lemma}
\begin{proof}
Since $\operatorname{le}(i,\operatorname{WF})=[\operatorname{WF}z_i]$,
the data cancellation law gives, for every $i$, a proof
\[
F(i):\operatorname{le}(i,\operatorname{WF})
\leftrightarrow\operatorname{Ind}(i_{z_i}).
\]
This evaluation uses neither $\operatorname{Resp}(z_i)$ nor
$\operatorname{Ext}(i)$.
To prove validity, take arbitrary $i,i':\mathsf P_X$ and
$d:i\approx i'$. We construct
\[
D(d):i_{z_i}\approx i_{z_{i'}}
\]
without introducing extensionality assumptions. At $x:X$ put
$t=(\operatorname{Round}_Xx)^0:L$. The predicate evaluation law
and the earlier rounded evaluation of $z_i$ give the following
chain of biconditionals:
\[
i_{z_i}@x
\ \leftrightarrow\ z_i\diamond_m t
\ \leftrightarrow\ i@\operatorname{lift}_m(\operatorname{Round}t)
\ \leftrightarrow\ i'@\operatorname{lift}_m(\operatorname{Round}t)
\ \leftrightarrow\ z_{i'}\diamond_m t
\ \leftrightarrow\ i_{z_{i'}}@x.
\]
The middle comparison is exactly
$d[\operatorname{lift}_m(\operatorname{Round}t)]$.
The other four comparisons are the two predicate evaluations and
the two rounded evaluations. Applying $\mathsf{pl}$ to those five
proofs at target $i_{z_i}@x\leftrightarrow i_{z_{i'}}@x$, then
abstracting over $x$, constructs $D(d)$. Therefore
\[
V_{\operatorname{WF}}=
\Lambda i,i'.\lambda^*d.\,
\mathsf{pl}_{\,\operatorname{le}(i,\operatorname{WF})
\leftrightarrow
\operatorname{le}(i',\operatorname{WF})}
\bigl(F(i),F(i'),\operatorname{IndC}(D(d))\bigr).
\]
Now assume $ex:\operatorname{Ext}(i)$. The proof $d_s$ from
\eqref{rel-shift-comparison} and Lemma~\ref{rel-ind-congruence} give
\[
\operatorname{IndC}(d_s):
\operatorname{Ind}(i_{z_i})\leftrightarrow\operatorname{Ind}(Si).
\]
The forward and reverse directions of $w_{ex}$ are, respectively,
\begin{align*}
&\lambda^*t.\,
\operatorname{to}(\operatorname{IndC}(d_s),
\operatorname{to}(F(i),t)),\\
&\lambda^*l_S.\,
\operatorname{back}(F(i),
\operatorname{back}(\operatorname{IndC}(d_s),l_S)).
\end{align*}
Their pair proves \eqref{rel-wf-evaluation}.
For the final assertion, fix $l:\operatorname{Ind}(i)$. We first
construct $l_S:\operatorname{Ind}(Si)$. Under $x:X$,
$u:\operatorname{Valid}(x)$ and $t:\operatorname{le}(Si,x)$,
the proof $\operatorname{back}(a_{ex,u},t)$ has type
$\operatorname{le}(i,\delta x)$. Since
$V_\delta(x):\operatorname{Valid}(\delta x)$, it follows that
\[
l[\delta x]\cdot V_\delta(x)\cdot
\operatorname{back}(a_{ex,u},t):i@\delta x.
\]
Applying the reverse direction of $s_{ex}(x)$ gives $Si@x$.
Thus the required builder is
\[
l_S=\Lambda x.\lambda^*u.\lambda^*t.\,
\operatorname{back}\bigl(s_{ex}(x),
l[\delta x]\cdot V_\delta(x)\cdot
\operatorname{back}(a_{ex,u},t)\bigr).
\]
Since $\operatorname{back}(w_{ex},l_S)$ has type
$\operatorname{le}(i,\operatorname{WF})$, define
\[
b(i,ex,l)=
l[\operatorname{WF}]\cdot V_{\operatorname{WF}}\cdot
\operatorname{back}(w_{ex},l_S).
\]
Its type is $i@\operatorname{WF}$, as required.
\end{proof}
\begin{proposition}[The diagonal contradiction]
\label{rel-contradiction}
The specialized relational construction yields a proof of
$\bot=F_b$ in the ambient labelled context.
\end{proposition}
\begin{proof}
Define the data formula and data predicate
\begin{align*}
Q(x)&=\forall i:\mathsf P_X.\bigl(\operatorname{Ext}(i)
\Rightarrow(\operatorname{le}(i,x)\Rightarrow i@\delta x)\bigr),\\
j_*&=\operatorname{pred}_X(x.\,\neg Q(x)):\mathsf P_X.
\end{align*}
Neither definition uses proof variables.
First we construct
\[
\operatorname{QC}(e):Q(x)\leftrightarrow Q(x')
\qquad(e:x\simeq x').
\]
For any $i:\mathsf P_X$ and $ex:\operatorname{Ext}(i)$, put
\[
c_{ex,e}=ex[\delta x][\delta x']\cdot\operatorname{DeltaC}(e)
:i@\delta x\leftrightarrow i@\delta x'.
\]
The forward direction of $\operatorname{QC}(e)$ is
\[
\lambda^*q.\Lambda i.\lambda^*ex.\lambda^*t'.\,
\operatorname{to}\bigl(c_{ex,e},
q[i]\cdot ex\cdot\operatorname{back}(e[i],t')\bigr),
\]
where $q:Q(x)$ and $t':\operatorname{le}(i,x')$.
Its reverse direction is
\[
\lambda^*q'.\Lambda i.\lambda^*ex.\lambda^*t.\,
\operatorname{back}\bigl(c_{ex,e},
q'[i]\cdot ex\cdot\operatorname{to}(e[i],t)\bigr),
\]
where $q':Q(x')$ and $t:\operatorname{le}(i,x)$.
Pairing these terms gives the asserted congruence.
The predicate evaluation law supplies
$j_*@x\leftrightarrow\neg Q(\operatorname{Round}_Xx)$.
Using $\operatorname{QC}(\operatorname{RoundRel}_X(x))$ and
$\mathsf{pl}$ with that evaluation yields
\begin{equation}
n(x):j_*@x\leftrightarrow\neg Q(x).
\label{rel-negative-evaluation}
\end{equation}
The extensionality builder is
\[
ex_*=
\Lambda x,x'.\lambda^*e.\,
\mathsf{pl}_{\,j_*@x\leftrightarrow j_*@x'}
\bigl(n(x),n(x'),\operatorname{QC}(e)\bigr)
:\operatorname{Ext}(j_*).
\]
In both uses of $\mathsf{pl}$ the passage from a biconditional
between the $Q$-formulas to the corresponding negated formulas is
propositional; no predicate is substituted inside data.
We next construct $l_*:\operatorname{Ind}(j_*)$.
Introduce $x:X$, $u:\operatorname{Valid}(x)$ and
$t:\operatorname{le}(j_*,x)$. To obtain $j_*@x$, it suffices,
by the reverse direction of $n(x)$, to obtain $\neg Q(x)$.
Under the further assumption $q:Q(x)$ we have
\[
q[j_*]\cdot ex_*\cdot t:j_*@\delta x,
\]
and hence
\begin{equation}
n_\delta=
\operatorname{to}\bigl(n(\delta x),q[j_*]\cdot ex_*\cdot t\bigr)
:\neg Q(\delta x).
\label{rel-negative-shift}
\end{equation}
To construct the opposite formula $Q(\delta x)$, take arbitrary
$i:\mathsf P_X$, $ex:\operatorname{Ext}(i)$ and
$t':\operatorname{le}(i,\delta x)$. At this point
$a_{ex,u}$ uses the original proof $u:\operatorname{Valid}(x)$.
Its forward direction gives
\[
\operatorname{to}(a_{ex,u},t'):\operatorname{le}(Si,x).
\]
Because $\operatorname{ExtS}(i,ex):\operatorname{Ext}(Si)$,
we may instantiate $q$ at $Si$ to obtain
\[
q[Si]\cdot\operatorname{ExtS}(i,ex)\cdot
\operatorname{to}(a_{ex,u},t'):Si@\delta x.
\]
The forward direction of $s_{ex}(\delta x)$ turns this into
$i@\delta(\delta x)$. Therefore
\begin{equation}
\begin{split}
p_\delta={}&\Lambda i.\lambda^*ex.\lambda^*t'.\,
\operatorname{to}\bigl(s_{ex}(\delta x),\\[-2pt]
&\hspace{35mm}
q[Si]\cdot\operatorname{ExtS}(i,ex)\cdot
\operatorname{to}(a_{ex,u},t')\bigr)
:Q(\delta x).
\end{split}
\label{rel-positive-shift}
\end{equation}
Combining \eqref{rel-negative-shift} and \eqref{rel-positive-shift}
gives $n_\delta\cdot p_\delta:\bot$. With these local terms
inlined in their indicated context, define
\[
l_*=
\Lambda x.\lambda^*u.\lambda^*t.\,
\operatorname{back}\bigl(n(x),
\lambda^*q.\,n_\delta\cdot p_\delta\bigr).
\]
Its body has type $j_*@x$, so
$l_*:\operatorname{Ind}(j_*)$.
Finally construct $q_0:Q(\operatorname{WF})$. Under arbitrary
$i:\mathsf P_X$, $ex:\operatorname{Ext}(i)$ and
$t:\operatorname{le}(i,\operatorname{WF})$, the forward direction
of $w_{ex}$ gives $\operatorname{Ind}(Si)$. Applying the induction
builder to the predicate $Si$ therefore gives
\[
b\bigl(Si,\operatorname{ExtS}(i,ex),
\operatorname{to}(w_{ex},t)\bigr):Si@\operatorname{WF}.
\]
Here the builder $b$ is instantiated at $Si$, while the displayed
$w_{ex}$ and the following $s_{ex}$ are the builders for the
original predicate $i$. Thus
\[
q_0=\Lambda i.\lambda^*ex.\lambda^*t.\,
\operatorname{to}\bigl(s_{ex}(\operatorname{WF}),
b(Si,\operatorname{ExtS}(i,ex),
\operatorname{to}(w_{ex},t))\bigr)
:Q(\operatorname{WF}).
\]
On the other hand,
$b(j_*,ex_*,l_*):j_*@\operatorname{WF}$, and hence
\[
\operatorname{to}\bigl(n(\operatorname{WF}),
b(j_*,ex_*,l_*)\bigr)
:\neg Q(\operatorname{WF}).
\]
The required ambient proof is therefore
\[
\operatorname{to}\bigl(n(\operatorname{WF}),
b(j_*,ex_*,l_*)\bigr)\cdot q_0:\bot.
\]
\end{proof}
\begin{remark}[Dependencies and discharged assumptions]
\label{rel-diagonal-dependencies}
At the fixed specialization, $i_v$ is defined before its
response and extensionality proofs; $\delta$ and $S$ are data
definitions independent of those proofs; $\operatorname{WF}$ uses
the already defined $i_v$ and $\operatorname{Ind}$; and $Q,j_*$ use
only the previously defined data operations. In particular,
$\operatorname{WF}$ is defined even when $v$ is not responsive.
Its validity proof uses rounded evaluations and does not assume
extensionality of the predicates it quantifies over.
The inputs $h,ex,u$ occur only in proof builders. Every use of
\eqref{rel-sb-law} or \eqref{rel-shift-predecessor} supplies the
stated response, extensionality and validity inputs. Every logical
quantifier introduced by the displayed tail builders ranges over
$X$ or $\mathsf P_X$ with its fixed direct-domain annotation.
After inlining the local builders,
the proof of Proposition~\ref{rel-contradiction} has no free proof
or data assumptions beyond the ambient context: $A_0,m_0,ad$ are
the earlier constructed specialization, and every introduced
logical assumption has been abstracted or supplied as an argument.
\end{remark}
==== END Weak-and-strong-normalization-in-pure-type-systems//sections/relational.tex ====
==== BEGIN Weak-and-strong-normalization-in-pure-type-systems//sections/wrappers.tex ====
\section{A typed calculus for the forbidden configuration}
\label{sec:enc-wrappers}
We now prove the exclusion used in constructing the payload spaces. Throughout
this section, $S$ is a primary strongly connected component containing an odd
closed walk and a profile triple $(a_0,b,k_0)$ with all three vertices in $S$.
We construct a small logical calculus inside the given PTS. Its judgments will
be genuine PTS judgments in one finite open context. The later contradiction
will therefore fall under the system-wide weak-normalization hypothesis.
We say that a type is \emph{sorted at a profile} $I$ if it has each sort in $I$.
Its actual profile may be larger than $I$. All constructions below use only
these separate sort judgments, and never uniqueness of sorts or product rules.
Since $S$ is strongly connected and has an odd closed walk, any two of its
vertices are joined inside $S$ by paths of both parities: join the first vertex
to the walk and the walk to the second, and either insert the odd walk or omit
it. A path's parity is the number of its negative edges modulo two.
\subsection{Modes and the ambient context}
\label{subsec:enc-modes}
Partition variable names into two infinite classes, of modes $\mathsf d$
and $\mathsf p$. Sorts have mode $\mathsf d$. Products, abstractions and
applications carry a label
\[
(i,j)\in\{(\mathsf d,\mathsf d),(\mathsf d,\mathsf p),
(\mathsf p,\mathsf p)\}.
\]
In a binder, $i$ is the bound variable's mode. A product
$\Pi^{i,j}x:A.B$ has mode $\mathsf d$ and both $A,B$ have mode
$\mathsf d$. An abstraction $\lambda^{i,j}x:A.M$ has annotation of mode
$\mathsf d$ and body and result of mode $j$. In an application with label
$(i,j)$, the argument has mode $i$ and the function and result have mode $j$.
Consequently, an expression of mode $\mathsf d$ has no free variable of mode
$\mathsf p$. Declaration types and expected types always have mode
$\mathsf d$.
The typing rules are the original PTS rules with the displayed label retained
on the product in abstraction and application rules. A beta step contracts
an abstraction and application with matching labels; reduction is closed under
all syntax positions, including annotations. Conversion is generated by this
labelled reduction. We suppress application labels only when the displayed
function type determines them. The labelled metatheory and its relation to
ordinary reduction are proved in Lemma~\ref{lem:enc-labelled-metatheory}.
In particular, the weakening, substitution, conversion and generation
arguments used below apply in these modes.
\subsection{Reduction after forgetting the modes}
\label{sec:normal-erasure}
Before constructing the witnesses and wrappers, we establish the
labelled metatheory and its relation to the given pure type system. Write $|M|$ for the term obtained by
forgetting every mode label. Erasure keeps all applications, binders, and
annotations. In particular, a redex in an annotation remains a redex after
erasure.
Labelling and erasure also occur in the structural transformations of
Roux and van Doorn \cite[Sections~3--4]{RouxVanDoorn2014}.
Here the exact interface is preservation of typing together with lifting
of every erased beta step. Keeping annotations is part of that interface;
the domain-erasure comparison studied by Barthe and Coquand
\cite[Theorem~17]{BartheCoquand2006} concerns a different operation.
\begin{lemma}[Labelled metatheory and reduction lifting]
\label{lem:enc-labelled-metatheory}
The labelled typing rules have context validity, correctness of types,
weakening, typed substitution by terms of the declared modes, context
conversion, generation, and subject reduction at the exact expected type.
Labelled beta reduction is confluent, and convertible
labelled products have the same pair of labels and convertible corresponding
components. Erasing a labelled typing derivation gives a typing derivation
in the original pure type system.
If $\Gamma\vdash M:A$ is a labelled judgment and
$|M|\longrightarrow_\beta N$, there is a labelled $M'$ with
\[
M\longrightarrow_\beta M',\qquad |M'|=N,
\qquad \Gamma\vdash M':A,
\]
up to alpha conversion. The mode of $M'$ is the mode of $M$.
Consequently, every finite reduction of $|M|$ lifts to a typed labelled
reduction. If $|M|$ is weakly normalizing, some labelled reduct of $M$ has
beta-normal erasure.
\end{lemma}
\begin{proof}
Substitution preserves modes by induction on syntax. A data expression has
no free proof variable, so substitution for a proof variable cannot introduce
proof syntax into a data expression. Substitution for a data variable uses
a data term. At binders, choose fresh names in the same mode class.
Context validity follows by rule induction, retaining the sort typing of
each declaration from its introduction premise.
The proofs of weakening and typed substitution are inductions on typing
derivations. Each binder retains its label, and each substituted term has
the mode required by that binder or declaration. Context conversion follows
by the identity substitution, typing the changed variable at its old type
by conversion. Generation follows by removing final conversions and
weakenings. None of these arguments compares distinct possible sort
assignments.
Correctness of types is another rule induction: an expected type is a literal
sort or is itself
sorted. At application, the function's product type is sorted by induction;
generation on that product and typed substitution sort the application's
result type. This remains true through conversion and weakening.
For confluence, use parallel reduction with homomorphic clauses at every
constructor, including annotation children, and a contracting clause only
when the application and lambda labels match. Parallel substitution is
proved by syntax induction. Every parallel reduct of a term parallel-reduces
to its complete development: contract the matching redexes already present
in the original term and develop all children. At an unmatched
lambda--application pair only the homomorphic clause applies. This proves
the triangle property, hence confluence. The reflexive transitive closures
of parallel and ordinary reduction agree, since parallel contractions can be
performed from the children upwards. Reduction never changes a product's
outer constructor or labels. Common reducts therefore give labelled product
compatibility, and a product cannot be convertible to a sort.
Subject reduction now follows by induction on a typing derivation. At a root
beta step, generation and product compatibility identify the lambda's
annotation with the application's domain up to conversion. Convert the
argument to the annotation type, substitute in the body, and convert the
result to the original expected type. A reduction of an application
argument changes its substituted result type by conversion. A reduction
of a product domain is handled by context conversion in the codomain
premise. For a lambda annotation step, reduce the corresponding domain in
its supporting product judgment, context-convert its body premise,
re-form the lambda, and convert back to the original sorted product type.
The other positions, including positions inside
annotations, follow by induction. These constructions keep every label.
Erasure of typing follows directly by induction on the labelled derivation.
It remains to check that an erased redex can be contracted with the labels
present. Every syntactic subterm of a typable term has a typing in the
appropriate binder context; for an annotation this follows from context
validity. Consider the subterm at the erased redex. Its shape is
\[
(\lambda^{i,j}x:D.P)\mathbin{@^{i',j}}Q.
\]
The result modes already force the displayed common $j$. Lambda generation
gives a product type with labels $(i,j)$; application generation gives a
convertible product type with labels $(i',j)$. Product compatibility forces
$i=i'$. Thus this is a matching labelled redex. Contract it at the same
position. Capture-free substitution commutes with erasure, so its erasure
is $N$; subject reduction gives the asserted judgment and substitution
preserves its mode. This applies to any position, including one in a
lambda or product annotation. Induction on a finite erased reduction proves
the remaining assertions.
\end{proof}
\subsection{Witnesses and terminal transformations}
For each feasible profile $I$ needed in the finite construction, choose a
normal witness $D_I$ sorted at $I$, using only data names and labels
$(\mathsf d,\mathsf d)$. Such witnesses follow from the profile-generation
construction: literals realize nonempty axiom profiles, variables of sorted
literal type realize the singleton generators, and dummy products realize
$\operatorname{Out}(I,J)$. Combine the finitely many witness contexts by
renaming their data variables disjointly and weakening. Extend the result
by a data variable $e_I:D_I$ for each needed witness. Denote this finite
valid data context by $\Delta_{\mathsf d}$.
Here and below every profile triple means
$K=\operatorname{Out}(I,J)$. If $T$ is sorted at $J$, the positive edge
$J\longrightarrow K$ associated with this triple sends $T$ to
\[
\Pi^{\mathsf d,j}z:D_I.T,
\qquad j=\mathsf p\text{ for proof values},\quad
j=\mathsf d\text{ for data values},
\]
where $z$ is fresh and absent from $T$. This type is sorted at every sort
$c\in K$: choose $a\in I,b'\in J$ with $(a,b',c)\in\mathcal R$ and use
those two available sort judgments. The corresponding lift and projection
are
\[
\operatorname{up}(t)=\lambda^{\mathsf d,j}z:D_I.t,
\qquad \operatorname{pr}(w)=w\,e_I.
\]
They have the displayed types and
$\operatorname{pr}(\operatorname{up}(t))=_\beta t$.
A positive inclusion edge $I'\longrightarrow I$ with $I\subseteq I'$
uses the identity type, lift and projection.
A negative edge $I\longrightarrow K$ associated with $(I,J,K)$ sends a
type $T$ sorted at $I$ to
$\Pi^{j,j}z:T.F$, where $F$ is a fixed type sorted at $J$ and $j$ is
$\mathsf p$ or $\mathsf d$ according to the construction. Formation uses
exactly the same argument for each $c\in K$. Thus a path $\rho$ defines
a wrapper $W_\rho(T)$ by successive applications of these operations,
with specified tails at negative edges. Empty paths are permitted, and
\[
W_{\rho\sigma}(T)=W_\sigma(W_\rho(T))
\]
by the definition. We always specify whether the wrapper carries proof
values or data values.
For every internal negative edge of $S$ with triple $(I,J,K)$, fix the
proof tail $F_J=D_J$ before choosing any paths. Call these finitely many types the
\emph{terminals}; include $F_b=D_b$ by the negative edge of
$(a_0,b,k_0)$. Each terminal is normal and has only
$(\mathsf d,\mathsf d)$ labels.
\begin{lemma}[Terminal transformations]
\label{lem:enc-terminal-converters}
There is a finite valid extension $\Delta=\Delta_{\mathsf d},
\Delta_{\mathsf p}$ and, for every pair of terminals $F,F'$, a proof
term $\tau_{F,F'}(p):F'$ in $\Delta,p:F$. Every declaration of
$\Delta_{\mathsf p}$ has the form
\[
c:\Pi^{\mathsf p,\mathsf p}u:T.F_J,
\]
where $T$ is a normal, constant telescope of
$(\mathsf d,\mathsf p)$ products ending at a terminal. Its suffixes
are sorted, and its type contains no free proof variables.
\end{lemma}
\begin{proof}
Associate each terminal with a negative edge producing it. Lift the input
terminal along the positive edge of its associated triple, reaching $S$.
Choose a path in $S$ to the domain vertex of an edge producing the target
terminal, and append that negative edge. Carry a proof along this route.
At a positive edge use the lift above. At a negative edge $(I,J,K)$,
if the currently carried type is $T$, introduce a fresh proof variable
$c:\Pi^{\mathsf p,\mathsf p}u:T.F_J$ and replace the carried proof $t$
by $c\,t:F_J$. Unless this is the last edge, lift $c\,t$ along the
positive edge $J\longrightarrow K$ of this same triple before continuing.
The product type of $c$ is sorted at $K$, so the declaration is valid.
Initially the carried type is a terminal. Positive edges add constant
$(\mathsf d,\mathsf p)$ prefixes, and negative edges reset the carried
type to a terminal before the prescribed lift. Thus every converter domain
has precisely the asserted form. Its normality and the sorting of each
suffix follow from its construction. The types depend on chosen types and
paths, not on the input proof. Choose the finitely many pairwise routes
first and predeclare all their converters in $\Delta_{\mathsf p}$;
weakening makes every resulting transformation available in the same
context. Types use data only, so the converter declarations do not depend
on one another.
\end{proof}
\subsection{Proof transport and derived logic}
\label{subsec:enc-proof-transport}
Let $\rho$ be a proof path inside $S$ from a profile at which $T$ is sorted, and put
$W=W_\rho(T)$. The following operations are defined in every valid
extension of $\Delta$. All displayed inputs after a semicolon describe
an open term under the indicated fresh variable.
For an even path they have types
\[
\operatorname{in}_\rho(p:T):W,
\qquad \operatorname{out}_\rho(w:W;e.k):F
\quad(e:T\vdash k:F),
\]
and for an odd path they have types
\[
\operatorname{in}_\rho(e.k):W
\quad(e:T\vdash k:F),
\qquad \operatorname{out}_\rho(w:W,p:T):F,
\]
where $F$ is any terminal. Path and terminal subscripts will often be
omitted, but remain part of each chosen operation.
For the empty path, $\operatorname{in}(p)=p$ and
$\operatorname{out}(w;e.k)=k[e:=w]$.
Appending a positive edge lifts the previous $\operatorname{in}$ and
projects the input to the previous $\operatorname{out}$.
For a negative edge with tail $F'$ appended to an even path $\rho$, set
\begin{align*}
\operatorname{in}_{\rho-}(e.k)
&=\lambda^{\mathsf p,\mathsf p}u:W_\rho(T).
\operatorname{out}_\rho(u;e.\tau_{F,F'}(k)),\\
\operatorname{out}_{\rho-}(w,p)
&=\tau_{F',F}(w\,\operatorname{in}_\rho(p)).
\end{align*}
For a negative edge appended to an odd path $\rho$, set
\begin{align*}
\operatorname{in}_{\rho-}(p)
&=\lambda^{\mathsf p,\mathsf p}u:W_\rho(T).
\operatorname{out}_\rho(u,p),
&&\text{with output terminal }F',\\
\operatorname{out}_{\rho-}(w;e.k)
&=\tau_{F',F}(w\,\operatorname{in}_\rho(e.k)).
\end{align*}
These are recursion equations on path length. Each abstraction uses the
already formed negative-edge product. Each application uses its domain
exactly, and the terminal transformations have the displayed input and
output types. This proves the typings by induction; callbacks are thinned
by insertion before introducing each fresh variable.
Call a type \emph{stable} if it is a syntactic telescope of proof-result
products, with labels $(\mathsf d,\mathsf p)$ or
$(\mathsf p,\mathsf p)$, ending at a terminal. A telescope of length
zero is allowed. Let $Q$ be a sorted stable type independent of a proof
variable $e:T$. The even-path operation $\operatorname{out}(w;e.k)$
extends from terminal-valued callbacks to $k:Q$: introduce the successive
raw arguments $\vec x$ of $Q$, thin $w$ and the callback into that
context, apply terminal-valued $\operatorname{out}$ to
$e.k\,\vec x$, and abstract the same arguments $\vec x$.
Generation on the sorted telescope provides the domain sortings and the
supporting product judgments for all these abstractions. In particular,
if $T$ is stable, the identity callback gives
\[
\operatorname{down}_\rho(w):T
\qquad (\rho\text{ even}).
\]
A proof wrapper preserves stability of its input. A proof path containing
a negative edge produces a stable type even if its input was not stable,
because the first such edge ends at a terminal.
A \emph{formula} will mean a stable data type sorted at every sort of
$b$. A formula is therefore a data-mode expression used as a type; a proof
of that formula means a proof-mode inhabitant. The mode of an inhabitant
is not determined by its expected type. The next operations give a typed classical logical calculus of
formulas. These operations are defined terms, not additional PTS rules.
Fix even proof paths $\alpha:b\to a_0$, $\beta:b\to b$, and
$\gamma:k_0\to b$. Define
\[
P\Rightarrow Q=
W_\gamma\bigl(\Pi^{\mathsf p,\mathsf p}p:W_\alpha(P).
W_\beta(Q)\bigr).
\]
The product rule is supplied by $(a_0,b,k_0)$, and all wrappers are
already typed. Given $q:Q$ in a context extended by $p:P$, define
\begin{align*}
\lambda^*p.q
&=\operatorname{in}_\gamma\bigl(
\lambda^{\mathsf p,\mathsf p}p':W_\alpha(P).
\operatorname{in}_\beta(q[p:=\operatorname{down}_\alpha(p')])
\bigr),\\
f\cdot p
&=\operatorname{down}_\beta\bigl(
\operatorname{down}_\gamma(f)\,
\operatorname{in}_\alpha(p)\bigr).
\end{align*}
They have types $P\Rightarrow Q$ and $Q$, respectively. Data formulas
cannot contain $p$, so the product codomain is independent of this proof
variable.
For a data type $T$ sorted at a direct vertex $I$, fix once and for all
a triple $(I,J,K)$ with $J,K\in S$, and even proof paths
$\alpha_I:b\to J$ and $\gamma_I:K\to b$. For a formula $Q$ in
context $x:T$, put
\[
\forall x:T.Q=
W_{\gamma_I}\bigl(\Pi^{\mathsf d,\mathsf p}x:T.
W_{\alpha_I}(Q)\bigr).
\]
The associated introduction and elimination are
\[
\Lambda x.q=\operatorname{in}_{\gamma_I}
(\lambda^{\mathsf d,\mathsf p}x:T.
\operatorname{in}_{\alpha_I}(q)),
\qquad
f[t]=\operatorname{down}_{\alpha_I}
(\operatorname{down}_{\gamma_I}(f)\,t).
\]
They are typed using precisely the chosen triple. The direct vertex and
paths are part of the domain annotation and remain fixed under
substitution; paths are never reselected from a newly enlarged profile.
These constructions show that implication and universal quantification
again yield formulas.
Set $\bot=F_b$, $\neg P=P\Rightarrow\bot$, and
$\top=\bot\Rightarrow\bot$. There are derived operations
\[
\operatorname{abs}_P:\bot\longrightarrow P,
\qquad \operatorname{dn}_P:\neg\neg P\longrightarrow P,
\]
where the arrows describe input and output judgments, not an assertion that
these are primitive function types. To construct either operation, expose
the raw telescope arguments $\vec x$ of $P$, ending at a terminal $F$.
For $f:\bot$, abstract the terminal body $\tau_{\bot,F}(f)$.
For $w:\neg\neg P$, abstract the terminal body
\[
\tau_{\bot,F}\left(
w\cdot(\lambda^*p.\tau_{F,\bot}(p\,\vec x))\right).
\]
The applications $p\,\vec x$ use the original labels and annotations
of $P$. Sorting and abstraction support follow from generation on $P$,
as in the definition of $\operatorname{down}$.
For completeness, the other logical operations used below are the
following explicit abbreviations and term constructors:
\begin{align*}
P\land Q&=\neg(P\Rightarrow\neg Q),&
(p,q)_\land&=\lambda^*h.(h\cdot p)\cdot q,\\
\operatorname{fst}(w)
&=\operatorname{dn}_P
(\lambda^*n.w\cdot(\lambda^*p.\lambda^*q.n\cdot p)),&
\operatorname{snd}(w)
&=\operatorname{dn}_Q
(\lambda^*n.w\cdot(\lambda^*p.\lambda^*q.n\cdot q)),\\
P\leftrightarrow Q&=(P\Rightarrow Q)\land(Q\Rightarrow P),&
\operatorname{to}(e,p)&=\operatorname{fst}(e)\cdot p,\\
&&\operatorname{back}(e,q)&=\operatorname{snd}(e)\cdot q,\\
P\lor Q&=\neg(\neg P\land\neg Q),&
\operatorname{inl}(p)&=\lambda^*h.\operatorname{fst}(h)\cdot p,\\
&&\operatorname{inr}(q)&=\lambda^*h.\operatorname{snd}(h)\cdot q.
\end{align*}
Given $w:P\lor Q$ and branches $p:P\vdash u:R$ and
$q:Q\vdash v:R$, their case term is
\[
\operatorname{dn}_R\left(
\lambda^*n.w\cdot
(\lambda^*p.n\cdot u,\lambda^*q.n\cdot v)_\land\right).
\]
Excluded middle has the term
\[
\operatorname{em}(P)=
\lambda^*h.\operatorname{snd}(h)\cdot\operatorname{fst}(h)
:P\lor\neg P.
\]
For the same permitted quantified domains as above, put
\[
\exists x:T.Q=\neg\forall x:T.\neg Q.
\]
If $t:T$ and $p:Q[x:=t]$, a witness term is
$\operatorname{wit}(t,p)=\lambda^*h.h[t]\cdot p$.
If $w:\exists x:T.Q$ and $u:R$ under $x:T,p:Q$, where $R$ is
independent of $x,p$, existential elimination is
\[
\operatorname{open}_R(w;x,p.u)=
\operatorname{dn}_R\bigl(
\lambda^*n.w\cdot(\Lambda x.\lambda^*p.n\cdot u)\bigr).
\]
Each display can be checked from the introduction and elimination
judgments already proved. All new assumptions are introduced with their
formula or data type as annotation, and terms are weakened when necessary.
\begin{lemma}[Finite propositional derivations]
\label{lem:enc-propositional}
If formulas $P_1,\ldots,P_m$ propositionally entail a formula $R$, there
is a specified finite term
$\mathsf{pl}_R(p_1,\ldots,p_m):R$ under $p_i:P_i$.
Here $\bot$ has truth value false; specified Boolean connectives are
parsed, and other subformulas, including quantifiers, may be treated as
atoms.
\end{lemma}
\begin{proof}
List the finitely many atoms and nest cases on their terms
$\operatorname{em}$. Each resulting branch supplies either the atom or
its negation. Recursively build a proof of every true parsed formula and
a proof of the negation of every false parsed formula. For $\bot$ the
required negation is the identity term. For conjunction, a true case
uses pairing, and a false case contradicts the false conjunct's projection.
For disjunction, a true case uses its true injection, and a false case
uses case analysis to contradict either disjunct. For implication, a true
case either returns a proof of the consequent or derives it by
$\operatorname{abs}$ from the false antecedent; a false case contradicts
the application of an assumed implication to the already proved antecedent.
Negation is implication to $\bot$, and biconditional is its displayed
conjunction. If some premise is false, apply its constructed negation to
the given proof and use $\operatorname{abs}_R$. Otherwise the assumed
truth-table entailment makes $R$ true, so use its constructed proof.
The recursively typed case terms discharge all branch assumptions.
\end{proof}
We also use three explicit congruence constructors. For a proof
$e:P\leftrightarrow Q$ under data $x:T$, define
\[
\mathsf{All}_x(e)=
\bigl(\lambda^*h.\Lambda x.\operatorname{to}(e,h[x]),
\lambda^*h.\Lambda x.\operatorname{back}(e,h[x])\bigr)_\land.
\]
It compares $\forall x:T.P$ and $\forall x:T.Q$ with exactly the same
annotated domain. Define $\mathsf{Ex}_x(e)$ by pairing the two functions
which open an existential input, retain its data witness, and use
$\operatorname{to}$ or $\operatorname{back}$ on its proof witness.
For a proof $e:P\leftrightarrow Q$ under $v:D$, where $D$ is a formula,
put
\[
\mathsf{Gd}_{v:D}(e)=
\bigl(\lambda^*h.\lambda^*v.\operatorname{to}(e,h\cdot v),
\lambda^*h.\lambda^*v.\operatorname{back}(e,h\cdot v)\bigr)_\land.
\]
This compares $D\Rightarrow P$ and $D\Rightarrow Q$.
Multiple indices mean iteration of the corresponding constructor.
These conventions make later derivations finite algorithms for labelled
terms. A stated propositional consequence invokes
Lemma~\ref{lem:enc-propositional}; proving the two directions of an
equivalence means abstracting the two assumptions and pairing; opening an
existential means the displayed $\operatorname{open}$ term at the stated
target. A schematic data parameter is an open parameter, not an implicit
universal quantifier. Only displayed $\Lambda$ operations quantify over
data. Logical equivalences are used to construct proofs and never to
replace a data subterm. All fixed paths, roles and syntax choices are
preserved under substitution.
\subsection{Data wrappers and exact cancellation}
\label{subsec:enc-data-transport}
For a sort $u$ with $\{u\}\in S$ and
$\operatorname{Ax}(u)\ne\varnothing$, fix an even proof path from $b$
to $\{u\}$. For a formula $P$, its wrapper type along this path is a
data expression of type $u$; denote it by $\operatorname{encode}_u(P)$.
Fix also an even proof path from $\{u\}$ to $b$ containing a negative
edge. Such a path is obtained from any even one by inserting an odd
closed detour twice. Wrapping a data expression $t:u$ along this second
path defines a stable formula $\operatorname{decode}_u(t)$.
The two proof-path inclusions and the two stable retractions give a proof
\begin{equation}
\operatorname{decode}_u(\operatorname{encode}_u(P))
\leftrightarrow P.
\label{eq:enc-code-decode}
\end{equation}
Explicitly, the forward implication applies the two $\operatorname{down}$
operations and the reverse implication applies the two
$\operatorname{in}$ operations. No equality of the two formulas is asserted.
Recall that $H$ is the positive-path closure of the nonempty
$\operatorname{Ax}(u)$ with $\{u\}\in S$. For each tail vertex $J$
of a retained negative secondary edge, choose such a $u$ and an all-positive
primary path $\eta:\operatorname{Ax}(u)\to J$. Define the data type
\[
U_J=W_\eta(u),
\]
using data labels. It is sorted at $J$. Define
$\operatorname{send}_J(P):U_J$ by positively lifting
$\operatorname{encode}_u(P):u$, and define
$\operatorname{read}_J(t)$ by positively projecting $t:U_J$ to type
$u$ and applying $\operatorname{decode}_u$. Positive
projection--lift beta conversion and \eqref{eq:enc-code-decode} give a
specified proof
\begin{equation}
\operatorname{read}_J(\operatorname{send}_J(P))
\leftrightarrow P.
\label{eq:enc-read-send}
\end{equation}
These choices are fixed once for each retained edge.
Now use data wrappers on secondary paths, and on all-positive primary
paths when indicated. At a retained negative edge $(I,J,K)$, the tail is
$U_J$ and the label is $(\mathsf d,\mathsf d)$. For an even data path
$\rho$ from the sorting profile of $T$, define
\[
\operatorname{pack}_\rho(t:T):W_\rho(T),\qquad
\operatorname{use}_\rho(w:W_\rho(T);x.\Phi)\quad\text{a formula},
\]
where $\Phi$ is a formula under data $x:T$. For an odd data path define
\[
\operatorname{mk}_\rho(x.\Phi):W_\rho(T),\qquad
\langle w:W_\rho(T),t:T\rangle_\rho\quad\text{a formula}.
\]
At the empty path use $\operatorname{pack}(t)=t$ and
$\operatorname{use}(w;x.\Phi)=\Phi[x:=w]$.
A positive extension uses the same lift and projection operations as
before. If a negative edge with tail $U_J$ is appended to an even path,
put
\begin{align*}
\operatorname{mk}_{\rho-}(x.\Phi)
&=\lambda^{\mathsf d,\mathsf d}v:W_\rho(T).
\operatorname{send}_J(\operatorname{use}_\rho(v;x.\Phi)),\\
\langle w,t\rangle_{\rho-}
&=\operatorname{read}_J(w\,\operatorname{pack}_\rho(t)).
\end{align*}
If it is appended to an odd path, put
\begin{align*}
\operatorname{pack}_{\rho-}(t)
&=\lambda^{\mathsf d,\mathsf d}v:W_\rho(T).
\operatorname{send}_J(\langle v,t\rangle_\rho),\\
\operatorname{use}_{\rho-}(w;x.\Phi)
&=\operatorname{read}_J(w\,\operatorname{mk}_\rho(x.\Phi)).
\end{align*}
All expressions in these definitions have mode $\mathsf d$.
Path induction proves their typings: the body of each new lambda has type
$U_J$, the negative-edge product is sorted by $(I,J,K)$, and each
application supplies an argument at exactly its displayed domain. The
formula returned by a read is stable by the negative-containing decode
path. Fresh variables and weakening keep callbacks in scope.
\begin{lemma}[Exact data cancellation]
\label{lem:enc-data-cancellation}
For an even data path there is a proof of
\[
\operatorname{use}_\rho(\operatorname{pack}_\rho(t);x.\Phi)
\leftrightarrow\Phi[x:=t],
\]
and for an odd data path there is a proof of
\[
\langle\operatorname{mk}_\rho(x.\Phi),t\rangle_\rho
\leftrightarrow\Phi[x:=t].
\]
These are uniform term constructors in all the displayed open data
parameters. The right-hand sides contain the original input $t$.
\end{lemma}
\begin{proof}
Induct on the path. The empty-path equivalence is propositional
reflexivity. A positive extension beta-reduces its projection of a lift,
so conversion reduces its assertion to the preceding one. For a negative
extension, the displayed lambda beta-reduces the left side to
$\operatorname{read}_J(\operatorname{send}_J(\Psi))$, where $\Psi$
is the left side of the previous cancellation assertion. Apply
\eqref{eq:enc-read-send}, the induction hypothesis, and
$\mathsf{pl}$ for transitivity of equivalence. The expansions commute
with capture-free substitution because all paths, tails and names are
fixed hygienically. Consequently the final callback is exactly
$\Phi[x:=t]$ up to labelled conversion, with no extensional substitution
inside data.
\end{proof}
The preceding constructions use finitely many sorts, profiles, witnesses,
paths and converters. Each term in the remainder is built from finitely
many of their instances. Thus all the resulting judgments have the one
finite ambient context $\Delta$, with any explicitly stated local
parameters. The next construction uses these operations to encode the
forbidden profile configuration.
==== END Weak-and-strong-normalization-in-pure-type-systems//sections/wrappers.tex ====
==== BEGIN Weak-and-strong-normalization-in-pure-type-systems//references.bib ====
@phdthesis{Geuvers1993,
author = {Geuvers, Jan Herman},
title = {Logics and Type Systems},
school = {Katholieke Universiteit Nijmegen},
year = {1993},
url = {https://www.cs.ru.nl/~herman/PUBS/Proefschrift.pdf}
}
@article{BartheHatcliffSorensen2001,
author = {Barthe, Gilles and Hatcliff, John and S{\o}rensen, Morten Heine},
title = {Weak normalization implies strong normalization in a class of non-dependent pure type systems},
journal = {Theoretical Computer Science},
volume = {269},
number = {1--2},
pages = {317--361},
year = {2001},
doi = {10.1016/S0304-3975(01)00012-3}
}
@phdthesis{Sorensen1997,
author = {S{\o}rensen, M. H. B.},
title = {Normalization in {$\lambda$}-Calculus and Type Theory},
school = {University of Copenhagen},
year = {1997},
note = {Consulted revised edition, April 1998, DIKU Report 97/27},
url = {https://di.ku.dk/forskning/Publikationer/tekniske_rapporter/tekniske-rapporter-1997/97-27.pdf}
}
@inproceedings{RouxVanDoorn2014,
author = {Roux, Cody and van Doorn, Floris},
title = {The Structural Theory of Pure Type Systems},
editor = {Dowek, Gilles},
booktitle = {Rewriting and Typed Lambda Calculi},
series = {Lecture Notes in Computer Science},
volume = {8560},
pages = {364--378},
publisher = {Springer},
year = {2014},
doi = {10.1007/978-3-319-08918-8_25},
url = {https://florisvandoorn.com/papers/struct_pts.pdf}
}
@inproceedings{Mull2023,
author = {Mull, Nathan},
title = {An Irrelevancy-Eliminating Translation of Pure Type Systems},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
series = {Leibniz International Proceedings in Informatics},
volume = {269},
pages = {7:1--7:21},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
year = {2023},
doi = {10.4230/LIPIcs.TYPES.2022.7}
}
@phdthesis{MullThesis2023,
author = {Mull, Nathan},
title = {Weak and Strong Normalization of Tiered Pure Type Systems via Type-Preserving Translation},
school = {University of Chicago},
year = {2023},
note = {Consulted draft with title-page date June 16, 2023},
url = {https://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20230502/929cafeb/attachment-0001.pdf}
}
@book{Girard1989,
author = {Girard, Jean-Yves},
title = {Proofs and Types},
note = {Translated and with appendices by Paul Taylor and Yves Lafont},
publisher = {Cambridge University Press},
year = {1989},
isbn = {0-521-37181-3},
url = {https://www.paultaylor.eu/stable/prot.pdf}
}
@article{Tarski1955,
author = {Tarski, Alfred},
title = {A lattice-theoretical fixpoint theorem and its applications},
journal = {Pacific Journal of Mathematics},
volume = {5},
number = {2},
pages = {285--309},
year = {1955},
doi = {10.2140/pjm.1955.5.285}
}
@inproceedings{Hurkens1995,
author = {Hurkens, Antonius J. C.},
title = {A simplification of {Girard}'s paradox},
editor = {Dezani-Ciancaglini, Mariangiola and Plotkin, Gordon},
booktitle = {Typed Lambda Calculi and Applications},
series = {Lecture Notes in Computer Science},
volume = {902},
pages = {266--278},
publisher = {Springer},
year = {1995},
doi = {10.1007/BFb0014058}
}
@misc{Geuvers2007,
author = {Geuvers, Herman},
title = {Inconsistency of classical logic in type theory},
year = {2007},
month = nov,
note = {Public note},
url = {https://www.cs.ru.nl/~herman/PUBS/newnote.pdf}
}
@article{BartheCoquand2006,
author = {Barthe, Gilles and Coquand, Thierry},
title = {Remarks on the equational theory of non-normalizing pure type systems},
journal = {Journal of Functional Programming},
volume = {16},
number = {2},
pages = {137--155},
year = {2006},
doi = {10.1017/S0956796803004726}
}
@misc{Roux2025,
author = {Roux, Cody},
title = {Internal Proofs of Strong Normalization},
howpublished = {TYPES 2025, extended abstract and presentation},
year = {2025},
month = jun,
url = {https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper54.pdf},
note = {Slides: \url{https://msp.cis.strath.ac.uk/types2025/slides/TYPES2025-slides54.pdf}}
}
@phdthesis{Poll1994,
author = {Poll, Erik},
title = {A Programming Logic Based on Type Theory},
school = {Technische Universiteit Eindhoven},
year = {1994},
doi = {10.6100/IR423044},
url = {https://pure.tue.nl/ws/files/1718573/423044.pdf}
}
==== END Weak-and-strong-normalization-in-pure-type-systems//references.bib ====