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

摘要

J.-Y. Girard (Proc. ASL Meeting, 1988) proposed an interpretation of second order lambda -calculus in a C algebra and showed that the interpretation of a term is a nilpotent operator. By extending to untyped lambda -calculus the functional analysis interpretation for typed lambda -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 lambda -terms always makes sense, by showing that lambda -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 lambda -terms, which seems to be related to some basic property of environment machines.