y_combinator/
y_combinator.rs

1//! Y Combinator
2
3use lamcalc::{lambda, Error};
4
5fn main() -> Result<(), Error> {
6    // prepare some nats
7    let zero = lambda!(f. (x. x));
8    let suc = lambda!(n. f. x. f (n f x));
9    let prev = lambda!(n. f. x. n (g. h. h (g f)) (u. x) (u. u));
10    let mut nats = vec![zero];
11    for i in 1..10 {
12        let sx = lambda!({suc} {nats[i - 1]}).simplify()?.to_owned();
13        nats.push(sx);
14        assert_eq!(
15            lambda!({prev} {nats[i]}).simplify()?.to_string(),
16            nats[i - 1].to_string()
17        );
18    }
19
20    // utilities
21    let mul = lambda!(n. m. f. x. n (m f) x);
22    let if_n_is_zero = lambda!(n. n (w. x. y. y) (x. y. x));
23
24    assert_eq!(
25        lambda!({if_n_is_zero} {nats[0]} {nats[2]} {nats[1]} )
26            .simplify()?
27            .purify(),
28        nats[2].purify()
29    );
30
31    // Y combinator
32    let mut y = lambda!(f. (x. f (x x)) (x. f (x x)));
33
34    // factorial
35    let mut fact = lambda!(y. n. {if_n_is_zero} n (f. x. f x) ({mul} n (y ({prev} n))));
36
37    eprintln!("simplify fact");
38    while fact.eval_normal_order(true) { 
39        eprintln!("fact = {}", fact);
40    }
41
42    let y_fact = lambda!({y} {fact});
43
44    let res = lambda!({y_fact} {nats[3]}).purify().simplify()?.to_owned();
45    eprintln!("{}", res);
46    assert_eq!(res, nats[6].purify());
47
48    // if you try to simplify Y combinator ...
49    eprintln!("simplify y: {}", y.simplify().unwrap_err()); // lamcalc::Error::SimplifyLimitExceeded
50
51    Ok(())
52}
y_combinator/y_combinator.rs

y_combinator/
y_combinator.rs
