Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Date: Thu, 22 Apr 93 13:37:07 +0200
From: blok@cs.utwente.nl (Rintcius Blok)
Message-Id: <9304221137.AA28029@apollo.cs.utwente.nl>
To: info-hol@ted.cs.uidaho.edu

From deby@cs.utwente.nl Tue Apr 20 13:31:33 1993
Return-Path: <deby@cs.utwente.nl>
Received: from zoo.cs.utwente.nl by apollo.cs.utwente.nl (4.1/RBCS-2.0)
	id AA24659; Tue, 20 Apr 93 13:31:32 +0200
Date: Tue, 20 Apr 93 13:31:32 +0200
From: deby@cs.utwente.nl (Rolf de By)
Message-Id: <9304201131.AA24659@apollo.cs.utwente.nl>
To: blok, seven@dbis.informatik.uni-frankfurt.de
Subject: Re: an earfull
Forwarding: Mail from '" (Susan Johanna Even)" <seven@dbis.informatik.uni-frankfurt.de>'
     dated: Tue, 20 Apr 1993 14:48:00 +0200
Status: RO


Hi,

Suzan Even and Rolf de By (both conducting my research)
asked me to forward the following message to the HOL mail list.
So here it comes,

  Rintcius Blok

------------------------------------------------------------


Greetings HOL researchers/fanatics/hackers:

We are interested in extending the HOL system in order to provide
_indexed product types_ (labeled record types) for use in modeling
object-oriented databases.  Our database group is studying
transaction verification for object-oriented databases (dot dot dot).
We have chosen to use the HOL system because the types currently
supported by theories in the system, set types in particular, are
well-suited for our work.  However, we have encountered several
difficulties in designing a suitable representation type for labeled
records using the type definition facilities currently available in
the HOL system. Our database model is based on the Cardelli type system,
which includes subtyping.

If we represent records with finite function graphs, we must introduce
disjoint union types as the codomain.  This results in cumbersome
injection and projection operations becoming a part of the theory.
A similar problem arises with domain definition in traditional
denotational semantics: domains such as
	"Denotable-Value = Bool + Nat + Char + ..."
are introduced in order to union together different collections of
values into a common domain that can then be used as the codomain/result
type of a function.  Record types are then modeled as functions with
semantic domain "Record-Type = Identifier -> Denotable-Value".
We require more detailed typing information than simply "Denotable-Value"
for the component fields of a record. (For instance, record types may be
nested to arbitrary depth!) We would like the result type of record field
selection to actually be the exact type of the component selected.

If we represent records with product types, we are limited to a fixed
number of fields. As a result, we must define separate representations for
each different record width, using distinct types in the underlying ML
metalanguage.  This becomes problematic when we consider relations among
types such as subtyping, since the types we want comparable at the HOL
level are not comparable at the ML level. As a consequence, we are unable
to define a _general_ theory for records.

Our theory of subtyping is based on set inclusion on the underlying domains,
having the notion of "minimal type" (i.e., the most precise type
characterization) [Balsters & Fokkinga, Subtyping can have a Simple
Semantics, Theor. Comp. Sci. 87 (1991), 81-96].
In addition to the subtype relation "<=",
we use the operations "greatest lower bound" and "least upper bound" on types.
We want to model records by _indexed products_types in HOL, implemented
using the underlying ML metalanguage type "(string # type) list".
Having the representation directly implemented in ML would allow us
to define type comparison operators at the ML level for HOL types which
are incomparable at the HOL level in the current system.  Our theory
of subtyping would then be defined in HOL in terms of these types.

In addition to record types, we also have variant types. We wish
to extend the collections of type and term expressions in the HOL
system in the following ways (where "**" denotes a new BNF rule):

<type-exp> ::=
            <atomic-type-name>
          | <type-var>
          | ( <type-exp1> , ... , <type-expN> ) <type-operator-name>
          | <type-exp1> -> <type-exp2>
1**       | < <label1> : <type-exp1> , ... , <labelN> : <type-expN> >
2**       | [| <label1> : <type-exp1> , ... , <labelN> : <type-expN> |]

<term-exp> ::=
            <constant-term>
          | <term-var>
          | <term-exp1> <term-exp2>
          | ( lambda <term-var> dot <term-exp> )
3**       | < <label1> = <term-exp1> , ... , <labelN> = <term-expN> >
4**       | [| <label1> = <term-exp1> , ... , <labelN> = <term-expN> |]
5**       | <term-exp> dot <label>
6**       | <term-exp> is <label>
7**       | case <term-exp> of ...

The **'d rules require implementation of record (**1) and variant (**2) types,
implementation of record and variant-typed term constructors (**3 and **4),
and implementation of their corresponding destructors (**5, **6, and **7).

Hopefully, you or someone in your group could give us some idea of
how difficult it would be to extend the HOL system with these constructs,
which is something that _we_ are contemplating. It is, however, difficult
to judge how much work would be involved, which parts of the HOL system
need to be augmented, et cetera. If possible, could you give us a general
outline of how to proceed with kernel modifications?

We hope there would be enough interest in these extensions to the system
that our work could be incorporated into future versions of the system
for general release.  If you are aware of other researchers currently
working on similar extensions to the system, please point us in their
direction!