pr4xis 0.25.5

Axiomatic Intelligence — an ontology + category-theory reasoning engine: every claim derived from explicit axioms, with a proof path back to them
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

//! The `Arrow` trait — directed structures carrying kind and per-instance
//! provenance.
//!
//! # Ontological grounding
//!
//! Arrow is the Rust realisation of
//! [`crate::category::category_theory::CategoryTheoryConcept::Morphism`].
//! Mac Lane (1971) CWM Ch. I §1 uses "morphism" and "arrow" as synonyms;
//! Awodey (2010) uses "arrow" as primary. The Rust trait is `Arrow`
//! (avoids naming collision with the `Morphism` struct) and both names
//! point at the same ontological concept.
//!
//! The previous `Relationship` trait (Chen 1976 Entity-Relationship
//! database modelling vocabulary) has been absorbed — "relationship"
//! is ER modelling, not the category-theoretic or ontology-engineering
//! literature the rest of pr4xis cites. `Arrow` replaces it.
//!
//! # Per-instance provenance (required)
//!
//! Every arrow carries its own [`Provenance`] via [`Arrow::meta`]. Per
//! Gruber (1993) KAS 5 "formally-named relations", Smith et al. (2005)
//! OBO-RO "every relation-instance is named", W3C PROV-O (2013) "every
//! entity has provenance", W3C SKOS (2009) "every concept mapping has
//! labels + notes" — no anonymous arrows. `meta(&self)` is required
//! on every impl.
//!
//! # Dimensional scope
//!
//! Arrow is for **morphism-level** cells (0-cells to 0-cells within a
//! category). Higher cells — functors (1-cells in Cat), natural
//! transformations (2-cells), adjunctions (structured pairs) — keep
//! their own traits (`Functor`, `NaturalTransformation`, `Adjunction`)
//! with type-level `fn meta()`. Bénabou (1967) *Introduction to
//! Bicategories* distinguishes cells by dimension; their Rust encoding
//! follows.
//!
//! Literature:
//! - Mac Lane (1971) CWM Ch. I §1 — morphism / arrow
//! - Awodey (2010) *Category Theory* — "arrow" as primary
//! - Gruber (1993) KAS 5 — formally-named relations
//! - Smith et al. (2005) OBO-RO — relation-kinds with instance-level
//!   provenance
//! - W3C PROV-O (2013) — every entity has provenance
//! - W3C SKOS (2009) — every concept mapping has labels/notes

use core::fmt::Debug;

use super::entity::Concept;
use crate::ontology::meta::Provenance;

/// A directed structure between objects, carrying a relation kind and
/// per-instance provenance.
pub trait Arrow: Sized + Clone + Debug + Eq {
    /// The type of objects this arrow connects.
    type Object: Concept;

    /// The relation-kind tag — Subsumption, Parthood, Causation, etc.
    /// Per OBO-RO (Smith et al. 2005), every arrow has a canonical kind.
    type Kind: Copy + Debug + Eq;

    /// The domain of this arrow.
    fn source(&self) -> Self::Object;

    /// The codomain of this arrow.
    fn target(&self) -> Self::Object;

    /// The relation-kind carried by this arrow.
    fn kind(&self) -> Self::Kind;

    /// Per-instance provenance — name, description, citation, module
    /// path. Per Gruber / OBO-RO / PROV-O / SKOS — every arrow is a
    /// named, cited entity.
    ///
    /// The default uses `std::any::type_name::<Self>()` as an honest
    /// placeholder identifier with an empty citation — "no ontology
    /// source declared at this impl". The `ontology!` and
    /// `define_category!` macros override this to carry their
    /// ontology's source citation. Hand-written impls that represent
    /// a specific literature-grounded relation should override too.
    fn meta(&self) -> Provenance {
        let tn = core::any::type_name::<Self>();
        Provenance {
            name: crate::ontology::meta::OntologyName::new_static(tn),
            description: crate::ontology::meta::Label::new_static(tn),
            citation: crate::ontology::meta::Citation::EMPTY,
            module_path: crate::ontology::meta::ModulePath::new_static(module_path!()),
        }
    }
}

/// The named, round-trippable relation-kind of an [`Arrow`].
///
/// [`Arrow::Kind`] is bounded only `Copy + Debug + Eq` — the minimum to carry
/// and compare a kind in memory. `RelationKind` is the STRONGER contract a kind
/// needs to cross the wire: a canonical [`name`](Self::name) (the kind-level
/// parallel of [`Concept::name`]) and its typed inverse
/// [`from_name`](Self::from_name). The `ontology!` macro emits this impl for
/// every generated `*RelationKind` enum, forwarding to the inherent
/// `name`/`from_name` it already generates.
///
/// It is deliberately NOT a supertrait of [`Arrow::Kind`]: hand-written
/// `type Kind = ()` Arrow impls (terminal / HMI / test categories) stay legal.
/// Generic code that must name a kind on the wire bounds it at the USE SITE
/// (`where <C::Morphism as Arrow>::Kind: RelationKind`), the same discipline
/// structural reasoning already uses for `KindOf<C>: PartialEq`.
///
/// Per OBO-RO (Smith et al. 2005) a relation is a named, re-resolvable kind;
/// W3C SKOS (2009) — a mapping is carried by stable name, never an index.
pub trait RelationKind: Copy + Debug + Eq {
    /// The kind's canonical name — the stable wire identity (never `Debug`,
    /// never a positional discriminant).
    fn name(&self) -> &'static str;

    /// Re-resolve a kind from its canonical [`name`](Self::name); fail-closed
    /// `None` for an unknown name.
    fn from_name(name: &str) -> Option<Self>
    where
        Self: Sized;
}