1. Problem and contribution
Partial evaluation and self-application yield residual programs, compilers, and compiler generators [3,4]. Their correctness equations leave proof coherence, distributed compatibility, and resource cost to be established.
We combine higher e-graph proof spaces and initiality [1] with specialization and distribution [2]. We characterize compiler-coherence obstructions and their spaces of choices, exhibit a parameterized obstruction, and apply initiality and descent to verification. The underlying cofinality, descent, and Squier theorems are established results.
The main results are Theorems 3.2 and 5.2. Both source articles are labelled Editorially reviewed; [2] is a proposal. The attached PDF includes expanded discussion and appendices.
Conventions. Spaces are homotopy types, denoted by $\mathcal S$. Infinity-category means $(\infty,1)$-category. Limits, pullbacks and diagrams are homotopy coherent. Cartesian means finite-product-preserving. For paths, $r\cdot s$ means first $r$, then $s$. Indexing categories are small in fixed universes. Inhabitation does not imply an algorithm finding a witness.
2. Partial evaluation and its witness refinement
Definition 2.1 (Admissible self-application). Fix a set $C$ of program representations embedded in a data set $D$ with pairing, an evaluator $E:C\times D\rightharpoonup D$, and a partial specializer $\mu:C\times D\rightharpoonup C$. Write $E_p(d)=E(p,d)$ and $E_p(s,d)=E_p(\langle s,d\rangle)$. Whenever $\mu(p,s)$ is defined, require equality of partial functions $$ E_{\mu(p,s)}(-)\simeq E_p(s,-). \tag{PE} $$ Here extensional equality includes the domain of definition and returned values. Let $m\in C$ implement $\mu$: $E_m(p,s)=\mu(p,s)$ as partial functions. Self-application is admissible only for the particular expressions assumed defined below. In a typed implementation these conditions require compatible code encodings and stage types. This definition does not make the evaluator total or computably decide its termination domain.
For an interpreter $i\in C$ and source representation $p\in D$, assume the needed calls exist and put $$ r_{i,p}=\mu(i,p),\qquad c_i=\mu(m,i),\qquad g=\mu(m,m). $$ Proposition 2.2 (Projections and self-generation). Under Definition 2.1, $$ E_{r_{i,p}}(d)\simeq E_i(p,d),\quad E_{c_i}(p)=\mu(i,p),\quad E_g(i)=c_i, \qquad E_g(m)=g. \tag{1} $$ The first equality compares partial computations. The remaining displayed values exist under the stipulated specialization assumptions.
Proof. Apply (PE) to $(i,p)$, $(m,i)$, and $(m,m)$, respectively. The implementation equation for $m$ gives the middle equalities. Finally $$ E_g(m)=E_{\mu(m,m)}(m)=E_m(m,m)=\mu(m,m)=g. $$ Definedness follows because (PE) equates partial functions, including their domains. $\square$
Equation (1) does not prove witness uniqueness, a runtime bound, or that all projection schemes stop; see [4].
Definition 2.3 (Witness refinement). A witness refinement supplies a small cartesian infinity-category $T$ for the pure value and constraint theory, chosen expressions representing the relevant operations, and sound correctness paths in its mapping spaces. For specialization it includes a specified lift $\varepsilon_{p,s}$ of (PE), stable under the substitutions being used. Uniform reasoning requires a coherent family of such witnesses. A collection of unrelated pointwise proofs is insufficient. This is additional structure on the extensional setup.
Put $P_{A,B}=\operatorname{Map}_T(A,B)$. Programs, correctness paths, and homotopies between paths are 1-, 2-, and 3-cells in $T$. Directed presentations may retain noninvertible 2-cells. Partial execution and effects require explicit semantics; all partial functions are not being declared a cartesian category [7].
3. The obstruction to Futamura coherence
Let $Q$ be a space of compiler expressions, $P$ a space of their semantic expressions, and $e:Q\to P$ the chosen interpretation. Let $c_2,c_3\in Q$ denote the compiler obtained directly by F2 and the compiler obtained by evaluating F3 on the interpreter. A witness refinement supplies $$ \psi:c_3\rightsquigarrow c_2,\quad \kappa_2:e(c_2)\rightsquigarrow b,\quad \kappa_3:e(c_3)\rightsquigarrow b, $$ where $b\in P$ is the required behavior. The certificates $\kappa_2,\kappa_3$ may have been constructed independently.
Definition 3.1 (Coherence space). Set $a=e(c_3)$, $\beta=\operatorname{ap}_e(\psi)\cdot\kappa_2$, and $$ \operatorname{Coh}(\kappa_3,\beta) =\operatorname{Path}_{\operatorname{Path}_P(a,b)}(\kappa_3,\beta). \tag{2} $$ Thus a coherence compares parallel certificates after their compiler endpoints have been aligned. Defining $\kappa_3:=\beta$ provides one certificate by transport. Comparing an independently produced $\kappa_3$ is a further obligation.
Theorem 3.2 (Existence and choices). For any space $P$, points $a,b$, and paths $\alpha,\beta:a\rightsquigarrow b$:
1. $\operatorname{Coh}(\alpha,\beta)$ is inhabited exactly when $[\alpha\cdot\beta^{-1}]=1$ in $\pi_1(P,a)$. 2. After choosing one coherence $\Theta$, there is an equivalence $\operatorname{Coh}(\alpha,\beta)\simeq\Omega^2(P,a)$. This equivalence depends on the choices. 3. Consequently the set of components of the coherence space, when inhabited, is a torsor for $\pi_2(P,a)$. Choosing $\Theta$ identifies it with that group. For $k\geq1$, its based homotopy groups are $\pi_{k+2}(P,a)$.
Proof. Put $H=\operatorname{Path}_P(a,b)$. Concatenation with $\alpha^{-1}$ on the right identifies $H$ with $\Omega(P,a)$, taking $\alpha$ to the constant loop up to the standard inverse homotopy. The points $\alpha,\beta$ are in the same component exactly when their difference loop is null-homotopic, proving (1). Given $\Theta:\alpha\rightsquigarrow\beta$ in $H$, the maps $\gamma\mapsto\gamma\cdot\Theta^{-1}$ and $\ell\mapsto\ell\cdot\Theta$ identify $\operatorname{Path}_H(\alpha,\beta)$ with $\Omega(H,\alpha)$. The preceding equivalence identifies this loop space with $\Omega^2(P,a)$. Taking homotopy groups proves (3); changing the chosen coherence translates the component identification. $\square$
Corollary 3.3. If $P$ is a 1-type, an inhabited coherence space is contractible. If $P=K(A,2)$ for a nonzero abelian group $A$, the coherence space from the constant path to itself is the discrete space $A$. Thus existence need not imply a unique component of choices.
Example 3.4 (The unfilled diamond). Take a graph with vertices $s,u,v,t$ and edges $s\to u\to t$, $s\to v\to t$. Its realization is a circle. Its two routes from $s$ to $t$ determine a nontrivial difference loop, although all vertices have the same image in $\pi_0$. Attaching a disk along that loop supplies a comparison. Therefore equality classes and specified correctness edges alone do not force a comparison between their pastings. This is the proof-space distinction of [1, Proposition 5.1], applied to compiler certificates.
Proposition 3.5 (A conditional construction). Suppose a chosen fragment of the directed specialization calculus has a convergent 2-polygraph presentation. Suppose each generating confluence admits a sound semantic 3-cell with its stated boundary. Then every pair of parallel derivations in its free (2,1)-category admits a semantic comparison generated by those cells.
Proof. Squier completion supplies a homotopy basis for a convergent 2-polygraph [6, Theorem 4.3.2]. Every parallel pair is connected by a composite of generating 3-cells, inverses and whiskerings. Interpret these operations and the specified sound generators in the target. $\square$
The presentation must cover the relevant substitution and structural equations. Convergence and sound fillings are hypotheses. F2/F3 alone do not specify the data and laws of a pseudomonad.
4. Initiality and complete solution spaces
Let $\mathcal X$ be an infinity-topos and $M:T\to\mathcal X_{/U}$ a product-preserving model. A cartesian term diagram $D:J\to T$ has solution family $$ \operatorname{Sol}_M(D)=\lim_{j\in J}MD(j). \tag{3} $$ It can include candidate code, values, correctness paths and boundaries between those paths. Specifying which data are in $D$ determines what its solutions certify.
For $u:J\to K$, use the comma category $J_{/k}$ of arrows $u(j)\to k$. Write $|A|=\operatorname{colim}_A *$. Call $u$ initial if $|J_{/k}|\simeq *$ for every $k$, and $n$-initial if $\tau_{\leq n}|J_{/k}|\simeq *$.
Theorem 4.1 (Specification invariance). If $D\simeq D'u$ and $u$ is initial, then $\operatorname{Sol}_M(D')\to\operatorname{Sol}_M(D)$ is an equivalence. For $n\geq0$, $n$-initiality is equivalent to preservation of limits under restriction for every $H:K\to\mathcal S_{\leq n}$; it also implies this preservation for diagrams of $n$-truncated objects in $\mathcal X_{/U}$.
Proof. For initial $u$, apply the initial-functor theorem to each generalized-point functor $\operatorname{Map}_{\mathcal X_{/U}}(V,-)$; these preserve limits and jointly detect equivalences. For the truncated assertion, in $\operatorname{Fun}(K,\mathcal S_{\leq n})$ the left Kan extension of $1_J$ is $Y_n(k)=\tau_{\leq n}|J_{/k}|$. Restriction on limits is $$ \operatorname{Map}(1_K,H)\longrightarrow\operatorname{Map}(Y_n,H). $$ By Yoneda this is an equivalence for all $H$ exactly when $Y_n\to1_K$ is an equivalence. Generalized points prove the implication for slices. $\square$
This applies [1, Theorems 4.1 and 4.3] and [5, Section 4.1]. A compiler application must construct its diagram comparison and prove initiality; semantic correctness alone does not imply it.
For a cartesian $F:C\to D$, [1, Theorem 3.1] supplies $$ C\xrightarrow{\eta_F}\int_D Y_F\xrightarrow{p_F}D, \qquad Y_F(d)=|C_{/d}|. \tag{4} $$ Here $\eta_F$ is initial and $p_F$ is the left fibration classified by $Y_F$. This retains spaces of represented presentations over $d$, rather than just components. Its cartesian restriction uses product-preserving left Kan extension. The unique-up-to-contractible-choice factorization need not have contractible fibers. Neither (4) nor Theorem 4.1 supplies a terminating saturation algorithm.
5. Parameterized coherence and descent
Definition 5.1 (Relative coherence object). Let $P\to U$ be an object of $\mathcal X_{/U}$ and let $a,b$ be sections. Form the relative path object $$ H=U\times_{P\times_U P}P, $$ using $(a,b)$ and the diagonal. For sections $\alpha,\beta:U\to H$, put $$ W=U\times_{H\times_U H}H. \tag{5} $$ Its sections are coherent comparisons of $\alpha$ and $\beta$ over the entire parameter object. These are homotopy pullbacks, not set-theoretic equalizers.
Theorem 5.2 (Base change and descent of coherence). For every $f:V\to U$, $f^*W$ is the relative coherence object of the pulled-back data. If $q:U'\to U$ is an effective epimorphism with Cech nerve $U'_\bullet$, then $$ \operatorname{Map}_{\mathcal X_{/U}}(U,W) \simeq\lim_{[k]\in\Delta} \operatorname{Map}_{\mathcal X_{/U}}(U'_k,W). \tag{6} $$ For $\mathcal X=\mathcal S$, the fiber at $u$ is the coherence space of Theorem 3.2 for the corresponding fiber data. The same statement holds after applying any point's inverse-image functor.
Proof. Pullback preserves the finite limits defining (5), giving base change. Effectiveness means that $U$ is the colimit of its Cech nerve, also in the slice. Mapping into $W$ sends this colimit to the limit in (6). Pulling back to a point gives the iterated path space of Theorem 3.2. $\square$
Proposition 5.3 (Pointwise coherence need not globalize). There exist fiberwise inhabited coherence objects over $U=S^1$ with no global section, although sections exist after restriction to contractible open arcs.
Proof. Work in spaces. Set $P=U\times K(\mathbb Z,2)$ and let $a=b$ be the constant basepoint section. Then $H\simeq U\times K(\mathbb Z,1)\simeq U\times S^1$. Choose $\alpha$ to be the graph of $\operatorname{id}_{S^1}$ and $\beta$ the graph of a constant map. Every fiber of (5) is a path space between two points of the connected circle, hence inhabited. A section of $W$ would be a homotopy from $\operatorname{id}_{S^1}$ to a constant map, contradicting their actions on $\pi_1$. Both maps are homotopic on each contractible arc. Thus local sections exist, but no compatible complete descent datum can exist. $\square$
6. Verified distribution and guarded execution
Choose a site $(N,J)$ and set $\mathcal X=\operatorname{Sh}_\infty(N,J)$. A family $Z\to U$ may encode certified local executions and boundary values. The descent proof applies to $Z$ and its coherence constraints.
Corollary 6.1. Local certified executions with a complete compatible descent datum determine a global certified solution. Equivalences of solution families can be checked after effective-epimorphic pullback. Initial specification transformations preserve these families by Theorem 4.1.
Proof. Apply (6) to $Z$ and use descent for objects, which makes such pullback conservative. Then apply Theorem 4.1. $\square$
Certificate soundness is a separate hypothesis. An accepted attestation, agreement certificate, or probabilistic proof must be related to the required computation under its actual trust or error model. Sheafification alone does not prove that relation. Nor does a quorum cardinality alone prove stability under base change and composition of covers.
For guarded execution require a covering family and compatible behavior and state-transfer data. A guard need not have a Boolean complement in a general topos. Descent neither synthesizes a scheduler nor implements deoptimization.
Proposition 6.2 (Obstruction is not attribution). Failure of global constraint satisfaction, without further trusted observations, does not identify a dishonest participant.
Proof by counterexample. Let honest components report their local binary relations $x=y$, $y=z$, and $x\ne z$. Each relation is satisfiable and restricts to the full set $\{0,1\}$ on either single variable. No joint assignment satisfies all three. Thus locally nonempty constraints with agreeing marginal supports can be globally inconsistent with no dishonesty. This is not a compatible family of chosen sections of a sheaf; it is the absence of such a choice. $\square$
Contextuality [8] supplies an obstruction analogy. Fault attribution needs additional trusted observations. Agreeing marginal supports are not complete descent data.
7. Cost on presentations
Let $R$ be a set of implementation records, $\sigma:R\to P$ their semantic interpretation, and $b\in P$ a specification. A certificate can be a path $\sigma(x)\rightsquigarrow b$ together with further required data. Given cost $c:R\to[0,\infty]$ and latency $\ell:R\to[0,\infty]$, define $$ \inf\{c(x):x\in R,\ \operatorname{Cert}(x,b)\ne\varnothing,\ \ell(x)\leq L\}. \tag{7} $$ The infimum need not be attained or computable. Cost lives on implementation records; it is not assumed invariant under semantic equivalence.
Proposition 7.1. For $\rho:R\to Q$, a cost factors through its image $\rho(R)$ exactly when it is constant on each fiber of $\rho$. Moreover, an exactly additive nonnegative path cost on a groupoid assigns zero to every arrow.
Proof. Fiberwise constancy is precisely the condition that $\bar c(\rho(x))=c(x)$ be well defined. For a groupoid arrow $r$, exact additivity gives $0=c(1)=c(r)+c(r^{-1})$; nonnegativity forces both terms to vanish. $\square$
This concerns exact additivity, not arbitrary lax cost models. Directed migration costs and invertible semantic certificates must remain distinct.
Proposition 7.2 (Correctness gives no speedup bound). Under quotation facilities, the wrapper specializer $$ \mu_{\mathrm{wrap}}(p,s)=\ulcorner d\mapsto E_p(s,d)\urcorner $$ satisfies (PE) while retaining interpretation of $p$ at residual runtime.
Proof. Executing the wrapper invokes the evaluator on the captured $p,s$ and dynamic $d$, giving exactly the right-hand side of (PE). No interpretive work has been eliminated by this construction. $\square$
If specialize-then-distribute and distribute-then-specialize yield semantic expressions $a_{SD},a_{DS}$ with certificates $\eta_{SD}:a_{SD}\rightsquigarrow b$ and $\eta_{DS}:a_{DS}\rightsquigarrow b$, their semantic comparison is $\eta_{SD}\cdot\eta_{DS}^{-1}$. A syntactic rewrite realizing it requires completeness or an explicit derivation in the chosen calculus. Their cost difference has no predetermined sign. Coherence of independently produced comparisons is again governed by Theorem 3.2.
8. Evidence, scope and research obligations
The accompanying reproducibility package contains exact finite checks for the unfilled and filled diamond, a toy arithmetic specializer, the inconsistent binary constraints, and equivalent expressions with different operation counts. They validate the examples, not the general theorems. The toy specializer does not implement F2/F3 or a self-applicable compiler generator.
A typed self-applicable witness calculus, its sound generating confluences, and initiality for concrete transformations remain constructive obligations. No complete compiler, saturation engine, optimizer, or fault-localization theorem is supplied.
Authorship and automation. Anonymous. An AI assistant assisted with formulation, literature, proofs, typesetting and example code. The researcher authorized preparation and submission. Independent human verification, proof-assistant certification, and referee review are not asserted. The journal determines review and publication status.
References
1. Anonymous. *Higher E-Graphs: Cartesian Factorization, Proof Spaces, and Topos Semantics*. Higher Categorical Semantics, 2026. Editorially reviewed manuscript. Article. 2. Third Projection Collective. *Futamura Projections as Coherence: A Higher-Categorical Semantics of Specialization and Untrusted Distribution*. Higher Categorical Semantics, 2026. Editorially reviewed proposal. Article. 3. Y. Futamura. *Partial Evaluation of Computation Process--An Approach to a Compiler-Compiler*. Higher-Order and Symbolic Computation 12, 381-391, 1999; reprint of the 1971 paper. DOI. 4. R. Gluck. *Is there a fourth Futamura projection?* PEPM 2009, 51-60. Publisher identifier and author record. DOI: 10.1145/1480945.1480954. 5. J. Lurie. *Higher Topos Theory*. Princeton University Press, 2009, Sections 4.1 and 6.1-6.2. Text. 6. Y. Guiraud and P. Malbos. *Polygraphs of finite derivation type*. Mathematical Structures in Computer Science 28(2), 155-201, 2018, Theorem 4.3.2. Author version. 7. D. Pavlovic. *Monoidal computer I: Basic computability by string diagrams*. Information and Computation 226, 94-116, 2013. Author version. 8. S. Abramsky and A. Brandenburger. *The sheaf-theoretic structure of non-locality and contextuality*. New Journal of Physics 13, 113036, 2011. Author version.