Notes on linking HOL and ACL2

Contents Comments and questions are in red and highlighted like this.



The plan is to provide a semantically coherent link between the higher order logic supported by HOL4 and the logic and programming logic supported by ACL2.

The official specification of ACL2 can be found in the papers A Precise Description of the ACL2 Logic and Structured Theory Development for a Mechanized Logic.

ACL2 has a number of features that make it highly suitable for system modelling. Our goal is to enable HOL users to employ ACL2 as a trusted oracle. A specific case study we have in mind is to experiment with ACL2 for executing the verified ARM model due to Anthony Fox.


In 1999 Mark Staples implemented a tool for called ACL2PII for linking ACL2 and HOL. This was built with an early version of the Prosper Toolkit. It was quite successful, and was used by Susanto as part of his AMBA-ARM7 Formal Verification Platform.

ACL2PII is our starting point. However, the Prosper Toolkit, though influential and successful in its time, is no longer supported and HOL methodology has moved on. In particular, Konrad Slind has been developing a polytypism methodology for systematically processing and translating higher order logic terms. One (of several) applications is the translation from higher order logic to ML programs, so that ML can be used as an execution oracle for ground HOL terms.

One of the tricky things about translating from the untyped ACL2 logic to typed higher order logic is figuring out which types to assign. An example Staples gives is that, depending on the context, the ACL2 S-expression NIL might need to be translated to F (falsity of HOL type bool), or [] (the empty list) or NONE (the empty option). The ACL2PII user has to set up "translation specifications" that are pattern-matching rewrite rules to perform the ACL2 to HOL translation. These are encoded in ML and are thus outside the fully-expansive LCF methodology (and so may introduce inconsistency).

Inspired by Konrad's polytypism methodology, it is hoped to use a deeper linking, with families of semantic functions defined in higher order logic to perform the coding/decoding bewtween higher order logic and the ACL2 S-expressions. These Slind-style translation functions will be based on a semantics of the ACL2 logic in HOL (deep embedding) and should enable some formal assurance that the translations between the logics is sound. In Appendix A of Linking ACL2 and HOL, Staples gives the following definition of ACL2 S-expressions in HOL:

type_abbrev("packagename", ``:string``);
type_abbrev("name",        ``:string``);

 `sexp = ACL2_SYMBOL    of packagename => name
       | ACL2_STRING    of string
       | ACL2_CHARACTER of char
       | ACL2_NUMBER    of num
       | ACL2_PAIR      of sexp => sexp`;

Define `ACL2_NIL = ACL2_SYMBOL "ACL2" "NIL"`
Define `ACL2_T = ACL2_SYMBOL "ACL2" "T"`
Numbers in ACL2 are complex rationals (complex numbers with rational realpart and imagpart) and characters (i.e. ACL2_CHARACTER) lie in the range [0,256), and the HOL type ascii is now renamed to char, so this type above this isn't quite right.

There is one piece of background that may (but probably won't) turn out to be useful. This is the (somewhat unsuccessful) attempt to translate between untyped ZF set theory and higher order logic. The approach used was, like Staples', quite "shallow" (i.e. performed by metalanguage scripts rather than by proof). This endeavour floundered because the logical foundation of the translation scripts wandered into parts of set theory where I was out of my depth. I came away from the exercise feeling that it needed to be done more inside higher order logic, so as to ensure the various logical transformations were formally validated by HOL. This colours my reading of Staples' more successful ACL2PII work, and is one reason why I want to try a "deeper" approach to embedding.

Several people have looked into linking classical and constructive higher order logics. For example, Encoding the HOL Light logic in Coq - Freek Wiedijk, Importing Isabelle Formal Mathematics into NuPRL - Naumov (1999) and Semantic foundations for embedding HOL in Nuprl - Howe - 1996. These and similar papers tend to have scary math, but there might be some insights lurking in them.

First steps

This project has a backpack page here. For access contact Mike Gordon.


Page maintained by Mike Gordon.
Version 1.04, Mon Aug 02, 2004
Version 1.06, Fri Aug 27, 2004