Back to app index

Current reading: resources and reusable boundaries · wiring and its algebra · course-by-course dynamics. This supporting working retains the static-relation interpretation: component predicates compose by hiding internal values. It concerns a toy load/acceptance relation, distinct from the resource-flow construction sequence and from a full assume–guarantee contract theory.

Wall + Roof Safety as a Contracts Algebra over a Wiring Diagram

This page turns a simple construction “wall + roof” plan into a wiring diagram, annotates each box with a contract (a safety requirement), and then composes those contracts into a single system-level predicate that must hold.

Contracts = relations (predicates) Wiring diagram = composition syntax Algebra maps diagrams → composite constraints Interactive scenario checker
Click a box to see its contract. Use “Try a Scenario” to watch wires turn green/red. S (design load, kN) Cap_R (roof cap., kN) Code_R (roof code?) Cap_W (wall cap., kN) Code_W (wall code?) Roof subsystem Behaviour: computes reaction r to wall Contract C_R (safety) Code_R ∧ Cap_R ≥ γ_R·S r = S ∧ ok_R = ⊤ Wall subsystem Behaviour: checks support of roof reaction Contract C_W (safety) Code_W ∧ Cap_W ≥ γ_W·r ok_W = ⊤ AND ok = ok_R ∧ ok_W C_∧ Output ok_S (shell safe?) r=? ok_R=? ok_W=? ok_S=?
Input/resource/value wires
Internal signal wires
Wire consistent with contracts
Contract violation along that connection

Agent reading guide

To ground this example in the cited theory, focus your reading on:

  • Contracts as relations: a contract on a box \(X\) is a subset \(R \subseteq X_{in}\times X_{out}\), i.e. a predicate on input/output pairs.
  • Contracts form an algebra: a functorial mechanism that takes a wiring diagram and “pushes” internal contracts to a composite external contract.
  • Composition = existential elimination: internal wires disappear from the external view, so the composite predicate quantifies over them.

In the Formalism tab we write the generic rule and then instantiate it for wall+roof.

What you are seeing

This wiring diagram is the syntax (how subsystems connect). The contracts are the semantics (what must be true).

Wire colours indicate roles or the current check result, not exact types. The signatures distinguish nonnegative real values from Boolean values; a green wire means the selected toy predicate holds, not that a physical handoff is approved.

In operad language: a wiring diagram is a multi-input “arrangement” of inner boxes into an outer box, and an algebra evaluates that arrangement. In our case, the evaluation produces a predicate (a set of allowed I/O pairs).

C(f)(C_R × C_W × C_∧) = C_shell (where f is the wiring diagram)

Roof safety contract \(C_R\)

Safety requirement: the roof must (i) pass code checks, and (ii) have capacity ≥ safety factor × design load. It also computes the reaction \(r\) that the wall must carry.

Types: X_R,in = ℝ≥0 × ℝ≥0 × Bool (S, Cap_R, Code_R) X_R,out = ℝ≥0 × Bool (r, ok_R) Contract (predicate form): P_R(S, Cap_R, Code_R; r, ok_R) :⇔ Code_R = ⊤ ∧ r = S ∧ Cap_R ≥ γ_R · S ∧ ok_R = ⊤ "Maximum load" implied: S ≤ Cap_R / γ_R

Wall safety contract \(C_W\)

Safety requirement: the wall must (i) pass code checks, and (ii) support the roof reaction load \(r\) with margin.

Types: X_W,in = ℝ≥0 × ℝ≥0 × Bool (r, Cap_W, Code_W) X_W,out = Bool (ok_W) Contract: P_W(r, Cap_W, Code_W; ok_W) :⇔ Code_W = ⊤ ∧ Cap_W ≥ γ_W · r ∧ ok_W = ⊤ "Maximum reaction" implied: r ≤ Cap_W / γ_W

Combiner contract \(C_{\wedge}\)

This box is just the “system verdict”: it turns two booleans into one. (You can treat this as “reporting” the outcome, or as a tiny behavioural model.)

Types: X_∧,in = Bool × Bool (ok_R, ok_W) X_∧,out = Bool (ok_S) Contract: P_∧(ok_R, ok_W; ok_S) :⇔ ok_S = (ok_R ∧ ok_W)

System-level meaning

When you connect roof → wall, the intermediate wire \(r\) becomes “internal”. So the system-level contract talks only about external inputs and outputs: it existentially quantifies over internal values.

That’s exactly the “contracts algebra” idea: a wiring diagram plus component contracts determines a composite contract.

