easy_lambda_calculus

Simple and easy to write lambda calculus

Examples

lambda!():

Makes a new lambda from a string

use easy_lambda_calculus::*;

fn main() {
  let l = lambda!("%x|y.y")
  println!("{}", lambda!("%x|y.(x y) &{}", l));
}
//outputs λx|y.(x y) &(λx|y.y)

Syntax:

%x.x to define function with input variable x and output defined after the dot.

%x|y.y to define a function with multiple inputs (equivalent to %x.(%y.y) ), variables separated by a pipe | character.

Variables can be multiple characters. eg: %var.var or %true|false.true are also valid.

(x y) to apply y into function x. (x y z) is not valid as the reduction order is ambiguous, define it with ((x y) z) or (x (y z)), see Lambda.reduce() for reduction order.

&(x) is used to mark function x for alpha reduction, so you can reuse variable names without any unintended interactions.

{} is used to input a lambda variable into the lambda, uses the same syntax as the format!() macro, &{} is shorthand for &({}).

Lambda.reduce():

A single step of beta reduction

use easy_lambda_calculus::*;

fn main() {
  println!("{}", lambda!("(%x.(x x)) (%y|z.z)").reduce());
}
//outputs (λy|z.z) (λy|z.z)

Reduction order:

Outer brackets are reduced first. eg: ((λx.(x x)) ((λy.(y y)) (λz.z))) will reduce to (((λy.(y y)) (λz.z)) ((λy.(y y)) (λz.z))) and not (λx.(x x)) ((λz.z) (λz.z))

If the left side is an application into a function rather then a function, it will be reduced first. eg: (((λx.x) (λy.(y y))) (λz.z)) will reduce to ((λy.(y y)) (λz.z))

For reduction with functions marked for alpha reduction, see Lambda.alpha_reduce().

Lambda.alpha_reduce():

Alpha reduce any functions marked for alpha reduction

use easy_lambda_calculus::*;

fn main() {
  println!("{}", lambda!("(%z.(z z)) &(%z.z)").alpha_reduce());
}
//outputs ((λx.(x x)) (λy.y))

Alpha reduction properties:

Alpha reduction will rename every variable based on when they show up in the function. They are renamed with the naming scheme: x, y, z, w, a, b ... u, v, xx, xy...

The renamed variables in any function marked for alpha reduction will be different from any other one.

The alpha reduction function can also be used when there are no functions marked for alpha reduction, to rename the function based on the naming scheme.

The functions marked for alpha reduction cannot be reduced, however can be reduced into other functions Note that reducing them into other functions does not remove that they are marked for alpha reduction, and can cause unwanted effects. For example if multiple variables are replaced with the function marked for alpha reduction, when alpha reduced, every copy will have different variable names.

Lambda.evaluate():

use easy_lambda_calculus::*;

fn main() {
  println!("{}", lambda!("(%x.&(%x.&(%x.x))) &(%x.x)").evaluate());
}
//outputs (λx|y.y)

Evaluation method:

Evaluation will first alpha reduce the function. It will then automatically reduce the function until it cannot be reduced anymore. Lastly it will alpha reduce the function again, to output it with predictable names.