lolli_core/
formula.rs

1//! Linear logic formula representation.
2//!
3//! This module provides the [`Formula`] enum representing linear logic formulas
4//! with all standard connectives.
5
6/// A linear logic formula.
7///
8/// Linear logic has a rich set of connectives split into multiplicative and additive families,
9/// plus exponentials for controlled structural rules.
10#[derive(Clone, Debug, PartialEq, Eq, Hash)]
11pub enum Formula {
12    // Atoms
13    /// Atomic proposition
14    Atom(String),
15    /// Negated atomic proposition (A⊥)
16    NegAtom(String),
17
18    // Multiplicatives
19    /// Tensor product (A ⊗ B) - "both A and B independently"
20    Tensor(Box<Formula>, Box<Formula>),
21    /// Par (A ⅋ B) - "A or B, opponent chooses"
22    Par(Box<Formula>, Box<Formula>),
23    /// Multiplicative unit (1)
24    One,
25    /// Multiplicative false (⊥)
26    Bottom,
27
28    // Additives
29    /// With (A & B) - "both available, you choose one"
30    With(Box<Formula>, Box<Formula>),
31    /// Plus (A ⊕ B) - "one of them, I choose which"
32    Plus(Box<Formula>, Box<Formula>),
33    /// Additive truth (⊤)
34    Top,
35    /// Additive false (0)
36    Zero,
37
38    // Exponentials
39    /// Of course (!A) - "unlimited supply of A, can copy/discard"
40    OfCourse(Box<Formula>),
41    /// Why not (?A) - "demand for A"
42    WhyNot(Box<Formula>),
43
44    // Derived (syntactic sugar)
45    /// Linear implication (A ⊸ B) - sugar for A⊥ ⅋ B
46    Lolli(Box<Formula>, Box<Formula>),
47}
48
49impl Formula {
50    /// Compute the linear negation of a formula.
51    ///
52    /// Linear negation is involutive: (A⊥)⊥ = A
53    ///
54    /// De Morgan dualities:
55    /// - (A ⊗ B)⊥ = A⊥ ⅋ B⊥
56    /// - (A ⅋ B)⊥ = A⊥ ⊗ B⊥
57    /// - (A & B)⊥ = A⊥ ⊕ B⊥
58    /// - (A ⊕ B)⊥ = A⊥ & B⊥
59    /// - 1⊥ = ⊥
60    /// - ⊥⊥ = 1
61    /// - (!A)⊥ = ?(A⊥)
62    /// - (?A)⊥ = !(A⊥)
63    pub fn negate(&self) -> Formula {
64        match self {
65            Formula::Atom(a) => Formula::NegAtom(a.clone()),
66            Formula::NegAtom(a) => Formula::Atom(a.clone()),
67
68            Formula::Tensor(a, b) => {
69                Formula::Par(Box::new(a.negate()), Box::new(b.negate()))
70            }
71            Formula::Par(a, b) => {
72                Formula::Tensor(Box::new(a.negate()), Box::new(b.negate()))
73            }
74            Formula::One => Formula::Bottom,
75            Formula::Bottom => Formula::One,
76
77            Formula::With(a, b) => {
78                Formula::Plus(Box::new(a.negate()), Box::new(b.negate()))
79            }
80            Formula::Plus(a, b) => {
81                Formula::With(Box::new(a.negate()), Box::new(b.negate()))
82            }
83            Formula::Top => Formula::Zero,
84            Formula::Zero => Formula::Top,
85
86            Formula::OfCourse(a) => Formula::WhyNot(Box::new(a.negate())),
87            Formula::WhyNot(a) => Formula::OfCourse(Box::new(a.negate())),
88
89            Formula::Lolli(a, b) => {
90                // (A ⊸ B)⊥ = (A⊥ ⅋ B)⊥ = A ⊗ B⊥
91                Formula::Tensor(a.clone(), Box::new(b.negate()))
92            }
93        }
94    }
95
96    /// Desugar the formula by expanding A ⊸ B to A⊥ ⅋ B.
97    pub fn desugar(&self) -> Formula {
98        match self {
99            Formula::Lolli(a, b) => {
100                Formula::Par(Box::new(a.negate().desugar()), Box::new(b.desugar()))
101            }
102            Formula::Tensor(a, b) => {
103                Formula::Tensor(Box::new(a.desugar()), Box::new(b.desugar()))
104            }
105            Formula::Par(a, b) => {
106                Formula::Par(Box::new(a.desugar()), Box::new(b.desugar()))
107            }
108            Formula::With(a, b) => {
109                Formula::With(Box::new(a.desugar()), Box::new(b.desugar()))
110            }
111            Formula::Plus(a, b) => {
112                Formula::Plus(Box::new(a.desugar()), Box::new(b.desugar()))
113            }
114            Formula::OfCourse(a) => Formula::OfCourse(Box::new(a.desugar())),
115            Formula::WhyNot(a) => Formula::WhyNot(Box::new(a.desugar())),
116            _ => self.clone(),
117        }
118    }
119
120    /// Returns true if this formula is positive (async/eager).
121    ///
122    /// Positive formulas: ⊗, 1, ⊕, 0, !, atoms
123    pub fn is_positive(&self) -> bool {
124        matches!(
125            self,
126            Formula::Atom(_)
127                | Formula::Tensor(_, _)
128                | Formula::One
129                | Formula::Plus(_, _)
130                | Formula::Zero
131                | Formula::OfCourse(_)
132        )
133    }
134
135    /// Returns true if this formula is negative (sync/lazy).
136    ///
137    /// Negative formulas: ⅋, ⊥, &, ⊤, ?, negated atoms
138    pub fn is_negative(&self) -> bool {
139        !self.is_positive()
140    }
141
142    /// Pretty print the formula with Unicode symbols.
143    pub fn pretty(&self) -> String {
144        match self {
145            Formula::Atom(a) => a.clone(),
146            Formula::NegAtom(a) => format!("{}⊥", a),
147            Formula::Tensor(a, b) => format!("({} ⊗ {})", a.pretty(), b.pretty()),
148            Formula::Par(a, b) => format!("({} ⅋ {})", a.pretty(), b.pretty()),
149            Formula::Lolli(a, b) => format!("({} ⊸ {})", a.pretty(), b.pretty()),
150            Formula::With(a, b) => format!("({} & {})", a.pretty(), b.pretty()),
151            Formula::Plus(a, b) => format!("({} ⊕ {})", a.pretty(), b.pretty()),
152            Formula::OfCourse(a) => format!("!{}", a.pretty()),
153            Formula::WhyNot(a) => format!("?{}", a.pretty()),
154            Formula::One => "1".to_string(),
155            Formula::Bottom => "⊥".to_string(),
156            Formula::Top => "⊤".to_string(),
157            Formula::Zero => "0".to_string(),
158        }
159    }
160
161    /// Pretty print the formula with ASCII symbols.
162    pub fn pretty_ascii(&self) -> String {
163        match self {
164            Formula::Atom(a) => a.clone(),
165            Formula::NegAtom(a) => format!("{}^", a),
166            Formula::Tensor(a, b) => format!("({} * {})", a.pretty_ascii(), b.pretty_ascii()),
167            Formula::Par(a, b) => format!("({} | {})", a.pretty_ascii(), b.pretty_ascii()),
168            Formula::Lolli(a, b) => format!("({} -o {})", a.pretty_ascii(), b.pretty_ascii()),
169            Formula::With(a, b) => format!("({} & {})", a.pretty_ascii(), b.pretty_ascii()),
170            Formula::Plus(a, b) => format!("({} + {})", a.pretty_ascii(), b.pretty_ascii()),
171            Formula::OfCourse(a) => format!("!{}", a.pretty_ascii()),
172            Formula::WhyNot(a) => format!("?{}", a.pretty_ascii()),
173            Formula::One => "1".to_string(),
174            Formula::Bottom => "bot".to_string(),
175            Formula::Top => "top".to_string(),
176            Formula::Zero => "0".to_string(),
177        }
178    }
179
180    /// Pretty print the formula for LaTeX.
181    pub fn pretty_latex(&self) -> String {
182        match self {
183            Formula::Atom(a) => a.clone(),
184            Formula::NegAtom(a) => format!("{}^{{\\bot}}", a),
185            Formula::Tensor(a, b) => {
186                format!("({} \\otimes {})", a.pretty_latex(), b.pretty_latex())
187            }
188            Formula::Par(a, b) => {
189                format!("({} \\parr {})", a.pretty_latex(), b.pretty_latex())
190            }
191            Formula::Lolli(a, b) => {
192                format!("({} \\multimap {})", a.pretty_latex(), b.pretty_latex())
193            }
194            Formula::With(a, b) => {
195                format!("({} \\with {})", a.pretty_latex(), b.pretty_latex())
196            }
197            Formula::Plus(a, b) => {
198                format!("({} \\oplus {})", a.pretty_latex(), b.pretty_latex())
199            }
200            Formula::OfCourse(a) => format!("{{!}}{}", a.pretty_latex()),
201            Formula::WhyNot(a) => format!("{{?}}{}", a.pretty_latex()),
202            Formula::One => "\\mathbf{1}".to_string(),
203            Formula::Bottom => "\\bot".to_string(),
204            Formula::Top => "\\top".to_string(),
205            Formula::Zero => "\\mathbf{0}".to_string(),
206        }
207    }
208
209    /// Create an atom formula.
210    pub fn atom(name: impl Into<String>) -> Self {
211        Formula::Atom(name.into())
212    }
213
214    /// Create a negated atom formula.
215    pub fn neg_atom(name: impl Into<String>) -> Self {
216        Formula::NegAtom(name.into())
217    }
218
219    /// Create a tensor (A ⊗ B).
220    pub fn tensor(a: Formula, b: Formula) -> Self {
221        Formula::Tensor(Box::new(a), Box::new(b))
222    }
223
224    /// Create a par (A ⅋ B).
225    pub fn par(a: Formula, b: Formula) -> Self {
226        Formula::Par(Box::new(a), Box::new(b))
227    }
228
229    /// Create a linear implication (A ⊸ B).
230    pub fn lolli(a: Formula, b: Formula) -> Self {
231        Formula::Lolli(Box::new(a), Box::new(b))
232    }
233
234    /// Create a with (A & B).
235    pub fn with(a: Formula, b: Formula) -> Self {
236        Formula::With(Box::new(a), Box::new(b))
237    }
238
239    /// Create a plus (A ⊕ B).
240    pub fn plus(a: Formula, b: Formula) -> Self {
241        Formula::Plus(Box::new(a), Box::new(b))
242    }
243
244    /// Create an of-course (!A).
245    pub fn of_course(a: Formula) -> Self {
246        Formula::OfCourse(Box::new(a))
247    }
248
249    /// Create a why-not (?A).
250    pub fn why_not(a: Formula) -> Self {
251        Formula::WhyNot(Box::new(a))
252    }
253}
254
255#[cfg(test)]
256mod tests {
257    use super::*;
258
259    #[test]
260    fn test_negation_involutive() {
261        let a = Formula::atom("A");
262        assert_eq!(a.negate().negate(), a);
263
264        let complex = Formula::tensor(Formula::atom("A"), Formula::atom("B"));
265        assert_eq!(complex.negate().negate(), complex);
266
267        // Test primitive connectives (not lolli, which is sugar)
268        let formulas = vec![
269            Formula::One,
270            Formula::Bottom,
271            Formula::Top,
272            Formula::Zero,
273            Formula::of_course(Formula::atom("X")),
274            Formula::why_not(Formula::atom("Y")),
275            Formula::with(Formula::atom("A"), Formula::atom("B")),
276            Formula::plus(Formula::atom("A"), Formula::atom("B")),
277            Formula::par(Formula::atom("A"), Formula::atom("B")),
278        ];
279
280        for f in formulas {
281            assert_eq!(f.negate().negate(), f, "Failed for: {:?}", f);
282        }
283
284        // Lolli is special: (A ⊸ B)⊥ = A ⊗ B⊥, which is not a Lolli
285        // But we can verify the semantics are correct
286        let lolli = Formula::lolli(Formula::atom("A"), Formula::atom("B"));
287        let neg_lolli = lolli.negate();
288        // (A ⊸ B)⊥ = A ⊗ B⊥
289        assert_eq!(
290            neg_lolli,
291            Formula::tensor(Formula::atom("A"), Formula::neg_atom("B"))
292        );
293    }
294
295    #[test]
296    fn test_de_morgan() {
297        // (A ⊗ B)⊥ = A⊥ ⅋ B⊥
298        let tensor = Formula::tensor(Formula::atom("A"), Formula::atom("B"));
299        let expected = Formula::par(Formula::neg_atom("A"), Formula::neg_atom("B"));
300        assert_eq!(tensor.negate(), expected);
301
302        // (A ⅋ B)⊥ = A⊥ ⊗ B⊥
303        let par = Formula::par(Formula::atom("A"), Formula::atom("B"));
304        let expected = Formula::tensor(Formula::neg_atom("A"), Formula::neg_atom("B"));
305        assert_eq!(par.negate(), expected);
306
307        // (A & B)⊥ = A⊥ ⊕ B⊥
308        let with = Formula::with(Formula::atom("A"), Formula::atom("B"));
309        let expected = Formula::plus(Formula::neg_atom("A"), Formula::neg_atom("B"));
310        assert_eq!(with.negate(), expected);
311
312        // (A ⊕ B)⊥ = A⊥ & B⊥
313        let plus = Formula::plus(Formula::atom("A"), Formula::atom("B"));
314        let expected = Formula::with(Formula::neg_atom("A"), Formula::neg_atom("B"));
315        assert_eq!(plus.negate(), expected);
316
317        // 1⊥ = ⊥
318        assert_eq!(Formula::One.negate(), Formula::Bottom);
319
320        // ⊥⊥ = 1
321        assert_eq!(Formula::Bottom.negate(), Formula::One);
322
323        // ⊤⊥ = 0
324        assert_eq!(Formula::Top.negate(), Formula::Zero);
325
326        // 0⊥ = ⊤
327        assert_eq!(Formula::Zero.negate(), Formula::Top);
328
329        // (!A)⊥ = ?(A⊥)
330        let bang = Formula::of_course(Formula::atom("A"));
331        let expected = Formula::why_not(Formula::neg_atom("A"));
332        assert_eq!(bang.negate(), expected);
333
334        // (?A)⊥ = !(A⊥)
335        let whynot = Formula::why_not(Formula::atom("A"));
336        let expected = Formula::of_course(Formula::neg_atom("A"));
337        assert_eq!(whynot.negate(), expected);
338    }
339
340    #[test]
341    fn test_polarity() {
342        // Positive formulas
343        assert!(Formula::atom("A").is_positive());
344        assert!(Formula::tensor(Formula::atom("A"), Formula::atom("B")).is_positive());
345        assert!(Formula::One.is_positive());
346        assert!(Formula::plus(Formula::atom("A"), Formula::atom("B")).is_positive());
347        assert!(Formula::Zero.is_positive());
348        assert!(Formula::of_course(Formula::atom("A")).is_positive());
349
350        // Negative formulas
351        assert!(Formula::neg_atom("A").is_negative());
352        assert!(Formula::par(Formula::atom("A"), Formula::atom("B")).is_negative());
353        assert!(Formula::Bottom.is_negative());
354        assert!(Formula::with(Formula::atom("A"), Formula::atom("B")).is_negative());
355        assert!(Formula::Top.is_negative());
356        assert!(Formula::why_not(Formula::atom("A")).is_negative());
357
358        // Lolli is negative (it's sugar for A⊥ ⅋ B)
359        assert!(Formula::lolli(Formula::atom("A"), Formula::atom("B")).is_negative());
360    }
361
362    #[test]
363    fn test_desugar() {
364        // A ⊸ B should desugar to A⊥ ⅋ B
365        let lolli = Formula::lolli(Formula::atom("A"), Formula::atom("B"));
366        let desugared = lolli.desugar();
367        let expected = Formula::par(Formula::neg_atom("A"), Formula::atom("B"));
368        assert_eq!(desugared, expected);
369
370        // Nested: (A ⊸ B) ⊸ C should desugar correctly
371        let nested = Formula::lolli(
372            Formula::lolli(Formula::atom("A"), Formula::atom("B")),
373            Formula::atom("C"),
374        );
375        let desugared = nested.desugar();
376        // (A ⊸ B)⊥ ⅋ C = (A ⊗ B⊥) ⅋ C
377        let expected = Formula::par(
378            Formula::tensor(Formula::atom("A"), Formula::neg_atom("B")),
379            Formula::atom("C"),
380        );
381        assert_eq!(desugared, expected);
382    }
383
384    #[test]
385    fn test_pretty_print() {
386        let f = Formula::lolli(Formula::atom("A"), Formula::atom("B"));
387        assert_eq!(f.pretty(), "(A ⊸ B)");
388        assert_eq!(f.pretty_ascii(), "(A -o B)");
389        assert_eq!(f.pretty_latex(), "(A \\multimap B)");
390
391        let f = Formula::tensor(
392            Formula::of_course(Formula::atom("A")),
393            Formula::why_not(Formula::atom("B")),
394        );
395        assert_eq!(f.pretty(), "(!A ⊗ ?B)");
396        assert_eq!(f.pretty_ascii(), "(!A * ?B)");
397    }
398
399    #[test]
400    fn test_units() {
401        assert_eq!(Formula::One.pretty(), "1");
402        assert_eq!(Formula::Bottom.pretty(), "⊥");
403        assert_eq!(Formula::Top.pretty(), "⊤");
404        assert_eq!(Formula::Zero.pretty(), "0");
405
406        assert_eq!(Formula::One.pretty_ascii(), "1");
407        assert_eq!(Formula::Bottom.pretty_ascii(), "bot");
408        assert_eq!(Formula::Top.pretty_ascii(), "top");
409        assert_eq!(Formula::Zero.pretty_ascii(), "0");
410    }
411}
lolli_core/formula.rs

lolli_core/
formula.rs
