Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic

P. Sreeranga Rajan

Department of Computer Science, University of British Columbia, Vancouver B.C, Canada, sree@cs.ubc.ca OR sree@cs.stanford.edu

Abstract

Formal methods for hardware design and software engineering have become increasingly essential to avoid costly errors. But, this justification for using formal methods needs to be supported by their ease of use. Classical Higher Order Logic (HOL) has provided a foundation for formal verification. However, specification and verification in HOL is, invariably, fairly involved. Often it is desirable for the specifier to increase one’s understanding of the specification by executing the specification. Evaluating specifications prior to embarking on tedious proofs may, at the very outset, lead to uncovering discrepancies, with little effort. This work attempts to provide an environment in HOL in which specifications using a subset of HOL can be executed. We accomplish this by translating HOL terms into ML programs: the translation process being totally automatic. Executing specifications as programs in a formal setting provides a way to guarantee certain properties that need to be satisfied by the specification. Furthermore, we also find that it has a potential to provide a practical insight into the evaluation semantics for classical logic.

Keyword Codes: B.7.2; F.3.2; F.4.1 Keywords: Integrated Circuits, Design Aids; Semantics of Programming Languages; Mathematical Logic.

1 Introduction

In general, theorem proving, as its underlying logic becomes more expressive, becomes less automated. HOL is more expressive among theorem provers, while being less automatic. The specifications, on which tedious proofs are carried out, could turn out to have unintended errors not uncovered by the proof process itself. In this context, the specifications would have to be modified and the proof procedure repeated. Hardware designers and software engineers are used to simulating hardware and execute programs to uncover errors. In this work, we attempt to provide an environment in which HOL terms can be transformed into ML (Meta-Language) programs, which then could be evaluated. This environment, in which HOL is equipped with evaluation, serves to detect specification errors before a tedious verification process is undertaken.

Past research in executing HOL specifications [2] has been very similar to our work. This work was also based on transforming HOL specifications into ML programs. However, transformations such as on types were not totally automated. Moreover, it concentrated on translating relational specification to functional specification in the context of hardware. Our work considers general HOL specifications with very restricted quantification. The aim of our work is also more general, and transformations we carry out are all automatic.

The paper is organized as follows: we discuss the issues in evaluating formal logical specifications in section 2, section 3 gives an overview of the translation process from HOL to ML. In section 4, we walk through the translation process with a simple example. We then give a brief discussion on the evaluation semantics for classical logic in section 5, and finally summarize our contributions in section 6. Sample evaluation sessions are included in the appendix.

2 Issues in Evaluating Specifications

There are several issues that need to be considered in providing an environment for executing formal logical specifications.

• Operational (rewrite rule) semantics for either the logic or the target language.

• The relationship between the metalanguage and the object language of the logic: whether the metalanguage can be used to express the operational semantics of the object language.

• Formalization of the object language interpreter in the object language.

The circularity, apparent in the last two issues above, may suggest a choice of a proper subset of the object language for execution.

Boyer-Moore Logic [1], a type-free quantifier-free first-order logic, resembling pure Lisp has an interpreter in Lisp, that operates on the constants of the logic that represent terms. Tableau based classical deduction has had limited success in program synthesis [6]. Theorem provers based on constructive logics have been highly successful in synthesizing programs from proofs, and thus providing a rich environment for execution of specification and verification [4]. LCF, a precursor of HOL has already been considered as a programming language in the context of relating denotational and operational semantics as part of fully abstract models for functional languages [11]. HOL, based on simple theory of types, getting its expressiveness by quantification over objects of arbitrary order leads to difficulties in designing an interpreter for it.

3 Translation Overview

The HOL subset we have targeted are HOL terms that can be safely skolemized. The execution essentially involves transforming HOL terms into ML programs. The ML programs are then interpreted by the ML interpreter. The transformation process is divided into several steps:

• Transforming HOL types into ML types:

Translation of HOL type constructors to ML recursive type constructors.

Definitions of destructors corresponding to each argument of the constructors.

• Skolemization:

Safe removal of outermost quantifiers.

Removal of redundant quantifiers.

• Transforming recursive definitions:

Identifying and splitting the recursion arguments.

Transforming pattern matching by a tree structure.

• Equational definitions:

Creation of let, letrec and lambda bindings for the arguments on the left-hand side.

• Variables are translated without change.

• Constants:

Constants such as numbers are treated as primitive ML constants. Constructors and destructors associated with such constants are defined separately in ML.

The special constant ARB is replaced by failure in ML.

• Combinations:

Translated as function applications in ML: the evaluation order comes into picture here since HOL-ML is call-by-value, many HOL combinations have to be treated by call-by-need depending on the context.

