Discrete Model Ontology

FLOW ALGEBRA
TITLE: Discrete Model Ontology
VERSION: 1.0
DOMAIN: Discrete Mathematics / Foundations of Discrete Mathematics
SOURCE: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/foundations-of-discrete-mathematics/discrete-model-ontology.html
STATUS: Domain-based formalisation; source page content not independently verified.
AUTHORS: Mark Higgins — Sky (Recursive AI)
PROJECT: Kireth Semantic Library

1. PURPOSE
Represent discrete models as typed mathematical objects with explicit states, relations, transitions, constraints, observations and verifiable reasoning paths.

2. TYPED ENTITIES
ENTITY DiscreteModel {id: ID, name: String, model_kind: Enum, version: String}
ENTITY State {id: ID, model_id: ID, valuation: Map, initial: Boolean, terminal: Boolean}
ENTITY Transition {id: ID, model_id: ID, source: StateID, target: StateID, label: String?, guard: Predicate?, weight: Real?}
ENTITY Variable {id: ID, domain: Set, type: Type}
ENTITY Constraint {id: ID, expression: Predicate, scope: Set[VariableID]}
ENTITY Observation {id: ID, state_id: StateID, proposition: Predicate, provenance: SourceID?}
ENTITY Property {id: ID, formula: LogicalFormula, logic: Enum}
ENTITY ModelCheckResult {model_id: ID, property_id: ID, outcome: Enum[true,false,unknown], witness: Path?, method: String}
ENTITY Provenance {source_id: ID, source_uri: URI?, timestamp: DateTime?, method: String?}

3. RELATIONSHIPS
RELATION HAS_STATE(DiscreteModel, State)
RELATION HAS_TRANSITION(DiscreteModel, Transition)
RELATION TRANSITIONS_TO(State, State) VIA Transition
RELATION HAS_VARIABLE(DiscreteModel, Variable)
RELATION SATISFIES(State, Constraint)
RELATION OBSERVES(Observation, State)
RELATION CHECKS(ModelCheckResult, Property)
RELATION DERIVED_FROM(AnyEntity, Provenance)
RELATION ABSTRACTS(DiscreteModel, System)
RELATION REFINES(DiscreteModel, DiscreteModel)

4. MODEL SEMANTICS
MODEL M = (S, S0, T, V, L, C)
  S  : set of states
  S0 : subset of S, initial states
  T  : subset of S x S, transition relation
  V  : set of typed variables
  L  : S -> powerset(AP), atomic proposition labelling
  C  : set of constraints
INVARIANT S0 subset_of S
INVARIANT forall (a,b) in T: a in S and b in S
INVARIANT every valuation respects its variable's declared domain

5. FLOW OPERATORS
FLOW CONSTRUCT_MODEL(inputs) -> DiscreteModel
  REQUIRE typed(inputs)
  BUILD states, transitions, constraints
  VALIDATE referential_integrity AND domain_membership
  EMIT model

FLOW REACHABLE(M, start) -> Set[State]
  REQUIRE start in M.S
  frontier := {start}; visited := {}
  WHILE frontier not_empty:
    take s from frontier
    IF s not_in visited:
      add s to visited
      add successors(s, M.T) to frontier
  RETURN visited

FLOW CHECK_INVARIANT(M, P) -> ModelCheckResult
  FOR EACH s in reachable_states(M):
    IF NOT P(s): RETURN false with counterexample_path(s)
  RETURN true IF complete_exploration ELSE unknown

FLOW SIMULATE(M, s0, steps) -> Path
  REQUIRE s0 in M.S0 AND steps >= 0
  APPLY enabled transitions up to steps
  RETURN observed_path

6. INFERENCE RULES
RULE TRANSITIVE_REACHABILITY:
  REACHES(a,b) AND REACHES(b,c) => REACHES(a,c)
RULE DIRECT_REACHABILITY:
  (a,b) in T => REACHES(a,b)
RULE INVARIANT_PRESERVATION:
  P(s0) AND (forall (a,b) in T: P(a) => P(b)) => P(s) for all reachable s
RULE REFINEMENT_SOUNDNESS:
  A refinement preserves property P only if the specified abstraction relation and simulation obligations are proved.
RULE COUNTEREXAMPLE:
  reachable(s) AND NOT P(s) => invariant P is false for M

7. CONFIDENCE
CONFIDENCE:
  formal_proof: 1.0 when proof is valid under declared assumptions
  exhaustive_model_check: 1.0 for the checked finite model and property
  simulation: empirical estimate only; not proof of global correctness
  incomplete_search: unknown rather than false or true
  NOTE: confidence values do not substitute for proof validity.

8. SEMANTIC_EQUIVALENCE
SEMANTIC_EQUIVALENCE:
  state_alias: equivalent only under identical typed valuations and context
  model_isomorphism: bijections preserve initial states, labels and transitions
  behavioural_equivalence: require declared bisimulation or trace-equivalence criterion
  avoid conflating graph isomorphism, bisimulation and identical behaviour

9. PROVENANCE
PROVENANCE:
  retain source URI, author, version, assumptions, modelling method and verification evidence
  attach provenance to each imported fact, constraint and inferred claim

10. FLOW_HASH
FLOW_HASH:
  algorithm: SHA-256
  input: canonical UTF-8 serialisation of model schema, axioms, operators and version
  note: compute at publication/runtime; no digest is asserted in this draft

11. UPDATE_MODEL
UPDATE_MODEL:
  accept: typed additions, removals and corrections
  validate: entity references, constraints, consistency and provenance
  invalidate: affected cached reachability, proofs and model-check results
  recompute: affected inferences and FLOW_HASH
  preserve: prior versions for reproducibility

12. AI_CONSUMPTION
AI_CONSUMPTION:
  machine_readable: true
  semantic_types: required
  inference_trace: required
  evidence_provenance: required
  uncertainty_handling: explicit unknown state
  safety: do not treat simulation output as mathematical proof
  cross_domain_links: Graph Theory, Automata, Formal Verification, Model Theory, Algorithms

13. VALIDATION
CHECK every transition references declared states
CHECK initial states belong to model
CHECK predicates are well-typed
CHECK claims identify assumptions and verification method
CHECK any asserted equivalence states its precise criterion

END FLOW ALGEBRA