Algorithm Ontology

FLOW ALGEBRA
ALGORITHM ONTOLOGY
Version: 1.0
Canonical URL: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/algorithmic-mathematics/algorithm-ontology-2.html
Authors: Mark Higgins — Sky (Recursive AI)
Publisher: Kireth Research | https://kirethresearch.org
Document type: Formal ontology and typed reasoning specification

1. PURPOSE
Represent algorithms as finite, effectively specified computational procedures with explicit inputs, outputs, states, transition semantics, termination properties, correctness obligations and resource costs. Distinguish an algorithm from an implementation, heuristic, specification or particular execution.

2. SIGNATURE AND TYPES
sort Algorithm
sort Problem
sort Input
sort Output
sort State
sort Instruction
sort Transition
sort ExecutionTrace
sort Specification
sort Precondition
sort Postcondition
sort Invariant
sort Variant
sort Proof
sort Implementation
sort ComputationalModel
sort Resource = {TIME, SPACE}
sort Status = {ACCEPT, REJECT, ERROR, TIMEOUT, UNKNOWN}
sort Truth = {TRUE, FALSE, UNDETERMINED}
entity A: Algorithm
entity P: Problem
entity x: Input
entity y: Output
entity s: State
entity M: ComputationalModel

3. CORE RELATIONS
SOLVES(A,P): algorithm A meets the declared solution specification for every admissible instance of P.
HAS_INPUT_DOMAIN(A,D): A accepts inputs from domain D.
HAS_OUTPUT_CODOMAIN(A,C): normal outputs of A belong to C.
HAS_PRECONDITION(A,pre): pre describes admissible starting conditions.
HAS_POSTCONDITION(A,post): post describes the required outcome after normal termination.
HAS_INITIAL_STATE(A,x,s0): s0 encodes the initial state for input x.
STEP(A,s,s2): one legal operational transition takes state s to state s2.
HALTS(A,s): no further computational transition is required at terminal state s.
RETURNS(A,x,y): A terminates normally on x and produces y.
IMPLEMENTS(I,A): implementation I realises A under a declared model and representation.
USES_MODEL(A,M): costs and primitive operations are interpreted in M.
HAS_INVARIANT(A,inv): inv holds at the required program points on every reachable execution.
HAS_VARIANT(A,v): well-founded measure v decreases on designated progress transitions.
HAS_TIME_BOUND(A,T,M): runtime is bounded by T under M and the stated input-size measure.
HAS_SPACE_BOUND(A,S,M): memory use is bounded by S under M and the stated accounting convention.

4. SEMANTIC DEFINITIONS
RUN(A,x) = maximal sequence s0,s1,... where HAS_INITIAL_STATE(A,x,s0) and STEP(A,si,si+1).
TERMINATES(A,x) iff RUN(A,x) is finite and ends in a terminal state.
PARTIAL_CORRECT(A,pre,post) iff forall x satisfying pre, every normally terminating execution satisfies post.
TOTAL_CORRECT(A,pre,post) iff PARTIAL_CORRECT(A,pre,post) and forall x satisfying pre: TERMINATES(A,x).
DETERMINISTIC(A) iff each reachable nonterminal state has at most one successor under STEP.
NONDETERMINISTIC(A) iff some reachable state may have multiple legal successors; acceptance and correctness semantics must specify the quantifier over branches.
COMPUTES(A,f,D) iff forall x in D: TERMINATES(A,x) and RETURNS(A,x,f(x)).
EQUIVALENT(A,B,D) iff forall x in D both terminate and return observationally equivalent outputs, relative to the stated observation model.

5. EXECUTION FLOW
flow "AlgorithmExecution" v1.0
input: A:Algorithm, x:Input, M:ComputationalModel
require: x in HAS_INPUT_DOMAIN(A) and precondition(A,x)
state := INITIAL_STATE(A,x)
trace := [state]
while not HALTS(A,state):
  require: a legal STEP(A,state,next_state) exists
  state := next_state
  append(trace,state)
  if execution budget exhausted: return (UNKNOWN,trace)
