delhi_syntax/
sugar.rs

1//! Derived attitudes (§8.4). Every one is a boolean combination of the six
2//! primitives, so `delhi-mb` never sees them.
3
4use crate::{AgentId, FormulaId, Store};
5
6impl Store {
7    /// `Kw[i]φ` — agent knows whether φ is true: `K[i]φ | K[i]!φ`.
8    pub fn knows_whether(&mut self, i: AgentId, f: FormulaId) -> FormulaId {
9        let nf = self.not(f);
10        let a = self.knows(i, f);
11        let b = self.knows(i, nf);
12        self.or(a, b)
13    }
14    /// `Bw[i]φ` — agent has a belief either way: `B[i]φ | B[i]!φ`.
15    pub fn believes_whether(&mut self, i: AgentId, f: FormulaId) -> FormulaId {
16        let nf = self.not(f);
17        let a = self.believes(i, f);
18        let b = self.believes(i, nf);
19        self.or(a, b)
20    }
21    /// `?[i]φ` — agent is ignorant whether: `!K[i]φ & !K[i]!φ`.
22    pub fn ignorant(&mut self, i: AgentId, f: FormulaId) -> FormulaId {
23        let kw = self.knows_whether(i, f);
24        self.not(kw)
25    }
26    /// `¿[i]φ` — agent suspends judgement: `!B[i]φ & !B[i]!φ`.
27    pub fn undecided(&mut self, i: AgentId, f: FormulaId) -> FormulaId {
28        let bw = self.believes_whether(i, f);
29        self.not(bw)
30    }
31    /// `K'[i]φ` — agent considers φ possible: `!K[i]!φ`.
32    pub fn considers_possible(&mut self, i: AgentId, f: FormulaId) -> FormulaId {
33        let nf = self.not(f);
34        let k = self.knows(i, nf);
35        self.not(k)
36    }
37    /// `B'[i]φ` — agent has not ruled out φ: `!B[i]!φ`.
38    pub fn not_ruled_out(&mut self, i: AgentId, f: FormulaId) -> FormulaId {
39        let nf = self.not(f);
40        let b = self.believes(i, nf);
41        self.not(b)
42    }
43    /// `S'[i]φ` — φ is safe for agent to act on: `!□[i]!φ`.
44    pub fn safe_dual(&mut self, i: AgentId, f: FormulaId) -> FormulaId {
45        let nf = self.not(f);
46        let s = self.safe(i, nf);
47        self.not(s)
48    }
49    /// `K[a,b,…]φ` — all agents in the list know φ.
50    pub fn knows_all(&mut self, agents: &[AgentId], f: FormulaId) -> FormulaId {
51        let mut parts = Vec::with_capacity(agents.len());
52        for &i in agents {
53            parts.push(self.knows(i, f));
54        }
55        self.all(&parts)
56    }
57    /// `B[a,b,…]φ` — all agents in the list believe φ.
58    pub fn believes_all(&mut self, agents: &[AgentId], f: FormulaId) -> FormulaId {
59        let mut parts = Vec::with_capacity(agents.len());
60        for &i in agents {
61            parts.push(self.believes(i, f));
62        }
63        self.all(&parts)
64    }
65}
66
67#[cfg(test)]
68mod tests {
69    use crate::{Node, Store};
70
71    #[test]
72    fn knows_whether_is_a_disjunction_of_knows() {
73        let mut s = Store::default();
74        let p = s.atom(0);
75        let kw = s.knows_whether(0, p);
76        let np = s.not(p);
77        let expect = {
78            let a = s.knows(0, p);
79            let b = s.knows(0, np);
80            s.or(a, b)
81        };
82        assert_eq!(kw, expect);
83    }
84
85    #[test]
86    fn ignorant_is_neither_knows() {
87        let mut s = Store::default();
88        let p = s.atom(0);
89        let ig = s.ignorant(0, p);
90        // ignorant is exactly !knows_whether
91        let kw = s.knows_whether(0, p);
92        let expect = s.not(kw);
93        assert_eq!(ig, expect);
94    }
95
96    #[test]
97    fn agent_lists_distribute_over_knows() {
98        let mut s = Store::default();
99        let p = s.atom(0);
100        let ka = s.knows(0, p);
101        let kb = s.knows(1, p);
102        let expect = s.and(ka, kb);
103        assert_eq!(s.knows_all(&[0, 1], p), expect);
104    }
105
106    #[test]
107    fn cond_bel_on_top_is_plain_belief() {
108        // §4.2: `B[i]φ ≡ B^⊤[i]φ` is asserted here syntactically only;
109        // Task 14 checks it semantically.
110        let mut s = Store::default();
111        let p = s.atom(0);
112        let t = s.tru();
113        let cb = s.cond_bel(0, t, p);
114        assert!(matches!(s.node(cb), Node::CondBel(0, _, _)));
115    }
116
117    #[test]
118    fn duals_negate_on_both_sides() {
119        let mut s = Store::default();
120        let p = s.atom(0);
121        let np = s.not(p);
122
123        let expect_k = {
124            let k = s.knows(0, np);
125            s.not(k)
126        };
127        assert_eq!(s.considers_possible(0, p), expect_k, "K'[a]p is !K[a]!p");
128
129        let expect_b = {
130            let b = s.believes(0, np);
131            s.not(b)
132        };
133        assert_eq!(s.not_ruled_out(0, p), expect_b, "B'[a]p is !B[a]!p");
134
135        let expect_s = {
136            let sf = s.safe(0, np);
137            s.not(sf)
138        };
139        assert_eq!(s.safe_dual(0, p), expect_s, "S'[a]p is ![][a]!p");
140    }
141
142    #[test]
143    fn believes_whether_and_undecided_are_complementary() {
144        let mut s = Store::default();
145        let p = s.atom(0);
146        let np = s.not(p);
147        let expect_bw = {
148            let a = s.believes(0, p);
149            let b = s.believes(0, np);
150            s.or(a, b)
151        };
152        assert_eq!(s.believes_whether(0, p), expect_bw);
153        let bw = s.believes_whether(0, p);
154        let expect_un = s.not(bw);
155        assert_eq!(s.undecided(0, p), expect_un, "undecided is the negation of believes-whether");
156    }
157
158    #[test]
159    fn believes_all_distributes_over_agents() {
160        let mut s = Store::default();
161        let p = s.atom(0);
162        let expect = {
163            let a = s.believes(0, p);
164            let b = s.believes(1, p);
165            s.and(a, b)
166        };
167        assert_eq!(s.believes_all(&[0, 1], p), expect);
168    }
169}
delhi_syntax/sugar.rs

delhi_syntax/
sugar.rs
