2.7.2 On Equality

One example of a property this operator should have, for reasons that will not be immediately clear, is that for any trees x and k, the equality cons(cons(nil,k),nil) x = k always holds. Even though the present exposition opts for readability over formality, statements like these demand clarification of the notion of equality. Some of the more pedantic points in Raw Material may be needed for the following ideas to hold water.

• As originally stipulated, it is always possible to distinguish nil from any member of the set. We can therefore decide on this basis whether a = b whenever at least one of them is nil.
• Where neither a nor b is nil in an expression a = b, but rather something of the form cons(x,y), the equality holds if and only if both pairs of corresponding subexpressions are equal. If at least one member of each pair of corresponding subexpressions is nil, the question is settled, but otherwise there is recourse to their respective subexpressions, and so on. This condition follows from the uniqueness property of the cons operator.
• If one side of an equality is of the form x y, or is defined in terms of such an expression, but (x,y) is one of those pairs with which the operator associates no result, then the equality holds if and only if the other side is similarly ill defined.
• Statements involving universal quantification (i.e., beginning with words similar to “for any tree x …”) obviously do not apply to instances of a variable (x) outside the indicated set (trees). Hence, they are not refuted by any consequence of identifying a variable with an undefined expression.

Readers who are aware of such issues as pointer equality or intensional versus extensional equality of functions are urged to forget all about them in the context of this document, and abide only by what is stated. Other readers should ignore this paragraph.

This document was generated on November 8, 2012 using texi2html 1.82.