[TYPES] rewriting of typed combinator expressions

[Jeremy Dawson]

HI,

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.

This could be proved by expressing I, W, S, etc as lambda-terms
and using the termination of beta-reduction (for well-typed terms).

But proofs to do with beta-reduction have complications to do with 
substitution.  Can anyone give me pointers to published proofs
of the termination of rewriting well-typed combinator expressions,
without going via lambda-calculus and beta-reduction?

Thanks for any help

Jeremy Dawson