**Organisers**: S Abramsky (*Imperial College, London*), G Kahn (*INRIA, Sophia-Antipolis*), J C Mitchell (*Stanford*), A M Pitts (*Cambridge*)

### Semantics of Computation Seminar

Friday September 8, 2:15 pm

#### Lambda-terms cannot be ordered

Peter Selinger,

University of Pennsylvania

Abstract: Our known examples of combinatory algebras seem to fall into two classes: `mathematically natural' ones, which are usually constructed using Scott-like order-theoretic methods, and syntactic ones, i.e. term algebras. In the first part, I will provide evidence that these two classes are disjoint. In particular, I will show that the best-known term algebras of the untyped lambda calculus do not allow a non-trivial partial ordering that is compatible with their structure.

In the second part, I will introduce what appears to be a new tool for establishing inequalities of untyped lambda-beta-(eta) terms. This is done via a notion of `very' partial models, which give denotations only for those terms that are relevant for the inequality at hand. Thereby, the problem of models for the full untyped lambda calculus is avoided: The latter are never finite or even recursive, while `very' partial models can be very small. I`ll give an example of a 3-element model establishing a non-trivial inequality.