Partial evaluation and Futamura projections

Honest formulation (Jones/Gomard/Sestoft): the three projections follow from the mix equation once the specializer is reflected as an object-level term (specTerm) with selfApp. Mix alone admits a trivial specializer; nontriviality is a separate obligation.

def ISAR.subst_env (t : ITerm) (env : Nat → ITerm) : ITerm

Substitution function replacing variables with terms.

Equations

• ISAR.subst_env (ISAR.ITerm.var n) env = env n
• ISAR.subst_env ISAR.ITerm.norm env = ISAR.ITerm.norm
• ISAR.subst_env ISAR.ITerm.konst env = ISAR.ITerm.konst
• ISAR.subst_env ISAR.ITerm.dup env = ISAR.ITerm.dup
• ISAR.subst_env ISAR.ITerm.swap env = ISAR.ITerm.swap
• ISAR.subst_env ISAR.ITerm.comp env = ISAR.ITerm.comp
• ISAR.subst_env ISAR.ITerm.sₛ env = ISAR.ITerm.sₛ
• ISAR.subst_env (f · x) env = ISAR.subst_env f env · ISAR.subst_env x env

def ISAR.specialize (t : ITerm) (static_env : Nat → Option ITerm) : ITerm

Meta-level specializer (partial evaluator) replacing static variables.

Equations

• ISAR.specialize (ISAR.ITerm.var n) static_env = match static_env n with | some val => val | none => ISAR.ITerm.var n
• ISAR.specialize ISAR.ITerm.norm static_env = ISAR.ITerm.norm
• ISAR.specialize ISAR.ITerm.konst static_env = ISAR.ITerm.konst
• ISAR.specialize ISAR.ITerm.dup static_env = ISAR.ITerm.dup
• ISAR.specialize ISAR.ITerm.swap static_env = ISAR.ITerm.swap
• ISAR.specialize ISAR.ITerm.comp static_env = ISAR.ITerm.comp
• ISAR.specialize ISAR.ITerm.sₛ static_env = ISAR.ITerm.sₛ
• ISAR.specialize (f · x) static_env = ISAR.specialize f static_env · ISAR.specialize x static_env

def ISAR.pair (s d : ITerm) : ITerm

Pairing of terms as a binary application spine.

Equations

• ISAR.pair s d = ISAR.ITerm.konst · s · d

def ISAR.Coherent (env : Nat → ITerm) (static_env : Nat → Option ITerm) (dynamic_env : Nat → ITerm) : Prop

Coherence condition relating full environment and partial environments.

Equations

• One or more equations did not get rendered due to their size.

theorem ISAR.subst_env_preserves_step {t u : ITerm} (env : Nat → ITerm) (h : IStep t u) : IStep (subst_env t env) (subst_env u env)

theorem ISAR.subst_env_preserves_red {t u : ITerm} (env : Nat → ITerm) (h : IRed t u) : IRed (subst_env t env) (subst_env u env)

theorem ISAR.futamura_first (t : ITerm) (env : Nat → ITerm) (static_env : Nat → Option ITerm) (dynamic_env : Nat → ITerm) (h_coh : Coherent env static_env dynamic_env) : subst_env (specialize t static_env) dynamic_env = subst_env t env

Mix equation at the subst layer (first Futamura projection / specialization soundness).

structure ISAR.PESetup : Type

Setup for object-level Futamura projections. spec is the meta specializer; specTerm is its reflection as an ITerm; mix is the characterizing equation; selfApp says evaluating specTerm implements spec.

TrivialPE is a sorry-free non-optimizing instance (¬ Nontrivial, ¬ JonesOptimal). OptimizingPE is a sorry-free fragment specializer with proved Nontrivial (identity / konstβ folds + tagged residual fallback). JGS_PE is online PE for the whole IStep signature (Nontrivial, ¬ JonesOptimal). Jones-optimality is the cost criterion (JonesOptimal); a toy self-interpreter pair JonesIdPE meets it. Full Jones–Gomard–Sestoft 1993 polyvariant BTA / cogen remains open; specTerm is still swap, not an encoding of jgs_spec / offline_spec. The projections below are the mix instantiations.

• eval : ITerm → ITerm → Option ITerm
• spec : ITerm → ITerm → ITerm
• specTerm : ITerm
• mix (p s d : ITerm) : self.eval (self.spec p s) d = self.eval p (pair s d)
• selfApp (p s : ITerm) : self.eval self.specTerm (pair p s) = some (self.spec p s)

