def ISAR.ISKSubtype : Type

The subtype of ISAR terms that belong to the pure SKI fragment.

Equations

• ISAR.ISKSubtype = { t : ISAR.ITerm // ISAR.ISKTerm t }

def ISAR.OperEq (t u : ISKSubtype) : Prop

Two terms are operationally equivalent if they can reduce to a common term.

Equations

• ISAR.OperEq t u = ∃ (v : ISAR.ITerm), ISAR.IRed t.val v ∧ ISAR.IRed u.val v

theorem ISAR.OperEq.refl (t : ISKSubtype) : OperEq t t

theorem ISAR.OperEq.symm {t u : ISKSubtype} (h : OperEq t u) : OperEq u t

theorem ISAR.OperEq.trans {t u w : ISKSubtype} (h1 : OperEq t u) (h2 : OperEq u w) : OperEq t w

@[implicit_reducible]

instance ISAR.operEqSetoid : Setoid ISKSubtype

Equations

• ISAR.operEqSetoid = { r := ISAR.OperEq, iseqv := ISAR.operEqSetoid._proof_1 }

def ISAR.InvariantLayer : Type

The Invariant Layer is defined as the operational equivalence quotient of the SKI fragment.

Equations

• ISAR.InvariantLayer = Quotient ISAR.operEqSetoid

def ISAR.app_raw (t u : ISKSubtype) : ISKSubtype

Application of raw fragment subtypes.

Equations

• ISAR.app_raw t u = ⟨t.val · u.val, ⋯⟩

theorem ISAR.app_congruence (t1 t2 u1 u2 : ISKSubtype) (ht : OperEq t1 t2) (hu : OperEq u1 u2) : OperEq (app_raw t1 u1) (app_raw t2 u2)

Operational equivalence is a congruence under application.

def ISAR.InvariantLayer.app (t u : InvariantLayer) : InvariantLayer

Application descends to a well-defined function on Invariant Layer quotient classes.

Equations

• t.app u = Quotient.lift₂ (fun (t u : ISAR.ISKSubtype) => Quotient.mk ISAR.operEqSetoid (ISAR.app_raw t u)) ISAR.InvariantLayer.app._proof_1 t u

def ISAR.toInvariantLayer (t : ISKSubtype) : InvariantLayer

Canonical projection to the Invariant Layer.

Equations

• ISAR.toInvariantLayer t = Quotient.mk ISAR.operEqSetoid t

def ISAR.HasNF (t : ISKSubtype) : Prop

Equations

• ISAR.HasNF t = ∃ (n : ISAR.ISKSubtype), ISAR.IRed t.val n.val ∧ ISAR.NormalI n.val

theorem ISAR.HasNF_of_OperEq {t u : ISKSubtype} (h : OperEq t u) (ht : HasNF t) : HasNF u

theorem ISAR.OperEq_HasNF_eq {t u : ISKSubtype} (h : OperEq t u) : HasNF t = HasNF u

def ISAR.InvariantLayer.HasNF (q : InvariantLayer) : Prop

Equations

• q.HasNF = Quotient.lift ISAR.HasNF ⋯ q

theorem ISAR.ISKTerm_cd {t : ITerm} (ht : ISKTerm t) : ISKTerm (cd t)

def ISAR.term_size : ITerm → Nat

Equations

• ISAR.term_size (ISAR.ITerm.var a) = 1
• ISAR.term_size ISAR.ITerm.norm = 1
• ISAR.term_size ISAR.ITerm.konst = 1
• ISAR.term_size ISAR.ITerm.dup = 1
• ISAR.term_size ISAR.ITerm.swap = 1
• ISAR.term_size ISAR.ITerm.comp = 1
• ISAR.term_size ISAR.ITerm.sₛ = 1
• ISAR.term_size (f · x_1) = ISAR.term_size f + ISAR.term_size x_1 + 1

inductive ISAR.IKTerm : ITerm → Prop

• norm : IKTerm ITerm.norm
• konst : IKTerm ITerm.konst
• app {f x : ITerm} : IKTerm f → IKTerm x → IKTerm (f · x)

theorem ISAR.cd_app_of_not_redex (f x : ITerm) (h1 : f ≠ ITerm.norm) (h2 : ∀ (y : ITerm), f ≠ ITerm.konst · y) (h3 : ∀ (y z : ITerm), f ≠ ITerm.comp · y · z) (h4 : ∀ (y z : ITerm), f ≠ ITerm.sₛ · y · z) : cd (f · x) = cd f · cd x

theorem ISAR.cd_size_le_IK (t : ITerm) (ht : IKTerm t) : term_size (cd t) ≤ term_size t

theorem ISAR.cd_size_lt_IK (t : ITerm) (ht : IKTerm t) (h : t ≠ cd t) : term_size (cd t) < term_size t

def ISAR.cd_loop_fuel (fuel : Nat) (t : ISKSubtype) : ISKSubtype

Equations

• ISAR.cd_loop_fuel 0 t = t
• ISAR.cd_loop_fuel fuel'.succ t = if t.val = ISAR.cd t.val then t else ISAR.cd_loop_fuel fuel' ⟨ISAR.cd t.val, ⋯⟩

theorem ISAR.OperEq_cd_loop_fuel (fuel : Nat) (t : ISKSubtype) : OperEq (cd_loop_fuel fuel t) t

theorem ISAR.cd_loop_fuel_quotient_eq (fuel : Nat) (t : ISKSubtype) : toInvariantLayer (cd_loop_fuel fuel t) = toInvariantLayer t

partial def ISAR.cd_loop (t : ISKSubtype) : ISKSubtype

@[implemented_by ISAR.cd_loop]

noncomputable def ISAR.nf_of_term (t : ISKSubtype) : ISKSubtype

Representative of an OperEq-class on concrete terms. AC section used by canonical_rep. Not claimed computable.

• If HasNF, pick some NF (Classical.choose on the nonempty NF fiber). The computational HasNF section is nf_of_HasNF_fuel / nf_of_HasNF in CanonicalRepresentative.lean (choose fuel, then cd_loop_fuel). That file imports this one, so this HasNF branch cannot call cd_loop_fuel via that path without a cycle.
• If ¬HasNF, pick any class representative via Quotient.exists_rep. SKI is not SN; no finite cd yields NormalI. This is expected, not a gap.

Computational path: @[implemented_by cd_loop] (iterated complete development).

Equations

• ISAR.nf_of_term t = if h : ISAR.HasNF t then Classical.choose h else Classical.choose ⋯

theorem ISAR.unique_nf_of_OperEq {t u : ISKSubtype} (h : OperEq t u) : nf_of_term t = nf_of_term u

theorem ISAR.nf_of_term_OperEq (t : ISKSubtype) : OperEq (nf_of_term t) t

nf_of_term is always an OperEq-representative (fixes the old false norm fallback).

noncomputable def ISAR.InvariantLayer.canonical_rep (q : InvariantLayer) : ISKSubtype

Equations

• q.canonical_rep = Quotient.lift ISAR.nf_of_term ⋯ q

def ISAR.dupCount : ITerm → Nat

Equations

• ISAR.dupCount ISAR.ITerm.dup = 1
• ISAR.dupCount (ISAR.ITerm.dup · a) = 0
• ISAR.dupCount (f · x_1) = ISAR.dupCount f + ISAR.dupCount x_1
• ISAR.dupCount x✝ = 0

inductive ISAR.LinearIKTerm : ITerm → Prop

• norm : LinearIKTerm ITerm.norm
• konst : LinearIKTerm ITerm.konst
• app {f x : ITerm} : LinearIKTerm f → LinearIKTerm x → dupCount (f · x) = 0 → LinearIKTerm (f · x)
• app_dup {x : ITerm} : LinearIKTerm x → LinearIKTerm (ITerm.dup · x)

theorem ISAR.dupCount_of_LinearIKTerm {t : ITerm} (ht : LinearIKTerm t) : dupCount t = 0

theorem ISAR.dupCount_app_of_zero {f x : ITerm} (h : dupCount f = 0) : dupCount (f · x) = dupCount f + dupCount x

theorem ISAR.dupCount_app {f x : ITerm} (hf : LinearIKTerm f) : dupCount (f · x) = dupCount f + dupCount x

theorem ISAR.cd_size_le_LinearIK (t : ITerm) (ht : LinearIKTerm t) : term_size (cd t) ≤ term_size t

theorem ISAR.cd_size_lt_LinearIK (t : ITerm) (ht : LinearIKTerm t) (h : t ≠ cd t) : term_size (cd t) < term_size t

theorem ISAR.LinearIKTerm_cd {t : ITerm} (ht : LinearIKTerm t) : LinearIKTerm (cd t)

theorem ISAR.cd_app_of_LinearIKTerm {f : ITerm} (x : ITerm) (hf : LinearIKTerm f) (h_norm : f ≠ ITerm.norm) (h_konst : ∀ (y : ITerm), f ≠ ITerm.konst · y) : cd (f · x) = cd f · cd x

theorem ISAR.normal_of_cd_eq (t : ITerm) (ht : LinearIKTerm t) (h : t = cd t) : NormalI t

theorem ISAR.cd_loop_fuel_spec (n : Nat) (t : ISKSubtype) (ht : LinearIKTerm t.val) (hn : term_size t.val ≤ n) : HasNF (cd_loop_fuel n t) ∧ NormalI (cd_loop_fuel n t).val

def ISAR.sufficient_fuel (t : ISKSubtype) : Nat

Equations

• ISAR.sufficient_fuel t = ISAR.term_size t.val

theorem ISAR.sufficient_fuel_correct (t : ISKSubtype) (ht : LinearIKTerm t.val) : HasNF (cd_loop_fuel (sufficient_fuel t) t) ∧ NormalI (cd_loop_fuel (sufficient_fuel t) t).val