[ 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 [[email protected]] Sent: Sunday, January 06, 2019 11:22 PM To: Ahmed Bhayat Cc: [email protected] 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 <[email protected]<mailto:[email protected]>> 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 [email protected]<mailto:[email protected]> PhD candidate at the University of Manchester -- James Koppel twitter.com/jimmykoppel<http://twitter.com/jimmykoppel> www.jameskoppelcoaching.com<http://www.jameskoppelcoaching.com>
