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.