Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: Phil Windley <windley@edu.uidaho.cs.panther>
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: mutual recursion
In-Reply-To: Your message of Wed, 22 Apr 92 09:42:49 -0700. <199204221642.AA13082@panther.cs.uidaho.edu>
Date: Thu, 23 Apr 92 10:04:14 +0100
From: Brian Graham <btg@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.513:23.03.92.09.04.22"@cl.cam.ac.uk>

Hi Phil,

  In fact I did hack this just enough so it runs under
HOL 2.0, and can happily send the modified files.  However
there are problems which I have not sorted through:

1. It lacks the generality of Tom's recursive types package.
   Given a typical grammar for mutually recursive types:

   B    ::=  B1  |  B2 ty1  |  B3 B ty2  |  B4 C ty3
   C    ::=  C1  |  C2 ty4  |  C3 B C ty5

   it will not permit the types ty_i above to be any but 
   simple types (ie. not previously defined type constructors
   such as list, etc.).  By extension it shares the restriction 
   of Tom's package that the types being defined cannot appear
   as arguments to type constructors other than those being
   defined in the grammar.

   I did alter it just enough to accept the target grammar I
   had in mind.  A more general revision should not be too difficult,
   and is really mainly a parsing adjustment.

2. The form of theorem returned by the above grammar will look like:

|- !f1 f2 f3 f4 f5 f6 f7.
    ?! x1 x2.
     (           x1 B1           = f1) /\
     (!z1.       x1(B2 z1)       = f2 z1) /\
     (!z1 z2.    x1(B3 z1 z2)    = f3(x1 z1)z1 z2) /\
     (!z1 z2.    x1(B4 z1 z2)    = f4(x2 z1)z1 z2) /\

     (           x2 C1           = f5) /\
     (!z1.       x2(C2 z1 z2)    = f6 z1) /\
     (!z1 z2 z3. x2(C3 z1 z2 z3) = f7(x1 z1)(x2 z2)z1 z2 z3)

   Defining an induction theorem from this would be a desirable 
   next step.  The paper from the HUG meeting at Aarhus gives 
   their suggested form of induction theorem as (for this example):

|- !PB PC.
   (                                  PB B1) /\
   (!z1.                              PB(B2 z1)) /\
   (!z1 z2.    (PB z1) ==>            PB(B3 z1 z2)) /\
   (!z1 z2.    (PC z1) ==>            PB(B4 z1 z2)) /\
   (                                  PC C1) /\
   (!z1.                              PC(C2 z1)) /\
   (!z1 z2 z3. (PB z1) /\ (PC z2) ==> PC(C3 z1 z2 z3))

   I believe that this result is NOT obtainable however.  The nested
   unique existence quantifiers in the theorem characterizing the 
   datatypes suggest that we want to derive a uniqueness property 
   somwhat like the following example:

   (?! x y. P(x,y)) ==>
   !x x' y y'. (P (x,y) /\ P(x',y')) ==> (x = x') /\ (y = y')

   For a contradictory example showing why the above does not work
   consider P = \x,y. y < (SUC x).  Certainly, 
		|- ?! x y . y < (SUC x).
   ie. (x = 0) and (y = 0).

   However, MANY other pairs satisfy P, such as (4,4), (4,5), (0,1), ....
   The meaning of nested unique existence quantifiers is clearly not what
   is desired.  Rather, the theorem may need to state the unique existence
   of a tuple of functions.

This is as far as I got when I turned to some other work.  I would 
certainly like to hear if anyone else has worked with this package,
and if indeed my suspicions about defining an induction theorem are
well founded.  

Brian Graham