Language Recognition Ontology

FLOW ALGEBRA
LANGUAGE RECOGNITION ONTOLOGY
Version: 1.0
Canonical URL: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/formal-languages/language-recognition-ontology.html
Authors: Mark Higgins — Sky (Recursive AI)
Publisher: Kireth Research | https://kirethresearch.org

1. PURPOSE
Formalise the entities, relations, computations and validation rules involved in deciding whether a string belongs to a formal language. Distinguish recognition, decision, parsing and generation, and preserve computational-model and resource-bound assumptions.

2. SIGNATURE AND TYPES
sort Symbol
sort Alphabet = finite_set(Symbol)
sort String(Sigma) = Sigma*
sort Language(Sigma) = subset(String(Sigma))
sort Grammar
sort Automaton
sort Recogniser
sort Configuration
sort State
sort Transition
sort Computation
sort Result = {ACCEPT, REJECT, UNKNOWN, DIVERGE}
sort LanguageClass = {REGULAR, CONTEXT_FREE, CONTEXT_SENSITIVE, RECURSIVE, RECURSIVELY_ENUMERABLE}
sort ResourceBound

entity L: Language(Sigma)
entity w: String(Sigma)
entity M: Recogniser
entity G: Grammar

3. CORE RELATIONS
MEMBER_OF(w,L) iff w in L
RECOGNISES(M,L) iff forall w: (w in L iff M accepts w)
DECIDES(M,L) iff RECOGNISES(M,L) and HALTS_ON_ALL_INPUTS(M)
GENERATES(G,L) iff L(G) = L
ACCEPTS(M,w) iff an accepting computation of M on w exists
REJECTS(M,w) iff M halts in a rejecting outcome on w
HALTS_ON_ALL_INPUTS(M) iff forall w: M halts on w
EQUIVALENT_RECOGNISERS(M1,M2) iff L(M1) = L(M2)

4. INPUT AND OUTPUT CONTRACT
input: alphabet Sigma; finite string w in Sigma*; recogniser M with declared operational semantics
output: ACCEPT, REJECT, UNKNOWN or DIVERGE (where divergence is established or modelled)
precondition: M and its alphabet/input encoding are well-formed
postcondition: ACCEPT only if an accepting computation exists; REJECT only if the relevant rejecting semantics are satisfied
note: a bounded simulation timeout produces UNKNOWN, not REJECT or a proof of DIVERGE

5. RECOGNITION FLOW
flow LanguageRecognition(M,w):
  VALIDATE_ALPHABET(M,w)
  VALIDATE_MODEL(M)
  INITIALISE_CONFIGURATION(M,w)
  EXECUTE_TRANSITIONS(M,w)
  if ACCEPTING_CONFIGURATION_REACHED: return ACCEPT
  if REJECTING_HALT_REACHED: return REJECT
  if RESOURCE_LIMIT_REACHED: return UNKNOWN
  if NONTERMINATION_PROVEN: return DIVERGE
  otherwise: continue computation

6. INFERENCE RULES
R1: ACCEPTS(M,w) and RECOGNISES(M,L) => MEMBER_OF(w,L)
R2: RECOGNISES(M,L) and MEMBER_OF(w,L) => ACCEPTS(M,w)
R3: DECIDES(M,L) and not MEMBER_OF(w,L) => M halts and rejects w
R4: DECIDES(M,L) => HALTS_ON_ALL_INPUTS(M)
R5: GENERATES(G,L) and DERIVES(G,start,w) => MEMBER_OF(w,L)
R6: EQUIVALENT_RECOGNISERS(M1,M2) => forall w: ACCEPTS(M1,w) iff ACCEPTS(M2,w)
R7: DETERMINISTIC_FINITE_AUTOMATON(M) => DECIDES(M,L(M))
R8: DECIDABLE(L) => RECOGNISABLE(L)
R9: RECOGNISABLE(L) and RECOGNISABLE(complement(L)) => DECIDABLE(L)

7. AUTOMATA AND LANGUAGE CLASSES
REGULAR: recognised by finite automata; membership decidable
CONTEXT_FREE: recognised by nondeterministic pushdown automata; membership decidable
CONTEXT_SENSITIVE: recognised by linear bounded automata under standard nondeterministic conventions; membership decidable
RECURSIVE: decided by Turing machines halting on every input
RECURSIVELY_ENUMERABLE: recognised by Turing machines that may not halt on nonmembers
containment: REGULAR subseteq CONTEXT_FREE subseteq CONTEXT_SENSITIVE subseteq RECURSIVE subseteq RECURSIVELY_ENUMERABLE
all displayed containments are proper for the standard language classes

