# SpherePOP reducer: specification of the first milestone

This document fixes what the Go code in this module implements. It is taken from two sources: the essay on scoped structural rules (the circle calculus with permission-gated constants, boundary rules and restricted absorption) and the essay on duplication and universality (the SK fragment, strategies, and the Omega family). Where the code departs from a source, the departure is listed in section 10, so nothing here should be read as a claim that the essays proved more than they did.

## 1. Separation of concerns

A sphere is a structural object, a pop is a reduction governed by explicit rules, and a host (a game entity, a test, a command line) is only somewhere the computation can run. The module is organised so that this separation is enforced by imports and not by convention.

| Package | Role | Imports |
|---|---|---|
| `term` | immutable, content-addressed circle terms, parser, printer, paths | standard library only |
| `reduce` | rule table, permission structure, strategies, bounded evaluation | `term` |
| `trace` | trace documents, hash chain, independent checker | `term`, `reduce` |
| `sched` | deterministic fuel-bounded scheduler and its log checker | `reduce`, `term`, `trace` |
| `encode` | Church-style data a combinator program can branch on | `term` |
| `driver` | persistent programs: observe, evaluate, extract, commit, repeat | `effects`, `reduce`, `sched`, `term` |
| `lambda` | front end: lambda expressions to combinator terms | `term` |
| `arena` | headless example world: cells, portals, doors, ships | `effects`, `encode`, `term` |
| `effects` | host boundary: schema, decoder, authorizer, disposition log | `term` and `reduce.Result` |
| `cmd/spherepop` | command line | all of the above and `internal/vectors` |
| `internal/vectors` | conformance vectors from the essays | `term`, `reduce`, `trace` |

No package imports a game engine, graphics code, a clock, a random source or a network library. Effects are not part of the language at this stage. A future host receives a `Result` and a trace, and decides what they mean.

## 2. Terms

The scoped terms are generated by

```
t ::= a | c | sc_l | (t t) | <t>_l
```

where `a` is an atom, `c` a constant, `l` a label, `(t t)` an application circle and `<t>_l` a bracket labelled `l`. Concrete syntax accepted by `term.Parse`:

| Form | Meaning |
|---|---|
| lower-case identifier, optionally with digits, `_` or `'` | atom |
| run of decimal digits | atom (a numeral; inert, read as an integer only by a host) |
| one of `S K I B C W` | constant |
| `sc_l` with `l` of letters and digits | scope constructor |
| `f x y` | application, associating to the left |
| `(t)` | grouping |
| `<t>_l` | bracket with label `l` of letters and digits |

Any other upper-case identifier is a syntax error. Nothing binds: there are no variables in the sense of lambda calculus, and an atom is simply inert. The printer is canonical and `Parse(String(t))` is the identity on terms.

Terms are immutable. Every node carries a SHA-256 digest computed from a domain string, a one-byte kind, and either the node's name or the digests of its children, so two terms are equal exactly when their digests are equal. Subterms off a modified path are shared by `Replace`. `Size` counts application circles in the tree reading (the quantity the essays call circles) and saturates instead of overflowing; `DistinctNodes` counts the shared graph.

A path addresses a subterm: `L` is the function child of an application, `R` its argument, `B` the body of a bracket. The empty path is the root.

## 3. Permission structure

A configuration fixes a finite alphabet of gated constants (`W`, `K`, `C`, and optionally `S`), a root permission `pi(eps)`, and a permission `pi(l)` for each label. The chain of an occurrence is the sequence of labels of the brackets that contain it. Its effective permission is `pi(eps)` intersected with `pi(l)` for every label on the chain. A gated constant may contract at a position only if it belongs to the effective permission there. `I` and `B` are never gated. By default `Gated = {W, K, C}`, which is the alphabet of the scoped essay, so `S` is admissible everywhere.

A term that uses a label with no entry in the configuration is rejected by `Reduce` and by the checker with `ErrUnknownLabel`. The reducer never guesses a permission.

## 4. Rules

Each rule has a stable identifier. A trace step cites one, and `reduce.Apply` is the only code that decides what a step means.

| ID | Kind | Rewrite | Condition |
|---|---|---|---|
| `I` | contraction | `I x -> x` | always |
| `B` | contraction | `B f g x -> f (g x)` | always |
| `C` | contraction | `C f x y -> f y x` | `C` in effective permission, if gated |
| `K` | contraction | `K x y -> x` | `K` in effective permission, if gated |
| `W` | contraction | `W f x -> f x x` | `W` in effective permission, if gated |
| `S` | contraction | `S f g x -> f x (g x)` | `S` in effective permission, if gated |
| `Sc` | boundary | `sc_l u -> <u>_l` | always |
| `Abs` | boundary | `<u>_l v -> <u v>_l` | the absorption mode, section 5 |