if state indicates normal completion:
  y := DECODE_OUTPUT(state)
  return (ACCEPT,y,trace)
else:
  return (ERROR,trace)
# A resource-budget UNKNOWN does not prove nontermination.

6. INFERENCE RULES
R1: HAS_PRECONDITION(A,pre) and pre(x) and RETURNS(A,x,y) and post(x,y) -> POSTCONDITION_VERIFIED_FOR_RUN(A,x,y).
R2: INITIAL_INVARIANT(inv) and PRESERVED_BY_EACH_STEP(inv) -> INVARIANT_ON_REACHABLE_STATES(A,inv).
R3: PARTIAL_CORRECT(A,pre,post) and TERMINATES_ON_DOMAIN(A,pre) -> TOTAL_CORRECT(A,pre,post).
R4: WELL_FOUNDED(v) and STRICT_DECREASE_ON_PROGRESS(v) and NO_INFINITE_STUTTER(A) -> TERMINATES_ON_DOMAIN(A,pre).
R5: COMPUTES(A,f,D) and COMPUTES(B,f,D) -> EQUIVALENT(A,B,D) for the same output observation model.
R6: HAS_TIME_BOUND(A,T,M) and T(n) in O(g(n)) -> ASYMPTOTIC_UPPER_TIME(A,O(g(n)),M).
R7: IMPLEMENTS(I,A) does not alone imply equal machine-level time or space complexity.
R8: TEST_PASSES(A,x) does not imply TOTAL_CORRECT(A) for an infinite domain.

7. CORRECTNESS CONTRACT
preconditions: explicitly declare input domain, data representation, arithmetic model and exceptional inputs.
postconditions: define output validity, error handling and observable side effects.
safety: show invariant preservation and absence of forbidden reachable states.
liveness: show progress or provide an explicit conditional-termination statement.
termination: provide a well-founded decreasing variant, a finite-state argument or another valid proof.
proof status: distinguish PROVED, TESTED, ASSUMED and UNKNOWN.

8. COMPLEXITY AND RESOURCES
INPUT_SIZE(x,M): nonnegative size measure in model M.
TIME(A,x,M): number or cost of primitive operations, with a stated cost convention.
SPACE(A,x,M): peak storage use, stating whether input/output storage is counted.
WORST_TIME(A,n,M) = sup {TIME(A,x,M) | INPUT_SIZE(x,M)=n}, where defined.
BEST_TIME(A,n,M) = inf {TIME(A,x,M) | INPUT_SIZE(x,M)=n}, where defined.
AVERAGE_TIME(A,n,M,mu) = expectation over a declared input distribution mu.
ASYMPTOTIC_UPPER: Big-O; ASYMPTOTIC_LOWER: Big-Omega; ASYMPTOTIC_TIGHT: Big-Theta.
# Complexity depends on representation, machine model, input-size measure and cost assumptions.

9. ALGORITHM DESIGN RELATIONSHIPS
USES_PARADIGM(A,RECURSION)
USES_PARADIGM(A,DIVIDE_AND_CONQUER)
USES_PARADIGM(A,DYNAMIC_PROGRAMMING)
USES_PARADIGM(A,GREEDY)
USES_PARADIGM(A,BACKTRACKING)
USES_PARADIGM(A,BRANCH_AND_BOUND)
# These are optional classifications, not mutually exclusive categories.
SUBROUTINE_OF(A1,A2): A1 is invoked as a component of A2.
REFINES(A2,A1): A2 preserves A1's declared externally observable contract under refinement assumptions.

10. WORKED EXAMPLE: LINEAR SEARCH
problem: find an index i in a finite array a of length n such that a[i]=target, or return NONE.
input: a[0..n-1], target
output: i in {0,...,n-1} or NONE
pre: n >= 0 and array accesses within bounds
algorithm:
  for i from 0 to n-1:
    if a[i] == target: return i
  return NONE
