[TYPES] HOAS versus meta reasoning

[Andrew Pitts]

Dear Alexander,

2008/11/14 Alexander Kurz <kurz at mcs.le.ac.uk>:

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

That's not quite accurate. We were looking at

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

(i.e. semi-HOAS) where

either [Fiore/Plotkin/Turi, and M.Hofmann] the equation is interpreted
in a category of presheaves and "Var=>(-)" is the ordinary function
space, right adjoint to Var x (-)) [good]; but the category does not
suppurt the law of excluded middle [not so good];

or [Gabbay/Pitts] the equation is interpreted in the category of
nominal sets and Var=>(-) is not the ordinary function space but
rather is right adjoint to the separated product Var \otimes (-)
[maybe not so good, but cf separation logic and the fact that Var=>(-)
has a very concrete description related to alpha-equivalence]; and in
this case the category does support the law of excluded middle [good].

>There has been a lot of work on this since then, in
> particular by Pitts and collaborators.

Quick tutorial on nominal sets in

A. M. Pitts, Alpha-Structural Recursion and Induction, Journal of the
ACM 53(2006)459-506.

The catgory of nominal sets is probably a good place to look for
denotational models of the Harper/Licata/Zeilberger "representational
arrow" that Karl Crary mentioned in a previous message in this thread.

Andy