On one hand, it is a very bad thing (TM) to make type checking depend on undecidable conditions, therefore inducing a proof obligation to ensure syntactic and type correctness. One of the best example is the need to prove that a given function lookup is made on a member of the domain of the mentioned function. When it is generated for an axiom, lemmata cannot be reused from one to the other.
On the other hand, if we are content with the fact that every proposition (i.e. axiom or theorem) concerning functions is accompanied by the assumption that the argument is part of the function's domain, we leave open the value of lookups of functions outside their domain.
Either we decide to associate the arbitrary value of the associated type to arguments outside a function's domain or we leave it undefined and accept a different value from function to function.
In the second case, whereas the interesting property of function equality is
f = g == dom.f = dom.g /\ < x =" g.x">
However, if we don't have also
f = g == dom.f = dom.g /\ < x =" g.x">
it becomes impossible to use the principle of substitutability.
If, to the contrary, we choose to assign the arbitrary value of the associated type to arguments outside of partial functions' domain we are asking for trouble as an axiom might specify the image of a function regardless of whether or not the mentioned argument is part of the image as in the following:
axm1: f.x = 3 axm2: dom.f = { x | x mod 3 = 2 : x } axm3: g.x = 7 axm4: dom.g = { 1, 2, 3, 4 }
However, an axiom of function theory might state
fun1: ¬ x in dom.f ==> f.x = choice (H)
For an arbitrary f: G +-> H, x: G and generic types G and H. Let's now assume x is neither a member of dom.f nor a member of dom.g (as the union of both of them does not include all the natural numbers, it is a sensible assumption).
| 3 | ||
| = | { axm1 } | |
| f.x | ||
| = | { fun1 with f, x := f, x } | |
| choice (NAT) | ||
| = | { fun1 with f, x := g, x } | |
| g.x | ||
| = | { axm3 } | |
| 7 |
Which is obviously nonsensical. This choice of interpretation is not the only way to introduce nonsense indirectly. Take for example the choice function. Asserting a particular type for it as an assumption is a nice way to run into trouble. The problem at hand is related to that kind of error. The goal here is to discuss several possibilities for making all the nonsense obvious and more difficult to introduce. In general, we would like to be able to build a theory in a modular way allowing different modules to reference each other in a non circular way. As is often the case in software design, it is desirable to limit the number of dependancies between modules. In that context, nonsense can be introduced when referencing two modules that have been developed independently if they postulate additional constraints on a common module. The trouble will arise when the accumulation of third-party constraints contradict each other.
In that case, axioms referencing definitions made in another module should make sure to make nothing more than put a name on an element for which it is possible to prove that it exists. In fact, it might be a good thing to require such a proof when postulating such axioms. In appearance, we are coming back at the apparent ugliness of set theory as it is used in B. To solve it, it might be sufficient to relax the constraint imposed on the order of the declaration of axioms and theorems. By allowing theorems to be defined before axioms, we retain the ability to reduce the labor of formal reasoning for every proof including those induced by the definition of axioms.
Simon Hudon ETH Zürich March 4th 2009
