Demonic non-determinism

Last updated

A term which describes the execution of a non-deterministic program where all choices are made in favour of non-termination.[ citation needed ]


Related Research Articles

In computer science, the occurs check is a part of algorithms for syntactic unification. It causes unification of a variable V and a structure S to fail if S contains V.

In computational complexity theory, a nonelementary problem is a problem that is not a member of the class ELEMENTARY. As a class it is sometimes denoted as NONELEMENTARY.

In computer science, Programming Computable Functions (PCF) is a typed functional language introduced by Gordon Plotkin in 1977, based on previous unpublished material by Dana Scott. It can be considered to be an extended version of the typed lambda calculus or a simplified version of modern typed functional languages such as ML or Haskell.

In automata theory, a deterministic pushdown automaton is a variation of the pushdown automaton. The class of deterministic pushdown automata accepts the deterministic context-free languages, a proper subset of context-free languages.

In computational complexity theory, L/poly is the complexity class of logarithmic space machines with a polynomial amount of advice. L/poly is a non-uniform logarithmic space class, analogous to the non-uniform polynomial time class P/poly.

ACC<sup>0</sup>

ACC0, sometimes called ACC, is a class of computational models and problems defined in circuit complexity, a field of theoretical computer science. The class is defined by augmenting the class AC0 of constant-depth "alternating circuits" with the ability to count; the acronym ACC stands for "AC with counters". Specifically, a problem belongs to ACC0 if it can be solved by polynomial-size, constant-depth circuits of unbounded fan-in gates, including gates that count modulo a fixed integer. ACC0 corresponds to computation in any solvable monoid. The class is very well studied in theoretical computer science because of the algebraic connections and because it is one of the largest concrete computational models for which computational impossibility results, so-called circuit lower bounds, can be proved.

Language equations are mathematical statements that resemble numerical equations, but the variables assume values of formal languages rather than numbers. Instead of arithmetic operations in numerical equations, the variables are joined by language operations. Among the most common operations on two languages A and B are the set union AB, the set intersection AB, and the concatenation AB. Finally, as an operation taking a single operand, the set A* denotes the Kleene star of the language A. Therefore language equations can be used to represent formal grammars, since the languages generated by the grammar must be the solution of a system of language equations.

In the theory of programming languages in computer science, deforestation is a program transformation to eliminate intermediate lists or tree structures that are created and then immediately consumed by a program.

<span class="mw-page-title-main">Orc (programming language)</span>

Orc is a concurrent, nondeterministic computer programming language created by Jayadev Misra at the University of Texas at Austin.

<span class="mw-page-title-main">Joseph Sifakis</span> Greek-French computer scientist

Joseph Sifakis is a Greek-French computer scientist. He received the 2007 Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his work on model checking.

In graph theory, the planarity testing problem is the algorithmic problem of testing whether a given graph is a planar graph (that is, whether it can be drawn in the plane without edge intersections). This is a well-studied problem in computer science for which many practical algorithms have emerged, many taking advantage of novel data structures. Most of these methods operate in O(n) time (linear time), where n is the number of edges (or vertices) in the graph, which is asymptotically optimal. Rather than just being a single Boolean value, the output of a planarity testing algorithm may be a planar graph embedding, if the graph is planar, or an obstacle to planarity such as a Kuratowski subgraph if it is not.

Oscar Peter Buneman, is a British computer scientist who works in the areas of database systems and database theory.

<span class="mw-page-title-main">Roland Carl Backhouse</span> British computer scientist and mathematician

Roland Carl Backhouse is a British computer scientist and mathematician. As of 2020, he is Emeritus Professor of Computing Science at the University of Nottingham.

In graph theory, a partial k-tree is a type of graph, defined either as a subgraph of a k-tree or as a graph with treewidth at most k. Many NP-hard combinatorial problems on graphs are solvable in polynomial time when restricted to the partial k-trees, for bounded values of k.

<span class="mw-page-title-main">Géraud Sénizergues</span> French computer scientist

Géraud Sénizergues is a French computer scientist at the University of Bordeaux.

In computer science, angelic non-determinism is the execution of a nondeterministic algorithm where particular choices are declared to always favor a desired result, if that result is possible.

<span class="mw-page-title-main">Kai Salomaa</span> Finnish Canadian theoretical computer scientist

Kai T. Salomaa is a Finnish Canadian theoretical computer scientist, known for his numerous contributions to the state complexity of finite automata. His highly cited 1994 joint paper with Yu and Zhuang laid the foundations of the area. He has published over 100 papers in scientific journals on various subjects in formal language theory. Salomaa is a full professor at Queen's University.

State complexity is an area of theoretical computer science dealing with the size of abstract automata, such as different kinds of finite automata. The classical result in the area is that simulating an -state nondeterministic finite automaton by a deterministic finite automaton requires exactly states in the worst case.

<span class="mw-page-title-main">Zone theorem</span> Theorem in computational and discrete geometry

In geometry, the zone theorem is a result that establishes the complexity of the zone of a line in an arrangement of lines.

In graph theory, a graph is a pairwise compatibility graph (PCG) if there exists a tree and two non-negative real numbers such that each node of has a one-to-one mapping with a leaf node of such that two nodes and are adjacent in if and only if the distance between and are in the interval .

References

Wirsing, M.; Broy, M. (5 March 1981). "On the algebraic specification of nondeterministic programming languages". Caap '81. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. 112: 162–179. doi:10.1007/3-540-10828-9_61. ISBN   978-3-540-10828-3.

McIver, A. K.; Morgan, Carroll (6 September 2001). "Partial correctness for probabilistic demonic programs". Theoretical Computer Science. 266 (1): 513–541. doi: 10.1016/S0304-3975(00)00208-5 . ISSN   0304-3975.