[FOM] Simply Typed Lambda Calculus

[Steven Obua]

immanuel litzroth wrote:

>
>Hindley "Basic Simple Type Theory"
>
>2C1: Subject Reduction Theorem:
>
>if Context |- term1:type and term1 |> term2 where |> stands for beta
>eta reduction
>then Context |- term2:type.
>The reverse is not true: if term2 is typed it could have com from a
>nontyped term (which is
>why no attempt is made at defining a typed convertability relation as
>he explains in chapter
>5 of the same work).
>  
>
Yes, I was thinking about looking into this book, too. But I fear my 
question might not be answered there.
Because in my setting I am not interested in the question if term1 or 
term2 are typeable.
But GIVEN term1 and also term2 are typeable, and there is a sequence S 
of steps involving eta/beta  reduction/abstraction which convert
term1 into term2, is there then also a sequence S' which does the same 
but such that each step of S' is contained in this
"typed convertability relation".

So S might lead to intermediate terms which are not typeable, but my 
question is, as I am going from a typed to another typed term, are these
intermediate untypeable terms somehow superfluous?

Best,

Steven Obua