|Computational class||Turing complete|
This language operates on natural numbers (non-negative integers). A natural number is either zero, or a successor of a natural number.
Source code consists of functions. There is only one builtin function:
<=. This function takes two arguments and returns
1 iff the first argument is less that or equal to the second argument, otherwise returns
Each function defined in the source code has one extra implicit argument. Such argument is the last argument of a function and such argument is not used explicitly when calling a function. When a function is called, the return value of the function is the smallest natural number such that, when that number is passed as the last argument, the function returns a non-zero value.
Here is how we define constant zero:
zero a = a <= a
a is the implicit argument. Function zero actualy takes no arguments. The return value of
zero is the smallest natural number
a such that
a <= a is a non-zero natural number. Since
0 is less than or equal to
0, the result of
0 <= 0 is
zero always returns
Here is a function that always returns
one a = (a <= a) <= a
a <= a is
1 <= a is
0. The smallest
a for which
(a <= a) <= a is non-zero is
1, so the function
one always returns
Here is a shorter example:
one a = a
Basically, the smallest number that is truthy, which is
We need a function that returns
1 if the argument is
0, otherwise returns
0. Since this function takes one argument, we need total of two formal arguments (because the second one is implicit):
not a b = (a <= zero) <= b
0, the smallest
b for which the expression is non-zero is
a is non-zero, then the smallest
0. So, this is a logical invertor. We can now use
0 as a falsy value and
1 as a truthy value.
Logical implication from
b is true if
a is false or
b is true. This function takes two arguments:
(->) a b c = (a <= b) <= c
Checking all possible boolean combinations of
b, it can be proved that this indeed represents the logical implication.
Note: we defined this function as an infix binary operator. We can use it in expressions like this:
a -> b.
(||) a b c = (not a -> b) <= c
Note: prefix operators have higher precedence, so
not a -> b is the same as
(not a) -> b.
(&&) a b c = a <= (b <= c)
(==) a b c = ((a <= b) && (b <= a)) <= c
1 iff the two given natural numbers are the same. We achieved that by asserting that both
a <= b and
b <= a. In other words, we assert that the result
c is the smallest number that is at least as truthy as
(a <= b) && (b <= a), which is exactly what we need.
(/=) a b c = c == not (a == b)
Less than (without being equal)
(<) a b c = c == ((a <= b) && (a /= b))
It says: the first argument is less than or equal to the second argument, but they are not equal.
inc a b = a < b
The result is the smallest
b such that
a < b, which is exactly one more than
dec a b = inc b == a
The result, when incremented, is equal to
dec 0 does not terminate, because there is no
b such that
inc b == 0.
(+) a b c = ((b == zero) -> (c == a)) && ((b /= zero) -> (c == inc (a + dec b)))
It says: if the second argument is
0, the result is the first argument, otherwise the result is one more than the sum of the first argument and decremented second argument.
(-) a b c = (c + b) == a
Subtracting a larger number from a smaller number does not terminate.
(*) a b c = ((b == zero) -> (c == zero)) && ((b /= zero) -> (c == (a + (a * dec b))))
(/) a b c = (c * b) == a
Division by zero does not terminate (except if both operands are
0, in which case the result is
0). If the result would be a non-integer number, division also does not terminate.
See the talk page.