[Prev][Next][Index][Thread]
types
Dear all,
could anyone tell me if the following simple result is already known?
(provided it is true, I mean)
Stefano Berardi
****************************************************
THERE IS NO MAXIMUM EQUATIONAL THEORY FOR LAMBDA->
(PURE SIMPLY TYPED LAMBDA CALCULUS WITH ONLY BETA-REDUCTIONS)
****************************************************
A FAMILY OF NON-EXTENSIONAL MODEL
Let I = {I(A) | A simple type} be any family of inhabited sets. By hypothesis
there is a choice function, we will denote by i(.) such that for any A,
i(A) is an element of I(A). We may now define for each I a model of
simply typed lambda calculus, as follows:
[atom] = I(atom)
[A->B] = {<f,i> | f : [A]->[B] and i in I(A->B)}
= [A]->[B] X I(A->B)
We define the application by <f,i>.a = f(a) for all i in I(A->B).
We extend the interpretation to the terms by:
[x]s = s(x)
[tu]s = [t]s.[u]s
[lambda x.u]s = <f,i(A->B)>,
where i(.) is our choice function,
A->B is the type of lambda x.u, and
f is defined by f(a) = [u]s,x:=a for all a in [A].
We may check that this is indeed a model of lambda->. Csi-rule holds
because [u]s,x:=a = [v]s,x:=a for all s, a implies that for all s,
for some f = g we have [lambda x.u]s = <f,i(A)> and [lambda x.v]s = <g,i(A)>.
We will write I |= t=u iff for all s we have [t]s = [u]s in the model
induced by I. We write I |= t=/=u iff not(I |= t=u).
We may check that, if f:A->B is a variable and I(A->B) contains at least
two elements, then I |= f=/=lambda x.f(x), beacause [lambda x.f(x)]s =
= <F,i(A->B)> for some F, while the second component of [f]s may be any
j in I(A->B). That is, in general eta may fail in I (I may not be an
extensional model).
*******************************************************
THERE IS NO MAXIMUM THEORY
Let now Ik be the family defined by:
Ik(A) = {0} if length(A) <= k
Ik(A) = {0,1} if length(A) > k.
In the model Ik, we have card[C] = 1 if length(C) <= k, while
card[C] > 1 if length(C) > k (Proof: by induction on the
length of the type). This means that Ik |= t=u
if the type of t, u has length <= k, while Ik |= x=/=y if x, y
are distinct variables having type with length > k.
In other words, Ik satisfies all equation whose type has at most
length k, but it is still consistent, because it does not satisfy all
equations. So there is no maximum consistent theory, because if it
would exist, it would include all theory induced by any Ik, hence would
include all equations, and it would be inconsistent.
*******************************************************
REMARK1. We indeed proved a more general result, namely that all
set of equation in lambda-> having a bound to the length of the type
(for instance, all finite set of equations) are consistent.
REMARK2. It is essential in the result above do not have eta reductions.
In fact, as Statman proved, there is a maximum consistent theory for
simply typed lambda calculus with eta. Such theory, however, is only
maximal among the beta-theories, because it is not comparable with the
theories induced by any Ik.