[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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]> 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] > PhD candidate at the University of Manchester >
