section_path: Construction/Other approaches
section_name: Other approaches
paragraph_text: Other approaches
  
  In theoretical computer science, other approaches for the construction of integers are used by automated theorem provers and term rewrite engines.Integers are represented as algebraic terms built using a few basic operations (e.g., zero, succ, pred) and, possibly, using natural numbers, which are assumed to be already constructed (using, say, the Peano approach).
  
  There exist at least ten such constructions of signed integers. These constructions differ in several ways: the number of basic operations used for the construction, the number (usually, between 0 and 2) and the types of arguments accepted by these operations; the presence or absence of natural numbers as arguments of some of these operations, and the fact that these operations are free constructors or not, i.e., that the same integer can be represented using only one or many algebraic terms.
  
  The technique for the construction of integers presented in the previous section corresponds to the particular case where there is a single basic operation pair (x, y) {\displaystyle (x,y)} that takes as arguments two natural numbers x {\displaystyle x} and y {\displaystyle y}, and returns an integer (equal to x − y {\displaystyle x-y}). This operation is not free since the integer 0 can be written pair (0,0), or pair (1,1), or pair (2,2), etc. This technique of construction is used by the proof assistant Isabelle; however, many other tools use alternative construction techniques, notable those based upon free constructors, which are simpler and can be implemented more efficiently in computers.