7.2.2 Bottom and meta-equality

Prev Up Next Page 171 of 800 Search internet

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

value define x factorial as if x = 0 then 1 else x * ( x - 1 ) factorial end define

If a computer is asked to compute the value of the expression ( - 1 ) factorial then the computer will loop indefinitely. For that reason we shall say that the value of ( - 1 ) factorial is bottom where bottom [bottom] reads bottom.

We shall say that ( - 1 ) factorial is meta-equal to bottom and write ( - 1 ) factorial == bottom. Meta-equality x == y is equality in the theory behind Logiweb. The theory behind Logiweb is called map theory.

The base page defines another equality named x = y. We shall refer to x = y 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 x == y 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 x = y 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, x == y is equality and x = y is an equivalence relation, which may confuse mathematicians.

Prev Up Next Page 171 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05