Skip to content

Instantly share code, notes, and snippets.

@brendanzab

brendanzab/boolean.rs

Last active Aug 29, 2015
Embed
What would you like to do?
/// 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 }
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment