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

[James Koppel]

Thanks for the explanation, Ahmed. I confess to not having studied
reduction orderings in higher-order term rewriting, only in first-order
term-rewriting. Problem 2 still seems easy to circumvent, however.

On Mon, Jan 7, 2019 at 7:38 AM Ahmed Bhayat <ahmed.bhayat at manchester.ac.uk>
wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Thank you James,
>
> It does not appear to meet the requirements. As a reduction ordering is
> being sought, compatibility with contexts is required. Consider the
> following terms:
>
> 1) t1 = ^x. (f x x) and  t2 = (f a). As we do not have that t1 -->beta t2
> or t2 -->beta t1, an arbitrary decision must be made as to the ordering.
> Choose t2 > t1. But, then in the context []a, [^x. (f x x)]a -->beta [fa]a
> and thus by compatibility with beta-reduction [t1]a > [t2]a contradicting
> compatibility with contexts.
>
> Further, as a reduction ordering is sought, the ordering must be
> well-founded. Making an arbitrary decision does not ensure this. Consider
> terms:
> 2) t1 = (^x. f x x x x)t and some arbitrary term t2. By compatibility with
> beta-reduction we must have t1 > f t t t t. We then make an arbitrary
> choice and have  f t t t t > t2. If by another arbitrary choice t2 > t1,
> well-founded has clearly been lost.
>
> Regards,
>
> Ahmed
> ________________________________
> From: James Koppel [jkoppel at mit.edu]
> Sent: Sunday, January 06, 2019 11:22 PM
> To: Ahmed Bhayat
> Cc: types-list at lists.seas.upenn.edu
> Subject: Re: [TYPES] Reduction ordering on terms of simply-typed
> lambda-calculus compatible with beta-reduction
>
> 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
> <mailto: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<mailto:ahmed.bhayat at manchester.ac.uk>
> PhD candidate at the University of Manchester
>
>
> --
> James Koppel
> twitter.com/jimmykoppel<http://twitter.com/jimmykoppel>
> www.jameskoppelcoaching.com<http://www.jameskoppelcoaching.com>
>