Symbolic Model Ontology

FLOW ALGEBRA
SYMBOLIC MODEL ONTOLOGY
Kireth Semantic Library | Computational Mathematical Entities
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/computational-mathematical-entities/symbolic-model-ontology.html
Authors: Mark Higgins — Sky (Recursive AI)
Status: Proposed formalisation; source page wording not independently verified.
Version: 1.0 | Date: 2026-10-14

1. PURPOSE
Represent mathematical models using symbolic expressions, typed variables, operators, assumptions, constraints and transformations. Support machine-readable reasoning, exact manipulation, verification and links to numerical models.

2. TYPED ENTITIES
SymbolicModel : Model
Symbol : Identifier
Variable : Symbol {domain: Set, units?: Unit}
Parameter : Symbol {domain: Set, value?: -Expression}
Constant : -Expression
Expression : AbstractSyntaxTree
Equation : Relation(Expression, Expression)
Inequality : Relation(Expression, Expression)
Constraint : Predicate
Assumption : Predicate
Operator : TypedFunction
Transformation : -Expression -> Expression
SolutionSet : Set(Assignment)
ProofCertificate : Derivation

3. RELATIONSHIPS
SymbolicModel HAS_VARIABLE Variable
SymbolicModel HAS_PARAMETER Parameter
SymbolicModel HAS_EXPRESSION Expression
SymbolicModel HAS_CONSTRAINT Constraint
SymbolicModel ASSUMES Assumption
Expression REFERENCES Symbol
Expression APPLIES Operator
Equation RELATES Expression Expression
Transformation REWRITES Expression
SolutionSet SATISFIES Constraint
ProofCertificate JUSTIFIES Transformation
SymbolicModel MAY_COMPILE_TO NumericalModel

4. FORMAL MODEL
M = (V, P, D, E, C, A, O)
V = finite set of variables
P = finite set of parameters
D : V union P -> Domains
E = set of well-typed symbolic expressions
C = set of constraints over V and P
A = set of assumptions
O = operator signature with input and output types
An assignment rho is admissible iff rho respects D and satisfies A.
A solution rho satisfies every c in C under the chosen interpretation.

5. CORE AXIOMS AND INVARIANTS
TYPE_SAFETY: every operator application matches its signature.
SCOPE: every free symbol is declared or explicitly external.
DEFINEDNESS: division denominators are nonzero; functions satisfy domain conditions.
EQUIVALENCE: a rewrite e -> e' is valid only if for all admissible rho, eval(e,rho) = eval(e',rho).
CONSTRAINT_PRESERVATION: an equivalent transformation preserves the solution set under stated assumptions.
UNITS: addition requires compatible dimensions; operators obey dimensional rules when units are declared.
EXACTNESS: symbolic equality is not inferred from approximate numerical agreement.

6. EXECUTABLE FLOW RULES (PSEUDOCODE)
flow PARSE_SYMBOLIC_MODEL(input):
  ast := parse(input)
  symbols := collect_free_symbols(ast)
  require symbols subset_of declared_symbols
  require typecheck(ast, operator_signatures)
  return SymbolicModel(ast, symbols, assumptions, constraints)

flow NORMALISE_EXPRESSION(e, assumptions):
  require well_typed(e)
  candidates := apply_sound_rewrite_rules(e, assumptions)
  for candidate in candidates:
    require preserve_definedness(e, candidate, assumptions)
  return canonical_choice(candidates)

flow SOLVE_SYMBOLIC(model):
  require valid_model(model)
  solutions := symbolic_solver(model.constraints, model.assumptions)
  for s in solutions:
    verify_by_substitution(s, model)
  return {solutions, verification_status, unresolved_conditions}

flow COMPILE_NUMERICAL(model, parameter_values):
  require all_required_parameters_bound(parameter_values)
  require domain_and_unit_checks_pass
  return {numerical_functions, guards, precision_policy, provenance}

7. INFERENCE RULES
IF expression references undeclared symbol THEN validation = FAIL.
IF denominator can equal zero THEN add domain guard or report unresolved condition.
IF rewrite proven under assumptions THEN SEMANTIC_EQUIVALENCE = CONDITIONAL_EQUIVALENT.
IF candidate assignment satisfies all constraints THEN candidate is VERIFIED_SOLUTION.
IF a solver returns a candidate without verification THEN label UNVERIFIED_CANDIDATE.
IF symbolic model is instantiated numerically THEN preserve provenance and approximation metadata.

8. SEMANTIC DISTINCTIONS
SymbolicModel != NumericalModel: symbols and exact relations versus instantiated numeric computation.
SymbolicModel != MathematicalModel: symbolic models are a representation class within mathematical modelling.
Expression != Equation: an equation asserts a relation between expressions.
Parameter != Variable: parameters are externally fixed for an instance; variables are solved or evaluated.
SyntacticIdentity != SemanticEquivalence: distinct syntax can denote the same value under assumptions.
ExactSolution != ApproximateSolution: exact satisfaction differs from bounded numerical error.

9. VALIDATION
CHECK parseability, declared symbols, type consistency, domain guards, unit consistency, assumption satisfiability where decidable, transformation proof status, solver output verification, and provenance completeness.
Return PASS | FAIL | UNKNOWN, with reason codes and evidence. UNKNOWN must never be silently promoted to PASS.

10. CONFIDENCE AND PROVENANCE
CONFIDENCE := {level: VERIFIED | CONDITIONAL | UNVERIFIED, evidence: [...], assumptions: [...]}.
Use VERIFIED only for derivations checked by a trusted checker or explicitly verified substitution; record checker and scope.

11. FLOW_HASH AND UPDATE_MODEL
FLOW_HASH := SHA256(canonical_UTF8(ontology_id, version, entity_schema, rules, axioms, assumptions, source_url)).
Canonicalisation must fix field ordering, Unicode normalisation and line endings.
UPDATE_MODEL := {previous_hash, new_hash, changed_fields, change_reason, validation_result, timestamp}.
Never claim a hash value without computing it on the final canonical payload.

12. AI_CONSUMPTION
input: {model_definition, symbols, assumptions, query}
output: {typed_model, inferred_relations, transformations, solutions, proof_status, confidence, provenance, errors}
Policy: disclose assumptions, avoid unsupported equivalence claims, distinguish exact and approximate results, and provide machine-checkable evidence where available.

13. EXAMPLE
variables: x : Real
parameters: a : Real
assumptions: a != 0
constraint: a*x + 2 = 0
solution: x = -2/a
verification: a*(-2/a) + 2 = 0, valid when a != 0

END FLOW ALGEBRA