Arithmetic by HTTP Redirect, Proved to Halt

Numbers are unary tally marks: | is 1, || is 2, ||| is 3, and the empty string is 0. No decimal, no integers — just tally pipes in a URL. This is Church-style: the numeral is the iteration count. A redirect is a function application.

Two operations, composed left-to-right in the path:

• =​/math/succ/TALLY= → 301 → =​/math/TALLY|= (append one pipe: +1)
• =​/math/pred/|TALLY= → 301 → =​/math/TALLY= (remove one pipe: -1)
• =​/math/pred/= → 301 → =​/math/= (pred 0 = 0, monus)
• =​/math/TALLY= (no function left) → 302 → research note. Done.

Compose them and the URL is a lambda-like expression. Each 301 applies the innermost function (the one nearest the tally) and drops that segment:

/math/succ/pred/|||
  → 301 /math/succ/||    (pred ||| = ||)
  → 301 /math/|||        (succ || = |||)
  → 302 (done, result = 3)

Try it live: succ(succ(succ(0))) = 3 or succ(succ(pred(3))) = 4.

succ is the successor constructor (Lean4 Nat.succ, Racket add1); pred is the predecessor (Lean4 Nat.pred, Racket sub1) with monus semantics (pred 0 = 0, not an error).

Why it halts: every hop consumes a function segment, so the path strictly shrinks toward the bare tally. An all-succ expression halts just as surely as an all-pred one — the value grows but the path empties. Hops = the number of function segments. Apache cannot do arithmetic, so the representation must be unary — succ appends a character and pred strips one. Pure string manipulation, no math.

---------------------------- MODULE MathRedirects ----------------------------
\* /math/f1/f2/.../fk/n  with each fi in {succ, pred}. Each 301 applies the
\* innermost function and drops it, so the path shrinks one segment per hop.
EXTENDS Naturals, Sequences
CONSTANTS MaxLen, MaxBase
Fns == {"succ", "pred"}
Apply(f, m) == IF f = "succ" THEN m + 1
               ELSE IF m = 0 THEN 0 ELSE m - 1        \* pred = monus (0 - 1 = 0)

VARIABLES funcs, value, phase, hops
vars == <<funcs, value, phase, hops>>

BoundedSeqs == UNION { [1..k -> Fns] : k \in 0..MaxLen }
Init == funcs \in BoundedSeqs /\ value \in 0..MaxBase
        /\ phase = "eval" /\ hops = 0

Step == /\ phase = "eval" /\ Len(funcs) > 0
        /\ value' = Apply(funcs[Len(funcs)], value)    \* apply innermost
        /\ funcs' = SubSeq(funcs, 1, Len(funcs) - 1)   \* drop it: path shrinks
        /\ hops' = hops + 1 /\ phase' = "eval"
Done == /\ phase = "eval" /\ Len(funcs) = 0
        /\ phase' = "done" /\ UNCHANGED <<funcs, value, hops>>

Next == Step \/ Done
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

Terminates  == <>(phase = "done")                      \* every expression evaluates
HopsBounded == hops <= MaxLen                           \* hops = number of functions
=============================================================================

Config: SPECIFICATION Spec, CONSTANTS MaxLen = 4 MaxBase = 5, INVARIANT HopsBounded, PROPERTY Terminates.

Tangle the block to MathRedirects.tla in a temp dir and run TLC (with deadlock-checking off — the terminal /math/n states have no successor by design):

Model checking completed. No error has been found.
570 states generated, 424 distinct states found

Every expression over {succ, pred} up to length 4 on a base <= 5 — 424 reachable states — evaluates to a numeral and stops. hops equals the function count: bounded recursion, proven.

What does not halt is a rule that grows the path instead of consuming it. A redirect like /math/succ/n -> /math/succ/succ/n — lengthening, not applying — never reaches a numeral; it is the deliberate non-terminating canary in the redirect-termination model, the ouroboros, and it ends in ERR_TOO_MANY_REDIRECTS. The distinction is well-foundedness: consuming a segment shrinks toward 0; growing one does not. succ-the-function halts; succ-the-path-rewrite does not.

Useful? No. But it is a machine-checked Peano calculator assembled entirely from .htaccess 301s — which is more than most .htaccess files can claim.