1: \section{Computation and legalization}\label{s.comp}
2:
3: \subsection{Coding and decoding}
4:
5: \subsubsection{Main track and redundancy track}\label{sss.main-and-redun}
6: Assume that the transition function $\trans_{k}$ and has bandwidth
7: $\bw =\bw_{k}$ as defined in ~\ref{sss.bandwidth}, and similary the
8: simulated transition function $\trans_{k+1}$ has bandwidth $\bw_{k+1}$.
9:
10: The state of each small cell is partitioned using
11: $\Buf=\Inbuf\cup \Outbuf$, etc.
12: Also, the field $\Info$ is partitioned into subfields
13: $\Info.\Main$\glo{info.main@$\Info.\Main, \Info.\Redun$} and
14: $\Info.\Redun$.
15: Each of the fields of a small cell mentioned in the construction of the
16: previous sections, with the exception of $\Info.\Main$, will be part of
17: $\Buf$.
18: Let%
19: \glo{p.cap@$P$}%
20: \[
21: P=\cp_{k+1}/\bw_{k+1}.
22: \]
23: Assume w.l.o.g.~ that this number is integer.
24: We partition the state of the represented cell into $P$ fields called
25: \df{packets}\index{packet} of size $\bw_{k+1}$.
26: We also break up the field $\Info.\Main$ into fields $\Info.\Main_{i}$,
27: $i=0,\ldots,P-1$ of equal size.
28: Assume without loss of generality that
29: \begin{equation}\label{e.bw-mon}
30: \frac{\cp_{k}}{\bw_{k}} \le \frac{\cp_{k+1}}{\bw_{k+1}}
31: \le 2 \frac{\cp_{k}}{\bw_{k}}.
32: \end{equation}
33: The first inequality implies that the width of track $\Info.\Main_{i}$ is
34: less than the bandwidth of a small cell.
35: The second inequality will be used in deriving ~\eqref{e.compute-time}.
36: (In case the first inequality was violated, we could distribute a packet
37: over several tracks whose width is the bandwidth, and otherwise the
38: algorithm would be similar.
39: In case the second inequality was violated, we could put several packets
40: onto each tracks whose width is the bandwidth, and otherwise the algorithm
41: would be similar.)
42:
43: Let us also break up the track $\Info.\Redun$ into locations (segments)
44: $\fld{-Info}.\Redun_{i}$, $i=0,1,\ldots, P-1$.
45: Our error-correcting code will distinguish, similarly to Example
46: ~\ref{x.no-stretch}, information symbols and error-check symbols.
47: Each packet of the represented state will be encoded separately.
48: Track $\Info.\Main_{i}$ will contain the information symbols, and
49: location $\fld{-Info}.\Redun_{i}$ contains the error-check bits of packet
50: $i$.
51: Let the location
52: \[
53: \fld{-Info}_{i}
54: \]
55: denote the union of track $\Info.\Main_{i}$ and location
56: $\fld{-Info.Redun}_{i}$.
57: These together form the error-correcting code of packet $i$.
58: The first three packets represent $\Inbuf^{*}$, $\Outbuf^{*}$ and
59: $\Pointer^{*}$.
60:
61: \begin{figure}
62: \setlength{\unitlength}{0.30mm}
63: \[
64: \begin{picture}(480,260)(40, 0)
65: \put(0, 0){\framebox(480, 260){}}
66:
67: \multiput(0,240)(0,-20){6}{\line(1,0){480}}
68: \put(490, 240){\makebox(0,20)[l]{$\var{Info.Main}_{0}$}}
69: \put(490, 220){\makebox(0,20)[l]{$\var{Info.Main}_{1}$}}
70: \put(520, 200){\makebox(0,20)[l]{$\vdots$}}
71: \put(490, 140){\makebox(0,20)[l]{$\var{Info.Main}_{P-1}$}}
72: \put(0,120){\line(1,0){480}}
73: \put(490, 120){\makebox(0,20)[l]{$\var{Info.Redun}$}}
74: \multiput(80,120)(80,0){5}{\line(0,1){20}}
75: \put(80, 120){\makebox(80,20){$\var{-Info.Redun}_{1}$}}
76:
77: \multiput(0,100)(0,-20){4}{\line(1,0){480}}
78: \put(490, 100){\makebox(0,20)[l]{$\var{Hold.Main}_{0}$}}
79: \put(520, 75){\makebox(0,20)[l]{$\vdots$}}
80: \put(490, 40){\makebox(0,20)[l]{$\var{Hold.Main}_{3}$}}
81: \put(0,20){\line(1,0){480}}
82: \put(490, 20){\makebox(0,20)[l]{$\var{Hold.Redun}$}}
83: \multiput(80,20)(80,0){5}{\line(0,1){20}}
84: \put(160, 20){\makebox(80,20){$\var{-Hold.Redun}_{2}$}}
85: \put(400, 20){\makebox(80,20){$\var{-Hold.Redun}_{n}$}}
86: \put(490, 0){\makebox(0,20)[l]{$\var{Target-addr} = n$}}
87:
88: \put(2, 222){\framebox(476,16){}}
89: \put(82, 122){\framebox(76,16){}}
90:
91: \end{picture}
92: \]
93: \caption[The $\protect\fld{Info}$ and $\protect\fld{Hold}$ tracks]{The
94: $\protect\fld{Info}$ and $\protect\fld{Hold}$ tracks] subdivided into
95: packets, with $P = 6$ and $n = 5$.
96: The location $\protect\fld{-Info}_{1}$ is the union of the framed
97: locations $\protect\fld{Info}.\protect\fld{Main}_{1}$ and
98: $\protect\fld{-Info}.\protect\fld{Redun}_{1}$.}
99: \label{f.cmp}
100: \end{figure}
101:
102: We will work with a 12-error-correcting code%
103: \glo{a.greek@$\ag$}%
104: \begin{equation}\label{e.err-corr-code-alpha}
105: \ag
106: \end{equation}
107: as in Example ~\ref{x.RS-code}, with $Q_{k}$ information symbols.
108: Since that code can correct errors in $t$ symbols with just $2t$
109: error-check symbols, so for each $i$, the location $\var{-Info}.\Redun_{i}$
110: is only 24 cells long.
111: When $\loc$ is a location representing a string $s$ then we will use the
112: notation
113: \[
114: \ag^{*}(\loc)=\ag^{*}(s)
115: \]
116: for the value decoded from it.
117:
118: The computation result will be stored temporarily on the track
119: $\Hold$\glo{hold@$\Hold$}.
120: This has, similarly to $\Info$, also subfields $\Main$ and $\Redun$.
121: This computation result corresponds to the output of
122: $\trans^{\bw_{k+1}}$.
123: Recall that the latter consists of 5 segments of size $\bw_{k+1}$.
124: The first three segments determine the new values of $\Inbuf^{*}$,
125: $\Outbuf^{*}$ and $\Pointer^{*}$.
126: The fourth segment determines the new value of a part of the cell state
127: whose position is determined by the fifth segment.
128: The output of the simulating computation, on the $\Hold$ track, will
129: correspond to the first four of these values, in four subfields.
130: The fifth one will be kept in a locally maintained field called
131: \[
132: \fld{Target-addr}
133: \]
134: which is supposed to have a constant value throughout the colony.
135: Track $\Hold.\Redun$ is split into locations $\fld{-Hold.Redun}_{i}$ for
136: $i=0,\ldots,P-1$, most of which will be unused.
137: For $i=0,1,2$ we define again $\fld{-Hold}_{i}$ as the union of the track
138: $\Hold.\Main_{i}$ and $\fld{-Hold.Redun}_{i}$, similarly to how
139: $\fld{-Info}_{i}$ was defined.
140: The redundancy bits for $\Hold.\Main_{3}$ will be put, however, not into
141: $\fld{-Hold.Redun}_{3}$ but into $\fld{-Hold.Redun}_{n}$ where
142: $n=\fld{Target-addr}$ (here, $n$ has the same meaning as in
143: ~\ref{sss.bandwidth}).
144: Correspondingly, we define
145: \[
146: \fld{-Hold}_{3} = \Hold.\Main_{3}\cup\fld{-Hold.Redun}_{n}.
147: \]
148:
149: \subsubsection{The code of the amplifier}\label{sss.amp-code}
150: Recall ~\eqref{e.crit}.
151: If $\fg^{*}(\eta)(y,t)\notin\Bad$ then let us define
152: \[
153: \eta^{*}(y,t)=\fg^{*}(y,t)=\Vac
154: \]
155: unless there is a time $v_{1}$ in
156: $[t-\cns{crit},t]$\glo{crit@$\cns{crit}$} such that the colony $\cC(y)$ is
157: covered with member cells belonging to the same work period at time $v_{1}$
158: and is not intersected by the extended damage rectangle at this time.
159: In case there is such a time $v_{1}$ let $t^{*}$ be the last time before
160: $t$ with this property that is also the switching time of a small cell
161: (just to make sure there is such a last time).
162: Let
163: \[
164: s=\eta(\cC(y),t^{*}).\Info
165: \]
166: (the meaning of this notation should be clear).
167: If $s$ contains at most 2 errors then (see ~\eqref{e.err-corr-code-alpha})
168: \[
169: \eta^{*}(y,t)=\ag^{*}(s),
170: \]
171: else it is $\Vac$.
172: The look-back to an earlier time in the definition avoids some
173: oscillation between the different states assigned to the large cell
174: that could occur as the result of damage and asynchronous updating.
175:
176: The encoding $\fg_{*}$ takes the state of a cell, applies $\ag_{*}$ and
177: copies the result to $\Info$ track of a colony.
178: The other parts of the colony are set in such a way as they are to be
179: found at the beginning of a work period.
180: The encoding $\fg_{**}$ is like $\fg_{*}$ except that all tracks but
181: $\Info$ will be filled with the don't care symbol $*$.
182:
183:
184: \subsubsection{Coding and decoding rules}
185: Let%
186: \glo{vacant-str@$\var{Vacant-str}$}%
187: \[
188: \var{Vacant-str}
189: \]
190: be a string representing a vacant state in our code.
191: Let %
192: \glo{code-size@$\var{Code-size}$}%
193: \begin{equation}\label{e.N}
194: \var{Code-size}(k) = \cei{\rep_{0}/\rep_{1}(k)} %?
195: \end{equation}
196: where $\rep_{0}$ and $\rep_{1}(k)$ were defined in ~\ref{sss.brc-fr} and
197: \ref{sss.amp-fr}.
198: Let $\rul{Decode-prog}$ %\glo{decode-prog@$\rul{Decode-prog}$}
199: be a program
200: for the medium $\univ$ such that location
201: $\fld{-Decode-output}$ %\glo{decode-output@$\fld{-Decode-output}$}
202: on track $\Cpt.\Output$ after applying
203: \[
204: \univ(\rul{Decode-prog}\cc S;Q,2Q)
205: \]
206: contains $\ag^{*}(S)$ (see ~\eqref{e.err-corr-code-alpha}) if
207: $\ag_{*}(\ag^{*}(S))$ differs from $S$ in at most 12 symbols: otherwise, it
208: contains $\var{Vacant-str}$.
209: The decoding rule takes a string from location $\loc_{1}$, decodes it and
210: copies the result to location $\loc_{2}$.
211: The rule $\Write$ was described in Subsection ~\ref{ss.simp-sim}.%
212: \glo{decode@$\Decode$}%
213: \begin{program}
214: rule $\Decode(\loc_{1},\loc_{2})$ \0{
215: \\ $\Cpt.\Input := *$;
216: \\ $\Write(\rul{Decode-prog}, \fld{-Prog})$
217: \\ $\Copy(0, \loc_{1}, \fld{-Decode-arg})$;
218: \\ \cmt{apply the rule $\univ$ $2Q$ times to $\Cpt$}
219: \\ $\Copy(0,\fld{-Decode-output}, \loc_{2})$;
220: \\ }
221: \end{program}
222: (Recall the assumption made in ~\ref{sss.effic-univ} that $\univ$ is
223: commutative, so we do not have to worry about the order of execution in
224: different cells.)
225: The rule%
226: \glo{encode@$\rul{Encode}$}%
227: \[
228: \rul{Encode}(\loc_{1},\loc_{2})
229: \]
230: performs encoding.
231: The locations $\loc_{i}$\glo{loc@$\loc_{i}$} in the encoding and decoding
232: rules will be allowed to be given indirectly, as explained in Remark
233: ~\ref{r.indirect-copy}.
234:
235:
236: \subsection{Refreshing} \label{ss.refresh}
237:
238: In each rule of the present section, the operation%
239: \glo{maj@$\Maj$}%
240: \[
241: \Maj_{i = 0}^{2}s_{j}
242: \]
243: when applied to strings $s_{0},s_{1},s_{2}$ is the result of taking the
244: bitwise majority of these three strings.
245:
246: We will have a general type of rule%
247: \glo{check0@$\rul{Check}_{0}, \rul{Check}_{1}$}%
248: \[
249: \rul{Check}_{0}(\prg{prop},\F(I),X_{1},X_{2},\ldots)
250: \]
251: checking some global property of some parameters $X_{1},X_{2},\ldots$ each of
252: which is either an explicit string or a location.
253: Here, $\var{prop}$ is some program for the universal computing medium
254: such that after we run the rule of that medium for $Q$ steps the bit $b$
255: representing the outcome of the check will be broadcast into field $\F$ of
256: every cell of interval $I$.
257: We will also need an error-checked version of $\rul{Check}_{0}$ which uses
258: some fields $\Vote_{i}$\glo{vote@$\Vote_{i}$} for $i=0,2,3$:%
259: \begin{program}
260: rule $\rul{Check}_{1}(\prg{prop},\F(I),X_{1},X_{2},\ldots)$ \0{
261: \\ for $i\in\{0,1,2\}$ do \0{
262: \\ $\rul{Check}_{0}(\prg{prop}, \Vote_{i}(I), X_{1}, X_{2}, \ldots)$
263: }
264: \proglb{pg.check1.middle}
265: \\ cond \0{
266: \\ ? $\Addr\in I$
267: \\ ! $\F := \Maj_{i=0}^{2}\Vote_{i}$
268: \\ }}
269: \end{program}
270: The rule%
271: \glo{nearly-equal@$\prg{nearly-equal}$}%
272: \[
273: \rul{Check}_{0}(\prg{nearly-equal},\F(I),\loc_{1},\loc_{2}, d)
274: \]
275: checks whether the strings in locations $\loc_{1}$ and $\loc_{2}$ differ
276: in at most $d$ code symbols.
277: The subrule $\Refresh$\glo{refresh@$\Refresh$} attempts to clean the
278: information on the $\Info$ and $\Hold$ tracks by decoding and re-encoding
279: it.
280: It also attempts to make sure that these tracks represent at least
281: something, even if this is only the vacant state.
282:
283: Rule
284: $\rul{Update-loc-maint}$\glo{update-loc-maint@$\rul{Update-loc-maint}$}
285: updates the locally maintained fields
286: \[
287: \Doomed, \Growing_{j}\ (j\in\{-1,1\}).
288: \]
289: (It need not update the fields
290: $\Control_{0.1j}$\glo{control@$\Control_{k}$} to be introduced later.)
291: Rule%
292: \glo{recheck-1@$\prg{recheck-1}$}%
293: \begin{equation}\label{e.recheck-1}
294: \rul{Check}_{0}(\prg{recheck-1}, \F(I), \G, d)
295: \end{equation}
296: checks whether track $\G$ is covered with 1's with possibly $d$ cells as
297: exceptions.
298: As usual, the argument $\F$ means $\F([0,Q-1])$.
299: The rule uses some additional locations and fields:
300: $\fld{-Decoded}_{0}$ %\glo{decoded@$\fld{-Decoded}_{m}$},
301: $\fld{-Encoded}_{n}$\glo{encoded@$\fld{-Encoded}_{n}$} for $n=0,1,2$,
302: $\fld{Ck-res}_{n}$\glo{ck-res@$\fld{Ck-res}_{n}$} for $n=0,1,2$.
303: \begin{program}
304: subrule $\Refresh$ \0{
305: \\ $\fld{Ck-res} := 1$;
306: \\ for $i=0$ to $P-1$ do \0{
307: \\ for $n=0$ to $2$ do \0{
308: \\ $\Decode(\fld{-Info}_{i}, \fld{-Decoded}_{0})$;
309: \\ $\rul{Encode}(\fld{-Decoded}_{0}, \fld{-Encoded}_{n})$;
310: \\ $\rul{Check}_{0}(\prg{nearly-equal}, \fld{Ck-res}_{n},
311: \fld{-Encoded}_{n},\fld{-Info}_{i}, 8)$;
312: \\ \cmt{Idle $Q$ steps}
313: }
314: \\ $\fld{-Encoded}:=\Maj_{n=0}^{2} \fld{-Encoded}_{n}$;
315: \\ $\fld{Ck-res}:=\fld{Ck-res}\wedge\Maj_{n=0}^{2}\fld{Ck-res}_{n}$;
316: \\ $\Copy(\fld{-Encoded}, \fld{-Info}_{i})$;
317: \\ \cmt{Idle $Q$ steps}
318: }
319: \\ $\rul{Check}_{1}(\prg{recheck-1}, \fld{Ck-res}, \fld{Ck-res}, 2)$;
320: \proglb{pg.refresh.middle}
321: \\ cond \0{
322: \\ ? $\fld{Ck-res}=0$
323: \\ ! $\Write(\var{Vacant-str}, \fld{-Info})$
324: }
325: \\ \cmt{Repeat the whole procedure with $\fld{-Hold}$ in place of
326: $\fld{-Info}$, ``mutatus mutandis''.}
327: \\ }
328: \end{program}
329:
330: Let us say that a string $s$ of symbols that can be the argument of a
331: certain error-correcting decoding \df{has $d$ errors}\index{error} if,
332: when applying the decoding and encoding to it, the result differs from $s$
333: in $d$ symbols.
334:
335: \begin{lemma}[Refresh]\label{l.refresh}\index{lemma@Lemma!Refresh}
336: Assume that we have a full colony in which all cells have ages before the
337: starting point of $\Refresh$.
338: Then we have:
339: \begin{cjenum}
340:
341: \item \label{refresh.valid-or-die}
342: At the end of $\Refresh$, for all $i$, locations $\fld{-Info}_{i}$, have
343: at most 4 errors;
344:
345: \item \label{refresh.refresh}
346: Suppose that at the beginning of $\Refresh$, for all $i$, locations
347: $\fld{-Info}_{i}$, have at most 4 errors.
348: Then during the whole $\Refresh$, the value $\ag^{*}(\fld{-Info}_{i})$
349: does not change and $\fld{-Info}_{i}$ has at most 8 errors.
350:
351: \end{cjenum}
352: The same statements hold for location $\fld{-Hold}$.
353: \end{lemma}
354: \begin{Proof}
355: We perform the analysis only for $\fld{-Info}$.
356: \begin{step+}{refresh.immed-dam}
357: For any $i$, the ``immediate'' effect of the damage can affect at most
358: 4 symbols of $\fld{-Info}_{i}$.
359: \end{step+}
360: \begin{pproof}
361: The damage rectangle can have immediate effect in the cell where it
362: happens, and its healing can change possibly one more cell next to it.
363: If the affected cells happens to contain the symbols from
364: $\fld{-Redun}_{i}$ then this can affect two information symbols and two
365: error-check symbols.
366: \end{pproof}
367: \begin{step+}{refresh.early-dam}
368: Assume that the damage rectangle occurs before point
369: ~\eqref{pg.refresh.middle} of the rule.
370: \end{step+}
371: \begin{prooof}
372: Let us look at the damage-free operations in $\rul{Check}_{1}$ after
373: ~\eqref{pg.refresh.middle}.
374: The first such operation turns $\fld{Ck-res}$ into all 0 or all 1.
375: If $\fld{Ck-res}=0$ then the last step writes $\var{Vacant-str}$ into
376: $\fld{-Info}$, and thus the latter will have no errors.
377:
378: Suppose therefore that if $\fld{Ck-res}=1$.
379: Then before $\rul{Check}_{1}$, we have $\fld{Ck-res}=1$ in all but two cells.
380: Let us look at any cell $x$ not affected immediately by damage (the large
381: majority is such).
382: Since the majority step computing $\fld{Ck-res}$ is correct in $x$, for
383: all $i$ there must have been two values of $n$ for which $\rul{Check}_{0}$
384: wrote the value 1 into $\fld{Ck-res}_{n}(x)$.
385: For at least one of these $n$, say $n_{1}$, the computing
386: period\index{period!computing} $(i,n_{1})$ is damage-free.
387: That period wrote an error-free string into $\fld{-Encoded}_{n_{1}}$, and
388: also determined that this string does not differ from $\fld{-Info}_{i}$ by
389: more than 8 symbols.
390: There is another damage-free period\index{period!damage-free} $(i,n_{2})$.
391: Its $\fld{-Info}_{i}$ could have been different at its beginning
392: (if damage occurred between the two periods), though according to
393: ~\ref{refresh.immed-dam} by not more than 4 symbols.
394: Therefore, since our code corrects 12 errors, we have
395: $\fld{-Encoded}_{n_{1}} = \fld{-Encoded}_{n_{2}}$.
396: Except for the immediate effect of new damage, this is going to be the
397: new value of $\fld{-Info}_{i}$, therefore there can be at most these 4 new
398: errors at the end of $\Refresh$.
399:
400: Suppose that at the beginning, each $\fld{-Info}_{i}$ has at most 4
401: errors.
402: By ~\ref{refresh.immed-dam}, the damage rectangle affects at most 4 cells
403: of $\fld{-Info}_{i}$ immediately.
404: Therefore during the whole $\Refresh$, the value
405: $\ag^{*}(\fld{-Info}_{i})$ does not change and $\fld{-Info}_{i}$ has at
406: most 8 errors.
407: \end{prooof}
408:
409: \begin{step+}{refresh.middle-dam}
410: Assume that the damage rectangle occurs on line
411: ~\eqref{pg.refresh.middle}.
412: \end{step+}
413: \begin{prooof}
414: Then the damage did not occur before and therefore the track
415: $\fld{Check-res}$ contains either all 0's or all 1's.
416:
417: Suppose the damage has occurred before line ~\eqref{pg.check1.middle} of
418: rule $\rul{Check}_{1}$, in iteration $n$ of that rule.
419: Then only $\Vote_{n}(I)$ will be affected, and possibly two
420: more cells, the cell where the damage occurred and a cell next to it due to
421: healing.
422: In the 2 other iterations, the track $\fld{Check-res}$ still contains
423: either all 0's or all 1's with these exceptions, and the result of these 2
424: iterations is the same as it was without the damage in the third iteration.
425: The majority vote brings out the same result, except for possibly 2
426: immediately affected cells.
427: \end{prooof}%
428:
429: If the damage occurs after line ~\eqref{pg.check1.middle}, in rule
430: $\rul{Check}_{1}$, i.e.~in the last step of the rule, then again only the cells
431: immediately affected will not have the correct result.
432:
433: If the damage occurs after line~\eqref{pg.refresh.middle} in rule
434: $\Refresh$ then again, this being a one-step action, only the cells
435: immediately affected by the damage would show up as errors.
436: \end{Proof} % {refresh}
437:
438:
439: \subsection{Computation rules}\label{ss.comp}
440:
441: After retrieval from neighbor colonies (to be discussed later), the
442: string returned from neighbor $m$ will be in some location%
443: \glo{retrieved@$\fld{-Retrieved}_{m}$}%
444: \[
445: \fld{-Retrieved}_{m}.
446: \]
447: These strings are inputs to the simulated transition function but still
448: in encoded form.
449: After decoding, the result will appear in
450: $\fld{-Decoded}_{m}$ %\glo{decoded@$\fld{-Decoded}_{m}$}.
451:
452: \subsubsection{Evaluation}\label{sss.eval}
453: As seen in ~\eqref{e.trans-b-in}, only the field $\Buf^{*}$ of the
454: neighbors is found in $\fld{-Retrieved}_{m}$ for $m \ne 0$.
455: For $m = 0$, the location $\fld{-Info}_{\a}$ is also needed, where $\a$
456: is determined by $\Pointer^{*}$, which according to
457: ~\ref{sss.main-and-redun} is found in $\fld{-Info}_{2}$.
458: Thus, first we broadcast this number $\a$ into a locally maintained field%
459: \glo{source-addr@$\fld{Source-addr}$}%
460: \[
461: \fld{Source-addr}
462: \]
463: of each cell of the colony, and then use indirect copying as in Remark
464: ~\ref{r.indirect-copy} to copy $\fld{-Info}_{\a}$ into the appropriate part
465: of $\fld{-Retrieved}_{0}$.
466:
467: Then, the subrule $\Eval$\glo{eval@$\Eval$} finds the intended output of
468: $\trans_{k+1}^{(\bw)}$, as defined in ~\ref{sss.bandwidth}, using the
469: universal computation, as in $\Decode$ above.
470: Here are the details.
471:
472: We are proving Lemma ~\ref{l.amp} (Amplifier), so what is given is an
473: amplifier frame $\Frame$, and the number $k$, and we are building the
474: transition function of the medium $M_{k}$.
475: Assume that $\Frame$ is described in a string
476: \[
477: \Param_{2} = \Frame,
478: \]
479: the parameter $k$ is described in a string
480: \[
481: \Param_{1} = k,
482: \]
483: and the program we are just writing is $\Param_{0}$.
484: First $\Eval$ computes $\trans_{k+1}^{(\bw)}$.
485: It uses several new locations, some of which were introduced in
486: ~\ref{sss.block-sim-eval}:
487: $\fld{-Interpr}$\glo{interpr@$\fld{-Interpr}$},
488: $\fld{-Param}_{i}$\glo{param@$\fld{-Param}_{i}$} for $\Param_{i}$,
489: $\fld{-Arg}_{m}$\glo{arg@$\fld{-Arg}_{m}$}.
490: The result will be deposited in
491: $\fld{-Sim-output}_{i}$\glo{sim-output@$\fld{-Sim-output}_{i}$} for
492: $i=1,2$.
493: \begin{program}
494: $\Cpt.\Input := *$;
495: $\Write(\rul{Interpr}, \fld{-Interpr})$;
496: \\ $\Write(\Param_{0}, \fld{-Param}_{0})$;
497: \\ $\Write(\Param_{1} + 1, \fld{-Param}_{1})$;
498: \\ $\Write(\Param_{2}, \fld{-Param}_{2})$;
499: \\ for $m\in\Nb-ind$ do \0{
500: \\ $Copy(0,\fld{-Decoded}_{m}, \fld{-Arg}_{m})$
501: }
502: \\ \cmt{apply $Q$ times the rule $\univ$ to $\Cpt$}
503: \\ \cmt{The result is in $\fld{-Sim-output}_{1}$.}
504: \\ $\Copy(0,\fld{-Sim-output}_{1}, \fld{-Sim-output}_{2})$
505: \end{program}
506: As seen in ~\eqref{e.trans-b-legal}, in the output string of
507: $\trans^{(\bw)}_{{k+1}}$, only the first segment of size $\bw_{k+1}$
508: (corresponding to field $\Inbuf^{*}$) depends on the neighbors.
509: To make sure that really this is the case, the above sequence of
510: operations will in fact be performed twice, with the following differences.
511: \begin{itemize}
512:
513: \item The first time, for all $m \ne 0$, the string written in
514: $\fld{-Arg}_{m}$ will not be a copy of $\fld{-Retrieved}_{m}$ but simply
515: the corresponding part of $\var{Vacant-str}$.
516: Thus, the result does not depend on retrieval from neighbor colonies;
517:
518: \item The second time, only field $\Inbuf^{*}$ of $\fld{-Sim-output}_{1}$
519: will be copied into the appropriate part of $\fld{-Sim-output}_{2}$;
520:
521: \end{itemize}
522: According to ~\ref{sss.combined}, the complete transition function is
523: combined from $\var{Sim-trans}$ and $\var{Rd-trans}$.
524: To make sure this is the case, we recompute $\var{Rd-trans}_{k+1}$ and
525: perform the combination.
526: Thus, now the rule $\Eval$ finds out from $\fld{-Sim-output}_{2}$ whether
527: the new big cell is going to be vacant.
528: If not then $\var{Rd-trans}_{k+1}$ is computed somewhat similarly to
529: $\var{Sim-trans}_{k+1}$ above.
530: The main difference is in what we copy into $\Param_{0}$.
531: According to the complexity upper bounds in Subsection ~\ref{ss.frame},
532: the sequence $\var{Rd-trans}_{i}$ of functions is uniformly simple.
533: Therefore $\Frame$ contains a program $\prg{Rd-trans-prog}$ computing
534: $\var{Rd-trans}_{k+1}$ on the universal medium $\univ$ from $k+1$ and its
535: arguments in time $\rep_{0}\nm{\SS_{k+1}}$ and space
536: $\rep_{0}\nm{\SS_{k+1}}$.
537: We will therefore copy $\prg{Rd-trans-prog}$ into $\fld{-Param}_{0}$.
538: The result will be stored in $\fld{-Rd-output}_{2}$.
539:
540: Finally, we combine $\fld{-Sim-output}_{2}$ and $\fld{-Rd-output}_{2}$ as
541: required in ~\ref{sss.combined}, into a location $\fld{-Eval-output}$.
542: In accordance with ~\eqref{e.trans-b-out}, this location can be broken up
543: into segments $\fld{-Eval-output}_{i}$ for $i=0,1,2,3,4$, of size
544: $\bw_{k+1}$.
545: Locations $\fld{-Eval-output}_{i}$ for $i=0,1,2$ are supposed to be the
546: first three packets of the new big cell state.
547: $\fld{-Eval-output}_{3}$ is also supposed to be the new value, to replace
548: some packet $\Info.\Main_{\n}$ of the new cell state, where
549: $\n = \fld{-Eval-output}_{4}$.
550: To use this information, the number $\n$ will be broadcast into a field
551: $\fld{Target-addr}$ of each cell.
552:
553: \begin{remark}
554: It seems wasteful to compute $\var{Rd-trans}_{k+1}$ twice: once as part
555: of $\trans_{k+1}$ and once separately.
556: To avoid this, in the first computation we can replace
557: $\prg{Rd-trans-prog}$ with a trivial program that does not do anything.
558: \end{remark}
559:
560: This ends the definition of the rule $\Eval$.
561:
562:
563: \subsubsection{The computation rule}
564: In the rule $\Compute$, the evaluation process will be repeated 3 times:
565: in repetition $n$, we code $\fld{-Eval-output}$ onto track
566: $\fld{Hold-vote}_{n}$, and finally $\Hold$ will be obtained by majority
567: vote from $\fld{Hold-vote}_{n}$ ($n=0,1,2$).
568:
569: In the rule $\rul{Randomize}$, the $\Rand$ bit of the first cell of the
570: colony is taken and an $\ag_{*}$-code of it is placed into the appropriate
571: location on the $\Hold$ track.
572: This is done only once, without any attempt of error-correction.
573:
574: Rule $\rul{Update-loc-maint}$ will be discussed below.%
575: \glo{compute@$\Compute$}%
576: \begin{program}
577: subrule $\Compute$ \0{
578: \\ $\Refresh$;
579: \\ for $n=0$ to $2$ do \0{
580: \\ for $m\in\Nb-ind$ do \0{
581: \\ $\Decode(\fld{-Retrieved}_{m}, \fld{-Decoded}_{m})$;
582: }
583: \\ $\Eval$;
584: \\ for $i=0,1,2,3$ do \0{
585: \\ $\rul{Encode}(\fld{-Eval-output}_{i}, \fld{-Hold}_{i})$;
586: \\ \cmt{For $i=3$, use indirect copying with
587: $\fld{Target-addr} = \fld{-Eval-output}_{4}$.}
588: }
589: \\ $\fld{Hold-vote}_{n}=\Hold$;
590: \\ $\fld{Target-addr}_{n} := \fld{Target-addr}$;
591: }
592: \\ $\Hold := \Maj_{n=0}^{2}\fld{Hold-vote}_{n}$;
593: \\ $\fld{Target-addr} := \Maj_{n=1}^{3}\fld{Target-addr}_{n}$;
594: \\ $\rul{Randomize}$;
595: \\ $\Refresh$;
596: \\ $\rul{Update-loc-maint}$
597: \\ }
598: \end{program}
599:
600:
601: \subsection{Finishing the work period}\label{sss.finish}
602:
603: The present subsection is devoted to achieving good upper and lower
604: bounds on the length of the colony work period, i.e.~ on $\Tu_{k+1}$ and
605: $\Tl_{k+1}$ in terms of $\Tu_{k}$ and $\Tl_{k}$.
606: Though it seems likely that these bounds can be proven if each cell of
607: the colony simply runs until the same maximum age $U_{k} - 1$, we did not
608: find such a proof.
609: Therefore we introduce some special rules.
610:
611: The $\rul{March}$ rule updates the age of a cell only when its neighbors
612: allow it, and this is what makes the time estimates difficult.
613: We will therefore define a different rule,
614: $\rul{March}_{1}$\glo{march@$\rul{March}_{1}$}, which allows updating a
615: different field, $\Age_{1}$,\glo{age@$\Age_{1}$} independently of any
616: neighbors.
617: The idea is to end the work period when a certain cell reaches
618: $\Age_{1}=U$, since then the (multiplicative) uncertainty in the length of
619: the colony work period will not be much greater than the uncertainty in the
620: length of the individual cell dwell period.
621: We will use the $\Age_{1}$ of more than one cell, for robustness, but
622: then we will need to reach a consensus among these about when the end
623: comes.
624: To leave clearly enough time for the consensus computation, and to make
625: sure the work period ends in a coordinated way, what will be determined by
626: consensus is some future value $\End$ of $\Age$ when the work period will
627: end.
628:
629:
630: \subsubsection{Finding the work period end}
631: We will also use the auxiliary field%
632: \glo{end@$\End_{i}$}%
633: \[
634: \End_{0} \in [0,U-1].
635: \]
636: At the beginning of the work period, we start with $\Age_{1}=0$,
637: $\End=\End_{0}=U-1$.
638: (These values are extremely large for $\End,\End_{0}$.)
639: Recall the definition of
640: $\cns{end-period}$\glo{end-period@$\cns{end-period}$} in
641: ~\eqref{e.end-period}.
642: The field $\End_{0}$ is required to have the property
643: \begin{equation}\label{e.End_{0}}
644: \End_{0}=U-1 \text{ or } \End_{0}\le\Age+\cns{end-period}
645: \end{equation}
646: which will be enforced by a trivial rule.
647: The update rule of $\Age_{1}$ is trivial.
648: \begin{program}
649: rule $\rul{March}_{1}$ \0{
650: \\ cond \0{
651: \\ ? $\Age_{1} < U-1$
652: \\ ! $\Age_{1} :=_{\p_{0}} \Age_{1}+\p_{0}$
653: \\ ?! cond \0{
654: \\ ? $\End_{0}=U-1$
655: \\ ! $\End_{0} :=_{\p_{0}} (U-1)\wedge(\Age+\cns{end-period})$
656: \\ }}}
657: \end{program}
658: Thus, each cell updates its $\Age_{1}$ independently of all other cells,
659: and the delays are also counted in.
660: When the upper bound $U-1$ of $\Age_{1}$ is reached each cell puts its
661: estimate of the end of the work period into $\End_{0}$.
662: The subrule $\rul{Find-end}$\glo{find-end@$\rul{Find-end}$} will last at
663: most%
664: \glo{synch-time@$\cns{synch-time}$}%
665: \begin{equation}\label{e.synch-time}
666: \cns{synch-time} = 16Q
667: \end{equation}
668: steps and will be run every $4\cns{synch-time}$ steps after
669: $\Age>\cns{synch-start-lb}$\glo{synch-start-lb@$\cns{synch-start-lb}$} (see
670: ~\eqref{e.synch-start-lb-req}).
671: It uses votes $\End_{i}\in[0,U-1]$ %\glo{end@$\End_{i}$}
672: ($i=1,2,3,4$) to achieve consensus of the $\End_{0}$ values and to store
673: it in $\End$.
674: The subrule%
675: \glo{synch-consensus@$\prg{synch-consensus}$}%
676: \glo{end-legal@$\fld{End-legal}$}%
677: \[
678: \rul{Check}_{0}(\prg{synch-consensus}, \fld{End-legal}, \End_{4})
679: \]
680: checks whether there is a $c$ such that $\End_{4}(x)=c$ for all but 3 of
681: the cells $x$ in the colony.
682:
683: \begin{program}
684: subrule $\rul{Find-end}$ \0{
685: \\ for $i\in\{1,2,3\}$ do \0{
686: \\ cond \0{
687: \\ ? \cmt{There is a $c<U-1$ such that $\End=c$}
688: \proglb{pg.synch.late}
689: \\ \cmt{for all but 2 cells in the colony}
690: \\ ! $\End_{i}:=_{\p_{1}} c$
691: \\ ? \cmt{All but $Q/4$ cells have $\End_{0}<U-1$}
692: \proglb{pg.synch.early}
693: \\ ! $\End_{i}:=_{\p_{1}}$ \cmt{the maximum of the $Q/2$
694: smallest values}
695: \\ \cmt{of $\End_{0}$ in the colony.};
696: }
697: };
698: \\ cond \0{
699: \\ ? \cmt{There are two equal values among}
700: $\setof{\End_{i}: i\in\{1,2,3\}}$
701: \\ ! $\End_{4} :=_{\p_{1}} \Maj_{i=1}^{3}\End_{i}$
702: };
703: \\ $\rul{Check}_{1}(\prg{synch-consensus}, \fld{End-legal}, \End_{4})$
704: \\ cond \0{
705: \\ ? $\fld{End-legal}=1$
706: \\ ! $\End:=\End_{4}$
707: \\ }}
708: \end{program}
709:
710:
711: \subsubsection{Finish}
712: At $\Age=\End$ for non-germ cells and
713: $\Age=\cns{germ-end}$\glo{germ-end@$\cns{germ-end}$} for germ cells, a
714: final computation takes place in the rule
715: $\rul{Finish}$\glo{finish@$\rul{finish}$}.
716: The information from the $\Hold$ track will be copied into the
717: corresponding locations on the $\Info$ track.
718: This is done in accordance with ~\eqref{e.trans-b-out}:
719: locations $\fld{-Hold}_{i}$ for $i=0,1,2$ go to $\fld{-Info}_{i}$.
720: On the other hand, location $\fld{-Hold}_{3}$ goes to $\fld{-Info}_{\n}$
721: where $\n = \fld{Target-addr}$.
722: Still, due to the positioning done earlier, the whole operation involves
723: only copying within each cell and takes therefore only a single step.
724: In particular, $\Outbuf^{*}$ remains unchanged until the last step.
725:
726: In the same step, addresses of growth cells will be reduced mod $Q$.
727: Outer cells and inner germ cells turn into members, outer germ cells turn
728: latent.
729: $\End,\End_{0},\Age,\Age_{1}$ become 0.
730:
731:
732: \subsubsection{Updating the locally maintained fields}
733: The rule
734: \[
735: \Broadcast(\loc, \F(I))
736: \]
737: takes the information found in location $\loc$ and writes it into the
738: $\F$ field of every cell in interval $I$.
739: The rule
740: \glo{check-vacant@$\rul{Check-vacant}$}
741: $\rul{Check}_{0}(\rul{Check-vacant}, \F(I), \loc)$
742: checks whether the string represented in $\loc$ is $\Vac^{*}$.
743: Let $\fld{-Creating}_{j}$\glo{creating@$\fld{-Creating}_{j}$} be the
744: known location of the field $\Creating_{j}^{*}$ of the represented cell
745: inside $\fld{-Decoded}_{0}$ after decoding.
746: The value in this represented field will be broadcast reliably to the
747: track $\Growing_{j}$\glo{growing@$\Growing_{j}$}.%
748: \glo{update-loc-maint@$\rul{Update-loc-maint}$}%
749: \begin{program}
750: rule $\rul{Update-loc-maint}$ \0{
751: \\ for $n=0$ to 2 do \0{
752: \\ $\Decode(\fld{-Hold}, \fld{-Decoded}_{0})$;
753: \\ $\rul{Check}_{0}(\rul{Check-vacant}, \Vote_{n}, \fld{-Decoded}_{0})$
754: }
755: \\ $\Doomed := \Maj_{n=0}^{2}\Vote_{n}$
756: \\ for $j\in\{-1,1\}$ do \0{
757: \\ for $n=0$ to 2 do \0{
758: \\ $\Decode(\fld{-Info}, \fld{-Decoded}_{0})$;
759: \\ $\Broadcast(\fld{-Creating}_{j}, \Vote_{n})$;
760: }
761: \\ $\Growing_{j} := \Maj_{n=0}^{2}\Vote_{n}$
762: \\ }}
763: \end{program}
764:
765: \begin{remark}
766: Defining the rules this way wastes many operations since we do not
767: extract all information from its decoded form at once but rather decode
768: repeatedly.
769: But it is easier to follow the analysis in this form.
770: \end{remark}
771:
772: \begin{lemma}\label{l.update-loc-maint}
773: Assume that we have a full colony in which all cells have ages before
774: a starting point of $\rul{Update-loc-maint}$.
775: Then at the end of this rule we have the same conditions as at the end of
776: $\Refresh$, and in addition the following:
777: \begin{cjenum}
778:
779: \item For all but at most 2 cells, the locally maintained fields
780: $\Doomed$ and $\Growing_{j}$ have constant values in the colony;
781:
782: \item We have $\Doomed=1$ almost everywhere if{f} $\fld{-Hold}$ represents
783: a vacant state;
784:
785: \item For $j\in\{-1,1\}$, for almost all cells in the colony,
786: $\Growing_{j}$ is equal to $\Creating_{j}^{*}$ of the cell state
787: represented by the colony;
788:
789: \end{cjenum}
790: \end{lemma}
791:
792: \begin{proof}
793: The proof is similar to, only simpler than the proof of Lemma
794: ~\ref{l.refresh}: simpler, since at the starting point of
795: $\rul{Update-loc-maint}$, we can already assume that the conditions asserted
796: by that lemma hold.
797: \end{proof}
798:
799: By choosing $Q$ sufficiently large ($\rep_{0}$ times the bandwidth), the
800: time complexity of each of the $\univ$ computations can be bounded by some
801: constant times $Q$ and therefore the total number of steps taken by
802: $\Compute$ can be estimated as%
803: \glo{compute-time@$\cns{compute-time}$}%
804: \begin{equation}\label{e.compute-time}
805: K_{0} Q P = K_{0} Q\frac{\cp_{k+1}}{\bw_{k+1}}
806: \le 2K_{0} Q\frac{\cp_{k}}{\bw_{k}}
807: \end{equation}
808: where $K_{0}$ is some absolute constant, which is consistent with
809: ~\eqref{e.compute-time-def}.
810:
811:
812: \subsection{Legality}
813:
814: Let us prove parts ~\eqref{ax.comput.legal-comp} and
815: ~\eqref{ax.comput.legal-birth} of Condition ~\ref{ax.comput} (Computation
816: Property) for big cells.
817:
818: \begin{lemma}[Legality]\label{l.legality}
819: Assume that, for some rational number $a$, $\Damage^{*}$ does not
820: intersect $\{x\}\times[a-\Tl^{*}/2+,a+2\Tu^{*}]$.
821: \begin{cjenum}
822: \item\label{comp.legal-compi}
823: If $\sg_{1},\sg_{2}$ is defined in the interval $[a+,a+2\Tu^{*}]$
824: Then
825: \begin{equation}\label{e.legality}
826: \legal_{k+1}(\eta^{*}(x, \sg_{2}-), \eta^{*}(x, \sg_{2})) = 1
827: \end{equation}
828: and $\Tl^{*} \le \sg_{2} - \sg_{1} \le \Tu^{*}$.
829: \item\label{comp.legal-birth}
830: If $\sg_{0}$ is defined then \eqref{e.legality} holds for $\sg_{0}$ in
831: place of $\sg_{2}$.
832: \end{cjenum}
833: \end{lemma}
834: \begin{Proof}
835: The discussion in Subsection ~\ref{ss.damage-rect} has shown that
836: $\eta^{*}(x,t)\not\in\Damage^{*}$ iff the damage can be covered by a single
837: damage rectangle in $(x,t)+V'$ where $V'$ is defined in~\eqref{e.V'}.
838: The space projection of $V'$ is at least $1.5QB$ and the time projection
839: is at least $\Tl^{*}/2$.
840: Thus, our assumption implies that during every time interval of size
841: $\Tl^{*}/2$ in $[a-\Tl^{*}/2, a+2\Tu^{*}]$, the interval
842: $[x-0.25QB, x+1.25QB]$ is intersected by at most one damage rectangle.
843:
844: Consider a time $v_{2}$ such that $\eta^{*}(x,v_{2})\ne\Vac$.
845: If $\sg_{0}$ is defined then let $v_{2}=\sg_{0}$, while if $\sg_{2}$ is
846: defined then let it be some time very close from below to $\sg_{2}$.
847:
848: According to ~\ref{sss.amp-code}, there is a time $v_{1}$ in
849: $[v_{2}-\cns{crit},v_{2}]$ such that the colony $\cC$ is covered with
850: member cells belonging to the same work period at time $v_{1}$ and is not
851: intersected by the extended damage rectangle at this time.
852: Lemma ~\ref{l.lg-progress} (Large Progress) says that, by setting
853: $u_{1}=v_{1}$, there is a time $u_{0} \in [u_{1}-5Q\tau_{1}, u_{1}]$, and a
854: path $P_{1}$ in $\cC\times[u_{0},u_{1}]$ with $d_{i}=(P_{1}(u_{i}),u_{i})$
855: within distance $B$ of the center of $\cC$ such that $\cC\times\{u_{0}\}$
856: is not in the wake of a damage rectangle, is covered by a domain, and
857: $Q\le \Age(d_{1})-\Age(d_{0})$.
858: If $d_{0}$ is a member cell let us apply the Large Progress Lemma
859: (backward) repeatedly until either the path crosses a work period boundary,
860: or the age along the path decreases by
861: \[
862: L=6\cns{synch-time}+\cns{end-period}.
863: \]
864: Suppose the cell we arrived at is not a member cell and has
865: $\Age\ge\End-Q$.
866: Then we perform one more repetition, but stop along the path as soon as
867: the age decreases below $\End-Q$.
868: Lemma ~\ref{l.cover-ancestor} (Cover Ancestor) shows that we can stop at
869: a time when the colony is covered by a domain.
870: Let us now denote by $d_{0}=(y_{0},u_{0})$ the cell at which we arrive
871: this way.
872:
873: \begin{step+}{legality.vacant}
874: Assume that $d_{0}$ is an outer cell.
875: \end{step+}
876: \begin{prooof}
877: Then we have
878: \begin{equation}\label{e.legality.vacant.short-time}
879: \Age(d_{1}) - \Age(d_{0}) \le L + Q
880: \end{equation}
881: and at time $u_{0}$, the whole colony is covered by outer cells.
882: Lemma ~\ref{l.attrib} (Attribution) shows that $d_{0}$ can be attributed
883: to its own colony and that this colony could not have been occupied by
884: member cells for at least $\cns{crit}$ time units before $u_{0}$.
885: Therefore $\eta^{*}(x,u_{0})=\Vac$.
886:
887: In this case we have $v_{2} = \sg_{0}$.
888: The outer cells at time $u_{0}$ encode a latent cell of medium
889: $M^{*}$.
890: Therefore eventually, when all outer cells turn into member cells, the
891: new colony will encode a latent cell.
892: Now, a vacant-to-latent transition is legal by Condition
893: ~\ref{cond.vac-to-lat}.
894: \end{prooof}%{legality.vacant}
895:
896: The reasoning is analogous in case $d_{0}$ is a germ cell.
897: Assume now that $d_{0}$ is a member cell in the same work period as
898: $c_{1}$: then $\Age(d_{1})-\Age(d_{0}) \ge L$.
899: Then we have the case when $\sg_{1},\sg_{2}$ are defined.
900:
901: \begin{step+}{legality.synch}
902: The Large Progress Lemma can extend the path repeatedly until we arrive
903: at a cell $c_{0}=(x_{0},v_{0})$ in the same work period, with
904: \begin{equation}\label{e.legality.synch}
905: \begin{aligned}
906: v_{0} &> \sg_{1},
907: \\ \Age(c_{0}) &\le 2Q,
908: \\ v_{1}-v_{0} &\le U\Tu + 5\tau_{1}L.
909: \end{aligned}
910: \end{equation}
911: \end{step+}
912: \begin{pproof}
913: One can find a time $t_{1}$ in $[u_{0},v_{1}]$ such that denoting
914: $\e_{1}=(P_{1}(t_{1}),t_{1})$\glo{e@$\e_{1}$} we have
915: \[
916: \Age(\e_{1})\le \Age(d_{0})+6\cns{synch-time},
917: \]
918: and there is a complete damage-free execution of $\rul{Find-end}$
919: during $[\Age(d_{0}),\Age(\e_{1})]$.
920:
921: \begin{step+}{legality.synch.not-done}
922: This execution of $\rul{Find-end}$ finds more than $Q/4$ cells in $\cC$
923: with $\End_{0}=U-1$.
924: \end{step+}
925: \begin{prooof}
926: Assume that this is not true.
927: Then this execution of $\rul{Find-end}$ sets the common value of
928: $\End$ to a value that was $\le\End_{0}(y,t)$ for one of the cells $y$ at
929: the time $t$ when it examined $y$.
930: By ~\eqref{e.End_{0}}, then $\End\le\Age(y,t)+\cns{end-period}$.
931: It is easy to see that subsequent executions of $\rul{Find-end}$ do
932: not change this value of $\End$ (except for the spot of damage, which will
933: be corrected).
934: Therefore the work period will have to end at an age before
935: $\Age(\e_{1})+\cns{end-period}$ which is not possible given our definition
936: of $\e_{1}$, since we came back $L$ steps within the work period
937: to $\Age(d_{0})$ and went forward at most $6\cns{synch-time}$ steps.
938: \end{prooof}%{legality.synch.not-done}
939:
940: Let us continue applying the Large Progress Lemma from $d_{1}$ and
941: extending the path backward from $d_{0}$ until a cell $c_{0}=(x_{0},v_{0})$
942: with $Q < \Age(x_{0}) \le 2Q$ or $v_{0} = \sg_{1}$, whichever comes first.
943: Look at the cells $y$ which were found by the above-mentioned run of
944: $\rul{Find-end}$ at some time $t$ to have $\End_{0}(y,t)=U-1$ and hence
945: $\Age_{1}(y,t)<U-1$.
946: There are so many of them that some of them will be damage-free during
947: the whole work period.
948: Take one such cell $y$.
949: Rule $\rul{March}_{1}$ keeps increasing $\Age_{1}(y)$ between times
950: $v_{0}$ and $t$, hence $t-v_{0}\le U\Tu$, and
951: \[
952: v_{1}-t\le v_{1}-u_{0}\le U\Tu + 5\tau_{1}L.
953: \]
954: Let us show that $\Age(c_{0})>2Q$ is not possible.
955: Indeed, this would mean $v_{0}=\sg_{1}$.
956: Then the big cell $y$ would go through a switch of a state in $\sg_{1}$
957: but our backward path has never changed a colony work period.
958: \end{pproof} %legality.synch
959:
960: \begin{step+}{legality.legal}
961: Under the assumptions, the switch in $\sg_{2}$ is legal.
962: \end{step+}
963: \begin{pproof}
964: Let us follow the development of the colony $\cC(x)$, starting from
965: the time $v_{0}$ found above.
966: Since the big cell is non-vacant during this, location $\fld{-Info}$
967: encodes a string with at most 2 errors.
968: The rule $\Compute$, begins, at age $\cns{compute-start}$, with an
969: application of $\Refresh$.
970: As the corresponding lemma shows, at the end of this, location
971: $\fld{-Info}$ will still encode the same string with possibly fewer errors.
972: Thereafter, the $\Info$ track will not change until the next work period,
973: except for the local changes caused by the damage and its corrections by
974: new applications of $\Refresh$.
975:
976: The following computation can be analyzed similarly to the first part of
977: the proof of Lemma ~\ref{l.refresh} (Refresh).
978: According to the definition of rule $\Eval$, the value put into the part
979: corresponding to $\Memory^{*}$ of $\fld{-Hold}$ is obtained without using
980: the result of $\Retrieve$, so it is certainly a value legally obtainable
981: from $\fld{-Info}$.
982:
983: Any subsequent change of $\fld{-Info}$ or $\fld{-Hold}$ caused by a
984: damage rectangle will be corrected by a later $\Refresh$, and any new
985: inhomogeneity of $\Doomed$ will be corrected by $\Heal$.
986: If $\Doomed=1$ then the whole colony dies, since the exposed right end is
987: impossible to heal.
988: In the case $\Doomed=0$, the rule $\rul{Finish}$ installs the changes on
989: the track $\Info$ in one step, leaving again no place for more than 2
990: errors.
991: In both cases, the state at time $\sg_{2}$ will be a legal consequence of
992: the state at time $\sg_{2}-$.
993: \end{pproof}%{legality.legal}
994:
995: \begin{step+}{legality.lb}
996: Let us lower-bound now the distance between the two switching times of
997: $\eta^{*}$ in $x$.
998: (The proof of the upper bound is similar but simpler.)
999: \end{step+}
1000: \begin{prooof}
1001: The usual analysis of $\rul{Find-end}$ shows that this rule changes
1002: $\End$ either in all cells (but possibly two) or in none of them (but two).
1003: Suppose first that $\End=U-1$ stays that way during the whole work
1004: period.
1005: Then the end would come only at $\Age=U-1$.
1006: Measuring the time for a cell that has never been affected by damage,
1007: this would give a lower bound $(U-2Q)\p_{1}\Tl>\Tl^{*}$.
1008:
1009: Suppose now that $\End$ becomes smaller than $U-1$.
1010: Consider the first execution of $\rul{Find-end}$ when this happens.
1011: Then there must have been some damage-free cell $x$ such that by the time
1012: $t_{1}$ this execution inspects $x$ it has $\Age_{1}(x,t_{1})=U-1$.
1013: Let $t_{0}$ be the time when $\Age_{1}(x,t_{0})=0$ at the beginning of
1014: the work period: then $t_{1}-t_{0}\ge U\Tl$.
1015: From here, the desired lower bound follows easily.
1016: \end{prooof} %legality.lb
1017: \end{Proof}% {l.legality}
1018:
1019: The lemma below follows easily from the above proof and from Condition
1020: ~\ref{cond.time-mark} (Time Marking).
1021:
1022: \begin{lemma}\label{l.dead-if-long}
1023: Assume that, for some rational number $a$, $\Damage^{*}$ does not
1024: intersect $\{x\}\times[a-\Tl^{*}/2+,a+2\Tu^{*}]$.
1025: If $\eta^{*}$ has no switching time during $[a+,a+2\Tu^{*}]$ then
1026: $\eta^{*}(x,a+)=\Vac$.
1027: \end{lemma}
1028:
1029: The following lemma infers about the present, not only about the past as
1030: the Attribution Lemma.
1031:
1032: For an extended damage rectangle $[a_{0},a_{1}]\times [u_{0},u_{1}]$, we
1033: call the rectangle
1034: \[
1035: [a_{0},a_{1}]\times [u_{0}, u_{0}+4\tau_{1}]
1036: \]
1037: its \df{healing wake}\index{damage!rectangle!healing wake}.
1038:
1039:
1040: \begin{lemma}[Present Attribution]\label{l.pres-attrib}
1041: \index{lemma@Lemma!Present Attribution}
1042: Assume that the live cell $c_{0}=(x_{0},t_{0})$ in colony $\cC$ with base
1043: cell $z_{0}$ is not a germ, and is to the left of the center of its
1044: originating colony.
1045: Assume also that $\cC$ at time $t_{0}$ does not intersect the healing
1046: wake of any damage rectangle.
1047: Then one of the following cases holds.
1048: \begin{djenum}
1049:
1050: \item\label{i.pres-attrib.center}
1051: $c_{0}$ is a member cell, attributed to $\cC$ which is covered by a domain
1052: of member cells at time $t_{0}$.
1053: If $Q <\Age <\End-Q$ then the $\Info$ track of this colony has at most 2
1054: errors;
1055:
1056: \item\label{i.pres-attrib.new}
1057: $c_{0}$ is a member cell from which a path of time projection at most
1058: $Q\tau_{1}$ leads back to to a growth cell in $\cC$ and this growth cell
1059: can be attributed to $\cC+QB$.
1060: At time $t_{0}$, if $\cC+QB$ does not intersect the healing wake of a
1061: damage rectangle then $[x_{0},z_{0}+QB-]$ is covered by a domain;
1062:
1063: \item\label{i.pres-attrib.ext}
1064: $c_{0}$ is an outer cell, attributed to its originating colony.
1065: At time $t_{0}$, if $\cC+QB$ does not intersect the healing wake of a
1066: damage rectangle then $[x_{0},z_{0}+QB-]$ is covered by a domain;
1067:
1068: \item\label{i.pres-attrib.vanish}
1069: $c_{0}$ is a member cell and there is in $\cC$ a backward path from
1070: $c_{0}$, with time projection $\le 2\cns{split-t}+(Q+1)\tau_{1}$ going back
1071: to a domain of doomed member cells covering $\cC$;
1072:
1073: \end{djenum}
1074: \end{lemma}
1075: \begin{Proof}\
1076: \begin{step+}{pres-attrib.old-member}
1077: Suppose that $c_{0}$ is a member cell and $\cC$ was covered by member
1078: cells at some time in the set $I\xcpt E$ (as defined around
1079: ~\eqref{e.attrib.I}).
1080: \end{step+}
1081: \begin{prooof}
1082: Using the Large Progress lemma repeatedly, we can go back to a time
1083: before age $\cns{compute-start}$ in $\cC$, just as in the proof of the
1084: Legality Lemma above.
1085: Then we can follow the development of the colony forward and see that it
1086: forms a continuous domain together with its extension.
1087: The $\Info$ track has at most 2 errors after the first application of
1088: $\Refresh$, as seen by Lemma ~\ref{l.refresh} (Refresh).
1089:
1090: If the computation results in a nonvacant value for the represented big
1091: cell then we have case ~\eqref{i.pres-attrib.center} of the present lemma.
1092: The represented field $\Creating_{j}$ of the colony will be broadcast
1093: into the field $\Growing_{j}$ of its cells, as shown in Lemma
1094: ~\ref{l.update-loc-maint}.
1095: The homogeneity of this latter field will be maintained by $\Heal$.
1096: Thus, depending on the value of $\Creating_{j}$ of the big cell, growth
1097: will take place and the growth forms a continuous domain with the
1098: originating colony.
1099:
1100: Suppose that the computation results in a vacant value.
1101: Then $\Growing_{j}$ will be 0 everywhere but in the healable wake of
1102: the damage.
1103: Growth cannot start accidentally by a temporary wrong value
1104: $\Growing_{j}=1$ in an endcell since there is enough time to correct
1105: this value during the long waiting time of
1106: $\rul{Grow-step}$. %prove!
1107: Also, all cells become doomed.
1108: After $\Age=1$, the doomed right end becomes exposed by definition, and
1109: the whole colony decays within $Q\tau_{1}$ time units.
1110: Before that, the colony is full.
1111: After that, we have case ~\eqref{i.pres-attrib.vanish} of the present
1112: lemma.
1113: \end{prooof}%{pres-attrib.old-member}
1114:
1115: \begin{step+}{pres-attrib.outer}
1116: If $c_{0}$ is an outer cell then we have case ~\eqref{i.pres-attrib.ext}
1117: of the present lemma.
1118: \end{step+}
1119: \begin{pproof}
1120: The Attribution Lemma attributes $c_{0}$ to the originating colony which is
1121: covered by member cells during $I\xcpt E$.
1122: It forms a continuous domain with its extension, until the age
1123: $\End$.
1124: From that age on, they form a multidomain.
1125: This could only change if the originating colony goes through a next work
1126: period and kills itself; however, there is not enough time for this
1127: due to ~\eqref{e.synch-start-lb-req}.
1128: \end{pproof}%{pres-attrib.outer}
1129:
1130: \begin{step+}{pres-attrib.young-member}
1131: Suppose that $c_{0}$ is a member cell but during $I\xcpt E$, the colony is
1132: never covered by member cells.
1133: Then we have case ~\eqref{i.pres-attrib.new} of the present lemma.
1134: \end{step+}
1135: \begin{pproof}
1136: Let $c_{1}$ be a non-member cell in $\cC$ during $I\xcpt E$.
1137: Then it is an outer cell that can be attributed to its originating
1138: colony and then the reasoning of ~\ref{pres-attrib.outer} above can
1139: be repeated.
1140: \end{pproof}%{pres-attrib.young-member}
1141: \end{Proof} %{l.pres-attrib}
1142:
1143: