The ant-lion paradigm for strong normalization (Q1336047)

This paper proposes -- via examples -- a paradigmatic way to find strongly normalizable solutions to fixed-point equations: 1) \(FX= X\), where \(F\) is normal and \(F= \lambda x.xM_ 1\dots M_ n\). 2) The extension of the adequacy theorem for numeral systems to the \(\lambda\)- \({\mathbf I}\) calculus.