A contraction redex at a node is a subterm `c x1 ... xn` with exactly `n` application circles, where `n` is the arity of `c` and the function-child chain from the node down to `c` contains no bracket. A bracket is never crossed by a spine, so the arguments of a redex all lie in the chain of its head, and a contraction never changes the chain of any surviving constant (Theorem 4.1 relies on this). Steps are closed under all contexts, including brackets.

## 5. Absorption modes

Unrestricted absorption is confluent only when `pi(eps)` is contained in `pi(l)` for every `l` (Theorem 4.2), and the essay gives the explicit counterexample `<a>_l (K b c)` with two normal forms, which the conformance vectors reproduce. The configuration therefore selects a side condition on `Abs`. In each case the argument `v` is tested at the chain of the application node being rewritten, using the effective permission there.

| Mode | `Abs` fires when | Status in the source |
|---|---|---|
| `off` | never | the core system, confluent for every permission structure (Theorem 4.1) |
| `any` | always | confluent iff `pi(eps)` is contained in every `pi(l)` (Theorem 4.2); kept to demonstrate failure |
| `nf` | `v` is R-normal | insufficient (Theorem 4.4) |
| `s` | `v` is settled | confluent (Lemma 4.5, Theorem 4.7) |
| `u` | `v` is R-normal and either settled or insensitive | confluent (Theorem 4.9); the default |

`v` is R-normal at a chain when it contains no permitted contraction there. It is settled when it is R-normal and no application inside it has a bracket as function child. It is insensitive when it contains no gated constant. `Config.Safe` exposes the criterion of Proposition 4.11, which is decidable in time linear in the size of `v`.

The `Sc` rule has a mode of its own, and restricting `Abs` does nothing for it. Theorem 4.2 states that the system with `Sc` is confluent iff `pi(eps)` is contained in every `pi(l)`, because `sc_l u` moves `u` into the chain of `l` whatever `u` contains. Randomized testing reproduces this: with `Sc` as stated and AbsU in force, divergent normal forms appear within a few hundred random terms. The mode `any` is the rule as the essay states it and is the default. The mode `safe` applies `Sc` only when its argument satisfies the same `Safe` criterion as AbsU. That restriction is not in the essays. It is status P: no proof, and the only evidence is the randomized test described in section 12.

## 6. Strategies

When several steps are available, a strategy chooses one. Order is by traversal of the term, with brackets entered at their body.

| Name | Order |
|---|---|
| `lo` leftmost-outermost | node before children, function child before argument |
| `ro` rightmost-outermost | node before children, argument before function child |
| `li` leftmost-innermost | children (function first) before node |
| `ri` rightmost-innermost | children (argument first) before node |

Strategies matter because they decide termination, not because they decide results when the system is confluent. The vectors reproduce the essay's table: `K a Omega` reaches `a` in one step under `lo` and `ro`, and cycles with period five under `li` and `ri`; `Omega` cycles with period five under `li`, `ri` and `ro`, and under `lo` never repeats a term.

## 7. Evaluation and fuel

`Reduce(term, strategy, fuel)` repeats: find the strategy's step, stop with a normal form if there is none, stop with `Exhausted` if `fuel` steps have been taken and a step remains, otherwise apply it. Every step, boundary steps included, costs one unit. A run that reaches a normal form on exactly its last unit of fuel is not exhausted. The result is a function of the term, the strategy and the configuration alone, so replay is deterministic.

Fuel is the host's tool for time slicing. A game loop gives each entity a budget per tick and keeps the `Result.Term` for the next tick; nothing else about the evaluator changes.

## 8. Traces and the checker

A trace is a JSON document with this content.

| Field | Content |
|---|---|
| `format` | the string `spherepop-trace/1`; anything else is rejected |
| `config` | the configuration, in canonical form |
| `start`, `start_digest` | the start term as text and its digest |
| `strategy`, `fuel` | what the worker claims it ran |
| `steps` | for each step: `rule`, `path`, `after` (digest of the whole term), `link` |
| `final`, `final_digest`, `exhausted` | the claimed outcome |
| `head` | the last link of the hash chain |

