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

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

use super::property::Quality;

/// An ontology: what exists, how things relate, and what rules govern them.
///
/// An `Ontology` ties together:
/// - A category (individuals + relations with composition)
/// - Qualities on individuals (attributes, capabilities)
/// - Axioms — all claims this ontology asserts
///
/// # One method for axioms (#168)
///
/// `Ontology` exposes a single required [`Ontology::axioms`] method. The prior
/// `structural_axioms()` / `domain_axioms()` split was coding convenience
/// — no source literature (Gruber 1993; Guarino 2009; Spivak 2012;
/// Smith et al. 2005 OBO-RO) distinguishes them as categories of
/// axiom. At the corpus level every axiom is a claim that must hold;
/// provenance (macro-generated structural property vs hand-authored
/// domain claim) is metadata, not kind.
///
/// Implementers combine whatever sources they use. The canonical
/// pattern uses [`crate::ontology::reasoning::structural_axioms_for`]
/// to inherit structural axioms from the Relations catalog (Smith et
/// al. 2005 OBO-RO), then appends hand-written domain axioms:
///
/// ```text
/// impl Ontology for FooOntology {
///     fn axioms() -> Vec<Box<dyn Axiom>> {
///         let mut all = structural_axioms_for::<Self::Cat>();
///         all.push(Box::new(MyDomainAxiom));
///         all
///     }
/// }
/// ```
///
/// Structural axioms are *inherited* — an ontology using the kind
/// `Subsumption` picks up `NoCyclesOnKind` and `AntisymmetricOnKind`
/// without re-emitting them. See the `catalog` module for the full
/// rule table.
///
/// The ontology validates itself — if it compiles and passes
/// validation, the domain model is mathematically sound.
pub trait Ontology {
    /// The underlying category (individuals + relations).
    type Cat: Category;

    /// Qualities that individuals can have.
    type Qual: Quality<Individual = <Self::Cat as Category>::Object>;

    /// All axioms this ontology asserts — merged from whatever sources
    /// (macro-generated structural + hand-authored domain) the
    /// implementer uses.
    fn axioms() -> Vec<Box<dyn Axiom>>;

    /// Validate the entire ontology: category laws + all axioms.
    ///
    /// Returns a typed [`Verdict`] (#160 / #162):
    /// - `Ok(Box<dyn Proof>)` — every category law and axiom discharges
    /// - `Err(Box<dyn Counterexample>)` — one or more sub-claims fail; the
    ///   counterexample carries the passing sub-proofs for context and the
    ///   specific failing sub-counterexamples
    ///
    /// Pattern-match the return; core does not expose any `is_valid() -> bool`
    /// convenience (see `feedback_core_no_bool_api`).
    fn validate() -> Verdict
    where
        Self::Cat: 'static,
        <Self::Cat as Category>::Morphism: PartialEq + 'static,
        // The category identity law verifies by enumerating objects
        // (closed-world); a domain ontology's concepts are finitely generated.
        <Self::Cat as Category>::Object: FinitelyGenerated,
    {
        let mut subverdicts: Vec<Verdict> = Vec::new();

        for law in category_law_axioms::<Self::Cat>() {
            subverdicts.push(law.verify());
        }
        for axiom in Self::axioms() {
            subverdicts.push(axiom.verify());
        }

        let meta = Provenance {
            name: OntologyName::new_static("OntologyValidation"),
            description: Label::new_static("aggregate validation: category laws + ontology axioms"),
            citation: Citation::parse_static(
                "Mac Lane (1971) Categories for the Working Mathematician; \
                 Barr & Wells (1999) CTCS §4 sketches; \
                 Spivak (2012) Functorial Data Model §§2–3",
            ),
            module_path: ModulePath::new_static(module_path!()),
        };
        combine_verdicts(meta, subverdicts)
    }
}