Basis of definitions

Question

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?

Answer 1

In C++ axioms are pure virtual functions.

Not really. Pure virtual functions are only about run-time polymorphism- this has nothing to do with axioms.

What you can do (which is commonly done) is define new operators through the CRTP which are defined in terms of some subset of existing ones- commonly done with relational and arithmetic operators. However, C++ currently contains no Standard mechanism for axioms. It was considered but rejected along with Concepts, afaik. And as something you can't even describe, it's surely impossible to check- in the general case, this would involve solving the Halting Problem.

Answer 2

In general, the dependencies between propositions form a digraph, which may, as you point out, contain cycles. A minimal complete subset is defined by a set of nodes such that all other nodes are reachable from (at least) one node in the set. I don’t believe there is any language that allows you to specify this directly; in Haskell the typical solution is to document convenient subsets, and keep typeclasses small and simple. Take Eq for example:

class Eq a where
  (==), (/=) :: a -> a -> Bool
  x == y = not (x /= y)
  x /= y = not (x == y)

In this case the minimal complete definitions include (==) and (/=), which is obvious enough that it doesn’t really need to be verified. I would argue that a typeclass with enough complexity to give a programmer pause is too complex, and warrants refactoring.

If you just want to specify a few reasonable minimal sets, you can leave the main definition abstract and derive a typeclass for each. But that quickly becomes cumbersome, and in Haskell you still don’t really know that the user has properly implemented your interface.

But it isn’t your responsibility, as an interface writer, to define behaviour for misuse of the interface.

Answer 3

You risk going off the rails in at least two ways:

1. C++'s pure virtual functions are nothing like axioms. An axiom is a defined assumption. A pure virtual function is the the absence or expectation of a definition. A set of axioms is required to create a mathematical system; a C++ class need not contain a single virtual function, pure or otherwise.

2. You're using two distinct notions of derivation. Lemmas are derived through the application of axioms. You can't claim that an expression is a lemma unless you can show that it is the result of axioms and nothing else. The set of axioms completely determines the set of possible lemmas. In OOP terminology, one class or method may be derived from another, but it's a different relationship than that of lemmas to axioms in that the creator of the class or method is free to add or remove parts.

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!).

There's a great deal of research on the topic of proving the correctness of programs. You might be interested in reading about formal verification. Two other topics that might interest you are inference systems and formal grammars.

How can we specify, and check, that an instance provides at least a basis?

Are you talking about code specifically, or any "set of functions which characterize something"? And what do you mean by "instance"? Those concerns and the ones above notwithstanding, one approach is:

• Enumerate all the definitions in the system.

• For each definition d, decide whether d depends solely on other definitions in the system and nothing else. If so, remove d from the system.

• Whatever remains in the system is by definition the "basis," i.e. the set of definitions that are necessary to create the original system.