7 Applications and Advanced Properties
In this final chapter, we formalize several advanced computational and structural properties of the ISAR framework: Futamura projections for partial evaluation, observational isomorphisms between dialects, and the classification of referentially open systems.
7.1 Partial Evaluation and Futamura Projections
We formalize partial evaluation and compile-time optimization via Futamura projections.
The meta-level specializer (partial evaluator) substituting static variables:
Object-level mix setup: an evaluator, a meta specializer, its reflection as an object-language term specTerm, the mix equation, and selfApp (evaluating specTerm implements spec). Mix+selfApp alone admit a trivial residualizer; Nontrivial is a separate obligation. Jones–Gomard–Sestoft 1993 polyvariant offline mix remains open.
We prove the three Futamura projections in this mix formulation.
Mix equation at the substitution layer: specializing then substituting dynamic data equals substituting the full environment, under a coherence hypothesis on static/dynamic environments.
Mix instantiation: evaluating the specialized specializer on source data yields the specialized interpreter. Holds for any PESetup; does not by itself give a compiler-generator of Jones–Gomard–Sestoft quality.
Self-application mix instantiation: evaluating specTerm specialized to itself yields a compiler generator at the mix-equation level. Online JGS_PE covers the IStep signature; 1993 polyvariant cogen remains open.
7.1.1 System Generation vs. Compilation
It is important to distinguish the ontological role of the ISAR kernel from the epistemological role of the Futamura projections. - ISAR Kernel (\(U(K) = I \cdot R \cdot A \cdot S\)): Acts as a **System Generator**. It creates the computational substrate itself, establishing the tensor manifold in which computation exists and from which operators (norm, app, composition) emerge constructively. - Futamura Kernel (\(I \times S \times A\)): Acts as a **Compiler Generator**. It operates within an established space to transform program representations (interpreter \(\to \) compiler).
7.2 Dialect Isomorphisms and Unification
We formalize structural unifications and observational equivalence between different dialects.
An observational isomorphism between two dialects \(D_1\) and \(D_2\) is a pair of maps between their objects preserving the evaluation and coding semantics.
A dialect packaged with its admissibility proofs, allowing it to induce a semantic kernel.
An observational isomorphism between two admissible dialects induces an isomorphism between their corresponding semantic kernels in the category of kernels.
7.3 Referential Openness and Anchor Dependency
We analyze systems that are operationally closed versus referentially open (anchor-dependent).
A standard operationally closed autonomous transition system.
If a state-space subset \(C\) is closed under the step relation (forward invariant), any state reachable from \(C\) remains in \(C\).
This applies to closed computational models (combinator engines, lambda calculus, stack VMs, set theory interpreters) where the state alone is sufficient to reconstruct the semantics at any step.
A referentially open transition system whose transitions depend on an external environment context (anchor).
If a state can lead to different observations under different anchor sequences, the semantics cannot be resolved from the state alone without environmental anchors.
This establishes the boundary of decodability (the “Reverse Rosetta” problem). For open systems like natural language or undeciphered scripts (e.g., Linear A), analyzing syntax is insufficient to decode meaning because the external semantic anchors are lost. Thus, referentially open systems cannot be reconstructed from syntactic relationships alone.