[POPLmark] F-sub decidability

[Jevgenijs Sallinenes/non-MAXIMUS]

Looks my previous e-mail in html style isn't showing properlly in PoplMark
archive, so here is another copy, hope better. I also rechecked mentioned
Benjamin's paper and for me it looks exactly same case as described in
challenge documentation.

Regarding third challenge: is there available some paper proof of
decidability of mentioned relations?
It looks to be not trivial at all, especially taking into account negative
result on decidability of subtyping relation
for Fsub ( http://citeseer.ist.psu.edu/pierce93bounded.html , by Benjamin
Pierce,which is one of PoplMark challenge authors).
Does same result is valid also for the calculus described in the challenge
problems?
As for AlphaProlog solution suggested by Matthew Fairbairn, there is
related question: is there a proof that
used AlphaProlog algorithms always terminates?
Thanks in advance for any highlighting information.
 Regards,
Jevgenijs.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050519/ad82ca20/attachment.htm