[Prev][Next][Index][Thread]
Church-Rosser for typed systems
Subsorting has been of some concern to people in the area of data
type specification. Without going into the subtleties of what "order-
sorting" might be, I think most people would agree that subsorting
is a way to avoid explicit injections but that one should be able
for any formalization of subsorting to show "equivalence" to a formali-
zation explicitly using injections.
If we use injections the problem of \x:A.(\y:B.y)x reduces to
\x:A.(\y:B.y)(mx)
where m : A -> B is an injection (This is the only way to make sense
of the term \x:A.(\y:B.y)x in the presence of subsorting).
Clearly eta-reduction cannot be applied.
As the system is strongly typed there are no problems with CR except
that we have to add all the necessary injections m : A -> B as
constants plus conditional equations m(x) = m(y) => x = y.
Question is if replacing equality by reduction
m(x) -> m(y) => x -> y
guarantees CR?
I guess the question has a positive answer; on the spot every
reduction m(x) -> m(y) seems to stem from a reduction x -> y
(at least as long as no other constants and equalities are
involved), thus the system should behave as the system where
just the injections are added as constants.
In a sense John Mitchell suggests the same mechanism talking
about retracts.
A second more difficult question is how to avoid the explicit
use of injections but to have some notion of eta-reduction?
The only answer I can offer is to guard eta-reduction by a
typing condition
\x:A.(Mx) -> M if M : A->B
This is not quite satisfactory as one might like a "eta-
reduction" \x:A(\y:B.y)x -> \y.A.y (though this is clearly
achieved by beta-reduction).
One should observe, however, that if we have overloading of
operators, e.g. f : B->C, f : A->C, this eta-reduction is
not the standard eta-reduction of the typed calculus:
Let us consider one of the standard examples in specification
theory talking about stacks. There are two types "stack" and
"nestack" (non empty) with the standard push and pop operations
as constants and the equality pop(push(x,d)) = x where x :"stack".
Let f be an overloaded (polymorphic?) operation which is defined
non "stack" and "nestack". Then
\x:"nestack".f(pop(push(x,d))
is well formed if we choose f :"stack" -> C. Application of the
equality yields
\x:"nestack".fx -> f
where f : "nestack" -> C.
The example may look weird to people working on \-calculus. However
we may develop a different interpretation of typing in that we
consider types as unary predicates by which we state "definedness"
(making explicit that that is used to express a certain degree
of partiality of operations). E.g. the untyped \x.x satisfies
the "predicates" A->A. The notation \x:A.x then states that we
"know" that the term \x.x "satisfies" the "predicate" A->A.
Assuming that A < B we can check that \x:A.(\y:B.y)x : A->B.
Then the eta-reduction above allows
\x:A.(\y:B.y)x -> \y:A.y
as we can prove \y.y : A->A.
I do not really know how reasonable the type-as-predicates idea
is in the framework of \-calculus but it works nicely for
algebra (as shown in a recent paper). Subsorting then is implication
of type predicates. The whole idea looks like an alternative
interpretation of polymorphism polluted by subsorting.