[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