SH53 - Natural Deduction seen as the Turing Machine for Logical Reasoning

Reading through the chapter of mathematical reasoning in the B Book, I couldn't help but notice how much emphasis was put in using natural deduction. I strengthening the belief that natural deduction is not appropriate as it is for practical reasoning. In fact, I think it is appropriate to compare it to Turing machines. When we are interested in the power of a system, we want to reduce it to its bare essential. In that sense, the few simple inference rules usually associated with natural deduction are very helpful. But we must keep in mind the bias that we have when delivering that judgment: we are doing the job of a logician who wants to compare different systems. It is the same for Turing machines. They are very simple and this is why it helps reasoning about their computability properties. I think nobody knowing anything about programming would suggest to use a Turing machine to build any kind of useful system unless it is sufficiently small as to be of no significance.

Similarly, I don't think that using natural deduction as a means for reasoning about systems is any wiser than programming with Turing machines. For simplifying the logic, natural deduction offers no means to exploit equivalence because it can be dealt with using implication. It is true but not helpful when carrying out an actual reasoning. Keeping equivalence intact is simply much more efficient. People don't have to go through the same proof twice. It is also true that even if case analysis can help achieve the proof, it also helps making it unmanageable.

In short, developing proof design techniques is as necessary as developing program design techniques and, similarly, it involves developing the right notation and finding powerful heuristics. Natural deduction is not a means to that end. However, it can be used to prove properties of equational logic without to need use it when carrying out the actual reasoning.

Simon Hudon Zürich June 9th, 2009

SH48 - Weakening Preconditions

I remember an instant messaging conversation I had with Prof. Jonathan Ostroff (YorkU) where he said he was buying more and more the view of preconditions as waiting conditions like in Event-B and SCOOP. I objected that, obviously, unlike Event-B, we can't hold the position that preconditions must be strengthen. It was, as I thought, some kind of law of nature and common sense that only postconditions can be strengthened. Preconditions can only be weakened. But what if it does not fit the essence of object oriented programming? Certainly, it is acceptable that the precondition of routines be weakened in the process of refinement. Since features in classes are implemented as routines (whenever they use arguments), why not just carry over the rule to the implementation of class features?

The fact that they are type bound makes an important difference. Rather than understand that the target of a call is just another kind of argument to a routine that will be dynamically chosen so that it meets (in a semi-formal way) the specifications of the routine, it should be understood as an event that occurs that (might) transform the current state of an object. That event can be or not provoked by a certain client. Whenever it is, it does not matter for the correctness of that client that the precondition gets weakened in the refinement of its supplier. On the other hand, since object aliasing is an important part of object oriented programming, considering the transformation of an object by other clients makes sense as the general case. If we assume that no other clients will invoke a certain feature unless its guard (or precondition) is satisfied, weakening it might produce surprising results. On the other hand, if we allow ourselves to blur the distinction between a class and an event-B abstract machine, we might want to make sure that the deadlock condition of a module is not strengthened in its refinements. It would mean that, in any refinement, if the guard of an action is strengthened, it must only be in the context of an action split where the guard of all resulting actions complement each other in a way that their disjunction is equivalent to the guard of the refined event.

The door does not seem to be completely closed for the notion of precondition weakening but I, for one, would not dwell on it.

Simon Hudon May 18th 2009 ETH Zürich

SH16 - Sacrificing Efficiency for Some Degree of Confidence

Is the concern for software correctness getting in the way of efficiency? or Sacrificing efficiency for confidence (as opposed to correctness)

Post-scriptum note: the opposition between correctness and confidence is based on the objectivity of the criterion of correctness and the subjectivity of the criterion of confidence. Confidence can be the result of obliviousness.

Also, I have not reread it since posting it on my blog and it might need some moderation. (End of note)

With modern trends like test driven development, it seems like, for the sake of having a testable system, one will always (or most of the time) take the shortest path allowing him to add just one feature. It is positive to see that he always worry about having something that works, albeit using very restrained notion of what a "working system" is. However, the fact that the modern programmer (or, to borrow a more trendy term, the average programmer) is unable to reason in any effective way about the formulation of his specifications or even those of his architecture makes him unable to postpone the implementation until such a time as his design has been validated on its own. This points out to a blatant lack of separation of concerns. A more disciplined approach would require that the programmer be able to validate his architecture using nothing but the information contained in it and the information contained in the formulation of the relevant requirements.

It is very important to make precise what is meant by validation. Like the term coined for any profound notion, it has been used to designate so many different concepts that, it cannot be understood as anything more than a buzz-term unless it is explicitly defined.

The validation of an architecture means that any implementation following its rules is bound to produce correct result for every valid input. This means that it is a validation impossible to accomplish using testing. Some might argue that model checking would be a valid choice to come to grip with that separation of concern. If we forget everything else, they could be right. The problem with model checking is that we still rely on a posteriori verification: the concern for correctness still fails to guide the programmer to his solution. Proponents of the notion of the "average programmer" might be satisfied with that since they accept that the layman has, at best, a third rate intellect and we cannot ask him reason in any formal way about his work. However, it is clearly a better approach than postponing any kind of validation until after an implementation has been provided.

What I'm coming at now is that since the implementations are rushed at, programmers don't seem to take any care for making it efficient or correct in a general way. All that is expected is that the test suite passes. If any efficiency issues arises (much later in the development) it is considered that it is the good time to address them. It seems that an efficient implementation would have been easier to produce at the very first moment that the programmer started writing it.

Simon Hudon Gatineau, December 2008 continued in Zuerich, May 2009

SH34 - Thoughts on the Use of Typed Logic and Dependent Types

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