Research Plan: A Terminating Language for Rational Algebraic Structures
Research plan for Chromos/Qrat — a total, termination-guaranteed programming language designed for rational algebraic computation.
Codename: Chromos (from chromogeometry) or Qrat (rational Q)
Part I: Philosophical Foundations
1.1 The Core Vision
You are designing what theorists call a total functional language—a language where every well-typed program is guaranteed to terminate. This is not a limitation but a feature: it gives you decidability properties that Turing-complete languages cannot have.
The key insight: By restricting computational power, we gain mathematical guarantees.
Your language sits at the intersection of:
- Constructive/Finitist mathematics (Wildberger, Bishop, Martin-Löf)
- Experimental mathematics (Zeilberger, Borwein)
- Total functional programming (Turner, McBride, Brady)
- Term rewriting systems (Baader, Nipkow)
1.2 Why This Approach is Sound
Wildberger's critique of infinite processes in mathematics aligns perfectly with a computational philosophy: if you cannot compute it in finite steps, it does not exist in your language. This gives you:
- Decidable type checking - you can always determine if a program is valid
- Guaranteed termination - every computation finishes
- Exact arithmetic - no floating point errors, no numerical instability
- Referential transparency - expressions can be freely substituted
1.3 What You Are NOT Building
- Not a general-purpose language (no infinite loops, no unbounded recursion)
- Not optimized for systems programming
- Not Turing complete (this is intentional and good)
- Not approximation-based (no floats, no limits, no ε-δ)
Part II: Theoretical Foundations to Study
2.1 Essential Reading: Termination Theory
Start here—this is the theoretical backbone of your language:
-
Gödel's System T (1958)
- The original "total" typed lambda calculus
- Primitive recursion over natural numbers
- Every function provably terminates
- Key insight: Recursion is only allowed on structurally smaller arguments
-
Turner's Total Functional Programming (2004)
- Paper: "Total Functional Programming"
- Argues TFP is sufficient for most real programs
- Shows how to handle infinite structures via codata
- Key insight: Totality can be enforced by syntactic restrictions
-
Structural Recursion and Well-Founded Orders
- A function terminates if it only recurses on "smaller" inputs
- "Smaller" is defined by a well-founded order (no infinite descending chains)
- For your language: polynomials have degree, rationals have height, trees have depth
2.2 Essential Reading: Type Theory
-
Martin-Löf Type Theory (constructive foundations)
- Types as propositions, programs as proofs
- Dependent types allow expressing mathematical properties
- Relevance: You might want
Polynomial(n)where n is the degree
-
Hindley-Milner Type System
- The type system of ML, Haskell (core)
- Decidable type inference
- Relevance: Simpler than dependent types, might be sufficient initially
2.3 Essential Reading: Computer Algebra
-
Geddes, Czapor, Labahn: "Algorithms for Computer Algebra"
- Polynomial arithmetic, GCD, factorization
- Rational function manipulation
- Critical for: Understanding exact arithmetic algorithms
-
von zur Gathen & Gerhard: "Modern Computer Algebra"
- More advanced algorithms
- Complexity analysis
- Key insight: Many CAS algorithms ARE terminating (they're your primitives)
2.4 Essential Reading: WZ Theory
-
Petkovšek, Wilf, Zeilberger: "A=B" (freely available online!)
- The bible of automated identity proving
- WZ algorithm in detail
- Key insight: Finding rational certificates for hypergeometric sums
-
Zeilberger's papers on experimental mathematics
- Philosophy of finite, explicit mathematics
- Opinion pieces on infinity and rigor
2.5 Languages to Study
-
Agda - Dependently typed, termination checker
- Study HOW it enforces termination
- Uses structural recursion + sized types
-
Idris - Similar to Agda, more practical
- Totality checking as a feature
- "Total" keyword for functions
-
Charity (historic) - Categorical language
- Only primitive recursion (folds) and corecursion (unfolds)
- Guaranteed termination by construction
-
Epigram - McBride's language
- "Eliminating Dependent Pattern Matching"
Part III: Language Design Decisions
3.1 Core Data Types (Your "Primitives")
┌─────────────────────────────────────────────────────────────┐
│ TYPE HIERARCHY │
├─────────────────────────────────────────────────────────────┤
│ │
│ Level 0: Naturals │
│ ℕ = Zero | Succ(ℕ) │
│ │
│ Level 1: Integers │
│ ℤ = (sign: Bool, magnitude: ℕ) │
│ │
│ Level 2: Rationals │
│ ℚ = (numerator: ℤ, denominator: ℕ⁺) │
│ Invariant: gcd(num, denom) = 1 │
│ │
│ Level 3: Polynomials over ℚ │
│ Poly(n) = ℚ^(n+1) -- coefficients, degree ≤ n │
│ "Polynumbers" in Wildberger's terminology │
│ │
│ Level 4: Rational Functions │
│ RatFunc = (numerator: Poly, denominator: Poly) │
│ Invariant: denominator ≠ 0 │
│ │
│ Level 5: Multinumbers / Trees │
│ Tree(A) = Leaf(A) | Branch(List(Tree(A))) │
│ "Box arithmetic" structures │
│ │
│ Level 6: Matrices over any of the above │
│ Matrix(m, n, T) = T^(m×n) │
│ "Maxels" - matrix elements │
│ "Vexels" - vector elements │
│ │
└─────────────────────────────────────────────────────────────┘
3.2 Core Operations (Guaranteed to Terminate)
Arithmetic (closed operations):
add : ℚ × ℚ → ℚ -- always terminates, exact
mul : ℚ × ℚ → ℚ -- always terminates, exact
sub : ℚ × ℚ → ℚ -- always terminates, exact
div : ℚ × ℚ⁺ → ℚ -- type ensures non-zero divisor
Polynomial operations:
poly_add : Poly × Poly → Poly
poly_mul : Poly × Poly → Poly
poly_degree : Poly → ℕ
poly_eval : Poly × ℚ → ℚ
poly_gcd : Poly × Poly → Poly -- Euclidean algorithm terminates!
poly_div : Poly × Poly → (Poly, Poly) -- quotient, remainder
Structural operations:
fold : (A → B → B) → B → List(A) → B -- THE primitive for lists
map : (A → B) → List(A) → List(B)
filter : (A → Bool) → List(A) → List(A)
3.3 Recursion: The Critical Design Choice
You have three main options:
Option A: Primitive Recursion Only (Simplest)
-- Only allowed to recurse on structurally smaller arguments
-- The compiler CHECKS this syntactically
factorial : ℕ → ℕ
factorial Zero = 1
factorial (Succ n) = (Succ n) * factorial n -- n is smaller than Succ(n) ✓
Pros: Simple to implement, easy to understand Cons: Some natural algorithms are awkward (Ackermann function impossible)
Option B: Well-Founded Recursion (More Expressive)
-- Must provide a "measure" that decreases
-- Measure maps to ℕ with standard < ordering
gcd : ℕ × ℕ → ℕ
gcd (a, 0) = a
gcd (a, b) = gcd (b, a mod b) -- measure: second argument decreases
Pros: More algorithms expressible Cons: Need to verify measures (can be automated for simple cases)
Option C: Sized Types (Most Sophisticated)
-- Types carry size information
-- Size must decrease in recursive calls
data List (i : Size) (A : Type) where
Nil : List i A
Cons : A → List j A → List (↑j) A -- ↑j is "successor size"
Pros: Very expressive while staying total Cons: Complex to implement
My Recommendation: Start with Option A (primitive recursion), extend to Option B as needed. This matches your philosophy of starting restricted.
3.4 What You Explicitly Forbid
┌─────────────────────────────────────────────────────────────┐
│ FORBIDDEN CONSTRUCTS │
├─────────────────────────────────────────────────────────────┤
│ │
│ ✗ General recursion (while loops, fix points) │
│ ✗ Floating point types and operations │
│ ✗ Bitwise operations (AND, OR, XOR, shifts) │
│ ✗ Unbounded iteration │
│ ✗ Non-terminating corecursion │
│ ✗ Side effects (IO, mutation, exceptions) │
│ ✗ Partial functions (head of empty list) │
│ ✗ Type coercion / casting │
│ ✗ Pointer arithmetic │
│ ✗ Dynamic code generation │
│ │
└─────────────────────────────────────────────────────────────┘
Part IV: Box Arithmetic Integration
4.1 Wildberger's Box Arithmetic Interpretation
Based on Wildberger's approach, boxes represent structured pairs/intervals:
-- A "box" is a pair of rationals, written [a, b]
Box : Type
Box = (ℚ, ℚ)
-- Box operations (from chromogeometry)
box_add : Box × Box → Box
box_add ([a,b], [c,d]) = [a+c, b+d]
box_mul : Box × Box → Box
box_mul ([a,b], [c,d]) = [a*c + b*d, a*d + b*c] -- like complex multiplication!
-- This generalizes to "chromatic" multiplication
-- Different "colors" have different multiplication rules
4.2 Quadrance and Spread (Rational Trigonometry)
-- Quadrance: squared distance (always rational for rational points)
quadrance : Point × Point → ℚ
quadrance ((x1,y1), (x2,y2)) = (x2-x1)² + (y2-y1)²
-- Spread: squared sine (rational for rational lines)
spread : Line × Line → ℚ
-- ... defined via cross-ratio, always rational
-- The key identities become THEOREMS your language can express:
-- spread_law : Q1/s1 = Q2/s2 = Q3/s3
-- cross_law : (s1 + s2 + s3)² = 2(s1² + s2² + s3²) + 4*s1*s2*s3
4.3 Multinumbers (Higher Structures)
-- A multinumber is a tree of rationals
-- Level 1: rational
-- Level 2: pair of rationals (box)
-- Level 3: pair of pairs, etc.
data MultiNum where
Base : ℚ → MultiNum
Branch : MultiNum × MultiNum → MultiNum
-- Operations lift through the tree structure
mn_add : MultiNum × MultiNum → MultiNum
mn_mul : MultiNum × MultiNum → MultiNum
Part V: WZ Algorithm Integration
5.1 The WZ Method (Core Idea)
Given a summation identity: Σₖ F(n,k) = result(n)
The WZ method finds a "certificate" R(n,k) such that:
F(n+1,k) - F(n,k) = G(n,k+1) - G(n,k)
where G(n,k) = R(n,k) · F(n,k)
The certificate R(n,k) is a RATIONAL FUNCTION — perfect for your language!
5.2 Language Support for WZ
-- Hypergeometric terms
data HyperTerm = HyperTerm {
polynomial_num : Poly,
polynomial_denom : Poly,
base : ℚ,
factorial_parts : List(ℤ) -- exponents of factorials
}
-- WZ certificate type
type WZCert = RatFunc × RatFunc -- R(n,k) and the proof
-- The key primitive: search for certificate
-- This is BOUNDED search, hence terminating
find_wz_cert : HyperTerm → Maybe(WZCert)
5.3 Zeilberger's "Holonomic" Approach
-- A sequence is "holonomic" if it satisfies a linear recurrence
-- with polynomial coefficients
data Holonomic = Holonomic {
initial_values : List(ℚ),
recurrence : List(Poly) -- a_n = Σᵢ pᵢ(n) * a_{n-i}
}
-- Closure properties (all terminating!)
holo_add : Holonomic × Holonomic → Holonomic
holo_mul : Holonomic × Holonomic → Holonomic
holo_sum : Holonomic → Holonomic -- indefinite summation
Part VI: Implementation Roadmap
Phase 1: Core Language (Months 1-3)
Goal: Minimal viable language with rational arithmetic
Week 1-2: Lexer and parser for basic syntax
Week 3-4: AST representation
Week 5-6: Type checker (simple Hindley-Milner)
Week 7-8: Termination checker (structural recursion)
Week 9-10: Interpreter for ℕ, ℤ, ℚ operations
Week 11-12: Basic REPL, testing infrastructure
Milestone: Compute factorial(100) as exact integer
Phase 2: Polynomial Algebra (Months 4-6)
Goal: Full polynomial and rational function support
Week 1-3: Polynomial representation and basic ops
Week 4-6: Polynomial GCD (Euclidean algorithm)
Week 7-9: Rational functions, simplification
Week 10-12: Polynomial factorization (over ℚ)
Milestone: Factor x⁴ - 1 symbolically
Phase 3: Box Arithmetic (Months 7-9)
Goal: Wildberger's geometric primitives
Week 1-3: Box type and operations
Week 4-6: Quadrance, spread, rational trig
Week 7-9: Chromogeometry (3 metrics)
Week 10-12: Projective coordinates
Milestone: Verify spread law for given triangle
Phase 4: WZ Integration (Months 10-12)
Goal: Automated identity proving
Week 1-4: Hypergeometric term representation
Week 5-8: WZ certificate search algorithm
Week 9-12: Holonomic sequence closure
Milestone: Automatically prove Σₖ C(n,k) = 2ⁿ
Phase 5: Exploration Tools (Year 2)
- Visualization of rational geometry
- Pattern search in coefficient sequences
- Export to LaTeX/mathematical notation
- Integration with OEIS
Part VII: Concrete First Steps
7.1 Choose Your Implementation Language
Recommended: Rust or Haskell
Rust:
- You already know it well
numcrate for big integers/rationals- Strong type system helps correctness
- Good for eventual performance
Haskell:
- Natural fit for language implementation (parsec, etc.)
- Algebraic data types match your AST
- Pattern matching for term rewriting
- Built-in arbitrary precision Integer/Rational
My suggestion: Given your background, Rust with heavy use of:
num-bigintfor integersnum-rationalfor rationalslalrpoporpestfor parsing- Algebraic data types via enums
7.2 First Implementation Exercise
Build this tiny language first (1-2 weeks):
-- Syntax
expr ::= nat | expr + expr | expr * expr | (expr)
nat ::= 0 | 1 | 2 | ...
-- Examples
3 + 4 → 7
(2 + 3) * 4 → 20
This teaches you:
- Lexing and parsing
- AST representation
- Tree-walking interpreter
- REPL basics
7.3 Second Implementation Exercise
Add rationals and one recursive construct (2-3 weeks):
-- Syntax
expr ::= rat | expr + expr | expr * expr | expr / expr | fold(f, base, list)
rat ::= integer | integer/integer
list ::= [expr, expr, ...]
-- Examples
1/2 + 1/3 → 5/6
fold(add, 0, [1,2,3]) → 6
7.4 Reference Implementations to Study
-
Kaleidoscope (LLVM tutorial)
- Simple language, well-documented
- Shows full pipeline
-
miniml (ML subset)
- Type inference implementation
- Pattern matching
-
Pie (from "The Little Typer")
- Dependent types, termination
- Very clear pedagogical implementation
Part VIII: Theoretical Boundaries
8.1 What Your Language CAN Express
According to the theory of primitive recursive functions:
- All polynomial-time algorithms
- Most practical mathematical computations
- GCD, factorization, symbolic integration (for rational functions)
- WZ certificates (when they exist)
- Combinatorial enumeration (bounded)
8.2 What Your Language CANNOT Express
- Ackermann function (grows too fast)
- General theorem proving (undecidable)
- Arbitrary search (unbounded)
- Kolmogorov complexity
- Busy beaver functions
This is fine! These are exactly the "infinite" or "non-constructive" things Wildberger critiques.
8.3 The Expressiveness Sweet Spot
Your language lives in the space:
Primitive Recursive ⊂ Your Language ⊂ Total Computable ⊂ Partial Computable
(System T) (goal) (System F) (Turing machines)
Part IX: Extended Reading List
Must Read (Priority Order)
-
"Total Functional Programming" - D.A. Turner (2004)
- FREE: https://kar.kent.ac.uk/22566/
- The manifesto for your approach
-
"A=B" - Petkovšek, Wilf, Zeilberger
- FREE: https://www.math.upenn.edu/~wilf/AesthB.html
- WZ method, hypergeometric summation
-
"Crafting Interpreters" - Robert Nystrom
- FREE: https://craftinginterpreters.com/
- Best practical guide to language implementation
-
"Types and Programming Languages" - Benjamin Pierce
- The standard type theory textbook
- Chapters 1-11 for basics, 21 for System F
-
Divine Proportions - Norman Wildberger
- Rational trigonometry foundations
- Your geometric primitives
Secondary Reading
-
"Practical Foundations for Programming Languages" - Robert Harper
- FREE draft online
- More advanced type theory
-
"Term Rewriting and All That" - Baader & Nipkow
- Termination proofs for rewriting systems
- Relevant if you go the term-rewriting route
-
"The Little Typer" - Friedman & Christiansen
- Gentle intro to dependent types
- Accompanying implementation "Pie"
Papers
-
"Why Dependent Types Matter" - McBride, McKinna
- Motivates total languages
-
"Eliminating Dependent Pattern Matching" - Goguen, McBride, McKinna
- Technical details of totality checking
Part X: Key Philosophical Alignment
Wildberger's Principles in Language Design
| Wildberger Principle | Language Implementation | |---------------------|------------------------| | "No infinite sets" | No unbounded types | | "No completed infinities" | No non-terminating recursion | | "Exact arithmetic" | Rationals, not floats | | "Explicit constructions" | All values computed, never postulated | | "Finitely checkable proofs" | Decidable type checking | | "Quadrance over distance" | Rationals stay rational |
Zeilberger's Principles in Language Design
| Zeilberger Principle | Language Implementation | |---------------------|------------------------| | "Let computers do the work" | Automated certificate search | | "Explicit over existential" | Witnesses required in proofs | | "Finite mathematics" | Bounded structures | | "Combinatorial proofs" | Pattern enumeration primitives |
Part XI: Community and Resources
Online Communities
- Proof Assistants: Agda/Idris/Lean Zulip chats
- Programming Languages: r/ProgrammingLanguages
- Wildberger: Insights into Mathematics YouTube comments
- Experimental Mathematics: Journal of Experimental Mathematics
Tools
- PLZoo: Collection of small language implementations
- Turnstile: Racket library for building typed languages
- BNFC: BNF Converter (grammar → parser)
Conclusion: Your Path Forward
- Week 1: Read Turner's "Total Functional Programming" paper
- Week 2: Work through first 3 chapters of "Crafting Interpreters"
- Week 3: Implement tiny arithmetic language in Rust
- Week 4: Add rationals with exact arithmetic
- Month 2: Add structural recursion with termination checking
- Month 3: Add polynomials and basic algebra
You are building something genuinely novel: a language that takes Wildberger's finitist philosophy seriously at the computational level. This is intellectually coherent and practically useful for experimental mathematics.
The key insight is that restriction is power: by giving up Turing completeness, you gain termination guarantees, decidability, and mathematical clarity.
"The price of reliability is the pursuit of the utmost simplicity." — Tony Hoare