The chain begins from a hash of the format, the start digest and the configuration digest, and each link hashes its predecessor with the step's rule, path and result digest. Unknown JSON fields are rejected.

The checker parses the start term and the configuration afresh, verifies the digest, and replays each step with `reduce.Apply`. It rejects a step whose rule is not in the table, whose rule does not match the subterm at the cited path, whose rule is not admissible at that position under the effective permission, or whose result digest differs from the claim. It then verifies the head, the final term, the termination status (`exhausted` must agree with whether a step remains), and that the step count does not exceed the stated fuel. A claim of exhaustion must use the whole budget: the step count must equal the stated fuel. Because a worker states its own fuel, a truncated run can be made self-consistent by restating the fuel, so a host that has agreed a budget passes it as `Options.Fuel` (`--fuel` on the command line) and the checker requires the document to state exactly that. With `RequireStrategy` it also demands that each step is the one the claimed strategy would take. Failures are `*Violation` values wrapping one of the sentinel errors in `trace/check.go`.

### What a successful check establishes

Every step is an instance of a rule in the table, at a position where that rule is permitted under the configuration recorded in the document, and the recorded final term is what that sequence produces from the recorded start term.

### What it does not establish

Matching final digests alone prove nothing, and the checker does not rely on them. A checked trace does not show that the result is the unique normal form, since confluence is a property of the system and configuration and not of a trace (it is why the absorption modes exist). Without `RequireStrategy` it does not show which order the worker used, because agreement on a result is different from agreement on how it was found. The hash chain gives integrity and order within the document, but a forger can recompute it, so tamper evidence holds only relative to an anchor held outside the document, such as a head digest published or signed elsewhere. The checker shares `reduce.Apply` with the reducer, so a bug in the definition of a rule would be shared by both; a second implementation written from this specification is the way to remove that dependence. Finally the trace does not say that anyone should accept or commit the result. Acceptance is a separate decision, made by whatever policy the host holds, and the reducer deliberately has no notion of commitment so that a verifier gains no authority from being able to replay.

## 9. Command line

| Command | Effect |
|---|---|
| `spherepop reduce TERM [--fuel N] [--strategy lo\|li\|ri\|ro] [--trace] [--out FILE] [--perm LABEL=K,C]... [--root W,K,C,S] [--absorb off\|any\|nf\|s\|u] [--sc any\|safe] [--def NAME=TERM]...` | reduce and print the result; flags may follow the term |
| `spherepop check FILE [--strategy] [--fuel N] [--max-steps N]` | verify a trace; `-` reads standard input |
| `spherepop test` | run the conformance vectors |
| `spherepop rules` | print the rule table |

Exit status is 0 on success (for `reduce`, a normal form), 1 on failure (invalid trace, failed vector, I/O or configuration error), 2 on a usage error, and 3 when `reduce` stops because fuel ran out.

Source text is bounded. `term.Parse` rejects input longer than `MaxSourceBytes` (4 MiB) or nested deeper than `MaxNesting` (100000) with a `SyntaxError`, so a hostile start term in a trace cannot exhaust the stack or memory of the checker. The checker's `MaxSteps` option bounds replay time.

## 10. Departures from the sources and open items

The essays use `S` only for comparison and gate only `W`, `K` and `C`. The code allows `S` to be gated as an option. The theorems are not claimed for a configuration that gates `S`.

The scoped essay defines settled without mentioning `sc`. The code also treats a pending `sc_l u` inside the argument as unsettled. This is stricter than the essay, so it can only refuse absorptions the essay would allow, but the confluence theorems have not been re-proved for the combination of `Sc` with restricted absorption; that combination is status P here. The `safe` mode of `Sc` (section 5) is likewise this module's own addition and also status P.

Theorem 4.4 is stated for an abstract spine-based relation, `((p x) y) -> x` permitted when a label is absent from the chain. The configuration here is combinatory, so that counterexample is not representable and is not among the vectors. The Theorem 4.2 counterexamples for `K`, `W`, `C` and `Sc` are.

Open mathematical obligation: a proof for the `safe` mode of `Sc`. What exists is an overlap analysis and an exhaustive search, both described in section 13. Neither is a proof.

Not implemented in this milestone: term graphs with sharing and the Any and All policies (Example 5.4), the Gross-Knuth strategy, bracket abstraction and the counter-machine compilation, the disposition calculus (POP, REFUSE, BIND, TRANSFORM, VERIFY, COLLAPSE), and any per-tick scheduler. The disposition lifecycle is intended to live in the evidence layer next to `trace`, not in the reducer. Redex search is a tree walk with memoisation on digest and effective permission, which is adequate for the vectors but will need a graph-based representation for terms with heavy sharing. Lemma 6.1 (effective permission of a surviving constant only shrinks) is relied on by the design but has no vector yet, because tracking the identity of a constant through duplication needs a term-graph representation.

