Logic in Computer Science (LICS 1991)

Paper: Some results on the interpretation of λ-calculus in operator algebras (at LICS 1991)

Authors: Pasquale Malacaria Laurent Regnier

Abstract

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

BibTeX

  @InProceedings{MalacariaRegnier-Someresultsontheint,
    author = 	 {Pasquale Malacaria and Laurent Regnier},
    title = 	 {Some results on the interpretation of λ-calculus in operator algebras },
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {63--72},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }