Introduction
This is a simple REPL shell for untyped lambda expressions. I wrote it mostly for playing around a little bit with the lambda calculus. Some parts of it are wildly inefficient, but it is fine for education purposes.
The shell can evaluate lambda expressions, assignments and macros. It is not fully tested yet, but you can help with that :).
Installation
Building from Source
You need two things to build the project from source: Cargo and a C compiler/linker like gcc or clang.
# Clone the source repository
git clone https://github.com/jzbor/lash.git
# Build release build with cargo
cargo build --release
# You can now find the binary in ./target/release
ls ./target/release
Running as Nix Flake
If you have Nix installed and Flakes enabled, installing lash should be as easy as:
nix profile install github:jzbor/lash
If you are using NixOS or home-manager you probably know how to install it best yourself.
You can also run the program without permanently installing it like so:
nix profile install github:jzbor/lash
The Language
The Lambda Shell is based on the untyped Lambda calculus. It is a simple system of term substitution.
Untyped Lambda Calculus
There are two basic notions in the Lambda calculus:
- Abstractions: The idea is that we define a function by specifying which variable we want to be able to substitute. A very simple example is the identity function, which takes a term as parameter and maps it to itself:
λx . x - Applications: This allows us to actually evaluate a function. We derive a new term by substituting the variable in the abstraction with the argument term:
(λ x . x x) (y z)→(y z) (y z)
The Lambda Shell allows you to use either λ or \ as lambda symbol for abstractions.
You are allowed to abbreviate multiple abstractions as one: \x . \y . x y = \x y . x y.
In batch mode (when processing .lsh files) you are required to end every statement with a semicolon (;).
This is not necessary in interactive mode.
Assignments
In order to keep this readable the Lambda Shell allows you to name terms and reuse them.
To assign a name to a term the := tag is used:
one := \f . \x . f x
true := \x . \y . y
These terms are referred to with their name until they get resolved explicitly or during reduction (see macros).
Macros
Macros allow you to modify Lambda terms at interpretation time. For example you might want to print out a term, resolve its named terms or reduce/normalize it. Macros are only evaluated once when the term is initially parsed, after that tey are just replaced with the terms they return.
Available Macros:
!cnormalize- like!normalizebut shows number of reductions performed!debug- prints out the argument term!macros- prints available macros!normalize- reduce the term until it cannot be reduced further (this is the so-called normal form)!reduce- execute one reduction step on the argument term!resolve- resolve named terms and church numerals!time- time the macro execution of term inside!vnormalize/!vreduce- like!normalizeand!reduce, but prints the reduction steps
Examples
[λ] one := \f . \x . f x
one := \f . \x . f x
[λ] !resolve (one y)
(\f . \x . f x) y
[λ] one := \f . \x . f x
one := \f . \x . f x
[λ] !vnormalize (one (\y . y y) z)
one (\y . y y) z
(\x . (\y . y y) x) z
(\x . x x) z
z z
Directives
Directives are a mechanism to influence certain behaviours of the interpreter. They do not interact with Lambda terms directly, but can change how for example macros are evaluated.
A directive always has to be on its own line and starts with an @:
@echo "hello world"
Available directives
@echo "<string>"
The @echo directives prints out the string that is passed to it to stdout.
Make sure to put the argument in parenthesis.
@include "<path>"
You can include files that are then directly evaluated. Directives in the included file might also have an effect on following code, so make sure to import files before actually setting important interpreter behavior.
@set <key> <value>
Set compiler behavior with this directive. Settings you can use are:
strategy normal|applicative- changes the reduction strategy (see Strategies)numerals true|false- enable or disable church numerals
@usestd
There is a unstable standard library, which is a collection of a few useful terms.
By running @usestd these get included as named terms.
You can find the terms in src/stdlib.rs.
Strategies
When reducing Lambda terms there are a few different strategies we can pick.
Applicative aka leftmost-innermost
This strategy always replaces inner terms first:
[λ] @set strategy applicative
@set strategy applicative
[λ] !reduce ((\x . (\y . y y) x) z)
(\x . x x) z
Normal aka leftmost-outermost
This strategy always replaces outer terms first:
[λ] @set strategy normal
@set strategy normal
[λ] !reduce ((\x . (\y . y y) x) z)
(\y . y y) z
Church Encodings
After Alonzo Church introduced the lambda calculus he also introduced means to represent different sorts of data with it.
Booleans
Booleans most often represent a truth value and can be either true or false.
In church encodings they are represented by a function that takes two inputs and discards either the first or second value:
TRUE := λx . λy . x
FALSE := λx . λy . y
In lash the standard library gives definitions for TRUE and FALSE as well as several operations such as AND, OR and NOT.
Numerals
A positiv number n is encoded by applying a function f n times to an argument x:
0 := λf . λx . x
1 := λf . λx . f x
2 := λf . λx . f (f x)
3 := λf . λx . f (f (f x))
.
.
.
In lash Church Numerals can be used by prefixing a demoniator with the $ sign.
This has to be enabled either at interpreter invocation or at runtime.
Operations are defined in the standard library.
Example:
[λ] @usestd
@usestd
[λ] @set numerals true
@set numerals true
[λ] !resolve $3
\f . \x . f (f (f x))
[λ] !normalize (ADD $1 $2)
\f . \x . f (f (f x))