Notes on "Focusing and higher-order abstract syntax"
13 March, 2008
A terminological regret:
Although the technique for encoding syntax described in this paper
is abstract and higher-order, it was probably a mistake to call it
"higher-order abstract syntax", since HOAS already has a
well-established usage for something very different: the use of
meta-level *substitution functions* to encode object-level binding.
Substitution functions are a very particular -- and very weak --
form of function space. In contrast, in this paper the meta-level
function space used to encode object-level pattern-matching is
deliberately open-ended. It could be, say, the Coq function space
(as described in Section 3.3), and hence restricted to primitive
recursion, but it could also include arbitrary set-theoretic
functions, which are treated as oracles. Indeed, if we are
modelling external input or a foreign function interface, we don't
necessarily want to assume that pattern-matching definitions take a
particular form, or are even computable.
To make a long story short, I've started calling this technique
"abstract higher-order syntax" (AHOS), rather than HOAS.
A few typos/clarifications:
Section 3.1, Fig. 5:
The typing rule for F(g(V)) should have Gamma |- F : Q > R
as a premise, rather than Gamma |- F : Q ; R
Section 3.3, declarations of val_tp, ..., exp_tp:
Each of the type declarations is missing an argument. They
should read:
val_tp : intctx -> val -> tp -> Prop
fnc_tp : intctx -> fnc -> tp -> tp -> Prop
sub_tp : intctx -> sub -> linctx -> Prop
exp_tp : intctx -> exp -> tp -> Prop
Section 3.4, Footnote 6:
The footnote mentions the \omega-rule, and then cites Buchholz et
al. This is a bit confusing. Indeed, the derived typing rule for
functions taking a Nat argument has one premise for every natural
number, so it is essentially the \omega-rule (it would be exactly
if we had dependent types), due to Schutte and others. However,
Buchholz' work was on the more general \Omega-rule, with a capital
\Omega. In fact, Buchholz' \Omega-rule corresponds almost exactly
to the *general* function-typing rule, for which the derived rule
for Nat-functions is an instance.