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

A uniqueness question





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