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}