pr4xis 0.23.1

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

#[allow(unused_imports)]
use alloc::{boxed::Box, format, string::String, string::ToString, vec, vec::Vec};
use core::marker::PhantomData;

use crate::category::laws::functor_law_axioms;
use crate::category::{Category, FinitelyGenerated, Functor};
use crate::logic::proof::{Verdict, combine_verdicts};
use crate::ontology::meta::{Citation, Label, ModulePath, OntologyName, Provenance};

/// An analogy is a structure-preserving map between two domains (a named Functor).
///
/// If domain A is-like domain B, there exists an analogy (functor) F: A → B
/// that maps objects and morphisms while preserving identity and composition.
pub struct Analogy<F: Functor> {
    _marker: PhantomData<F>,
}

impl<F: Functor> Analogy<F> {
    /// Validate that the analogy preserves structure (functor laws).
    pub fn validate() -> Verdict
    where
        F: 'static,
        <F::Source as Category>::Morphism: PartialEq + 'static,
        <F::Target as Category>::Morphism: PartialEq + 'static,
        // The functor identity law verifies by enumerating source objects
        // (closed-world); an analogy between closed-world domains satisfies this.
        <F::Source as Category>::Object: FinitelyGenerated,
    {
        let subverdicts: Vec<Verdict> = functor_law_axioms::<F>()
            .iter()
            .map(|l| l.verify())
            .collect();
        combine_verdicts(
            Provenance {
                name: OntologyName::new_static("AnalogyValidation"),
                description: Label::new_static(
                    "analogy preserves functor laws (identity and composition)",
                ),
                citation: Citation::parse_static(
                    "Mac Lane (1971) Categories for the Working Mathematician Ch. II §1",
                ),
                module_path: ModulePath::new_static(module_path!()),
            },
            subverdicts,
        )
    }

    /// Map a concept from the source domain to the target domain.
    pub fn translate(obj: &<F::Source as Category>::Object) -> <F::Target as Category>::Object {
        F::map_object(obj)
    }

    /// Map a relationship from the source domain to the target domain.
    pub fn translate_morphism(
        m: &<F::Source as Category>::Morphism,
    ) -> <F::Target as Category>::Morphism {
        F::map_morphism(m)
    }
}