The `M x` vector checks the normal form `x x x` only, since the essay gives no step count for it.

## 11. Scheduler

Package `sched` runs several terms under a deterministic, fuel-bounded schedule. Its authority is exactly a strategy and a fixed budget. It hands every reduction to `reduce` and cannot alter the rule table or the configuration after a world is built.

Entities run in byte order of their identifiers, whatever order they were supplied in. In each tick every unfinished entity receives the policy's budget and reduces from wherever it stopped; the continuation is simply its current term. An entity in normal form is skipped and spends nothing. A non-terminating entity therefore cannot starve the others.

The log separates two kinds of record. Scheduler decisions (`run` with a budget, or `skip`) are events. Reduction steps appear only inside the slice document attached to a `run` event, which is an ordinary trace document. `sched.CheckLog` verifies three things independently: that the decisions follow the policy (whole ticks, identifier order, finished entities skipped, exactly the budget granted); that every slice passes `trace.Check` with the strategy enforced, the fuel fixed at the budget, and the log's own configuration; and that the slices chain, each starting where the entity's previous slice ended, with the final states following from the chain.

`sched.HostConfig` is the configuration a game host should start from. It differs from `reduce.DefaultConfig` only in setting `Sc` to `safe`. The language default stays the essay's rule, and `--sc any` remains available as the research mode. `spherepop sim` follows the host default.

Entities do not communicate, because the language has no effects yet. This is deliberate: it makes the following experiment meaningful. Holding total fuel per entity constant while varying the frame subdivision (budgets 1, 2, 3, 4, 5, 6, 10, 12, 15, 20, 30 and 60 over a fixed total of 60) gives identical final states, equal to the unsliced reduction. The reason is that a strategy is a function of the current term, so slicing a run and resuming it reproduces the unsliced run. Scheduling alone therefore cannot change a result, entity order does not change any entity's outcome, and the same world under two different strategies on a non-confluent configuration does disagree. Any difference that appears after events are introduced can thus be attributed to event ordering and not to slicing or to the calculus.

A host can start a new round of a persistent program with `World.Rearm`, which stages a replacement term applied at the start of the next tick and recorded in that tick's event, with a flag marking whether it preempted an unfinished term. The scheduler carries the replacement and vouches for nothing about it; `CheckLog` verifies that the recorded digest matches the text, that the labels are known, that the preemption flag agrees with the entity's state, and that the following slice starts from the replacement. A replacement cannot ride on a skip event.

Not yet done: mailboxes, per-entity budgets or priorities, a bound on log size (slices are stored whole), and an agreed external anchor for the log head.

## 12. Audit record

The code was audited against this specification with randomized tests in `reduce/property_test.go`: random scoped terms over `I B C K W`, atoms, labels, brackets and `sc`, random permission structures, and for each term the four strategies plus several runs choosing a random available step at every point, with the set of normal forms compared.

With no absorption, with AbsU and with AbsS (terms without `sc`), no divergence appeared in several thousand terms per mode, in agreement with Theorems 4.1, 4.7 and 4.9. With unrestricted absorption the search finds divergence, so the test is not vacuous. With `sc` present and `Sc` as the essay states it, divergence appears under every absorption mode, as Theorem 4.2 predicts. With `Sc` in mode `safe` and AbsU or AbsS, no divergence appeared in 3000 terms per mode. This is evidence, not proof, and the generator uses small terms (depth five, three atoms, two labels).

The audit also found two defects in the first version, both fixed: a claim of exhaustion was not tied to the step count, so a truncated trace could pass, and the parser had no bounds on hostile input.

Not audited: behaviour on terms large enough to stress the memoisation tables, which grow with the number of distinct subterms visited in a run and are bounded only by fuel.

## 13. Overlap analysis and exhaustive search for the safe modes

Status P throughout: this section is an argument sketch and a bounded search, and neither is a proof. Section 17 supersedes the sketch for the settled form of both boundary rules, which it proves, and records why the sketch's route cannot prove the safe form as defined here.

### The structure of the argument

