[POPLmark] Experience report with Twelf
Randy Pollack
rap at inf.ed.ac.uk
Wed Aug 31 12:29:14 EDT 2005
Jevgenijs Sallinens writes:
> 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).
One can write a wrapper function that takes a natural number, n, and
executes evaluation n steps. In practice this is no different from
being able to execute non-total functions. And this point has nothing
to do with constructivity: classical HOL also has only total
functions. In Isabelle/HOL one could use the simplifier to
iteratively apply an evaluation relation.
Randy
More information about the Poplmark
mailing list