| Type Checking and Inductive Proof |
| This short
study is about the complexities of dealing with inductive
types; that is, types which are defined recursively such
as the type whose elements are the following 0 Such types will be encountered if we progress far enough into type theory; so let's begin the journey by looking at .. Matrices Matrix arithmetic is a foundational study in computer science, finding applications in image processing. Let's remind ourselves of what a matrix is; essentially nothing more than a rectangular array of numbers. In functional programing terms (ignoring linear time access problems) we can represent a matrix as a list of lists of numbers where each constituent list must be of the same length. Now here's the challenge; how do we get the type checker to recognise this idea of the lists being 'of the same length'? It turns out that the requirement 'of the same length' presents a challenge, but not one that is too difficult to solve in Qi, at least at the beginning. But the solution will take us quite quickly into interestingly deep waters where the Qi type checker gets left behind. Let's leave the safe but boring shore behind by paddling out from the shallows towards the open sea. First, we need to define a type operator len, that works like list except that it includes a parameter that indicates the length of the list. Here's a start __________ And we finish the job with an inductive rule. X : A; Y : (len N
A); If we put this definition into Qi and ask [[1] [2] [3] [4]] : (len N A) we get [[1] [2] [3] [4]] : (len (succ (succ (succ (succ 0)))) (list number)) which is right. We can now define a matrix of order M,N. X : (len M (len N number)); (17+) [[1 3] [5 8] [89 4]] :
(matrix M N) (18+) [[1 3] [5 8] [89 56 4]] :
(matrix M N) You can amuse yourself by defining the type square_matrix (a matrix with equal rows and columns) which is not too hard. Now so far, we are intellectually still in sight of land. However we are packing some explosive cargo, because we are using inductive types to defines matrices; namely those types which include 0 Matrix Addition The complexity of dealing with these types become apparent when we start to work with matrix arithmetic and we begin with matrix addition which is simply defined in Qi. (define add and this works too (26-) (add [[1 2 3] [4 5 6] [7 8
9]] [[1 2 3] [4 5 6] [7 8 9]]) But we want to add types to this program and say that matrix addition requires matrices of the same order; like this. (define add And here we find that the type checker rejects the annotation. Now the reasons why the type checker fails are multitudinous. You can trace and find out for yourself. But accepting that it does fail to verify, does this show Qi is wrong? No; it only shows that the Qi type checker is incomplete. For instance the following expression can be computed for any value of N (e.g. N = 1000). (if (goldbachs-conjecture-is-true-up-to N) true 0) and, we will find that it will hold true for N = 1000. What is the type of the above expression? We might say that since apriori, it evaluates to 'true' for N = 1000, it must return 'true' and hence the type is boolean. However no type checker will know this and hence a type error will be returned. We could actually get round this, by building an arithmetic evaluator into our checker and thereby making the program more intelligent. But once we embark on this course, we must see that however 'intelligent' we make our program, such examples will multiply and hence our type checker will always incomplete; that is, there are expressions whose types will be provable to the mathematical mind, but closed to the checker. Qi is no exception. From Type Checking to Formal Methods In computer science there is an area called formal methods which is concerned with the verification (i.e proof) that programs have desired properties. Now type checking is almost, but not quite, coextensive with the decidable part of formal methods. We often find that any usefully decidable form of error checking or proof of correctness will end up in the compiler or the type checker. Moreover the concept of a type is extremely stretchy; we can invent types ad hoc. Instead of saying that a program has property P we can say it has the type P. How about the type of all terminating programs in a language L? If we can formalise the notion, why not? Now though this will give some type theorists palpitations, it suggests that type theory is not really a nicely closed off area seperate from the rest of computational logic, but rather a way of representing and doing formal methods in a certain notation. So let's go back to the matrix problem and see what is needed to prove the following. add : (matrix M N) --> (matrix M N) --> (matrix M N) The M and the N are, of course, placeholders for inductive types. Which should incline us, correctly, to believe that inductive proof will be needed somewhere. Indeed we end up doing formal methods. We start with the base case for M. add : (matrix 0 N) --> (matrix 0 N) --> (matrix 0 N) which transposes to x : (matrix 0 N), y : (matrix 0 N) >> (add x y) : (matrix 0 N) But then this is just x : (len 0 (len N number)), y : (len 0 (len N number)) >> (add x y) : (len 0 (len N number)) But we know that x : (len 0 (len N number)) just when x = [] and hence we have to prove [] : (len 0 (len N number)), [] : (len 0 (len N number)) >> (add [] []) : (len 0 (len N number)) But (add [] []) = [] and so the base case is proved. The inductive case requires that we show that if for some arbitrary natural number m. add : (matrix m N) --> (matrix m N) --> (matrix m N) holds that the following holds add : (matrix (succ m) N) --> (matrix (succ m) N) --> (matrix (succ m) N) Or alternatively x : (matrix (succ m) N), y : (matrix (succ m) N) >> (add x y) : (matrix (succ m) N) Now if x : (matrix (succ m) N) then x is a non-empty list (cons x1 x2) and so is y (cons y1 y2) . So we reformulate our target: we need to prove, for some x1,x2,y1,y2 (cons x1 x2) :
(matrix (succ
m) N), (cons y1 y2) : (matrix (succ m) N) By substitution, (add (cons x1 x2) (cons y1 y2)) is just (cons (add-row x1 y1) (add x2 y2)) (cons x1 x2) :
(matrix (succ
m) N), (cons y1 y2) : (matrix (succ m) N) Again (matrix (succ m) N) is just (len (succ m) (len N number)) (cons x1 x2) :
(len (succ
m) (len N number)), (cons y1 y2) : (len (succ m) (len N number)) From the definition of len we know (cons (add-row x1 y1) (add x2 y2)) : (len (succ m) (len N number)) just when
So these two conclusions are what we have to prove. But we also have as assumptions (cons x1 x2) :
(len (succ
m) (len N number)), and by parity of reasoning it must hold that x1 : (len N number), x2 : (len m (len N number)), y1 : (len N number), y2 : (len m (len N number)), Our inductive hypothesis states add : (matrix m N) --> (matrix m N) --> (matrix m N) holds; that is add : (len m (len N number)) --> (len m (len N number)) --> (len m (len N number)) holds. So given x2 : (len m (len N number)) and y2 : (len m (len N number)) then (add x2 y2) : (len m (len N number)) must hold and we have proved one of the two conclusions. What remains to be proved now is (add-row x1 y1) : (len N number). We already have as assumptions x1 : (len N number) and y1 : (len N number) so what we need to prove is x1 : (len N number), y1 : (len N number) >> (add-row x1 y1) : (len N number) This is of course nothing more than the signature attached to add-row and the proof requires a further induction over N. I won't do this here, but the proof process is similar to the one taken so far. This done, the proof is completed. Reflections on Qi III The complexity of the proof process in typechecking add makes it no surprise that the Qi type checker fails. Indeed, once we grasp the complexity of the reasoning involved, it becomes silly to hope that the T* algorithm in Qi could possibly cope with such challenges. And yet, the matrix addition function is simple and the type definitions are not too hard. How did the water get so deep? The answer is that in Qi, the sequent notation allows us to express types and ideas which are resistant to easy automation of proof. T* is an automation of proof that suffices for nearly all of what is decidable and has nice properties like termination that are great for programming. We do not want to swap T* for something worse; yet something worse, or to put it more gently, more powerful and more messy, is needed to prove these signatures. The correct way, I believe, to incorporate this insight into a future version of Qi, is to give the user the power to jump out of Qi into a tactic-driven and interactive theorem-proving environment in which these problems can be attacked. Changing Qi to allow this to be done is not hard, but determining the shape and form of the environment is less easy to determine, mainly because so many environments have been built. My analysis has two tentative conclusions. The first is that the solution should be generic; that is, Qi III should contain a shell for people to experiment with tactic-driven and interactive solutions to formal methods. People who want to experiment with Coq or Isabelle-like approaches should be able to do so. We should not hard-wire a solution into the system. The second is that this example shows that many of the techniques of reasoning used to discharge this proof use techniques developed for the Boyer-Moore ATP (or ACL2 as it is now) and some fruitful fusion of ACL2 technology with Qi might produce something genuinely useful and impressive. Mark Copyright (c) 2009, Mark Tarver |