The orthogonality argument of Theorem 4.1 does not apply once a boundary rule is present, because the admissibility of a contraction depends on the chain of its position and a boundary rule changes chains. The relevant overlaps are therefore not syntactic; they are the interactions in which a boundary step moves a subterm into a chain with fewer permissions while another step is available inside or around it. Both `Abs` and `Sc` are transport steps of this kind: `<u>_l v -> <u v>_l` carries `v` into the chain of `l`, and `sc_l u -> <u>_l` carries `u` into it.

Both safe modes fire only when the transported argument `w` satisfies `Safe(w, m)`, where `m` is the effective permission at the site: `w` is R-normal at `m`, and is either settled or insensitive. The sketch rests on one observation. After transport `w` sits at a mask contained in `m`. If `w` is settled it has no permitted contraction and no pending boundary step at `m`, and shrinking the mask removes permitted contractions without adding any (Lemma 3.5), so it has none after transport either; its available steps are the same, namely none. If `w` is insensitive it contains no gated constant, so every contraction inside it is headed by `I` or `B`, which are permitted at every chain, and every boundary step inside it has a transported argument that is itself insensitive, hence passes `Safe` at every chain. The steps available inside an insensitive term, with their side conditions, are the same at the source chain and at the target chain. So a safe transport never changes what can happen inside the transported term.

The cases for `Sc` against another step at a distinct position are then as follows. A step inside `u` while `sc_l u` is pending: `Safe(u, m)` allows only chain-independent boundary steps inside `u`, which are available identically after the transport, so the two orders join. If such a step creates an `I` or `B` redex, the `Sc` is blocked until that redex fires and the other order catches up. A contraction that copies or discards a term containing `sc_l u` as an argument: the copies lie at the chain of the redex root, so each has the same side condition and all fire. An `Abs` or `Sc` above that carries a term containing `sc_l u`: such a term is not settled, because of the conservative clause for pending `sc`, so it must be insensitive, and an insensitive term passes `Safe` at every chain. `Sc` against `Abs` where the `Sc` redex lies in the body of the bracket: the body stays at the same chain, so they commute. The case that fails for the essay's `Sc`, a permitted contraction inside `u` that the transport would strand, is excluded because `Safe` requires `u` to be R-normal at the source chain.

