pr4xis 0.5.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

use std::collections::HashMap;
use std::marker::PhantomData;

use crate::category::entity::Entity;

/// Domains implement this to declare context-dependent disambiguation.
///
/// Context is the semantic mechanism for resolving ambiguity:
/// given an ambiguous entity and a contextual signal, produce
/// the correct interpretation.
///
/// This is NOT a Category — it's a ternary relation:
/// (ambiguous entity, signal) → resolution.
///
/// Example: ("bank", MoneyContext) → FinancialInstitution
///          ("bank", RiverContext) → Riverbank
pub trait ContextDef {
    /// The ambiguous entities that need disambiguation.
    type Entity: Entity;
    /// Contextual signals that guide disambiguation.
    type Signal: Entity;
    /// Resolved interpretations.
    type Resolution: Entity;

    /// Resolution rules: (entity, signal) → resolution.
    fn resolutions() -> Vec<(Self::Entity, Self::Signal, Self::Resolution)>;
}

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

/// Resolve an ambiguous entity given a contextual signal.
pub fn resolve<T: ContextDef>(entity: &T::Entity, signal: &T::Signal) -> Option<T::Resolution> {
    T::resolutions()
        .into_iter()
        .find(|(e, s, _)| e == entity && s == signal)
        .map(|(_, _, r)| r)
}

/// All possible resolutions for an ambiguous entity (across all signals).
pub fn interpretations<T: ContextDef>(entity: &T::Entity) -> Vec<(T::Signal, T::Resolution)> {
    T::resolutions()
        .into_iter()
        .filter(|(e, _, _)| e == entity)
        .map(|(_, s, r)| (s, r))
        .collect()
}

/// All signals that can disambiguate a given entity.
pub fn signals_for<T: ContextDef>(entity: &T::Entity) -> Vec<T::Signal> {
    T::resolutions()
        .into_iter()
        .filter(|(e, _, _)| e == entity)
        .map(|(_, s, _)| s)
        .collect()
}

/// All entities that are ambiguous (have more than one possible resolution).
pub fn ambiguous_entities<T: ContextDef>() -> Vec<T::Entity> {
    let mut counts: HashMap<T::Entity, usize> = HashMap::new();
    for (e, _, _) in T::resolutions() {
        *counts.entry(e).or_default() += 1;
    }
    counts
        .into_iter()
        .filter(|(_, count)| *count > 1)
        .map(|(e, _)| e)
        .collect()
}

// ---- Axioms ----

/// Axiom: every resolution is deterministic — no (entity, signal) pair
/// maps to more than one resolution.
pub struct Deterministic<T: ContextDef> {
    _marker: PhantomData<T>,
}

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

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

impl<T: ContextDef> crate::logic::Axiom for Deterministic<T> {
    fn description(&self) -> &str {
        "context resolution is deterministic: each (entity, signal) has at most one resolution"
    }

    fn holds(&self) -> bool {
        let resolutions = T::resolutions();
        let mut seen: HashMap<(T::Entity, T::Signal), T::Resolution> = HashMap::new();
        for (e, s, r) in resolutions {
            if let Some(existing) = seen.get(&(e.clone(), s.clone())) {
                if *existing != r {
                    return false;
                }
            } else {
                seen.insert((e, s), r);
            }
        }
        true
    }
}

/// Axiom: every ambiguous entity has at least two distinct resolutions.
/// (If an entity only has one resolution, it's not truly ambiguous.)
pub struct TrueAmbiguity<T: ContextDef> {
    _marker: PhantomData<T>,
}

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

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

impl<T: ContextDef> crate::logic::Axiom for TrueAmbiguity<T> {
    fn description(&self) -> &str {
        "every entity in the context map has at least two distinct resolutions"
    }

    fn holds(&self) -> bool {
        let mut resolutions_per_entity: HashMap<T::Entity, Vec<T::Resolution>> = HashMap::new();
        for (e, _, r) in T::resolutions() {
            let rs = resolutions_per_entity.entry(e).or_default();
            if !rs.contains(&r) {
                rs.push(r);
            }
        }
        resolutions_per_entity.values().all(|rs| rs.len() >= 2)
    }
}