Annette Bunker, Computer Science
The field of formal methods uses mathematical proof techniques to help ensure the reliability of computer systems. These proofs are complex enough to warrant the use of a proof tool. Proof tools assist system designers by enforcing logical rules. But in order to reason about designs, we must build a representation of the design within the proof tool.
There are two basic representational choices available in our proof tool, HOL88: shallow embedding and deep embedding [Tas92]. In a shallow embedding, we merely represent the meaning of the design using HOL88 terms. Deep embedding means we represent the design language itself in the logic of HOL88, allowing the designer to reason about both the design and the design language. Shallow embedding is quick and easy, while deep embedding takes more time and is more difficult. However, deep embedding allows a closer investigation of the system.
Unfortunately, there are limits in our proof tools. Until recently, mutual recursion, a very common programming technique, was not available in HOL88. Using a new package that implements non-primitive recursion in HOL88 [AF95] [Age95], I improved the deep embedding method.
My original research plan consisted of four steps.
1. Review literature for pertinent work, both in deep embedding and the use of the new non-primitive recursion package. (10/15 – 11/15)
2. Build and learn how to use the non-primitive recursion package. (11/1 – 11/15)
3. Modify an existing Scheme interpreter in HOL88, using mutual recursion. The new interpreter will be faster, cleaner and smaller. (11/15 – 1/15)
4. Compare performance of the mutually recursive embedding with the measured recursive implementation in terms of ease of development and speed. (1/1 – 1/15)
The literature review was conducted. I found several papers and other resources that proved helpful in my research. The resources that proved most helpful to me were [AF95] and [Age95]. The former was an overview paper presented to the Conference for Higher Order Logic and its Applications in 1995, while the latter is Sten Agerholm’s original technical report on the non-primitive recursion package. Sten was also very willing to answer questions and discuss problems along the way.
After spending some time studying the technical reports on the recursion package and asking its author many questions, I began working with the package directly. Building the package and duplicating the examples that Sten offered were both easy. However, when I began this project, both my advisor and I thought that Sten’s work implemented mutual recursion directly. Instead, it merely implements non-primitive recursion, the theoretical foundation for mutual recursion. This gave me the opportunity to extend the package to include mutual recursion.
The greatest difficulty in this project and the portion of it on which I spent the most time was the part that I did not know I would have to do. However, augmenting the nonprimitive recursion package to implement mutual recursion proved to be very interesting, as well as a great learning experience. I employed the parameterized technique used by Brock and Hunt in dual-eval[HB92b],[HB92a]. This technique ties the mutually recursive function calls into a single, non-primitively recursive function call. Then we can prove the mutually recursive functions correct, just as we would any other non-primitively recursive function.
For example, we would like to define a pair of mutually recursive functions that decide whether a number is even or odd like this:
let is-even = “is-even(n) = ((n = 0) => T I is-odd(PRE n)) II; ;
let is-odd = “is-odd(n) = ((n = 0) => F I is-even (PRE n) ) “; ;
These definitions say that if the number we give is_even is 0, then the function will return a true value. If the number (n) is not 0, the function will subtract 1 from it and checks to see if that number is odd. is_odd works similarly. If the input is 0, then is_odd returns a false value, otherwise, it subtracts one and asks is_even for its opinion. No matter where we start, the functions will eventually reach a point at which n = 0 (as we only deal with the natural numbers in HOL) and return the appropriate truth value.
The parameterized version pulls both functions into a single definition. The user must tell the function where to start in the input variable, flag. If n = 0 and we told it to start with even, then the function returns true. If ng0 and we started it with even, then the function will subtract one from n, tell the flag to try odd and call itself (recurse). The odd cases work similarly.
Once these definitions are made, we need only prove the correctness of the recursion according to the guidelines set out in the non-primitive recursion package. Some of this work has been automated, but some of it must be done by hand by the user.
Shortly before I finished implementing mutual recursion in HOL88, our lab was finally able to overcome the obstacles that have kept us from using HOL90, previously. HOL90 ships with a mutual recursion package, though it is fairly crude and difficult to use. One of my co-workers is currently building the non-primitive recursion package in the HOL90 tool. When he finishes this, we hope to be able to implement mutual recursion in HOL90 the same way we’ve done in HOL88.
Once the non-primitive recursive package is complete in HOL90, building mutual recursion onto it should be straight forward. I do not foresee any major differences between what I have done in HOL88 and what I will need to do in HOL90.
The original plan for performance evaluation has been scrapped, entirely. We do not care how well our method performs compared to a method that we know is inferior (ie, measured recursion in HOL88). Instead, we want to see if we can do better than the best that is currently available. We plan to evaluate performance using some HOL90 mutually recursive applications.
Should the performance analysis turn out favorably, I would like to implement some tools that automate as much of the definition process as possible. Ideally this tool would allow the user to input the mutually recursive functions, create the parameterized function, and do as much of the correctness proof as possible.
Overall, the project was a moderate success. Even though I faced some major set-backs and have been unable to complete all the goals of the project at this time, I was able to implement mutual recursion in HOL88 and improve the method of deeply embedding system representations in HOL88. Special thanks to the Office of Research and Creative Work at Brigham Young University for supporting this work.
References
- [AF95] E. Thomas Schubert Phillip J. Wiiadley James Alves-Foss, editor. Higher Order Logic Theorem Proving and Its Application,,, number 971 in Lecture Notes in Computer Science, Aspen Grove, UT, USA, September 1995. Sprinter-Verlag.
- [Age95] Sten Agerholm. A package for non-primitive recursive function definitions in hol. Technical Report 370, University of Cambridge Computer Laboratory, New Museums Site, Cambridge CB2 3QG, UK, 1995.
- [HB92a] Warren A. Hunt and Bishop C. Brock. The dual-eval hardware description language and its’ use in the formal specification and verification of the fm9OOl microprocessor. Technical Report 78, Computational Logic, Inc., 1717 W. 6th St., Suit 290 Austin, TX 78703- 4776 USA, April 1992.
- [HB92b] Warren A. Hunt and Bishop C. Brock. An introduction to a formally defined hardware description language. Technical Report 76, Computational Logic, Inc., 1717 W. 6th St., Suit 290 Austin, TX 78703-4776 USA, April 1992.
- [Tas92] Richard Boulton Andrew Gordon Mike Gordon John Harrison John Herbert John Van Tassel. Experience with embedding hardware description languages in hol. In V. Stavridou T. F. Melham R. T. Boute, editor, Theorem Provers in Circuit Design. 1992.