Path Ontology

FLOW ALGEBRA
PATH ONTOLOGY — DISCRETE MATHEMATICS / GRAPH THEORY
Version: 1.0
Source: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/graph-theory/path-ontology.html
Authors: Mark Higgins — Sky (Recursive AI)
Project: Kireth Semantic Library | https://kirethresearch.org
Status: Formal mathematical model; source-page text not independently verified.

1. PURPOSE
Represent graph paths as typed, verifiable sequences of vertices and incident edges. Distinguish walks, trails, simple paths, cycles, and directed paths. Support reachability, shortest-path reasoning and semantic retrieval.

2. TYPED ENTITIES
Graph := (V: Set[Vertex], E: Set[Edge], directed: Boolean)
Vertex := identifier within V
Edge := (source: Vertex, target: Vertex, id?: Identifier, weight?: Real)
Walk := (vertices: Sequence[Vertex], edges: Sequence[Edge])
Trail := Walk with pairwise-distinct edge identifiers
Path := Walk with pairwise-distinct vertices (simple-path convention)
ClosedWalk := Walk with first vertex = last vertex
Cycle := ClosedWalk with no repeated vertices except first/last, and positive length
PathLength := NaturalNumber (number of edges)
PathWeight := Real (sum of edge weights when defined)
Reachability := Relation[Vertex, Vertex]

3. WELL-FORMEDNESS
For W=(v0,e1,v1,...,ek,vk), k >= 0:
  all vi in V; all ei in E;
  directed graph: ei goes from v(i-1) to vi;
  undirected graph: endpoints(ei) = {v(i-1),vi}.
Zero-edge walk (v0) is permitted; it is a trivial path.
Parallel edges require edge identifiers to distinguish trails.

4. CORE OPERATIONS
validate_walk(G,W) -> Boolean
is_trail(W) -> Boolean
is_simple_path(W) -> Boolean
start(W) := v0
end(W) := vk
length(W) := k
reverse(W) := reversed vertex and edge sequence (valid in undirected graphs; in directed graphs only if reversed arcs exist)
concatenate(W1,W2) := W1 followed by W2 if end(W1)=start(W2)
subwalk(W,i,j) := contiguous segment from vi to vj where 0 <= i <= j <= k
reachable(G,u,v) := exists a directed/undirected walk from u to v as appropriate
shortest_path(G,u,v,cost) := minimum-cost admissible path if one exists and a minimum is attained

5. FORMAL RELATIONSHIPS
Path IS_A Walk
Trail IS_A Walk
SimplePath IS_A Trail (when edges are identified and the graph has no loops along the path)
Cycle IS_A ClosedWalk
Path CONNECTS Vertex TO Vertex
Path CONTAINS Vertex
Path TRAVERSES Edge
Path BELONGS_TO Graph
Reachability DERIVED_FROM WalkExistence
ShortestPath OPTIMISES PathWeight

6. AXIOMS AND LAWS
A1. A simple path has no repeated vertices.
A2. A trail has no repeated edges.
A3. Every simple path is a trail.
A4. A walk of k edges has k+1 vertex occurrences.
A5. A path exists from u to v iff a walk exists from u to v (for finite graphs; indeed holds generally for finite walks by removing cycles).
A6. Concatenation of compatible walks is associative as a sequence operation.
A7. Concatenating simple paths need not yield a simple path.
A8. For unweighted graphs, shortest path length is minimum edge count.
A9. For nonnegative edge weights, a shortest walk can be chosen to be a simple path whenever u != v and a finite minimum exists.
A10. Directed reachability is reflexive and transitive, but need not be symmetric.
A11. Undirected reachability is an equivalence relation.

7. INFERENCE RULES
R1. EDGE_TO_REACH: (u,v) in E -> reachable(u,v) [respect direction].
R2. REACH_TRANSITIVE: reachable(u,v) and reachable(v,w) -> reachable(u,w).
R3. TRIVIAL_REACH: u in V -> reachable(u,u).
R4. PATH_TO_REACH: valid_path(P) and start(P)=u and end(P)=v -> reachable(u,v).
R5. NONREACHABILITY: no graph-search traversal from u reaches v in a finite fully enumerated graph -> not reachable(u,v).
R6. SHORTEST_PATH: candidate path P and proof no admissible path has smaller cost -> shortest_path(P).

8. EXAMPLES
G: V={A,B,C,D}; undirected E={{A,B},{B,C},{A,C},{C,D}}.
[A,B,C,D] is a simple path of length 3.
[A,B,C,A] is a cycle, not a simple path under the distinct-vertex convention.
[A,B,C,B] is a walk but not a trail, because {B,C} is reused.
[A,C,D] is a shortest unweighted path from A to D of length 2.

9. VALIDATION
Check vertex and edge membership, edge direction, adjacency of consecutive vertices, repeated vertices/edges, endpoints, edge-count consistency and weight definitions.
Reject disconnected vertex sequences and wrong-way directed edges.
For shortest-path assertions require a valid optimisation proof or a verified algorithm with appropriate preconditions (e.g. BFS for unit weights; Dijkstra for nonnegative weights; Bellman-Ford for negative edges without reachable negative cycles affecting the destination).
Do not treat an unverified shortest-path claim as established.

10. SEMANTIC_EQUIVALENCE
"simple path" <=> "vertex-simple path" in this ontology.
"path" is ambiguous across sources: some authors use it for any walk; preserve the local definition.
"route" is context-dependent and not automatically logically equivalent to path.
"directed path" and "undirected path" are not interchangeable.

11. CONFIDENCE
Formal definitions and elementary theorems: 1.00 when assumptions are satisfied.
Algorithmic results: 1.00 only after preconditions and execution/proof verification.
Extracted or mapped external claims: attach provenance, evidence and calibrated confidence; never assign certainty solely from terminology.

12. FLOW_HASH
Canonicalise UTF-8 text, normalise line endings to LF, serialise typed statements in deterministic order, and compute SHA-256 externally.
FLOW_HASH := SHA256(canonical_serialisation); hash value is not asserted until computed.

13. UPDATE_MODEL
On graph mutation, invalidate affected reachability and shortest-path results; recompute or incrementally update with provenance.
Record version, timestamp, graph identity, changed vertices/edges, validation status and new hash.

14. AI_CONSUMPTION
Expose machine-readable typed definitions, formal predicates, rule preconditions, counterexamples and provenance.
Preserve directionality, path-versus-walk distinction, weighting assumptions and uncertainty.
Never infer reachability from semantic similarity alone.

END FLOW ALGEBRA