Anoma Resource Machine Explainer in Long Form

[kike]

Thanks for the write-up! I really like the abstraction you’ve put forward. It (almost) all makes sense to me. There are some subtle points that I’d like to bring to focus.

@graphomath

A state transition X \to Y is allowed if

• there are k pairs of disjoint simple states \langle U_1, W_1\rangle, \ldots, \langle U_k, W_k\rangle such that
  • the first components are a partition of all consumed persistables, i.e., \bigcup_{i=1}^k U_i = X \setminus Y and U_i \cap U_j = \varnothing if i\neq j;
  • the second components are a partition of the created persistables, i.e., \bigcup_{i=1}^k W_i = Y \setminus X and W_i \cap W_j = \varnothing if i\neq j;
  • the predicate P_v of every persistable v involved in some component of a pair of partitions \langle U_i, W_i\rangle is satisfied, i.e., for each i, and for each v \in U_i \cup W_i, it is the case that P_v(\langle U_i, W_i\rangle) is true.

In one phrase, a transition x \to y is allowed if its SoC can be partitioned into pairs of disjoint sets of persistables such that the logic of any involved persistable is satisfied for the partition in which it is contained. One important consequence of this definition is that we are able to batch together several consecutive but independent allowed state transitions into a single “parallel” transition such that the logics of the persistables are satisfied for the relevant portion of the SoC.

Above, a transition x \to y is defined as two partitions, one for x\backslash y, and another for y\backslash x. That is, two disjoint sequence of sets \{U_i\}_{i\leq k},\{W_i\}_{i\leq k}.

What if instead we use covers (i.e. not necessarily disjoint sequences) of x\backslash y and y\backslash x? I think they will also do the job. I mean, we can still pack independent state transitions into a “paralel” transition.

The reason for requiring partitions and not covers might be what @cwgoes said:

@cwgoes

logic scope checks are exclusive: checking a persistable in my logic scope ensures not only does that it satisfies my requirements but also that it does not satisfy other persistables’ requirements other than the ones which I allow to be included in the logic scope.

In my view, this design might be too limiting. Too limiting with respect two goals:

• Parallelization
• Tasks with preprocessing

Parallelization. The goal is to parallelize an algorithm between different nodes or threads (different logic scopes), and then pack their results into a single transaction.

There are tasks that cannot be distributed if we do not allow persistables to participate in different logic scopes. In general, the design won’t work for any problem in NC whose input is not partitioned.

For example, computing a matrix multiplication \mathbf C = \mathbf A\mathbf B can be parallelized by computing the inner product of every pair of row, column. Each row \mathbf a_i in \mathbf A participates in as many inner products as columns \mathbf b_j in \mathbf B. If you see rows and columns as persistables of kind ‘vector’, then there is no way to split n-dimensional matrix multiplication into disjoint logic scopes, each in charge of a subset of the inner products. The only possible partition we have is \langle U, W\rangle, where the consumed persistables are U = \{\mathbf a_i, \mathbf b_i\}_{i\leq n}, and the created persistables are W = \{\mathbf c_i\}_{i\leq n}. In other words, we are forced to deal with persistables of kind ‘matrix’ as a whole.

@graphomath

Given a pair of disjoint finite sets of persistables \langle U, W \rangle that contain the persistable v, its logic P_v will assign a truth value to the pair \langle U, W \rangle. More formally, we consider the logic P_v to be a Boolean valued partial function that expresses the logic of the persistable v; it is defined for every disjoint pair of sets of persistables whose union contains the persistable v, i.e., any \langle U, W \rangle such that v \in U \cup W and U \cap W = \varnothing hold.

This brings me to the second point I’d like to drawn attention to.

Tasks with preprocessing. What if we want to do reactive computations? Namely, algorithms that re-use (part of) the state without modifying it. Tasks that need some sort of pre-processing would fall into this category. To capture this type of tasks, I think the domain of the logic P_v should be X \cup Y, so we also account for X \cap Y–the unchanged portion of the state for this transition.

For example, following with linear algebra. For a given set of vectors \mathcal B = \{\mathbf v_1, \ldots, \mathbf v_n\} we’d like to check linear combinations of them, but only if the elements in \mathcal B are independent. The algorithm P is then

P(\mathcal B, \mathbf v)=\mathsf{true} \Leftrightarrow \land \begin{cases} rank \{\mathcal B\} =n, // \text{ task 1}\\ \mathbf v \in span\{\mathcal B\} // \text{ task 2} \end{cases}

We could first prove the n vectors in \mathcal B are independent, and add them to the state as persistables of kind ‘linear independent vectors’ in transition X \to Y. Later on, we add vector \mathbf v to the state as a persistable of kind ‘linear dependent’, in transition Y \to Z. With the current design, we cannot re-use \mathcal B, it must be re-created, or copied, every time (and its linear independence proved in each copy).

In a related post I discussed these two notions (with different terminology). Therein, the conclusion (as I got it, @vveiln) was that we can always capture parallelization and preprocessing by passing resources as application data. Fair enough. However, it feels to me that application data is some sort of ‘miscellaneous’ category, that comes to fix anything the abstraction may miss out. I do like really your abstraction, and feel it should be able to capture more.