8 Discussion, Related Work, and Limitations

We present a review of related literature, establish the formal boundaries of validity for our theorems, and outline directions for future research.

8.1 Related Work

The ISAR framework intersects several foundational areas of computer science and logic:

Combinatory Logic and Lambda Calculus: The bracket abstraction algorithm compiled to combinator form is a classical approach pioneered by Curry and Feys [ 2 ] and Barendregt [ 1 ] . While traditional implementations suffer from code size explosion (e.g., \(O(n^3)\) for standard abstraction), the linear fragment of ISAR maintains bounded sizing, sharing a direct connection to optimal reduction.
Optimal Evaluation and Interaction Nets: Yves Lafont’s interaction nets [ 6 ] provide a graphical formulation of computation where reductions are local and symmetric. Our formalization of the linear fragment (LinearIKTerm) and its bounds mirrors the behavior of optimal virtual machines like the Higher-Order Virtual Machine 2 (HVM2) [ 10 ] , which compiles terms to interaction nets for parallel execution.
Categorical Semantics of Computation: Lawvere’s functorial semantics [ 7 ] established algebraic theories as categories. Our formulation of semantic kernels (\(\mathcal{K}\)) and the proof of terminality of the Invariant Layer quotient formalizes view-independence as a universal factorization property.
Proof Assistant Kernels: The verification and automated generation of documentation utilizing Lean 4 quotients and metadata mappings (e.g., doc-gen4 [ 8 ] ) represent the state-of-the-art in proof design. Our work extends this by proving formal simulation theorems directly against the proof assistant’s environment.

The theorems presented in this work are accompanied by strict boundary conditions:

Closed Dialects Only: The terminality and factorization theorems apply exclusively to computational dialects that are operationally closed—meaning they possess a total encoding function into the substrate and their evaluation dynamics can be modeled as deterministic, confluent rewrite steps. This excludes open, dynamic, or referentially open systems (such as natural languages, interactive APIs, or non-deterministic transition systems) that require contextual anchors.
ZFC HF Set Scope: The set-theoretic relative interpretation is verified solely for the Hereditarily Finite set fragment. Extension to infinite sets (ZFC with the axiom of infinity) requires different ordinals and is outside the scope of the current Lean 4 proofs.
Interpretive Physical Assumptions: The application of the Universal Approximation Theorem to physical systems rests on the interpretive hypothesis that a physical system’s state space can be modeled as an admissible continuous kernel. This hypothesis is a modeling choice and is not mechanically verified by the Lean 4 proof assistant.

This paper forms the core substrate of a multi-part series of monographs:

Paper 2 (Continuous Approximation): Extension of the discrete kernel to real-valued physical quantities and continuous address spaces. Unique representation in a completion of KernelAddress is axiomatic (ISAR_UAT stays named; there is no metric on KernelAddress). Classical citations: Cybenko [ 3 ] and Leshno et al. [ 9 ] .
Paper 3 (Hardware Compilation): Verification of the compilation path from the algebraic matrix representations to optimal virtual machines (HVM2) and relational database schemas. We also formalize partial evaluation and dialect specialization via the first, second, and third Futamura projections [ 4 ] .