One of the cool features missing in ACL2 is the ability to create counterexamples to a claim upon a failed proof attempt. This isn't always possible of course1, but it would still be a useful feature, since the existence of a counterexample would let users know that the attempt failed because the proposition wasn't a theorem, not because of a lack of capability in ACL2.
A failed search for counterexamples might also help ACL2 recognize why a proposition is in fact probably true, and find a new approach to proving it. This is pretty unlikely, but it could be a useful step in helping the ATP get over the problem of emulating human proof techniques. When we're stuck finding a proof for a theorem, and we suspect that the conjecture is false, we might try to find a counterexample. As we search for a counterexample, we may discover that a certain tact we pick is fruitless because a subtle condition of the conjecture that we missed covers this case. This newfound insight can help us find a new proof by observing some previously overlooked structure in the problem.
Some interesting work in this realm has been done in the form of QuickCheck, and its Lisp child ClickCheck. There is also a technical report on this topic by Myung Won Kim that I haven't made my way through yet.
1 Consider if a program were always able to construct a counterexample to every false claim. Then theorem proving would be decidable, since we could tell a whether a conjecture was a theorem by whether or not we can construct a counterexample to it. But it is in fact undecidable, so we have a contradiction.
Sunday, April 8, 2007
Thesis Idea
The immediate point of my foray into ATP is for my Bachelors Thesis. My current working idea is to employ ACL2 to prove theorems about Haskell programs. Proving theorems about any Haskell program would be far too difficult a project for something to be completed within 2 years (I graduate in Spring '09), so at the moment I am evaluating what subset of Haskell I wish to work on.
I'd like to have a subset that captures at least SOME of the interesting properties of Haskell. Some of the features I'm considering include:
Modeling any of these features in ACL2 presents a challenge in and of itself.
#1 is tricky since ACL2 itself only has finite objects, so reasoning about the properties of infinite objects without creating an instance of such a creature won't be simple. Fortunately, Matt Kaufmann did some work in this area back in the 80's for adapting Nqthm (predecessor to ACL2) into a theorem prover about the SASL language. He just put up a soft copy of a tech report he wrote on the subject (exactly 1 year and 1 day before I was born...) here.
#2 Shouldn't be too tricky. Since the subset of Haskell I'll be using will be completely side-effect free, I can model call-by-need with call-by-name and maintain correctness.
#3 The hard part about including this would be handling types in the untyped ACL2. I'm not sure how to go about this, but it seems like someone has probably worked on this before, so I can base my work on previous works. It's a pretty essential part of Haskell, so it is certainly going in.
#4 Would be quite difficult. I probably wouldn't be able to include this. Instead I will require explicit type annotations on functions.
#5 Definitely want to include this. Should be pretty simple.
#6 Not sure about this. Will definitely require a fair bit of research on my part. It's an important part of Haskell, but I honestly have no idea how it works. It seems really cool, so I'd really like to include it.
Since my formal background in programming languages is about nil, I've slotted myself a fair bit of reading. So far today I've humped through the first 11 chapters of Types and Programming Languages. I'm not the biggest fan of the way the book goes about things, but it's not bad.
I'd like to have a subset that captures at least SOME of the interesting properties of Haskell. Some of the features I'm considering include:
- Infinite objects
- Lazy evaluation (specifically call-by-need)
- Static typing
- Type inference
- Currying
- Pattern Matching
Modeling any of these features in ACL2 presents a challenge in and of itself.
#1 is tricky since ACL2 itself only has finite objects, so reasoning about the properties of infinite objects without creating an instance of such a creature won't be simple. Fortunately, Matt Kaufmann did some work in this area back in the 80's for adapting Nqthm (predecessor to ACL2) into a theorem prover about the SASL language. He just put up a soft copy of a tech report he wrote on the subject (exactly 1 year and 1 day before I was born...) here.
#2 Shouldn't be too tricky. Since the subset of Haskell I'll be using will be completely side-effect free, I can model call-by-need with call-by-name and maintain correctness.
#3 The hard part about including this would be handling types in the untyped ACL2. I'm not sure how to go about this, but it seems like someone has probably worked on this before, so I can base my work on previous works. It's a pretty essential part of Haskell, so it is certainly going in.
#4 Would be quite difficult. I probably wouldn't be able to include this. Instead I will require explicit type annotations on functions.
#5 Definitely want to include this. Should be pretty simple.
#6 Not sure about this. Will definitely require a fair bit of research on my part. It's an important part of Haskell, but I honestly have no idea how it works. It seems really cool, so I'd really like to include it.
Since my formal background in programming languages is about nil, I've slotted myself a fair bit of reading. So far today I've humped through the first 11 chapters of Types and Programming Languages. I'm not the biggest fan of the way the book goes about things, but it's not bad.
Saturday, April 7, 2007
Welcome
Howdy!
Welcome to my blog. My name is Mark Reitblatt, and I'm an undergraduate in the University of Texas (Austin) Department of Computer Sciences. The purpose of this blog is to document what I learn as I journey into the broad and deep world of Automated Theorem Proving (ATP for short). Hopefully, this will be a useful resource to other students interested in the domain of formal methods, but unsure about where to start.
Welcome to my blog. My name is Mark Reitblatt, and I'm an undergraduate in the University of Texas (Austin) Department of Computer Sciences. The purpose of this blog is to document what I learn as I journey into the broad and deep world of Automated Theorem Proving (ATP for short). Hopefully, this will be a useful resource to other students interested in the domain of formal methods, but unsure about where to start.
For the time being, my primary focus will be on the ACL2 theorem prover written by J Moore and Matt Kaufmann. Written in its own logic (based upon Common Lisp), ACL2 is the latest incarnation of the Boyer-Moore theorem prover. In 2006, the Boyer-Moore theorem prover won an ACM Software System Award.
ACL2 has seen extensive use throughout industry, being used to prove the correctness of the floating point division algorithm in the AMD K5 processor, the correctness of the first silicon implementation of the JVM and the correctness of the pipeline hazard detection algorithm of the Motorola CAP DSP, among many other projects. One current project is constructing a model of the Java Virtual Machine in order to prove theorems about programs written in JVM Bytecode.
In my next post I'll talk about my current goals with ACL2, namely my ideas for my Bachelors Honors Thesis.
ACL2 has seen extensive use throughout industry, being used to prove the correctness of the floating point division algorithm in the AMD K5 processor, the correctness of the first silicon implementation of the JVM and the correctness of the pipeline hazard detection algorithm of the Motorola CAP DSP, among many other projects. One current project is constructing a model of the Java Virtual Machine in order to prove theorems about programs written in JVM Bytecode.
In my next post I'll talk about my current goals with ACL2, namely my ideas for my Bachelors Honors Thesis.
Subscribe to:
Posts (Atom)