View source for BIT predicate

{{good article}}
{{short description|Test of a specified bit in a binary number}}
In [[mathematics]] and [[computer science]], the '''BIT predicate''', sometimes {{nowrap|written <math>\text{BIT}(i,j)</math>,}} is a [[Predicate (mathematical logic)|predicate]] that tests whether the {{nowrap|<math>j</math>th}} [[bit]] of the {{nowrap|number <math>i</math>}} (starting from the [[least significant digit]]) {{nowrap|is 1,}} when <math>i</math> is written as a [[binary number]]. Its mathematical applications include modeling the membership relation of [[hereditarily finite set]]s, and defining the adjacency relation of the [[Rado graph]]. In computer science, it is used for efficient representations of set [[data structure]]s using [[bit vector]]s, in defining the [[private information retrieval]] problem from [[communication complexity]], and in [[descriptive complexity theory]] to formulate logical descriptions of [[complexity class]]es.

==History==
The BIT predicate was first introduced in 1937 by [[Wilhelm Ackermann]] to define the [[Ackermann coding]], which encodes [[hereditarily finite set]]s as {{nowrap|[[natural number]]s.{{r|ackermann|kirby}}}} The BIT predicate can be used to perform membership tests for the encoded sets: <math>\text{BIT}(i,j)</math> is true if and only if the set encoded {{nowrap|by <math>j</math>}} is a member of the set encoded {{nowrap|by <math>i</math>.{{r|ackermann}}}}

Ackermann denoted the predicate <math>\text{BIT}(i,j)</math> {{nowrap|as <math>\mathfrak{El}(j,i)</math>,}} using a [[Fraktur]] font to distinguish it from the notation <math>\mathrm{El}(j,i)</math> that he used for set membership (short for {{nowrap|"<math>j</math> is}} an element {{nowrap|of <math>i</math>"}} in German).{{r|ackermann}} The notation {{nowrap|<math>\text{BIT}(i,j)</math>,}} 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 {{nowrap|1990s.{{efn|An early use of the BIT predicate name is {{harvtxt|Immerman|1989}}.{{r|immerman89}} In a 1990 paper, David Mix Barrington attributes the <math>\text{BIT}(i,j)</math> notation, and its application in [[descriptive complexity]], to Fagin; Barrington credits Fagin for inspiring Immerman to work in this {{nowrap|area.{{r|mix-barrington}}}} However, {{harvtxt|Ajtai|Fagin|1990}} refer to "Immerman's BIT {{nowrap|relation".{{r|ajtai-fagin}}}}}}}}

==Description and implementation==
The [[binary representation]] of a number <math>i</math> is an expression for <math>i</math> as a sum of distinct [[power of two|powers of two]],
<math display=block>i = \cdots b_3 2^3 + b_2 2^2 + b_1 2^1 + b_0 2^0</math>
where each [[bit]] <math>b_j</math> in this expression is either 0 or 1. It is commonly written in binary notation as just the sequence of these bits, <math>\cdots b_3b_2b_1b_0</math>. Given this expansion for <math>i</math>, the BIT predicate <math>\text{BIT}(i,j)</math> is defined to equal <math>b_j</math>. It can be calculated from the formula
<math display=block>\text{BIT}(i,j) = \left\lfloor \frac{i}{2^j} \right\rfloor \bmod 2,</math>
where <math>\lfloor \cdot \rfloor</math> is the [[floor function]] and mod is the [[modulo function]].{{r|lindell}}
The BIT predicate is a [[primitive recursive function]].{{r|kirby|rautenberg}} As a [[binary relation]] (producing true and false values rather than 1 and 0 respectively), the BIT predicate is [[asymmetric relation|asymmetric]]: there do not exist two numbers <math>i</math> and <math>j</math> for which both <math>\text{BIT}(i,j)</math> and <math>\text{BIT}(j,i)</math> are true.{{efn|For the asymmetry of the set membership relation that the BIT predicate encodes, see {{harvtxt|Cameron|2001}}.{{r|cameron}}}}

