The delete button is a distributed systems problem

A delete button feels like a solved problem until you put the data on two computers.

Suppose I remove a paper from a reading list on my laptop. My phone is offline and still has the old list. It reconnects, sends its copy, and the paper comes back.

Taking the union of both lists sounds reasonable. Keep everything either device knows about. But that includes the thing I just deleted.

The problem is that an absent entry does not tell us why it is absent. This device might never have seen it. Or it might have seen it and deliberately removed it. Those are different histories, even when the current list looks identical.

I want a merge function that preserves that distinction.

First, decide what remove means

For an ordinary set, adding and removing the same element do not commute. Changing their order changes the result.

\begin{aligned} \operatorname{remove}_x \bigl(\operatorname{add}_x(\varnothing)\bigr) &= \varnothing \\[4pt] \operatorname{add}_x \bigl(\operatorname{remove}_x(\varnothing)\bigr) &= \{x\} \end{aligned}

That is straightforward when one computer executes the operations in order. It becomes a specification question when separate replicas perform them concurrently. Should the add win? Should the remove win? We need to choose rather than leave the answer to message arrival order. arXiv

An observed-remove set makes a specific choice. Each addition gets a unique tag. A removal targets the tagged additions that its source replica has already observed. A concurrent addition with a new, unseen tag survives. This is add-wins behavior, not a claim that every application should prefer additions. arXiv

Keep the history that matters

For this derivation, I will use a deliberately unoptimized representation.

Each replica stores two sets. A contains the tagged additions it knows about. R contains the tagged additions it knows have been removed. A tagged addition is a pair consisting of an element and its unique tag.

Nothing gets physically erased from either set in this model. The visible reading list is derived from them. This two-set representation makes the merge particularly direct. XRAPH

s = (A,R), \qquad R \subseteq A

An element is visible when at least one of its addition tags has not been removed.

\operatorname{contains}((A,R),x) \iff \exists u\, \bigl( (x,u)\in A \land (x,u)\notin R \bigr)

From that representation, we can write the local updates directly. Adding creates a fresh tag. Removing records all additions for that element known at the source.

\begin{aligned} \operatorname{add}((A,R),x,u) &= \bigl(A\cup\{(x,u)\},R\bigr) \\[6pt] \operatorname{remove}((A,R),x) &= \left( A,\, R\cup\{(x,u)\mid(x,u)\in A\} \right) \end{aligned}

The tag supplied to add must be globally unique for that addition. The removal’s observed tags must also be preserved when it is replicated. Receiving a removal is not permission to rerun remove(x) against a different, more recent view of the world. arXiv

The slightly strange part is that deleting something from the visible set adds information to the stored state.

We are not forgetting the addition. We are remembering its removal.

The merge is two unions

Now the equation becomes small.

\boxed{ (A_1,R_1)\sqcup(A_2,R_2) = \bigl(A_1\cup A_2,\;R_1\cup R_2\bigr) }

Combine the known additions. Combine the known removals. Then compute visibility from the result.

For this representation, the merge inherits three properties from set union.

\begin{aligned} s\sqcup t &=t\sqcup s &&\text{commutativity} \\[4pt] (s\sqcup t)\sqcup v &=s\sqcup(t\sqcup v) &&\text{associativity} \\[4pt] s\sqcup s &=s &&\text{idempotence} \end{aligned}

Swapping the inputs does not matter. Regrouping merges does not matter. Receiving the same state twice does not change the answer.

There is another condition hiding underneath those equations. Local updates must preserve accumulated information. Ours do, because both sets only grow. Together, monotonic state updates and a merge that computes a least upper bound are the basis of the state-based CRDT approach. UMinho Web Archive

For our model, the convergence argument is direct. Replicas that have incorporated the same additions and removal records have the same sets, so they produce the same reading list. If updates stop and state exchanges eventually carry every update to every replica, all replicas reach that result.

The merge tolerates reordered and duplicate state deliveries. It cannot compensate for information that never arrives.

Now make the sets functions

Writing a lambda in front of the union equation would be easy. I want to go a little further and encode the merge itself.

For the lambda-calculus version, represent a set by a membership function. Give it a tagged element, and it returns true or false.

Those booleans can be functions too. A Church boolean chooses between two arguments. True chooses the first; false chooses the second. The names below are abbreviations for lambda terms, not built-in values. Cornell Computer Science

\begin{aligned} \mathsf{T} &\coloneqq \lambda a.\,\lambda b.\,a \\[4pt] \mathsf{F} &\coloneqq \lambda a.\,\lambda b.\,b \\[4pt] \mathsf{or} &\coloneqq \lambda p.\,\lambda q.\, p\,\mathsf{T}\,q \end{aligned}

The last definition says that if the first boolean is true, return true. Otherwise, return the second boolean.

Now union is a function that accepts two membership functions and produces another one.

