Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Subject: Semantics of HOL
Date: Tue, 27 Jun 1995 11:47:28 +0200
From: schneide <schneide@ira.uka.de>
Message-Id: <"irafs1.ira.130:27.06.95.09.49.35"@ira.uka.de>


I have two simple? questions concerning the semantics 
of HOL.

(1) Semantics of the type operator ->. 
    In the chapter on the semantics of HOL in the HOL 
    documentation, the type a -> b is defined to be 
    the set of a l l functions from the set assigned 
    to a to the set assigned to the type b. 
      However, in type frames the type a -> b is more 
    generally defined to be the set of s o m e  functions 
    from the set assigned to a to the set assigned to the 
    type b (see e.g. Andrew's book). E.g. a and b assigned 
    to cpos, this definition allows to assign a -> b the 
    set of all continous functions which form a strict 
    subset of the set of all functions (if a and b assigned 
    to cpos).
      In the HOL documentation it is stressed that the 
    semantics is the set of all functions, but it is not 
    mentioned (and also not clear to me) if this means a 
    real restriction or not?

(2) Type abstraction and application.
    Some (predicative) polymorphic lambda calculi allow 
    abstraction over type variables. Therefore, some
    useful terms like \a.\(x:a).x can be constructed,
    where a is a type variable and x is a term variable.
    The semantics of \a.\(x:a).x is a function which
    maps a set of the universe on its identity function.
    Assume, we would add the syntax of terms to contain
    type abstraction and application. We also would have 
    to add type abstractions to the semantics of HOL by 
    new rules for beta reducing type-beta redici (terms 
    like (\a.\(x:a).x) bool yielding \(x:bool).x).
      Therefore, it would be straightforward to extend the
    syntax and semantics of HOL to type abstraction and
    application, isn't it? It would the be possible to
    define terms like (--`let f = \x.x in (f 0, f T)`--)
    similar to SML, which is currently not possible in HOL.
      I know there is a paper of Th.Melham which considered 
    universal quantification on type variables, but the 
    abstraction over type variables would be even more 
    powerful.


Can anybody answer the questions?