> The algebra of semilattices has a single operator: join. Notably it doesn't have any operator that corresponds to read or inspect. In fact, CRDTs as described in the literature provide absolutely no guarantees to readers, so a "proper" CRDT implementation should not allow reads!
Perhaps a proper mathematician can weigh in, but for a layman like me this assertion makes no sense at all.
A join-semilattice is a class of set characterized by a specific type of order and the support for an operation. If you add additional operations, it just further specializes the type of join semilattice. It's properties stay the same, and you just add more of them.
Also, there is nothing in a set that prevents it from verifying membership of said set.
Nevertheless, let's entertain the idea and assume that formally you could not verify membership of a set as it would imply loss of correctness. Let's entertain that idea.
In practical terms this point would be moot. You could simply copy the current state of a set after each join, call it a realization of the CRDT set or something of the sort, treat it as a snapshot of the CRDT, and keep the original CRDT as a data structure that just supports a join. This realization of the CRDT does not need to be bound to any formal constraint enforced on the CRDT.
motorest•8mo ago
Perhaps a proper mathematician can weigh in, but for a layman like me this assertion makes no sense at all.
A join-semilattice is a class of set characterized by a specific type of order and the support for an operation. If you add additional operations, it just further specializes the type of join semilattice. It's properties stay the same, and you just add more of them.
Also, there is nothing in a set that prevents it from verifying membership of said set.
Nevertheless, let's entertain the idea and assume that formally you could not verify membership of a set as it would imply loss of correctness. Let's entertain that idea.
In practical terms this point would be moot. You could simply copy the current state of a set after each join, call it a realization of the CRDT set or something of the sort, treat it as a snapshot of the CRDT, and keep the original CRDT as a data structure that just supports a join. This realization of the CRDT does not need to be bound to any formal constraint enforced on the CRDT.
But that would be silly, wouldn't it?