A note on preservation of strong normalisation in the lambda-calculus

作者：Santo Jose Espirito^*

来源：Theoretical Computer Science, 2011, 412(11): 1027-1032.

DOI：10.1016/j.tcs.2010.10.049

An auxiliary notion of reduction rho on the lambda-terms preserves strong normalisation if all strongly normalising terms for beta are also strongly normalising for beta boolean OR rho. We give a sufficient condition for rho to preserve strong normalisation. As an example of application, we check easily the sufficient condition for Regnier's sigma-reduction rules and the "assoc"-reduction rule inspired by calculi with let-expressions. This gives the simplest proof so far that the union of all these rules preserves strong normalisation.

• 出版日期2011-3-11