Python tools for lambda calculus.
This is not an officially supported Google product. This is not meant for some serious end; it's a toy to explore something I've been thinking about.
In order to define new very large numbers, people usually invent new notation, and this process is less than perfectly formal. Where the number is computable, it would be cleaner to represent these numbers as the output of a computer program, even though usually these numbers are far too large for the program to actually run to completion. Since such definitions typically make use of many higher-order functions, the pure, untyped lambda calculus is an appealing choice of language. This also has the advantage of a convenient and attractive visual representation in the form of a Tromp diagram.
For an example application, see this detailed description of the largest number defined. This also describes a clean and convenient method for representing computable countable ordinals with fundamental sequences which as far as I know is original.
More output from this program on my blog.
.olc files such as those in the
Install poetry, then try
alias poetry='python3 $HOME/.poetry/bin/poetry' poetry update poetry run ./olcrun --outdir=/tmp/out demofiles/*
If the file ends in
.md, the file is parsed as Markdown, the blockcode parts are extracted,
and this is then parsed as before. It's a very cheap and dirty form of literate programming :)
.olc files support the following directives (grammar):
; immutably binds a variable to the value given.
expr applies beta reduction to the given expression to reach weak head normal form. It's
a goal for this project to try to keep this somewhat readable, so:
- we preserve variable names instead of using de Bruijn form,
- we defer variable substitution until the variable is in the head position
Define a variable
Y such that
Y f is replaced with
f (Y f) when in head position. The Y
combinator can be defined in pure lambda calculus, but the reduction is much easier to follow when
the magic Y is used instead.
Define a variable
eager such that if the expression is
x is reduced if
possible. This is useful for measuring Church integers: if
n represents an expression that
is equivalent to the Church integer 3, then
reduce n eager term; reduces to
eager (eager (eager term)).
variable draws a Tromp diagram of the
expression named by the variable. Before drawing, free variables are substituted for their
values, and beta reductions are performed wherever they reduce the size of the expression.
Finally the size of the expression in bits, represented using binary lambda calculus, is printed.
olcrun --outdir <directory> <olcfile>
will additionally write the drawings as
.png files to the directory named.
draw will fail if the expression contains undefined or "magic" names.
To run tests, use
poetry run ./tests/run_tests.
Each file in the
tests/testdata directory contains a list of question/answer pairs. To
guard against regressions, the
poetry run ./tests/rewrite_test tool can be used to replace the
answers in such a file with the answers that the current version of the software generates.