[TYPES] rewriting of typed combinator expressions
Jeremy.Dawson at nicta.com.au
Tue Aug 3 18:31:05 EDT 2004
Rewriting of combinator expressions according to the rules
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
More information about the Types-list