Features

Installation

[dependencies]lambda_calculus ="3"

[dependencies.lambda_calculus]version ="3"default-features =false# do not build the data encoding modulesfeatures = ["backslash_lambda"]# use a backslash lambda

Examples

Comparing classic and De Bruijn index notation

use lambda_calculus::data::num::church::{succ, pred};fnmain(){println!("SUCC := {0} = {0:?}", succ());println!("PRED := {0} = {0:?}", pred());}

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

use lambda_calculus::*;fnmain(){assert_eq!(        parse(&"λa.λb.λc.b (a b c)",Classic),        parse(&"λλλ2(321)",DeBruijn));}

Showing β-reduction steps

use lambda_calculus::*;use lambda_calculus::data::num::church::pred;fnmain(){letmut 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);}}

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

use lambda_calculus::*;use lambda_calculus::data::num::church::fac;fnmain(){let expr =app(fac(),3.into_church());println!("comparing normalizing orders' reduction step count for FAC 3:");for&orderin[NOR,APP,HNO,HAP].iter(){println!("{}: {}", order, expr.clone().reduce(order,0));}}

comparing normalizing orders' reduction step count for FAC 3:normal: 46applicative: 39hybrid normal: 46hybrid applicative: 39

Comparing different numeral encodings

use lambda_calculus::*;fnmain(){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());}

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)