theorem ISAR.futamura_second (S : PESetup) (int src : ITerm) : S.eval (S.spec S.specTerm int) src = some (S.spec int src)

Second Futamura projection: specializing the specializer w.r.t. an interpreter.

theorem ISAR.futamura_third (S : PESetup) (int : ITerm) : S.eval (S.spec S.specTerm S.specTerm) int = some (S.spec S.specTerm int)

Third Futamura projection: self-application yields a compiler generator.

def ISAR.pe_cost : ITerm → Nat

Cost measure for nontriviality (term size).

Equations

• ISAR.pe_cost = ISAR.term_size

theorem ISAR.term_size_pos (t : ITerm) : 1 ≤ term_size t

def ISAR.Nontrivial (S : PESetup) : Prop

Nontriviality: specialization strictly reduces cost on some nonempty class of programs. Without this, mix+selfApp alone are satisfied by residualizers that do no optimization (e.g. the identity residualizer spec p s = p).

Equations

• ISAR.Nontrivial S = ∃ (p : ISAR.ITerm), ∃ (s : ISAR.ITerm), ISAR.pe_cost (S.spec p s) < ISAR.pe_cost p

def ISAR.SelfInterpreter (S : PESetup) (int : ITerm) : Prop

Self-interpreter: running int on (src, d) agrees with running src on d.

Equations

• ISAR.SelfInterpreter S int = ∀ (src d : ISAR.ITerm), S.eval int (ISAR.pair src d) = S.eval src d

def ISAR.JonesOptimal (S : PESetup) : Prop

Jones-optimality (Neil Jones): some self-interpreter specializes to a residual no more expensive than the source, for every source. Cost/pe_cost form matches Nontrivial. This is not 1993 polyvariant mix / compiler-generator quality; specTerm is not an encoding of jgs_spec or offline_spec.

Equations

• ISAR.JonesOptimal S = ∃ (int : ISAR.ITerm), ISAR.SelfInterpreter S int ∧ ∀ (src : ISAR.ITerm), ISAR.pe_cost (S.spec int src) ≤ ISAR.pe_cost src

def ISAR.identity_spec (p _s : ITerm) : ITerm

Identity residualizer (ignores static data). Cost-vacuous, but cannot be packaged as PESetup with eval prog _ := some prog: selfApp forces specTerm to behave like a realizer, colliding when programs can equal specTerm.

Equations

• ISAR.identity_spec p _s = p

theorem ISAR.identity_spec_mix (p s d : ITerm) : some (identity_spec p s) = some p

theorem ISAR.identity_spec_not_shrinking : ¬∃ (p : ITerm), ∃ (s : ITerm), pe_cost (identity_spec p s) < pe_cost p

Vacuity witness: identity residualization never shrinks under pe_cost.

Principled trivial PESetup (tagged residual, recursive unpack)

Identity spec cannot satisfy selfApp for a universal eval prog _ := some prog. Instead residualize under a dup tag and reflect the specializer as bare swap. Evaluation recursively unpacks residuals so mix holds for all p (including when p is itself tagged); selfApp is the swap clause. Cost never shrinks, so ¬ Nontrivial. A real self-applicable optimizing specTerm / BTA remains future work.

def ISAR.trivial_spec (p s : ITerm) : ITerm

Tagged residual: dup · (pair p s). Strictly larger than p under pe_cost.

Equations

• ISAR.trivial_spec p s = ISAR.ITerm.dup · ISAR.pair p s

def ISAR.trivial_run : ITerm → ITerm → ITerm

Object-level evaluator for the toy specializer.

• swap on pair p s returns the tagged residual (selfApp).
• A tagged residual applied to dynamic d continues as run p (pair s d) (mix), recursively, so residual-shaped programs do not break the mix equation.
• Otherwise return the syntactic application.

Equations

• ISAR.trivial_run ISAR.ITerm.swap (ISAR.ITerm.konst · p · s) = ISAR.trivial_spec p s
• ISAR.trivial_run ISAR.ITerm.swap x✝ = ISAR.ITerm.swap · x✝
• ISAR.trivial_run (ISAR.ITerm.dup · (ISAR.ITerm.konst · p · s)) x✝ = ISAR.trivial_run p (ISAR.pair s x✝)
• ISAR.trivial_run x✝¹ x✝ = x✝¹ · x✝

