Logic in Computer Science (LICS 1996)

Paper: Order-Incompleteness and Finite Lambda Models, Extended Abstract (at LICS 1996)

Authors: Peter Selinger

Abstract

Many familiar models of the type-free lambda calculus are constructed by order theoretic methods. This paper provides some basic new facts about ordered models of the lambda calculus. We show that in any partially ordered model that is complete for the theory of $\beta$- or $\beta\eta$-conversion, the partial order is trivial on term denotations. Equivalently, the open and closed term algebras of the type-free lambda calculus cannot be non-trivially partially ordered. Our second result is a syntactical characterization, in terms of so-called generalized Mal'cev operators, of those lambda theories which cannot be induced by any non-trivially partially ordered model. We also consider a notion of finite models for the type-free lambda calculus. We introduce partial syntactical lambda models, which are derived from Plotkin's syntactical models of reduction, and we investigate how these models can be used as practical tools for giving finitary proofs of term inequalities. We give a 3-element model as an example.

BibTeX

  @InProceedings{Selinger-OrderIncompleteness,
    author = 	 {Peter Selinger},
    title = 	 {Order-Incompleteness and Finite Lambda Models, Extended Abstract},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {432-439},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }