[POPLmark] Experience report with Twelf

[Jevgenijs Sallinens]

Quoting Karl Crary <crary at cs.cmu.edu>:

> Sure, we could stipulate that a program runs on an oracle machine that 
> is capable of deciding undecidable problems.  We could work out the 
> metatheory for the oracle version and it's easy to see how classical 
> logic would arise in such an account.
> 
> However, I never thought the downcasting check in FJ was intended to 
> require an oracle machine.  Rather, I took it as a technical shorthand 
> for a dynamic check that really could be implemented.  (I am fairly 
> certain that Benjamin intended it that way as well.)  If so, then 
> proving that it actually can be is an essential part of the metatheory.  
> Whether you prefer to call it part of "safety," I don't really care.
> 
> The only other option is to lay out the operational semantics in such a 
> way that it shows how to do the downcasting check (presumably, using 
> some sort of tagging regime).  If you do that, you're off the hook for 
> the proof, but I don't see it as an option to do neither, unless you're 
> embracing the oracle-machine interpretation.


Being newcomer in the field (and knowing nothing about FJ and down-casting),
I will try just to formulate my understanding of decidability problems
in context of PoplMark challenge. 
Writing it more as a questions to be confirmed by experts, since understanding 
of these problems could be helpful also for others challenge contibutors/users. 
Sorry for trouble, if these things lloks to be so trivial for experts.
As I suspect (nobody answered my previous e-mail in that respect), F-sub 
described
in the challenge is exactly the same proven by Benjamin to be undesidable
(for subtyping (and therefore for typing) relation). 
This lloks basicly making impossible to present solution for problem 2 of 
challenge 3
(at least with Coq), since reflexive-transitive closure of evaluation relation
could not be given as always terminating total computable function
(to be presented in Coq with fixpoint definitions).
But all this doesn't prevent us from reasoning about subtyping/typing relations
or reflexive-transitive closure of evaluation relation and such reasoning could 
be
performed (for challanges in question) by intuitionistic resoning 
(without excluded middle assumptions).
Within logical enviroment, we can interpret results about undecidable relations
as something like: if we are able to prove relation valid for some specific 
objects, 
then we can use general results about this relation to derive some other results
about same objects.
Possible similar we can do for computation: 
if we are so lucky that computations terminates for some objects, then we can 
use general results to establish their properties. 
This was stated in Hongwei Xi's submission letter, but I am not sure if  
we have safe basis to reason about (possible) unterminating algorithms.
Looks, such algorithms and relations provided by Coq inductive definitions
are not the same thing and not clear what then means such 'algorithm' for Coq. 
I am not familiar with Twelf, but interested (hope also many others readers)
on information about how Twelf submission is related to undecidabilty
of F-sub. Are they somehow affecting assumption made to belief proofs 
(or typechecking of proof scripts)?.

Best regards,
Jevgenijs Sallinens.

PS: undecidable means no the same as not realizable with Turing machine,as
could be interpreted from one of previous e-mails.


-------------------------------------------------
This mail sent through IMP: http://webmail.dva.lv/