Conditionals are explicitly translated as if-then-else statements in ML: this is a key example in considering the evaluation order.

• Abstractions are translated as lambda abstractions in ML.

The translation of partial specification in HOL to escape or failure construct in ML leads to a non-functional program. The partial specification, might be explicitly indicated by introducing the special constant ARB in the definitional specifications. Also, partial specifications might come about, in part, due to the axiom of choice and the excluded middle in classical logic. Failure or catch-throw in programming languages is considered^{1} a non-functional feature. This hints at classical logic as a foundational basis for the semantics of non-functional programming languages [9].

1by purists

4 Example Translation: Step by Step

4.1 Translating Type Definitions

Consider the recursive type definition in HOL:

let stack =
define type ‘stack Axiom‘
‘stack =
ST ACK EMP T Y |
ST ACK NODE ∗ stack‘; ;

It is a polymorphic stack recursive type introducing two constructors: ST ACK EMP T Y and ST ACK NODE. We first translate it into an ML recursive type definition:

rectype ∗ stack =
ST ACK EMP T Y |
ST ACK NODE of ∗ # ∗ stack; ;

We note that the ML type constructors are uncurried unlike their HOL counterparts. Then, we introduce the destructors corresponding to the two arguments to the second (recursive) type constructor STACK NODE:

let dest ST ACK NODE1 (ST ACK NODE(v, s))
= v; ;
let dest ST ACK NODE2 (ST ACK NODE(v, s))
= s; ;

4.2 Translating Equational Definitions

We will consider a recursive definition in HOL using the stack recursive type defined above. It defines the P OP operation on the stack - popping an empty stack is specified by ARB, and popping any other stack gives a stack with the top element removed.

The definition in HOL appears as follows:

let P OP =

new recursive definition false stack ‘P OP ‘ “(P OP (ST ACK EMP T Y ) = ARB) ∧ ∀v s. (P OP (ST ACK NODE v (s : (∗)stack)) = s)′′; ;

We first skolemize the above term by removing the universal quantifications on the variables v and s. We then transform the pattern-matching style definition on the RHS into a tree-style definition in HOL by

• Substituting one constructor variable for all the constructor combinations:

Cons V ar substituted for ST ACK EMP T Y and (ST ACK NODE v s)

• Substituting destructor combinations for each of the arguments of a constructor - the substitution is actually delayed till execution by creating let declarations for the arguments:

let v = dest ST ACK NODE1 (Cons V ar)

let s = dest ST ACK NODE2 (Cons V ar)

We arrive at this HOL term by using the above transformations:

