Hacker News new | ask | show | jobs
by sbazerque 656 days ago
> A program P is monotonic if for any input sets S,T where S ⊆ T, P(S) ⊆ P(T).

> A program is monotonic if, when you run it on a subset of its inputs, you get a subset of its outputs. As you run it on more data, the set of true things may grow, but it never shrinks.

Yeah, this framework seems powerful.

Something I find interesting is that you can get monotonic (and therefore coordination-free) relaxations of arbitrary problems. In extremis, you can derive a relaxed version P' thus

P'(S) = {<s, P(s)> | s ⊆ S}

and now

P'(S) ⊆ P'(T) if S ⊆ T for _any_ (well defined) P

This seems tautological but in some cases a relaxed version is good enough: it gives you convergence and eventual consistency in a coordination-free setting, at the cost of maybe having to roll back some results. And when it doesn't, it gives you a coherent model of what to make of the situation until coordination yields a definitive answer.

I wrote about this idea here: https://www.hyperhyperspace.org/report.html#conflict-resolut...

But that was like last week, haven't really put this in practice yet.

In those examples what is being processed are partially-ordered operational logs, but it's essentially the same (just that whenever S ⊆ T there, what you're seeing is an extension of an op log, which is a bit more intuitive).

1 comments

This boils down to materalizing every possible nondeterministic outcome. I wouldn't call anything that involves a power set with 2^n space complexity "relaxed" tbh ^^'. While I do agree with the general sentiment, I do still think that going with states that can be reconciled/merged is a more realistic approach, than just wildy diverging.
This is a great submission.

The logic for taming unbounded nondeterminism has been around for decades though. As Dijkstra and Scholten admit, it’s basically just applied lattice theory.

In fact, at a glance, this paper appears to be building on that foundation. It’s not hard to see how monotonicity makes reasoning about nondeterminism considerably more manageable!

Did you read the remark at the end of my comment? In the practical cases I was exploring, that combinatorial explosion does not happen. It's relaxed in the sense that it is coordination-free.
Not sure what you mean.

I'm talking about the "relaxed" P' being defined via the power set of S.

2^S= {s | s ⊆ S}

Now if all your P is only a mapping then

P'(S) = {<s, P(s)> | s ∈ S}

but then your "coordination free" P was monotonic anyways.