3.5 KiB
Lamb: A Lambda Calculus Engine
Installation
Method 1: PyPi (not yet)
- Put this on PyPi
- Write these instructions
Method 2: Git
- Clone this repository.
- Make and enter a virtual environment.
cd
into this directory- Run
pip install .
- Run
python .
Usage
Type lambda expressions into the prompt, and Lamb will evaluate them.
Use your \
(backslash) key to type a λ
.
To define macros, use =
. For example,
==> T = λab.a
==> F = λab.a
==> NOT = λa.a F T
Note that there are spaces in λa.a F T
. With no spaces, aFT
will be parsed as one variable.
Lambda functions can only take single-letter, lowercase arguments. λA.A
is not valid syntax.
Free variables will be shown with a '
, like a'
.
Macros are case-sensitive. If you define a macro MAC
and accidentally write mac
in the prompt, mac
will become a free variable.
Numbers will automatically be converted to Church numerals. For example, the following line will reduce to T
.
==> 3 NOT F
If an expression takes too long to evaluate, you may interrupt reduction with Ctrl-C
.
Exit the prompt with Ctrl-C
or Ctrl-D
.
There are many useful macros in macros.lamb. Load them with the :load
command:
==> :load macros.lamb
Have fun!
Commands
Lamb understands many commands. Prefix them with a :
in the prompt.
:help
Prints a help message
:clear
Clear the screen
:rlimit [int | None]
Set maximum reduction limit. :rlimit none
sets no limit.
:macros
List macros in the current environment.
:mdel [macro]
Delete a macro
:clearmacros
Delete all macros
:save [filename]
:load [filename]
Save or load macros from a file.
The lines in a file look exactly the same as regular entries in the prompt, but can only contain macro definitions. See macros.lamb for an example.
Internals
Lamb treats each λ expression as a binary tree. Variable binding and reduction are all simple operations on that tree. All this magic happens in nodes.py
.
Highlights:
TreeWalker
is the iterator we (usually) use to traverse our tree. It walks the "perimeter" of the tree, visiting some nodes multiple times.Node
is the base class for all nodes. Any node has.left
and.right
elements, which may beNone
(empty).Node
s also reference their parent and their direction relative to their parent, to make tree traversal easy.- Before any reduction is done, variables are bound via
bind_variables
. This prevents accidental conflicts common in many lambda parsers.
Todo (pre-release, in this order):
- Cleanup warnings
- Truncate long expressions in warnings
- Prevent macro-chaining recursion
- Full-reduce option (expand all macros)
- step-by-step reduction
- Cleanup files
- Update screenshot
- Update documentation & "internals" section.
- PyPi package
Todo:
- History queue + command indexing
- Show history command
- Better class mutation: when is a node no longer valid?
- Loop detection
\alpha
-equivalence check- Command-line options (load a file, run a set of commands)
- Unchurch macro: make church numerals human-readable
- Syntax highlighting: parenthesis, bound variables, macros, etc
- Tests