[Prev][Next][Index][Thread]
consistency proof
A LITTLE VICTORY FOR MODEL THEORISTS !!
A year and half ago I suggested the following "competition" to my friends,
the topmost experts in the proof-theory of lambda calculus I know. Namely,
consider the extension lbp of type-free lambda calculus given by:
add to lambda beta (eta) a fresh constant p such that
pp = p
pxopx = px (o is composition)
MoM = M implies pM = M .
Is lbp consistent ? I suggested that we tried to see whether we
could get first an answer by model-theoretic arguments or by proof-theory.
The problem was inspired by the
retraction models of higher order calculi (see Amadio&Longo in the
IFIP 1986 volume, Wirsing ed., where the question is raised). Indeed,
if consistent, lbp above gives a very simple model of the Tp:Tp theory and
proves that (even though the "types-as-proposition" analogy in the model is
lost) the equational theory of typed lambda terms in the Tp:Tp theory is still
consistent. This is done, of course, by any retraction based model a' la
Scott-MacCracken, but (the term model of ) lbp is particularly simple. Or,
more precisely, any interpretation given by "factorizing via" lbp is so.
Thus the problem, besides being difficult, had some good motivations.
(Note that, for reduction from left to right, lbp is provably not
Church-Rosser).
Stefano Berardi, a student of mine also visiting CMU, has just found a model
for lbp. Indeed, by some non trivial work on Scott's domain (and its
subcategory of Girard's coherent spaces) he has shown:
THEOR (Berardi) Any coherent space which yields a
model of lambda beta yields also a model for lbp.
(... and there are plenty of "coherent" models ).
I understand that it is not the first time that an (interesting)
extension of lambda calculus is known to be consistent only by model
theoretic constructions....
Cheers Giuseppe Longo