Basis of definitions
- by Yttrill
Let us suppose we have a set of functions which characterise something: in the OO world methods characterising a type. In mathematics these are propositions and we have two kinds: axioms and lemmas. Axioms are assumptions, lemmas are easily derived from them. In C++ axioms are pure virtual functions.
Here's the problem: there's more than one way to axiomatise a system. Given a set of propositions or methods, a subset of the propositions which is necessary and sufficient to derive all the others is called a basis.
So too, for methods or functions, we have a desired set which must be defined, and typically every one has one or more definitions in terms of the others, and we require the programmer to provide instance definitions which are sufficient to allow all the others to be defined, and, if there is an overspecification, then it is consistent.
Let me give an example (in Felix, Haskell code would be similar):
class Eq[t] {
virtual fun ==(x:t,y:t):bool => eq(x,y);
virtual fun eq(x:t, y:t)=> x == y;
virtual fun != (x:t,y:t):bool => not (x == y);
axiom reflex(x:t): x == x;
axiom sym(x:t, y:t): (x == y) == (y == x);
axiom trans(x:t, y:t, z:t): implies(x == y and y == z, x == z);
}
Here it is clear: the programmer must define either == or eq or both. If both are defined, the definitions must be equivalent. Failing to define one doesn't cause a compiler error, it causes an infinite loop at run time. Defining both inequivalently doesn't cause an error either, it is just inconsistent. Note the axioms specified constrain the semantics of any definition. Given a definition of == either directly or via a definition of eq, then != is defined automatically, although the programmer might replace the default with something more efficient, clearly such an overspecification has to be consistent.
Please note, == could also be defined in terms of !=, but we didn't do that.
A characterisation of a partial or total order is more complex. It is much more demanding since there is a combinatorial explosion of possible bases.
There is an reason to desire overspecification: performance. There also another reason: choice and convenience.
So here, there are several questions: one is how to check semantics are obeyed and I am not looking for an answer here (way too hard!). The other question is:
How can we specify, and check, that an instance provides at least a basis?
And a much harder question: how can we provide several default definitions which depend on the basis chosen?