\boxed{ \mathsf{union} \coloneqq \lambda a.\,\lambda b.\,\lambda z.\, \mathsf{or}\,(a\,z)\,(b\,z) }

Read it from the inside out.

Ask whether z belongs to the first set. Ask whether it belongs to the second. Return true when either answer is true.

Here, z is a tagged addition, not just the paper itself. That distinction is what lets the model remove one addition without erasing a different, concurrent one.

We have replaced union with function application and boolean selection.

Make the state a function too

Our replica state still looks like a pair of sets. We can encode the pair without introducing a built-in tuple.

A Church pair stores two values by waiting for a function that knows how to consume them. Its projections select the first or second value. UCSD PL

\begin{aligned} \mathsf{pair} &\coloneqq \lambda a.\,\lambda b.\,\lambda k.\, k\,a\,b \\[4pt] \mathsf{fst} &\coloneqq \lambda p.\,p\,\mathsf{T} \\[4pt] \mathsf{snd} &\coloneqq \lambda p.\,p\,\mathsf{F} \end{aligned}

For our replica, the first value is the additions predicate. The second is the removals predicate.

That gives us the lambda-calculus version of the merge.

\boxed{ \begin{aligned} \mathsf{merge} \coloneqq {}& \lambda s.\,\lambda t.\, \mathsf{pair} \\ &\quad \bigl( \mathsf{union}\, (\mathsf{fst}\,s)\, (\mathsf{fst}\,t) \bigr) \\ &\quad \bigl( \mathsf{union}\, (\mathsf{snd}\,s)\, (\mathsf{snd}\,t) \bigr) \end{aligned} }

Take two states. Extract their additions and merge them. Extract their removals and merge those. Return a new state containing both results.

Every named operation in that expression has a lambda definition above. Expanding those definitions leaves only variables, function abstraction, and function application.

This is not a new distributed algorithm. It is an encoding of the merge we already specified.

Check what the function actually computes

Pick any tagged addition z. Ask whether it belongs to the additions component of the merged state.

Substituting the definitions gives the following reduction.

\begin{aligned} &(\mathsf{fst}\, (\mathsf{merge}\,s\,t))\,z \\[4pt] &\quad\xrightarrow{\beta^{*}} \mathsf{or}\, \bigl((\mathsf{fst}\,s)\,z\bigr)\, \bigl((\mathsf{fst}\,t)\,z\bigr) \end{aligned}

The beta-star arrow means a sequence of beta reductions, each substituting an argument into a function body. Cornell Computer Science

The result is exactly the membership rule for union. The merged additions contain z if either input’s additions contain it. The same reduction works for the removals component.

The convergence properties have not changed. We have changed the representation.

For these encoded sets, equality means that their predicates give the same membership answers for every tagged element. It does not mean the functions must have identical source text.

An old copy is not a new addition

Return to the reading list.

Both devices initially know about a paper added with tag α. The laptop removes it. Meanwhile, the phone performs a new addition of the same paper with a fresh tag β, without seeing the laptop’s removal.

Call the paper p. The two states are now:

\begin{aligned} s_{\mathrm{laptop}} &= \bigl( \{(p,\alpha)\}, \{(p,\alpha)\} \bigr) \\[6pt] s_{\mathrm{phone}} &= \bigl( \{(p,\alpha),(p,\beta)\}, \varnothing \bigr) \end{aligned}

Applying our merge gives:

s_{\mathrm{laptop}} \sqcup s_{\mathrm{phone}} = \bigl( \{(p,\alpha),(p,\beta)\}, \{(p,\alpha)\} \bigr)

The paper is visible because β has not been removed.

Now change one detail. Suppose the phone never made that new addition. It only returned with its old copy containing α.

Then the merged state contains α in both the additions and removals sets. There is no surviving tag. The paper stays deleted.

That is the distinction I wanted. A stale copy does not resurrect an observed removal. A genuinely concurrent addition survives under the rule we chose.

Both replicas can compute that answer without choosing a global order for every update.

What this does not buy us

I would not use nested membership functions as the storage format for an actual service. They make the algebra visible, but this derivation does not implement tag generation, persistence, network transport, or enumeration of stored elements.

The history also has a cost. Our simple representation keeps accumulating additions and removal records. Reducing that metadata requires preserving enough causal information to distinguish an unseen addition from a known removal. Optimized OR-set designs address this bookkeeping; simply throwing away deletion records is not equivalent. CMI

And convergence is not linearizability. This does not make every read immediately reflect every completed update, or turn the set into a consensus protocol. It gives us a deterministic way to reconcile replicas under the specified concurrency semantics. arXiv

That is what I like about this example.

The lambda expression is not doing anything mysterious. It combines two pairs of predicates. The difficult decision happened earlier, when we chose what the state needed to remember.

A delete button asks for something to disappear. Making that work across replicas may require remembering more, not less.