Re: [TYPES] Reduction ordering on terms of simply-typed lambda-calculus compatible with beta-reduction
Frédéric Blanqui <[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hello. I am not aware of such results. Concerning reduction orders on simply-typed lambda-terms, you can have a look at the works of Jouannaud and Rubio: http://doi.org/10.1145/1206035.1206037 and http://doi.org/10.1145/2699913. Best regards, Frédéric. Le 06/01/2019 à 12:54, Ahmed Bhayat a écrit : > [ 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