The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

Isaac Newton Institute for Mathematical Sciences

Semantics of Computation

1 July - 31 December 1995

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.

Copyright © Isaac Newton Institute