def ISAR.trivial_eval (prog data : ITerm) : Option ITerm

Equations

• ISAR.trivial_eval prog data = some (ISAR.trivial_run prog data)

theorem ISAR.trivial_mix (p s d : ITerm) : trivial_eval (trivial_spec p s) d = trivial_eval p (pair s d)

theorem ISAR.trivial_selfApp (p s : ITerm) : trivial_eval ITerm.swap (pair p s) = some (trivial_spec p s)

def ISAR.TrivialPE : PESetup

Toy PESetup: mix and selfApp by rfl; residualizer is cost-non-shrinking.

Equations

• ISAR.TrivialPE = { eval := ISAR.trivial_eval, spec := ISAR.trivial_spec, specTerm := ISAR.ITerm.swap, mix := ISAR.trivial_mix, selfApp := ISAR.trivial_selfApp }

theorem ISAR.pe_cost_trivial_spec (p s : ITerm) : pe_cost (trivial_spec p s) = pe_cost p + pe_cost s + 5

theorem ISAR.trivial_spec_not_shrinking : ¬∃ (p : ITerm), ∃ (s : ITerm), pe_cost (trivial_spec p s) < pe_cost p

theorem ISAR.TrivialPE_not_nontrivial : ¬Nontrivial TrivialPE

Mix+selfApp alone do not imply optimization: TrivialPE is not Nontrivial.

theorem ISAR.trivial_run_result_konst_norm (n : Nat) (p d : ITerm) : term_size p ≤ n → trivial_run p d = ITerm.konst · ITerm.norm → p = ITerm.konst ∧ d = ITerm.norm

trivial_run returns konst · norm only by the default clause on those atoms.

theorem ISAR.TrivialPE_not_self_interpreter (int : ITerm) : ¬SelfInterpreter TrivialPE int

theorem ISAR.TrivialPE_not_jonesOptimal : ¬JonesOptimal TrivialPE

Tagged residuals are strictly larger than the source, so no self-interpreter can meet the Jones cost bound either — TrivialPE is not Jones-optimal.

Toy Jones-optimal pair (identity interpreter, not 1993 mix)

norm as a degenerate self-interpreter: running it on (src, d) continues as src on d. Specializing that interpreter copies the source (spec norm src = src), so the Jones cost bound holds with equality. Mix/selfApp still use tagged residuals for every other program. This is a cost-criterion toy, not a 1993 compiler-generator.

def ISAR.jones_spec (p s : ITerm) : ITerm

Equations

• ISAR.jones_spec p s = if p = ISAR.ITerm.norm then s else ISAR.trivial_spec p s

@[irreducible]

def ISAR.jones_run : ITerm → ITerm → ITerm

Equations

• ISAR.jones_run ISAR.ITerm.swap (ISAR.ITerm.konst · p · s) = ISAR.jones_spec p s
• ISAR.jones_run ISAR.ITerm.swap x✝ = ISAR.ITerm.swap · x✝
• ISAR.jones_run (ISAR.ITerm.dup · (ISAR.ITerm.konst · p · s)) x✝ = ISAR.jones_run p (ISAR.pair s x✝)
• ISAR.jones_run ISAR.ITerm.norm (ISAR.ITerm.konst · p · s) = ISAR.jones_run p s
• ISAR.jones_run ISAR.ITerm.norm x✝ = ISAR.ITerm.norm · x✝
• ISAR.jones_run x✝¹ x✝ = x✝¹ · x✝

def ISAR.jones_eval (prog data : ITerm) : Option ITerm

Equations

• ISAR.jones_eval prog data = some (ISAR.jones_run prog data)

theorem ISAR.jones_mix (p s d : ITerm) : jones_eval (jones_spec p s) d = jones_eval p (pair s d)

theorem ISAR.jones_selfApp (p s : ITerm) : jones_eval ITerm.swap (pair p s) = some (jones_spec p s)

def ISAR.JonesIdPE : PESetup

Equations

• ISAR.JonesIdPE = { eval := ISAR.jones_eval, spec := ISAR.jones_spec, specTerm := ISAR.ITerm.swap, mix := ISAR.jones_mix, selfApp := ISAR.jones_selfApp }

theorem ISAR.JonesIdPE_self_interpreter_norm : SelfInterpreter JonesIdPE ITerm.norm

