boolean.rs

/// Sets that form a boolean algebra.
/// 
/// These must contain exactly two elements, top and bottom: `{⊤, ⊥}`, and be
/// equipped with three basic operators: `¬`, `∧`, and `∨`, the definitions of
/// which are outlined below.
pub trait Boolean: Eq {
    /// The bottom value, `⊥`.
    fn bottom() -> Self;

    /// The top value, `⊤`.
    #[inline]
    fn top() -> Self { not(&bottom()) }

    /// The logical complement, `¬`.
    ///
    /// # Truth table
    ///
    /// ~~~ignore
    ///   p        ¬p
    /// +--------+--------+
    /// | top    | bottom |
    /// | bottom | top    |
    /// +--------+--------+
    /// ~~~
    fn not(p: &Self) -> Self;

    /// Logical conjunction, `∧`.
    ///
    /// # Truth table
    ///
    /// ~~~ignore
    ///   p        q        p ∧ q
    /// +-----------------+--------+
    /// | top      top    | top    |
    /// | top      bottom | bottom |
    /// | bottom   top    | bottom |
    /// | bottom   bottom | bottom |
    /// +-----------------+--------+
    /// ~~~
    fn and(p: &Self, q: &Self) -> Self;

    /// Logical disjunction, `∨`.
    ///
    /// # Truth table
    ///
    /// ~~~ignore
    ///   p        q        p ∨ q
    /// +-----------------+--------+
    /// | top      top    | bottom |
    /// | top      bottom | top    |
    /// | bottom   top    | top    |
    /// | bottom   bottom | top    |
    /// +-----------------+--------+
    /// ~~~
    fn or(p: &Self, q: &Self) -> Self;

    /// Exclusive disjunction, `⊕`, where:
    ///
    /// ~~~ignore
    /// p ⊕ q = (p ∨ q) ∧ ¬(p ∧ q)
    /// ~~~
    ///
    /// # Truth table
    ///
    /// ~~~ignore
    ///   p        q        p ⊕ q
    /// +-----------------+--------+
    /// | top      top    | bottom |
    /// | top      bottom | top    |
    /// | bottom   top    | top    |
    /// | bottom   bottom | bottom |
    /// +-----------------+--------+
    /// ~~~
    #[inline]
    fn xor(p: &Self, q: &Self) -> Self { and(&or(p, q), &not(&and(p, q))) }

    /// Material implication, `→`, where:
    ///
    /// ~~~ignore
    /// p → q = ¬p ∨ q
    /// ~~~
    ///
    /// # Truth table
    ///
    /// ~~~ignore
    ///   p        q        p → q
    /// +-----------------+--------+
    /// | top      top    | top    |
    /// | top      bottom | bottom |
    /// | bottom   top    | top    |
    /// | bottom   bottom | top    |
    /// +-----------------+--------+
    /// ~~~
    #[inline]
    fn implies(p: &Self, q: &Self) -> Self { or(&not(p), q) }

    /// Material biconditional, `≡`, where:
    ///
    /// ~~~ignore
    /// p ≡ q = ¬(p ⊕ q)
    /// ~~~
    ///
    /// # Truth table
    ///
    /// ~~~ignore
    ///   p        q        p ≡ q
    /// +-----------------+--------+
    /// | top      top    | top    |
    /// | top      bottom | bottom |
    /// | bottom   top    | bottom |
    /// | bottom   bottom | top    |
    /// +-----------------+--------+
    /// ~~~
    #[inline]
    fn iff(p: &Self, q: &Self) -> Self { not(&xor(p, q)) }

    /// Converts a value to the corresponding `⊥` and `⊤` value from
    /// another boolean algebra.
    #[inline]
    fn to_boolean<T: Boolean>(&self) -> T {
        if *self == top() { top() } else { bottom() }
    }

    /// Converts the value either `zero` or `one` in a set that has those
    /// elements defined.
    ///
    /// # Example
    ///
    /// ~~~
    /// use num::Boolean;
    ///
    /// assert_eq!(true.to_bit::<u8>(), 1);
    /// assert_eq!(false.to_bit::<u8>(), 0);
    /// ~~~
    #[inline]
    fn to_bit<T: Zero + One>(&self) -> T {
        if *self == top() { one() } else { zero() }
    }
}

/// The truth value, `⊤`.
#[inline] pub fn top<T: Boolean>() -> T { Boolean::top() }
/// The false value, `⊥`.
#[inline] pub fn bottom<T: Boolean>() -> T { Boolean::bottom() }
/// The logical complement, `¬`.
#[inline] pub fn not<T: Boolean>(p: &T) -> T { Boolean::not(p) }
/// Logical conjunction, `∧`.
#[inline] pub fn and<T: Boolean>(p: &T, q: &T) -> T { Boolean::and(p, q) }
/// Logical disjunction, `∨`.
#[inline] pub fn or<T: Boolean>(p: &T, q: &T) -> T { Boolean::or(p, q) }
/// Exclusive disjunction, `⊕`.
#[inline] pub fn xor<T: Boolean>(p: &T, q: &T) -> T { Boolean::xor(p, q) }
/// Material implication, `→`.
#[inline] pub fn implies<T: Boolean>(p: &T, q: &T) -> T { Boolean::implies(p, q) }
/// Logical biconditional, `≡`.
#[inline] pub fn iff<T: Boolean>(p: &T, q: &T) -> T { Boolean::iff(p, q) }

impl Boolean for bool {
    #[inline] fn bottom() -> bool { false }
    #[inline] fn top() -> bool { true }
    #[inline] fn not(&p: &Self) -> Self { !p }
    #[inline] fn and(&p: &Self, &q: &Self) -> Self { p & q }
    #[inline] fn or(&p: &Self, &q: &Self) -> Self { p | q }
    #[inline] fn xor(&p: &Self, &q: &Self) -> Self { p ^ q }
    #[inline] fn iff(&p: &Self, &q: &Self) -> Self { p == q }
}