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

[Damiano Mazza]

Dear Ahmed,

I'm not sure I fully understand what you are asking, if you're looking 
for a total order on the set of simply-typed lambda-terms such that t 
--> t' implies t < t', then you can do as follows.

In the simply-typed lambda-calculus, every term strongly normalizes, so 
you may define an integer #t which is equal to the length of the longest 
reduction of t to its normal form.  This induces a partition on the set 
of simply-typed lambda-terms in countably many sets, call them S_n, such 
that S_n contains all terms t s.t. #t = n.  Each S_n is of course 
countable, so you may pick an injection beta_n : S_n ---> N, which 
induces a total ordering within S_n.  Observe now that t --> t' implies 
#t' < #t, which means that no two terms in the same S_n beta-reduce to 
one another.  Therefore, the map

    t |---> (#t, beta_n(t)).

induces a total order on the simply-typed lambda-terms isomorphic to 
omega^2 with the desired property.

Best wishes,

Damiano


On 06/01/2019 12:54, Ahmed Bhayat 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
> PhD candidate at the University of Manchester
>