Logic in Computer Science (LICS 1991)

Paper: An inverse of the evaluation functional for typed λ-calculus (at LICS 1991)

Authors: U. Berger H. Schwichtenberg

Abstract

A functional p→e (procedure→expression) that inverts the evaluation functional for typed λ-terms in any model of typed λ-calculus containing some basic arithmetic is defined. Combined with the evaluation functional, p→e yields an efficient normalization algorithm. The method is extended to λ-calculi with constants and is used to normalize (the λ-representations of) natural deduction proofs of (higher order) arithmetic. A consequence of theoretical interest is a strong completeness theorem for βη-reduction. If two λ-terms have the same value in some model containing representations of the primitive recursive functions (of level 1) then they are probably equal in the βη-calculus

BibTeX

  @InProceedings{BergerSchwichtenber-Aninverseoftheevalu,
    author = 	 {U. Berger and H. Schwichtenberg},
    title = 	 {An inverse of the evaluation functional for typed λ-calculus },
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {203--211},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }