Movement by propose and grant¶

Items move where they intend, each target granting one, each group moving all or nothing by whole-item assignment.

Requires

each item's Intent (the item it wants to move to, or none), its Priority (1), and its Group (a relation, such as a cell's body; an item alone is a group of one); the space's items, every quantity each carries (state).

Provides

the items rearranged, every quantity travelling with its item; the groups that moved and the groups refused (each a contact).

Law

propose stages each intent as (target, source, group, priority) from the step's input; grant gives each target to the proposal of the greatest priority, ties to the lowest canonical group, then source; commit moves a group only if all its proposals were granted, each item assigned whole to its target and each displaced item to the place its target's chain of moves vacated. A permutation of whole items, so every quantity is conserved; deterministic, the order of the proposals never read.

Source

lusine's rule on G15 and G10's propose and grant; Toffoli & Margolus, Cellular Automata Machines (1987), ch. 12, for the partitioned form it generalises.

Proof

invariant, limit.

No Trait form: not written in draft 5 yet: three kernels, propose, grant and commit, over the language's one primitive of whole-item assignment `it = it @ source`; until then a reference.

motion.moves(state, intent, priority, group, grant_fn)

Movement is three library kernels:

1. propose stages each item's intent: the item it wants to move to, or none; its priority; its group.
2. grant gives each target to one proposal: the greatest priority, ties to the lowest canonical key.
3. commit moves a group only if all its proposals were granted. Each item is assigned whole to its target, and a displaced item goes to the place the move vacated.

The game writes only the rules that set the intent. Here those rules are a toy game's, grains_and_liquid: sand and water fall into what is lighter, and water resting on a floor spreads.

In [1]:

import os, sys
root = os.getcwd()
while not os.path.isfile(os.path.join(root, 'docsite.json')):
    root = os.path.dirname(root)
sys.path.insert(0, os.path.join(root, 'tools'))
import numpy as np
import matplotlib.pyplot as plt
from lusine import library
from lusine.kernels.motion import moves as M
from lusine.kernels.motion.moves import moves, propose, grant, commit, NONE

import os, sys root = os.getcwd() while not os.path.isfile(os.path.join(root, 'docsite.json')): root = os.path.dirname(root) sys.path.insert(0, os.path.join(root, 'tools')) import numpy as np import matplotlib.pyplot as plt from lusine import library from lusine.kernels.motion import moves as M from lusine.kernels.motion.moves import moves, propose, grant, commit, NONE

The reference¶

The kernel's reference, in numpy. Its Trait forms are not written yet: three kernels over a proposals list binned by target, and the primitive it = it @ source, whole-item assignment.

In [2]:

library.reference(moves)

library.reference(moves)

Out[2]:

the reference, moves.py

def moves(state, intent, priority, group=None, grant_fn=None):
    """MOVEMENT BY PROPOSE AND GRANT: items move where they intend, each target
    granting one, each group moving all or nothing by whole-item assignment.

    Requires: each item's `Intent` (the item it wants to move to, or none),
    its `Priority` (1), and its `Group` (a relation, such as a cell's body;
    an item alone is a group of one); the space's items, every quantity
    each carries (`state`).
    Provides: the items rearranged, every quantity travelling with its item;
    the groups that moved and the groups refused (each a contact).
    Law: propose stages each intent as (target, source, group, priority)
    from the step's input; grant gives each target to the proposal of the
    greatest priority, ties to the lowest canonical group, then source;
    commit moves a group only if all its proposals were granted, each item
    assigned whole to its target and each displaced item to the place its
    target's chain of moves vacated. A permutation of whole items, so every
    quantity is conserved; deterministic, the order of the proposals never
    read.
    Source: lusine's rule on G15 and
    G10's propose and grant; Toffoli & Margolus, Cellular
    Automata Machines (1987), ch. 12, for the partitioned form it generalises.
    Proof: invariant, limit."""
    proposals = propose(intent, priority, group)
    granted = (grant_fn or grant)(proposals)
    return commit(state, proposals, granted)

Invariant: grains, every item kept¶

A random world of sand and water falls for forty steps. Every step is a permutation of whole items, so each material's count is the start's to the item, and every tag is still there once. The grains settle with nothing over a hole, and no sand rests over water.

In [3]:

rng = np.random.default_rng(5)
world = rng.choice([M.EMPTY, M.SAND, M.WATER], size=(16, 24), p=[0.5, 0.3, 0.2])
end, tags = M.run(world, 60)
for m in (M.EMPTY, M.SAND, M.WATER):
    assert (end == m).sum() == (world == m).sum()
assert sorted(tags.tolist()) == list(range(world.size))
assert not any(end[y, x] == M.SAND and end[y + 1, x] == M.WATER for y in range(15) for x in range(24))
fig, ax = plt.subplots(1, 2, figsize=(8, 3.2))
for a, img, title in ((ax[0], world, 'start'), (ax[1], end, 'after 60 steps')):
    a.imshow(img, cmap='viridis', vmin=0, vmax=3); a.set_title(title); a.set_xticks([]); a.set_yticks([])
plt.show()

rng = np.random.default_rng(5) world = rng.choice([M.EMPTY, M.SAND, M.WATER], size=(16, 24), p=[0.5, 0.3, 0.2]) end, tags = M.run(world, 60) for m in (M.EMPTY, M.SAND, M.WATER): assert (end == m).sum() == (world == m).sum() assert sorted(tags.tolist()) == list(range(world.size)) assert not any(end[y, x] == M.SAND and end[y + 1, x] == M.WATER for y in range(15) for x in range(24)) fig, ax = plt.subplots(1, 2, figsize=(8, 3.2)) for a, img, title in ((ax[0], world, 'start'), (ax[1], end, 'after 60 steps')): a.imshow(img, cmap='viridis', vmin=0, vmax=3); a.set_title(title); a.set_xticks([]); a.set_yticks([]) plt.show()

Limit: a liquid finds its level¶

Three cells of water stacked against a tank's wall lie in one row once they settle: the liquid spreads to a level.

In [4]:

tank = np.zeros((4, 9), dtype=np.int64)
tank[0:3, 0] = M.WATER; tank[3, :] = M.STEEL; tank[0:3, 8] = M.STEEL
end, _ = M.run(tank, 60)
print(end)
assert (end == M.WATER).sum() == 3 and (end[2, 0:8] == M.WATER).sum() == 3

tank = np.zeros((4, 9), dtype=np.int64) tank[0:3, 0] = M.WATER; tank[3, :] = M.STEEL; tank[0:3, 8] = M.STEEL end, _ = M.run(tank, 60) print(end) assert (end == M.WATER).sum() == 3 and (end[2, 0:8] == M.WATER).sum() == 3

[[0 0 0 0 0 0 0 0 3]
 [0 0 0 0 0 0 0 0 3]
 [0 2 2 0 0 2 0 0 3]
 [3 3 3 3 3 3 3 3 3]]

Invariant: two bodies contend, and one is refused whole¶

Body A (steel, two cells) moves right by two. Body B (sand, two cells) wants one of the same cells for one of its own. The cell goes to the heavier body. B moves nothing, not even its member whose target was free: a group moves all or nothing. Its refusal is the contact.

In [5]:

n = 12
mat = np.zeros(n, dtype=np.int64); mat[[0, 1]] = M.STEEL; mat[[4, 5]] = M.SAND
intent = np.full(n, NONE); intent[[0, 1]] = [2, 3]; intent[[4, 5]] = [3, 6]
prio = np.zeros(n); prio[[0, 1]] = 7800.0; prio[[4, 5]] = 1600.0
group = np.arange(n); group[[0, 1]] = 0; group[[4, 5]] = 4
new, committed, refused = moves({'material': mat}, intent, prio, group)
print('before', mat.tolist()); print('after ', new['material'].tolist()); print('moved', committed, 'refused', refused)
assert committed == {0} and refused == {4} and new['material'][6] == M.EMPTY and new['material'][5] == M.SAND

n = 12 mat = np.zeros(n, dtype=np.int64); mat[[0, 1]] = M.STEEL; mat[[4, 5]] = M.SAND intent = np.full(n, NONE); intent[[0, 1]] = [2, 3]; intent[[4, 5]] = [3, 6] prio = np.zeros(n); prio[[0, 1]] = 7800.0; prio[[4, 5]] = 1600.0 group = np.arange(n); group[[0, 1]] = 0; group[[4, 5]] = 4 new, committed, refused = moves({'material': mat}, intent, prio, group) print('before', mat.tolist()); print('after ', new['material'].tolist()); print('moved', committed, 'refused', refused) assert committed == {0} and refused == {4} and new['material'][6] == M.EMPTY and new['material'][5] == M.SAND

before [3, 3, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0]
after  [0, 0, 3, 3, 1, 1, 0, 0, 0, 0, 0, 0]
moved {0} refused {4}

Limit: a swap and a body's rotation are the same move¶

• A lone item moved into an occupied cell swaps with its occupant.
• A body moved down one cell takes its column's next item up to its top.

Both are one rule: a displaced item goes to where its target's chain of moves began. That is a rotation, and nothing is lost.

In [6]:

s, _, _ = moves({'tag': np.arange(3)}, [1, NONE, NONE], [1.0, 0.0, 0.0])
col, _, _ = moves({'tag': np.arange(4)}, [1, 2, NONE, NONE], [1.0, 1.0, 0, 0], [0, 0, 2, 3])
print(s['tag'].tolist(), col['tag'].tolist())
assert s['tag'].tolist() == [1, 0, 2] and col['tag'].tolist() == [2, 0, 1, 3]

s, _, _ = moves({'tag': np.arange(3)}, [1, NONE, NONE], [1.0, 0.0, 0.0]) col, _, _ = moves({'tag': np.arange(4)}, [1, 2, NONE, NONE], [1.0, 1.0, 0, 0], [0, 0, 2, 3]) print(s['tag'].tolist(), col['tag'].tolist()) assert s['tag'].tolist() == [1, 0, 2] and col['tag'].tolist() == [2, 0, 1, 3]

[1, 0, 2] [2, 0, 1, 3]

Invariant: the grant never reads the order the proposals came in¶

Shuffled, the same proposals grant the same targets to the same sources.

In [7]:

props = propose(intent, prio, group)
rng = np.random.default_rng(2)
for _ in range(20):
    assert grant([props[i] for i in rng.permutation(len(props))]) == grant(props)
print('the same grant over 20 orders')

props = propose(intent, prio, group) rng = np.random.default_rng(2) for _ in range(20): assert grant([props[i] for i in rng.permutation(len(props))]) == grant(props) print('the same grant over 20 orders')

the same grant over 20 orders

The planted fault: a double grant¶

A grant that gives a target to every proposal aimed at it lands two items on one place and loses one. The permutation breaks, which the first section's check refuses.

In [8]:

state = {'material': mat.copy(), 'tag': np.arange(n)}
bad, _, _ = M.WRONG(state, intent, prio, group)
print(sorted(bad['tag'].tolist()))
assert sorted(bad['tag'].tolist()) != list(range(n))

state = {'material': mat.copy(), 'tag': np.arange(n)} bad, _, _ = M.WRONG(state, intent, prio, group) print(sorted(bad['tag'].tolist())) assert sorted(bad['tag'].tolist()) != list(range(n))

[0, 0, 1, 4, 4, 5, 5, 7, 8, 9, 10, 11]