[TYPES] theorems on termination of reduction

[Jeremy Dawson]

Dear all,

There are two related theorems:

(1) Rewriting of combinator expressions according to the rules
such as
I x -> x
W f x -> f x x
S x y z -> x z (y z)

terminates if the terms are well-typed, but not in general.

(2) the termination of beta-reduction in the simply-typed lambda calculus

It's easy to see that (1) is provable from (2), simply
 by expressing I, W, S, etc as lambda-terms

I would guess that to prove (2) from (1) is possible, and not very deep,
(since a lambda-term is expressible using S,K,I)
but it seems nonetheless tedious, since one has to show that *any*
beta-reduction step in lambda-terms corresponds to one or more
reduction steps in the combinator expressions

Can anyone give me a source for a proof of (2) from (1)?

Thanks

Jeremy Dawson

PS Thanks also to all those who repsonded to my query a few months ago 
about a direct proof of (1) (ie not from (2))

PPS - FYI I've now worked out how to do (1) as a corollary of some work 
I've done
(now being written up) on termination of rewriting in a more general context