[TYPES] HOAS versus meta reasoning

[Alexander Kurz]

Karl Crary wrote:
> Their framework also shows that the concern that is sometimes raised 
> over negative instances arising in HOAS is really a red herring.  The 
> problem, as I understand it, is as follows:  Suppose I take the 
> higher-order representation of the lambda calculus:
> 
> lam : (exp -> exp) -> exp.
> app : exp -> exp -> exp.
> 
> and try to make it into a recursive definition.  Then I obtain something 
> like:
> 
> mu X . (X -> X) + (X * X)
> 
> and this doesn't work the way it is supposed to, because of the negative 
> occurrence of X.  Consequently, you cannot use HOAS in this manner.

Can you expand on this? I would like to understand better what the
problem is. In particular in the light of the work of Gabbay/Pitts,
Fiore/Plotkin/Turi, and M.Hofmann, all at Lics'99, who showed that

  mu X . (X -> X) + (X * X) + Var

is an initial algebra (lambda terms up to alpha equivalence) supporting
proofs by induction. There has been a lot of work on this since then, in
particular by Pitts and collaborators.

Thanks in advance,

Alexander