Controllers and Solvers in the Abstract

Solvers
, ,
1

Controllers and Solvers in the Abstract

The aim of this post is to describe the minimal general shape of a solver-controller architecture, as well as the two primary ways in which controllers can interact under such a system, with discussion of the elements involved and the reason as to their involvement.

Background

First of all, a follow-up on Why Does PROLOG Resist Distribution?. @graphomath was quite correct, naturally, to point out the CALM principle’s relevance to this problem. For those who want a simple introduction to the principle, the bloom folk have a good page on the topic calm: consistency as logical monotonicity | Bloom Programming Language. Something missing from this description, however, is the topic of convergence. I believe that Rich Hickey’s favourite paper is correct https://curtclifton.net/papers/MoseleyMarks06a.pdf to be so adamant about the disentanglement of functional and relational concerns, for two core reasons, and this is something that the bloom people have also considered.

Why? Firstly, if the order of execution and in which events are triggered matters within a transaction, then we cannot guarantee that race conditions will be avoided without coordination. This is why in datalog, order of execution within a transaction does not matter, hence the emphasis on sets. Time will, otherwise, be left outside of the data, and time is in fact a form of state.

This seemingly innocuous occurrence can actually significantly compli-
cate the process of informal reasoning. This is because the person reading
the code above must effectively duplicate the work of the hypothetical com-
piler — they must (by virtue of the definition of the language semantics)
start with the assumption that the ordering specified is significant, and then
by further inspection determine that it is not (in cases less trivial than the
one above determining this can become very dicult). The problem here
is that mistakes in this determination can lead to the introduction of very
subtle and hard-to-find bugs.

More generally, conflation of functional and relational concerns makes it very hard to reason intensionally about the system. Bloom, for the most part, despite some issues I have with it, works quite well for the purposes of this separation in a distributed setting and in my opinion should be understood as possessing the correct model for any kind of distributed, monotonic architecture. The way Bloom essentially works is that controllers define event rules which trigger on receiving events, and also may perform other triggers, crucially in a disorderly fashion (results are always sets). Here is an example of the Raft protocol implemented within Bloom, which I think gives a good indication of its expressive power and limits GitHub - noeleo/raft: An implementation of the Raft consensus algorithm in Bloom..

Note, Bloom is fundamentally an extensional system. Although, as in SQL, it is capable of returning sets of all possible results, and though it is true that one can provide the general shape of a query up-front, certain things cannot be defined within datalog. This is a consequence of the guarantee that datalog will eventually reach a fixed point (please see Three Popular Resolution Strategies).

For example, in PROLOG I can define factorial as two ordered clauses and find arbitrary solutions thereby without anything more- but datalog, being not turing complete, must provide cannot infer solutions past what follows from applying rules/facts it already knows about repeatedly. Obviously, I won’t want to use something non-turing complete locally, and that’s why the functional-relational split exists.

(PS: I also think there is room to improve Bloom even on its own terms. For example, I cannot dynamically reconfigure or introspect on said triggers/rules and pass them around, which is sad.)

Minimal Shape of a Solver-Controller Architecture

With this split understood, we may imagine two different kinds of principled interaction between two or more controllers which differ based on how the controllers organise themselves. @apriori’s mention of Cosmos inspired this abstraction.

Suppose that each controller has its own domain over which it has total, turing-complete control.

Figure 1
Figure 11669×816 77.3 KB

The green arrows here represent negotation via consensus, with event-handling operated via a datalog-like communication protocol. For example, C2 could use a consensus mechanism to plan a transaction and negotiate with other controllers C3 & C1 directly to figure out how it ought to be resolved, provided those controllers have some defined rules which can handle those transactions. One could imagine that, supposing a given green transaction succeeds, that it triggers some post-transactional code that is turing complete. This could be done via a separate mechanism, such as the event broker.

The red arrows represent solver-dependencies. A controller which has one or more solver-dependents I term a solver. When controllers ‘subscribe’ to a solver, they are giving the solver permissions to, in a turing complete manner, read and propose changes to certain resources. Internally within the solver, The solver may choose a few different methods by which it can attempt to solve the intents of its subscribers. Note that intents are ephemeral and only exist within the context of the solver.

For the record, I have been made aware that an existing idea was to have solvers subscribe to the pools or controllers. I think this language is the wrong way around, since the solver acts in this sense as a court which its controllers may or may not acquiesce to. The solver would know about and have a representation of resources which the controllers permit consideration of.

However, I think the general correct shape of how solving is done would ideally look similar to an XSB-like tabling protocol, in which the known resources of subscribers would be represented internally with tables, and intent resources which await resolution could have computation suspended within a strongly-connected component which describes the specifications for tables the computation depends upon (how and when suspension is lifted may be up to the particular solver). This would allow the solver to propose changes by updating these tables, and then when it has converged on a solution, it can send out this information via the datalog-like messaging protocol (what would be nice about having this is that the terms to this protocol could have semantic meaning in the turing-complete language), and cut the result to commit. The users of course, would need to confirm the acceptability of the transaction.

This would guarantee that any situation in which the order of execution matters would take place within a local context. Consequently, this would allow users to perform basic, monotonic constraint processing amongst themselves, and/or compose transactions with other users. More interesting search interactions would require the help of a solver. Important to note from the diagram is that solvers can depend on solvers, and that controllers can subscribe to many solvers. This should be safe due to the fact that a given solving context is only a ‘proposal’ and that the transaction would be executed in a CALM manner, so there is not necessarily any contradiction with, for example, two solvers depending on one another, under an optimistic concurrency model.

If we view it in this way, Anoma-Level would/should seek to provide all three of the following in an integrated fashion:

  • Object orientation for live dynamism
  • Support for different kinds of solving through this hierarchical search tree
  • Distributed-Datalog-esque transactions.

Thanks to @Jamie for inspiring this post in light of recent discussions.

4 Likes
A Roadmap for AL
2

Do you really, though? I tend to think that wherever Turing can be kept out, he should be. Even your factorial example is primitive recursive; more generally, “process N things” is usually sub-Turing, just often hard to prove (counting mangling into a sub-Turing language as a form of proof). Datalog’s even better at factorials than, say, Haskell because it remembers the factorial facts it’s learned.

More broadly, the more places we can guarantee Turing-incompleteness without putting program authors through hell, the sounder the system is against weird behaviors.

2 Likes
3

I think you make a good point here. datalog is not The Only DSL in Existence and there are often cases where exposing a DSL makes more sense for various reasons. Moreover, I actually find it less annoying in general to learn lots of small DSLs than figure out the structure of an unbounded program.

In the factorial example though if I am a general user datalog won’t cut it since it can’t solve factorials in general outside of specified finite domains.

Also there’s something to be said for “helping the expert user break the system” since it can become opaque over how to do that in a case where we have a lot of DSLs interacting.

4

Well, more broadly, we wade through the Turing tarpit constantly because we want to write a lot of things that look like

while (!processing_done()) {
  do_processing();
}

which don’t come with a proof that processing will eventually be done, or even that our predicate for deciding if it’s done will have an answer, and then scaffold it defensively against the Turing demons forever.

But this is a bug (the bug? the only bug that exists?) because it is exceptionally rare for real problems to be unbounded; the actual infinite loops we see in useful practice are not computational infinite loops, they’re user interface loops. We are just too dumb as human beings to actually write these proofs most of the time, so we live with the bug.

Sometimes, however, our domain is nice to us. Maybe we can write the predicate for deciding if work is done in a total language and furthermore find a bound on the number of work units we’ll process. I think this is actually possible quite often. It’s possible in Anoma (I contend).

This pseudo-Datalog is acceptable, I think (it’s not really my thing):

factorial(0, 1).
factorial(n, n * prev_factorial) :-
  n > 0,
  factorial(n - 1, prev_factorial),
  factorial_input(n).

factorial_input(0).
factorial_input(n - 1) :-
  n > 0,
  factorial_input(n).

and then we “call” by making factorial_input(whatever) true and querying, which is different from a functional programming “function call” but not in ways that bother me, you just need to have a number before you have its factorial, which is also true of the “function call”.

But the proof is really easy for this function, even if we’re used to wielding the nuclear weapon of unrestricted recursion on it because it’s close at hand. We don’t even explicitly write the equivalent of a processing_done predicate because we just do the one arithmetic operation right there. Usually it’s a lot harder. But I’m still optimistic wrt Anoma.

5

I think I’m generally comprehending your point, which is that if you don’t care about infinite domains you can utilise certain methods to avoid requiring computational loops. I think you’re right to want to avoid it where possible. However, this only really applies to exploratory cases. In a solver I don’t necessarily know what the boundaries of my domain are. If constraint processing over finite domains are all we need then great we just ended computer science forever- but that’s not the case for a solver. But there are many pl it is best. For example in transaction planning I benefit from providing the minimal info I can and so I just discount stupid things and guarantee termination which is great. But negotiating on it for instance isn’t just a user interface loop. I am considering possibilities that may be wrong and the conflicts for which can’t be known upfront which is a search without explicit boundaries

1 Like