[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
________________________________________________________________