tensorlogic_compiler/
config.rs

1//! Compilation configuration and strategy selection.
2//!
3//! This module provides configurable compilation strategies for mapping
4//! logical operations to tensor operations. Different strategies optimize
5//! for different objectives (accuracy, efficiency, differentiability).
6
7/// Strategy for compiling AND operations.
8#[derive(Debug, Clone, Copy, PartialEq, Eq)]
9pub enum AndStrategy {
10    /// Hadamard product (element-wise multiplication): `a * b`
11    /// - Differentiable, efficient
12    /// - Soft semantics (values in \[0,1\])
13    Product,
14
15    /// Minimum: `min(a, b)`
16    /// - Hard semantics (preserves Boolean values)
17    /// - Not differentiable at equality points
18    Min,
19
20    /// Probabilistic product: `a + b - a*b`
21    /// - Alternative soft semantics
22    /// - Differentiable
23    ProbabilisticSum,
24
25    /// Gödel t-norm: `min(a, b)`
26    /// - Same as Min but explicit fuzzy logic semantics
27    Godel,
28
29    /// Product t-norm: `a * b`
30    /// - Same as Product but explicit fuzzy logic semantics
31    ProductTNorm,
32
33    /// Łukasiewicz t-norm: `max(0, a + b - 1)`
34    /// - Strict t-norm
35    /// - Differentiable
36    Lukasiewicz,
37}
38
39/// Strategy for compiling OR operations.
40#[derive(Debug, Clone, Copy, PartialEq, Eq)]
41pub enum OrStrategy {
42    /// Maximum: `max(a, b)`
43    /// - Hard semantics
44    /// - Not differentiable at equality points
45    Max,
46
47    /// Probabilistic sum: `a + b - a*b`
48    /// - Soft semantics
49    /// - Differentiable
50    ProbabilisticSum,
51
52    /// Gödel s-norm: `max(a, b)`
53    /// - Same as Max but explicit fuzzy logic semantics
54    Godel,
55
56    /// Probabilistic s-norm: `a + b - a*b`
57    /// - Same as ProbabilisticSum but explicit fuzzy logic semantics
58    ProbabilisticSNorm,
59
60    /// Łukasiewicz s-norm: `min(1, a + b)`
61    /// - Dual of Łukasiewicz t-norm
62    /// - Differentiable
63    Lukasiewicz,
64}
65
66/// Strategy for compiling NOT operations.
67#[derive(Debug, Clone, Copy, PartialEq, Eq)]
68pub enum NotStrategy {
69    /// Complement: `1 - a`
70    /// - Standard negation
71    /// - Differentiable
72    Complement,
73
74    /// Temperature-controlled sigmoid: `1 / (1 + exp(T * a))`
75    /// - Smoother gradients
76    /// - Configurable sharpness via temperature
77    Sigmoid {
78        /// Temperature parameter (higher = sharper)
79        temperature: u8,
80    },
81}
82
83/// Strategy for compiling existential quantifiers (∃).
84#[derive(Debug, Clone, Copy, PartialEq, Eq)]
85pub enum ExistsStrategy {
86    /// Sum reduction: `sum(P, axis)`
87    /// - Soft semantics (counts satisfying instances)
88    /// - Differentiable
89    Sum,
90
91    /// Max reduction: `max(P, axis)`
92    /// - Hard semantics (true if any instance satisfies)
93    /// - Not differentiable at unique maximum
94    Max,
95
96    /// LogSumExp: `log(sum(exp(P), axis))`
97    /// - Smooth approximation to max
98    /// - Differentiable
99    LogSumExp,
100
101    /// Mean reduction: `mean(P, axis)`
102    /// - Normalized soft semantics
103    /// - Differentiable
104    Mean,
105}
106
107/// Strategy for compiling universal quantifiers (∀).
108#[derive(Debug, Clone, Copy, PartialEq, Eq)]
109pub enum ForallStrategy {
110    /// Dual of exists via double negation: `NOT(EXISTS(NOT(P)))`
111    /// - Inherits properties from NOT and EXISTS strategies
112    DualOfExists,
113
114    /// Product reduction: `product(P, axis)`
115    /// - Direct product semantics
116    /// - Differentiable
117    Product,
118
119    /// Min reduction: `min(P, axis)`
120    /// - Hard semantics (true if all instances satisfy)
121    /// - Not differentiable at unique minimum
122    Min,
123
124    /// Mean reduction with threshold: `mean(P, axis) >= threshold`
125    /// - Soft semantics with configurable strictness
126    MeanThreshold {
127        /// Threshold for satisfaction (typically 0.9-1.0)
128        threshold_times_100: u8,
129    },
130}
131
132/// Strategy for compiling implication (→).
133#[derive(Debug, Clone, Copy, PartialEq, Eq)]
134pub enum ImplicationStrategy {
135    /// ReLU-based: `ReLU(b - a)`
136    /// - Differentiable
137    /// - Soft semantics
138    ReLU,
139
140    /// Material implication: `NOT(a) OR b`
141    /// - Classical logic semantics
142    /// - Inherits properties from NOT and OR strategies
143    Material,
144
145    /// Gödel implication: `if a <= b then 1 else b`
146    /// - Fuzzy logic semantics
147    /// - Not differentiable
148    Godel,
149
150    /// Łukasiewicz implication: `min(1, 1 - a + b)`
151    /// - T-norm based
152    /// - Differentiable
153    Lukasiewicz,
154
155    /// Reichenbach implication: `1 - a + a*b`
156    /// - Probabilistic interpretation
157    /// - Differentiable
158    Reichenbach,
159}
160
161/// Strategy for compiling modal logic operators (Box □, Diamond ◇).
162#[derive(Debug, Clone, Copy, PartialEq)]
163pub enum ModalStrategy {
164    /// All worlds must satisfy (min reduction over worlds)
165    /// - Box: min_w P(w)
166    /// - Diamond: max_w P(w)
167    AllWorldsMin,
168
169    /// Product over all worlds
170    /// - Box: ∏_w P(w)
171    /// - Diamond: 1 - ∏_w (1 - P(w))
172    AllWorldsProduct,
173
174    /// Threshold-based satisfaction
175    /// - Box: ∀w. P(w) > threshold
176    /// - Diamond: ∃w. P(w) > threshold
177    Threshold {
178        /// Threshold value (0.0 to 1.0)
179        threshold: f64,
180    },
181}
182
183impl Eq for ModalStrategy {}
184
185/// Strategy for compiling temporal logic operators (Next X, Eventually F, Always G).
186#[derive(Debug, Clone, Copy, PartialEq, Eq)]
187pub enum TemporalStrategy {
188    /// Max over time (for Eventually, min for Always)
189    Max,
190
191    /// Sum over time (probabilistic interpretation)
192    Sum,
193
194    /// LogSumExp (smooth max approximation)
195    LogSumExp,
196}
197
198/// Complete compilation configuration.
199#[derive(Debug, Clone, PartialEq)]
200pub struct CompilationConfig {
201    /// Strategy for AND operations
202    pub and_strategy: AndStrategy,
203    /// Strategy for OR operations
204    pub or_strategy: OrStrategy,
205    /// Strategy for NOT operations
206    pub not_strategy: NotStrategy,
207    /// Strategy for existential quantifiers
208    pub exists_strategy: ExistsStrategy,
209    /// Strategy for universal quantifiers
210    pub forall_strategy: ForallStrategy,
211    /// Strategy for implication
212    pub implication_strategy: ImplicationStrategy,
213    /// Strategy for modal logic operators
214    pub modal_strategy: ModalStrategy,
215    /// Strategy for temporal logic operators
216    pub temporal_strategy: TemporalStrategy,
217    /// Number of possible worlds for modal logic (default: 10)
218    pub modal_world_size: Option<usize>,
219    /// Number of time steps for temporal logic (default: 100)
220    pub temporal_time_steps: Option<usize>,
221}
222
223impl Eq for CompilationConfig {}
224
225impl Default for CompilationConfig {
226    fn default() -> Self {
227        Self::soft_differentiable()
228    }
229}
230
231impl CompilationConfig {
232    /// Soft, differentiable configuration (default).
233    ///
234    /// Optimized for neural network training and gradient-based optimization.
235    /// All operations are differentiable with smooth gradients.
236    pub fn soft_differentiable() -> Self {
237        Self {
238            and_strategy: AndStrategy::Product,
239            or_strategy: OrStrategy::ProbabilisticSum,
240            not_strategy: NotStrategy::Complement,
241            exists_strategy: ExistsStrategy::Sum,
242            forall_strategy: ForallStrategy::DualOfExists,
243            implication_strategy: ImplicationStrategy::ReLU,
244            modal_strategy: ModalStrategy::AllWorldsProduct,
245            temporal_strategy: TemporalStrategy::Sum,
246            modal_world_size: Some(10),
247            temporal_time_steps: Some(100),
248        }
249    }
250
251    /// Hard, Boolean-like configuration.
252    ///
253    /// Optimized for discrete reasoning with Boolean-like values.
254    /// Uses min/max operations for crisp logic semantics.
255    pub fn hard_boolean() -> Self {
256        Self {
257            and_strategy: AndStrategy::Min,
258            or_strategy: OrStrategy::Max,
259            not_strategy: NotStrategy::Complement,
260            exists_strategy: ExistsStrategy::Max,
261            forall_strategy: ForallStrategy::Min,
262            implication_strategy: ImplicationStrategy::Material,
263            modal_strategy: ModalStrategy::AllWorldsMin,
264            temporal_strategy: TemporalStrategy::Max,
265            modal_world_size: Some(10),
266            temporal_time_steps: Some(100),
267        }
268    }
269
270    /// Fuzzy logic configuration (Gödel semantics).
271    ///
272    /// Standard fuzzy logic with Gödel t-norms and s-norms.
273    pub fn fuzzy_godel() -> Self {
274        Self {
275            and_strategy: AndStrategy::Godel,
276            or_strategy: OrStrategy::Godel,
277            not_strategy: NotStrategy::Complement,
278            exists_strategy: ExistsStrategy::Max,
279            forall_strategy: ForallStrategy::Min,
280            implication_strategy: ImplicationStrategy::Godel,
281            modal_strategy: ModalStrategy::AllWorldsMin,
282            temporal_strategy: TemporalStrategy::Max,
283            modal_world_size: Some(10),
284            temporal_time_steps: Some(100),
285        }
286    }
287
288    /// Fuzzy logic configuration (Product semantics).
289    ///
290    /// Fuzzy logic with product t-norms.
291    pub fn fuzzy_product() -> Self {
292        Self {
293            and_strategy: AndStrategy::ProductTNorm,
294            or_strategy: OrStrategy::ProbabilisticSNorm,
295            not_strategy: NotStrategy::Complement,
296            exists_strategy: ExistsStrategy::Mean,
297            forall_strategy: ForallStrategy::Product,
298            implication_strategy: ImplicationStrategy::Reichenbach,
299            modal_strategy: ModalStrategy::AllWorldsProduct,
300            temporal_strategy: TemporalStrategy::Sum,
301            modal_world_size: Some(10),
302            temporal_time_steps: Some(100),
303        }
304    }
305
306    /// Fuzzy logic configuration (Łukasiewicz semantics).
307    ///
308    /// Fuzzy logic with Łukasiewicz t-norms, fully differentiable.
309    pub fn fuzzy_lukasiewicz() -> Self {
310        Self {
311            and_strategy: AndStrategy::Lukasiewicz,
312            or_strategy: OrStrategy::Lukasiewicz,
313            not_strategy: NotStrategy::Complement,
314            exists_strategy: ExistsStrategy::LogSumExp,
315            forall_strategy: ForallStrategy::DualOfExists,
316            implication_strategy: ImplicationStrategy::Lukasiewicz,
317            modal_strategy: ModalStrategy::Threshold { threshold: 0.5 },
318            temporal_strategy: TemporalStrategy::LogSumExp,
319            modal_world_size: Some(10),
320            temporal_time_steps: Some(100),
321        }
322    }
323
324    /// Probabilistic logic configuration.
325    ///
326    /// Interprets logical operations as probabilistic events.
327    pub fn probabilistic() -> Self {
328        Self {
329            and_strategy: AndStrategy::ProbabilisticSum,
330            or_strategy: OrStrategy::ProbabilisticSum,
331            not_strategy: NotStrategy::Complement,
332            exists_strategy: ExistsStrategy::Mean,
333            forall_strategy: ForallStrategy::Product,
334            implication_strategy: ImplicationStrategy::Reichenbach,
335            modal_strategy: ModalStrategy::AllWorldsProduct,
336            temporal_strategy: TemporalStrategy::Sum,
337            modal_world_size: Some(10),
338            temporal_time_steps: Some(100),
339        }
340    }
341
342    /// Create a custom configuration.
343    pub fn custom() -> CompilationConfigBuilder {
344        CompilationConfigBuilder::default()
345    }
346}
347
348/// Builder for custom compilation configurations.
349#[derive(Debug, Clone, Default)]
350pub struct CompilationConfigBuilder {
351    and_strategy: Option<AndStrategy>,
352    or_strategy: Option<OrStrategy>,
353    not_strategy: Option<NotStrategy>,
354    exists_strategy: Option<ExistsStrategy>,
355    forall_strategy: Option<ForallStrategy>,
356    implication_strategy: Option<ImplicationStrategy>,
357    modal_strategy: Option<ModalStrategy>,
358    temporal_strategy: Option<TemporalStrategy>,
359    modal_world_size: Option<usize>,
360    temporal_time_steps: Option<usize>,
361}
362
363impl CompilationConfigBuilder {
364    /// Set AND strategy.
365    pub fn and_strategy(mut self, strategy: AndStrategy) -> Self {
366        self.and_strategy = Some(strategy);
367        self
368    }
369
370    /// Set OR strategy.
371    pub fn or_strategy(mut self, strategy: OrStrategy) -> Self {
372        self.or_strategy = Some(strategy);
373        self
374    }
375
376    /// Set NOT strategy.
377    pub fn not_strategy(mut self, strategy: NotStrategy) -> Self {
378        self.not_strategy = Some(strategy);
379        self
380    }
381
382    /// Set EXISTS strategy.
383    pub fn exists_strategy(mut self, strategy: ExistsStrategy) -> Self {
384        self.exists_strategy = Some(strategy);
385        self
386    }
387
388    /// Set FORALL strategy.
389    pub fn forall_strategy(mut self, strategy: ForallStrategy) -> Self {
390        self.forall_strategy = Some(strategy);
391        self
392    }
393
394    /// Set implication strategy.
395    pub fn implication_strategy(mut self, strategy: ImplicationStrategy) -> Self {
396        self.implication_strategy = Some(strategy);
397        self
398    }
399
400    /// Set modal logic strategy.
401    pub fn modal_strategy(mut self, strategy: ModalStrategy) -> Self {
402        self.modal_strategy = Some(strategy);
403        self
404    }
405
406    /// Set temporal logic strategy.
407    pub fn temporal_strategy(mut self, strategy: TemporalStrategy) -> Self {
408        self.temporal_strategy = Some(strategy);
409        self
410    }
411
412    /// Set number of possible worlds for modal logic.
413    pub fn modal_world_size(mut self, size: usize) -> Self {
414        self.modal_world_size = Some(size);
415        self
416    }
417
418    /// Set number of time steps for temporal logic.
419    pub fn temporal_time_steps(mut self, steps: usize) -> Self {
420        self.temporal_time_steps = Some(steps);
421        self
422    }
423
424    /// Build the configuration.
425    ///
426    /// Uses default soft_differentiable() values for any unset strategies.
427    pub fn build(self) -> CompilationConfig {
428        let default = CompilationConfig::soft_differentiable();
429        CompilationConfig {
430            and_strategy: self.and_strategy.unwrap_or(default.and_strategy),
431            or_strategy: self.or_strategy.unwrap_or(default.or_strategy),
432            not_strategy: self.not_strategy.unwrap_or(default.not_strategy),
433            exists_strategy: self.exists_strategy.unwrap_or(default.exists_strategy),
434            forall_strategy: self.forall_strategy.unwrap_or(default.forall_strategy),
435            implication_strategy: self
436                .implication_strategy
437                .unwrap_or(default.implication_strategy),
438            modal_strategy: self.modal_strategy.unwrap_or(default.modal_strategy),
439            temporal_strategy: self.temporal_strategy.unwrap_or(default.temporal_strategy),
440            modal_world_size: self.modal_world_size.or(default.modal_world_size),
441            temporal_time_steps: self.temporal_time_steps.or(default.temporal_time_steps),
442        }
443    }
444}
445
446#[cfg(test)]
447mod tests {
448    use super::*;
449
450    #[test]
451    fn test_default_config() {
452        let config = CompilationConfig::default();
453        assert_eq!(config.and_strategy, AndStrategy::Product);
454        assert_eq!(config.or_strategy, OrStrategy::ProbabilisticSum);
455        assert_eq!(config.exists_strategy, ExistsStrategy::Sum);
456    }
457
458    #[test]
459    fn test_hard_boolean_config() {
460        let config = CompilationConfig::hard_boolean();
461        assert_eq!(config.and_strategy, AndStrategy::Min);
462        assert_eq!(config.or_strategy, OrStrategy::Max);
463        assert_eq!(config.exists_strategy, ExistsStrategy::Max);
464    }
465
466    #[test]
467    fn test_fuzzy_godel_config() {
468        let config = CompilationConfig::fuzzy_godel();
469        assert_eq!(config.and_strategy, AndStrategy::Godel);
470        assert_eq!(config.or_strategy, OrStrategy::Godel);
471        assert_eq!(config.implication_strategy, ImplicationStrategy::Godel);
472    }
473
474    #[test]
475    fn test_custom_config_builder() {
476        let config = CompilationConfig::custom()
477            .and_strategy(AndStrategy::Min)
478            .or_strategy(OrStrategy::Max)
479            .build();
480
481        assert_eq!(config.and_strategy, AndStrategy::Min);
482        assert_eq!(config.or_strategy, OrStrategy::Max);
483        // Should use defaults for unset strategies
484        assert_eq!(config.not_strategy, NotStrategy::Complement);
485    }
486
487    #[test]
488    fn test_builder_with_all_strategies() {
489        let config = CompilationConfig::custom()
490            .and_strategy(AndStrategy::Lukasiewicz)
491            .or_strategy(OrStrategy::Lukasiewicz)
492            .not_strategy(NotStrategy::Sigmoid { temperature: 10 })
493            .exists_strategy(ExistsStrategy::LogSumExp)
494            .forall_strategy(ForallStrategy::Min)
495            .implication_strategy(ImplicationStrategy::Lukasiewicz)
496            .build();
497
498        assert_eq!(config.and_strategy, AndStrategy::Lukasiewicz);
499        assert_eq!(config.or_strategy, OrStrategy::Lukasiewicz);
500        assert_eq!(
501            config.not_strategy,
502            NotStrategy::Sigmoid { temperature: 10 }
503        );
504    }
505
506    #[test]
507    fn test_probabilistic_config() {
508        let config = CompilationConfig::probabilistic();
509        assert_eq!(config.and_strategy, AndStrategy::ProbabilisticSum);
510        assert_eq!(config.or_strategy, OrStrategy::ProbabilisticSum);
511        assert_eq!(
512            config.implication_strategy,
513            ImplicationStrategy::Reichenbach
514        );
515    }
516
517    #[test]
518    fn test_fuzzy_lukasiewicz_config() {
519        let config = CompilationConfig::fuzzy_lukasiewicz();
520        assert_eq!(config.and_strategy, AndStrategy::Lukasiewicz);
521        assert_eq!(config.or_strategy, OrStrategy::Lukasiewicz);
522        assert_eq!(config.exists_strategy, ExistsStrategy::LogSumExp);
523    }
524}
tensorlogic_compiler/config.rs

tensorlogic_compiler/
config.rs