1) Contracts as an algebra over wiring diagrams

A static contract on a box \(X\) is a relation \(R \subseteq X_{in}\times X_{out}\), i.e. a predicate \(P_X(x_{in},x_{out})\). A wiring diagram tells you how inner boxes are connected inside an outer box.

Given a wiring diagram f : X → Y in the wiring-diagram category W, and a contract R_X ⊆ X_in × X_out, the contracts algebra produces a composite contract: R_Y = C(f)(R_X) ⊆ Y_in × Y_out Membership / predicate view: (y_in, y_out) ∈ R_Y ⇔ ∃ x_out : ( f_in(x_out, y_in), x_out ) ∈ R_X ∧ f_out(x_out) = y_out Read this as: "there exists an internal behaviour on hidden wires that makes all component constraints true."

This generic formula belongs to a wiring category that can express feedback; it is not a definition of the narrower acyclic, one-attachment-per-port syntax used in the current resource essay. The example below uses an acyclic connection and computes the existential elimination explicitly. Here “contract” means a static allowed relation, not a separately established assume–guarantee calculus.

2) Instantiating the rule for the wall+roof wiring diagram

Let the outer system (the “shell”) have external inputs \((S, Cap_R, Code_R, Cap_W, Code_W)\) and external output \((ok_S)\). The internal wires are \(r\), \(ok_R\), \(ok_W\).

Component predicates: P_R(S, Cap_R, Code_R; r, ok_R) :⇔ Code_R ∧ (r=S) ∧ (Cap_R ≥ γ_R·S) ∧ (ok_R=⊤) P_W(r, Cap_W, Code_W; ok_W) :⇔ Code_W ∧ (Cap_W ≥ γ_W·r) ∧ (ok_W=⊤) P_∧(ok_R, ok_W; ok_S) :⇔ ok_S = (ok_R ∧ ok_W) Composite predicate produced by the contracts algebra: P_shell(S, Cap_R, Code_R, Cap_W, Code_W; ok_S) :⇔ ∃ r, ok_R, ok_W : P_R(S, Cap_R, Code_R; r, ok_R) ∧ P_W(r, Cap_W, Code_W; ok_W) ∧ P_∧(ok_R, ok_W; ok_S)
Because P_R forces r = S and ok_R = ⊤, and P_W forces ok_W = ⊤, we can simplify: P_shell(...) ⇔ (Code_R = ⊤) ∧ (Code_W = ⊤) ∧ (Cap_R ≥ γ_R·S) ∧ (Cap_W ≥ γ_W·S) ∧ (ok_S = ⊤) Equivalently, in "maximum load" form: S ≤ min( Cap_R/γ_R , Cap_W/γ_W ) and both code checks are true.

This is the promised “diagram → predicate” mapping: the wiring determines which internal variables are existentially eliminated.

3) Composing contracts with behaviour

To demonstrate composition with system behaviour, we use a simple deterministic behaviour model: the roof sets \(r := S\); the “ok” booleans compute from the inequalities and code flags; and the system ok is an AND.

Behaviour (toy, deterministic): r := S ok_R := Code_R ∧ (Cap_R ≥ γ_R·S) ok_W := Code_W ∧ (Cap_W ≥ γ_W·r) ok_S := ok_R ∧ ok_W Safety as contracts demands ok_R = ⊤ and ok_W = ⊤ (not merely computed). So the composed system satisfies the composed contract exactly when: Code_R ∧ Code_W ∧ (Cap_R ≥ γ_R·S) ∧ (Cap_W ≥ γ_W·S) i.e., when the behaviour outputs land in the allowed relation.

Inputs (external wires)

As you change inputs, the diagram overlays update: reaction \(r\), booleans \(ok_R, ok_W, ok_S\), and wire colors.

Outputs + contract checks

Computed reaction
r = 80 kN
Max roof load
Cap_R/γ_R = 93.3 kN
Max wall load
Cap_W/γ_W = 146.7 kN
Overall max load
min(...) = 93.3 kN
Roof contract \(C_R\)
Cap_R ≥ γ_R·S and Code_R
?
Wall contract \(C_W\)
Cap_W ≥ γ_W·r and Code_W
?
Composite contract \(C_{shell}\)
Existentially eliminate internal wires
?

Composite predicate (live)

P_shell ⇔ Code_R ∧ Code_W ∧ (Cap_R ≥ γ_R·S) ∧ (Cap_W ≥ γ_W·S) ∧ (ok_S=⊤)

This is the “contracts algebra output”: the wiring diagram plus component contracts yields a single checkable condition.