nLab nondeterministic computation

Contents

Context

Computation

Idea
Formalizations

Via indefiniteness-effects

Examples

Quantum computation
Differential linear logic

Related concepts
References

Idea

Broadly speaking nondeterministic computations/algorithms are those whose outcome is indefinite, or else dependent on parameters that are not known or specified when the computation/algorithm is laid out (they may become known at “runtime”).

Beware that in complexity theory, at least, by a “non-determinstic algorithm” one really refers instead (or more specifically) to the shortest path that a non-deterministic machine could potentially take to arrive at a desired result (cf. the NIST entry). This is the sense in which “non-determinism” appears for instance in the name of the complexity class “NP” .

(…)

Formalizations

Via indefiniteness-effects

A basic programming language-model of non-determinism is via dependence of a program on an unspecified parameter $b \colon B$ , whose value is indefinite but imagined to become known at execution time – say via user input, or by observing the actual value of a random variable in an experiment and/or by making a measurement of a stochastic process or a quantum measurement of a quantum state (see below).

In this model, a non-deterministic program taking input data of data type $D$ and producing output data of nominal type $D'$ would be an actual (determinstic) program of the form

prog \;\colon\; D \longrightarrow \big( B \to D' \big) \,,

whose de facto output data type is not $D'$ but the function type $B \to D'$ . This means that the $D'$ -result of computing $prog(d)$ for any $d \colon D$ remains “un-determined” or “indefinite” unless and until a parameter $b \colon B$ is somehow chosen (say “randomly”, “experimentally” or in whichever way), in which case only we obtain definite data $prog(d)(b) \;\colon\; D'$ .

It makes sense to say that the data type

\bigcirc_B D' \;\coloneqq\; \big( B \to D'\big)

exhibits a “ $B$ -indefinitess effect” that goes along with the execution of the program, making its output indefinite. Such side effects in computing may be modeled by monads in computer science (see there for more). Indeed $\bigcirc_B$ is a classical example of such a monad, often called the $B$ -reader monad, reflecting the idea that it postpones returning definite output data until it has “read in” an otherwise unspecified parameter.

Incidentally, in terms of modal logic the parameter type $B$ plays the role of the set of “possible worlds” in which the given non-deterministic computation may take definite values. For more on this modal logic perspective see at necessity and possibility the section relation to potentiality.

Now the monad-structure on $\bigcirc_B$ allows to carry along this indefiniteness effect so that followup programs, nominally waiting for input data in $D'$ , are consistently treated as non-deterministic, dependent on specification of $b \colon B$ , too.

Concretely, if

prog \;\colon\; D \to \bigcirc_B D'

and

prog' \;\colon\; D' \to \bigcirc_B D''

are two such non-deterministic programs but conditioned on the same global random variable $b \colon B$ , then their consistent composition, as such, is their Kleisli composition (which involves the categorical multiplication-operation in the reader monad, see there for details):

prog \;\;\text{>>=}\;\; prog' \;\;\;\; \equiv \;\;\;\; bind^{\bigcirc_B} prog' \;\circ\; prog \;\colon\; D \to \bigcirc_B D'' \,.

Of course, in general the non-determinism of a program need not be parameterized over a fixed parameter type $B$ . If the sequence $(B_i)_{i \colon I}$ of parameters is known beforehand, one can form their product type $B \equiv \prod_i B_i$ and proceed as above, but in general even that sequence may not be pre-specified and further effect handling besides a fixed reader monad needs to be considered (…).

Examples

Quantum computation

A fundamental example of non-deterministic computation is quantum computation, where the process of quantum measurement produces outcomes that – to the best knowledge of the current state of fundamental physics – are fundamentally non-deterministic in that there is not even in principle a way to predict a given outcome with certainty (only their probability distribution is fixed by quantum theory).

The possible results of a quantum measurement are indexed by a “measurement basis” which is exactly a (finite) set $B$ serving as the parameter type in the modal logic-discussion above. The only difference for quantum computation is that quantum data types are linear types, so that the relevant reader monad here is a linear version of the classical reader monad – see at quantum reader monad for details.

A formulation of (non-deterministic) quantum computation in terms of the resulting $\bigcirc_B$ -modal linear type theory is discussed at quantum circuits via dependent linear types.

But in fact the quantum reader monad is (for finite $B$ ) a Frobenius monad and as such isomorphic (see here) to the “classical structures” Frobenius monad has long been proposed to model quantum measurement in quantum information theory via dagger-compact categories (Coecke & Pavlović (2008))

Differential linear logic

Something reminiscent of – but different from – non-deterministic computation appears (see the quotes below) in differential linear logic, where the cut-elimination procedure has been argued to “intuitively correspond” to non-determinism:

The differential linear cut rule receives as input a proof of type $\Gamma \vdash \Delta$ and returns as output a formal sum of proofs of type $\Gamma \vdash \Delta$ . During the procedure, several proofs can be formed to eliminate cuts from the proof in the previous step, these different possibilities are summed and thus the algorithm returns a formal sum of proofs. The nondetermism is here realized by the addition of proofs as formal sums of proofs that can be understood as a disjunction but in not exactly the same way that the linear disjunction because it’s a disjunction of proofs and not of formulas. An algorithm which returns $\pi_{1} + \pi_{2}$ where $\pi_{1},\pi_{2}$ are two proofs of the same type $\Gamma \vdash \Delta$ returns in fact the disjunction of $\pi_{1}$ and $\pi_{2}$ because it can’t chose between the two possibilities. On the level of the syntactic proof theory, one cannot code this sum only by the intermediate of a biproduct in a semiadditive category, because it would imply that the algorithm would introduce cuts that will not be eliminated: in a semiadditive category, the sum is defined by combining the structural morphisms of the products and coproducts, which are then equal, through composition, ie. through the cut rule. One thus works in a CMon-enriched symmetric monoidal category where we have access to a sum of morphism without necessarily biproducts. In the case where one considers the additive connectors in the logic, the additive disjunction and the additive conjunction are then equated under the presence of formal sums and one can reobtain this formal sum through the biproduct in the semantics. But the semantics is not able to explain the syntactic subtleties related to cut elimination and the difference between a formal sum of two proofs and a sum obtained through cuts and biproducts.

In contradistinction, the cut elimination of linear logic is a deterministic algorithm and doesn’t imply formal sums of proofs. Thus, in linear logic, if one includes the additive disjunction and the additive conjunction, they are not necessarily equated forming a biproduct in the syntax, as in differential linear logic.

From Ehrhard (2008), Introduction:

“when one linearizes a proof obtained by contracting two linear inputs of a proof, one has to choose between these two inputs, and there is no canonical way of doing so: we take the non-deterministic superposition of the two possibilities. Syntactically, this means that one must accept the possibility of adding proofs of the same formula, which is standard in mathematics, but hard to accept as a primitive logical operation on proofs.”

However, Erhardt & Regnier (2009), p. 3 admit that:

“Notice that in our axiomatization of sums in the differential lambda-calculus, the non-deterministic reduction rule $s + s' \to s$ will not be valid, but sums will nevertheless intuitively correspond to a version of non-deterministic choice where all the actual choice operations are postponed: the result of a term reduction will in general be a large formal sum of terms, and we can reduce the really ”non-deterministic“ part of the computation to a unique ultimate step consisting in choosing one term of that sum. This step is however a fiction and will not appear as a reduction rule of our calculus”

Related concepts

References

Michael Sipser, §1.2 in: Introduction to the Theory Of Computation, 3rd ed: Cengage Learning (2012) [ISBN:978-1-133-18779-0,pdf, pdf]