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::normalize; /// /// assert_eq!(normalize(and().app(tru()).app(tru())), tru()); /// assert_eq!(normalize(and().app(tru()).app(fls())), fls()); /// assert_eq!(normalize(and().app(fls()).app(tru())), fls()); /// assert_eq!(normalize(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::normalize; /// /// assert_eq!(normalize(or().app(tru()).app(tru())), tru()); /// assert_eq!(normalize(or().app(tru()).app(fls())), tru()); /// assert_eq!(normalize(or().app(fls()).app(tru())), tru()); /// assert_eq!(normalize(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::normalize; /// /// assert_eq!(normalize(not().app(tru())), fls()); /// assert_eq!(normalize(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::normalize; /// /// assert_eq!(normalize(xor().app(tru()).app(tru())), fls()); /// assert_eq!(normalize(xor().app(tru()).app(fls())), tru()); /// assert_eq!(normalize(xor().app(fls()).app(tru())), tru()); /// assert_eq!(normalize(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::normalize; /// /// assert_eq!(normalize(if_else().app(tru()).app(one()).app(zero())), one()); /// assert_eq!(normalize(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)) ))) }