Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <9875.9303291042@frogland.inmos.co.uk>
Subject: Re: Curried/Un-Curried type constructors
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Mon, 29 Mar 1993 11:42:18 +0100 (BST)
Content-Type: text
Content-Length: 5825

shb@oracorp.com has said:
> 
> 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.)

(As Konrad says in another reply) this seems to be an ommision in hol90 -
I think its due to an attempt to reuse the type parser rather than write
a new parser for the type definition!

> 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.)

I think, from my understanding on how recursive types get defined, that 
this should not be too difficult to add. However, as TFM said when first
talking about recursive types, many of the simple additions to the syntax
could be added with sufficient work but where do you stop -if you
put in pairing then what about sums or lists. Assuming the mutual type stuff
is reasonably clean to use (I haven't looked at it yet) then that seems the
better way with a simple primitive mechanism and a general method of
extension.

> 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?

I sort of investigated this idea a few months ago. E.g. I got a method
of defining e.g. a zip function from

ZIP [] [] = []
ZIP (CONS x xs)(CONS y ys) = CONS (x,y)(ZIP xs ys)

The implementation needed a lot of reworking but the outline method is as
follows.

1) take a set of defining equations with identified recursive parameters
along with the relevant recursion theorems. In example both parameters
a identified as recursing with the list recursion theorem.

2) Extend the set by adding equations by
   i) expanding any variables in recursive places by all possible top level
      expansions
   ii) adding extra equations for any combinations of recurisve parameters
       missing with arbitrary value.
   In example above we obtain

ZIP [] [] = []
ZIP (CONS x xs)(CONS y ys) = CONS (x,y)(ZIP xs ys)
ZIP (CONS x xs)[] = ARB
ZIP [](CONS y ys) = ARB

3) define with inductive definition package a relation between the 
arguments and function values from these equations. I.e. define:

------------------
ZIPrel [] [] []

------------------
ZIPrel (CONS x xs) [] []

------------------
ZIPrel [] (CONS y ys) []

ZIPrel xs ys zs
-------------------
ZIPrel (CONS x xs)(CONS y ys)(CONS(x,y)zs)

4) Prove that this relation is one to one and total when 
considered as a function

5) Define function

ZIP xs ys = @ zs. ZIPrel xs ys zs

6) Use theorems in 4 to obtain expected definition.

> 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.

Part of the problem is that in HOL you can write uncurried functions quite
easily due to support in the parser/printer, but this hides a large
amount of underlying trash which means proofs are lot more complex than
it seems. E.g. to beta reduce

(\ (a0,a1,....,an). ...) (exp0,exp1,...,expn)

is a lot more compex than it would seem from a naive inspection.

Also two things spring to mind here

i) What about proper tuples (i.e. as in SML) where (a,b,c) and (a,(b,c)) have
different types
ii) How much difference to the logic would it make if tuples were allowed as
bound "variables" to lambda terms? I.e. so that you could genuinely
write

\ (a,b). a+b

rather than

UNCURRY \a. \b. a+b

This may require bringing tuples in as a primitive construct, though
I think that could be fairly justifiable.

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

(As a potentially off the wall comment,) perhaps now that witn hol90 we
have a much cleaner base than we had with the aglomeration of hol88 we
can consider various extensions to the logic as a future  version (HOL
1999? :-) - TFM has already suggested that he may experiment with
adding type quantification to hol90, perhaps bringing in tuples as
primitives?

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		Life doesn't imitate art, it imitates bad television