lambdul

A pure lambda calculus interpreter with built-in macro support.

The interpreter will attempt to reduce any lambda expression to its normal form via α-, β-, and η-reductions.

Setup

Build the interpreter by running ./build from the base directory.

The interpreter can then be used by running ./lambdul from the base directory.

The interpreter accepts lambda expressions in the following format:

Abstractions: \V.(E), where V is a valid identifier and Y is any other lambda expression
Applications: (M N), where M and N are any two lambda expressions
Variables: V, where V is any valid identifier

A valid identifier is any string satisfying the regex [a-zA-Z]+ - i.e. any string comprised of one or more letters.

An actual λ can be used instead of the backslash \ in an abstraction.

To reduce the need for brackets, the interpreter automatically assumes:

left associativity for expressions
- (E1 E2 E3 ... EN) <=> ((...((E1 E2) E3) ...) EN)
right associativity for abstractions
- \x1.\x2....\xN.E <=> (\x1.(\x2.(...(\xN.(E)))))

The interpreter allows the use of macros during a session.

A macro can be assigned with the following syntax:

M := E

where E is any lambda expression, and M is a valid identifier prepended with an underscore (_).

For example, we can assign the following expressions to the _TRUE and _FALSE macros:

_TRUE := \x.(\y.x)
_FALSE := \x.(\y.y)

The macros can then be used as expressions in any input. For instance, the input

((_TRUE \x.x) _FALSE)

is now equivalent to the input

((\x.(\y.x) \x.x) \x.(\y.y))

and will produce the same output:

\x.x

The interpreter supports the use of certain commands, such as:

@evaluate EXPR
- evaluates the expression EXPR in the usual way
- e.g. @evaluate (\x.x \x.y)
@assign MACRO EXPR
- equivalent to MACRO := EXPR
- e.g. @assign _NiceExpression ((\x.(\y.x)) \x.x)
@import "FILE_PATH"
- evaluates all lines in the specified file at FILE_PATH
- results are not printed, but all environment changes (e.g. assignments) are maintained
- e.g. @import "macros.txt"
@exit
- exits the interpreter