Some results on the interpretation of λ-calculus in operator algebras

J.-Y. Girard (Proc. ASL Meeting, 1988) proposed an interpretation of second order λ-calculus in a C algebra and showed that the interpretation of a term is a nilpotent operator. By extending to untyped λ-calculus the functional analysis interpretation for typed λ-terms, V. Danos (Proc. 3rd Italian Conf. on Theor. Comput. Sci., 1989) showed that all and only strongly normalizable terms are interpreted by nilpotent operators; in particular all and only nonstrongly normalizable terms are interpreted by infinite sums of operators. It is shown that interpretation of λ-terms always makes sense, by showing that λ-terms are interpreted by weakly nilpotent operators in the sense of Girard. This result is obtained as a corollary of an aperiodicity property of execution of λ-terms, which seems to be related to some basic property of environment machines