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

tensorlogic_compiler/
config.rs
