NumLang: A research programming language with a higher-order supercompiler, polyhedral recurrence solver, and Lean 4 mechanized correctness proofs.
Abstract
NumLang is an experimental compiled research language and program optimizer implemented in Rust. It integrates multiple program transformation paradigms into a unified SSA Mid-Level Intermediate Representation (MIR) pipeline: Hamilton-style Global Distillation: Inter-procedural process tree distillation that folds across distinct call sites to eliminate intermediate algebraic structures (e.g. multi-stage stream and tree traversals). Multi-Result Supercompilation (MRSC): Bounded configuration hypergraph search paired with Pareto-optimal candidate selection under register and instruction cost models. Polyhedral Recurrence Detection: Algebraic difference engine detecting constant forward differences and companion matrices, collapsing arithmetic progressions and linear recurrences. Reynolds Defunctionalization: Type-directed whole-program closure conversion mapping higher-order lambdas into first-order tagged variants with static dispatches. Lazy Thunk / Codata Supercompilation: Demand-driven symbolic forcing over SSA MIR converting lazy producer-consumer stream pipelines into scalar register loops. Self-Applicable Specialization: A subset specializer (src/stdlib/minspec.nl) structured for Futamura projections (specializing interpreters into compiled residuals). Lean 4 Mechanized Operational Models: Formal machine-checked small-step operational semantics and semantic preservation proofs with zero sorry and zero unproven axioms.
