Maximal Monoids of Normal Form

Abstract

In this paper, a characterization of the sets of normal forms which are monoids with respect to the composition combinator is obtained as application of the type theory to λ-calculus developed in [5]. The main result is that there is a monoid of normal form which is maximal in the sense that all extensions lead to terms without normal forms.