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

Authors: Ulrich Berger Helmut 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 = 	 {Ulrich Berger and Helmut Schwichtenberg},
    title = 	 {An inverse of the evaluation functional for typed λ-calculus },
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {203--211},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }