Statebox Language Primer
This is an early working version of the Statebox language primer which describes the related mathematical formalisms and capabilities of the language.
The advantages of modelling out a process using Statebox tooling, namely Petri nets, are the following:
- we can guarantee that the process does not enter illegal states
- it allows for easier integration with other platforms such as blockchains and cloud hosting solutions
- it manages logic which otherwise has to be managed elsewhere, typically via code implementation which doesn’t have the guarantees derived from Petri nets with additional structure imposed by category theory.
Formalisms Used in Statebox
Below is a brief summary of the different mathematical concepts used in the Statebox language, necessary for a thorough understanding of how the language functions.
Wikipedia: “A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic systems. A Petri net is a directed bipartite graph, in which the nodes represent transitions (i.e. events that may occur, represented by bars) and places (i.e. conditions, represented by circles). The directed arcs describe which places are pre- and/or postconditions for which transitions (signified by arrows). Some sources state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes.”
Statebox has a special “flavor” of Petri nets as described in the monograph. A notable difference is that Statebox nets allow one to mathematically reason about “firing transitions” in a net, as opposed to only static analysis which is typically practiced in the use and study of Petri nets. This is achieved via the use of Category Theory to ensure, amongst other things, compositionality, structure and behaviour of the nets.
Transitions in a net are transformations which process resources in the form of tokens living in their input place(s), and turn them into other resources in the form of tokens in their output place(s).
Transitions process tokens as pointed out above by firing. A transition firing carries a net from one state to another. In the context of a Statebox net, a message with the required data and signed by the correct key (corresponding to a user with privileges for a particular role) is processed by the Statebox engine to represent the firing of the corresponding transition, carrying the net from one state to (one of the possible) next ones.
Places can be considered “bags” which denote the type of resource they are holding. Resources of that type are represented as tokens living in that place. For instance, a place of type $A$ holding 3 tokens can be thought of as a bag holding 3 resources of type $A$. Given a place, inbound and outbound edges to/from transitions represent ways to put in/take out tokens from a place.
Tokens represent the resources that a net can process. They live in places that denote their type and are transformed into other resources by transitions, which carry them into other places.
The state of a net is given by the distribution of its tokens in the various places. Every time a transition fires, moving tokens around, the net is carried to a new state.
Wikipedia: “Category theory formalizes mathematical structure and its concepts in terms of a labeled directed graph called a category, whose nodes are called objects, and whose labelled directed edges are called arrows (or morphisms). A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. The language of category theory has been used to formalize concepts of other high-level abstractions such as sets, rings, and groups.”
The Statebox Language
This section outlines the capabilities of the language, how it ties to the formalisms mentioned in the previous section and how it is implemented.
Once the process is modelled, then in order to implement & run it, we need to further ensure that:
- we have a live bounded Petri net. Intuitively this means that the net does not jam, meaning that the net never enters into a state where no transition can fire – i.e. no further computation can happen.
- This is achieved using static analysis methods for Petri nets.
- we specify initial and final transitions of the net and their meaning.
- This is to specify how the process interacts with external systems in terms of how it is initialized and what happens once it completes in terms of passing data and making calls to other programs.
- we give type definitions for the information that is recorded when a transaction fires.
- This is important for data integrity to insure inputs and outputs are correct.
- we specify folds, they are “scans” over the history of a net-execution.
The instantiation of a process is achieved by firing a transition against the genesis block which is simply a representation of a given process (as a Petri net). Once the first transition against this genesis block is fired, a new process is created, with a unique ID, pointing back to the genesis block using a hash. The following transitions are fired against the last recorded transaction for that particular net instances which results in a structure similar to a blockchain in that every transaction is a hash of the new state of the net which points to the previous transaction.
Wikipedia: “In functional programming, fold (also termed reduce, accumulate, aggregate, compress, or inject) refers to a family of higher-order functions that analyze a recursive data structure and through use of a given combining operation, recombine the results of recursively processing its constituent parts, building up a return value.”
Folds in the Statebox system can occur in two ways:
- READ ONLY They analyze the (entire) history of the next execution and compute a value that is used in the UI or stored in an SQL data warehouse.
- AS GUARD INPUT The output of a computation could be used in a guard query, which determines a further refinement on when a transition can be fired.
Read only is not a problem, but guarded input is problematic because we cannot have Turing completeness here (or undecidability of checking some property, which is usually the result of having TC or even something much weaker). Simply speaking, we want to be sure that the computation for cheking some property always terminates. This is non-trivial to achieve in the general case.
When there is a limit for the number of tokens in one place, the nets are refered to as bounded nets. If the limit is ‘k’ for all places, then the net is called k-bounded. This means that the net has a finite reachability graph.