beta_reduce/
beta_reduce.rs

1use lamcalc::lambda;
2
3fn main() {
4    let and = lambda!(x. y. (x y x));
5    let tt = lambda!(x. (y. x));
6    let ff = lambda!(x. (y. y));
7    let mut exp = lambda!({and} {tt} {ff});
8
9    eprintln!("exp = {}", exp); // ((λx. λy. (x y) x) λx. λy. x) λx. λy. y
10
11    assert!(exp.into_app().unwrap().0.is_beta_redex());
12    assert!(exp.into_app().unwrap().0.beta_reduce());
13    eprintln!("exp = {}", exp); // (λy. ((λx. λy. x) y) λx. λy. x) λx. λy. y
14
15    assert!(exp
16        .into_app()
17        .unwrap()
18        .0 // λy. ((λx. λy. x) y) λx. λy. x
19        .into_abs()
20        .unwrap()
21        .1 // ((λx. λy. x) y) λx. λy. x
22        .into_app()
23        .unwrap()
24        .0 // (λx. λy. x) y
25        .beta_reduce());
26    eprintln!("exp = {}", exp); // (λy. (λy. y) λx. λy. x) λx. λy. y
27
28    assert!(exp
29        .into_app()
30        .unwrap()
31        .0 // λy. (λy. y) λx. λy. x
32        .into_abs()
33        .unwrap()
34        .1 // (λy. y) λx. λy. x
35        .beta_reduce());
36    eprintln!("exp = {}", exp); // (λy. y) λx. λy. y
37
38    assert!(exp.beta_reduce());
39    eprintln!("exp = {}", exp); // λx. λy. y
40}