theorem ISAR.JonesIdPE_jonesOptimal : JonesOptimal JonesIdPE

Optimizing fragment PE (identity / konstβ folding)

Not a full Jones–Gomard–Sestoft BTA for all of ISAR. This is a principled optimizing specializer on a fragment:

• Peel norm · body (identity elimination) and (konst · x) · y (konstβ / dead elim).
• Atomic combinators (except swap, reserved as specTerm) residualize to themselves.
• Remaining programs get a dup-tagged residual (same packaging as TrivialPE).

mix / selfApp hold by computation on this evaluator; Nontrivial is witnessed by stripping a norm redex. Full self-applicable optimizing mix for the whole calculus remains dissertation-scale future work.

def ISAR.opt_spec (p s : ITerm) : ITerm

Meta specializer with static identity / konstβ folds.

Equations

• ISAR.opt_spec (ISAR.ITerm.norm · body) s = ISAR.opt_spec body s
• ISAR.opt_spec (ISAR.ITerm.konst · x · _y) s = ISAR.opt_spec x s
• ISAR.opt_spec ISAR.ITerm.norm s = ISAR.ITerm.norm
• ISAR.opt_spec ISAR.ITerm.konst s = ISAR.ITerm.konst
• ISAR.opt_spec ISAR.ITerm.sₛ s = ISAR.ITerm.sₛ
• ISAR.opt_spec ISAR.ITerm.dup s = ISAR.ITerm.dup
• ISAR.opt_spec ISAR.ITerm.comp s = ISAR.ITerm.comp
• ISAR.opt_spec (ISAR.ITerm.var n) s = ISAR.ITerm.var n
• ISAR.opt_spec p s = ISAR.ITerm.dup · ISAR.pair p s

def ISAR.opt_run : ITerm → ITerm → ITerm

Object-level evaluator matching opt_spec:

• swap on pair p s implements selfApp.
• Tagged residuals unpack via mix.
• Program-position norm / konstβ peels mirror opt_spec.
• Atomic values are data-insensitive (so constant residuals satisfy mix).

Equations

• ISAR.opt_run ISAR.ITerm.swap (ISAR.ITerm.konst · p · s) = ISAR.opt_spec p s
• ISAR.opt_run ISAR.ITerm.swap x✝ = ISAR.ITerm.swap · x✝
• ISAR.opt_run (ISAR.ITerm.dup · (ISAR.ITerm.konst · p · s)) x✝ = ISAR.opt_run p (ISAR.pair s x✝)
• ISAR.opt_run (ISAR.ITerm.norm · body) x✝ = ISAR.opt_run body x✝
• ISAR.opt_run (ISAR.ITerm.konst · x_2 · _y) x✝ = ISAR.opt_run x_2 x✝
• ISAR.opt_run ISAR.ITerm.norm x✝ = ISAR.ITerm.norm
• ISAR.opt_run ISAR.ITerm.konst x✝ = ISAR.ITerm.konst
• ISAR.opt_run ISAR.ITerm.sₛ x✝ = ISAR.ITerm.sₛ
• ISAR.opt_run ISAR.ITerm.dup x✝ = ISAR.ITerm.dup
• ISAR.opt_run ISAR.ITerm.comp x✝ = ISAR.ITerm.comp
• ISAR.opt_run (ISAR.ITerm.var n) x✝ = ISAR.ITerm.var n
• ISAR.opt_run x✝¹ x✝ = x✝¹ · x✝

def ISAR.opt_eval (prog data : ITerm) : Option ITerm

Equations

• ISAR.opt_eval prog data = some (ISAR.opt_run prog data)

theorem ISAR.opt_mix (p s d : ITerm) : opt_eval (opt_spec p s) d = opt_eval p (pair s d)

theorem ISAR.opt_selfApp (p s : ITerm) : opt_eval ITerm.swap (pair p s) = some (opt_spec p s)

def ISAR.OptimizingPE : PESetup

Optimizing fragment PESetup: mix/selfApp by induction/rfl; Nontrivial below.

Equations

• ISAR.OptimizingPE = { eval := ISAR.opt_eval, spec := ISAR.opt_spec, specTerm := ISAR.ITerm.swap, mix := ISAR.opt_mix, selfApp := ISAR.opt_selfApp }

def ISAR.opt_witness_p : ITerm

Witness program: norm · konst strips to konst.

Equations

• ISAR.opt_witness_p = ISAR.ITerm.norm · ISAR.ITerm.konst

theorem ISAR.opt_spec_norm_konst (s : ITerm) : opt_spec opt_witness_p s = ITerm.konst

theorem ISAR.pe_cost_opt_witness (s : ITerm) : pe_cost (opt_spec opt_witness_p s) < pe_cost opt_witness_p

theorem ISAR.OptimizingPE_nontrivial : Nontrivial OptimizingPE

Jones–Gomard–Sestoft online PE for the whole IStep signature

Offline BTA classifies subterms; online PE is the 1985 mix technique once every object-language redex can fire at specialization time. ISAR's object reductions are exactly normβ, konstβ, compβ, sβ. This specializer folds all four.

• Size-decreasing folds (norm, konst, comp) recurse.
• sβ can grow term_size; we unfold once into a tagged residual (no recursion).
• swap remains specTerm. Polyvariant offline mix that generates a compiler-generator of Jones–Gomard–Sestoft 1993 quality is still open; the object-language signature is covered.

inductive ISAR.BindingTime : Type

Offline binding-time sketch: swap is the dynamic hole; other atoms are static; application is static iff both sides are. Monovariant: no call strings, no program-point splitting. Unused by jgs_spec (online PE). Lemmas below relate bta to specialization; they do not give 1993 polyvariant mix.

• static : BindingTime
• dynamic : BindingTime

@[implicit_reducible]

instance ISAR.instDecidableEqBindingTime : DecidableEq BindingTime

Equations

• ISAR.instDecidableEqBindingTime x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ISAR.instReprBindingTime : Repr BindingTime

Equations

• ISAR.instReprBindingTime = { reprPrec := ISAR.instReprBindingTime.repr }

def ISAR.instReprBindingTime.repr : BindingTime → Nat → Std.Format

Equations

• ISAR.instReprBindingTime.repr ISAR.BindingTime.static prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.BindingTime.static")).group prec✝
• ISAR.instReprBindingTime.repr ISAR.BindingTime.dynamic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.BindingTime.dynamic")).group prec✝

def ISAR.bta : ITerm → BindingTime

Equations

• ISAR.bta ISAR.ITerm.swap = ISAR.BindingTime.dynamic
• ISAR.bta (f · x_1) = match ISAR.bta f, ISAR.bta x_1 with | ISAR.BindingTime.static, ISAR.BindingTime.static => ISAR.BindingTime.static | x, x_2 => ISAR.BindingTime.dynamic
• ISAR.bta x✝ = ISAR.BindingTime.static

def ISAR.containsSwap : ITerm → Bool

Equations

• ISAR.containsSwap ISAR.ITerm.swap = true
• ISAR.containsSwap (f · x_1) = (ISAR.containsSwap f || ISAR.containsSwap x_1)
• ISAR.containsSwap x✝ = false

theorem ISAR.bta_swap : bta ITerm.swap = BindingTime.dynamic

theorem ISAR.bta_norm : bta ITerm.norm = BindingTime.static

theorem ISAR.bta_konst : bta ITerm.konst = BindingTime.static

theorem ISAR.bta_dup : bta ITerm.dup = BindingTime.static

theorem ISAR.bta_comp : bta ITerm.comp = BindingTime.static

theorem ISAR.bta_s : bta ITerm.sₛ = BindingTime.static

theorem ISAR.bta_var (n : Nat) : bta (ITerm.var n) = BindingTime.static

theorem ISAR.bta_app_static (f x : ITerm) : bta (f · x) = BindingTime.static ↔ bta f = BindingTime.static ∧ bta x = BindingTime.static

theorem ISAR.bta_eq_dynamic_iff_containsSwap (t : ITerm) : bta t = BindingTime.dynamic ↔ containsSwap t = true

@[irreducible]

def ISAR.jgs_spec : ITerm → ITerm → ITerm

Online specializer covering every IStep constructor.

Equations

• ISAR.jgs_spec (ISAR.ITerm.norm · body) x✝ = ISAR.jgs_spec body x✝
• ISAR.jgs_spec (ISAR.ITerm.konst · x_2 · _y) x✝ = ISAR.jgs_spec x_2 x✝
• ISAR.jgs_spec (ISAR.ITerm.comp · f · g · x_2) x✝ = ISAR.jgs_spec (f · (g · x_2)) x✝
• ISAR.jgs_spec (ISAR.ITerm.sₛ · x_2 · y · z) x✝ = ISAR.ITerm.var 0 · ISAR.pair (x_2 · z · (y · z)) x✝
• ISAR.jgs_spec ISAR.ITerm.norm x✝ = ISAR.ITerm.norm
• ISAR.jgs_spec ISAR.ITerm.konst x✝ = ISAR.ITerm.konst
• ISAR.jgs_spec ISAR.ITerm.sₛ x✝ = ISAR.ITerm.sₛ
• ISAR.jgs_spec ISAR.ITerm.dup x✝ = ISAR.ITerm.dup
• ISAR.jgs_spec ISAR.ITerm.comp x✝ = ISAR.ITerm.comp
• ISAR.jgs_spec (ISAR.ITerm.var n) x✝ = ISAR.ITerm.var n
• ISAR.jgs_spec x✝¹ x✝ = ISAR.ITerm.dup · ISAR.pair x✝¹ x✝

theorem ISAR.jgs_spec_norm (s : ITerm) : jgs_spec ITerm.norm s = ITerm.norm

theorem ISAR.jgs_spec_konst (s : ITerm) : jgs_spec ITerm.konst s = ITerm.konst

theorem ISAR.jgs_spec_comp_atom (s : ITerm) : jgs_spec ITerm.comp s = ITerm.comp

theorem ISAR.jgs_spec_s_atom (s : ITerm) : jgs_spec ITerm.sₛ s = ITerm.sₛ

theorem ISAR.jgs_spec_static_atom_independent (s₁ s₂ : ITerm) : jgs_spec ITerm.norm s₁ = jgs_spec ITerm.norm s₂ ∧ jgs_spec ITerm.konst s₁ = jgs_spec ITerm.konst s₂ ∧ jgs_spec ITerm.comp s₁ = jgs_spec ITerm.comp s₂ ∧ jgs_spec ITerm.sₛ s₁ = jgs_spec ITerm.sₛ s₂ ∧ jgs_spec ITerm.dup s₁ = jgs_spec ITerm.dup s₂

@[irreducible]

def ISAR.offline_spec : ITerm → ITerm → ITerm

Monovariant offline specializer: fold a redex only when bta classifies the whole redex as static. Static S unfolds once into a residual with no s tag (no recursion — size may grow). Dynamic terms are tagged residuals. This is still monovariant (one division). It is not 1993 polyvariant mix.

Equations

• One or more equations did not get rendered due to their size.
• ISAR.offline_spec ISAR.ITerm.norm x✝ = ISAR.ITerm.norm
• ISAR.offline_spec ISAR.ITerm.konst x✝ = ISAR.ITerm.konst
• ISAR.offline_spec ISAR.ITerm.sₛ x✝ = ISAR.ITerm.sₛ
• ISAR.offline_spec ISAR.ITerm.dup x✝ = ISAR.ITerm.dup
• ISAR.offline_spec ISAR.ITerm.comp x✝ = ISAR.ITerm.comp
• ISAR.offline_spec (ISAR.ITerm.var n) x✝ = ISAR.ITerm.var n
• ISAR.offline_spec x✝¹ x✝ = if ISAR.bta x✝¹ = ISAR.BindingTime.static then x✝¹ else ISAR.ITerm.dup · ISAR.pair x✝¹ x✝

theorem ISAR.offline_spec_static_atom_independent (s₁ s₂ : ITerm) : offline_spec ITerm.norm s₁ = offline_spec ITerm.norm s₂ ∧ offline_spec ITerm.konst s₁ = offline_spec ITerm.konst s₂ ∧ offline_spec ITerm.comp s₁ = offline_spec ITerm.comp s₂ ∧ offline_spec ITerm.sₛ s₁ = offline_spec ITerm.sₛ s₂ ∧ offline_spec ITerm.dup s₁ = offline_spec ITerm.dup s₂

theorem ISAR.offline_spec_I_static (body s₁ s₂ : ITerm) (ht : bta (ITerm.norm · body) = BindingTime.static) : offline_spec (ITerm.norm · body) s₁ = offline_spec body s₁

theorem ISAR.offline_spec_K_static (x y s₁ : ITerm) (ht : bta (ITerm.konst · x · y) = BindingTime.static) : offline_spec (ITerm.konst · x · y) s₁ = offline_spec x s₁

