4 Symbolic Views and Dialects

The ISAR architecture supports multiple symbolic views or “dialects” over the representation-free substrate. Each view compiles to the substrate and decodes back, satisfying a preservation law. In this chapter, we formalize several dialects: the Lambda calculus fragment, ZFC hereditarily finite sets, term rewriting systems, bytecode compilation, and Barker’s Iota combinator.

4.1 The Lambda Calculus Fragment

The bracket abstraction compiler and simulation properties in this section are mechanically verified in src/ISAR/LambdaFragment.lean. We define the standard \(\lambda \)-calculus with de Bruijn indices.

Definition 20 Lambda Terms

Lambda terms with variables (represented by natural number de Bruijn indices), applications, and abstractions:

\begin{align*} t, u \in \text{LTerm} & ::= \mathbf{var}\ n \mid \mathbf{app}\ t\ u \mid \mathbf{lam}\ t \end{align*}

Definition 21 Lambda Step

Single-step \(\beta \)-reduction on LTerm using de Bruijn shifts and substitutions.

Definition 22 Lambda Compiler

Compiles lambda terms into the ISAR substrate via bracket abstraction:

\[ \text{compile} : \text{LTerm} \to \text{ITerm} \]

Theorem 10 Compiler Simulation

The compiler faithfully simulates lambda reductions in the ISAR kernel:

\[ \forall t, u \in \text{LTerm}, \quad t \to _\beta u \implies \text{compile } t \to ^* \text{compile } u \]

4.2 Hereditarily Finite Sets and ZFC

The set-theoretic encoding and relative ZFC interpretation verified in this section are mechanically verified in src/ISAR/HFSet.lean, src/ISAR/HFSetEncoding.lean, and src/ISAR/HFSetSemantics.lean. This relative interpretation is strictly limited to the Hereditarily Finite (HF) set fragment (ZFC without the axiom of infinity). We formalize HF Sets, their encoding, and show they satisfy set-theoretic axioms.

Definition 23 HF Sets

The type of hereditarily finite sets, built inductively from the empty set:

\[ x, y \in \text{HF} ::= \emptyset \mid x \cup \{ y\} \]

Definition 24 Extensional Equality

Set-theoretic extensional equivalence (\(x =_{ext} y\)) defined via Ackermann’s bijective encoding ‘toNat‘:

\[ x =_{ext} y \iff \text{ExtEq } x\ y \]

Definition 25 HF Set Encoding

Encodes HF sets into substrate invariant layers:

\[ \text{HF\_ encode} : \text{HF} \to \text{InvariantLayer} \]

Theorem 11 HF Encoding Correctness

The encoding is sound and invertible:

\[ \forall c \in \text{HF}, \quad \text{decode\_ layer}(\text{HF\_ encode } c) = c \]

We package HF Sets as a semantic kernel.

Definition 26 HF Set Kernel

The set-theoretic admissible semantic kernel HF_Kernel.

Theorem 12 ZFC Interpretation Factorization

The HF set kernel factors uniquely through ISAR_Kernel:

\[ \forall f : \text{KernelHom HF\_ Kernel ISAR\_ Kernel}, \quad f(c) \sim _{op} \text{encode\_ raw } c \]

This faithful factorization proves that the ZFC HF set fragment faithfully interprets into the ISAR substrate, satisfying empty set, pairing, and union axioms.

Syntactically distinct terms representing the same set (e.g., \(\{ a, b\} \) and \(\{ b, a\} \)) project to the exact same element in the ‘InvariantLayer‘ quotient, demonstrating extensional equivalence.

4.3 Term Rewriting, Bytecode, and Iota Views

The SKI TRS view, stack bytecode compiler, and Barker’s iota dialect are verified in src/ISAR/TRSView.lean, src/ISAR/BytecodeView.lean, and src/ISAR/IotaView.lean respectively. We define dialects for other standard computational models.

Definition 27 SKI TRS Dialect

The term rewriting dialect modeling pure SKI combinator terms TTerm.

Definition 28 Bytecode Dialect

The dialect representing stack-based virtual machine instruction bytecode Instruction compiled and decompiled.

Definition 29 Barker’s Iota Dialect

The dialect modeling the single-combinator IotaTerm utilizing Barker’s universal combinator \(\iota = \lambda x. x\ S\ K\).

In Barker’s iota combinator view, iterating iota-application produces the closed orbit:

\[ I \to A \to K \to S \to X \to I \]

where:

\(I\) = identity (\(I x = x\))
\(A\) = flip constant (\(A x y = y\))
\(K\) = constant (\(K x y = x\))
\(S\) = substitution (\(S f g x = f x (g x)\))
\(X\) = self-application kernel

These four distinct active combinators map directly onto the four matrices (\(I, R, A, S\)) of the ISAR substrate, proving the ontological completeness of the 4-carrier representation.