path: root/note.tex

% Created 2023-02-02 Thu 17:47
% Intended LaTeX compiler: lualatex
\documentclass[11pt,a4paper]{article}
\usepackage{longtable}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{ebproof}
\usepackage{hyperref}
\usepackage[capitalise,noabbrev]{cleveref}
\usepackage{mathtools}
\usepackage{stmaryrd}
\usepackage{unicode-math}
\usepackage{parskip}
\usepackage{newunicodechar}
%% \usepackage[moderate]{savetrees}
\author{Greg Brown}
\date{\today}
\title{Frex\textsuperscript{2}: Normalisation by Evaluation for Second-Order Algebras}
\hypersetup{
 pdfauthor={Greg Brown},
 pdftitle={Frex\textsuperscript{2}: Normalisation by Evaluation for Second-Order Algebras},
 pdfkeywords={},
 pdfsubject={},
 pdfcreator={},
 pdfborder={0 0 0},
 pdflang={English}}

\newfontfamily{\fallbackfont}{STIX Two Math}[Scale=MatchLowercase]
\DeclareTextFontCommand\textfallback{\fallbackfont}

\setmathfont{STIX Two Math}

\newunicodechar{β}{\textfallback{β}}
\newunicodechar{ζ}{\textfallback{ζ}}
\newunicodechar{η}{\textfallback{η}}
\newunicodechar{λ}{\textfallback{λ}}
\newunicodechar{↝}{\textfallback{↝}}
\newunicodechar{↦}{\textfallback{↦}}
\newunicodechar{⟨}{\textfallback{⟨}}
\newunicodechar{⟩}{\textfallback{⟩}}

