This blog post is a little different from the rest, as it considers two articles from the SIGACT Logic Column. The first, Logic Column 14, written by Cheney, begins with a critique of higher-order abstract syntax (HOAS), and ends by arguing in favour of nominal abstract syntax, and nominal logic. Crary and Harper respond in Logic Column 16, with a rebuttal of Cheney’s claims about HOAS, specifically the implementation of HOAS as seen in LF.

Higher-order abstract syntax uses an enriched meta-language, usually the simply typed lambda-calculus, in order to encode languages at the object level. Name binders at the object level are implemented by binders at the meta-level, using the meta-level lambda. For instance, a statement like forall x:Nat. p(x) could be encoded in HOAS by the term FORALL (lambda x. P x). Here FORALL has type (Nat -> Prop) -> Prop, and P has type Nat -> Prop, with lambda being the meta-level binder. This idea is very old, dating back to Church’s work on simple type theory and his encoding of the universal and existential quantifiers, but HOAS as we know it now was popularised by Pfenning and Elliott (see this prior blog post).

Higher-order abstract syntax has been highly successful: lambdaProlog, Twelf, Delphin, Beluga, LF etc. all use HOAS, and, in effect, at the time Cheney was writing, HOAS was still the “state-of-the-art”, and probably the most widely implemented solution to the “binding problem”. Nominal techniques, and nominal logic in particular, were still new on the scene.

Cheney identifies five areas where he believes HOAS is lacking. His first and fourth critiques can be lumped together, under the heading “simplicity”:

Higher-order abstract syntax is based on complex semantic and algorithmic foundations (higher-order logic [17], recursive domain equations [77], higher-order unification [46]) so requires a fair amount of ingenuity to learn, implement and analyze [27, 43, 74].

Higher-order language encodings are often so different from their informal “paper” presentations that proving “adequacy” (that is, equivalence of the encoding and the real language) is nontrivial, and elegant-looking encodings can be incorrect for subtle reasons. Hannan [39] developed and proved partial correctness of a closure conversion translation in LF, but did not prove adequacy of the encoding; careful inspection suggests that it is not adequate. Abel [2] investigated an elegant and natural-seeming but inadequate third-order and less elegant but adequate second-order HOAS encoding of the λμ-calculus.

Both of these criticisms are interesting, as they feed directly into what many view as nominal techniques’ greatest advantages: a simple, set-based semantics, where names exist in the denotation independently, with tractable algorithmic content, and straightforward, intuitive encodings, with reasoning close to informal practice.

However, Crary and Harper disagree with the first claim:

All the metatheory of LF can be (and typically is) carried out in first-order logic; higher- order logic is not necessary.

The metatheory of LF is carried out using entirely syntactic means. There is no need to resort to any denotational semantics, including recursive domain equations.

While higher-order unification is used in the Twelf implementation [3] of LF to support type inference and proof search, it is not at all relevant to the methodology of encoding abstract syntax in LF. Moreover, even in regards to the Twelf implementation, experience suggests that understanding the higher-order unification algorithm is not essential; students who do are not familiar with it nevertheless have little difficulty in using Twelf.

And also with the fourth:

A fundamental part of the LF methodology is the notion of an adequate encoding. Syntactic terms and derivations of judgements are represented in LF as certain canonical forms, and the encoding is said to be adequate if there exists an isomorphism (in a sense that can be made precise) between the terms/derivations on the object language and the canonical forms that represent them. This provides a clear criterion for whether an encoding is correct or not.

The column notes that inadequate encodings have appeared in papers, and takes that fact as evidence that it is too hard to develop adequate encodings. To the contrary, we see the existence of incorrect encodings as merely the inevitable consequence of the existence of a correctness criterion.

To the best of our knowledge, nominal logic does not currently enjoy a precise criterion for correctness. Consequently, it is hard formally to justify the statement that anything at all has been encoded in nominal logic. When nominal logic is better understood, we expect that a correctness criterion will be developed for it as well. Once that happens, we expect that that criterion too will be used to identify incorrect encodings.

Cheney’s third and fifth critiques can also be lumped together, under the heading “expressivity”:

Variable names are “second class citizens”; they only represent other object-language expressions and have no existence or meaning outside of their scope. This complicates formalizing languages with generativity (for example, datatype names in ML), program logics with mutable variables such as Hoare logic [51] or dynamic logic [44] and translations such as closure conversion that rely on the ability to test for name-equality.

Higher-order abstract syntax is less expressive than first-order abstract syntax: it apparently cannot deal with situations involving “open terms” mentioning an indefinite number of free variables. For example, HOAS apparently cannot model the behavior of ML-style let-bound polymorphism as usually implemented [41], though a simulation is possible [40].

Again, the standard claim is that nominal techniques handle these features well. Bound names in nominal encodings can be easily tested for (in)equality. Indeed, a “standard example” (and by this, I mean an example used more than once!) in the nominal literature is an encoding of alpha-inequivalence, where bound names must be tested by inequality, precisely because it is thought hard to do with HOAS.

However, Crary and Harper disagree:

…

Moreover, taking alpha-equivalence as built-in does not preclude the isolation of variables in LF (which can be done easily using a hypothetical judgement). Consequently, it is not difficult to encode logics that deal with variables specially or that compare free variables for equality.

…

The column claims that HOAS cannot address ML-style let-polymorphism due to difficulties with open terms. This is not so. There are at least two perfectly satisfactory formulations of let-polymorphism in LF.

…

Finally, Cheney argues that using HOAS encodings pollutes the encoded object language with features inherited from the meta-language, whether desirable or not. For instance, if the meta-language has a weakening property, then this is inherited in the object-language, and thus makes encoding substructural logics, like linear logic, inconvenient:

Properties of the metalanguage (such as weakening and substitution lemmas) are inherited by object languages, whether or not this is desirable; this necessitates modifications to handle logics and languages with unusual behavior. Examples include linear logic [10] and concurrency [86].

Yet, again, however, Crary and Harper disagree:

The column claims that structural properties of the meta-language must be inherited by the object language. This is simply untrue. For example, linear logic can be adequately represented in ordinary LF using a linearity judgement; one need not resort to a linear variant of LF.

A counter rebuttal to Crary and Harper wasn’t provided. However, both techniques now quite happily live side-by-side. Nominal implementations, such as Nominal Isabelle, are now extremely popular, and connections between the two approaches are being realised (see the work on higher-order patterns and nominal unification, as well as Gabbay and Hofmann’s nominal renaming sets).