theorem ISAR.offline_spec_B_static (f g x s₁ : ITerm) (ht : bta (ITerm.comp · f · g · x) = BindingTime.static) : offline_spec (ITerm.comp · f · g · x) s₁ = offline_spec (f · (g · x)) s₁

theorem ISAR.offline_spec_S_static (x y z s₁ s₂ : ITerm) (ht : bta (ITerm.sₛ · x · y · z) = BindingTime.static) : offline_spec (ITerm.sₛ · x · y · z) s₁ = offline_spec (ITerm.sₛ · x · y · z) s₂

@[irreducible]

def ISAR.jgs_run : ITerm → ITerm → ITerm

Equations

• ISAR.jgs_run ISAR.ITerm.swap (ISAR.ITerm.konst · p · s) = ISAR.jgs_spec p s
• ISAR.jgs_run ISAR.ITerm.swap x✝ = ISAR.ITerm.swap · x✝
• ISAR.jgs_run (ISAR.ITerm.dup · (ISAR.ITerm.konst · p · s)) x✝ = ISAR.jgs_run p (ISAR.pair s x✝)
• ISAR.jgs_run (ISAR.ITerm.norm · body) x✝ = ISAR.jgs_run body x✝
• ISAR.jgs_run (ISAR.ITerm.konst · x_2 · _y) x✝ = ISAR.jgs_run x_2 x✝
• ISAR.jgs_run (ISAR.ITerm.comp · f · g · x_2) x✝ = ISAR.jgs_run (f · (g · x_2)) x✝
• ISAR.jgs_run (ISAR.ITerm.var 0 · (ISAR.ITerm.konst · c · s)) x✝ = c · ISAR.pair s x✝
• ISAR.jgs_run (ISAR.ITerm.sₛ · x_2 · y · z) x✝ = x_2 · z · (y · z) · x✝
• ISAR.jgs_run ISAR.ITerm.norm x✝ = ISAR.ITerm.norm
• ISAR.jgs_run ISAR.ITerm.konst x✝ = ISAR.ITerm.konst
• ISAR.jgs_run ISAR.ITerm.sₛ x✝ = ISAR.ITerm.sₛ
• ISAR.jgs_run ISAR.ITerm.dup x✝ = ISAR.ITerm.dup
• ISAR.jgs_run ISAR.ITerm.comp x✝ = ISAR.ITerm.comp
• ISAR.jgs_run (ISAR.ITerm.var n) x✝ = ISAR.ITerm.var n
• ISAR.jgs_run x✝¹ x✝ = x✝¹ · x✝

def ISAR.jgs_eval (prog data : ITerm) : Option ITerm

Equations

• ISAR.jgs_eval prog data = some (ISAR.jgs_run prog data)

theorem ISAR.jgs_mix (p s d : ITerm) : jgs_eval (jgs_spec p s) d = jgs_eval p (pair s d)

theorem ISAR.jgs_selfApp (p s : ITerm) : jgs_eval ITerm.swap (pair p s) = some (jgs_spec p s)

def ISAR.JGS_PE : PESetup

Full-signature online PE: every IStep rule has a specialization clause.

Equations

• ISAR.JGS_PE = { eval := ISAR.jgs_eval, spec := ISAR.jgs_spec, specTerm := ISAR.ITerm.swap, mix := ISAR.jgs_mix, selfApp := ISAR.jgs_selfApp }

theorem ISAR.JGS_PE_nontrivial : Nontrivial JGS_PE

def ISAR.jgs_comp_witness : ITerm

Extra Nontrivial witness: a static compβ redex folds to norm.

Equations

• ISAR.jgs_comp_witness = ISAR.ITerm.comp · ISAR.ITerm.norm · ISAR.ITerm.norm · ISAR.ITerm.norm

theorem ISAR.jgs_spec_comp_witness (s : ITerm) : jgs_spec jgs_comp_witness s = ITerm.norm

theorem ISAR.JGS_PE_nontrivial_comp : Nontrivial JGS_PE

theorem ISAR.jgs_spec_eq_konst_independent (n : Nat) (a s1 s2 : ITerm) : term_size a ≤ n → jgs_spec a s1 = ITerm.konst → jgs_spec a s2 = ITerm.konst

Residual konst does not depend on the static argument. Used to rule out swap as a self-interpreter (it specializes via jgs_spec).