What the sketch does not cover, and what a proof must supply: the passage from local joinability to confluence for terms containing `W` or `S`, which do not terminate (the essay's route is strong commutation with a termination measure, Lemmas 4.5 and 4.6, and the measure has to be extended to count `sc` nodes); and a check that the conservative clause for pending `sc` in the definition of settled does not break any step of those lemmas.

### The exhaustive search

`reduce/exhaustive_test.go` enumerates every term up to a bound on leaves and brackets over a fixed set of symbols, assigns every combination of permissions from `{W, K, C}` to the labels it uses with the root permission full (which loses nothing, since effective permissions are intersections), explores every reduction path, and collects the distinct normal forms. A second normal form is a counterexample whether or not the term terminates. If exploration exceeds 600 states or 40 circles the term is counted as capped and not as a pass. Two positive controls guard the test: the search must find the essay's `Sc` failing and unrestricted `Abs` failing, and it does, at the minimal terms `sc_x (K a a)` and `<a>_x (K a a)`.

Safe `Sc` with AbsU, AbsS and Abs off, symbols `a K C W I sc_x`, one label: no second normal form for terms of up to four leaves and one bracket (about 0.5 million explorations per mode), up to five leaves and one bracket (about 10.9 million per mode, 0.16 percent capped), and up to four leaves and two brackets (about 3.3 million per mode, 0.1 percent capped). With two labels, so that nested brackets can carry different permissions, and the symbol `sc_y` added: no counterexample for terms of up to three leaves and two brackets (about 2.6 million explorations per mode, under 0.01 percent capped) up to four leaves and one bracket (about 6.7 million per mode, 0.04 percent capped), or up to three leaves and three brackets (about 17.9 million per mode, 0.01 percent capped). A run at four leaves and two brackets with two labels did not finish within its time limit and is not counted. The search is rerun at larger bounds by setting `SPHEREPOP_SEARCH_LEAVES`, `SPHEREPOP_SEARCH_BRACKETS` and `SPHEREPOP_SEARCH_LABELS=2`, and the default `go test` runs only the small configuration. Capped terms contain `W` loops, so the unexplored remainder is exactly the nonterminating region the sketch above also leaves open.

## 14. The effects boundary

A program can describe an effect and cannot perform one. The design keeps three relations apart, and the code keeps them in different packages: reduction, `t ->* n`, belongs to `reduce`; extraction of proposals from a normal form, `n |-> E`, belongs to `effects`; and the transition of the world with its recorded dispositions, `(W, E) |-> (W', D)`, belongs to the host. Reduction rules are not touched. The words `effects`, `effect` and the host's own vocabulary (`door`, `open`) are ordinary atoms, and the reducer treats them as it treats any atom.

### Output convention

The host reads one designated position and only after reduction has reached a normal form: the normal form must be an application whose head is the atom `effects`, with one request per argument, in order. A normal form of any other shape is not an error, it is simply an output with nothing to consider, and the host records that. A reduction that ran out of fuel is never read, even when its partial term happens to look like an output, because a partial term is not a result. No suspension points exist yet; when they are added they will be explicit, defined moments and not something a constructor appearing in a term can cause.

Reading a normal form and not an intermediate term is what keeps effects independent of strategy. An effect inside a subterm that `K` later discards is never proposed, and one that `W` duplicates is proposed twice, whichever strategy got there. Tests exercise both.

### Requests and the schema

A request has the form `effect (kind id) verb arg...`, for instance `effect (door 3) open`. The host supplies a schema that lists, for each target kind, the type of its identifier and the verbs it accepts with the types of their arguments. There are two types, `sym` (an identifier atom) and `int` (a canonical unsigned decimal numeral that fits 32 bits; `03` is rejected, so one number has one spelling). A request that is a well-formed term but not an instance of the schema is malformed. The decoder never reduces and never panics.

### Authorization and independence

Each request is decoded, authorized and committed on its own, in the order the program listed them. A malformed request, a denied request or a commit the world refuses does not affect the others. The authorizer is an interface asked after decoding and before the world is touched, and the supplied `Policy` is fail-closed: only explicit grants of a subject to a verb on a kind are allowed. A request that must be atomic with others is out of scope for this milestone and should be expressed through a separate host-level transaction mechanism, not by changing these semantics. A per-output cap (64 by default) stops a program from handing the host an unbounded list, and the excess is recorded as a single truncation entry.

### Dispositions and the log

Every outcome is appended to a log: committed, denied, failed (authorized but the world refused), malformed, no output, exhausted, or truncated. Each entry carries the tick, the subject, an opaque reference to the evidence (for instance a trace head), the position of the request in the output, the canonical text of the request, and a reason. The log is append-only and hash-chained, and it can be streamed as JSON lines. `Verify` checks the chain; `VerifyAnchored` also requires the head to equal a digest held elsewhere, because a bare chain cannot reveal removal of its tail; `VerifyAgainst` also checks the entries against the schema, so a log cannot present a schema-invalid request as committed or a valid one as malformed. As with trace documents, tamper evidence is relative to an external anchor.

### What the experiment shows

Two entities propose conflicting changes to one door. Their programs reach the same normal form under all four strategies and under every subdivision of the same total fuel tested, so the proposals are identical in every run. The committed state of the door then depends only on the order in which the host processes the two entities, while the recorded dispositions are the same in both orders. In this setting, then, a difference in committed world state can be attributed to host ordering and not to the calculus, the strategy, or the frame subdivision.

### Not yet done

Atomic transactions. Explicit suspension points. A command-line entry point for the host. A second implementation of the log verifier written from this section.

## 15. Observation and the frame loop

### Data a program can use

Atoms are inert, and no combinator can inspect one, so a program cannot branch on an atom. It can branch on a function. Observations are therefore given to a program as Church-style functions, and package `encode` is the host's side of that contract. A Boolean is `K` for true and `K I` for false, so that `b x y` reduces to `x` or to `y`. A natural number `n` is the Church numeral that applies its first argument `n` times to its second, built from `K I` by repeated `S B`; numerals are unary, so `encode.MaxNat` bounds them. An identifier passes through as an atom, which a program cannot examine but can copy into an effect it proposes, and that is how it names a target it was told about. These encodings use `K`, so a configuration that withholds `K` from the scope where a program runs also disables its Booleans; that is a property of the configuration and is not hidden.

### Rounds

A persistent program is a term `P` that takes the observation as arguments, one per observed fact, in an order the host and the program agree on. A round is the evaluation of `P o1 ... on`. When the round reaches a normal form the host reads its proposed effects as in section 14, and the next round is `P` applied to a fresh observation. Programs are stateless between rounds; whatever a program must remember has to be part of the world, where the next observation will show it. A host-held memory for an entity could be added as an ordinary effect on the entity itself, but it is not part of this milestone.

### The frame

One frame is, in order: the scheduler gives every unfinished entity its budget; the effects of every round that finished are handled in identifier order; and then, from the world as it stands after all of those commits, every entity that finished or was abandoned is observed and re-armed, again in identifier order, with all observations taken before any re-arm. Observations are therefore a simultaneous snapshot. No entity sees another's commit from the same frame before it has acted, and none sees a commit made after the snapshot. The alternative of observing each entity immediately after its own commit would make an entity's view depend on its identifier, and a test exists that fails if the loop is changed to do that. The first observation of each entity is taken, in identifier order, when the driver is built.

A round may span several frames when a program needs more steps than the budget allows. The partial term is never read. A host can set a bound on frames per round; a round that reaches it is recorded as exhausted in the effects log, the entity is re-armed with a fresh observation, and the scheduler log marks the replacement as a preemption. Without a bound, a program that never terminates simply never acts again and appears in no effects log, because there is nothing for the host to say about it.

### What changes now that programs observe

Before observation existed, the schedule could not change any entity's result, because a strategy is a function of the current term. That remains true of a single round. It is no longer true of a run, because the time at which a round finishes decides which world its effects land in and which world the next observation sees. The tests show the shape of the new dependence: a toggling program run with a small budget and with a large one proposes the same sequence of requests, but the door is in a different state at the same frame, because the slow program's effects land later. With several entities the sequences themselves can diverge. The scheduler log and the effects log together record both the timing and the proposals, so a difference can be located in one or the other.

### Evidence

Each effects entry carries the head of the trace slice that produced its output, and a test checks that every such reference is the head of a slice in the scheduler log. The scheduler log verifies on its own, replacements included, and the effects log verifies against the schema. Two runs of the same world are byte-identical in both logs. What no checker establishes is that the observer reported the world truthfully: an observation is an input, recorded in the log as the replacement term, and the host is trusted to have produced it from the world it committed to.

### Not yet done

Suspension points inside a round. Atomic transactions. A command-line entry point for the driver (the arena is exercised by tests only). A second implementation of the verifiers written from sections 11, 14 and 15.

## 16. Lambda front end and the arena world

### Lambda front end

Package `lambda` is a convenience for writing programs. It reads `\x y. body`, applications by juxtaposition and parentheses, and compiles by bracket abstraction into the combinators `S K I B C`, using the usual optimizations (`B`, `C`, and eta contraction). The output is an ordinary term, so nothing in reduction, traces or the checker knows the front end exists, and a trace of a compiled program is checked like any other. Bound names are variables. Any other lower-case name stays an inert atom, which is how a program mentions `effects`, `effect`, `door` and the like. Brackets and `sc_` are rejected, since the front end has no account of scope. `spherepop compile 'EXPR' [--def NAME=TERM]` prints the term. The compiler is not part of the trusted base for a result: the checker validates the reduction of the compiled term, and says nothing about whether the compiled term means what the source meant. Compilation is tested by reducing compiled programs against their lambda reading, with mutation checks on the `B`/`C` choices.

Limits: source of at most 1 MiB and nesting of at most 10000.

### The arena

Package `arena` is the first world. It is a host and not part of the language. It has boxes (cells) joined by portals on shared faces, doors that gate portals, and spheres (ships) of fixed radius. All arithmetic is integer: velocity gains `Accel` per thrust request, is damped by 7/8 with truncation toward zero, and is clamped to `MaxSpeed`. A tick moves ships in identifier order, each along X then Y then Z, so the result does not depend on the order of requests within a frame. A ship's surface stops at a wall. Its centre may reach a portal plane only if the portal's door is open and the centre lies inside the opening shrunk by the radius on both transverse axes; then it changes cell. `World.Check` verifies that every ship lies inside its cell and within the speed limit after each tick.

The arena supplies the three host-side pieces the driver needs. `Schema` lists `door N open|close` and `ship S thrust east|west|north|south|up|down`. `Commit` applies an authorized request and refuses, without side effects, one that names nothing that exists. `Authorizer` adds one rule above the grant list: a ship may command only itself. `Observer` gives a ship eight Church Booleans: goal beyond it on each of six directions (measured to the goal cell's centre), ship in the goal cell, door open. The driver's `Params.Advance` hook runs the world's own step once per frame after effects are committed and before observation, so observations see the world after it moved.

Tests run a behavior written in lambda syntax end to end: open the door and thrust east until in the goal cell, then close the door. They also check that a closed door blocks the ship, that a ship off-centre by either bound cannot use an open portal, that a ship cannot command another, and that two runs give identical ship state and identical effects-log heads. Mutating the door check, either transverse bound, or the self-command rule makes a test fail.

### Host-held memory

A program is stateless between rounds, so memory is a fact about the world. Each ship has a register holding an integer from 0 to `MaxReg` (64), changed only by the effect `ship S set N`, which goes through the same decode, authorization and logging as every other effect, and so appears in the effects log. With `Observer.Registers` on, the register is passed as a ninth argument, a Church numeral. A two-state behavior can then branch on it (`reg (\z. idle) active` selects `active` for 0 and `idle` otherwise), and a test shows a ship that cruises, closes the door on arrival, records that in its register, and afterwards leaves an outside change to the door alone. Memory therefore adds no authority: a program can write only its own ship's register, because the self-command rule applies to every ship verb, and the register is bounded so that its numeral stays small.

### What this shows and does not show

The Church encodings are livable once the front end exists: the behavior above is three lines. Programs are still stateless between rounds, so any behavior that needs memory has to put it in the world. The physics is deliberately crude and is not a model of Descent. Nothing here is evidence about the confluence of safe `Sc`; the arena runs with `Sc = safe` as the host default, as in section 11.

## 17. Confluence of the scope constructor

The full statement and proof are in `notes/settled-scope.tex`. This section records what the specification relies on.

### Result

Add a third scope mode, `settled`, in which `Sc` fires only when its argument is settled at the effective permission of the redex. Settled means no permitted contraction and no application whose function child is a bracket or a scope constructor, so a settled term contains no step of any kind and is unchanged by every step elsewhere in the term. With `--absorb s` and `--sc settled`, and for every permission structure and gated set, the single-round parallel reduction has the diamond property, so the system is confluent, for terms that do not terminate as well. The proof is the Takahashi argument for an orthogonal system, with the one addition that the side conditions concern only frozen arguments and are therefore stable under every step. Status: proved on paper (the note), supported by a bounded search over all pairs of parallel successors of all small terms, with no failures and no capped terms, at up to four leaves and two brackets, five leaves and one bracket, and three leaves, three brackets and two labels.

### The safe form

The `safe` mode, which admits an argument that is R-normal and either settled or insensitive, does not satisfy the parallel diamond. The minimal witness is `sc_x (<I>_x a)`: `Sc` and the inner `Abs` are both available, and after the `Abs` creates the contraction redex `I a` the `Sc` is blocked until that contraction runs, so the two branches need a different number of rounds. The failure is already present with `--absorb s`, so it comes from the insensitive clause of `Sc`. It is a failure of this proof method and not a counterexample: local confluence of the full relation (both kinds of step on both legs, joins searched to depth eight) held for every peak in the runs described below, and the normal-form search of section 13 stands. The `u` absorption mode has the same pattern when brackets nest, at `<a>_x (<I>_x a)`. The earlier claim that the overlap sketch of section 13 covers `safe` is therefore withdrawn as a route to a proof; the sketch remains a description of the cases.

### Recommendation

Before the game host treats scope construction as a stable part of the language, change its restriction from safe to settled for both boundary rules, that is `--absorb s --sc settled`. The cost is that `sc_l u` waits until every boundary step inside `u` has run, so a scope whose argument holds a boundary step that never fires stays inert, which matches what a blocked `Abs` already does. The host default in package `sched` is still `safe` and `u`; changing it is a decision for the language owner, not a consequence of the tests.

### Tests

`reduce/parallel_test.go` holds the parallel step and the diamond checks, with the essay's unrestricted `Sc` as a positive control and the safe-form failure recorded as an expected, named witness. `reduce/peaks_test.go` checks local peaks of the full relation. `reduce/settled_test.go` checks the mode's behaviour on the witness and, over all small terms and all permission structures, that a settled term has no step at its own or any smaller permission. Larger bounds are set with `SPHEREPOP_SEARCH_LEAVES`, `SPHEREPOP_SEARCH_BRACKETS` and `SPHEREPOP_SEARCH_LABELS`; the two largest reported runs took about twenty minutes each.

### Not covered

The search uses the symbols `a K C W I sc_x` (and `sc_y`), so `S` and `B` appear in the theorem but not in the enumeration. Permissions are subsets of `{W,K,C}`. The theorem does not cover `--absorb u`, which remains the reducer's default outside the host, or `--absorb any` and `nf`.