pr4xis 0.3.0

Prove your domain is correct — ontology-driven rule enforcement with category theory, logical composition, and runtime state machines
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161

use std::marker::PhantomData;

use crate::category::Category;
use crate::category::entity::Entity;
use crate::category::relationship::Relationship;

use super::graph;

/// Domains implement this to declare their causal relationships.
///
/// A causal graph is a directed acyclic graph where edges represent
/// "A causes B" relationships.
pub trait CausalDef {
    type Entity: Entity;
    /// Direct causal pairs: (cause, effect).
    fn relations() -> Vec<(Self::Entity, Self::Entity)>;
}

/// Causal relationship morphism: cause causes effect.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct Causes<E: Entity> {
    pub cause: E,
    pub effect: E,
}

impl<E: Entity> Relationship for Causes<E> {
    type Object = E;
    fn source(&self) -> E {
        self.cause.clone()
    }
    fn target(&self) -> E {
        self.effect.clone()
    }
}

/// Category adapter for a causal graph.
///
/// Objects are the entities. Morphisms are causal relationships
/// (direct + identity + transitive closure).
pub struct CausalCategory<T: CausalDef> {
    _marker: PhantomData<T>,
}

impl<T: CausalDef> Category for CausalCategory<T> {
    type Object = T::Entity;
    type Morphism = Causes<T::Entity>;

    fn identity(obj: &T::Entity) -> Causes<T::Entity> {
        Causes {
            cause: obj.clone(),
            effect: obj.clone(),
        }
    }

    fn compose(f: &Causes<T::Entity>, g: &Causes<T::Entity>) -> Option<Causes<T::Entity>> {
        if f.effect != g.cause {
            return None;
        }
        Some(Causes {
            cause: f.cause.clone(),
            effect: g.effect.clone(),
        })
    }

    fn morphisms() -> Vec<Causes<T::Entity>> {
        let entities = T::Entity::variants();
        let adj = graph::adjacency_map(&T::relations());

        let mut morphisms = Vec::new();
        for entity in &entities {
            morphisms.push(Self::identity(entity));
            for effect in graph::reachable(entity, &adj) {
                morphisms.push(Causes {
                    cause: entity.clone(),
                    effect,
                });
            }
        }
        morphisms
    }
}

// ---- Query functions ----

/// All direct and transitive effects of a cause. Does not include the entity itself.
pub fn effects_of<T: CausalDef>(cause: &T::Entity) -> Vec<T::Entity> {
    let adj = graph::adjacency_map(&T::relations());
    graph::reachable(cause, &adj)
}

/// All direct and transitive causes of an effect. Does not include the entity itself.
pub fn causes_of<T: CausalDef>(effect: &T::Entity) -> Vec<T::Entity> {
    let adj = graph::reverse_adjacency_map(&T::relations());
    graph::reachable(effect, &adj)
}

// ---- Axioms ----

/// Axiom: asymmetry — if A causes B (and A != B), then B does NOT cause A.
pub struct Asymmetric<T: CausalDef> {
    _marker: PhantomData<T>,
}

impl<T: CausalDef> Asymmetric<T> {
    pub fn new() -> Self {
        Self {
            _marker: PhantomData,
        }
    }
}

impl<T: CausalDef> Default for Asymmetric<T> {
    fn default() -> Self {
        Self::new()
    }
}

impl<T: CausalDef> crate::logic::Axiom for Asymmetric<T> {
    fn description(&self) -> &str {
        "causation is asymmetric: if A causes B then B does not cause A"
    }

    fn holds(&self) -> bool {
        let direct = T::relations();
        for (cause, effect) in &direct {
            if cause != effect && effects_of::<T>(effect).contains(cause) {
                return false;
            }
        }
        true
    }
}

/// Axiom: no self-causation — no entity directly causes itself.
pub struct NoSelfCausation<T: CausalDef> {
    _marker: PhantomData<T>,
}

impl<T: CausalDef> NoSelfCausation<T> {
    pub fn new() -> Self {
        Self {
            _marker: PhantomData,
        }
    }
}

impl<T: CausalDef> Default for NoSelfCausation<T> {
    fn default() -> Self {
        Self::new()
    }
}

impl<T: CausalDef> crate::logic::Axiom for NoSelfCausation<T> {
    fn description(&self) -> &str {
        "no entity directly causes itself"
    }

    fn holds(&self) -> bool {
        T::relations().iter().all(|(cause, effect)| cause != effect)
    }
}