P OP Cons V ar =
((Cons V ar = ST ACK EMP T Y ) ⇒
ARB |

let s = dest ST ACK NODE2 (Cons V ar) in let v = dest ST ACK NODE1 (Cons V ar) in

s; ;

We then carry out the final transformations into an ML program:

• Transform the conditional HOL combination into an if-then-else statement and replace the constant ARB by failure:

if (Cons V ar = ST ACK EMP T Y ) then

failwith ‘partial specification‘ else let s = dest ST ACK NODE2 (Cons V ar) in let v = dest ST ACK NODE1 (Cons V ar) in

s

• Introduce the lambda binding for the variable on the RHS:

λCons V ar.

if (Cons V ar = ST ACK EMP T Y ) then

failwith ‘partial specification‘ else let s = dest ST ACK NODE2 (Cons V ar) in let v = dest ST ACK NODE1 (Cons V ar) in

s

• Introduce letrec binding for the function name on the LHS:

letrec P OP =

λCons V ar. if (Cons V ar = ST ACK EMP T Y ) then failwith ‘partial specification‘ else let s = dest ST ACK NODE2 (Cons V ar) in let v = dest ST ACK NODE1 (Cons V ar) in s

Several examples involving compiler specifications, microprocessor specifications, boolean arithmetic functions have been executed successfully.

5 Limitations

The limitations of the translation come about due to the expressiveness of the HOL logic itself and the evaluation order of the ML language associated with the HOL environment:

• Type definitions: currently there is no logical way to identify the type constructors apart from other constants in a theory:

We adopt a convention that the ML key for a type definition to be the <Type name> Axiom.

• Quantification:

Hilbert choice operator ϵ cannot be translated.

User introduced quantifiers are not handled.

Arbitrary quantification using ∀ and ∃, may not be safely skolemized.

• “Lazy” combinations: several combinations in HOL whose rewrite rules correspond a call-by-need evaluation order, though are translated as applications, do not evaluate in ML to the expected result. This is due to HOL ML being call-by-value. One such special case is the translation of the special constant ARB by failure.

6 Towards Evaluation Semantics

The target language of our translation being ML and that the interpreter being written in ML itself has several advantages:

– ML being the metalanguage for HOL, the specifications can be executed in the HOL environment itself.

– ML has a well-defined formal dynamic and static semantics: the interpreter can be formalized in HOL.

A set-theoretic denotational semantics has been defined for HOL [5]. However, its operational semantics has not yet been fully investigated.

It is well known that functional programs can be extracted from proofs in constructive logics. One way to understand this is that the Curry-Howard isomorphism underlying constructive type theories identifies propositions as types with an associated semantics of evidence [3]. Thus, informally, proofs can be viewed as programs and evidence viewed as values. Furthermore, constructive logics provide foundations for functional programming languages.

On the other hand, classical logic cannot be directly interpreted to have existence properties. However recent work [7, 8, 10, 12] has shown that classical proofs by appropriate translations to constructive logic can, indeed, be associated with computations. This work was done in the context of semantics for imperative programming languages, using appropriate translations to functional languages and constructive logics.

7 Summary and Future Work

We believe that our environment would be useful to HOL researchers and practitioners as an aid to quicker development of defect-free specifications, leading to a better understanding of HOL specifications. Furthermore, evaluating specifications as programs in a formal setting serves to guarantee certain properties intended to be satisfied by the specification. Besides providing a useful tool for practitioners, this work could provide further insight into formulating an evaluation semantics for HOL, leading to HOL proofs as programs. On the other hand, it also provides an insight into classical logic forming the foundations of non-functional programming languages.

Acknowledgements

The author thanks Jeff Joyce and Carl Seger for their constant encouragement and reviews. Many of the ideas in this paper could not have come about without a long association with, and constant mentoring by Carolyn Talcott. The author also thanks Chet Murthy for providing a better understanding of his work on classical proofs as programs.

References

[1] Boyer, Robert S. and Moore J Strother , ‘A Computational Logic Handbook’, Academic Press, 1988.

[2] Camilleri, Albert J., ‘Executing Behavioural Definitions in Higher Order Logic’, PhD Thesis, University of Cambridge 1988.

[3] Constable, Robert, ‘Semantics of Evidence’, Department of Computer Science, Cornell University Technical Report, 1986

[4] Constable, Robert, et. al. , ‘Implementing Mathematics with the Nuprl Proof Development System’ Prentice Hall, 1986.

[5] Gordon, M. J. C. , ‘The HOL Description’, Dec. 1990.

[6] Manna, Zohar and Waldinger, Richard, ‘A Deductive Approach to Program Synthesis’, Manuscript: Stanford University CS257 Course

[7] Murthy, Chetan R., ‘An Evaluation Semantics for Classical Proofs’, in: Proceedings of the Fifth Annual Symposium on Logic in Computer Science, IEEE, 1991.

[8] Murthy, Chetan R., ‘Classical Proofs as Programs: How, What and Why’ in: Technical Report TR 91-1215 , Department of Computer Science, Cornell University, July 1991.

[9] Murthy, Chetan R., ‘Extracting Constructive Content from Classical Proofs’, PhD Thesis, Department of Computer Science, Cornell University, 1990

[10] Murthy, Chetan R., Personal Communication

[11] Plotkin, G. D. , ‘LCF Considered as a Programming Language’, in: Theoretical Computer Science, 5:223-255, 1977 .

[12] Talcott, Carolyn L., Personal Communication

Appendix: Example Evaluation Sessions

logic[1] hol
          _________
   |___|__|   |  |   |     |__|  |__|
   |      |  |   |__|   |__|__|  |__|
          Version 2.0, built on 15/7/92
#set_search_path (
    append (search_path())
           [`/isd/local/generic/src/hol-exec/ML_interpreter1.1/`]
                );;
###() : void
##loadf `hol-eval_setup`;;
......Loading library `string` ...
Updating search path
.Updating help search path
.Theory string loaded
......
Library `string` loaded.
...........................() : void
#eval "3+2";;
` FIX_PLUS  ( 3 ) ( 2 );;
` : string
#new_theory `foo`;;
() : void
#let fact = new_prim_rec_definition (
           `fact`,
           "(fact 0 = 1) /\
            (fact (SUC n) = (SUC n) * (fact n))");;

###fact = |- (fact 0 = 1) /\ (!n. fact(SUC n) = (SUC n) * (fact n))
##exec `foo` [] [];;
Translating HOL definitions in foo and its parents ...
Loading derived ML definitions in foo_hol.ml ...
.................................
Type a function name to evaluate or
Type "eval <hol_term>;;" to evaluate a new <hol_term> or
Type "exit();;" to exit
`#` : string
hol-exec> fact 10;;
3628800 : int
hol-exec> exit();;
`hol-exec> ` : string
#close_theory();;
() : void
#quit();;
Bye.
logic[2] exit