[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