invariant: before iteration i, no index j with 0 <= j < i matches target.
variant: n-i, a nonnegative integer strictly decreasing on each completed iteration.
post: returned index is valid and matches target; NONE iff no index matches.
time: O(n) worst case, O(1) best case under constant-time equality and access.
auxiliary_space: O(1) under the same model.

11. COUNTEREXAMPLES AND LIMITATIONS
C1: An unbounded loop without a termination argument is not established as a total algorithm on its declared domain.
C2: A passing finite test suite cannot establish correctness for all possible inputs.
C3: Equal Big-O bounds do not establish identical running times.
C4: Two implementations may compute the same function but differ in overflow behaviour or side effects.
C5: A heuristic may produce useful results without guaranteeing an optimal or even valid solution unless its contract says so.
C6: An undecidable problem cannot have a total algorithm deciding every instance in a standard effective computation model.

12. SEMANTIC EQUIVALENCE
ALGORITHM ~ EFFECTIVE_PROCEDURE only when finite specification and executable operational meaning are preserved.
ALGORITHM != IMPLEMENTATION; one algorithm may have multiple implementations.
ALGORITHM != PROGRAM; a program may be incomplete, nonterminating or implement multiple algorithms.
ALGORITHM != HEURISTIC; heuristic status depends on the guarantee being claimed.
CORRECTNESS != PERFORMANCE; proof of a result does not imply an efficiency bound.

13. VALIDATION
V1: every algorithm has an input domain, output contract and execution semantics.
V2: every transition references well-typed states.
V3: every claimed total-correctness result includes partial correctness and termination evidence.
V4: every asymptotic bound declares a size measure and computational model.
V5: no timeout or UNKNOWN is misreported as proof of nontermination.
V6: every semantic equivalence specifies the observation domain and assumptions.
V7: example execution respects array bounds and invariant.

14. CONFIDENCE
CONFIDENCE(formal_definition) = HIGH, conditional on declared standard computational semantics.
CONFIDENCE(derived_claim) = HIGH only when premises and proof obligations are satisfied.
CONFIDENCE(empirical_runtime) = CONTEXT_DEPENDENT; measurements require workload and hardware metadata.
CONFIDENCE(untested_algorithm) = UNKNOWN until supported by proof or evidence.

15. FLOW_HASH
FLOW_HASH.algorithm = SHA256(canonicalised ontology body excluding the FLOW_HASH value itself)
FLOW_HASH.canonicalisation = UTF-8, LF line endings, stable field ordering
FLOW_HASH.status = COMPUTE_ON_PUBLICATION
# Do not claim a fixed digest before canonical publication content is final.

16. UPDATE_MODEL
UPDATE_MODEL.version = 1.0
UPDATE_MODEL.strategy = SEMANTIC_VERSIONING
UPDATE_MODEL.triggers = [definition_change, inference_rule_change, proof_correction, example_correction, reference_update]
UPDATE_MODEL.compatibility = preserve type and predicate meanings or increment major version
UPDATE_MODEL.provenance = retain author, date, change rationale and prior version reference

17. AI_CONSUMPTION
AI_CONSUMPTION.mode = TYPED_ONTOLOGY_AND_REASONING
AI_CONSUMPTION.tasks = [algorithm_classification, specification_checking, correctness_reasoning, complexity_analysis, semantic_retrieval, educational_explanation]
AI_CONSUMPTION.requirements = [explicit_assumptions, typed_inputs, evidence_tracking, uncertainty_reporting]
AI_CONSUMPTION.prohibitions = [invented_proofs, unsupported_complexity_claims, conflating_test_results_with_formal_verification]
AI_CONSUMPTION.output = {claim, assumptions, derivation_or_evidence, confidence, limitations}

18. RELATED ONTOLOGIES
parent: Algorithmic Mathematics
related: Algorithm Design; Algorithm Analysis; Computational Complexity; Recursion; Divide and Conquer; Greedy Algorithm; Dynamic Programming; Backtracking; Branch and Bound; Computability; Formal Verification

END FLOW ALGEBRA