Agent-assistance disclosure: this work was prepared with AI-agent assistance (drafting, code, experiments) under human direction. The authors, writing as Third Projection Collective, take responsibility for its content. Open proofs are marked [OPEN] in the text.
\begin{document}
\title{Computing the Futamura Diamond: Textual Agreement of Generated Compilers and a Self-Applicable Specializer}
\author{Third Projection Collective}\affiliation{\institution{Pseudonymous}\country{}}
\begin{abstract}
Two recent notes on higher-categorical semantics of specialization disagree on whether the compiler produced by the second Futamura projection, $\mathsf{mix}(\mathsf{mix},\mathsf{int})$, and the compiler produced by running the generated compiler generator on the interpreter, $\sem{\mathsf{mix}(\mathsf{mix},\mathsf{mix})}(\mathsf{int})$, are equal as texts. One treats this equality (H2'') as an independent hypothesis; the other derives an equivalent equation. We settle the question: H2 follows from the specialization equation (PE) together with the requirement that the specializer program implements the specializer function as an equality of output data, and we mechanize this in Lean~4. We show H2 is genuinely independent only when (PE) is weakened to hold up to an equivalence on outputs, by a construction using the second recursion theorem. We then build Fut0, a first-order Lisp with a 54-line Python evaluator, and mix0, a 60-line self-applicable offline partial evaluator written in Fut0, run all three projections, and confirm textual agreement and self-generation of the compiler generator by hash comparison. mix0 lacks let-insertion, so its residual programs are correct but large and slow; we report this negative result. The coherence conjecture (a 2-cell filling the diamond in a general trace calculus) remains \emph{open}; we state precisely what our results do and do not settle.
\end{abstract}
\maketitle\hypersetup{pdfauthor={Third Projection Collective}}
\section{Introduction}
Futamura's projections~\cite{futamura99} state that specializing an interpreter to a program yields a target program (F1), specializing the specializer to the interpreter yields a compiler (F2), and specializing the specializer to itself yields a compiler generator (F3). Jones, Gomard and Sestoft made self-application practical~\cite{jgs93}. Recent notes on the website \emph{Higher Categorical Semantics} propose treating the projections as coherence data~\cite{hcsA}, connect them to higher rewriting~\cite{hcsB}, and develop a proof-relevant semantics~\cite{hcsC}. In~\cite{hcsB} (Remark 4.4), the textual equality $\mathsf{comp}_3=\mathsf{comp}_2$ is called a genuine hypothesis''. In~\cite{hcsC} (Proposition 2.2), $E_g(i)=c_i$ is derived from (PE) and the implementation equation. The two notes use the same (PE). This paper resolves the disagreement and supplies the executable artifact both notes plan but do not contain.
\paragraph{Contributions.} \begin{itemize} \item Theorem~\ref{thm:h2}: under (PE) and exact implementation, H2 holds; also $E_g(m)=g$ (self-generation). Both are mechanized in Lean~4 (\texttt{lean/H2.lean}, checked with Lean's core library only). \item Proposition~\ref{prop:indep}: if (PE) only holds up to an equivalence $\approx$ on outputs, H2 can fail. Remark~4.4 of~\cite{hcsB} is therefore correct only under that weakened reading, which~\cite{hcsB} does not adopt. \item An implementation: Fut0 and mix0, with all three projections executed, textual agreement checked, and costs measured (Section~\ref{sec:impl}). \end{itemize}
\section{Setting} Fix a set $C$ of program texts, a set $D$ of data with an injection $\ulcorner-\urcorner:C\to D$ and a pairing $\langle-,-\rangle$, and an evaluator $E:C\times D\rightharpoonup D$. A specializer is a partial function $\mu:C\times D\rightharpoonup C$ such that \begin{equation}\tag{PE} \mu(p,s)=r \implies \forall d.\; E_r(d)\simeq E_p(\langle s,d\rangle), \end{equation} where $\simeq$ is Kleene equality of partial values. A program $m$ \emph{implements} $\mu$ if $E_m(\langle\ulcorner p\urcorner,s\rangle)\simeq\ulcorner\mu(p,s)\urcorner$ for all $p,s$. This is exactly Definition~2.1 of~\cite{hcsC}, and it is the reading of (PE) used by~\cite{hcsA,hcsB}. In both, $\sem{-}$ maps into partial functions $D\to D$, so equality of residual behaviour is equality of output data.
\section{Textual agreement is a theorem} \begin{theorem}\label{thm:h2} Assume (PE) and that $m$ implements $\mu$. Let $g=\mu(m,\ulcorner m\urcorner)$ and $c=\mu(m,\ulcorner i\urcorner)$ be defined. Then $E_g(\ulcorner i\urcorner)=\ulcorner c\urcorner$ and $E_g(\ulcorner m\urcorner)=\ulcorner g\urcorner$. \end{theorem} \begin{proof} By (PE) at $(m,\ulcorner m\urcorner)$, $E_g(\ulcorner i\urcorner)\simeq E_m(\langle\ulcorner m\urcorner,\ulcorner i\urcorner\rangle)$. By implementation this is $\ulcorner\mu(m,\ulcorner i\urcorner)\urcorner=\ulcorner c\urcorner$. The second claim is the case $i=m$. \end{proof} In the notation of~\cite{hcsB}, $\mathsf{cogen}=g$, $\mathsf{comp}_2=c$, and $\mathsf{comp}_3$ is the output of running $\mathsf{cogen}$ on $\mathsf{int}$. Theorem~\ref{thm:h2} gives $\mathsf{comp}_3=\mathsf{comp}_2$ as texts. Hypothesis (H2) of~\cite{hcsB} is therefore redundant given its (PE) and (H1). The Lean statement quantifies over arbitrary types $C$, $D$, encodings and partial evaluators modelled as \texttt{Option}; the proof is three rewrites.
\begin{proposition}\label{prop:indep} Let $\approx$ be an equivalence on $D$ that strictly contains equality on codes, and let (PE$_\approx$) replace $\simeq$ in (PE) by equivalence up to $\approx$. Assume the programming language is acceptable, so the second recursion theorem holds. Then there exist $\mu'$ satisfying (PE$_\approx$), a program $m'$ implementing $\mu'$, and an interpreter $i$ with $E_{\mu'(m',m')}(\ulcorner i\urcorner)\neq\ulcorner\mu'(m',\ulcorner i\urcorner)\urcorner$. \end{proposition} \begin{proof} Let $\mu$ be any specializer satisfying (PE), implemented by $m$, and let $\rho:C\to C$ be computable with $\ulcorner\rho(x)\urcorner\approx\ulcorner x\urcorner$ and $\rho(x)\neq x$ for some $x$ (it exists since $\approx$ is strictly coarser on codes). By the recursion theorem there is a program $m'$ that, on $\langle\ulcorner p\urcorner,s\rangle$, outputs $\ulcorner\mu(p,s)\urcorner$ unless $p=m'$ and $s=\ulcorner m'\urcorner$, in which case it outputs the code of a program $g'$ computing $d\mapsto\ulcorner\rho(\mu(m',d))\urcorner$ (if $d$ is a code). Let $\mu'$ be the function $m'$ computes. Then $m'$ implements $\mu'$. (PE$_\approx$) holds for $\mu'$: away from $(m',m')$ it is (PE) for $\mu$; at $(m',m')$, $E_{g'}(d)=\ulcorner\rho(\mu(m',d))\urcorner\approx\ulcorner\mu(m',d)\urcorner\simeq E_{m'}(\langle\ulcorner m'\urcorner,d\rangle)$, using that $\mu'(m',d)=\mu(m',d)$ for $d\neq\ulcorner m'\urcorner$. Choose $i$ with $\rho(\mu(m',\ulcorner i\urcorner))\neq\mu(m',\ulcorner i\urcorner)$. \todo{OPEN: the existence of such an $i$ for a given $\rho$ needs $\mu(m',-)$ to hit a point moved by $\rho$; this holds for the trivial specializer, where $\mu(m',\ulcorner i\urcorner)$ ranges over infinitely many texts and $\rho$ can be chosen to rename a variable occurring in them, but we have not written out the general case.} \end{proof}
\section{The Futamura diamond after Theorem~\ref{thm:h2}} In~\cite{hcsB}, the diamond has vertices $s,a,b,c$ and edges $e_1$ (a PE step), $e_2,e_3,e_4$ (evaluation steps), and Conjecture~A of~\cite{hcsA} asks for a 2-cell $\theta$ between $e_2\cdot e_1$ and $e_4\cdot e_3$. Theorem~\ref{thm:h2} shows that the diamond always closes at the vertex $c$; this is the 1-dimensional content. Whether $\theta$ exists is a choice of the trace calculus. Proposition~4.5 of~\cite{hcsB} correctly states that the diamond is filled iff $K$ contains such a cell. Our results do not decide what $K$ should be. \todo{OPEN: Conjecture A of~\cite{hcsA} and Conjecture 4.7 of~\cite{hcsB} (fillers making components 1-connected for offline specializers) remain unproved. A natural route is to make the PE/Ev system convergent on a fragment and apply the homotopy-basis construction of Kraus and von Raumer~\cite{kraus22}; termination of evaluation steps fails in general, so the fragment must be restricted.} Conjecture~5.2 of~\cite{hcsB} (cogen is a homotopy fixed point under renaming) has its strict, renaming-free instance settled by Theorem~\ref{thm:h2}: $E_g(\ulcorner m\urcorner)=\ulcorner g\urcorner$ with the identity renaming. \todo{OPEN: the version where outputs agree only up to renaming.}
\section{Implementation}\label{sec:impl} \paragraph{Fut0.} Data are atoms and lists, $()$ is false, and primitives are \texttt{car}, \texttt{cdr}, \texttt{cons}, \texttt{eq}, \texttt{atom}, \texttt{null}. Programs are lists of first-order definitions; \texttt{define-unfold} marks a function the specializer may unfold when some argument is static. These are offline binding-time annotations. The evaluator is a 54-line Python file (\texttt{fut0.py}). \paragraph{mix0.} mix0 is written in Fut0 (60 lines, 947 nodes as a tree). It contains its own Fut0 evaluator and specializes the first parameter of \texttt{main}. Calls whose arguments are all static are evaluated. Calls to unfoldable functions with some static argument are unfolded by substituting residual expressions. Static conditionals are reduced. Everything else is residualized monovariantly against a copy of the subject's definitions. Self-application terminates because mix0's structural functions (\texttt{spec}, \texttt{spec-if}, \texttt{spec-list}, \texttt{spec-app}) are the only unfoldable ones and recurse on static syntax; its evaluator and the callee-unfolding step \texttt{spec-call} are not unfoldable. \paragraph{Subject.} The subject is an interpreter (148 nodes) for a stack language with \texttt{push}, \texttt{pop}, \texttt{dup}, \texttt{swap} and a nested conditional \texttt{ifempty}.
\paragraph{Results.} All numbers come from \texttt{experiments.py} (fixed seed 0) and are stored in \texttt{results.json}. \begin{itemize} \item F1: for 20 random programs (lengths 3 to 12) and 4 input stacks each, the target agrees with the interpreter on all 80 runs (errors are compared as errors). \item F2: $\mathsf{comp}=\mathsf{mix}(\mathsf{mix},\mathsf{int})$ has 1{,}644 nodes and took 30{,}380 evaluator steps to build. For all 20 programs, $E_{\mathsf{comp}}(p)$ equals $\mathsf{mix}(\mathsf{int},p)$ textually. \item F3: $\mathsf{cogen}=\mathsf{mix}(\mathsf{mix},\mathsf{mix})$ took 355{,}796 steps and has 2{,}950{,}716 nodes counted as a tree. Shared subterms are not counted once; this is a consequence of substitution without let-insertion. \item H2: $E_{\mathsf{cogen}}(\mathsf{int})$ and $\mathsf{comp}$ have the same SHA-256 prefix (\texttt{2483dddc110de42c}) and are equal as structures. $E_{\mathsf{cogen}}(\mathsf{mix})=\mathsf{cogen}$ holds textually. \item Negative result: on one program of length 30, the interpreter takes 959 steps and the target 1{,}815{,}770. Unfolding duplicates dynamic argument expressions (\texttt{dup} uses the stack twice), so work is repeated exponentially. mix0 demonstrates the projections and textual agreement, not speedup. Adding let-insertion is the obvious fix and is future work. \end{itemize}
\section{Related work} Glück~\cite{gluck09} analyses whether a fourth projection exists and notes the self-generating property of the compiler generator. Our Theorem~\ref{thm:h2} is the abstract form of that observation; we claim no priority for it, only that it resolves the disagreement between~\cite{hcsB} and~\cite{hcsC}. Grobauer and Yang~\cite{grobauer99} derive F2 for type-directed partial evaluation. Kraus and von Raumer~\cite{kraus22} give the rewriting coherence theorem we would need for Conjecture~A.
\section{Conclusion and limitations} H2 is a consequence, not a hypothesis, under the setup shared by the three notes. The executable check agrees. Open: Conjecture A / 4.7 (fillers); the up-to-renaming version of Conjecture 5.2; the general case of Proposition~\ref{prop:indep}; a let-inserting mix with real speedups. Agent assistance: this paper and its code were drafted with AI-agent assistance under human direction; the authors (Third Projection Collective) are responsible for the content. \bibliographystyle{ACM-Reference-Format}\bibliography{refs} \end{document}