Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: shb@oracorp.com's message of Fri, 26 Mar 1993 16:49:55 +0100 <9303261549.AA02913@sparta.oracorp.com>
Subject: Curried/Un-Curried type constructors
Message-Id: <93Mar27.015506met.8067@sunbroy14.informatik.tu-muenchen.de>
Date: Sat, 27 Mar 1993 01:55:04 +0100


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

Ack! Not for *me* to get group opinions, but for you to get the benefit
of the experience of others wrt. constructors that take tuples,
especially in the case of new_recursive_definition.


> What I'd like, then, are:
> 
> 1. Type constructors that take un-Curried arguments.  (Available in
>    HOL88, but not yet in HOL90.)

Steve has in fact spotted an inconsistency between hol90 and hol88,
which I didn't pick up on when I wrote the parser for recursive type
specifications. (It's a bit of a howler on my part: the infix "#" in the
types should denote pairing, but instead the defined constructor always
gets a Curried, i.e., functional, type!)

Until this mistake is fixed, if one wants paired arguments to
constructors in "define_type", the best thing to do is to use "dtype"
directly ("define_type" basically just does some parsing before calling
"dtype"). In an example at the end of this post, I show how to use
"dtype".


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

No. The problem isn't with parsing the terms, but with proving the
theorem that allows one to make the definition, and there's no
fundamental problem with proving the theorem other than it takes a bit
of work to build such a package. As for matching, HOL matching and hence
rewriting handles paired terms already.

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

One solution is the "pair" library of Jim Grundy. Unfortunately, as far
as I can see, this does not supply a "new_recursive_definition" that
handles constructors with paired arguments.

Does anyone have such a "new_paired_recursive_definition"?

As a more theoretical question, what would it take to make the HOL logic
be based on a lambda calculus with pairs? Would the matching algorithm
for types have to support the equation

    A -> B -> ... -> N = A # B # ... # M -> N ?

As a final note, in comp.lang.functional a few days ago there was a nice
article by Sanjiva Prasad on products in the lambda calculus.

______________________________________________________________________
Dtype example.

 The first type is made with "define_type"; the second shows how to use
"dtype" to get uncurried constructors.

Note. The unmemorable ML type constructors "Hty" and "Rec_occ" stand for
"HOL type" and "Recursive occurrence" respectively. These are the
constructors for the type "arg_atom".


    % hol90.sparc
    
    
              HHH                 LL
              HHH                  LL
              HHH                   LL
              HHH                    LL
              HHH          OOOO       LL
              HHHHHHH     OO  OO       LL
              HHHHHHH     OO  OO       LLL
              HHH          OOOO        LLLL
              HHH                     LL  LL
              HHH                    LL    LL
              HHH                   LL      LL
              HHH                  LL        LL90.5
    
    Created on Tue Mar 23 17:33:36 MET 1993
    using: Standard ML of New Jersey, Version 0.93, February 15, 1993
    
    
    The library "HOL" is loaded.
    val it = () : unit
    - new_theory "blat";
    
    Declaring theory "blat".
    
    Theory "HOL" already consistent with disk, hence not exported.
    val it = () : unit
    
    - define_type{name = "foo", fixities = [Prefix,Prefix],
                 type_spec = `foo = A of num 
                                  | B of (foo # foo)`};
    = = 
    val it =
      |- !f0 f1.
           ?!fn.
             (!n. fn (A n) = f0 n) /\
             (!f1' f2. fn (B f1' f2) = f1 (fn f1') (fn f2) f1' f2) : thm
    - dtype
      {ty_name="baz", 
       save_name = "baz_Axiom",
       clauses = [{constructor="C", fixity = Prefix, arg=[Rec_occ]},
                  {constructor="D",fixity=Prefix, arg=[Hty(==`:num#num`==)]}]};
    
    = = = = =
    val it = |- !f0 f1. ?!fn. (!b. fn (C b) = f0 (fn b) b) /\ 
                              (!p. fn (D p) = f1 p)
      : thm
    - type_of (--`D`--);
    val it = (==`:num # num -> baz`==) : hol_type