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

Re: confluence, subject reduction for F^{omega} with products, eta

[Duggan asked about confluence and subject reduction for System F omega
extended with products and eta conversion.  Here is a reply from Ghelli,
with Duggan's comments interleaved.  -- Phil Wadler, moderator]

[Note to contributors: When you supply an answer to a previous
question, please write a short introduction, so that I don't need to
write one for you!  Cheers,  -- P]


> System F with subtyping is not confluent w.r.t. beta-eta, hence the answer
> to this sub-question is NO. 

Thanks, I already knew this.  

> By the way F-sub admits an interesting
> confluent system which is beta-eta-top (top identifies terms of type Top)
> [Curien Ghelli]; extensions of beta-eta-top to products, for system F without
> subtyping, have been studied in [Curien Di Cosmo] and [Di Cosmo Kesner]
> 
> Best Regards,
> 
>    Giorgio Ghelli
> 
> [Curien Ghelli] P.-L. Curien and G. Ghelli, Confluence and decidability of
> beta-eta-top reduction in Fsub, Information & Computation, to appear.
> A preliminary version in Proc. Conf. on Theoretical Aspects of Computer 
> Software, Sendai, Japan, Springer-Verlag, Berlin, Lecture Notes in Comput. 
> Sci. 526 (1991).
> 
> [Curien Di Cosmo] P.-L. Curien,  R. Di Cosmo, Confluence in the Typed 
> lambda-calculus Extended with Surjective Pairing and a Terminal Type, Proc. 
> Int. Coll. on Automata, Languages and Programming 91, Lecture Notes in
> Comput. Sci. 510 (1991).
> 
> [Di Cosmo Kesner] R. Di Cosmo, D. Kesner, A confluent reduction for the 
> extensional typed lambda-calculus with pairs, sums, recursion and terminal 
> object, in Intern. Conf. on Automata, Languages and Programming (ICALP), LNCS,
> Springer-Verlag, (1993).

My (ill-worded) question was meant to be:  does any of the proof theory
for F-sub *which does show confluence* carry over (I was thinking of a
couple of papers presented at TACS 91).  Thanks for the references, I
will look into this.

--dd

Spoken: Dominic Duggan  Internet: dduggan@uwaterloo.ca
Canada: Dept of Computer Science, University of Waterloo,
        Waterloo, Ontario, Canada N2L 3G1