lambda_calculus 0.4.1

A simple implementation of the untyped lambda calculus in Rust.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

//! [Church booleans](https://en.wikipedia.org/wiki/Church_encoding#Church_Booleans)

use term::*;
use term::Term::*;

/// A Church-encoded boolean `true`.
///
/// TRUE := λab.a = λ λ 2
pub fn tru() -> Term { abs(abs(Var(2))) }

/// A Church-encoded boolean `false`.
///
/// FALSE := λab.b = λ λ 1
pub fn fls() -> Term { abs(abs(Var(1))) }

/// Applied to two Church-encoded booleans it returns their Church-encoded conjunction.
///
/// AND := λpq.p q p = λ λ 2 1 2
///
/// # Examples
/// ```
/// use lambda_calculus::booleans::{and, tru, fls};
/// use lambda_calculus::reduction::beta_full;
///
/// assert_eq!(beta_full(and().app(tru()).app(tru())), tru());
/// assert_eq!(beta_full(and().app(tru()).app(fls())), fls());
/// assert_eq!(beta_full(and().app(fls()).app(tru())), fls());
/// assert_eq!(beta_full(and().app(fls()).app(fls())), fls());
/// ```
pub fn and() -> Term {
    abs(abs(
        Var(2)
        .app(Var(1))
        .app(Var(2))
    ))
}

/// Applied to two Church-encoded booleans it returns their Church-encoded disjunction.
///
/// OR := λpq.p p q = λ λ 2 2 1
///
/// # Examples
/// ```
/// use lambda_calculus::booleans::{or, tru, fls};
/// use lambda_calculus::reduction::beta_full;
///
/// assert_eq!(beta_full(or().app(tru()).app(tru())), tru());
/// assert_eq!(beta_full(or().app(tru()).app(fls())), tru());
/// assert_eq!(beta_full(or().app(fls()).app(tru())), tru());
/// assert_eq!(beta_full(or().app(fls()).app(fls())), fls());
/// ```
pub fn or() -> Term {
    abs(abs(
        Var(2)
        .app(Var(2))
        .app(Var(1))
    ))
}

/// Applied to a Church-encoded boolean it returns its Church-encoded negation.
///
/// NOT := λp.p FALSE TRUE = λ 1 FALSE TRUE
///
/// # Examples
/// ```
/// use lambda_calculus::booleans::{not, tru, fls};
/// use lambda_calculus::reduction::beta_full;
///
/// assert_eq!(beta_full(not().app(tru())), fls());
/// assert_eq!(beta_full(not().app(fls())), tru());
/// ```
pub fn not() -> Term {
    abs(
        Var(1)
        .app(fls())
        .app(tru())
    )
}

/// Applied to a Church-encoded boolean it returns its Church-encoded exclusive disjunction.
///
/// XOR := λab.a (NOT b) b = λ λ 2 (NOT 1) 1
///
/// # Examples
/// ```
/// use lambda_calculus::booleans::{xor, tru, fls};
/// use lambda_calculus::reduction::beta_full;
///
/// assert_eq!(beta_full(xor().app(tru()).app(tru())), fls());
/// assert_eq!(beta_full(xor().app(tru()).app(fls())), tru());
/// assert_eq!(beta_full(xor().app(fls()).app(tru())), tru());
/// assert_eq!(beta_full(xor().app(fls()).app(fls())), fls());
/// ```
pub fn xor() -> Term {
    abs(abs(
        Var(2)
        .app(not().app(Var(1)))
        .app(Var(1))
    ))
}

/// Applied to a Church encoded predicate and two terms it returns the first one if the predicate
/// is true or the second one if the predicate is false.
///
/// IF_ELSE := λpab.p a b = λ λ λ 3 2 1
///
/// # Examples
/// ```
/// use lambda_calculus::booleans::{if_else, tru, fls};
/// use lambda_calculus::arithmetic::{zero, one};
/// use lambda_calculus::reduction::beta_full;
///
/// assert_eq!(beta_full(if_else().app(tru()).app(one()).app(zero())), one());
/// assert_eq!(beta_full(if_else().app(fls()).app(one()).app(zero())), zero());
/// ```
pub fn if_else() -> Term {
    abs(abs(abs(
        Var(3)
        .app(Var(2))
        .app(Var(1))
    )))
}