[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Chris,
In some (or many) cases, already known proofs can work for predicative
versions
of System F as well. You can find one example from the paper with
Aleksy, as
informed by Frank Pfenning:
http://www.sciencedirect.com/science/article/pii/S0890540112001150
Fujita, Schubert: The undecidability of type related problems in the
type-free
style System F with finitely stratified polymorphic types,
Information and Computation Vol. 218, pp. 69--87, 2012.
With best regards,
Ken
---
Ken-etsu Fujita
Gunma University
(2013/01/29 9:23), Frank Pfenning wrote:
[ The Types Forum,http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Chris,
It depends on exactly how you defined type reconstruction.
For one definition, I proved undecidability for the predicative
case in the paper below, based on a suggestion by Bob Harper.
Frank Pfenning. On the undecidability of partial polymorphic type
reconstruction. Fundamenta Informaticae, 19(1,2):185-199, 1993.
Preliminary version available as Technical Report CMU-CS-92-105, School of
Computer Science, Carnegie Mellon University, January 1992.
http://www.cs.cmu.edu/~fp/papers/CMU-CS-92-105.pdf
Fujita and Schubert have results for other definitions, while
remaining predicative (RTA 2010, with a longer version in I&C 2012).
Best,
- Frank
On Mon, Jan 28, 2013 at 5:38 PM, Christian Skalka<[email protected]>wrote:
[ The Types Forum,http://lists.seas.upenn.edu/mailman/listinfo/types-list]
I am wondering if there are formal results related to the (un?)decidability
of type reconstruction in predicative System-F. As I understand it, Joe
Wells' well-known undecidability result only applies to impredicative
System-F.
Pointers/citations appreciated.
Thanks,
-chris
--
Christian Skalka
Associate Professor
Department of Computer Science
University of Vermont
http://www.cs.uvm.edu/~skalka
