[Prev][Next][Index][Thread]

Uniqueness problem answered



A solution has been given by Thierry Coquand to my question
as to whether the type-assignment deduction of a \I-term is
unique.

It is unique.

Details follow (with problem repeated after solution)

_______________________________________________________________

Received: from animal.cs.chalmers.se by chalmers.se (5.60+IDA/3.14+gl)
          id AA06208; Thu, 21 Jan 93 10:56:43 +0100
Date: Thu, 21 Jan 93 10:56:42 +0100
From: Thierry Coquand <coquand@se.chalmers.cs>
Message-Id: <9301210956.AA09457@animal.cs.chalmers.se>
Received: by animal.cs.chalmers.se (5.60+IDA/3.14+gl) id AA09457;
          Thu, 21 Jan 93 10:56:42 +0100
To: majrh@uk.ac.swan.pyr


 Is not the following reasoning a proof of the uniqueness
of type assignemnent for M?


 A non normal term is of the form

 (\x M) N N1 ... Np : T

by induction on the length of a head reduction to its normal form, we
show that that there exists exactly one type assignement to it.
Indeed, if (\x:A M') N' N1' ... Np' : T is such a type assignement
then

 M'[x/N'] N1' ... Np'

is a type assignement for M[x/N] N1 ... Np.
It is unique by induction
hypothesis (or because this redex is a normal term),
and determines the type assignment of N because x appears in M.

 A related reasoning is done in Thomas Streicher's thesis (email
streiche@unipas.fmi.uni-passau.de), where he proves that type
information is redondant for a type system with dependent types.
His argument uses normalisation.

 A natural question is if there exist direct combinatorial
arguments, both for this result about \I term and Streicher's
results, that are purely combinatorial and do not rely on
a normalisation theorem.

                        Best regards,

                                        Thierry
________________________________________________________________
________________________________________________________________

Here is a uniqueness question on type-assignment. Any info
especially literature references would be very gratefully
received.
-------------------------------------------------------
In type-assignment (only arrow-types, type-variables, &
pure lambda-terms but RESTRICTED TO \I-TERMS),
is the whole deduction of an assignment
              M:tau
determined completely by M?
-------------------------------------------------------

  (The rules are the usual arrow-intro and elim:
        
     (->E)  P:A->B  Q:A
            ___________
               PQ:B        (A,B are arbitrary types)

     (->I)   [x:A]
               :
              M:B
           __________
           (\x.M):(A->B)  (discharge x:A).)

 If the M in the question is not restricted to \I-terms
then the answer is "Certainly not". For example in the
following deduction where M is (\xy.y)(\z.z) the type B can
be arbitrary without affecting the conclusion.

      [y:A]
   ___________ (->I)
   \y.y:(A->A)                     [z:B]
   ___________________ (->I)     ___________ (->I)
   \xy.y:(B->B)->(A->A)          \z.z:(B->B)
   ________________________________________ (->E)
         (\xy.y)(\z.z):(A->A) .

 If the M in the question is restricted to being in beta-
normal form then the answer is "Yes" even when M is not a \I-term.
(Easy proof.)

 But, what happens when M is a \I-term not in nf?

This question looks the kind of thing that must have occurred to
someone already; if anyone knows of a published answer
(or an unpublished one) I would be very interested in the source.

     Roger Hindley, majrh@pyramid.swansea.ac.uk
________________________________________________________________