[POPLmark] [Provers] Re: Adequacy for LF

[Geoffrey A. Washburn]

On Mon, 9 May 2005, Geoffrey A. Washburn wrote:

> 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.

	Oops.  We in fact did.  But that was before we thought about the
  problem further.

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