[FOM] Simply Typed Lambda Calculus
obua at in.tum.de
Mon Jan 14 20:15:01 EST 2008
immanuel litzroth wrote:
>Hindley "Basic Simple Type Theory"
>2C1: Subject Reduction Theorem:
>if Context |- term1:type and term1 |> term2 where |> stands for beta
>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?
More information about the FOM