Via:  uk.ac.ucl.cs.nss; 6 Dec 88 18:14 GMT  (UK.AC.Cam.Cl.scaup)
Date: Tue, 6 Dec 88 16:44 GMT
From: Mike Gordon <mjcg%uk.co.sri@com.sri.ai.warbucks>
To: info-hol@edu.ucdavis.clover
Subject: Definitions in HOL88
Message-Id: <mjcg.88.12.06.16:44.920@gwyndir>
Sender: mjcg <mjcg%uk.co.sri%com.sri.ai.warbucks%com.sri.ai.drakes%com.sri.ai.iu@edu.ucdavis.clover>
Status: R


                 |============================|
                 |                            |
                 |   HOL 88 PROGRESS REPORT   |
                 |   ----------------------   |
                 |                            |
                 |        Mike Gordon         |
                 |   Cambridge, 6 Dec 1988    |
                 |                            |
                 |============================|


As discussed at the HOL meeting, it is planned to reorganise the definition
primitives in HOL88. This note describes the planned primitive constant and
type definition mechanisms. It also raises some issues for discussion. It is
not yet too late to change things if you don't like what follows!


Constant Definitions
====================

Following a suggestion of Roger Jones of ICL, the primitive definition
mechanism of HOL has been changed to be as follows:

   If

      |- ?x. t[x]

   where "?x. t[x]" is a closed term, then a new constant,
   c say, can be introduced satisfying:

      |- t[c]

To prevent problems (discovered by Roger and others) with unbound type
variables, the type of c must include all type variables occurring
in the whole term t[c].

The purpose of this change is:

   (i)  To get around the problem that if

           |- c1 = @x.P(x)
           |- c2 = @x.P(x)

        then |- c1 = c2. This prevents "@" being used for Z-style
        loose specifications.

   (ii) To make primitive recursive definitions nicer (see below).


The ML function:

   new-constant_specification : string -> string -> string -> thm -> thm

is used to make constant definitions as described above. Evaluating:

   new-constant_specification `flag` `name` `c` (|- ?x. t[x])

introduces a new constant named c satisfying the property:

   |- t[c]

If `flag` is `constant` then c is declared an ordinary constant, if it is
`infix` then it is declared an infix and if it is `binder` then it is declared
a binder.  Any other value of flag causes an error. This theorem is stored,
with name `name`, as a definition in the current theory.

The existing definitional primitives:

   new_definition
   new_infix_definition
   new_binder_definition

can be defined in terms of new_constant_specification.

