[Prev][Next][Index][Thread]

Church-Rosser for typed systems


> In what you call the alternate (actually, historically first)
> presentation of the simply typed lambda calculus (Barendregt, Appendix
> A), you have a different way of defining terms, and
>         A     B
>       \x . (\y . y) x 
> is not a term at all. 

In the simply typed lambda calculus, Val is of course right.

How about in a lambda calculus with subtyping, in which a term of type A can
be interpreted as one of type B?  Yes, it's not the classical simply typed
case, but it's reasonably common in real life.  Say, nat is the type of
naturals (0,1,2,3..) and int is integers (...-2,-1,0,1,2...).  Every nat can
be understood as an int (nat is a subtype of int); consider:
     \x:nat. (\y:int . y) x
It beta-reduces to \x:nat.x, and eta-reduces to \y:int.y.

This one is somewhat persuasive.  There's an implicit coercion going on, but
in a simply typed calculus with subtypes it is hard to say formally just what
the coercion is.  When I try to say, "(\y:int.y) coerced to be nat->nat", I
find myself saying "\x:nat. (\y:int.y) x".    

In any event, this term is certainly well-typed, and does not conflue (*)
under beta+eta.  I'll say "M conflues" for "the reduction relation restricted
to descendents of M is confluent", mostly because it sounds funny.

It might conflue if we throw in a suitable subtyping rule: 
   If s is a subtype of t, then \x:t.M --> \x:s.M.
This rule seems plausible in the sense that subtyping is plausible, and
dangerous because it doesn't preserve meaning or typing.  Since eta already
doesn't,  it's not clear how bad that is.

Also, in a calculus that allows both typed and untyped terms
     \x:int. (\y:any.y) x 
beta-reduces to \x:int.x, and eta-reduces to \y:any.y. (It vaguely reminds me
of some complied Lisps which allow optional typechecking.  I don't think I've
ever seen it formally defined.)

This trick is less persuasive, since the obvious way of really typing in a
calculus with explicit polymorphism would make it work right.  (If you had to
write \x:int (\t\y:t.y) int x, then it would eta-reduce to (\t\y:t.y)int, and
this one at least is confluent.

I hope this helps confuse the issue.

-- Bard