theorem ISAR.jgs_run_not_konst_dup_same_static (n : Nat) (p s e1 e2 : ITerm) : term_size p ≤ n → ¬(jgs_run p (pair s e1) = ITerm.konst ∧ jgs_run p (pair s e2) = ITerm.dup)

If the first argument of pair is shared, jgs_run cannot return both konst and dup (atoms ignore data; swap specializes independently of the remaining static payload).

theorem ISAR.jgs_run_not_three (n : Nat) (p : ITerm) : term_size p ≤ n → ¬(jgs_run p (pair ITerm.konst ITerm.norm) = ITerm.konst ∧ jgs_run p (pair ITerm.dup ITerm.norm) = ITerm.dup ∧ jgs_run p (pair ITerm.swap ITerm.norm) = ITerm.swap · ITerm.norm)

Online one-step JGS_PE has no self-interpreter: the three atom tests (konst, dup, swap as sources) cannot hold together. Not Jones-optimal. This is not a 1993 polyvariant mix / cogen claim.

theorem ISAR.JGS_PE_not_self_interpreter (int : ITerm) : ¬SelfInterpreter JGS_PE int

theorem ISAR.JGS_PE_not_jonesOptimal : ¬JonesOptimal JGS_PE

One-step online JGS_PE is not Jones-optimal. 1993 polyvariant division / cogen remains open; specTerm is still swap.

theorem ISAR.specialize_ISKTerm (t : ITerm) (ht : ISKTerm t) (s_env : Nat → Option ITerm) : specialize t s_env = t

theorem ISAR.specialize_is_ISKTerm (t : ITerm) (ht : ISKTerm t) (s_env : Nat → Option ITerm) : ISKTerm (specialize t s_env)

theorem ISAR.specialize_respects_OperEq (t u : ITerm) (ht : ISKTerm t) (hu : ISKTerm u) (h : OperEq ⟨t, ht⟩ ⟨u, hu⟩) (s_env : Nat → Option ITerm) : ∃ (ht_spec : ISKTerm (specialize t s_env)), ∃ (hu_spec : ISKTerm (specialize u s_env)), OperEq ⟨specialize t s_env, ht_spec⟩ ⟨specialize u s_env, hu_spec⟩

Parameterized Futamura Square & Commutative Diagram

Formal verification that all 4 execution pathways across the Futamura Projections commute to identical operational semantics:

• Pathway 0 (Direct Evaluation): eval int (pair src d)
• Pathway 1 (1st Projection Target): eval (spec int src) d
• Pathway 2 (2nd Projection Compiler): eval (eval (spec specTerm int) src) d
• Pathway 3 (3rd Projection Cogen): eval (eval (eval (spec specTerm specTerm) int) src) d

structure ISAR.FutamuraSquare (S : PESetup) (int src d : ITerm) : Type

The four corner evaluations of the Futamura Square for a given PESetup.

• direct_eval : Option ITerm
• proj1_target : Option ITerm
• compiler : ITerm
• cogen : ITerm

theorem ISAR.futamura_square_proj1_commutes (S : PESetup) (int src d : ITerm) : S.eval (S.spec int src) d = S.eval int (pair src d)

Commutative Futamura Square Theorem: Evaluating the source program via direct interpretation (Pathway 0) produces the exact same result as executing the 1st Projection compiled target (Pathway 1).

theorem ISAR.futamura_square_proj2_compiler_yields_target (S : PESetup) (int src : ITerm) : S.eval (S.spec S.specTerm int) src = some (S.spec int src)

Compiler Synthesis Commutative Theorem (2nd Projection): Applying the synthesized compiler to the source program yields the 1st projection target.

theorem ISAR.futamura_square_proj3_cogen_yields_compiler (S : PESetup) (int : ITerm) : S.eval (S.spec S.specTerm S.specTerm) int = some (S.spec S.specTerm int)

Compiler-Generator Synthesis Commutative Theorem (3rd Projection): Applying the synthesized cogen to an interpreter yields the 2nd projection compiler.

theorem ISAR.futamura_square_all_pathways_commute (S : PESetup) (int src d : ITerm) : have target1 := S.spec int src; have compiler := S.spec S.specTerm int; have cogen := S.spec S.specTerm S.specTerm; S.eval target1 d = S.eval int (pair src d) ∧ S.eval compiler src = some target1 ∧ S.eval cogen int = some compiler

Full Commutative Futamura Square: All four pathways of the Futamura hierarchy compute identical values on all dynamic inputs.