use crate::value::Ternary;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub enum Algebra {
Kleene,
Lukasiewicz,
Bochvar,
}
impl Algebra {
pub const ALL: [Self; 3] = [Self::Kleene, Self::Lukasiewicz, Self::Bochvar];
pub const fn as_str(self) -> &'static str {
match self {
Self::Kleene => "kleene",
Self::Lukasiewicz => "lukasiewicz",
Self::Bochvar => "bochvar",
}
}
pub fn parse(s: &str) -> Option<Self> {
match s.trim().to_ascii_lowercase().as_str() {
"kleene" | "k3" => Some(Self::Kleene),
"lukasiewicz" | "luk" | "l3" => Some(Self::Lukasiewicz),
"bochvar" | "b3" => Some(Self::Bochvar),
_ => None,
}
}
pub const fn is_poisonous(self) -> bool {
matches!(self, Self::Bochvar)
}
pub const fn not(self, a: Ternary) -> Ternary {
match a {
Ternary::False => Ternary::True,
Ternary::Unknown => Ternary::Unknown,
Ternary::True => Ternary::False,
}
}
pub const fn and(self, a: Ternary, b: Ternary) -> Ternary {
match self {
Self::Bochvar => {
if a.is_unknown() || b.is_unknown() {
Ternary::Unknown
} else if a.is_true() && b.is_true() {
Ternary::True
} else {
Ternary::False
}
}
Self::Kleene | Self::Lukasiewicz => match (a, b) {
(Ternary::False, _) | (_, Ternary::False) => Ternary::False,
(Ternary::True, Ternary::True) => Ternary::True,
_ => Ternary::Unknown,
},
}
}
pub const fn or(self, a: Ternary, b: Ternary) -> Ternary {
match self {
Self::Bochvar => {
if a.is_unknown() || b.is_unknown() {
Ternary::Unknown
} else if a.is_true() || b.is_true() {
Ternary::True
} else {
Ternary::False
}
}
Self::Kleene | Self::Lukasiewicz => match (a, b) {
(Ternary::True, _) | (_, Ternary::True) => Ternary::True,
(Ternary::False, Ternary::False) => Ternary::False,
_ => Ternary::Unknown,
},
}
}
pub const fn strong_add(self, a: Ternary, b: Ternary) -> Ternary {
match self {
Self::Lukasiewicz => {
let s = a.as_f64() + b.as_f64();
if s >= 1.0 {
Ternary::True
} else if s <= 0.0 {
Ternary::False
} else {
Ternary::Unknown
}
}
Self::Kleene | Self::Bochvar => {
if a.is_unknown() || b.is_unknown() {
Ternary::Unknown
} else if a.is_true() && b.is_true() {
Ternary::True
} else {
Ternary::False
}
}
}
}
pub const fn strong_and(self, a: Ternary, b: Ternary) -> Ternary {
match self {
Self::Lukasiewicz => {
let s = a.as_f64() + b.as_f64() - 1.0;
if s <= 0.0 {
Ternary::False
} else if s >= 1.0 {
Ternary::True
} else {
Ternary::Unknown
}
}
Self::Kleene | Self::Bochvar => {
if a.is_unknown() || b.is_unknown() {
Ternary::Unknown
} else if a.is_true() && b.is_true() {
Ternary::True
} else {
Ternary::False
}
}
}
}
pub const fn implies(self, a: Ternary, b: Ternary) -> Ternary {
match self {
Self::Kleene => self.or(self.not(a), b),
Self::Bochvar => {
if a.is_unknown() || b.is_unknown() {
Ternary::Unknown
} else if a.is_true() {
b
} else {
Ternary::True
}
}
Self::Lukasiewicz => {
let s = 1.0 - a.as_f64() + b.as_f64();
if s >= 1.0 {
Ternary::True
} else if s <= 0.0 {
Ternary::False
} else {
Ternary::Unknown
}
}
}
}
pub const fn equiv(self, a: Ternary, b: Ternary) -> Ternary {
self.and(self.implies(a, b), self.implies(b, a))
}
}
impl std::fmt::Display for Algebra {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
f.write_str(self.as_str())
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn kleene_and_truth_table() {
use Ternary::*;
assert_eq!(Algebra::Kleene.and(False, Unknown), False);
assert_eq!(Algebra::Kleene.and(Unknown, Unknown), Unknown);
assert_eq!(Algebra::Kleene.and(Unknown, True), Unknown);
assert_eq!(Algebra::Kleene.and(True, True), True);
}
#[test]
fn bochvar_and_is_poisonous() {
use Ternary::*;
assert_eq!(Algebra::Bochvar.and(False, Unknown), Unknown);
assert_eq!(Algebra::Bochvar.and(True, Unknown), Unknown);
assert_eq!(Algebra::Bochvar.and(True, True), True);
assert_eq!(Algebra::Bochvar.and(False, False), False);
}
#[test]
fn bochvar_or_is_poisonous() {
use Ternary::*;
assert_eq!(Algebra::Bochvar.or(True, Unknown), Unknown);
assert_eq!(Algebra::Bochvar.or(False, Unknown), Unknown);
assert_eq!(Algebra::Bochvar.or(True, True), True);
}
#[test]
fn kleene_and_or_are_lattice_ops() {
for a in Ternary::ALL {
for b in Ternary::ALL {
assert_eq!(Algebra::Kleene.and(a, b), Algebra::Lukasiewicz.and(a, b));
assert_eq!(Algebra::Kleene.or(a, b), Algebra::Lukasiewicz.or(a, b));
}
}
}
#[test]
fn strong_add_differs_between_semantics() {
use Ternary::*;
assert_eq!(Algebra::Kleene.strong_add(Unknown, Unknown), Unknown);
assert_eq!(Algebra::Lukasiewicz.strong_add(Unknown, Unknown), True);
assert_eq!(Algebra::Bochvar.strong_add(Unknown, Unknown), Unknown);
assert_eq!(Algebra::Kleene.strong_add(True, False), False);
assert_eq!(Algebra::Kleene.strong_add(False, True), False);
assert_eq!(Algebra::Bochvar.strong_add(True, False), False);
assert_eq!(Algebra::Lukasiewicz.strong_add(False, True), True);
assert_eq!(Algebra::Lukasiewicz.strong_add(False, False), False);
assert_eq!(Algebra::Kleene.strong_add(True, True), True);
}
#[test]
fn strong_and_lukasiewicz_matches_formula() {
use Ternary::*;
assert_eq!(Algebra::Lukasiewicz.strong_and(Unknown, Unknown), False);
assert_eq!(Algebra::Lukasiewicz.strong_and(Unknown, True), Unknown);
assert_eq!(Algebra::Lukasiewicz.strong_and(True, True), True);
assert_eq!(Algebra::Lukasiewicz.strong_and(False, True), False);
assert_eq!(Algebra::Kleene.strong_and(Unknown, True), Unknown);
assert_eq!(Algebra::Kleene.strong_and(True, False), False);
assert_eq!(Algebra::Bochvar.strong_and(True, False), False);
assert_eq!(Algebra::Bochvar.strong_and(Unknown, True), Unknown);
}
#[test]
fn implication_differs_between_semantics() {
use Ternary::*;
assert_eq!(Algebra::Kleene.implies(Unknown, Unknown), Unknown);
assert_eq!(Algebra::Lukasiewicz.implies(Unknown, Unknown), True);
assert_eq!(Algebra::Bochvar.implies(Unknown, Unknown), Unknown);
assert_eq!(Algebra::Kleene.implies(True, False), False);
assert_eq!(Algebra::Kleene.implies(False, True), True);
assert_eq!(Algebra::Kleene.implies(False, Unknown), True);
assert_eq!(Algebra::Bochvar.implies(False, Unknown), Unknown);
assert_eq!(Algebra::Lukasiewicz.implies(False, Unknown), True);
}
#[test]
fn algebra_parsing() {
assert_eq!(Algebra::parse("K3"), Some(Algebra::Kleene));
assert_eq!(Algebra::parse("luk"), Some(Algebra::Lukasiewicz));
assert_eq!(Algebra::parse("b3"), Some(Algebra::Bochvar));
assert_eq!(Algebra::parse("nope"), None);
}
}