Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Date: Tue, 31 Aug 93 09:26:18 EDT
From: shb@oracorp.com
Message-Id: <9308311326.AA00262@sparta.oracorp.com>
To: info-hol@dworshak.cs.uidaho.edu
Subject: Useful trick: invocations

Shui-Kai Chin and I used a trick in our HUG93 paper, ``Server-Process
Restrictiveness in HOL'', that can be used to effectively define a
concrete recursive type T in terms of a finite number of arbitrary
HOL-definable T-valued functions.  The trick requires no additions or
modifications to the usual define_type.  I described the trick to
several people at HUG93 that I thought might be able to use it,
particularly those working on defining an operational semantics for SML
in the HOL object language, and one of these people, Donald Syme,
thought the trick was worth a note to info-hol.  Here is that note.

The idea for the trick is that although it is not possible to use
define_type to define a concrete recursive type T in terms of T-valued
functions, it is possible to use it to define T in terms of *names* for
the T-objects returned by particular T-valued functions.  The names,
which we call ``invocations'', are given by a concrete recursive type N
whose constructors correspond to the particular T-valued functions used
in the definition of T.  A separate function, a function defined with
new_recursive_definition, maps the invocations to the T-objects that
they name;  the interpretation of T-objects varies with the mapping of
N to T.  For example, if foo is a function mapping nums to T-objects,
FOO can be taken as the corresponding constructor mapping nums to
invocations, and then the ``correct'' function mapping invocations to
T-objects maps (FOO x) to (foo x).

I believe the general trick is called ``naming'' in computer science.
The constructors for the type N of invocations are analogous to
function declarations, as opposed to definitions, in C, but the
invocation constructors give the types of functions' arguments rather
than the types of their return values -- the type of the return values
is always T.

Our paper gives an example of using the trick to define a process
specification language as a concrete recursive type, define an
operational semantics for this language, and specify a simple process
in this language.

Steve Brackin
ORA