[TYPES] Reduction ordering on terms of simply-typed lambda-calculus compatible with beta-reduction

[James Koppel]

Hello Ahmed,

Because the STLC is strongly-normalizing, beta reduction is itself a
reduction order. Terms A and B which do not transitively reduce to each
other may then be ordered arbitrarily. I believe this satisfies everything
you're looking for.

Yours,
Jimmy Koppel
MIT

On Sun, Jan 6, 2019 at 5:57 PM Ahmed Bhayat <ahmed.bhayat at manchester.ac.uk>
wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Dear all,
>
> Would welcome information on the following:
>
> Does there exist a reduction ordering, total on ground terms of the
> simply-typed lambda calculus, that is compatible with beta-reduction?
>
> That is, does there exist a reduction order ‘>’, total on ground terms of
> STT, such that for all terms t1 and t2 such that t1 beta-reduces to t2, we
> have t1 > t2?
>
> Alternatively, is there a proof that no such ordering  can exist?
>
> Failing either of the above, I would be interested in any partial results
> or possibly relevant results.
>
> Thanks
>
> Ahmed Bhayat
>
> ahmed.bhayat at manchester.ac.uk
> PhD candidate at the University of Manchester
>