Promise Algebra: An Algebraic Model of Non-Deterministic Computations

Our goal is to define an algebraic language for reasoning about non-deterministic computations. Towards this goal, we introduce an algebra of string-to-string transductions. Specifically, it is an algebra of partial functions on words over the alphabet of relational $τ$-structures over the same domain. The algebra has a two-level syntax, and thus, two parameters to control its expressive power. The top level defines algebraic expressions, and the bottom level specifies atomic transitions. History-dependent Choice functions resolve atomic non-determinism, and make general relations functional. Equivalence classes of such functions serve as certificates for computational problems specified by algebraic terms. The algebra has an equivalent syntax in the form of a Dynamic Logic, where terms describing computational processes or programs appear inside the modalities. We define a simple secondary logic for representing atomic transitions, which is a modification of conjunctive queries. With this logic, the algebra can represent both reachability and counting examples, which is not possible in Datalog. We analyze the data complexity of this logic, measured in the size of the input structure, and show that a restricted fragment of the logic captures the complexity class NP. The logic can be viewed as a database query language, where atomic propagations are separated from control.