Reading Pulpit — Euclid

Sugya · Text (with lemmas)

focus: Kan square interactive lemmas

Reading pulpit

A staged text with programmable margins. The center speaks, the margins test, the inspector certifies.

              Let
              
                (S, ⊔)
                [L]
              
              be a join-semilattice. A state-based CRDT is a monotone system: every update moves upward.
            

              Define merge
              
                merge : S × S → S
                [M]
              
              by join. The algebra is commutative, associative, idempotent:
              merge(x, y) = x ⊔ y.
            

              Let
              
                δ : S → S
                [Δ]
              
              be a delta generator. Deltas are partial joins that preserve convergence with smaller payloads.
            

              Operation-based CRDTs expose a log
              
                Log(Ops)
                [Log]
              
              ordered by causality
              
                (→)
                [C]
              ;
              applying the log is a fold over a commutative monoid.
            

              In lambda calculus, merge is executable:
              
                merge = λx.λy. join(x,y)
                [λ]
              .
              The equation is the contract, the program is the proof.
            

              API boundaries declare obligations:
              
                Promise/Obligation
                [API]
              ,
              then adjunctions explain the UI switch:
              
                Lan = expand
                [Lan]
              
              and
              
                Ran = filter
                [Ran]
              .
              The user toggles between free construction and invariant projection.
            

              Canonical CRDTs anchor the playbook:
              
                OR-Set
                [OR]
              ,
              
                PN-Counter
                [PN]
              ,
              
                LWW-Register
                [LWW]
              ,
              and
              
                Vector Clocks
                [VV]
              .
              Each has a distinct merge law and boundary contract.
            

              The practical output: a replica protocol
              
                Sync/Apply/Replay
                [P]
              
              that is safe under reordering, tolerates loss, and keeps invariants explicit.
            

Reading rule: click a lemma token ([L],[M],[Δ],[Log],[λ]...) to light up its linked marginalia and open the inspector.

Method: algebra → merge law → executable proof.

Bridge: CRDTs provide the algebra, lambda calculus makes it executable, and adjunctions explain the UI switch between expansion and filtering.

See: CRDTs lesson and Adjunctions.

Worked example: Two replicas track a set. Replica A has {a,b}, Replica B has {b,c}. Merge via join = union.

Now apply an inflationary delta Δ = {d}. The new state is {a,b,c,d}. This is monotone and idempotent.

CRDT playbook: OR-Set uses tagged add/remove; PN-Counter tracks separate inc/dec; LWW-Register resolves by timestamp; Vector Clocks certify causality.

Each entry below has a contract and a counterexample note so API obligations stay visible.

Pragmatic checklist: Choose the lattice, define merge, prove inflation, choose transport (state vs delta vs log), then bind the API.

If you cannot name the invariant, you cannot enforce it. Surface the proof in the protocol.

Walkthrough run: Replica B sends Δb with deps [a1]. Replica A has not seen a1, so it queues Δb.

Sync: A requests a1. Apply: once a1 arrives, A merges a1 then Δb. Replay: A replays queued deltas. Invariant holds.

Seven perspectives for distributed page construction: Treat each as a distinct lens with its own apparatus and techniques.

Build graph (DAG + topological order), Dataflow (streams + backpressure), Consistency (lattices + CRDTs), Security (capability policy + proofs), UX (attention + progressive disclosure), Observability (traces + invariants), Deployment (provenance + reproducibility).

Exercise P · CRDT merge

practice

Given two replicas with state sets A={a,b} and B={b,c}, compute merge(A,B) and show idempotence.

Exercise Q · Causal log fold

practice

Given ops o1 → o3 and o2 concurrent with both, list valid application orders and show convergence.

Exercise R · OR-Set remove

practice

Replica A adds x with tag a1. Replica B adds x with tag b1. A removes x after seeing a1 only. What remains after merge? Explain why tombstones are needed.

Exercise S · PN-Counter merge

practice

P=(2,1), N=(0,3) at replica A. P=(1,4), N=(2,1) at replica B. Compute merged value.

Checklist · CRDT loop

checklist

1) Identify lattice. 2) Define merge. 3) Choose delta or ops. 4) Show convergence.

Walkthrough · Lambda merge

walk

Define merge = λx.λy. join(x,y). Evaluate on two concrete states and track the resulting join.

API boundary · State vs delta

contract

Promise: server accepts either full state or delta. Obligation: delta must be inflationary.

Example

POST /merge {state:S} or {delta:Δ} → returns state S' with S ⊑ S'

Protocol sketch · Sync/Apply/Replay

protocol

Sync: send delta + deps. Apply: gate on deps then merge. Replay: fill missing ops.

Walkthrough · Causal gap repair

walk

Δb depends on a1. Queue Δb, fetch a1, merge a1, then replay Δb. No divergence, no dropped update.

Interactive · Protocol demo

interactive

Click the buttons to emit protocol events into the ribbon and observe the state update.

State: idle

Queue: 0 · Deps: none

These actions update the event ribbon and inspector immediately.

Perspective · Build graph

architecture

Apparatus: DAG of assets, edges as dependencies. Techniques: topological build, cache keys, partial rebuilds.

Perspective · Dataflow

systems

Apparatus: streams + backpressure. Techniques: windowed updates, debouncing, streaming renders.

Perspective · Consistency

crdt

Apparatus: lattices and CRDTs. Techniques: delta sync, causal metadata, merge-law tests.

Perspective · Security

policy

Apparatus: capability policies, proof-carrying updates. Techniques: signed artifacts, allowlists, proof checks.

Perspective · UX control

design

Apparatus: attention model + progressive disclosure. Techniques: staged reveal, focus+context, reduced motion.

Perspective · Observability

trace

Apparatus: event traces + invariants. Techniques: structured logs, inspector views, replayable timelines.

Perspective · Deployment

ops

Apparatus: provenance + reproducibility. Techniques: content hashes, status beacons, deterministic builds.

Counterexample · Non-commutative ops

counterexample

If op1 ∘ op2 ≠ op2 ∘ op1, replicas disagree when delivery order swaps. Fix by CRDT design or enforce order.

Playbook · OR-Set obligations

contract

Promise: adds carry unique tags. Obligation: remove only clears tags it observed.

Playbook · PN-Counter obligations

contract

Promise: increments and decrements tracked separately. Obligation: merge by componentwise max.

Playbook · LWW-Register obligations

contract

Promise: timestamp monotonic per replica. Obligation: resolve ties deterministically.

Invariant · Join monotonicity

invariant

For all x,y: x ⊑ merge(x,y) and y ⊑ merge(x,y). Violations imply non-convergent replicas.

Counterexample · Non-idempotent merge

counterexample

If merge(x,x) ≠ x (e.g., merge increments a counter), repeated delivery diverges. Must be rejected.

Dependent type · Inflationary delta

type

Type idea: Delta(s) : { d : S | s ⊑ merge(s,d) }. The API only accepts deltas certified to be inflationary.

Related Notes