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
123
124
125
126
127
128

//! [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))
    )))
}

impl From<bool> for Term {
    fn from(b: bool) -> Self {
        if b { tru() } else { fls() }
    }
}