The primitive recursive definition mechanisms have been changed so that the
recursion equations become stored as definitions rather than theorems. Given a
primitive recursion theorem (as generated by Tom Melham's package) of the
form:

   |- !f0 f1 f2 e. ?! fn.
      (!x0 x1 t t'. fn(C1 t x0 t' x1) = f0(fn t)(fn t')x0 x1 t t') /\
      (!t. fn(C2 t) = f1(fn t)t) /\
      (!x. fn(C3 x) = f2 x) /\
      (fn C4 = e)

and a candidate recursive definition, presented as a term:

   "(!n b. Fn n C4 b = ...) /\
    (!b n m t x t'. Fn n (C1 t' b t m) x = ...) /\
    (!m x q. Fn m (C3 x) q = ...)"

Tom Melham's general tool is used to prove a theorem of the form:

   |- !e f0 f2. ?fn.
      (!g1 g2. fn C4 g1 g2 = e g1 g2) /\
      (!g3 g4 g5 g6 g7 g8. fn(C1 g5 g3 g6 g4) g7 g8 =
                               f0(fn g5)(fn g6)g3 g4 g5 g6) g7 g8 /\
      (!g9 g10 g11. fn(C3 g9) g10 g11 = f2 g9 g10 g11)

and this is then fed to new_constant_specification to make the definition:

   |- !e f0 f2.
      (!g1 g2. Fn C4 g1 g2 = e g1 g2) /\
      (!g3 g4 g5 g6 g7 g8. Fn(C1 g5 g3 g6 g4) g7 g8 =
                               f0(Fn g5)(Fn g6)g3 g4 g5 g6) g7 g8 /\
      (!g9 g10 g11. Fn(C3 g9) g10 g11 = f2 g9 g10 g11)

which is stored as a definition, not as a theorem.

Note that in HOL88, the recursion equations defining the built-in constants
listed below are retrieved using definition not (as in old HOL) using
theorem.

   ADD, SUB, MULT, EXP,
   NULL_DEF, HD, TL, SUM, APPEND, FLAT, LENGTH, MAP, EL, EVERY_DEF


Some issues for discussion
--------------------------

What I have said above is not quite accurate. Since "?" is presupposed by the
definition mechanism, this mechanism cannot be used to define it.  (currently
"?" is defined by |- (?x.P(x)) = P(@x.P(x))). There are two obvious solutions
to this:

   1. Retain a stripped down version of the old definition
      mechanism as a primitive.

   2. Reorganise the core logic with "?" instead of "@" as primitive.

Option 1 is the one I have currently implemented as it requires least work;
however option 2 might be quite elegant. Various people have complained that
taking "@" as primitive is weird. With 2, "@" could be defined from the
following version of the Axiom of Choice.

   |- ?f. !P. (?x. P x) ==> P(f P)

The snag with 2 is that I don't know a satisfying logical basis based
on "?" rather than "@" (e.g. will the Axiom of Choice need to be an axiom).

Does anyone have any suggestions and/or views on this. From the user's point
of view the choice between 1, 2 or some other scheme doesn't make much
difference. The tools used in practice will be the same.

A second issue is whether the definition primitive should allow simultaneous
definitions, i.e.:

   If

      |- ?x1 x2 ... xn. t[x1,...,xn]

   then c1, c2, ... , cn can be simultaneously defined satisfying:

      |- t[c1,...,cn]

This scheme is redundant; it is possible to make a sequence of single
definitions of c1, ... , cn so that |- t[c1,...,cn], however these definitions
will look complicated when the theory is printed.
I am currently veering towards make simultaneous definitions primitive for
two reasons:

   1. Tom tells me it will simplify the implementation of simultaneous
      recursive type definitions.

   2. It will increase compatibility between HOL and Z.

What do you think?


Type Definitions
================

The HOL88 type definition primitive is slightly different from the old one.
Executing:

   new_type_definition(`ty`, "P", |- ?x. P x)

yields the definitional axiom:

   |- ?rep. TYPE_DEFINITION P rep

which is stored as a definition, not as an axiom as in old HOL.
The constant TYPE_DEFINITION is defined by:

   |- TYPE_DEFINITION (P:*->bool) (rep:**->*) =
       (!x' x''. (rep x' = rep x'') = (x' = x'')) /\
                 (!x. P x = (?x'. x = rep x'))

The ABS and REP constants are defined automatically.

There are two ways to interpret a type definition:

   new_type_definition(`ty`, "P", |- ?x:ty'. P x)

that appear to avoid the unbound type variable problems
Roger Jones spotted.

   1. Introduce a new type operator ":(*1,...,*m)op"
      where ":*1", ... , ":*m" are the free type variables
      occurring in ":ty'". To prevent inconsistency, it must be
      checked that ":*1", ... , ":*m" are the only type variables
      occurring in "P".

   2. Introduce a new type operator ":(*1,...,*m,...,*n)op"
      where ":*1",...,"*n" are all the type variables occurring in
      "P" (including those not in ":ty'").

Option 2 has been tentatively taken as it seems more general. It makes
it easy, for example, to define a type operator ":(*)retract" such that

                  *-
                  | {0}     if ty has two or more members
   (ty)retract =  <
                  | {0,1}   if ty has only one member
                  *-

Does anyone have any views on this?


Finally, here is yet another version of the patch for upgrading old HOL to
have nice HOL88-style error messages. Previous patches I sent to info-hol had
bugs (thanks to Phil Windley and others for pointing them out). Please try the
patch and let me know if you have problems; it can be compiled with liszt.


;========================= patch.l =========================


(eval-when (compile)
 (special %term %link-names %type_error-flag %stickylist
          %show_types-flag %printtypes %linkcount %canonlist)
)


; Some system macros
(defmacro dml (ml-fn n lisp-fn mty)
  `(declare-ml-fun (quote ,ml-fn) (quote ,n) (quote ,lisp-fn) (quote ,mty)))

(defmacro new-exit (name . body)
  `(throw (progn ,@body) ,name))

(defmacro make-var (name ty) `(cons 'var (cons ,name ,ty)))
(defmacro is-var (tm) `(eq(car ,tm)'var))
(defmacro get-var-name (tm) `(cadr ,tm))

(defmacro make-const (name ty) `(cons 'const (cons ,name ,ty)))
(defmacro is-const (tm) `(eq(car ,tm)'const))
(defmacro get-const-name (tm) `(cadr ,tm))

(defmacro make-abs (var body ty) `(cons 'abs (cons (cons ,var ,body) ,ty)))
(defmacro is-abs (tm) `(eq (car ,tm) 'abs))
(defmacro get-abs-var (tm) `(caadr ,tm))
(defmacro get-abs-body (tm) `(cdadr ,tm))

(defmacro make-comb
 (rator rand ty) `(cons 'comb (cons (cons ,rator ,rand) ,ty)))
(defmacro is-comb (tm) `(eq (car ,tm) 'comb))
(defmacro get-rator (tm) `(caadr ,tm))
(defmacro get-rand (tm) `(cdadr ,tm))

(defmacro get-type (tm) `(cddr ,tm))
(defmacro put-type (tm ty) `(rplacd (cdr ,tm) ,ty)) ; used in F-thyfns

(defmacro term-class (tm) `(car ,tm))

; types

(defmacro make-type (tyop tyargs) `(cons ,tyop ,tyargs))
(defmacro get-type-op (ty) `(car ,ty))
(defmacro get-type-args (ty) `(cdr ,ty))

(defmacro make-vartype (name) `(cons '%VARTYPE ,name))
(defmacro is-vartype (ty) `(eq (car ,ty) '%VARTYPE))

(defmacro type-class (ty) `(car ,ty))

(defmacro is-antiquot (ob) `(eq (car ,ob) '%ANTIQUOT))

; Miscellaneous macros

(defmacro ptoken (str)
  `(pstringlen (quote ,str) ,(flatc str)))

(defmacro failwith (tok)
  `(new-exit evaluation ,tok))

(defmacro while (test . body)
  `(prog ()
      *etiq* (cond (,test ,@body (go *etiq*))
                   (t (return nil)))))

(defmacro incr (var val)
 `(setq ,var (if (null ,val) (add1 ,var) (add ,var ,val))))

(defmacro newl (var val)
  `(setq ,var (cons ,val ,var)))

(defun q-typeof (tm) (get-type (strip-antiquot tm)))

(defun strip-antiquot (ob) (while (is-antiquot ob) (setq ob (cdr ob))) ob)

; From F-ol-syntax.l

; MJCG 13/11/88 for HOL88
; Function for making a partially evaluated term printable
; (remove antiquotations etc)
(defun prep-term-fn (tm)
 (selectq (term-class tm)
   (var (make-var (get-var-name tm) (prep-ty-fn(get-type tm))))
   (const (make-const (get-const-name tm) (prep-ty-fn(get-type tm))))
   (comb (make-comb (prep-term-fn(get-rator tm))
                    (prep-term-fn(get-rand tm))
                    (prep-ty-fn(get-type tm))))
   (abs (make-abs (prep-term-fn(get-abs-var tm))
                  (prep-term-fn(get-abs-body tm))
                  (prep-ty-fn(get-type tm))))
   (%ANTIQUOT (prep-term-fn(cdr tm)))
   (t  (failwith
         "Error in Lisp function prep-term-fn -- please report"))))

(defun prep-term-for-print (tm)
 (let ((tm1 (add-term-links tm)))
      (let ((%link-names (make-link-names(get-term-links tm1))))
           (prep-term-fn tm1))))

; MJCG 2/12/88 for HOL88
; Replace (%LINK) by (%LINK . N) in a term
; side effects %linkcount
(defun add-term-links (tm)
 (selectq (term-class tm)
   (var (make-var(get-var-name tm) (add-type-links(get-type tm))))
   (const (make-const(get-const-name tm) (add-type-links(get-type tm))))
   (comb (make-comb (add-term-links(get-rator tm))
                    (add-term-links(get-rand tm))
                    (add-type-links(get-type tm))))
   (abs  (make-abs (add-term-links(get-abs-var tm))
                   (add-term-links(get-abs-body tm))
                   (add-type-links(get-type tm))))
   (%ANTIQUOT (add-term-links(cdr tm)))
   (t  (failwith
         "Error in Lisp function add-term-links -- please report"))))

; MJCG 2/12/88 for HOL88
; Replace (%LINK) by (%LINK . N) in a type
; side effects %linkcount
(defun add-type-links (ty)
 (selectq (type-class ty)
   (%ANTIQUOT (cdr ty))
   (%VARTYPE ty)
   (%LINK (cond ((numberp (cdr ty)) ty)
                ((null (cdr ty))
                 (cons '%LINK (incr %linkcount)))
                (t (add-type-links(cdr ty)))))
   (t (make-type
       (get-type-op ty)
       (mapcar (function add-type-links) (get-type-args ty))))))

; MJCG 2/12/88 for HOL88
; Function for extracting %LINKs from a type
(defun get-type-links (ty)
 (selectq (type-class ty)
  ((%ANTIQUOT %VARTYPE) nil)
   (%LINK (if (numberp (cdr ty))
              (list (cdr ty))
              (get-type-links(cdr ty))))
   (t (apply (function append)
             (mapcar (function get-type-links) (get-type-args ty))))))

; MJCG 25/11/88 for HOL88
; Function for extracting %LINKs from a term
(defun get-term-links (tm)
 (selectq (term-class tm)
   (var (get-type-links(get-type tm)))
   (const (get-type-links(get-type tm)))
   (comb (append (get-term-links(get-rator tm))
                 (get-term-links(get-rand tm))))
   (abs (append  (get-term-links(get-abs-var tm))
                 (get-term-links(get-abs-body tm))))
   (%ANTIQUOT (get-term-links(cdr tm)))
   (t  (failwith
         "Error in Lisp function get-term-links -- please report"))))

; MJCG 25/11/88 for HOL88
; Make a map from %LINK numbers to print names ?, ?1, ?2 ...
(defun make-link-names (l)
 (prog (ll link-names n)
       (cond ((null l)          (return (list nil)))
             ((eq (length l) 1) (return (list(cons (car l) '|?|)))))
       (setq n 1)
       (setq ll l)
       (setq link-names nil)
  loop (cond ((null ll) (return link-names))
             ((assoc (car ll) link-names))
             (t
              (setq link-names
              (cons (cons (car ll) (concat '|?| n)) link-names))
              (setq n (add1 n))))
       (setq ll (cdr ll))
       (go loop)))

; MJCG 13/11/88 for HOL88
; Function for making a partially typechecked type printable
; (remove antiquotations, %LINK, %VARTYPE etc)
; MJCG 25/11/88 for HOL88
; Code for ?, ?1, ?2, ?3 ... added

(defun prep-ty-fn (ty)
 (selectq (type-class ty)
   (%ANTIQUOT (cdr ty))
   (%VARTYPE ty)
   (%LINK (if (numberp (cdr ty))
              (make-vartype (cdr (assoc (cdr ty) %link-names)))
              (prep-ty-fn(cdr ty))))
   (t (make-type (get-type-op ty)
                 (mapcar (function prep-ty-fn)
                         (get-type-args ty))))))

(defun prep-ty-for-print (ty)
 (let ((ty1 (add-type-links ty)))
      (let ((%link-names (make-link-names(get-type-links ty1))))
           (prep-ty-fn ty1))))

; MJCG 13/11/88 for HOL88
; Get type (stripping off %ANTIQUOT if necessary)
(defun prep-term-ty (tm)
 (if (eq (car tm) '%ANTIQUOT) (get-type(cdr tm)) (get-type tm)))

; MJCG 13/11/88 for HOL88
; Function for printing mk_comb failure error messages
(defun print-mk_comb-error (tm1 tm2)
 (progn (ptoken "Badly typed application of:")
        (pbreak 2 4)
        (ml-print_term(prep-term-for-print tm1))
        (pnewline)
        (ptoken "   which has type:         ")
        (pbreak 2 4)
        (ml-print_type(prep-ty-for-print(prep-term-ty tm1)))
        (pnewline)
        (ptoken "to the argument term:      ")
        (pbreak 2 4)
        (ml-print_term(prep-term-for-print tm2))
        (pnewline)
        (ptoken "   which has type:         ")
        (pbreak 2 4)
        (ml-print_type(prep-ty-for-print(prep-term-ty tm2)))
        (pnewline)
        (pnewline)))

; MJCG 13/11/88 for HOL88
; Flag to control printing of type errors
(setq %type_error-flag t)

; MJCG 10/11/88 for HOL88
; add error message printing
; combinations

(defun q-mk_comb (tm1 tm2)
  (let ((ty (genlink)))
       (if (unify (q-typeof tm1) (make-type '|fun| (list (q-typeof tm2) ty)))
           (make-comb tm1 tm2 ty)
           (prog2 (if %type_error-flag (print-mk_comb-error tm1 tm2))
                  (failwith '|mk_comb|)))))  ;q-mk_comb


; From F-typeol.l


; MJCG 2/12/88 for HOL88
; Make %term a special variable useable for error messages.
; for terms only.
(defun canon-quot-tm (%term)
 (selectq (term-class %term)
  (%ANTIQUOT (cdr %term))
  (comb
   (make-comb (canon-quot-tm (get-rator %term))
              (canon-quot-tm (get-rand %term))
              (canon-ty (get-type %term))))
  (abs
   (make-abs (canon-quot-tm (get-abs-var %term))
             (canon-quot-tm (get-abs-body %term))
             (canon-ty (get-type %term))))
  (var (let ((tok (get-var-name %term)) (ty (canon-ty(get-type %term))))
         (newl %stickylist (cons tok ty)) (mk_realvar tok ty)))
  (const (ml-mk_const (get-const-name %term) (canon-ty(get-type %term))))
  (t (lcferror 'canon-quot-tm))
 ))  ;canon-quot-tm

(setq %printtypes nil)
(setq %show_types-flag nil)

; MJCG 1/12/88 for HOL88
; Function for printing types indeterminate error messages
(defun print-indeterminate-error (tm)
 (prog  (save-flag)
        (setq save-flag %show_types-flag)
        (setq %show_types-flag t)
        (setq %printtypes t)
        (ptoken "Indeterminate types:")
        (pbreak 2 4)
        (ml-print_term(prep-term-for-print tm))
        (pnewline)
        (pnewline)
        (setq %show_types-flag save-flag)
        (setq %printtypes save-flag)))

; Strip all links from a type, complain if any are still undefined.
; To prevent expanding the DAG of links into a tree (which is exponential),
; retain before/after pairs of types in %canonlist
; Types beginning with %ANTIQUOT are already in canonical form.
; MJCG 1/12/88 for HOL88
; Printer of error message added
(defun canon-ty (ty)
 (cond ((assq1 ty %canonlist))
   ((selectq (type-class ty)
     (%ANTIQUOT (cdr ty))
     (%LINK (if (atom (cdr ty))
                (prog2 (if %type_error-flag
                           (print-indeterminate-error %term))
                       (new-exit evaluation "types indeterminate"))
                (canon-ty (cdr ty))))
     (%VARTYPE ty)
     (t (let ((cty (make-type (get-type-op ty)
                       (mapcar 'canon-ty (get-type-args ty)))))
          (if (get-type-args ty) (newl %canonlist (cons ty cty)))
          cty)))))
 )              ; canon-ty