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

[Ahmed Bhayat]

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>