1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
Friday September 8, 2:15 pm
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.