tensorlogic_ir/expr/
distributive_laws.rs

1//! Distributive law transformations for logical expressions.
2//!
3//! This module implements distributive law transformations that can convert expressions
4//! between equivalent forms, which is useful for optimization and normalization.
5//!
6//! # Distributive Laws
7//!
8//! ## Basic Distributive Laws
9//! - **AND over OR**: A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C)
10//! - **OR over AND**: A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)
11//!
12//! ## Quantifier Distribution
13//! - **∀ over ∧**: ∀x.(P(x) ∧ Q(x)) ≡ (∀x.P(x)) ∧ (∀x.Q(x))
14//! - **∃ over ∨**: ∃x.(P(x) ∨ Q(x)) ≡ (∃x.P(x)) ∨ (∃x.Q(x))
15//!
16//! ## Modal Distribution
17//! - **□ over ∧**: □(P ∧ Q) ≡ □P ∧ □Q
18//! - **◇ over ∨**: ◇(P ∨ Q) ≡ ◇P ∨ ◇Q
19
20use super::TLExpr;
21
22/// Strategy for applying distributive laws.
23#[derive(Clone, Copy, Debug, PartialEq, Eq)]
24pub enum DistributiveStrategy {
25    /// Distribute AND over OR: A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
26    AndOverOr,
27    /// Distribute OR over AND: A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C)
28    OrOverAnd,
29    /// Distribute quantifiers when possible
30    Quantifiers,
31    /// Distribute modal operators
32    Modal,
33    /// Apply all distributive laws
34    All,
35}
36
37/// Apply distributive laws to an expression.
38///
39/// # Arguments
40/// * `expr` - The expression to transform
41/// * `strategy` - Which distributive laws to apply
42///
43/// # Returns
44/// A transformed expression with distributive laws applied.
45pub fn apply_distributive_laws(expr: &TLExpr, strategy: DistributiveStrategy) -> TLExpr {
46    match strategy {
47        DistributiveStrategy::AndOverOr => distribute_and_over_or(expr),
48        DistributiveStrategy::OrOverAnd => distribute_or_over_and(expr),
49        DistributiveStrategy::Quantifiers => distribute_quantifiers(expr),
50        DistributiveStrategy::Modal => distribute_modal(expr),
51        DistributiveStrategy::All => {
52            let mut result = expr.clone();
53            result = distribute_and_over_or(&result);
54            result = distribute_or_over_and(&result);
55            result = distribute_quantifiers(&result);
56            result = distribute_modal(&result);
57            result
58        }
59    }
60}
61
62/// Distribute AND over OR: A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
63fn distribute_and_over_or(expr: &TLExpr) -> TLExpr {
64    match expr {
65        // A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
66        TLExpr::And(a, b) if matches!(**b, TLExpr::Or(_, _)) => {
67            if let TLExpr::Or(b1, b2) = &**b {
68                let left = TLExpr::and(distribute_and_over_or(a), distribute_and_over_or(b1));
69                let right = TLExpr::and(distribute_and_over_or(a), distribute_and_over_or(b2));
70                TLExpr::or(left, right)
71            } else {
72                expr.clone()
73            }
74        }
75        // (A ∨ B) ∧ C → (A ∧ C) ∨ (B ∧ C)
76        TLExpr::And(a, c) if matches!(**a, TLExpr::Or(_, _)) => {
77            if let TLExpr::Or(a1, a2) = &**a {
78                let left = TLExpr::and(distribute_and_over_or(a1), distribute_and_over_or(c));
79                let right = TLExpr::and(distribute_and_over_or(a2), distribute_and_over_or(c));
80                TLExpr::or(left, right)
81            } else {
82                expr.clone()
83            }
84        }
85        // Recursively apply to subexpressions
86        TLExpr::And(l, r) => TLExpr::and(distribute_and_over_or(l), distribute_and_over_or(r)),
87        TLExpr::Or(l, r) => TLExpr::or(distribute_and_over_or(l), distribute_and_over_or(r)),
88        TLExpr::Not(e) => TLExpr::negate(distribute_and_over_or(e)),
89        TLExpr::Imply(l, r) => TLExpr::imply(distribute_and_over_or(l), distribute_and_over_or(r)),
90        TLExpr::Exists { var, domain, body } => {
91            TLExpr::exists(var.clone(), domain.clone(), distribute_and_over_or(body))
92        }
93        TLExpr::ForAll { var, domain, body } => {
94            TLExpr::forall(var.clone(), domain.clone(), distribute_and_over_or(body))
95        }
96        TLExpr::Box(e) => TLExpr::modal_box(distribute_and_over_or(e)),
97        TLExpr::Diamond(e) => TLExpr::modal_diamond(distribute_and_over_or(e)),
98        TLExpr::Next(e) => TLExpr::next(distribute_and_over_or(e)),
99        TLExpr::Eventually(e) => TLExpr::eventually(distribute_and_over_or(e)),
100        TLExpr::Always(e) => TLExpr::always(distribute_and_over_or(e)),
101        TLExpr::Until { before, after } => TLExpr::until(
102            distribute_and_over_or(before),
103            distribute_and_over_or(after),
104        ),
105        _ => expr.clone(),
106    }
107}
108
109/// Distribute OR over AND: A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C)
110fn distribute_or_over_and(expr: &TLExpr) -> TLExpr {
111    match expr {
112        // A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C)
113        TLExpr::Or(a, b) if matches!(**b, TLExpr::And(_, _)) => {
114            if let TLExpr::And(b1, b2) = &**b {
115                let left = TLExpr::or(distribute_or_over_and(a), distribute_or_over_and(b1));
116                let right = TLExpr::or(distribute_or_over_and(a), distribute_or_over_and(b2));
117                TLExpr::and(left, right)
118            } else {
119                expr.clone()
120            }
121        }
122        // (A ∧ B) ∨ C → (A ∨ C) ∧ (B ∨ C)
123        TLExpr::Or(a, c) if matches!(**a, TLExpr::And(_, _)) => {
124            if let TLExpr::And(a1, a2) = &**a {
125                let left = TLExpr::or(distribute_or_over_and(a1), distribute_or_over_and(c));
126                let right = TLExpr::or(distribute_or_over_and(a2), distribute_or_over_and(c));
127                TLExpr::and(left, right)
128            } else {
129                expr.clone()
130            }
131        }
132        // Recursively apply to subexpressions
133        TLExpr::And(l, r) => TLExpr::and(distribute_or_over_and(l), distribute_or_over_and(r)),
134        TLExpr::Or(l, r) => TLExpr::or(distribute_or_over_and(l), distribute_or_over_and(r)),
135        TLExpr::Not(e) => TLExpr::negate(distribute_or_over_and(e)),
136        TLExpr::Imply(l, r) => TLExpr::imply(distribute_or_over_and(l), distribute_or_over_and(r)),
137        TLExpr::Exists { var, domain, body } => {
138            TLExpr::exists(var.clone(), domain.clone(), distribute_or_over_and(body))
139        }
140        TLExpr::ForAll { var, domain, body } => {
141            TLExpr::forall(var.clone(), domain.clone(), distribute_or_over_and(body))
142        }
143        TLExpr::Box(e) => TLExpr::modal_box(distribute_or_over_and(e)),
144        TLExpr::Diamond(e) => TLExpr::modal_diamond(distribute_or_over_and(e)),
145        TLExpr::Next(e) => TLExpr::next(distribute_or_over_and(e)),
146        TLExpr::Eventually(e) => TLExpr::eventually(distribute_or_over_and(e)),
147        TLExpr::Always(e) => TLExpr::always(distribute_or_over_and(e)),
148        TLExpr::Until { before, after } => TLExpr::until(
149            distribute_or_over_and(before),
150            distribute_or_over_and(after),
151        ),
152        _ => expr.clone(),
153    }
154}
155
156/// Distribute quantifiers: ∀x.(P(x) ∧ Q(x)) → (∀x.P(x)) ∧ (∀x.Q(x))
157fn distribute_quantifiers(expr: &TLExpr) -> TLExpr {
158    match expr {
159        // ∀x.(P(x) ∧ Q(x)) → (∀x.P(x)) ∧ (∀x.Q(x))
160        TLExpr::ForAll { var, domain, body } if matches!(**body, TLExpr::And(_, _)) => {
161            if let TLExpr::And(p, q) = &**body {
162                let left = TLExpr::forall(var.clone(), domain.clone(), distribute_quantifiers(p));
163                let right = TLExpr::forall(var.clone(), domain.clone(), distribute_quantifiers(q));
164                TLExpr::and(left, right)
165            } else {
166                expr.clone()
167            }
168        }
169        // ∃x.(P(x) ∨ Q(x)) → (∃x.P(x)) ∨ (∃x.Q(x))
170        TLExpr::Exists { var, domain, body } if matches!(**body, TLExpr::Or(_, _)) => {
171            if let TLExpr::Or(p, q) = &**body {
172                let left = TLExpr::exists(var.clone(), domain.clone(), distribute_quantifiers(p));
173                let right = TLExpr::exists(var.clone(), domain.clone(), distribute_quantifiers(q));
174                TLExpr::or(left, right)
175            } else {
176                expr.clone()
177            }
178        }
179        // Recursively apply to subexpressions
180        TLExpr::And(l, r) => TLExpr::and(distribute_quantifiers(l), distribute_quantifiers(r)),
181        TLExpr::Or(l, r) => TLExpr::or(distribute_quantifiers(l), distribute_quantifiers(r)),
182        TLExpr::Not(e) => TLExpr::negate(distribute_quantifiers(e)),
183        TLExpr::Imply(l, r) => TLExpr::imply(distribute_quantifiers(l), distribute_quantifiers(r)),
184        TLExpr::Exists { var, domain, body } => {
185            TLExpr::exists(var.clone(), domain.clone(), distribute_quantifiers(body))
186        }
187        TLExpr::ForAll { var, domain, body } => {
188            TLExpr::forall(var.clone(), domain.clone(), distribute_quantifiers(body))
189        }
190        TLExpr::Box(e) => TLExpr::modal_box(distribute_quantifiers(e)),
191        TLExpr::Diamond(e) => TLExpr::modal_diamond(distribute_quantifiers(e)),
192        _ => expr.clone(),
193    }
194}
195
196/// Distribute modal operators: □(P ∧ Q) → □P ∧ □Q
197fn distribute_modal(expr: &TLExpr) -> TLExpr {
198    match expr {
199        // □(P ∧ Q) → □P ∧ □Q
200        TLExpr::Box(body) if matches!(**body, TLExpr::And(_, _)) => {
201            if let TLExpr::And(p, q) = &**body {
202                let left = TLExpr::modal_box(distribute_modal(p));
203                let right = TLExpr::modal_box(distribute_modal(q));
204                TLExpr::and(left, right)
205            } else {
206                expr.clone()
207            }
208        }
209        // ◇(P ∨ Q) → ◇P ∨ ◇Q
210        TLExpr::Diamond(body) if matches!(**body, TLExpr::Or(_, _)) => {
211            if let TLExpr::Or(p, q) = &**body {
212                let left = TLExpr::modal_diamond(distribute_modal(p));
213                let right = TLExpr::modal_diamond(distribute_modal(q));
214                TLExpr::or(left, right)
215            } else {
216                expr.clone()
217            }
218        }
219        // Recursively apply to subexpressions
220        TLExpr::And(l, r) => TLExpr::and(distribute_modal(l), distribute_modal(r)),
221        TLExpr::Or(l, r) => TLExpr::or(distribute_modal(l), distribute_modal(r)),
222        TLExpr::Not(e) => TLExpr::negate(distribute_modal(e)),
223        TLExpr::Imply(l, r) => TLExpr::imply(distribute_modal(l), distribute_modal(r)),
224        TLExpr::Exists { var, domain, body } => {
225            TLExpr::exists(var.clone(), domain.clone(), distribute_modal(body))
226        }
227        TLExpr::ForAll { var, domain, body } => {
228            TLExpr::forall(var.clone(), domain.clone(), distribute_modal(body))
229        }
230        TLExpr::Box(e) => TLExpr::modal_box(distribute_modal(e)),
231        TLExpr::Diamond(e) => TLExpr::modal_diamond(distribute_modal(e)),
232        TLExpr::Next(e) => TLExpr::next(distribute_modal(e)),
233        TLExpr::Eventually(e) => TLExpr::eventually(distribute_modal(e)),
234        TLExpr::Always(e) => TLExpr::always(distribute_modal(e)),
235        _ => expr.clone(),
236    }
237}
238
239#[cfg(test)]
240mod tests {
241    use super::*;
242    use crate::Term;
243
244    #[test]
245    fn test_and_over_or_simple() {
246        // A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
247        let a = TLExpr::pred("A", vec![Term::var("x")]);
248        let b = TLExpr::pred("B", vec![Term::var("x")]);
249        let c = TLExpr::pred("C", vec![Term::var("x")]);
250
251        let expr = TLExpr::and(a.clone(), TLExpr::or(b.clone(), c.clone()));
252        let result = apply_distributive_laws(&expr, DistributiveStrategy::AndOverOr);
253
254        // Result should be (A ∧ B) ∨ (A ∧ C)
255        assert!(matches!(result, TLExpr::Or(_, _)));
256        if let TLExpr::Or(left, right) = result {
257            assert!(matches!(*left, TLExpr::And(_, _)));
258            assert!(matches!(*right, TLExpr::And(_, _)));
259        }
260    }
261
262    #[test]
263    fn test_and_over_or_left() {
264        // (A ∨ B) ∧ C → (A ∧ C) ∨ (B ∧ C)
265        let a = TLExpr::pred("A", vec![Term::var("x")]);
266        let b = TLExpr::pred("B", vec![Term::var("x")]);
267        let c = TLExpr::pred("C", vec![Term::var("x")]);
268
269        let expr = TLExpr::and(TLExpr::or(a.clone(), b.clone()), c.clone());
270        let result = apply_distributive_laws(&expr, DistributiveStrategy::AndOverOr);
271
272        // Result should be (A ∧ C) ∨ (B ∧ C)
273        assert!(matches!(result, TLExpr::Or(_, _)));
274    }
275
276    #[test]
277    fn test_or_over_and_simple() {
278        // A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C)
279        let a = TLExpr::pred("A", vec![Term::var("x")]);
280        let b = TLExpr::pred("B", vec![Term::var("x")]);
281        let c = TLExpr::pred("C", vec![Term::var("x")]);
282
283        let expr = TLExpr::or(a.clone(), TLExpr::and(b.clone(), c.clone()));
284        let result = apply_distributive_laws(&expr, DistributiveStrategy::OrOverAnd);
285
286        // Result should be (A ∨ B) ∧ (A ∨ C)
287        assert!(matches!(result, TLExpr::And(_, _)));
288        if let TLExpr::And(left, right) = result {
289            assert!(matches!(*left, TLExpr::Or(_, _)));
290            assert!(matches!(*right, TLExpr::Or(_, _)));
291        }
292    }
293
294    #[test]
295    fn test_or_over_and_left() {
296        // (A ∧ B) ∨ C → (A ∨ C) ∧ (B ∨ C)
297        let a = TLExpr::pred("A", vec![Term::var("x")]);
298        let b = TLExpr::pred("B", vec![Term::var("x")]);
299        let c = TLExpr::pred("C", vec![Term::var("x")]);
300
301        let expr = TLExpr::or(TLExpr::and(a.clone(), b.clone()), c.clone());
302        let result = apply_distributive_laws(&expr, DistributiveStrategy::OrOverAnd);
303
304        // Result should be (A ∨ C) ∧ (B ∨ C)
305        assert!(matches!(result, TLExpr::And(_, _)));
306    }
307
308    #[test]
309    fn test_forall_over_and() {
310        // ∀x.(P(x) ∧ Q(x)) → (∀x.P(x)) ∧ (∀x.Q(x))
311        let p = TLExpr::pred("P", vec![Term::var("x")]);
312        let q = TLExpr::pred("Q", vec![Term::var("x")]);
313
314        let expr = TLExpr::forall("x", "D", TLExpr::and(p, q));
315        let result = apply_distributive_laws(&expr, DistributiveStrategy::Quantifiers);
316
317        // Result should be (∀x.P(x)) ∧ (∀x.Q(x))
318        assert!(matches!(result, TLExpr::And(_, _)));
319        if let TLExpr::And(left, right) = result {
320            assert!(matches!(*left, TLExpr::ForAll { .. }));
321            assert!(matches!(*right, TLExpr::ForAll { .. }));
322        }
323    }
324
325    #[test]
326    fn test_exists_over_or() {
327        // ∃x.(P(x) ∨ Q(x)) → (∃x.P(x)) ∨ (∃x.Q(x))
328        let p = TLExpr::pred("P", vec![Term::var("x")]);
329        let q = TLExpr::pred("Q", vec![Term::var("x")]);
330
331        let expr = TLExpr::exists("x", "D", TLExpr::or(p, q));
332        let result = apply_distributive_laws(&expr, DistributiveStrategy::Quantifiers);
333
334        // Result should be (∃x.P(x)) ∨ (∃x.Q(x))
335        assert!(matches!(result, TLExpr::Or(_, _)));
336        if let TLExpr::Or(left, right) = result {
337            assert!(matches!(*left, TLExpr::Exists { .. }));
338            assert!(matches!(*right, TLExpr::Exists { .. }));
339        }
340    }
341
342    #[test]
343    fn test_box_over_and() {
344        // □(P ∧ Q) → □P ∧ □Q
345        let p = TLExpr::pred("P", vec![Term::var("x")]);
346        let q = TLExpr::pred("Q", vec![Term::var("x")]);
347
348        let expr = TLExpr::modal_box(TLExpr::and(p, q));
349        let result = apply_distributive_laws(&expr, DistributiveStrategy::Modal);
350
351        // Result should be □P ∧ □Q
352        assert!(matches!(result, TLExpr::And(_, _)));
353        if let TLExpr::And(left, right) = result {
354            assert!(matches!(*left, TLExpr::Box(_)));
355            assert!(matches!(*right, TLExpr::Box(_)));
356        }
357    }
358
359    #[test]
360    fn test_diamond_over_or() {
361        // ◇(P ∨ Q) → ◇P ∨ ◇Q
362        let p = TLExpr::pred("P", vec![Term::var("x")]);
363        let q = TLExpr::pred("Q", vec![Term::var("x")]);
364
365        let expr = TLExpr::modal_diamond(TLExpr::or(p, q));
366        let result = apply_distributive_laws(&expr, DistributiveStrategy::Modal);
367
368        // Result should be ◇P ∨ ◇Q
369        assert!(matches!(result, TLExpr::Or(_, _)));
370        if let TLExpr::Or(left, right) = result {
371            assert!(matches!(*left, TLExpr::Diamond(_)));
372            assert!(matches!(*right, TLExpr::Diamond(_)));
373        }
374    }
375
376    #[test]
377    fn test_all_strategy() {
378        // Test that All strategy applies AndOverOr transformation
379        let a = TLExpr::pred("A", vec![Term::var("x")]);
380        let b = TLExpr::pred("B", vec![Term::var("x")]);
381        let c = TLExpr::pred("C", vec![Term::var("x")]);
382
383        // A ∧ (B ∨ C)
384        let expr = TLExpr::and(a, TLExpr::or(b, c));
385        let result = apply_distributive_laws(&expr, DistributiveStrategy::AndOverOr);
386
387        // Should be distributed to (A ∧ B) ∨ (A ∧ C)
388        assert!(matches!(result, TLExpr::Or(_, _)));
389    }
390
391    #[test]
392    fn test_no_distribution_needed() {
393        // Test that expressions that don't need distribution are unchanged
394        let a = TLExpr::pred("A", vec![Term::var("x")]);
395        let b = TLExpr::pred("B", vec![Term::var("x")]);
396
397        // A ∧ B (no distribution needed)
398        let expr = TLExpr::and(a.clone(), b.clone());
399        let result = apply_distributive_laws(&expr, DistributiveStrategy::AndOverOr);
400
401        // Should remain A ∧ B
402        assert!(matches!(result, TLExpr::And(_, _)));
403    }
404}
tensorlogic_ir/expr/distributive_laws.rs

tensorlogic_ir/expr/
distributive_laws.rs
