A second row needs the remaining materials and somewhere to stand.
Returning the bricks, mortar, line, drawing and bricklayer makes another step possible. It does not, by itself, say how the new course becomes part of a wall.
A SMALL, FINITE MODEL
Build one course. Inspect what changed.
Wall W-1 · no courses yet8 bricks + 2 mortar units per course
Bricks returned
Mortar returned
Courses in W-1
Every brick shown is one model unit. Bond pattern and proportions are illustrative. The line shows its declared position, not a measured site condition.
The starting inputs are ready for one model step.
Still at the boundary
Worker BL-07 · drawing revision A · line L-1
The same worker, drawing and line remain available. No resource is copied or silently discarded; the remaining material counts are returned too. The built courses now belong to W-1.
Follow the state trace
END
Reusable work, with memory
Find what a recurring work block must retain when its next use depends on what has already been built.
WAY
Types plus state
Distinguish a repeated output tile from a wall-state update. Track finite stock, the support relation and persistent identities.
MEANS
A change you can see
Lay a course, try again, declare the next conditions and inspect the accepted or rejected transition. The trace and picture use the same state.
01 / TWO DIFFERENT COMPOSITIONS
Two outputs do not yet make one wall.
Write Q = M ⊗ L ⊗ BL ⊗ D ⊗ B for the mortar, positioned line, worker, drawing and bricks carried between steps. These are typed records: a count can decrease while its type stays the same. A returned worker has the same identity.
A tile that emits a course
Here the course is a separate output. It is not an input to the next step, so it has to pass that step on an identity wire. A suitable local support and setup for each independent output are assumed outside this toy model.
E : Q → Q ⊗ Co (E ⊗ idCo) ∘ E : Q → Q ⊗ Co ⊗ Co
The written output order is Q, new Co₂, bypassed Co₁. A symmetry can put the courses in chronological order; neither operation attaches one to the other.
Uses the selected starting supplies above, in a separate calculation.
A step that extends a wall
The existing structure is now an explicit input. A successful step appends one course, consumes eight bricks and two mortar units, and retains the worker, drawing and line.
S : Q ⊗ W → Q ⊗ W A : Q ⊗ W → Q ⊗ W S ∘ A ∘ S : Q ⊗ W → Q ⊗ W
W carries a foundation declaration, an ordered list of courses and the latest support-readiness declaration. Each new course records what supports it: the foundation or the preceding course. A is the explicit preparation between accepted steps: position the line for the next course and supply a new support declaration.
Both S and A are partial functions on these records. A declaration is an input to the model, not something the program discovers. After S, the line is still at the old height and support readiness is cleared. Thus S ∘ S rejects the ordinary first-step output.
This is the model you can run above. It remembers the wall; the emitted-course model only returns separate outputs.
02 / WHAT THE MODEL CHECKS
Repeated work keeps an account.
Three visible obligations
Materials: each accepted course consumes exactly eight bricks and two mortar units. Initial stock = returned stock + stock in courses.
Support: the first course needs the foundation declaration; later courses need a fresh declaration for the existing top course.
Continuity: the line must be positioned for the next course. The worker ID, line ID and drawing revision pass through unchanged.
Rejected attempts leave the wall and stock unchanged. The interface permits up to five courses, forty bricks and ten mortar units. Reaching this bound ends this example, not a real construction process.
One worker is a different interface
Here mortar is already supplied and the example uses one worker for successive laying steps. A serial Mix → Set → Lay plan could also use one worker if its assumptions permit it.
That is a different boundary from Essay 01’s two-worker preparation: one person mixes, a second sets out and builds, and both return. Two ports of type BL do not create two people. Turning two supplied worker ports into one is a change of interface, not an equivalent collapse.
Q deliberately contains no mixer, mixing inputs, lintels, roof or access equipment. They have not been hidden inside this course step; they belong to a different scope.
How to read these signatures
The boxes are interpreted in the symmetric monoidal category of partial functions with Cartesian product, or equivalently as their graphs inside Rel. A product-valued output is still one function value, so multiple output ports do not require nondeterminism. A rejected input has no accepted result.
The accepted set is guarded by the stated predicates. Identity wires carry a record unchanged; composition passes an intermediate state to the next function. Acyclic wiring explains the connections but does not prove physical feasibility. We do not claim a complete treatment of linear resources: the accounting is in these explicit state updates and guards.
Return materials, line and worker; repeat a laying box; keep corresponding ports in order. The early request also noticed that the first course is special.
The old claim that all six outputs could plug directly into an identical five-input Lay was ill-typed. The bypass identity and explicit W state make the two alternatives precise.
Separate architecture from a chosen input/output interpretation; hide matching intermediate values when composing relations.
Static relational composition alone supplies no curing duration, engineering release or resource schedule. The sequential state update here is explicitly proposed.
What is established: the finite program conserves its counted materials, preserves its declared resource identities and exposes rejected transitions. Its tests compare sequential state updates and the two-step emitted-output composition.
What remains assumed: eight bricks and two mortar units per course are illustrative constants. Suitable design, workmanship, bond, dimensions, mortar condition, site access and safe loading are not calculated. A checked declaration represents supplied evidence; it does not verify that evidence or approve a wall. Time, replenishment, waste, weather and multiple crews require a richer model.