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

[ 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