```

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