\newcommand*\tarr[2]{\ensuremath{{#1} \rightarrowtail {#2}}}
\newcommand*\ctxext[2]{{#1} + {#2}}
\newcommand*\ctxcons[2]{{#1}, {#2}}
\newcommand*\copair[2]{{#1} + {#2}}
\newcommand*\InFamily[4]{\ensuremath{{#2} \vdash^{#1} {#3} : {#4}}}

\newcommand*\Litt[1]{\texttt{#1}}
\newcommand*\Var[1]{\Litt{x}_{#1}}
\newcommand*\Lapp[2]{\texttt{\ensuremath{#1} \$ \ensuremath{#2}}}
\newcommand*\Labs[2]{\texttt{λ{#1}. \ensuremath{#2}}}
\newcommand*\Lsub[2]{\texttt{\ensuremath{#1}[\ensuremath{#2}]}}

\newcommand*\mvar[2]{\texttt{\ensuremath{#1}⟨\ensuremath{#2}⟩}}
\newcommand*\msub[2]{\texttt{\ensuremath{#1}\{\ensuremath{#2}\}}}

\newcommand*\term[1]{\ensuremath{\mathbb{T}{[{#1}]}}}

\newcommand*\sta[1]{\mathop{\overline{#1}}}
\newcommand*\dyn[1]{\mathop{\underline{#1}}}

\begin{document}

\maketitle

\section{Second-Order Algebra}

Universal second-order algebra is a technique to describe syntax and theories
for algebras with operations that can bind variables. One notable example of a
second-order algebra is the simply-typed lambda calculus (STLC). Second-order
algebras depend on a set \(T\) of types. For instance, the grammar \(T \coloneqq
{N \mid \tarr{T}{T}}\) gives the types for the STLC, where \(N\) describes some
neutral base type (e.g.\ natural numbers).

A \emph{signature} is a pair of a set \(O\) and function \({\vert\cdot\vert} \in {O \to
{{(T^* \times T)}^* \times T}}\). The set \(O\) is the set of operators in the signature.
The function gives the arity and return type of each operator. Each operator can
take a number of arguments, hence the arity is a list of descriptors. Because
arguments can bind variables, each descriptor has a list of bound variable
types, as well as the argument type. Let the notation \((\gamma_i)\sigma_i \vdash o : \tau\)
denote \({\vert o \vert} = {{(\gamma_i , \sigma_i)}_i , \tau}\).

The signature for the STLC has the two operators \(\mathtt{app}_{\alpha,\beta}\) and
\(\mathtt{abs}_{\alpha,\beta}\) for each pair of types \(\alpha\) and \(\beta\). Their arities are
\({\ctxcons{\tarr{\alpha}{\beta}}{\alpha}} \vdash \mathtt{app}_{\alpha,\beta} : \beta\) and \({(\alpha)\beta} \vdash
\mathtt{abs}_{\alpha,\beta} : \tarr{\alpha}{\beta}\).  Application (\(\mathtt{app}\)) takes two
arguments---a function and value---and returns a result. Neither argument to
application binds variables.  Abstraction (\(\mathtt{abs}\)) takes a single
argument, whose type is the output type of the function. This argument has
access to a freshly-bound variable of the input type.

The unpairing operation in STLC with products is also a second-order operation.
The operation \verb|let (x, y) = e in e'| is represented by an operator
\(\mathtt{unpair}_{\alpha,\beta,\tau}\), with \({\ctxcons{\alpha \times \beta}{(\ctxcons{\alpha}{\beta})\tau}} \vdash
\mathtt{unpair}_{\alpha,\beta,\tau} : \tau\). The argument \verb|e| is a pair and has no
additional variables in scope. The second argument \verb|e'| has access to two
new variables, corresponding to the two components of the pair \verb|x| and
\verb|y|\footnotemark.

\footnotetext{Think of a good non-example.}

Define a \emph{sorted family} to be a type-and-context-indexed set. For example,
the family of variables \(\mathcal{I}\,\tau\,\Gamma\) is the set of positions of type \(\tau\) in the
context \(\Gamma\). Write \InFamily{\mathfrak{X}}{\Gamma}{\Litt{t}}{\tau} for \(\Litt{t} \in
{\mathcal{X}\,\tau\,\Gamma}\), for any sorted family \(\mathcal{X}\).

Given a signature \(\Sigma = (O , {\vert\cdot\vert})\), an \emph{algebra} has four constituent
parts:

\begin{itemize}
\item a carrier sorted family \(\mathcal{A}\)
\item an operation \({\llbracket\cdot\rrbracket}_o \in
  {{(\mathcal{A}\,\sigma_i\,(\ctxext{\gamma_i}{\Gamma}))}_i \to {\mathcal{A}\,\tau\,\Gamma}}\) for each operator
  \({(\gamma_i)\sigma_i} \vdash o : \tau\)
\item a mapping \(\mathtt{var} \in {{\mathcal{I}\,\tau\,\Gamma} \to {\mathcal{A}\,\tau\,\Gamma}}\)
\item a mapping \(\mathtt{sub} \in {{\mathcal{A}\,\tau\,\Gamma} \to (\forall \sigma. {{\mathcal{I}\,\sigma\,\Gamma} \to {\mathcal{A}\,\sigma\,\Delta}}) \to
  {\mathcal{A}\,\tau\,\Delta}}\)
\end{itemize}

subject to the following conditions:

\begin{description}
\item[left unit:] \({\mathtt{sub}(\mathtt{var}_i, \sigma)} = \sigma_i\)
\item[right unit:] \({\mathtt{sub}(\Litt{t}, \mathtt{var})} = \Litt{t}\)
\item[associativity:]
  \({\mathtt{sub}(\mathtt{sub}(\Litt{t}, \sigma), \varsigma)} =
    {\mathtt{sub}(\Litt{t}, {i \mapsto {\mathtt{sub}(\sigma_i, \varsigma)}})}\)
\item[naturality:]
  \({\mathtt{sub}({\llbracket \Litt{ts} \rrbracket}_o, \sigma)} =
    {\llbracket{(\mathtt{sub}(\Litt{ts}_i, {\Uparrow\sigma}))}_i\rrbracket}_o\)
\end{description}

where \(\Uparrow\sigma\) uses \(\mathtt{var}\) and \(\mathtt{sub}\) to lift a substitution
\(\sigma\) from \({\mathcal{I}\,\tau\,\Gamma}\to{\mathcal{A}\,\tau\,\Delta}\) to
\({\mathcal{I},\tau\,(\ctxext{\Theta}{\Gamma})}\to{\mathcal{A},\tau\,(\ctxext{\Theta}{\Delta})}\). The dual extension, \({\sigma\Uparrow} \in
  {{\mathcal{I},\tau\,(\ctxext{\Gamma}{\Theta})}\to{\mathcal{A},\tau\,(\ctxext{\Gamma}{\Theta})}}\) will be used later.

The associativity, left and right unit conditions assert that \(\mathcal{A}\) is a
\emph{substitution monoid}. This means that substitution interacts with itself
and variables in an intuitive way. The naturality condition asserts that
substitution passes through operators and is capture-avoiding. Substitution
lifting maps freshly-bound variables to themselves.

For the STLC, an algebra \(\mathcal{A}\) has a carrier \(\mathcal{A}\); a pair of operations
\({\llbracket\cdot\rrbracket}_\mathtt{app} \in {{\mathcal{A}\,(\tarr{\alpha}{\beta})\,\Gamma} \to {\mathcal{A}\,\alpha\,\Gamma} \to
{\mathcal{A}\,\beta\,\Gamma}}\), and \({\llbracket\cdot\rrbracket}_\mathtt{abs} \in
{{\mathcal{A}\,\beta\,(\ctxcons{\alpha}{\Gamma})} \to {\mathcal{A}\,(\tarr{\alpha}{\beta})\,\Gamma}}\); and the variable and
substitution maps.

One example algebra for any signature is the unit algebra \(\mathbf{1}\), where
\(\mathbf{1}\,\tau\,\Gamma = {\{\ast\}}\). Each operation \({\llbracket\cdot\rrbracket}_o\),
and the maps \(\mathtt{var}\) and \(\mathtt{sub}\), return the unique value of
the appropriate type. This trivially satisfies the conditions.

Another example is the algebra of sets and functions for the STLC.\@ First, take
any set \(V\) to represent values of type \(N\). A type \(T\) can then be
interpreted as a set of values \(\mathcal{V}[T]\):
\begin{align*}
{\mathcal{V}[N]} &\mapsto V \\
{\mathcal{V}[\alpha \rightarrowtail \beta]} &\mapsto {{\mathcal{V}[\alpha]} \to {\mathcal{V}[\beta]}}
\end{align*}

We can take the carrier sorted family \({\mathcal{A}\,\tau\,\Gamma} = {(\forall \sigma. {{\mathcal{I}\,\sigma\,\Gamma} \to
{\mathcal{V}[\sigma]}}) \to {\mathcal{V}[\tau]}}\). From here, defining the operations and mappings
is straight forward:
\begin{align*}
{{\llbracket {f , g} \rrbracket}_{\mathtt{app}}(\gamma)} &= {f(\gamma,(g(\gamma)))} \\
{{\llbracket {f} \rrbracket}_{\mathtt{abs}}(\gamma)} &=
  {x \mapsto {f({\mathtt{here} \mapsto x}; {{\mathtt{there}\,i} \mapsto \gamma\,i})}} \\
{\mathtt{var}(i, \gamma)} &= \gamma_i \\
{\mathtt{sub}(f,\sigma,\gamma)} &= {f\,(i \mapsto {\sigma_i(\gamma)})}
\end{align*}

Verifying that this definition satisfies the coherence conditions is left as an
exercise\footnotemark{}.

\footnotetext{This is me being lazy.}

\section{Metavariables}

Here is a typical way of writing the \(\beta\)-reduction relation for STLC:\@

\begin{verbatim}
(λ x. t) $ u ↝ t[x ↦ u]
\end{verbatim}

The variable \verb|t| is implicitly parameterised by the bound variable
\verb|x|, meaning \InFamily{}{\ctxcons{\alpha}{t}}{\Litt{t}}{\beta}. In contrast,
\verb|u| is not parameterised by any terms. We can make the parameters explicit:

\begin{verbatim}
(λ x. t<x>) $ u<> ↝ t<u<>>
\end{verbatim}

\verb|t| and \verb|u| are \emph{metavariables}---free variables with parameters.
We can instantiate metavariables with concrete terms to create new ones. This
property is formalised in the definition of a \emph{syntactic algebra}.

A syntactic algebra for a signature \(\Sigma\) over a sorted family of metavariables
\(\mathfrak{X}\) is:

\begin{itemize}
\item an algebra \(\mathcal{A}\) over the signature
\item a map \(\mathtt{mvar} \in {{\mathfrak{X}\,\tau\,\Pi} \to (\forall \sigma. {{\mathcal{I}\,\sigma\,\Pi} \to {\mathcal{A}\,\sigma\,\Gamma}}) \to
  {\mathcal{A}\,\tau\,\Gamma}}\)
\item and a map \(\mathtt{msub} \in {{\mathcal{A}\,\tau\,\Gamma} \to (\forall {\sigma, \Theta}. {{\mathfrak{X}\,\sigma\,\Theta} \to
  {\mathcal{A}\,\sigma\,(\ctxext{\Theta}{\Delta})}}) \to {\mathcal{A}\,\tau\,(\ctxext{\Gamma}{\Delta})}}\)
\end{itemize}

which satisfy these conditions\footnotemark{}:

\footnotetext{Explain why these conditions exist, and why they are so ugly.}

\begin{enumerate}
\item
  \({\mathtt{sub}(\mathtt{mvar}(\mathfrak{m},\sigma),\varsigma)} =
    {\mathtt{mvar}(\mathfrak{m},{i \mapsto {\mathtt{sub}(\sigma_i,\varsigma)}})}\)
\item
  \({\mathtt{msub}({\llbracket ts \rrbracket}_o,\zeta)} =
    {\llbracket{\mathtt{msub}(ts_i,\zeta)}\rrbracket}_o\)
\item
  \({\mathtt{msub}(\mathtt{var}(i),\zeta)} =
    {\mathtt{var}(\mathtt{inl}(i))}\)
\item
  \({\mathtt{msub}(\mathtt{sub}(t,\sigma),\zeta)} =
    {\mathtt{sub}(\mathtt{msub}(t,\zeta),{\sigma\Uparrow})}\)
\item
  \({\mathtt{sub}(\mathtt{msub}(t,\zeta),{\Uparrow\sigma})} =
    {\mathtt{msub}(t,{\mathfrak{m} \mapsto {\mathtt{sub}(\zeta_{\mathfrak{m}},{\Uparrow\sigma})}})}\)
\item
  \({\mathtt{msub}(\mathtt{mvar}(\mathfrak{m},\sigma),\zeta)} =
    {\mathtt{sub}(\zeta_{\mathfrak{m}},\copair{(i \mapsto {\mathtt{msub}(\sigma_i,\zeta)})}{\mathtt{inr}\circ\mathtt{var}})}\)
\item
  \({\mathtt{msub}(\mathtt{msub}(t,\zeta),\xi)} =
    {\mathtt{msub}(t,{\mathfrak{m} \mapsto {\mathtt{msub}(\zeta_{\mathfrak{m}},\xi)}})}\)
\end{enumerate}

The map \(\mathtt{mvar}\) takes a metavariable \InFamily{\mathfrak{X}}{\Pi}{\mathfrak{m}}{\tau} and
converts it into a term in context \(\Gamma\). This is by giving a value for each of
\(\mathfrak{m}\)'s parameters, achieved via the substitution argument.

The syntactic substitution map \(\mathtt{msub}\) is more complex. First note
that it is linear: the output context is an extension of the input. This means
that metasubstitution can use bound variables, as long as they were bound in a
higher scope. Also observe that the substitution map (the second parameter) is
independant of the input context \(\Gamma\). Because metavariables are always
associated with a substitution, it is sufficient to map only the metavariables
in their original contexts. The context can be ``corrected'' by a substitution.

%% Conditions 1, 2 and 3 require syntactic substitution to pass through normal term
%% operations. \(\zeta\) remains unchanged because it never mentions the original
%% context. The most subtle

The term algebra \term{\mathfrak{X}} for a signature is the free syntactic algebra over
\(\mathfrak{X}\), with for each map \(f \in {{\mathfrak{X}\,\tau\,\Gamma}\to{\mathcal{A}\,\tau\,\Gamma}}\) a unique homomorphism
\(\mathtt{bind}(f) \in {\term{\mathfrak{X}} \to \mathcal{A}}\).

Return to the earlier example of \(\beta\) reduction. We have metavariables \(\mathfrak{X}\)
with two elements: \InFamily{\mathfrak{X}}{\alpha}{\Litt{t}}{\beta} and \InFamily{\mathfrak{X}}{}{\Litt{u}}{\alpha}.
We then have two terms, both of type \(\beta\) in an empty context:
\verb|(λ x. t<x>) $ u<>| and \verb|t<u<>>|.

As a more complex example, we can construct a syntactic substitution map \(\zeta \in
{{\mathfrak{X}\,\sigma\,\Theta} \to {\mathcal{A}\,\sigma\,(\ctxext{\Theta}{\ctxcons{\tarr{\alpha}{\beta}}{\alpha}})}}\)\footnotemark{}:
\begin{gather*}
  \InFamily{\mathcal{A}}{\ctxcons{\alpha}{\ctxcons{\tarr{\alpha}{\beta}}{\alpha}}}{\Lapp{\Var{1}}{\Var{0}}}{\beta} \\
  \InFamily{\mathcal{A}}{\ctxcons{\tarr{\alpha}{\beta}}{\alpha}}{\Var{1}}{\alpha}
\end{gather*}

\footnotetext{Include some examples.}

Metavariables allow a formal definition of equational theories, and then models.
An \emph{equation} is a quintuple \((\mathfrak{X},\Gamma,\tau,\Litt{t},\Litt{u})\) such that
\InFamily{\term{\mathfrak{X}}}{\Gamma}{\Litt{t}}{\tau} and \InFamily{\term{\mathfrak{X}}}{\Gamma}{\Litt{u}}{\tau}. An
\emph{equational theory} is a signature with a finite set of axioms
\InFamily{\term{\mathfrak{X}}}{\Gamma}{\Litt{t} =_a \Litt{u}}{\tau}. This can be extended to an
equivalence relation \InFamily{\term{\mathfrak{X}}}{\Gamma}{\Litt{t} = \Litt{u}}{\tau} by taking
the closure of axioms with respect to metasubstitution.

A \emph{model} of an equational theory is an algebra \(\mathcal{A}\) where all equations
are valid: given an equation \InFamily{\term{\mathfrak{X}}}{\Gamma}{\Litt{t} = \Litt{u}}{\tau},
then for any environment map \(f \in {\mathfrak{X}\,\tau\,\Gamma}\to{\mathcal{A}\,\tau\,\Gamma}\), the equality
\(\mathtt{bind}(f,t) = \mathtt{bind}(f,u)\) holds.

\section{Free Extensions}

%% Computation involving terms of second-order algebras often starts by
%% transforming them into a normal form. Informally, this is a syntactic operation
%% that usually performs some evaluation of the term that preserves the semantics.

%% An algebra (or model) \(\mathcal{A}\) is a \emph{normal form} of term algebra (model)
%% \(\term{\mathfrak{X}}\) if it consists of:

%% \begin{itemise}
%% \item a map \(\mathtt{env} \in {{\mathfrak{X}\,\tau\,\Gamma}\to{\mathcal{A}\,\tau\,\Gamma}}\)
%% \item a homomorphism \(\mathtt{reify} \in \mathcal{A}\to{\term{\mathfrak{X}}}\)
%% \end{itemise}

%% where the composite homomorphism
%% \({{\mathtt{bind}(\mathtt{env})}\circ\mathtt{reify}}\) is the identity. Define
%% \(\mathtt{eval} = {\mathtt{bind}(\mathtt{env})}\).

%% The main structure of a normal form is the \(\mathtt{reify}\) homomorphism,
%% which interprets the algebra as terms. The map \(\mathtt{env}\) provides the
%% intended interpretation of the non-algebraic values of \(\mathcal{A}\), reflected in the
%% identity condition.

%% Note that normal forms make no requirement of \(\mathtt{eval}\) or
%% \(\mathtt{reify}\) to perform any computation. This means that terms are a
%% trivial normal form.

%% At first, you may think that \(\mathcal{A}\) is trivially a normal form of \(\term{\mathcal{A}}\), where
%% \(\mathtt{env}\) is the identity. However, there is in general no homomorphism
%% \(\mathcal{A}\to{\term{\mathcal{A}}}\).

Given an algebra (or model) \(\mathcal{A}\) and metavariables \(\mathfrak{X}\), a \emph{free
extension} of \(\mathcal{A}\) by \(\mathfrak{X}\) is a syntactic algebra (or model) \(\mathcal{F}\) over \(\mathfrak{X}\)
with the following additional structure:

\begin{itemize}
\item a homomorphism \(\mathtt{sta} \in {\mathcal{A}\to\mathcal{F}}\)
\item for every pair of homomorphism \(f \in {\mathcal{A}\to\mathcal{B}}\) and map \(g \in
  {{\mathcal{X}\,\tau\,\Gamma}\to{\mathcal{B}\,\tau\,\Gamma}}\), a unique homomorphism \(\mathtt{interp}(f,g) \in
  {\mathcal{F}\to\mathcal{B}}\)
\end{itemize}

with the following two conditions:

\begin{itemize}
\item \({{\mathtt{interp}(f,g)}\circ\mathtt{sta}} = g\)
\item
  \({{\mathtt{interp}(f,g,{\mathtt{mvar}(\mathfrak{m},\sigma)})}} =
    {\mathtt{sub}(g(\mathfrak{m}),{{\mathtt{interp}(f,g)} \circ \sigma})}\)
\end{itemize}

This is equivalently the algebraic (model) coproduct of \(\mathcal{A}\) and \(\term{\mathfrak{X}}\).
The free extension is an extension in the sense that the algebra \(\mathcal{A}\) is given
an interpretation of metavariables. It is free in the sense that adding the
metavariables minimally restricts the homomorphisms to or from the algebra.

Define the map \(\mathtt{dyn} \in {{\mathfrak{X}\,\tau\,\Gamma}\to{\mathcal{F}\,\tau\,\Gamma}}\) by \(\mathtt{dyn}(\mathfrak{m}) =
\mathtt{msub}(\mathfrak{m},\mathtt{var})\). The names \(\mathtt{sta}\) and \(\mathtt{dyn}\)
come from the perspective of staged compilation: values made with
\(\mathtt{sta}\) are known statically and can be acted on during compilation.
Values defined via \(\mathtt{dyn}\) are only known at runtime and have no
inherent algebraic structure.

Using \(\mathtt{sta}\) and \(\mathtt{dyn}\), there is a homomorphism
\(\mathtt{eval} \in {\term{\mathcal{A} \cup \mathfrak{X}}\to\mathcal{F}}\) given by \(\mathtt{eval} =
{\mathtt{bind}(\mathtt{sta}\cup\mathtt{dyn})}\). Because there is a morphism
\(\mathcal{A}\to{\term{\mathcal{A}}_{/\approx}}\)\footnotemark{}, there is also a morphism
\(\mathtt{reify} \in {\mathcal{F}\to{\term{\mathcal{A} \cup \mathfrak{X}}_{/\approx}}}\) defined using \(\mathtt{interp}\).

\footnotetext{Define what \(\approx\) is.}

%% One universal instance of the free extension is given by \(\mathbb{T}{[\mathcal{A} \cup \mathfrak{X}]}\), quotient
%% the conditions listed earlier. Define homomorphisms \(\mathtt{eval} \in
%% {{\mathbb{T}{[\mathcal{A} \cup \mathfrak{X}]}} \to \mathcal{F}}\) and \(\mathtt{reify} \in {\mathcal{F} \to {\mathbb{T}{[\mathcal{A} \cup \mathfrak{X}]}}}\) given by
%% \(\mathtt{bind}\) and \(\mathtt{interp}\) respectively. \(\mathtt{eval}\)
%% ideally performs static computations, normalising the term in some way, and
%% \(\mathtt{reify}\) exports the normal form as a term.

For brevity, let \(\sta{\Litt{t}}\) represent \(\mathtt{sta}(\Litt{t})\) and
understand \(\dyn{\mathfrak{m}}\) to be \(\mathtt{dyn}(\mathfrak{m})\).

\section{βη-Normal Form as a Free Extension}

In the STLC, βη-normal form is a way of writing terms such that test for βη
equivalence is a simple identity check. I will adapt this normal form to attempt
to produce a free extension of a STLC model \(\mathcal{A}\) by metavariables \(\mathfrak{X}\),
dubbed \(\mathcal{A}_{\beta\eta}[\mathfrak{X}]\).

%% There are a couple of minor conceptual optimisations that we can apply before
%% evaluating terms. Remember that \(\mathtt{sta}\) is a homomorphism, thus
%% \(\Var{i} = \sta{\Var{i}}\) for all variables \(\Var{i}\). By
%% applying this as a substitution on terms, we only have to consider application,
%% abstraction, static values and dynamic metavariables. Further, we write
%% \(\sta{\Litt{t}}\) for \(\mvar{\sta{\Litt{t}}}{\mathtt{var}}\), and treat it
%% as a distinct case.

A term is \emph{dynamic} if there is a subterm that uses a dynamic metavariable.
Otherwise it is static. For example, \(\mvar{\dyn{\mathfrak{m}}}{\zeta}\) and
\(\Lapp{\sta{\Litt{t}}}{(\Labs{x}{\mvar{\dyn{\Litt{n}}}{\Litt{x}}})}\) are
both dynamic, whilst \(\Var{i}\), \(\sta{\Litt{t}}\) and
\(\Labs{x}{\mvar{\sta{\Litt{u}}}{\Litt{x}}}\) are static.

The sorted family \(\mathcal{A}_{\beta\eta}[\mathfrak{X}]\) and a family \(\mathcal{A}_{ne}[\mathfrak{X}]\) are defined
inductively by the following judgements:

\begin{gather*}
\begin{prooftree}
  \hypo{\InFamily{\mathcal{A}_{\beta\eta}[\mathfrak{X}]}{\ctxcons{\Litt{x} : \alpha}{\Gamma}}{\Litt{t}}{\beta}}
  \infer1[1]{\InFamily{\mathcal{A}_{\beta\eta}[\mathfrak{X}]}{\Gamma}{\Labs{x}{\Litt{t}}}{\tarr{\alpha}{\beta}}}
\end{prooftree}
\qquad
\begin{prooftree}
  \hypo{\InFamily{\mathcal{A}_{ne}[\mathfrak{X}]}{\Gamma}{\Litt{t}}{N}}
  \infer1[2]{\InFamily{\mathcal{A}_{\beta\eta}[\mathfrak{X}]}{\Gamma}{\Litt{t}}{N}}
\end{prooftree}
\\
\begin{prooftree}
  \hypo{\InFamily{\mathcal{A}_{ne}[\mathfrak{X}]}{\Gamma}{\Litt{t}}{\tarr{\alpha}{\beta}}}
  \hypo{\InFamily{\mathcal{A}_{\beta\eta}[\mathfrak{X}]}{\Gamma}{\Litt{u}}{\alpha}}
  \hypo{\Litt{t} \text{ or } \Litt{u} \text{ uses a dynamic variable}}
  \infer3[3]{\InFamily{\mathcal{A}_{ne}[\mathfrak{X}]}{\Gamma}{\Lapp{\Litt{t}}{\Litt{u}}}{\beta}}
\end{prooftree}
\\
\begin{prooftree}
  \hypo{\InFamily{\mathfrak{X}}{\Pi}{\mathfrak{m}}{\tau}}
  \hypo{\InFamily{\mathcal{A}_{ne}[\mathfrak{X}]}{\Gamma}{\sigma_i}{\Pi_i}}
  \infer2[4]{\InFamily{\mathcal{A}_{ne}[\mathfrak{X}]}{\Gamma}{\mvar{\dyn{\mathfrak{m}}}{\sigma}}{\tau}}
\end{prooftree}
\qquad
\begin{prooftree}
  \hypo{\InFamily{\mathcal{A}}{\Gamma}{\Litt{t}}{\tau}}
  \infer1[5]{\InFamily{\mathcal{A}_{ne}[\mathfrak{X}]}{\Gamma}{\mvar{\sta{\Litt{t}}}{\mathtt{var}}}{\tau}}
\end{prooftree}
\\
\begin{prooftree}
  \hypo{\InFamily{\mathcal{A}}{\Pi}{\Litt{t}}{\tau}}
  \hypo{\InFamily{\mathcal{A}_{\beta\eta}[\mathfrak{X}]}{\Gamma}{\sigma_i}{\Pi_i}}
  \hypo{\sigma \text{ uses a dynamic variable}}
  \infer3[6]{\InFamily{\mathcal{A}_{ne}[\mathfrak{X}]}{\Gamma}{\mvar{\sta{\Litt{t}}}{\sigma}}{\tau}}
\end{prooftree}
\end{gather*}

In summary, this normal form first requires terms to have no β~reductions
(resulting in a family of neutral terms \(\mathcal{A}_{ne}[\mathfrak{X}]\)). Then terms are
η~expanded so each type constructor has exactly one constructor.

Rules 1~and~2 describe how to convert neutral terms into normal forms: each
function requires an explicit abstraction, and terms of neutral type must be
neutral.

Rule~3 describes which applications are irreducible. The first argument to the
application must itself be irreducible. If the only requirement was for it to be
in normal form, then it could be an abstraction term. This is β-reducible, so
goes against the principal of performing all possible reductions. Further at
least one argument must use a dynamic variable. If both arguments to application
were static, then they are both values in \(\mathcal{A}\) so the application can be
reduced by using application from \(\mathcal{A}\). Thus, evaluation is stuck only if at
least one of the two argument has a dynamic variable.

Rule~4 states that dynamic variables are always stuck. There is no information
to allow for further evaluation, so they are always neutral.

Rules 5~and~6 describe which substitutions into static values are neutral.
Rule~5 says that the identity substitution is stuck. Static values always appear
with a substitution in terms. Because applying the identity substitution doesn't
change the static value, nor does it influence any later substitutions, it is
the maximally-reduced substitution where all components are static. The
hypothesis of rule~6 requires at least one substitution parameter to be dynamic.
Vecause substitutions are performed in parallel, this blocks the full
substitution.

Notice that neither normal forms or neutral terms used bound variables. Any
variable \(\Var{i}\) is equivalent to \(\mvar{\sta{\Var{i}}}{\mathtt{var}}\).
Expanding bound variables into static values can be seen as a reduction, so
should be evaluated according to the principal of performing all possible
reductions.

Using a logical relations argument, it is possible to define a mapping
\(\mathbb{T}[\mathcal{A} \cup \mathfrak{X}] \to \mathcal{A}_{\beta\eta}[\mathfrak{X}]\)\footnotemark{}.

\footnotetext{How, exactly?}

\section{The Equality Problem}

Unfortunately, the normal form just presented using equality is not a model of
STLC.\@ In fact, it is not even an algebra. The problem comes from substitution,
and can be demonstrated by the following two equal terms:
\begin{align*}
\mvar{\sta{\Lapp{\Var{i}}{\Litt{t}}}}{\dyn{\sigma}}
  &= \Lsub{(\Lapp{\sta{\Var{i}}}{\sta{\Litt{t}}})}{\dyn{\sigma}} \\
  &= \Lsub{(\Lapp{\Var{i}}{\sta{\Litt{t}}})}{\dyn{\sigma}} \\
  &= \Lapp{\Lsub{\Var{i}}{\dyn{\sigma}}}{\Lsub{\sta{\Litt{t}}}{\dyn{\sigma}}} \\
  &= \Lapp{\dyn{\sigma_i}}{\mvar{\sta{\Litt{t}}}{\dyn{\sigma}}}
\end{align*}

Assuming the terms have type \(N\), then they are in normal form. The top two
lines normalise to the first term, and the bottom two lines normalise to the
final term. However, because the subterm \(\sta{\Lapp{\Var{i}}{\Litt{t}}}\) is
opaque for an arbitrary algebra \(\mathcal{A}\), these two normal forms for the same term
are distinct.

For this normal form to be an algebra, it must be taken quotient \(\approx\), the same
relation the term algebra is subject to.

\section{Removing the Quotient: Effective Free Extensions}

In practical systems, using a quotient for equality can be undesirable.
Especially when the quotient is undecidable. An \emph{effective} free extension
uses identity of values for equality---both easy to compute and decidable.

I suspect that there is no free extension for STLC that is effective for all
algebras, due to the equality problem. Instead, I will discuss classes of
algebras where the βη-normal form is effective.

The simplest case is when \(\mathcal{A} = \term{\emptyset}\): the initial algebra. In this case,
\(\term{\term{\emptyset} \cup \mathfrak{X}}_{/\approx} \cong \term{\mathfrak{X}}\), and \(\term{\emptyset}_{\beta\eta}[\mathfrak{X}]\) is the
classical βη-normal form extended with metavariables. By design, βη-normal form
identifies terms that are equivalent, thus this is an effective free extension.
This argument can be generalised to \(\mathcal{A} = \term{\mathfrak{Y}}\), for any fixed set of
metavariables \(\mathfrak{Y}\), as \(\term{\term{\mathfrak{Y}} \cup \mathfrak{X}}_{/\approx} \cong \term{\mathfrak{Y} \cup \mathfrak{X}}\).

Now consider an algebra \(\mathcal{A}\) such that there is an isomorphism \(\mathcal{A}\cong\term{\mathfrak{Y}}\).
This is true for all ``normal forms'' of \term{\mathfrak{Y}}, such as weak-head normal
form, βη-normal form, and CPS form. \(\mathcal{A}_{\beta\eta}[\mathfrak{X}]\) is an effective free
extension, because it is isomorphic to \(\term{\mathfrak{Y}}_{\beta\eta}[\mathfrak{X}]\), which is effective.

One thing missing from the previous form is terms that compute on values of the
neutral type. For example, if an algebra \(\mathcal{A}\) treats values of type \(N\) as
naturals, with an addition operator, then \(\mathcal{A}\not\to\term{\mathbb{N}\cup\{+\}}\), because
\(\sta{5} = \sta{\mvar{add}{2, 3}} = \mvar{\sta{add}}{\sta{2}, \sta{3}}\), but
the outer terms are not equal in \term{\mathbb{N}\cup\{+\}}.

Everthing past here is a rough sketch.

Define \(\mathcal{A}\) to be a (sub|super)-model\footnotemark{} of the STLC when there is:

\footnotetext{I don't know which is better. Maybe it should be something
  completely different?}

\begin{itemize}
\item a sorted family \(\mathfrak{Y}\)
\item a set of axioms \(\mathbf{Ax} \in \InFamily{\term{\mathfrak{X}\cup\mathfrak{Y}}}{\emptyset}{t =_{\mathcal{A}} u}{\tau}\)
\item an isomorphism \(\mathcal{A} \cong \term{\mathfrak{Y}}_{/\mathbf{Ax}}\)
\end{itemize}

where

\begin{itemize}
\item abstraction does not occur in  \(\mathbf{Ax}\)
\item all equalities in \(\mathcal{A}\) are generated by β- and η- equalities and \(\mathbf{Ax}\)
\end{itemize}

\appendix
\section{Commentary about \LaTeX}

The character \(\mathfrak{Y}\) is written \verb|\mathfrak{Y}|, yet it looks much more like an ``N'' to
me.

\end{document}

% LocalWords:  unpair/pair