Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Fri, 26 Mar 93 10:49:55 EST
From: shb@com.oracorp
Message-Id: <9303261549.AA02913@sparta.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Curried/Un-Curried type constructors

Konrad Slind asked me to post questions about Curried vrs. Un-Curried
type constructors to info-hol, presumably because he wants to judge
group opinions on the issues.

I'm working on a HOL-based computer-security analysis tool that S-K
Chin and I will shortly be writing a paper about.  For the purpose of
these questions, the relevant things about the tool are that it uses
define_type type constructors and new_recursive_definition functions in
specifications, and that it's intended for Air Force and Army engineers
who are more likely to use specifications than produce proofs and are
typically not familiar with Currying as a technique for representing
multivariable functions.

What I'd like, then, are:

1. Type constructors that take un-Curried arguments.  (Available in
   HOL88, but not yet in HOL90.)

2. Type constructors with un-Curried arguments including those of the
   type being defined.  (Slind tells me that this can be done with the
   new mutually-recursive types package, but it would be better not to
   have to do something noteworthy.)

3. new_recursive_definition definitions that allowed direct reference
   to the elements of tuples, as in

     `(myfunction (foo(x,y)) = (2*x + y)) /\
      (myfunction (bar(x,y,z)) = (3*z))`

   where foo and bar are both constructors for the concrete-recursive
   type blah.

For points 2 and 3, SML/NJ allows uninhibited matching of such
patterns;  could the same algorithms be used in define_type and
new_recursive_definition?  Could object-language fragments be treated
as meta-language fragments, parsed with tools available in the meta-
language, and then be transcribed back into the object language?

Of course, another alternative would have been defining an interface
language that the engineers would see, and for proofs translating
everything into the Curried forms that the HOL community is used to,
but at the time I didn't think it would be necessary.  I do think the
HOL community would be better off, for sales purposes if no others, if
its tools supported the free use of un-Curried functions.

So what are group opinions on how difficult and how worthwhile it
would be to do these things?

Steve Brackin
ORA