lumbda/README.md
russell@unturf.com b3ab4bb19a Add proof friction benchmark, update README
Benchmark: Python 0.04s, uncommonlisp 59s, Lean 1.5s — for the same claim.
The formal proof is 40x faster than brute-force search with mathematical
certainty instead of floating-point tolerance.

This is MOAD-0001 at the proof layer: O(N²) search friction where
O(1) algebraic reasoning suffices. Proof assistants are the hash set
to numerical analysis's nested loop.
2026-04-14 13:31:05 -04:00

180 lines
7.3 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

# uncommonlisp
A Scheme interpreter in one Python file, with a bytecode compiler.
```
λ> (define (fib n)
(let loop ((a 0) (b 1) (i 0))
(if (= i n) a (loop b (+ a b) (+ i 1)))))
λ> (map fib (iota 10))
(0 1 1 2 3 5 8 13 21 34)
```
## Usage
```bash
python3 uncommonlisp.py # interactive REPL
python3 uncommonlisp.py script.lsp # run a file
python3 uncommonlisp.py -e '(+ 1 2)' # eval an expression
python3 uncommonlisp.py --fast script.lsp # auto-compile (7-19x faster)
```
## Bytecode compiler
uncommonlisp includes a stack-based bytecode compiler and VM. Enable it with `--fast` or `(auto-compile! #t)`:
```bash
python3 uncommonlisp.py --fast examples/fibonacci.lsp
```
```scheme
(auto-compile! #t)
(define (ack m n)
(cond ((= m 0) (+ n 1))
((= n 0) (ack (- m 1) 1))
(else (ack (- m 1) (ack m (- n 1))))))
(compiled? ack) ; => #t
(ack 3 4) ; => 125
```
The compiler handles: `if`, `begin`, `and`, `or`, `when`, `unless`, `cond`, `define`, `set!`, `lambda`, `let`, named-let, `let*`, `letrec`, `do`, `call/cc`, function calls with tail-call optimization. Macros are expanded at compile time. 20 specialized opcodes for hot builtins (`+`, `-`, `*`, `=`, `<`, `car`, `cdr`, `cons`, `null?`, etc.) avoid function call overhead.
Features:
- **Explicit frame stack** — compiled-to-compiled calls don't grow the Python stack
- **Full continuations** — `call/cc` supports upward continuations; generators work
- **Constant folding** — `(+ 1 2)` folds to `3` at compile time
- **Peephole optimizer** — eliminates dead code (VOID+POP, JUMP-to-next)
- **`(disassemble proc)`** — inspect generated bytecode
## What's implemented
**Core language**
- Full lexical scoping and closures
- Tail-call optimization (TCO) — deep recursion never blows the stack
- Hygienic macros via `syntax-rules` with ellipsis (`...`) support
- `define-macro` / `defmacro` for procedural macros
- `call/cc` — full continuations (escape + upward) in compiled code
- `values` / `call-with-values`
- `dynamic-wind`, `guard`, `with-exception-handler`
- `quasiquote` / `unquote` / `unquote-splicing` with proper nesting
- R7RS internal defines with letrec* body semantics
- R7RS error objects
- Exact rational arithmetic — `(/ 1 3)``1/3`, `(+ 1/4 3/4)``1`
- String ports — `open-input-string` `open-output-string` `read` on ports
- Mutable strings — `string-set!` `string-fill!` `string-copy!`
- Module system — `module` / `import` with export lists
- `define-record-type` with `(inherit parent)` for single-inheritance
- Pretty-print — `pp` / `pretty-print`
- Tracing — `(trace fn)` / `(untrace fn)`
**Special forms**
`define` `set!` `lambda` `λ` `if` `cond` `case` `and` `or` `when` `unless`
`begin` `let` `let*` `letrec` `letrec*` named-let `do`
`quasiquote` `define-macro` `define-syntax` `syntax-rules`
`let-syntax` `letrec-syntax` `apply` `eval` `values` `call/cc`
`dynamic-wind` `guard` `parameterize` `load` `error`
`module` `import` `define-record-type`
**Built-ins**
- Arithmetic: `+` `-` `*` `/` `quotient` `remainder` `modulo` `expt` `sqrt` `abs` `floor` `ceiling` `round` `truncate` `min` `max` `gcd` `lcm` `log` `exp` trig functions, `numerator` `denominator`
- Rationals: `(/ 1 3)``1/3`, literal `1/3` syntax, `exact` / `inexact` conversion
- Comparison: `=` `<` `>` `<=` `>=` `zero?` `positive?` `negative?` `odd?` `even?`
- Pairs & lists: `cons` `car` `cdr` `list` `length` `append` `reverse` `map` `for-each` `filter` `fold-left` `fold-right` `reduce` `any` `every` `sort` `partition` `find` `take` `drop` `zip` `flatten` and more
- SRFI-1: `last` `first``fifth` `delete` `lset-union` `lset-intersection` `lset-difference` `unfold` `list-tabulate`
- Strings: `string-length` `string-ref` `string-set!` `substring` `string-append` `string-copy` `string-copy!` `string-fill!` `string->list` `string->number` `format` and more
- Characters: `char->integer` `integer->char` `char-alphabetic?` `char-upcase` `char-downcase`
- Vectors: `make-vector` `vector` `vector-ref` `vector-set!` `vector-copy` `vector-copy!`
- Hash tables: `make-hash-table` `hash-table-set!` `hash-table-ref` `hash-table-keys` `hash-table-values` `hash-table-walk` and more
- I/O: `display` `write` `newline` `read` `read-char` `read-line` `open-input-string` `open-output-string` `with-output-to-string`
- File system: `file-exists?` `delete-file` `rename-file` `directory-files` `current-directory`
- System: `command-line` `get-environment-variable` `current-time` `exit`
- Python interop: `py-eval` `py-exec` `py-import` `py-call` `py-attr`
- Compiler: `compile` `compiled?` `disassemble` `auto-compile!`
**Standard library** (`stdlib.lsp`)
Additional macros, string/list/numeric/tree utilities, alist/hash helpers, simple object system, SRFI-2/8/64 test framework.
## Examples
```bash
python3 uncommonlisp.py --fast examples/fibonacci.lsp
python3 uncommonlisp.py --fast examples/generator.lsp
python3 uncommonlisp.py --fast examples/mergesort.lsp
python3 uncommonlisp.py examples/objects.lsp
```
```scheme
;; Generator using full continuations
(auto-compile! #t)
(define (make-gen thunk)
(let ((k #f) (done #f))
(lambda ()
(if done 'done
(call/cc (lambda (return)
(if k (k return)
(begin (thunk (lambda (val)
(call/cc (lambda (next)
(set! k next) (return val)))))
(set! done #t) (return 'done)))))))))
(define counter (make-gen (lambda (yield)
(let loop ((i 0)) (yield i) (loop (+ i 1))))))
(counter) ; => 0
(counter) ; => 1
(counter) ; => 2
```
## Running tests & benchmarks
```bash
make test # run 529 tests
make test-verbose # verbose output
make bench # compare interpreter vs bytecode vs CPython
make lint # syntax check all Python files
```
## Portal — machine state migration
Serialize a running VM mid-computation, transfer to another machine, resume:
```bash
# Machine A: start a long computation with checkpoints
python3 uncommonlisp.py --fast examples/portal-prime.lsp
# saves prime-state.portal at checkpoint
# Machine B: resume from checkpoint
python3 uncommonlisp.py --portal-resume prime-state.portal
# continues from exact instruction
```
The portal captures the full env chain, compiled procedures, continuations,
and frame stack as JSON. 16KB for a primality test in progress.
## EML universality proof
The `proof/` directory contains a formal verification that `eml(x,y) = exp(x) - ln(y)`
with constant 1 generates all elementary functions (arXiv:2603.21852v2).
Three approaches, benchmarked:
| Approach | Time | Guarantee |
|----------|------|-----------|
| Python (numerical) | 0.04s | 1e-10 tolerance |
| uncommonlisp (numerical) | 59s | 1e-10 tolerance |
| Lean 4 (formal proof) | 1.5s | kernel-verified |
The formal proof is 40x faster than brute-force search with infinitely stronger
guarantees. See `proof/benchmark_results.md` for the full analysis — including
why this is MOAD-0001 (the sedimentary defect) at the proof methodology layer.
## File layout
```
uncommonlisp.py interpreter + bytecode compiler (one file, ~3200 lines)
stdlib.lsp extended standard library
tests.py test suite (571 tests)
bench.py benchmarks vs CPython
examples/ example programs
proof/ EML universality proof (Python, Scheme, Lean 4)
Makefile make test / make bench / make repl
```