Select Git revision
report-2-logrels.tex
report-2-logrels.tex 3.21 KiB
% !TeX root = report.tex
% !TeX encoding = UTF-8
\section{Logical Relations}\label{sec:logrels}
Logical relations are an informal class of proof methods
commonly used to prove meta theorems of type theories.
By informal we mean that the concrete incarnation of the concept ``logical relation'' may differ from type theory to type theory and also from proof to proof.
Below is a non-exhaustive compilation of meta-theoretic properties that are usually shown via proofs by logical relation~\cite{ahmed_log_rel}.
\begin{itemize}
\item Strong normalization: There is no infinite path $t_1 \step t_2 \step \ldots$ where $\step$ is some reduction relation on terms.
\item Type safety: If a term $t$ has type $T$ and $t \step t'$, then $t'$ also has type $T$.
\item Program equivalences
\begin{itemize}
\item Correctness of programs and compiler optimizations
\item Parametricity and free theorems~\cite{wadler:theorems-for-free}:
in type theories admitting such ``free theorems,''
we can generate theorems that terms have to obey by just looking at their type.
For example, in System $F$ all terms $t$ of type $\forall \alpha.\ \alpha \to \alpha$ obey: for all terms $f\colon A \to A'$, we have $f \circ t_A = t_{A'} \circ f$, where $\circ$ is function composition.
With a small bit of more work, we can show that all such $t$ are equal to $\ulam{x} x$ for some reasonable notion of equality~\cite{pfenning:lecture-parametricity}.
\item Representation independence~\cite{mitchell:abstraction}:
overlapping with the previous point,
programs should not depend on specific implementations (or terms) of
abstract datatypes (or types).
Instead, programs with either implementation should be observationally equivalent.
\item Information flow control~\cite{rg:ifc-labeling}:
type theories have been proposed that allow to label the type of variables (e.g. with \emph{public} and \emph{secret})
with the idea to restrict certain information flow.
For example, to lessen certain \emph{side channel attacks} (of cryptographic programs), we might forbid outputs labeled as public to ``noticeably'' depend on inputs labeled as secret.
\end{itemize}
\end{itemize}
Note that the concept of logical relations is not limited to type theory.
We refer to~\cite{hur:logrels-program}
for a modern take on logical relations
as applied on broad fields of mathematics and computer science.
In \Cref{sec:logrels:sn},
following the exposition of~\cite{ziliani_stlc_sn}%
\footnote{Further explanations have been incorporated from~\cite{ahmed_log_rel}, for which typeset notes can be found at~\cite{skorstengaard_log_rel}.},
we consider strong normalization of the simply-typed lambda calculus (STLC)
as one concrete example
to motivate the necessity of logical relations
and to also flesh out some light technical details lest logical relations remain an abstract concept for the reader.
Readers not interested in such a detailed exposition
may safely skip to~\Cref{sec:logrels:summary},
where we summarize logical relations to an extent necessary to understand later sections.
\input{report-2-logrels-1-sn}
\input{report-2-logrels-2-summary}