Reduce — leftmost-outermost single-step interpreter

step? matches IStep redexes only (normβ, konstβ, compβ, sβ, appL, appR). No dupβ/swapβ — those belong to IStepBasis, not the main reduction.

reduceFuel iterates step? up to a fuel bound.

Soundness: step?_sound proves step? t = some u → IStep t u.

def ISAR.step? : ITerm → Option ITerm

Leftmost-outermost one-step reduction matching IStep.

Equations

• ISAR.step? (ISAR.ITerm.norm · x_1) = some x_1
• ISAR.step? (ISAR.ITerm.konst · x_1 · a) = some x_1
• ISAR.step? (ISAR.ITerm.comp · f · g · x_1) = some (f · (g · x_1))
• ISAR.step? (ISAR.ITerm.sₛ · x_1 · y · z) = some (x_1 · z · (y · z))
• ISAR.step? (f · x_1) = match ISAR.step? f with | some f' => some (f' · x_1) | none => match ISAR.step? x_1 with | some x' => some (f · x') | none => none
• ISAR.step? x✝ = none

def ISAR.reduceFuel : Nat → ITerm → ITerm

Fuelled iteration of step?.

Equations

• ISAR.reduceFuel 0 x✝ = x✝
• ISAR.reduceFuel n.succ x✝ = match ISAR.step? x✝ with | some u => ISAR.reduceFuel n u | none => x✝

def ISAR.reduceCount : Nat → ITerm → Nat × ITerm

Count steps taken before normal form or fuel exhaustion.

Equations

• ISAR.reduceCount 0 x✝ = (0, x✝)
• ISAR.reduceCount n.succ x✝ = match ISAR.step? x✝ with | some u => match ISAR.reduceCount n u with | (k, r) => (k + 1, r) | none => (0, x✝)

Soundness

theorem ISAR.step?_sound (t u : ITerm) : step? t = some u → IStep t u

theorem ISAR.reduceFuel_IRed (n : Nat) (t : ITerm) : IRed t (reduceFuel n t)

#eval / #guard on step? path