Machine Native Reasoning: wider continuation

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

1 \chapter{Changing a representation without losing correctability}\label{ch:migration}
2 
3 A representation can be sufficient for yesterday's questions and insufficient for today's. The old theorem need not be false. Its target may have changed. A revision procedure must therefore distinguish two tasks: translating information already retained and acquiring information that the old record discarded.
4 
5 The simplest exact model makes this distinction precise. It also gives a constructive lower bound on the extra information required when a direct migration is impossible.
6 
7 \section{A migration map exists exactly on constant fibres}
8 Let $H$ be a finite nonempty set of possible source histories. A history may include a model tag or a past observation whose value must remain available for later correction. Let
9 \[
10  M:H\to U,\qquad N:H\to V
11 \]
12 be the old record and the required new record. Work on their attained images $U_0=M(H)$ and $V_0=N(H)$. The new record must be specified before sufficiency is claimed. It can be an answer, a correction signature, or the complete profile of future outputs in a declared finite contract.
13 
14 \begin{theorem}[Exact migration criterion]\label{r:migration}
15 There is a map $J:U_0\to V_0$ satisfying $JM=N$ if and only if
16 \[
17  M(h)=M(h')\quad\Longrightarrow\quad N(h)=N(h')
18  \qquad(h,h'\in H).
19 \]
20 When it exists, $J$ is unique on attained old records.
21 \end{theorem}
22 \begin{proof}
23 Necessity follows by applying $J$ to the equal old records. Conversely, define $J(M(h))=N(h)$. The fibre condition makes the definition independent of the representative. Every $u\in U_0$ has such a representative, so the same equation determines $J$ uniquely.
24 \end{proof}
25 
26 \source{This is the attained-record factorization of Proposition~\ref{r:factor}, applied to a representation revision. Grounded Abstraction [GA] supplies the correction-memory and evidence-migration setting. The argument does not assert a separate novelty claim for the fibre criterion.}
27 
28 A collision with unequal new records is a complete obstruction to an exact deterministic migration from the old record alone. Adding more computation cannot distinguish the two histories. A randomized translator cannot be certainly correct on both either: the same old input gives the same output law, which cannot be concentrated at two different required values.
29 
30 \section{What additional evidence must provide}
31 Suppose an allowed observation produces $E:H\to W$. A translator can use the pair $(M(h),E(h))$ rather than $M(h)$ alone.
32 
33 \begin{corollary}[Evidence-assisted migration]\label{r:migration-evidence}
34 An exact translator from the available pair $(M,E)$ to $N$ exists if and only if
35 \[
36  M(h)=M(h'),\ E(h)=E(h')\quad\Longrightarrow\quad N(h)=N(h').
37 \]
38 If a collision remains after the observation, that particular evidence interface cannot support the requested migration.
39 \end{corollary}
40 \begin{proof}
41 Apply Theorem~\ref{r:migration} to the record $h\mapsto(M(h),E(h))$.
42 \end{proof}
43 
44 This result does not choose a physical observation or show that the observation is affordable. It tests the information supplied by a specified observation. A protocol with several actions can be treated similarly once its complete attained transcript is defined. Its admissibility, state changes, and costs then require the controller analysis of Chapter~\ref{ch:inquiry}.
45 
46 \section{The least joint refinement}
47 When both the old and new uses must remain available, retain
48 \[
49  P(h)=(M(h),N(h))\in P(H).
50 \]
51 The projections recover each record. No ordering between the old and new information is required.
52 
53 \begin{proposition}[Universal property of the joint record]\label{r:joint-refinement-record}
54 If a record $R:H\to W$ determines both $M$ and $N$, then it determines $P$. In particular, $|R(H)|\ge |P(H)|$. The pair record attains this lower bound among records required to preserve both uses.
55 \end{proposition}
56 \begin{proof}
57 Let $fR=M$ and $gR=N$ on $H$. Then $w\mapsto(f(w),g(w))$ maps every attained value of $R$ to the corresponding attained pair. This map is onto $P(H)$, since every pair comes from a source history. Finiteness gives the cardinality inequality. The record $P$ itself has the required two projection maps.
58 \end{proof}
59 
60 This is a statement about distinct attained values, not the byte size of a particular data structure. It allows the new state to discard duplicated encodings while preserving both information contracts.
61 
62 \begin{theorem}[Minimum fixed-length supplementary information]\label{r:migration-bits}
63 For $u\in U_0$, put
64 \[
65  k(u)=|N(M^{-1}\{u\})|,\qquad k_* =\max_{u\in U_0}k(u).
66 \]
67 Suppose an auxiliary encoder may inspect the complete source history and sends one fixed-length binary word in addition to the old record. Exact recovery of $N$ is possible with $b$ supplementary bits if and only if $2^b\ge k_*$. Thus the minimum is $\lceil\log_2 k_*\rceil$.
68 \end{theorem}
69 \begin{proof}
70 For a fixed old record $u$, distinct required new values must receive distinct supplementary words. Otherwise the decoder would receive identical inputs with different required outputs. Hence $2^b\ge k(u)$ for every $u$.
71 
72 Conversely, within each old fibre assign distinct binary words to the distinct attained new values, using at most $k_*\le 2^b$ words. The same word can be reused in different old fibres because the decoder receives $u$ as well. Define the encoder by this fibre-specific table and decode by the inverse table. Every source history is recovered correctly.
73 \end{proof}
74 
75 The encoder's access assumption is essential. The bound does not allow a controller holding only $M(h)$ to manufacture the missing bits. It describes the amount of supplementary information when an encoder actually has the source information. With restricted observations, Corollary~\ref{r:migration-evidence} must be checked first. Code tables, acquisition, transmission, and validation also carry costs not counted by the fixed binary payload.
76 
77 \section{Migration must commute with subsequent operations}
78 Recovering one new record is not yet preserving a method. Let a common finite action alphabet act on $H$ through total maps $F_a:H\to H$. Suppose both representations close under those same source operations:
79 \[
80  M F_a=P_a M,\qquad N F_a=Q_a N.
81 \]
82 The maps $P_a$ and $Q_a$ preserve the attained record sets. These equations refer to the same source action, not merely to operations sharing a name.
83 
84 \begin{theorem}[A valid migration intertwines the common operations]\label{r:migration-operations}
85 If $JM=N$, then on $U_0$,
86 \[
87  JP_a=Q_aJ.
88 \]
89 Consequently $JP_w=Q_wJ$ for every finite action word $w$, with the execution-order convention of Chapter~\ref{ch:evidence}. Any protected readout that factors through $N$ agrees along the two migrated executions.
90 \end{theorem}
91 \begin{proof}
92 Take $u=M(h)$. Then
93 \[
94  JP_a(u)=JM(F_a h)=N(F_a h)=Q_aN(h)=Q_aJ(u).
95 \]
96 Every attained $u$ has a representative, so the equality holds throughout $U_0$. Closure keeps later values within that domain. Induction on the word length gives the continuation identity. Composing with the protected readout gives equality of outputs.
97 \end{proof}
98 
99 If a revision changes the underlying operation, the second closure equation must be proved for the changed semantics. A successful initial decoding does not imply it. For example, the identity translator on a bit preserves its current value, but cannot intertwine an old hold operation with a new flip operation. The same stored bit and the same printed operation name do not supply the missing commuting equation.
100 
101 \section{A worked change of task}
102 Use the eight histories $(b,s,n)\in\{0,1\}^3$ and the old display record $M=b\oplus s$. For display prediction under physical-bit flips, this record is sufficient. Suppose the new task requires both the display and the physical target, so $N=(b\oplus s,b)$.
103 
104 There are two possible new records inside each old display fibre. Direct migration fails, but $k_*=2$, so one supplementary bit is information-theoretically sufficient. Calibration supplies $E=s$, and
105 \[
106  b=M\oplus E
107 \]
108 gives the actual decoder. The joint old/new record has four attained states. The nuisance bit remains discarded because the new task still does not use it.
109 
110 Now require the nuisance bit as well. The new record $N'=(b\oplus s,b,n)$ has four possible values inside each old fibre, giving a two-bit supplementary lower bound. Calibration alone no longer suffices. Two histories with equal $b,s$ and different $n$ collide under $(M,E)$ but have different $N'$. The lower bound identifies a missing distinction rather than a computational bottleneck.
111 
112 \begin{figure}[htbp]\centering
113 \includegraphics[width=.93\linewidth]{figures/migration_fibres.pdf}
114 \caption{The required information depends on the revised task. Display alone has two attained values. Adding the target bit requires four joint values. Adding the nuisance bit requires eight. Calibration supplies the first missing distinction, not the second.}\label{fig:migration-fibres}
115 \end{figure}
116 
117 \section{Certificates after a change of contract}
118 A migration map transports data. A certificate authorizes a conclusion only relative to its premises. To reuse a certificate across a revision, specify an old predicate $\varphi$ on $U_0$, a new predicate $\psi$ on $V_0$, and a proved implication
119 \[
120  \varphi(u)\ \Longrightarrow\ \psi(Ju).
121 \]
122 An old witness for $\varphi(u)$ and this implication then yield the new conclusion. The implication may express semantic preservation, a stronger guard, or a deliberately weaker postcondition. It cannot be replaced by equality of file names or by an unchanged serialization format.
123 
124 Chapter~\ref{ch:revision} handles the dependency graph needed to know which such implications remain applicable. The present chapter handles information loss and operation transport. Together they separate three questions that a revision must answer: can the new record be recovered, does it support the required operations, and do the old proof premises still justify the intended conclusions?

Back to source controls

Back to Machine Native Reasoning: wider continuation