lambda_calculus
lambda_calculus is a simple, zero-dependency implementation of pure lambda calculus in Safe Rust.
Features
- a parser for lambda expressions, both in classic and De Bruijn index notation
- 7 尾-reduction strategies
- a set of standard terms (combinators)
- lambda-encoded boolean, pair, tuple, option and result data types
- single-pair-encoded list
- Church-, Scott- and Parigot-encoded numerals and lists
- Stump-Fu (embedded iterators)- and binary-encoded numerals
- signed numbers
Installation
Include the library by adding the following to your Cargo.toml:
[dependencies]
lambda_calculus = "3"Compilation features:
-
backslash_lambda: changes the display of lambdas from位to\ -
encoding: builds the data encoding modules; default feature
Example feature setup in Cargo.toml:
[dependencies.lambda_calculus]
version = "3"
default-features = false # do not build the data encoding modules
features = ["backslash_lambda"] # use a backslash lambdaExamples
Comparing classic and De Bruijn index notation
code:
use lambda_calculus::data::num::church::{succ, pred};
fn main() {
println!("SUCC := {0} = {0:?}", succ());
println!("PRED := {0} = {0:?}", pred());
}stdout:
SUCC := 位a.位b.位c.b (a b c) = 位位位2(321)
PRED := 位a.位b.位c.a (位d.位e.e (d b)) (位d.c) (位d.d) = 位位位3(位位1(24))(位2)(位1)
Parsing lambda expressions
code:
use lambda_calculus::*;
fn main() {
assert_eq!(
parse(&"位a.位b.位c.b (a b c)", Classic),
parse(&"位位位2(321)", DeBruijn)
);
}Showing 尾-reduction steps
code:
use lambda_calculus::*;
use lambda_calculus::data::num::church::pred;
fn main() {
let mut expr = app!(pred(), 1.into_church());
println!("{} order 尾-reduction steps for PRED 1 are:", NOR);
println!("{}", expr);
while expr.reduce(NOR, 1) != 0 {
println!("{}", expr);
}
}stdout:
normal order 尾-reduction steps for PRED 1 are:
(位a.位b.位c.a (位d.位e.e (d b)) (位d.c) (位d.d)) (位a.位b.a b)
位a.位b.(位c.位d.c d) (位c.位d.d (c a)) (位c.b) (位c.c)
位a.位b.(位c.(位d.位e.e (d a)) c) (位c.b) (位c.c)
位a.位b.(位c.位d.d (c a)) (位c.b) (位c.c)
位a.位b.(位c.c ((位d.b) a)) (位c.c)
位a.位b.(位c.c) ((位c.b) a)
位a.位b.(位c.b) a
位a.位b.b
Comparing the number of steps for different reduction strategies
code:
use lambda_calculus::*;
use lambda_calculus::data::num::church::fac;
fn main() {
let expr = app(fac(), 3.into_church());
println!("comparing normalizing orders' reduction step count for FAC 3:");
for &order in [NOR, APP, HNO, HAP].iter() {
println!("{}: {}", order, expr.clone().reduce(order, 0));
}
}stdout:
comparing normalizing orders' reduction step count for FAC 3:
normal: 46
applicative: 39
hybrid normal: 46
hybrid applicative: 39
Comparing different numeral encodings
code:
use lambda_calculus::*;
fn main() {
println!("comparing different encodings of number 3 (De Bruijn indices):");
println!(" Church encoding: {:?}", 3.into_church());
println!(" Scott encoding: {:?}", 3.into_scott());
println!(" Parigot encoding: {:?}", 3.into_parigot());
println!("Stump-Fu encoding: {:?}", 3.into_stumpfu());
println!(" binary encoding: {:?}", 3.into_binary());
}stdout:
comparing different encodings of number 3 (De Bruijn indices):
Church encoding: 位位2(2(21))
Scott encoding: 位位1(位位1(位位1(位位2)))
Parigot encoding: 位位2(位位2(位位2(位位1)1)(2(位位1)1))(2(位位2(位位1)1)(2(位位1)1))
Stump-Fu encoding: 位位2(位位2(2(21)))(位位2(位位2(21))(位位2(位位21)(位位1)))
binary encoding: 位位位1(13)
