2 Core Combinatory Calculus

In this chapter, we formalize the syntax, reduction semantics, and computational properties of the ISAR combinatory logic kernel. The core ISAR calculus is a substrate-independent combinator system that supports S-K combinator reductions, parallel reductions, complete developments, and normalization.

2.1 Syntax and Reduction Semantics

The definitions and operational behavior described in this section are mechanically verified in src/ISAR/Kernel.lean. The syntax consists of standard S-K combinators and the specialized ISAR terms.

Definition 1 S-K Term Syntax

The inductive type of basic S-K combinator expressions is defined by:

\begin{align*} t, u \in \text{SK} & ::= \mathbf{S} \mid \mathbf{K} \mid t\ u \end{align*}

Definition 2 ISAR Term Syntax

The core term syntax of the ISAR kernel extends basic combinators with norms, constants, and custom operations:

\begin{align*} t, u \in \text{ITerm} & ::= \mathbf{var}\ n \mid \mathbf{norm} \mid \mathbf{konst} \mid \mathbf{dup} \mid \mathbf{swap} \mid \mathbf{comp} \mid \mathbf{s_s} \mid \mathbf{app}\ t\ u \end{align*}

where \(\mathbf{app}\ t\ u\) denotes term application (also written \(t \cdot u\)).

We define the reduction rules for both systems.

Definition 3 SKStep Reduction

The reduction relation on SK terms represents the standard combinatory logic reduction rules:

\(\mathbf{K}\ x\ y \to x\)
\(\mathbf{S}\ x\ y\ z \to (x\ z)(y\ z)\)

Definition 4 IStep Reduction

The single-step reduction relation on ISAR terms defines the operational semantics of norms and constants. The reduction rules (\(\to _I\)) are:

\(\mathbf{norm} \cdot x \to _I x\)
\(\mathbf{konst} \cdot x \cdot y \to _I x\)
\(\mathbf{comp} \cdot f \cdot g \cdot x \to _I f \cdot (g \cdot x)\)
\(\mathbf{s_s} \cdot x \cdot y \cdot z \to _I (x \cdot z) \cdot (y \cdot z)\)

together with congruence rules for application:

\[ \frac{f \to _I f'}{f \cdot x \to _I f' \cdot x} \qquad \frac{x \to _I x'}{f \cdot x \to _I f \cdot x'} \]

The relation \(\twoheadrightarrow _I\) (denoted IRed) is the reflexive-transitive closure of IStep.

2.2 Parallel Reduction and Confluence

The parallel reduction relation, Takahashi’s Lemma, and the confluence theorems are formalized and proved in src/ISAR/Kernel.lean. To prove confluence, we define the parallel reduction relation ParStep (\(\Rightarrow \)), which allows simultaneous contractions of multiple redexes in a single step:

Definition 5 Parallel Step

The parallel reduction relation is defined inductively by:

\(x \Rightarrow x\)
\(\mathbf{norm} \cdot x \Rightarrow x'\) if \(x \Rightarrow x'\)
\(\mathbf{konst} \cdot x \cdot y \Rightarrow x'\) if \(x \Rightarrow x'\) and \(y \Rightarrow y'\)
\(\mathbf{comp} \cdot f \cdot g \cdot x \Rightarrow f' \cdot (g' \cdot x')\) if \(f \Rightarrow f'\), \(g \Rightarrow g'\), \(x \Rightarrow x'\)
\(\mathbf{s_s} \cdot x \cdot y \cdot z \Rightarrow (x' \cdot z') \cdot (y' \cdot z')\) if \(x \Rightarrow x'\), \(y \Rightarrow y'\), \(z \Rightarrow z'\)
\(f \cdot x \Rightarrow f' \cdot x'\) if \(f \Rightarrow f'\) and \(x \Rightarrow x'\)

Theorem 1 Takahashi’s Lemma

If \(x \Rightarrow y\), then \(y \Rightarrow \text{cd}(x)\), where \(\text{cd}\) is the complete development function.

Theorem 2 Confluence of IRed

The reduction relation \(\text{IRed}\) satisfies the Church-Rosser confluence property:

\[ \forall t, u_1, u_2, \quad t \to ^* u_1 \land t \to ^* u_2 \implies \exists v, \quad u_1 \to ^* v \land u_2 \to ^* v \]

Theorem 3 Unique Normal Forms

If a term \(t\) reduces to two normal forms \(n_1\) and \(n_2\), then \(n_1 = n_2\).

2.3 Conservative Basis Translation

The derived combinator simulation and conservative translation are verified in src/ISAR/Kernel.lean. The distributive combinator \(s_s\) is not strictly necessary for the rewrite algebra. We constructively define the derived S combinator as:

\begin{align*} \text{derived\_ s} & \triangleq (\mathbf{comp} \cdot (\mathbf{comp} \cdot \mathbf{dup})) \\ & \quad \cdot \big((\mathbf{swap} \cdot ((\mathbf{comp} \cdot \mathbf{comp}) \cdot ((\mathbf{comp} \cdot \mathbf{comp}) \cdot \mathbf{swap}))) \cdot \mathbf{norm}\big) \end{align*}

Theorem 4 Derived S reduction

The derived S combinator simulates the beta-reduction rule of \(S\) using only the basis operators (without \(s_s\)):

\[ \text{derived\_ s} \cdot x \cdot y \cdot z \twoheadrightarrow _{I_{basis}} (x \cdot z) \cdot (y \cdot z) \]

Theorem 5 Conservative Translation

The translation map translate_to_basis (which replaces \(s_s\) with derived_s) preserves reduction steps.

2.4 The Invariant Layer

The operational quotient and application congruence are formalized and proved in src/ISAR/InvariantLayer.lean. Using the uniqueness of normal forms, we define the quotient space representing behavioral equivalence classes of terms.

Definition 6 ISKSubtype

The subtype of ISAR terms belonging to the S-K fragment:

\[ \text{ISKSubtype} := \{ t : \text{ITerm} \mid \text{ISKTerm } t \} \]

Definition 7 Operational Equivalence

Two terms are operationally equivalent if they behave identically under reduction:

\[ t \sim _{op} u \iff \text{OperEq } t\ u \]

Definition 8 Invariant Layer

The quotient type of ISKSubtype modulo OperEq:

\[ \text{InvariantLayer} := \text{Quotient } (\text{operEqSetoid}) \]

Definition 9 Invariant Layer Application

The application operator lifted to the quotient space:

\[ \text{app} : \text{InvariantLayer} \to \text{InvariantLayer} \to \text{InvariantLayer} \]

Definition 10 Canonical Representative

A noncomputable function mapping each equivalence class to its canonical representative in ISKSubtype.

2.5 Linear Duplication and Computable Normalization

Local duplication counts, size-decrease properties of complete development, and fuel correctness are verified in src/ISAR/Kernel.lean and src/ISAR/InvariantLayer.lean. We define the linear duplication fragment LinearIKTerm and its termination metrics, which share a direct isomorphism with linear interaction nets.

Definition 11 Linear Duplication

The function dupCount tracks the duplication multiplicity of a term. For the linear fragment LinearIKTerm, we verify that duplication is strictly localized:

\[ \text{dupCount } t = 0 \]

We prove that complete development (cd) strictly decreases term size for all non-fixed-point linear terms.

Theorem 6 Complete Development Size Decrease

For any term \(t\) in the LinearIKTerm fragment:

\[ \text{term\_ size}(\text{cd } t) \leq \text{term\_ size}(t) \]

And if \(t \neq \text{cd } t\), the inequality is strict.

Definition 12 Computable Normalization Loop

A fuel-based normalization loop that computes the normal form.

Theorem 7 Fuel Correctness

The optimal fuel limit computed from the term size is sufficient to guarantee complete normalization at runtime.