globals [states ;; translation to colors
rule ] ;; cellular automaton rule as a list of eight booleans
to-report state report position pcolor states end
to startup setup end
to setup
no-display clear-all
set states [white black 96] set rule encode 3 rule-number
ask patches [set pcolor 6.7 set plabel-color lime - 2]
let init read-from-string (word "[" initial-state "]")
set-init (0 - ceiling (length init / 2)) (max-pycor - 1) init
reset-ticks display
end
to set-init [x y sts]
let i 0 foreach fput 2 lput 2 sts
[ask patch (x + i) y
[set-state ? if ? != 2 [sprout 1 [set shape "dot" set color lime]]]
set i i + 1] ;; turtles act as read-write 'heads'
end
to go ;; one step
let ready turtles with [color = lime]
let n (min list (count ready) parallelism)
set ready selected n ready
if ready = no-turtles [stop] ask ready [step]
ask turtles [set color ifelse-value ready? [lime] [yellow]]
tick
end
to-report selected [n agents]
if bias = "none" [report n-of n agents ]
if bias = "left" [report min-n-of n agents [pxcor]]
if bias = "right" [report max-n-of n agents [pxcor]]
if bias = "breadth" [report max-n-of n agents [pycor]]
if bias = "depth" [report min-n-of n agents [pycor]]
end
to-report ready? report ;; not at edge of display
count (patch-set patch-at -2 0 patch-at 2 0 patch-at 0 -1) = 3
and all? nbrs [member? pcolor states] ;; no blank neighbors
end
to set-state [b] set pcolor item b states end ;; state encoded as color
to-report nbrs report (patch-set patch-at -1 0 patch-at 0 0 patch-at 1 0) end
to step
let a [state] of patch-at -1 0
let b [state] of patch-at 0 0
let c [state] of patch-at 1 0
let b' apply-rule (list (ifelse-value (a = 2) [b] [a])
b (ifelse-value (c = 2) [b] [c]))
let a' false ;; a' = c' won't be used unless at end
let ends [] if a = 2 [set ends fput -1 ends]
if c = 2 [set ends lput 1 ends]
if not empty? ends [set a' apply-rule (list b b b)]
foreach ends
[ifelse (a' = b')
[ask patch-at ? -1 [set-state 2 ]]
[ask patch-at ? -1 [set-state a']
ask patch-at (2 * ?) -1 [set-state 2 ]
hatch 1 [move-to patch-at ? -1 ] ]]
move-to patch-at 0 -1 set-state b'
end
to-report apply-rule [bs]
report ifelse-value (eval-bfn rule from-binary bs) [1] [0]
end
;;;;;;;;;;; the CA rule coding and evaluation machinery ;;;;;;;;;;;;;
to-report eval-bfn [fn-code args]
let l length fn-code
report ifelse-value (l = 1)
[last fn-code]
[ifelse-value first args
[eval-bfn (sublist fn-code 0 (l / 2)) (butfirst args)]
[eval-bfn (sublist fn-code (l / 2) l) (butfirst args)]]
end
to-report encode [r n] ;; 'r' for arity
report pad-to-length (2 ^ r) binary-list n
end
to-report binary-list [n] report
;; integer n represented as a list of booleans, where item i is the (2^i)'s bit.
;; to read the list as a 'normal' binary number (with the low bit on the right)
;; replace true by 1, false by 0
ifelse-value (n < 1)
[ [] ] [lput (odd? n) binary-list (floor (n / 2))]
end
to-report pad-to-length [n a-list]
if length a-list > n [error "list too long!"]
report ifelse-value (length a-list >= n)
[a-list] [pad-to-length n (fput false a-list)]
end
to-report decode [a-bool-list] ;; decimal representation
report ifelse-value (empty? a-bool-list) [0]
[2 ^ (length a-bool-list - 1)
* ifelse-value (first a-bool-list) [1] [0]
+ decode butfirst a-bool-list]
end
to-report to-binary [a-bool-list] ;; true/false --> 1/0
report map [ifelse-value ? [1] [0]] a-bool-list end
to-report from-binary [a-number-list] ;; 1/0 --> true/false
report map [? = 1] a-number-list end
to-report even? [n] report n mod 2 = 0 end
to-report odd? [n] report n mod 2 = 1 end
@#$#@#$#@
GRAPHICS-WINDOW
209
10
714
536
16
16
15.0
1
10
1
1
1
0
0
0
1
-16
16
-16
16
1
1
1
ticks
30.0
BUTTON
141
111
205
146
NIL
go
T
1
T
OBSERVER
NIL
NIL
NIL
NIL
1
SLIDER
3
151
205
184
parallelism
parallelism
1
world-width
1
1
1
operations per tick
HORIZONTAL
SLIDER
3
12
205
45
rule-number
rule-number
0
255
90
1
1
in Wolfram code
HORIZONTAL
BUTTON
3
111
80
146
NIL
setup
NIL
1
T
OBSERVER
NIL
NIL
NIL
NIL
1
INPUTBOX
3
48
205
108
initial-state
0 1 0
1
0
String
BUTTON
82
111
139
146
NIL
go
NIL
1
T
OBSERVER
NIL
1
NIL
NIL
1
CHOOSER
3
188
205
233
bias
bias
"none" "left" "right" "breadth" "depth"
0
TEXTBOX
33
302
169
421
patch cell\ncolor: state:\n----- -----\nwhite 0\nblack 1\nblue '...'\ngrey unknown
14
5.0
1
@#$#@#$#@
## Asynchronous parallel computation of Wolfram's 'elementary' cellular automata (ECA)
This model demonstrates a method of computing cellular automata with a fixed number of simultaneously active sequential processors, using non-deterministic scheduling and localized access to shared mutable state.
The algorithm corresponds to carrying out a derivation in a constructive logic, so the space-time diagrams it generates can be interpreted as formal proofs about the values of the 'lowest' (or 'newest') cells in the diagram. Thus, in some sense, the result or effect of the program is a proof of its own correctness. This method is independent of the actual CA rule, and may be extended to asynchronous computation of synchronized cellular automata in spaces of any dimension.
## More precisely,
I'll represent a single ECA cell, located at index _x_ in the array (that is, column _x_ in the in the ECA's space-time diagram), at time _t_ (that is, row _t_ in the diagram, counting up from 0 but conventionally 'reading' downward), having state (or color) _b_, as a proposition **cell**(_x_,_t_,_b_), where _x_ ∈ **Z**, _t_ ∈ **N**, and 'bit' _b_ ∈ **Z**_{2} = {0, 1}. (More generally, we could use any CA alphabet for _b_ --- I use **Z**_{2} here only because ECA cells have binary states. In the diagram, I'll color 0 white and 1 black.) Because this is a _constructive_ logic (without an excluded-middle law), propositions are simply either present or absent in the context of any particular step of a proof, and we cannot conclude anything about a cell's state from the absence of a proposition about it.
Although an elementary cellular automaton inhabits a linear array of infinite extent (modeled by the negative and positive integers **Z**), we can of course only represent a finite number of cells in this way for our computational purposes. So, as is customary, let us restrict our attention to global ECA states (at a particular time _n_) having a form somewhat like
⋯ 0 1 0 1 0 0 0 1 ⋯
where the '⋯' on the left (which precedes a 0) stands for an infinite string of 0s, and the '⋯' on the right (which follows a 1) stands for an infinite string of 1s, with a finite number of explicitly represented cells in-between. I'll represent these ellipses as literals, extending the CA's alphabet **Z**_{2} with an additional symbol '⋯'. This new alphabet is isomorphic to **Z**_{3} since we may as well encode '⋯' as '2'. So we will also have propositions of the form **cell**(_x_,_t_,⋯). During computation, it will be convenient to be able to represent _partial_ global states like
⋯ 0 1 0 0 1
where the gaps simply mark the place of values that we don't yet know, and are thus not yet explicitly represented by **cell** propositions.
Given an initial condintion and a maximum temporal index in the form of an integer _t__{max} such that 0 ≤ _t_ ≤ _t__{max} for all represented times _t_, or (alternatively) minimum and maximum spatial indices so that that _x__{min} ≤ _x_ ≤ _x__{max} for all represented spatial locations _x_, we can construct an ECA space-time diagram by the process described below (and in the code). This diagram is a finite subset of **Z** × **Z** × **Z**_{3} that forms a partial lattice under the usual successor / predecessor relations on **Z**, with points (_x_,_t_) in the lattice (representing space-time locations in the CA) decorated with states in **Z**_{3}. As I will show, these diagrams correspond quite directly with a tree-like presentation of a natural deduction proof in a constructive logic.
Elementary CA rules are Boolean functions of arity 3. We can encode an ECA rule _r_ : **Z**_{2}^{3} ⟶ **Z**_{2} into our system with eight four-place propositions of the form **rule**(_a_,_b_,_c_,_b_'): one for each of the eight distinct possible valuations of the three sequential 'input' bits _a_,_b_,_c_ together with the corresponding 'output' bit _b_'.
We interpret application of the ECA rule _r_ as the formal implication:
> **cell**(_x_--1, _t_, _a_), **cell**(_x_, _t_, _b_), **cell**(_x_+1, _t_, _c_), **rule**(_a_, _b_, _c_, _b_') → **cell**(_x_, _t_+1, _b_')
where _a_, _b_, _c_, and _b_' are 'bits' in {0, 1} and the commas between propositions denote simultaneous conjunction. An initial condition or starting state for the CA is a finite proposition sequence of the form
> **cell**(_x_--1, 0, ⋯), **cell**(_x_, 0, _b__{1}), ... , **cell**(_x_ + _n_, 0, _b__{_n_}), **cell**(_x_ + _n_ + 1, 0, ⋯)
We'll denote **cell**(_x_, _t_, _b_) visually in the space-time diagram by coloring the cell located at (_x_,_t_) white if _b_ = 0, and black if _b_ = 1. In the standard tree-like presentation of a natural deduction system, we could denote this implication as **r** with the following deduction rule
cell(x-1,t,a) cell(x,t,b) cell(x+1,t,c)
rule(a,b,c,b') a b c
------------------------------------------- r -----
cell(x,t+1,b') b'
On the right, I've written the same rule in a more compact syntax where **cell**(_x_, _t_, _b_) is denoted positionally by writing bit _b_ at position _x_ on line _t_ of the proof, with the implicit **rule** elided. This syntax can be used to denote parallel applications of **r** to cells at different _x_ locations, but at the same time _t_. For example, the position-annotated partial proof
x : 1 2 3 4 5 6 7 8 9 horizontal index
t = 0 ... 0 1 0 0 1 1 0 1 0 ... (initial state)
----- ---------
t = 1 1 0 1
shows three separate (and quite possible simultaneous) applications of **r**, where the corresponding ECA rule _r_ is that with Wolfram code 30.
Working downward in any order, successively applying the single rule **r** in all locations having three adjacent 'input' cells, we'll have made a lattice-shaped proof of the proposition **cell**(5,4,1) using nine initial 'facts' of the form **cell**(_x_,0,_b_) and sixteen applications of ECA rule 30:
t : 0 ... 0 1 0 0 1 1 0 1 0 ...
-----------------
1 1 1 1 1 0 0 1
-------------
2 0 0 0 1 1
---------
3 0 1 1
-----
4 1
which is essentially identical with an ECA space-time diagram. Notice that the order in which the rule is applied (in the 'forward' or downward direction) does _not_ affect the content of the finished proof. Backward inference is possible, but non-deterministic, as ECA rules are not generally reversible: an ECA array state at time _t_ may have many distinct predecessor states at time (_t_ -- 1), or none. But with this single rule, we can only derive shorter and shorter bit-strings, as we have no way of applying the ECA rule at their ends. It remains to operationalize the "⋯" symbol, allowing these sequences to expand during the course of a proof. To this purpose, I'll introduce four new rules (with their positional-notation shorthands):
cell(x-1,t,⋯) cell(x,t,b) cell(x+1,t,c)
rule(b,b,c,b') rule(b,b,b,a') a' = b' ⋯ b c
-------------------------------------------------- .r ------
cell(x-1,t+1,⋯) cell(x,t+1,b') ⋯ b'
cell(x-1,t,⋯) cell(x,t,b) cell(x+1,t,c)
rule(b,b,c,b') rule(b,b,b,a') a' ≠ b' ⋯ b c
-------------------------------------------------- ..r ---------
cell(x-2,t+1,⋯) cell(x-1,t+1,a') cell(x,t+1,b') ⋯ a' b'
cell(x-1,t,a) cell(x,t,b) cell(x+1,t,⋯)
rule(a,b,b,b') rule(b,b,b,c') b' = c' a b ⋯
-------------------------------------------------- r. -------
cell(x,t+1,b') cell(x+1,t+1,⋯) b' ⋯
cell(x-1,t,⋯) cell(x,t,b) cell(x+1,t,c)
rule(a,b,b,b') rule(b,b,b,c') b' ≠ c' a b ⋯
-------------------------------------------------- r.. ---------
cell(x,t+1,b') cell(x+1,t+1,c') cell(x+2,t+1,⋯) b' c' ⋯
The effect of these additional rules is to cause the number of propositions about cells at time _t_ + 1 to increase by as many as two, relative to the number of those about cells at time _t_. This increase happens only when necessary: if a newly deduced end symbol is the same as those indicated by the previous `⋯` symbol, then we can safely omit it. Consequently, the proofs may grow without bound unless some additional finiteness constraint is imposed.
To keep proofs finite, it is sufficient to require for every newly deduced **cell**(_x_,_t_,_b_) that 0 ≤ _t_ ≤ _t__{max}, a maximum _temporal_ index, resulting in a trapezoid-shaped proof. Alternatively, we may impose minimum and maximum _spatial_ indices so that _x__{min} ≤ _x_ ≤ _x__{max}. The latter constraint brings the bottom of the diagram to a single point **cell**(_x_,_t__{max},_b_), the _meet_ or _infimum_ of the entire finite partial lattice. Because no cell states above the initial state at _t_ = 0 are given, the _join_ or _supremum_ may not be defined for all pairs of cells, although its location certainly exists in **Z** × **Z**, and it may sometimes be possible to infer hypothetical values of cells with 'negative _t_ indices' using backward deduction. For this model, the 'boundary' indices are set by NetLogo's `max-pycor`, `min-pxcor`, and `max-pxcor` variables, so that the diagrams always fit the display.
Only one complete diagram (or proof) can be constructed for a given initial condition and specific finiteness constraint, regardless of the order in which the rules are applied. To avoid spuriously recalculating already-known values, it is useful to have a variable for each spatial index _x_ (each column in the diagram) which acts as a counter, being incremented with each application of a rule at _x_. Then we need only check the locations with the highest counter values in each column as sites for the possible application of a rule. The algorithm implemented in this model simply applies any applicable rules at available sites, possibly several at a time, terminating when no more can be applied. The finiteness conditions and counters themselves can be modelled in a _linear_ constructive logic, as I show in the Info tab of the **CA-synch-linear.nlogo** model (which should accompany this one).
Cells are shown in the diagram as white and black squares, corresponding to the symbols `0` and `1`, and '⋯' symbols are shown as blue squares. Those cells that are located where a rule _could_ be applied to yield new information are marked with a dot. These 'counter dots' turn green when enough information is available to apply a rule at the indicated site, and remain yellow otherwise. While the computation progresses they form a jagged but continuous "wavefront" whose shape depends on the bias (if any) of the nondeterministic rule-application scheduler. A pop-up menu on the interface allows you to choose a spatial bias.
@#$#@#$#@
default
true
0
Polygon -7500403 true true 150 5 40 250 150 205 260 250
circle
false
0
Circle -7500403 true true 0 0 300
circle 2
false
0
Circle -7500403 true true 0 0 300
Circle -16777216 true false 30 30 240
dot
false
0
Circle -7500403 true true 90 90 120
Circle -16777216 false false 90 90 120
line
true
0
Line -7500403 true 150 0 150 300
line half
true
0
Line -7500403 true 150 0 150 150
pentagon
false
0
Polygon -7500403 true true 150 15 15 120 60 285 240 285 285 120
square
false
0
Rectangle -7500403 true true 30 30 270 270
square 2
false
0
Rectangle -7500403 true true 30 30 270 270
Rectangle -16777216 true false 60 60 240 240
star
false
0
Polygon -7500403 true true 151 1 185 108 298 108 207 175 242 282 151 216 59 282 94 175 3 108 116 108
triangle
false
0
Polygon -7500403 true true 150 30 15 255 285 255
triangle 2
false
0
Polygon -7500403 true true 150 30 15 255 285 255
Polygon -16777216 true false 151 99 225 223 75 224
@#$#@#$#@
NetLogo 5.0.1
@#$#@#$#@
@#$#@#$#@
@#$#@#$#@
@#$#@#$#@
@#$#@#$#@
default
0.0
-0.2 0 1.0 0.0
0.0 1 1.0 0.0
0.2 0 1.0 0.0
link direction
true
0
Line -7500403 true 150 150 90 180
Line -7500403 true 150 150 210 180
@#$#@#$#@
0
@#$#@#$#@