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