horner-fold

Horner’s Method as Universal Fold

The kernel acc * base + element appears everywhere in CS under different names. This repository collects implementations across Lisp dialects and verifies core properties with formal methods.

flowchart LR
    S["string\n\"horner!\""]
    L["list of chars\n(h o r n e r !)"]
    I["list of ints\n(104 111 114 ...)"]
    N["bignum\n461241602111777"]
    S -->|string->list| L
    L -->|map char->int| I
    I -->|fold Horner| N
    N -->|unfold quot/rem| I
    I -->|map int->char| L
    L -->|list->string| S

Loading

The Pattern

encode = foldl (λ acc c → acc * base + c) 0   -- catamorphism
decode = unfoldr (λ n → (n `div` b, n `mod` b))  -- anamorphism

Instances: polynomial evaluation (Knuth §4.6.4), base conversion, Rabin-Karp hashing, Gödel numbering, positional/tuple encoding, CRC over GF(2)[x].

The encode/decode pair is a fold/unfold duality — catamorphism and anamorphism composed give a hylomorphism (round-trip identity).

Implementations

Dialect	File	Fold primitive	Lambda order
Guile	horner-guile.scm	fold (SRFI-1)	(element acc)
Guile	horner-guile-rnrs.scm	fold-left (rnrs)	(acc element)
Chez	horner-chez.scm	fold-left	(acc element)
Racket	horner-racket.rkt	foldl	(element acc)
Elisp	horner.el	cl-reduce	(acc element)
Clojure	horner.clj	reduce	(acc element)
Janet	horner.janet	reduce	(acc element)

Lambda argument order is the main portability hazard. SRFI-1 and Racket’s foldl use (element accumulator); everything else uses (accumulator element).

Formal Verification

Tool	Path	Properties verified
Alloy	formal/alloy/horner.als	Roundtrip (len 2, 3), recurrence, example instance
TLA+	formal/tlaplus/Horner.tla	Roundtrip, non-negativity, injectivity (base 3, len 3)
Lean4	formal/lean4/Horner/Basic.lean	hornerEncode_append, _nil, _singleton, _pair, _triple

Running

# Guile
guile horner-guile.scm

# Alloy (requires alloy-analyzer)
bash formal/alloy/run.sh

# TLA+ (requires tla2tools.jar)
bash formal/tlaplus/run.sh

# Lean4 (requires lean/lake via elan)
bash formal/lean4/run.sh

Mathematical Background

Horner Evaluation

For coefficients $a_0, a_1, \ldots, a_n-1$ and base $b$:

$$\text{encode}(\vec{a}, b) = \text{foldl}\;(λ\; \text{acc}\; c → \text{acc} ⋅ b + c)\; 0\; \vec{a}$$

Expanded: $(\cdots((a_0 ⋅ b + a_1) ⋅ b + a_2) \cdots) ⋅ b + a_n-1$

This uses $n-1$ multiplications — optimal (Knuth Vol.2 §4.6.4).

Decode (Unfold)

$$\text{decode}(n, b, k) = \text{unfoldr}\;(λ\; n → (n ÷ b,\; n \bmod b))\; n$$

terminated after $k$ steps.

Roundtrip Property

For $b > 1$ and $0 ≤ a_i < b$:

$$\text{decode}(\text{encode}(\vec{a}, b),\; b,\; |\vec{a}|) = \vec{a}$$

Verified by TLA+ model checking (exhaustive for small domains) and Lean4 theorem proving (structural induction via hornerEncode_append).

Where Horner Appears

Domain	Kernel instance	Reference
Polynomial evaluation	$∑ a_i x^i$ via fold	Knuth §4.6.4
Base conversion	digits → integer	elementary
Tuple encoding	$(i,j,k) → i m^2 + j m + k$	SICP §2.5.3
Rabin-Karp hash	rolling polynomial hash mod $p$	Rabin & Karp 1987
Gödel numbering	sequence → $\mathbb{N}$ injection	Gödel 1931
Mixed-radix encoding	Lehmer codes, factorial number system	Knuth Vol.4A
CRC	polynomial division over GF(2)[x]	Peterson & Brown 1961
Transformer positional PE	continuous relaxation of discrete Horner	Vaswani et al. 2017

Literate Source

The org-mode literate source is in horner-fold.org — all code blocks tangle to the implementation files. The org file includes the comparison table, argument-order analysis, and threading-macro variants.

Project Structure

horner-fold/
├── horner-fold.org          # literate source (org-babel, multi-dialect)
├── horner-guile.scm         # Guile Scheme (SRFI-1 fold)
├── horner-guile-rnrs.scm    # Guile Scheme (rnrs fold-left)
├── horner-chez.scm          # Chez Scheme (native fold-left)
├── horner-racket.rkt        # Racket (foldl, for/fold, threading)
├── horner.el                # Emacs Lisp (cl-reduce, seq-reduce)
├── horner.clj               # Clojure (reduce, ->> threading)
├── horner.janet              # Janet (reduce, string/bytes)
└── formal/
    ├── alloy/horner.als     # Alloy: bounded model checking
    ├── tlaplus/Horner.tla   # TLA+: state-level invariants
    └── lean4/               # Lean4: proofs by structural induction

References

• Knuth, The Art of Computer Programming, Vol.2 §4.6.4; Vol.4A (combinatorial encodings)
• Abelson & Sussman, Structure and Interpretation of Computer Programs, §2.5.3
• Meijer, Fokkinga & Paterson, “Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire” (1991)
• Rabin & Karp, “Efficient Randomized Pattern-Matching Algorithms” (1987)
• Vaswani et al., “Attention Is All You Need” (2017) — sinusoidal PE as continuous Horner