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 129 130 131 132 133 134 135 136 137 138
//! [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 /// ``` /// # #[macro_use] extern crate lambda_calculus; /// # fn main() { /// use lambda_calculus::booleans::{and, tru, fls}; /// use lambda_calculus::reduction::beta; /// use lambda_calculus::reduction::Order::*; /// /// assert_eq!(beta(app!(and(), tru(), tru()), &Normal, 0), tru()); /// assert_eq!(beta(app!(and(), tru(), fls()), &Normal, 0), fls()); /// assert_eq!(beta(app!(and(), fls(), tru()), &Normal, 0), fls()); /// assert_eq!(beta(app!(and(), fls(), fls()), &Normal, 0), fls()); /// # } /// ``` pub fn and() -> Term { abs(abs( app!(Var(2), Var(1), Var(2)) )) } /// Applied to two Church-encoded booleans it returns their Church-encoded disjunction. /// /// OR := λpq.p p q = λ λ 2 2 1 /// /// # Examples /// ``` /// # #[macro_use] extern crate lambda_calculus; /// # fn main() { /// use lambda_calculus::booleans::{or, tru, fls}; /// use lambda_calculus::reduction::beta; /// use lambda_calculus::reduction::Order::*; /// /// assert_eq!(beta(app!(or(), tru(), tru()), &Normal, 0), tru()); /// assert_eq!(beta(app!(or(), tru(), fls()), &Normal, 0), tru()); /// assert_eq!(beta(app!(or(), fls(), tru()), &Normal, 0), tru()); /// assert_eq!(beta(app!(or(), fls(), fls()), &Normal, 0), fls()); /// # } /// ``` pub fn or() -> Term { abs(abs( app!(Var(2), Var(2), Var(1)) )) } /// Applied to a Church-encoded boolean it returns its Church-encoded negation. /// /// NOT := λp.p FALSE TRUE = λ 1 FALSE TRUE /// /// # Examples /// ``` /// # #[macro_use] extern crate lambda_calculus; /// # fn main() { /// use lambda_calculus::booleans::{not, tru, fls}; /// use lambda_calculus::reduction::beta; /// use lambda_calculus::reduction::Order::*; /// /// assert_eq!(beta(app!(not(), tru()), &Normal, 0), fls()); /// assert_eq!(beta(app!(not(), fls()), &Normal, 0), tru()); /// # } /// ``` pub fn not() -> Term { abs( app!(Var(1), fls(), 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 /// ``` /// # #[macro_use] extern crate lambda_calculus; /// # fn main() { /// use lambda_calculus::booleans::{xor, tru, fls}; /// use lambda_calculus::reduction::beta; /// use lambda_calculus::reduction::Order::*; /// /// assert_eq!(beta(app!(xor(), tru(), tru()), &Normal, 0), fls()); /// assert_eq!(beta(app!(xor(), tru(), fls()), &Normal, 0), tru()); /// assert_eq!(beta(app!(xor(), fls(), tru()), &Normal, 0), tru()); /// assert_eq!(beta(app!(xor(), fls(), fls()), &Normal, 0), fls()); /// # } /// ``` pub fn xor() -> Term { abs(abs( app!(Var(2), app(not(), Var(1)), 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 /// ``` /// # #[macro_use] extern crate lambda_calculus; /// # fn main() { /// use lambda_calculus::booleans::{if_else, tru, fls}; /// use lambda_calculus::arithmetic::{zero, one}; /// use lambda_calculus::reduction::beta; /// use lambda_calculus::reduction::Order::*; /// /// assert_eq!(beta(app!(if_else(), tru(), one(), zero()), &Normal, 0), one()); /// assert_eq!(beta(app!(if_else(), fls(), one(), zero()), &Normal, 0), zero()); /// # } /// ``` pub fn if_else() -> Term { abs(abs(abs( app!(Var(3), Var(2), Var(1)) ))) } impl From<bool> for Term { fn from(b: bool) -> Self { if b { tru() } else { fls() } } }