Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: donald.syme@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:293460:950411184033"@cl.cam.ac.uk> (message from Donald Syme on Tue, 11 Apr 1995 20:40:01 +0200)
Subject: Re: Preterms and term location specifications
Message-Id: <95Apr12.161822met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 12 Apr 1995 16:18:11 +0200


> I am wondering whether the internals of the preterm signature in hol90
> should be publically available or not.  (It isn't at the moment.)

Yes, it should be! Otherwise hol90 will never be able to emulate the
magisterial syntactic manipulations that Mike Gordon has performed in
the course of embedding Hoare Logic and Z in hol88.

> [Note "_" is allowed as a variable name in hol90.  A small
> problem with the term lexical analyser actually means the above
> won't pass syntax checking, but a term such as
> 
>         (--`_ /\ _ /\ P /\ _`--)
> 
> will.  The problem is with the !_.

Phrases such as

    !_. M

won't work because "!_" is taken to be a single lexeme. (A minor
extension to the parser is also necessary.) The same problem crops up
with identifiers incorporating ":", ",", and "~"; one wants these to be
both separate names in their roles as delimiters (or prefixes) and also
subcomponents in names, e.g., one might want to use "::" as an infix
version of "CONS". Aside from that, expressions such as

>   "!_. (_ = [P;_]) /\ _ /\ Q"

won't be as general as wished because the "_" as a variable is not
polymorphic (let-bound polymorphism only arises from constants in
HOL). On the other hand, if the "_" had been declared as a constant, the
expression would be deemed silly at the point of attempting to quantify
over a constant. I suppose one could teach the parser that underscores
in binding occurrences are to be treated as variables, and all other
occurrences of underscores are to be treated as instances of a
polymorphic constant.

> Using preterms for these seems suitable, as I don't care about type
> inference.  Another option would be to use lambdas, but there is no
> parse support for these.  A third option, and perhaps the best, would
> be to tweek the term type checker so that setting a flag would let
> conflicting types be inferred for variables (or just the variable _),
> and also assume polymorphic types for all unconstrained type
> variables.  These would still be type-correct terms, after all.  Then
> we could define a new term parser, say "-|" -|`!_. _ /\ _ /\ P /\ _`|-

It may be less effort to operate off of preterms and dodge the type
inference issue entirely. I would just make the preterm datatype
visible. (Extra pain warning - preterms will need a prettyprinter for
any serious use!) The only difficulty then is that many term operations,
such as computing free variables, are unavailable in preterms. Since the
aim of this exercise, as I understand it, is to give "director terms"
for operations, the preterm structure should suffice.

> To be honest, such parser behaviour would be useful in other situations 
> too.  I often want to know a general type for a polymorphic constant,
> as in
> 	type_of (-|`$RES_FORALL`|-)

How about "type_of o #const o const_decl"?


Konrad.