ora-0089

6.1 From a semantic section to a learning machine

Let \(\mathbf{Doc}\) be a category of admissible categorical doctrines and let

\[ p:\int H_{\mathrm{doc}}\longrightarrow \mathbf{Doc} \]

be the hypothesis fibration of Chapter 3. For a doctrine \(\mathbb T\), the fiber \(H_{\mathrm{doc}}(\mathbb T)\) contains its admissible realized worlds. A presentation prefix determines an extension \(u_t:\mathbb T_t\to \mathbb T_{t+1}\), and reindexing gives \(u_t^*:H_{\mathrm{doc}}(\mathbb T_{t+1})\to H_{\mathrm{doc}}(\mathbb T_t)\).

The semantic ORACLE formulation asks for a coherent sequence of objects in these fibers. An algorithm must also resolve three choices hidden by that statement: which lift to select when several fit, which probe to issue when the presentation is active, and what to change when no acceptable lift exists.

Definition 6.1 UOCL instance

A UOCL instance consists of:

  1. a presentation category \(\mathbf{Pres}\) and a doctrine map \(d:\mathbf{Pres}\to \mathbf{Doc}\);

  2. the pulled-back hypothesis fibration \(p_d:\int H_d\to \mathbf{Pres}\);

  3. a query indexed category \(\mathcal Q\) and a declared observational equivalence \(\simeq _{\mathcal Q}\) in each hypothesis fiber;

  4. a category \(\mathbf{Probe}(T)\) of admissible probes at each presentation prefix \(T\), together with response extensions; and

  5. admissibility predicates for conservative lifts and for changes of doctrine.

This data says what counts as evidence, a hypothesis, a successful answer, an interaction, and a legitimate repair. It still does not choose among them.

Definition 6.2 Lift fiber

For \(u:T\to T'\) and \(M\in H_d(T)\), define

\[ \operatorname {Lift}_{u}(M)= \bigl\{ (M',\alpha )\mid M'\in H_d(T'),\; \alpha :u^*M'\to M\text{ is admissible}\bigr\} . \]

An element is conservative on a settled query family \(\mathcal Q^{\mathrm{set}}\) when every component of \(\alpha \) observed by that family is an equivalence.