8. EXECUTION SEMANTICS
INITIAL(M,w) -> c0
STEP(M,ci,ci+1) iff the transition relation permits ci -> ci+1
ACCEPTS(M,w) iff exists finite path c0 ->* ca with ca accepting
For a deterministic decider, every input has a finite computation ending in ACCEPT or REJECT.
For nondeterministic recognition, acceptance means at least one accepting branch; rejecting an input requires that no accepting branch exists under the model's semantics.

9. RESOURCE MODEL
TIME(M,w): number of transition steps, when defined
SPACE(M,w): maximum work/storage usage, according to the machine model
BOUNDED_RUN(M,w,b): simulate under bound b; unresolved outcome is UNKNOWN
Complexity depends on input encoding, machine model and deterministic/nondeterministic assumptions.
A finite resource bound does not generally establish nonmembership in a recursively enumerable language.

10. EXAMPLES
Example A: Sigma={a,b}; L={w | number_of_a(w) is even}.
A two-state DFA toggles parity on 'a', ignores 'b', and accepts exactly L.
recognise('abba') = ACCEPT; recognise('aba') = ACCEPT; recognise('aab') = ACCEPT; recognise('abb') = REJECT.

Example B: L={a^n b^n | n >= 0}.
A context-free grammar S -> aSb | epsilon generates L.
recognise('aabb') = ACCEPT; recognise('aab') = REJECT.

Example C: L={a^n b^n c^n | n >= 1}.
L is context-sensitive and not context-free; an LBA can decide membership.
recognise('aabbcc') = ACCEPT; recognise('aabcc') = REJECT.

11. SEMANTIC EQUIVALENCE
SEMANTIC_EQUIVALENCE:
  accept: "membership confirmed by the specified recogniser semantics"
  recognise: "accept all and only members of a language"
  decide: "recognise with guaranteed termination on all inputs"
  parse: "recover a syntactic derivation or structural analysis, when available"
  generate: "define or enumerate strings belonging to a language"
  warning: "recognise, decide, parse and generate are related but not interchangeable operations"

12. CONSTRAINTS AND VALIDATION
C1: Alphabet must be finite for the standard formal-language model.
C2: Input string must use symbols from the declared alphabet.
C3: A recogniser need not halt on nonmembers.
C4: A decider must halt on every input.
C5: Timeout is not proof of rejection or divergence.
C6: Acceptance semantics for nondeterministic machines use existence of an accepting branch.
C7: Membership and equivalence claims must name the machine/grammar model.
C8: Do not infer language-class membership solely from a single accepted string.

13. DEPENDENCIES AND ONTOLOGY LINKS
IS_A(LanguageRecognition, FormalLanguageComputation)
USES(LanguageRecognition, Alphabet)
USES(LanguageRecognition, String)
USES(LanguageRecognition, Automaton)
RELATED_TO(LanguageRecognition, FormalGrammar)
RELATED_TO(LanguageRecognition, RegularLanguage)
RELATED_TO(LanguageRecognition, ContextFreeGrammar)
RELATED_TO(LanguageRecognition, ContextSensitiveLanguage)
RELATED_TO(LanguageRecognition, Computability)
RELATED_TO(LanguageRecognition, Parsing)

14. CONFIDENCE AND PROVENANCE
CONFIDENCE:
  formal_definitions: HIGH
  standard_class_correspondences: HIGH
  bounded_runtime_outcomes: CONDITIONAL_ON_MODEL_AND_BOUND
PROVENANCE:
  basis: standard formal-language theory, automata theory and computability definitions
  scope: mathematical specification; not a claim that a particular website executes this algebra

15. FLOW HASH AND UPDATE MODEL
FLOW_HASH:
  method: SHA-256 over canonical UTF-8 flow text
  value: COMPUTE_ON_PUBLICATION
UPDATE_MODEL:
  version: 1.0
  trigger: correction of semantics, expansion of language classes or model-specific rules
  policy: retain version history and revalidate examples on revision

16. AI CONSUMPTION
AI_CONSUMPTION:
  representation: typed declarative ontology and executable-style inference rules
  intended_uses: semantic retrieval, knowledge graphs, automated reasoning, education, formal-methods tooling
  required_context: alphabet, language definition, recogniser model, termination assumptions
  uncertainty_policy: report UNKNOWN when computational evidence is insufficient
  safety_rule: never turn a timeout into a proof of nonmembership

END FLOW ALGEBRA