In programming languages such as [[C (programming language)|C]], [[C++]], [[Java (programming language)|Java]], or [[Python (programming language)|Python]] that provide a {{nowrap|[[Bitwise operation#Bit shifts|right shift operator]] <code>&gt;&gt;</code>}} and a {{nowrap|[[Bitwise operation|bitwise Boolean and operator]] <code>&amp;</code>,}} the BIT predicate <math>\text{BIT}(i,j)</math> can be implemented by the expression
<code>(i>>j)&1</code>. The subexpression <code>i>>j</code> shifts the bits in the binary representation of <math>i</math> so that {{nowrap|bit <math>b_j</math>}} is shifted to {{nowrap|position 0,}} and the {{nowrap|subexpression <code>&1</code>}} [[Mask (computing)|masks off]] the remaining bits, leaving only the bit in {{nowrap|position 0.}} As with the modular arithmetic formula above, the value of the expression is {{nowrap|1 or 0,}} respectively as the value of <math>\text{BIT}(i,j)</math> is true or false.{{r|venugopal}}

==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 <math>\{0, 1, \ldots\}</math> may be represented by a bit array with a one in {{nowrap|position <math>i</math>}} when <math>i</math> 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 <math>\{i,j,k,\dots\}</math> for distinct <math>i,j,k,\dots</math> is represented as the binary number <math>2^i+2^j+2^k+\cdots</math>. If <math>S</math> is a set, represented in this way, and <math>i</math> is a number that may or may not be an element of <math>S</math>, then <math>\text{BIT}(S,i)</math> returns a nonzero value when <math>i</math> is a member and zero when it is not.{{efn|{{harvtxt|Arndt|2011}}. Arndt implements the BIT predicate by <code>S&(1<<i)</code> rather than <code>(S>>i)&1</code>, but the result is zero or nonzero equally for both implementations.{{r|arndt}}}}

The same technique may be used to test membership in subsets of any sequence <math>x_0,x_1,\dots</math> 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]], <code>java.util.EnumSet</code> uses this technique to implement a set data structure for [[enumerated type]]s.{{r|bloch}} Ackermann's encoding of the hereditarily finite sets is an example of this technique, for the recursively-generated sequence of hereditarily finite sets.{{efn|1={{harvtxt|Tarau|2010}}. Tarau's implementation of the membership test (as <code>inSet</code> in the section "Deriving set operations") amounts to testing whether <code>S&(1<<i) == 1<<i</code> rather than <code>(S>>i)&1</code>, similar to that for {{harvtxt|Arndt|2011}}.{{r|tarau}}}}

===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 {{nowrap|number <math>i</math>,}} wishes to determine the result of a BIT predicate <math>\text{BIT}(i,j)</math> without divulging the value {{nowrap|of <math>j</math>}} to the servers. {{harvtxt|Chor|Kushilevitz|Goldreich|Sudan|1998}} describe a method for replicating <math>i</math> 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 {{nowrap|of <math>i</math>.{{r|ckgs}}}}

===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 describes the class of [[formal language]]s that can be described by a formula in first-order logic with a comparison operation on [[total order|totally ordered]] variables (interpreted as the indexes of characters in a [[string (computer science)|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 model theory|finite models]].{{efn|In some sources this class is written {{nowrap|FO[<]}}, to indicate the comparison operation; however, when defining complexity classes from logic in this way, the comparison operation cannot be omitted,{{r|immerman99}} so it is not necessary to indicate that it is present.}} However, with these operations, only a very restricted class of languages, the [[Star-free language|star-free regular languages]], can be described.{{r|pp}} Adding the BIT predicate to the repertoire of operations used in these logical formulas results in a more robust complexity class, {{nowrap|FO[BIT]}}, 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}}

===Construction of the Rado graph===
[[File:Rado graph.svg|thumb|upright=1.1|The Rado graph, constructed from the BIT predicate. For instance, an edge connects 0 to 3 because the 0th bit of 3 is nonzero.]]
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 <math>i</math> and <math>j</math> are adjacent in the Rado graph when either <math>\text{BIT}(i,j)</math> or <math>\text{BIT}(j,i)</math> is nonzero.{{r|rado}}

The resulting graph has many important properties: it contains every finite undirected graph as an [[induced subgraph]], and any [[graph isomorphism|isomorphism]] of its induced subgraphs can be extended to a symmetry of the whole graph.{{r|cameron}}

==Notes==
{{notelist}}

==References==
{{reflist|refs=

<ref name=ackermann>{{cite journal|
last=Ackermann|first=Wilhelm| author-link=Wilhelm Ackermann|title=Die Widerspruchsfreiheit der allgemeinen Mengenlehre|
journal=[[Mathematische Annalen]]|language=de|year=1937|volume=114|pages=305–315|
url=http://www.digizeitschriften.de/dms/img/?PPN=PPN235181684_0114&DMDID=dmdlog23|
access-date=2012-01-09|doi=10.1007/bf01594179
|s2cid=120576556}}</ref>

<ref name=arndt>{{cite book|last=Arndt|first=Jörg| title=Matters Computational: Ideas, Algorithms, Source Code|publisher=Springer|year=2011|url=http://jjj.de/fxt/fxtbook.pdf| contribution=1.9.2: Testing whether an element is in a given set|page=24}}</ref>

<ref name=ajtai-fagin>{{cite journal
 | last1 = Ajtai | first1 = Miklós | author1-link = Miklós Ajtai
 | last2 = Fagin | first2 = Ronald | author2-link = Ronald Fagin
 | doi = 10.2307/2274958
 | issue = 1
 | journal = [[The Journal of Symbolic Logic]]
 | mr = 1043548
 | pages = 113–150
 | title = Reachability is harder for directed than for undirected finite graphs
 | volume = 55
 | year = 1990| jstor = 2274958 | s2cid = 14177866 }}</ref>

<ref name=bis>{{cite journal
 | last1 = Mix Barrington | first1 = David A.
 | last2 = Immerman | first2 = Neil | author2-link = Neil Immerman
 | last3 = Straubing | first3 = Howard
 | doi = 10.1016/0022-0000(90)90022-D
 | issue = 3
 | journal = [[Journal of Computer and System Sciences]]
 | mr = 1079468
 | pages = 274–306
 | title = On uniformity within NC<sup>1</sup>
 | volume = 41
 | year = 1990}}</ref>

<ref name=bloch>{{cite book|title=Effective Java|first=Joshua|last=Bloch|author-link=Joshua Bloch|edition=2nd|publisher=Addison-Wesley Professional|year=2008|isbn=9780132778046|contribution=Item 32: Use enumSet instead of bit fields|pages=159–160|contribution-url=https://books.google.com/books?id=ka2VUBqHiWkC&pg=PA159}}</ref>

<ref name=cameron>{{cite conference
 | last = Cameron | first = Peter J. | authorlink = Peter Cameron (mathematician)
 | title = The random graph revisited
 | url = https://www.math.uni-bielefeld.de/~rehmann/ECM/cdrom/3ecm/pdfs/pant3/camer.pdf
 | doi = 10.1007/978-3-0348-8268-2_15
 | mr = 1905324
 | location = Basel
 | pages = 267–274
 | publisher = Birkhäuser
 | series = Progr. Math.
 | book-title = [[European Congress of Mathematics]], Vol. I (Barcelona, 2000)
 | volume = 201
 | year = 2001}}</ref>

<ref name=ckgs>{{cite journal
 | last1 = Chor | first1 = Benny | author1-link = Benny Chor
 | last2 = Kushilevitz | first2 = Eyal
 | last3 = Goldreich | first3 = Oded | author3-link = Oded Goldreich
 | last4 = Sudan | first4 = Madhu | author4-link = Madhu Sudan
 | date = 1998
 | doi = 10.1145/293347.293350
 | issue = 6
 | journal = [[Journal of the ACM]]
 | pages = 965–981
 | title = Private information retrieval
 | volume = 45
 | s2cid = 544823
 | doi-access = free
 }}.</ref>

<ref name=immerman89>{{cite journal
 | last = Immerman | first = Neil | author-link = Neil Immerman
 | doi = 10.1137/0218043
 | issue = 3
 | journal = [[SIAM Journal on Computing]]
 | mr = 996841
 | pages = 625–638
 | title = Expressibility and parallel complexity
 | volume = 18
 | year = 1989}}</ref>

<ref name=immerman99>{{cite book | last = Immerman | first = Neil | author-link = Neil Immerman | title = Descriptive Complexity|title-link= Descriptive Complexity | year = 1999 | publisher = Springer-Verlag | location = New York | isbn = 0-387-98600-6 | pages=[https://books.google.com/books/about/Descriptive_Complexity.html?id=a53eBwAAQBAJ&pg=PA13 13–16]}}</ref>

<ref name=kirby>{{cite journal|
last=Kirby|first=Laurence|
title=Finitary Set Theory|
journal=Notre Dame Journal of Formal Logic|
year=2009|volume=50|issue=3|pages=227–244|doi=10.1215/00294527-2009-009
|doi-access=free}}</ref>

<ref name=lindell>{{cite conference
 | last = Lindell
 | first = Steven
 | title = A purely logical characterization of circuit uniformity
 | url = http://ww3.haverford.edu/cmsc/slindell/Uniformity.pdf
 | doi = 10.1109/SCT.1992.215393
 | pages = 185–192
 | publisher = IEEE Computer Society
 | book-title = Proceedings of the Seventh Annual Structure in Complexity Theory Conference, Boston, Massachusetts, USA, June 22-25, 1992
 | year = 1992
 | access-date = 2023-07-04
 | archive-date = 2017-08-30
 | archive-url = https://web.archive.org/web/20170830004340/http://ww3.haverford.edu/cmsc/slindell/Uniformity.pdf
 | url-status = bot: unknown
 }}</ref>

<ref name=mix-barrington>{{cite journal
 | last = Mix Barrington | first = David A.
 | doi = 10.1007/BF02090772
 | issue = 3
 | journal = Mathematical Systems Theory
 | mr = 1062347
 | pages = 147–164
 | title = Extensions of an idea of McNaughton
 | volume = 23
 | year = 1990| s2cid = 198177167
 }}</ref>

<ref name=pp>{{cite journal
 | last1 = Perrin | first1 = Dominique | author1-link = Dominique Perrin
 | last2 = Pin | first2 = Jean-Éric | author2-link = Jean-Éric Pin
 | doi = 10.1016/0022-0000(86)90037-1
 | issue = 3
 | journal = [[Journal of Computer and System Sciences]]
 | mr = 858236
 | pages = 393–406
 | title = First-order logic and star-free sets
 | volume = 32
 | year = 1986| doi-access = free
 }}</ref>

<ref name=rado>{{cite journal|first=Richard|last=Rado|author-link=Richard Rado|url=http://matwbn.icm.edu.pl/ksiazki/aa/aa9/aa9133.pdf|title=Universal graphs and universal functions|journal=Acta Arith.|year=1964|volume=9|issue=4|pages=331–340|doi=10.4064/aa-9-4-331-340|doi-access=free}}.</ref>

<ref name=rautenberg>{{cite book|page=261|last=Rautenberg|first=Wolfgang|author-link=Wolfgang Rautenberg|doi=10.1007/978-1-4419-1221-3|title=A Concise Introduction to Mathematical Logic|publisher=[[Springer Science+Business Media]]|location=[[New York City|New York]]|edition=3rd|isbn=978-1-4419-1220-6|year=2010}}</ref>

<ref name=tarau>{{cite conference
 | last = Tarau | first = Paul
 | editor1-last = Autexier | editor1-first = Serge
 | editor2-last = Calmet | editor2-first = Jacques
 | editor3-last = Delahaye | editor3-first = David
 | editor4-last = Ion | editor4-first = Patrick D. F.
 | editor5-last = Rideau | editor5-first = Laurence
 | editor6-last = Rioboo | editor6-first = Renaud
 | editor7-last = Sexton | editor7-first = Alan P.
 | arxiv = 1006.5768
 | title = A unified formal description of arithmetic and set theoretical data types
 | doi = 10.1007/978-3-642-14128-7_21
 | pages = 247–261
 | publisher = Springer
 | series = Lecture Notes in Computer Science
 | book-title = 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
 | volume = 6167
 | year = 2010}}</ref>

<ref name=venugopal>{{cite book|title=Mastering C++|first=K. R.|last=Venugopal|publisher=Tata McGraw-Hill Publishing Company|year=1997|isbn=9780074634547|page=123|url=https://books.google.com/books?id=2soaY85jGQIC&pg=PA123}}.</ref>

}}

{{DEFAULTSORT:Bit Predicate}}
[[Category:Binary arithmetic]]
[[Category:Binary relations]]
[[Category:Descriptive complexity]]
[[Category:Circuit complexity]]
[[Category:Set theory]]