In mathematics and computer science, the BIT predicate, sometimes written , is a predicate that tests whether the th bit of the number (starting from the least significant digit) is 1, when is written as a binary number. Its mathematical applications include modeling the membership relation of hereditarily finite sets, and defining the adjacency relation of the Rado graph. In computer science, it is used for efficient representations of set data structures using bit vectors, in defining the private information retrieval problem from communication complexity, and in descriptive complexity theory to formulate logical descriptions of complexity classes.
The BIT predicate was first introduced in 1937 by Wilhelm Ackermann to define the Ackermann coding, which encodes hereditarily finite sets as natural numbers. [1] [2] The BIT predicate can be used to perform membership tests for the encoded sets: is true if and only if the set encoded by is a member of the set encoded by . [1]
Ackermann denoted the predicate as , using a Fraktur font to distinguish it from the notation that he used for set membership (short for " is an element of " in German). [1] The notation , and the name "the BIT predicate", come from the work of Ronald Fagin and Neil Immerman, who applied this predicate in computational complexity theory as a way to encode and decode information in the late 1980s and early 1990s. [lower-alpha 1]
The binary representation of a number is an expression for as a sum of distinct powers of two,
where each bit in this expression is either 0 or 1. It is commonly written in binary notation as just the sequence of these bits, . Given this expansion for , the BIT predicate is defined to equal . It can be calculated from the formula
where is the floor function and mod is the modulo function. [6] The BIT predicate is a primitive recursive function. [2] [7] As a binary relation (producing true and false values rather than 1 and 0 respectively), the BIT predicate is asymmetric: there do not exist two numbers and for which both and are true. [lower-alpha 2]
In programming languages such as C, C++, Java, or Python that provide a right shift operator >>
and a bitwise Boolean and operator &
, the BIT predicate can be implemented by the expression (i>>j)&1
. The subexpression i>>j
shifts the bits in the binary representation of so that bit is shifted to position 0, and the subexpression &1
masks off the remaining bits, leaving only the bit in position 0. As with the modular arithmetic formula above, the value of the expression is 1 or 0, respectively as the value of is true or false. [9]
For a set represented as a bit array, the BIT predicate can be used to test set membership. For instance, subsets of the non-negative integers may be represented by a bit array with a one in position when is a member of the subset, and a zero in that position when it is not a member. When such a bit array is interpreted as a binary number, the set for distinct is represented as the binary number . If is a set, represented in this way, and is a number that may or may not be an element of , then returns a nonzero value when is a member and zero when it is not. [lower-alpha 3]
The same technique may be used to test membership in subsets of any sequence of distinct values, encoded using powers of two whose exponents are the positions of the elements in this sequence, rather than their values. For instance, in the Java collections framework, java.util.EnumSet
uses this technique to implement a set data structure for enumerated types. [11] Ackermann's encoding of the hereditarily finite sets is an example of this technique, for the recursively-generated sequence of hereditarily finite sets. [lower-alpha 4]
In the mathematical study of computer security, the private information retrieval problem can be modeled as one in which a client, communicating with a collection of servers that store a binary number , wishes to determine the result of a BIT predicate without divulging the value of to the servers. Chor et al. (1998) describe a method for replicating across two servers in such a way that the client can solve the private information retrieval problem using a substantially smaller amount of communication than would be necessary to recover the complete value of . [13]
The BIT predicate is often examined in the context of first-order logic, where systems of logic result from adding the BIT predicate to first-order logic. In descriptive complexity, the complexity class FO describes the class of formal languages that can be described by a formula in first-order logic with a comparison operation on totally ordered variables (interpreted as the indexes of characters in a string) and with predicates that test whether this string has a given character at a given numerical index. A formula in this logic defines a language consisting of its finite models. [lower-alpha 5] However, with these operations, only a very restricted class of languages, the star-free regular languages, can be described. [15] Adding the BIT predicate to the repertoire of operations used in these logical formulas results in a more robust complexity class, FO[BIT], meaning that it is less sensitive to minor variations in its definition. [lower-alpha 6]
The class FO[BIT] is the same as the class FO[+,×], of first-order logic with addition and multiplication predicates. [14] It is also the same as the circuit complexity class DLOGTIME-uniform AC0. Here, AC0 describes the problems that can be computed by circuits of AND gates and OR gates with polynomial size, bounded height, and unbounded fanout. "Uniform" means that the circuits of all problem sizes must be described by a single algorithm. More specifically, it must be possible to index the gates of each circuit by numbers in such a way that the type of each gate and the adjacency between any two gates can be computed by a deterministic algorithm whose time is logarithmic in the size of the circuit (DLOGTIME). [6] [16]
In 1964, German–British mathematician Richard Rado used the BIT predicate to construct the infinite Rado graph. Rado's construction is just the symmetrization of Ackermann's 1937 construction of the hereditary finite sets from the BIT predicate: two vertices numbered and are adjacent in the Rado graph when either or is nonzero. [17]
The resulting graph has many important properties: it contains every finite undirected graph as an induced subgraph, and any isomorphism of its induced subgraphs can be extended to a symmetry of the whole graph. [8]
S&(1<<i)
rather than (S>>i)&1
, but the result is zero or nonzero equally for both implementations. [10] inSet
in the section "Deriving set operations") amounts to testing whether S&(1<<i) == 1<<i
rather than (S>>i)&1
, similar to that for Arndt (2011). [12] First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.
In mathematics, the transitive closureR+ of a homogeneous binary relation R on a set X is the smallest relation on X that contains R and is transitive. For finite sets, "smallest" can be taken in its usual sense, of having the fewest related pairs; for infinite sets R+ is the unique minimal transitive superset of R.
In mathematics and set theory, hereditarily finite sets are defined as finite sets whose elements are all hereditarily finite sets. In other words, the set itself is finite, and all of its elements are finite sets, recursively all the way down to the empty set.
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
In computational complexity theory, P, also known as PTIME or DTIME(nO(1)), is a fundamental complexity class. It contains all decision problems that can be solved by a deterministic Turing machine using a polynomial amount of computation time, or polynomial time.
Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.
Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to interpretations on finite structures, which have a finite universe.
Fagin's theorem is the oldest result of descriptive complexity theory, a branch of computational complexity theory that characterizes complexity classes in terms of logic-based descriptions of their problems rather than by the behavior of algorithms for solving those problems. The theorem states that the set of all properties expressible in existential second-order logic is precisely the complexity class NP.
AC0 is a complexity class used in circuit complexity. It is the smallest class in the AC hierarchy, and consists of all families of circuits of depth O(1) and polynomial size, with unlimited-fanin AND gates and OR gates (we allow NOT gates only at the inputs). It thus contains NC0, which has only bounded-fanin AND and OR gates.
In the mathematical field of graph theory, the Rado graph, Erdős–Rényi graph, or random graph is a countably infinite graph that can be constructed by choosing independently at random for each pair of its vertices whether to connect the vertices by an edge. The names of this graph honor Richard Rado, Paul Erdős, and Alfréd Rényi, mathematicians who studied it in the early 1960s; it appears even earlier in the work of Wilhelm Ackermann (1937). The Rado graph can also be constructed non-randomly, by symmetrizing the membership relation of the hereditarily finite sets, by applying the BIT predicate to the binary representations of the natural numbers, or as an infinite Paley graph that has edges connecting pairs of prime numbers congruent to 1 mod 4 that are quadratic residues modulo each other.
In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi–Elgot–Trakhtenbrot theorem gives a logical characterization of the regular languages.
In computer science, more specifically in automata and formal language theory, nested words are a concept proposed by Alur and Madhusudan as a joint generalization of words, as traditionally used for modelling linearly ordered structures, and of ordered unranked trees, as traditionally used for modelling hierarchical structures. Finite-state acceptors for nested words, so-called nested word automata, then give a more expressive generalization of finite automata on words. The linear encodings of languages accepted by finite nested word automata gives the class of visibly pushdown languages. The latter language class lies properly between the regular languages and the deterministic context-free languages. Since their introduction in 2004, these concepts have triggered much research in that area.
In the study of graph algorithms, Courcelle's theorem is the statement that every graph property definable in the monadic second-order logic of graphs can be decided in linear time on graphs of bounded treewidth. The result was first proved by Bruno Courcelle in 1990 and independently rediscovered by Borie, Parker & Tovey (1992). It is considered the archetype of algorithmic meta-theorems.
In mathematical logic, the spectrum of a sentence is the set of natural numbers occurring as the size of a finite model in which a given sentence is true. By a result in descriptive complexity, a set of natural numbers is a spectrum if and only if it can be recognized in non-deterministic exponential time.
In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power.
In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query languages, in particular to Datalog.
In computer science and mathematics, more precisely in automata theory, model theory and formal language, a regular numerical predicate is a kind of relation over integers. Regular numerical predicates can also be considered as a subset of for some arity . One of the main interests of this class of predicates is that it can be defined in plenty of different ways, using different logical formalisms. Furthermore, most of the definitions use only basic notions, and thus allows to relate foundations of various fields of fundamental computer science such as automata theory, syntactic semigroup, model theory and semigroup theory.
In mathematics, S2S is the monadic second order theory with two successors. It is one of the most expressive natural decidable theories known, with many decidable theories interpretable in S2S. Its decidability was proved by Rabin in 1969.