Skip to main content

qualia_core_db/modalities/likeliness/
inference.rs

1//! Naive inference and defeasible revision over likeliness — the "specific update rule"
2//! half of the calculus. Built on the [`super::algebra`] lattice so the laws are
3//! inherited (reuse, not a parallel set of rules).
4
5use super::algebra::{and, not, or};
6use super::Likeliness;
7
8/// Lower a likeliness by `steps` ordinal levels — chain attenuation. Saturating at
9/// `Impossible`.
10pub fn attenuate(l: Likeliness, steps: u8) -> Likeliness {
11    Likeliness::from_level(l.level().saturating_sub(steps as i8))
12}
13
14/// **Naive modus ponens.** From a premise `p` (how expected it is to hold) and a rule's
15/// reliability `r` (how expected it is that `p ⇒ q`), the conclusion `q` is `and(p, r)`
16/// — inference never produces a conclusion stronger than its weakest input.
17pub fn modus_ponens(premise: Likeliness, rule_reliability: Likeliness) -> Likeliness {
18    and(premise, rule_reliability)
19}
20
21/// Inference along a chain of default rules from a premise: the weakest link, then
22/// **attenuated by the number of inferential steps beyond the first**. Longer defeasible
23/// chains weaken — the qualitative analogue of multiplying probabilities along a path.
24/// An empty rule list returns the premise unchanged.
25pub fn infer_chain(premise: Likeliness, rule_reliabilities: &[Likeliness]) -> Likeliness {
26    if rule_reliabilities.is_empty() {
27        return premise;
28    }
29    let weakest = rule_reliabilities.iter().copied().fold(premise, and);
30    attenuate(weakest, (rule_reliabilities.len() as u8).saturating_sub(1))
31}
32
33/// **Rebuttal.** A counter-argument of strength `counter` (how expected it is that the
34/// conclusion is *false*) caps the conclusion at `not(counter)`. A strong rebuttal
35/// defeats: a `Certain` conclusion rebutted by a `Likely` counter falls to `Unlikely`.
36pub fn rebut(conclusion: Likeliness, counter: Likeliness) -> Likeliness {
37    and(conclusion, not(counter))
38}
39
40/// **Defeasible revision.** Fold a new supporting route and a rebuttal into a prior:
41/// `and(or(prior, support), not(against))`. The support is an alternative route
42/// (best-of), and the rebuttal caps the result. Symmetric in the sense that a strong
43/// `against` overrides any amount of `support`.
44pub fn revise(prior: Likeliness, support: Likeliness, against: Likeliness) -> Likeliness {
45    and(or(prior, support), not(against))
46}
47
48#[cfg(test)]
49mod tests {
50    use super::*;
51    use Likeliness::*;
52
53    #[test]
54    fn modus_ponens_is_weakest_link() {
55        // "p is Likely" + "p⇒q is VeryLikely" → q is Likely.
56        assert_eq!(modus_ponens(Likely, VeryLikely), Likely);
57        // A certain rule cannot rescue an unlikely premise.
58        assert_eq!(modus_ponens(Unlikely, Certain), Unlikely);
59    }
60
61    #[test]
62    fn chains_attenuate_with_length() {
63        // One step: just the weakest link.
64        assert_eq!(infer_chain(Certain, &[Likely]), Likely);
65        // Three Certain rules from a Certain premise → Certain weakest, attenuated by 2.
66        assert_eq!(infer_chain(Certain, &[Certain, Certain, Certain]), Likely);
67        // Empty chain is identity.
68        assert_eq!(infer_chain(VeryLikely, &[]), VeryLikely);
69    }
70
71    #[test]
72    fn rebuttal_defeats_in_proportion_to_strength() {
73        // A Certain conclusion, rebutted by a Likely counter → Unlikely.
74        assert_eq!(rebut(Certain, Likely), Unlikely);
75        // A weak counter barely dents a strong conclusion.
76        assert_eq!(rebut(Certain, Unlikely), Likely);
77        // No counter (Impossible that it's false) leaves it untouched.
78        assert_eq!(rebut(Likely, Impossible), Likely);
79    }
80
81    #[test]
82    fn revision_combines_support_and_rebuttal() {
83        // Supporting route lifts a weak prior; no rebuttal.
84        assert_eq!(revise(Unlikely, Likely, Impossible), Likely);
85        // A strong rebuttal overrides strong support.
86        assert_eq!(revise(Likely, VeryLikely, Likely), Unlikely);
87        // Neither support nor rebuttal → prior unchanged.
88        assert_eq!(revise(Even, Impossible, Impossible), Even);
89    }
90
91    #[test]
92    fn attenuate_saturates() {
93        assert_eq!(attenuate(Unlikely, 10), Impossible);
94        assert_eq!(attenuate(Likely, 1), Even);
95    }
96}