| Search internet |
A program may loop indefinitely. As an example, take the factorial function:

If a computer is asked to compute the value of the expression
then the computer will loop indefinitely. For that reason we shall say that the value of
is
where
[bottom] reads bottom.
We shall say that
is meta-equal to
and write
. Meta-equality
is equality in the theory behind Logiweb. The theory behind Logiweb is called map theory.
The base page defines another equality named
. We shall refer to
as computable equality. As an example, computable equality appears in the definition of the factorial function above.
Readers with a mathematical background should note this: meta-equality
is a genuine equality relation with all the properties one expects from equality, including the rule of substitution of equals. Meta-equality lives in the meta-theory, which is map theory. In contrast, computable equality
is an equivalence relation over a certain domain. Computable equality lives in Logiweb in the sense that the Logiweb Abstract Machine can compute it.
In short,
is equality and
is an equivalence relation, which may confuse mathematicians.
| Search logiweb.eu |