[POPLmark] [Provers] Re: Adequacy for LF

[Geoffrey A. Washburn]

On Mon, 9 May 2005, Karl Crary wrote:

> There's no problem at all computing the free variables of a term.
> Here's a particularly slick implementation, but there's many other ways
> to do it:
>
> appearsfree : (term -> term) -> type.
>
> appearsfree_var : appearsfree ([x] x).
> appearsfree_app : appearsfree ([x] app (E1 x) (E2 x))
>        <- appearsfree E1
>        <- appearsfree E2.
> appearsfree_lam : appearsfree ([x] lam ([y] E x y))
>        <- ({y:term} appearsfree ([x] E x y)).
>
> The judgement "appearsfree ([x] E x)" will be derivable iff x appears
> free in E.  (I typed this directly into this message, so it's possible
> I've made a typo.)

	I don't think it was ever claimed that one could not calculate the
  free variables of a term in Twelf.  If so, correct me.

> Closure conversion is a little more interesting.  I suspect it's
> possible, but a certain amount ingenuity would be required.  The problem
> is getting your hands on the context, which is not usually a
> manipulatible object in LF.  (That is, the LF context is never
> manipulatible and ordinarily one identifies the object language context
> with LF's.)  To resolve this, I suspect one would have to reify the
> context.
>
>  Let me make a more general comment.  Many of the criticisms levelled at
> LF here have been of the form "you can't do X in LF/HOAS," and so far,
> all of those have been wrong, or at least unsubstantiated.  So why don't
> we declare a moratorium on that sort of thing.  Instead we can say that
> some things require some ingenuity to represent in HOAS, a statement on
> which we should all be able to agree.

	I'm not sure I agree.  You've said closure conversion would
  require ingenuity, but you have not actually exhibited that it is
  possible.  Without a solution in hand it would be more acceptable to
  agree "that it is an open problem".

-- 
-- Geoff Washburn | geoffw at cis.upenn.edu | http://www.cis.upenn.edu/~geoffw/ --