[TYPES] rewriting of typed combinator expressions

[Jonathan P. Seldin]

On Aug 3, 2004, at 3:31 AM, Jeremy Dawson wrote:

> [The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
>
> 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
>
>


Curry and Feys, _Combinatory Logic_, vol. I, (North-Holland, 1958) 
Chapter 9, contains a proof of normalization for combinatory terms 
typed by basic type assignment.  The proof uses an L-formulation 
(sequent calculus) for the rules of type assignment, provided that the 
basis (typing assumptions) satisfy certain conditions.  The 
L-formulation uses a rule for introducing the arrow type on the right 
that is like the corresponding rule for lambda-calculus, but uses the 
defined abstraction operator on combinatory terms.  Thus, while it does 
not technically detour via lambda-calculus and beta-reduction, it may, 
in some ways, seem to do so.  (By the way, Curry writes the type A -> B 
as FAB.)

Since the book was first published in 1958, I think this is the first 
published proof that the reductions of typed terms terminate.  (Turing 
had a proof of this for lambda-terms in 1942, but it was not published 
until 1980 when Roger Hindley and I convinced Robin Gandy to publish 
that proof in the book we edited _To H. B. Curry:  Essays on 
Combinatory Logic, Lambda Calculus, and Formalism_ (Academic Press, 
1980).  Turing's proof was almost certainly the first, but it was not 
published first.)

Jonathan P. Seldin                                     tel: 403-329-2364
Department of Mathematics and Computer Science  jonathan.seldin at uleth.ca
University of Lethbridge                              seldin at cs.uleth.ca
4401 University Drive                    http://www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4