[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |

*Originator: Jean-Jacques Lévy *

*Date: April 1991*

Summary: Can strong normalization of the typed lambda calculus be proved by a reasonably straightforward mapping from typed terms to a well-founded ordering?

Can strong normalization (termination) of the typed lambda calculus be proved by a reasonably straightforward mapping from typed terms to a well-founded ordering? Note that the type structure can remain unchanged by β-reduction. The same question arises with polymorphic (second-order) lambda calculus.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |