Typechecking in ATS involves generating and solving constraints.
As an example, the code below implements the well-known factorial
function:

In this implementation, the function

fact is assigned the
following type:

which means that

fact returns a natural number r when applied
to a natural number n. When the code is typechecked, the following
constraints need to be solved:

For each natural number n, n > 0 implies n - 1 >= 0

For each natural number n and each natural number r_{1}, n > 0 implies n * r_{1}>= 0

For each natural number n, 1 >= 0 holds.

The first constraint is generated due to the call

fact(x-1),
which requires that

x-1 be a natural number. The second
constraint is generated in order to verify that

x * fact(x-1)
is a natural number under the assumption that

fact(x-1) is a
natural number. The third constraint is generated in order to verify that

1 is a natural number. The first and the third constraints can
be readily solved by the constraint solver in ATS, which is based on the
Fourier-Motzkin variable elimination method. However, the second constraint
cannot be handled by the constraint solver as it is nonlinear: The
constraint cannot be turned into a linear integer programming problem due
to the occurrence of the nonlinear term (n*r

_{1}). While nonlinear
constraints cannot be handled automatically by the constraint solver in
ATS, the programmer can verify them by constructing proofs in ATS
explicitly. I will cover the issue of explicit proof construction in an
elaborated manner elsewhere.

By default, the constraint-solver implemented for ATS/Postiats makes use of
the standard arithmetic of infinite precision. For the sake of efficiency,
one may also choose to use machine-level arithmetic for solving integer
constraints. Due to potential arithmetic overflow, results returned by the
constraint-solver that uses machine-level arithmetic can be incorrect (but
I have so far not knowingly encountered such a situation in practice).