[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