BIT predicate: Difference between revisions
→Complexity and logic: which one |
|||
Line 29: | Line 29: | ||
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]] {{nowrap|FO[BIT,<]}} describes the class of [[formal language]]s that can be described by a formula in first-order logic using this predicate, together with predicates that test whether a string (considered as a [[model theory|model]] of the given formula) has a given character at a given numerical index and that compare the positions of two given indices. Adding the BIT predicate to {{nowrap|FO[<]}} results in a more robust complexity class, meaning that it is less sensitive to minor variations in its definition.{{efn|{{harvtxt|Immerman|1999}}, p. 13: "Adding BIT ... makes the set of first-order definable boolean queries a more robust complexity class."}} |
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]] {{nowrap|FO[BIT,<]}} describes the class of [[formal language]]s that can be described by a formula in first-order logic using this predicate, together with predicates that test whether a string (considered as a [[model theory|model]] of the given formula) has a given character at a given numerical index and that compare the positions of two given indices. Adding the BIT predicate to {{nowrap|FO[<]}} results in a more robust complexity class, meaning that it is less sensitive to minor variations in its definition.{{efn|{{harvtxt|Immerman|1999}}, p. 13: "Adding BIT ... makes the set of first-order definable boolean queries a more robust complexity class."}} |
||
The class {{nowrap|FO[BIT,<]}} is the same as the class {{nowrap|FO[+,×,<]}}, of first-order logic with addition and multiplication predicates.{{r|immerman99}} |
|||
It is also the same as the [[circuit complexity]] class [[DLOGTIME]]-[[Uniformity (complexity)|uniform]] [[AC0|AC<sup>0</sup>]]. Here, AC<sup>0</sup> describes the problems that can be computed by circuits of [[AND gate]]s and [[OR gate]]s 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).{{r|lindell|bis}} |
It is also the same as the [[circuit complexity]] class [[DLOGTIME]]-[[Uniformity (complexity)|uniform]] [[AC0|AC<sup>0</sup>]]. Here, AC<sup>0</sup> describes the problems that can be computed by circuits of [[AND gate]]s and [[OR gate]]s 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).{{r|lindell|bis}} |
||
Revision as of 19:26, 11 July 2023
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.
History
The BIT predicate was first introduced in 1937 by Wilhelm Ackermann to define the Ackermann coding, which encodes hereditarily finite sets as natural numbers. 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][2]
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.[a]
Description and implementation
In mathematical notation, the BIT predicate can be described as where is the floor function and mod is the modulo function.[6] It is a primitive recursive function.[2][7] As a binary relation, the BIT predicate is asymmetric: there do not exist two numbers and for which both and are true.[b]
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
. Here the bits of are numbered from the low-order bits to high-order bits in the binary representation of , with the ones bit being numbered as bit 0. The subexpression i>>j
shifts these bits 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]
Applications
Set data structures
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.[c]
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.[d]
Private information retrieval
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]
Complexity and logic
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[BIT,<] describes the class of formal languages that can be described by a formula in first-order logic using this predicate, together with predicates that test whether a string (considered as a model of the given formula) has a given character at a given numerical index and that compare the positions of two given indices. Adding the BIT predicate to FO[<] results in a more robust complexity class, meaning that it is less sensitive to minor variations in its definition.[e]
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][15]
Construction of the Rado graph
Ackermann in 1937 and Richard Rado in 1964 used this predicate to construct the infinite Rado graph. In their construction, the vertices of this graph correspond to the non-negative integers, written in binary, and there is an undirected edge from vertex to vertex , for , when is nonzero.[16]
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]
Notes
- ^ An early use of the BIT predicate name is Immerman (1989).[3] In a 1990 paper, David Mix Barrington attributes the notation, and its application in descriptive complexity, to Fagin; Barrington credits Fagin for inspiring Immerman to work in this area.[4] However, Ajtai & Fagin (1990) refer to "Immerman's BIT relation".[5]
- ^ For the asymmetry of the set membership relation that the BIT predicate encodes, see Cameron (2001).[8]
- ^ Arndt (2011). Arndt implements the BIT predicate by
S&(1<<i)
rather than(S>>i)&1
, but the result is zero or nonzero equally for both implementations.[10] - ^ Tarau (2010). Tarau's implementation of the membership test (as
inSet
in the section "Deriving set operations") amounts to testing whetherS&(1<<i) == 1<<i
rather than(S>>i)&1
, similar to that for Arndt (2011).[12] - ^ Immerman (1999), p. 13: "Adding BIT ... makes the set of first-order definable boolean queries a more robust complexity class."
References
- ^ a b Ackermann, Wilhelm (1937). "Die Widerspruchsfreiheit der allgemeinen Mengenlehre". Mathematische Annalen (in German). 114: 305–315. doi:10.1007/bf01594179. S2CID 120576556. Retrieved 2012-01-09.
- ^ a b Kirby, Laurence (2009). "Finitary Set Theory". Notre Dame Journal of Formal Logic. 50 (3): 227–244. doi:10.1215/00294527-2009-009.
- ^ Immerman, Neil (1989). "Expressibility and parallel complexity". SIAM Journal on Computing. 18 (3): 625–638. doi:10.1137/0218043. MR 0996841.
- ^ Mix Barrington, David A. (1990). "Extensions of an idea of McNaughton". Mathematical Systems Theory. 23 (3): 147–164. doi:10.1007/BF02090772. MR 1062347.
- ^ Ajtai, Miklós; Fagin, Ronald (1990). "Reachability is harder for directed than for undirected finite graphs". The Journal of Symbolic Logic. 55 (1): 113–150. doi:10.2307/2274958. MR 1043548.
- ^ a b Lindell, Steven (1992). "A purely logical characterization of circuit uniformity" (PDF). Proceedings of the Seventh Annual Structure in Complexity Theory Conference, Boston, Massachusetts, USA, June 22-25, 1992. IEEE Computer Society. pp. 185–192. doi:10.1109/SCT.1992.215393.
- ^ Rautenberg, Wolfgang (2010). A Concise Introduction to Mathematical Logic (3rd ed.). New York: Springer Science+Business Media. p. 261. doi:10.1007/978-1-4419-1221-3. ISBN 978-1-4419-1220-6.
- ^ a b Cameron, Peter J. (2001). "The random graph revisited" (PDF). European Congress of Mathematics, Vol. I (Barcelona, 2000). Progr. Math. Vol. 201. Basel: Birkhäuser. pp. 267–274. doi:10.1007/978-3-0348-8268-2_15. MR 1905324.
- ^ Venugopal, K. R. (1997). Mastering C++. Tata McGraw-Hill Publishing Company. p. 123. ISBN 9780074634547..
- ^ Arndt, Jörg (2011). "1.9.2: Testing whether an element is in a given set". Matters Computational: Ideas, Algorithms, Source Code (PDF). Springer. p. 24.
- ^ Bloch, Joshua (2008). "Item 32: Use enumSet instead of bit fields". Effective Java (2nd ed.). Addison-Wesley Professional. pp. 159–160. ISBN 9780132778046.
- ^ Tarau, Paul (2010). "A unified formal description of arithmetic and set theoretical data types". In Autexier, Serge; Calmet, Jacques; Delahaye, David; Ion, Patrick D. F.; Rideau, Laurence; Rioboo, Renaud; Sexton, Alan P. (eds.). Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5–10, 2010, Proceedings. Lecture Notes in Computer Science. Vol. 6167. Springer. pp. 247–261. arXiv:1006.5768. doi:10.1007/978-3-642-14128-7_21.
- ^ Chor, Benny; Kushilevitz, Eyal; Goldreich, Oded; Sudan, Madhu (1998). "Private information retrieval". Journal of the ACM. 45 (6): 965–981. doi:10.1145/293347.293350. S2CID 544823..
- ^ Immerman, Neil (1999). Descriptive Complexity. New York: Springer-Verlag. pp. 13–16. ISBN 0-387-98600-6.
- ^ Mix Barrington, David A.; Immerman, Neil; Straubing, Howard (1990). "On uniformity within NC1". Journal of Computer and System Sciences. 41 (3): 274–306. doi:10.1016/0022-0000(90)90022-D. MR 1079468.
- ^ Rado, Richard (1964). "Universal graphs and universal functions" (PDF). Acta Arith. 9 (4): 331–340. doi:10.4064/aa-9-4-331-340..