Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
have cross-linked with abstract syntax tree.
have to admit that I find the current Idea section (here) hard to follow. Would it be right to say more directly:
Higher-order abstract syntax equips the data type of abstract syntax trees with quantifiers i.e. with higher-order logic, whence the name.
?
have added link to Hofmann’s article and added also pointer to
and to the Wikipedia entry.
Would it be right to say more directly:
I think the issue with this page at present is that it describes a specific logical framework called “higher-order abstract syntax” by Pfenning and Elliot. However, the concept of “higher-order abstract syntax” is more general, and in that context your description is more accurate. I think a page specifically for Pfenning–Elliot’s theory is unhelpful, and it would be better to use this page for the general concept (in keeping with the references I added on second-order abstract syntax, before I realised the original intent of the page).
In a little more detail: higher-order abstract syntax is a way to represent syntax in a form free from concrete syntactic details (e.g. alphabets of symbols, grammars, etc.). One way to do this is via a logical framework, representing higher-order operators via functions in some meta-theory. However, this is not the only way to represent higher-order abstract syntax (presheaf models being another example), and I think it is misleading to conflate “higher-order abstract syntax” with any one of these approaches.
Thanks. I have added links to the articles
Marcelo Fiore, Gordon Plotkin, Daniele Turi. Abstract syntax and variable binding, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158). IEEE (1999) [doi:10.1109/LICS.1999.782615, pdf, weboage]
Marcelo Fiore, Chung-Kil Hur. Second-order equational logic, International Workshop on Computer Science Logic. Springer, Lecture Notes in Computer Science 6247 (2010) [doi:10.1007/978-3-642-15205-4_26, pdf]
and am copying them to their author’s pages, too
No, I don’t think it’s accurate to say that HOAS refers to all treatments of syntax with variables that are sufficiently abstract. Fiore-Plotkin-Turi do not refer to their system as HOAS, and mention it in the introduction as related but not the same. HOAS specifically means using functions in the metalanguage to model binding structure. My plan for this page was to write some notes modernizing/condensing Hofmann’s paper that use presheaf models to justify this approach as “adequate” (his terminology). I put a bit about the 2nd order approach in https://ncatlab.org/nlab/show/second+order+algebraic+theory
Also I don’t think it’s accurate to say that it is about “quantifiers” unless you have a very general meaning of quantifier in mind (is a lambda term a quantifier?).
Fiore-Plotkin-Turi do not refer to their system as HOAS
No: they refer to their system as second-order abstract syntax, because they only have a single level of variable binding. The generalisation of their work to arbitrary levels of binding is therefore higher-order abstract syntax in their terminology. They mention the HOAS of Pfenning–Elliot is related but not the same, but the evident generalisation of their terminology is technically in conflict with that of Pfenning–Elliot. The usage of Fiore–Plotkin–Turi seems much more reasonable that Pfenning–Elliot’s, who incorporate features that do not obviously deserve to be included in a notion of higher-order abstract syntax, like polymorphism.
HOAS specifically means using functions in the metalanguage to model binding structure.
I disagree. This is what a logical framework means. Pfenning–Elliot’s HOAS is a specific logical framework.
Also I don’t think it’s accurate to say that it is about “quantifiers” unless you have a very general meaning of quantifier in mind (is a lambda term a quantifier?).
I agree that not all variable-binding operators should be called quantifiers: I’ve edited the text to reflect this.
The Wikipedia article on higher-order abstract syntax reflects my understanding:
In computer science, higher-order abstract syntax (abbreviated HOAS) is a technique for the representation of abstract syntax trees for languages with variable binders.
With regards to logical frameworks, it states:
In the domain of logical frameworks, the term higher-order abstract syntax is usually used to refer to a specific representation that uses the binders of the meta-language to encode the binding structure of the object language.
In particular, logical frameworks make use of higher-order abstract syntax in the manner you describe, but the meaning of “higher-order abstract syntax” is more general than this.
Your opinion on the terminology of HOAS vs logical framework does not match the usage in my experience. For instance in Jon Sterling’s recent tutorial on logical relations he refers to this as HOAS (https://www.jonmsterling.com/papers/sterling-2022-naive.pdf) or Adam Chlipala’s book (http://adam.chlipala.net/cpdt/html/Hoas.html).
There is enough room in the entry to discuss all variants of usage.
Just the first line of an Idea-section on “higher-order abstract syntax” really ought to be a sentence that contains both the words “higher-order” and “abstract syntax”, with some logical connectives.
After that is out of the way, we can continue in any way, for instance with: “However, some authors use the term to mean…”
As I understand it, “higher-order abstract syntax” has been used to mean three distinct but related concepts.
The relationship is that (1) makes use of the technique (2), and (2) is a specific representation form of (3).
Ironically, even though Pfenning–Elliot use the term to mean a specific framework (1), later work tends to cite theirs as a reference for the usage for (2). This usage shift seems to have occurred early on: for instance, Hofmann uses the term to mean (2).
It is true that many authors follow convention (2), in particular for the term “higher-order abstract syntax”. However, the terms “first-order abstract syntax” and “second-order abstract syntax” tends to refer to usage (3).
At the very least, we should disambiguate the meanings, as Urs suggests. My personal opinion is that the term should be reserved for (3). Historically, the technique was a defining feature in (Edinburgh) LF, which is a precursor to Pfenning–Elliot’s paper, and does not use the term “higher-order abstract syntax”. It does not seem to make sense to distinguish “logical framework” from (2), and this term has also been used alternatively as far as I can tell. The term “higher-order abstract syntax” is generic enough that it ought to refer to the general concept, rather than specific representation techniques.
I agree we should disambiguate the terms and especially explain the more principled terminology that Fiore uses. Looks to me like you (varkor) are in the best position to write this.
I have made some small modifications to the page to clarify the ambiguity in the terminology. The page needs some cleaning up and expansion, but I don’t have time to do so right now. Hopefully this at least provides a starting point to expand upon the ideas behind each of the usages without contention about naming conventions. I wasn’t sure exactly how to disambiguate the usages, so I have used “higher-order abstract syntax in logical frameworks” for the usage suggested by Max’s references, and “higher-order abstract syntax in algebraic type theory” for the usage suggested by the Fiore references. Feel free to modify these if anyone has better ways to disambiguate (ideally more concise ones). Apologies for being contentious: I think it is important to get terminology right, particularly as the nLab is a standard reference for many people, and I find the logical framework usage of “higher-order abstract syntax” to be somewhat misleading in its specificity.
Thanks. But I vote for re-instantiating an explanation of the term “higher-order” right at the beginning. I find it’s bad style to have jargon in a title that is not explained.
Previously I thought that “higher-order abstract syntax” is to abstract syntax as “higher-order logic” is to logic.
That seemed to me to be the main and first thing anyone should be told about this subject. Above I had the impression you agreed with that, now the explanations seems to have been removed again. Maybe it was wrong after all; but some comment along these lines ought to be retained, right at the beginning of the Idea-section – if only to say that/why this is not the intended meaning!
Above I had the impression you agreed with that
I do agree, but as Max points out, there is a widespread convention in the logical framework literature that adopts a restricted perspective on the meaning of “higher-order abstract syntax”. I chose to rewrite the ideas section to be unbiased about to what the term ought to refer. If there is consensus that the most sensible usage of the term is the one that you mention, then having an introductory explanation would be ideal, I agree.
I see, thanks. But if its just about having a “restricted perspective”, then that’s already what we need:
After a lead-in sentence:
Higher-order abstract syntax equips the data type of abstract syntax trees with quantifiers i.e. with higher-order logic, whence the name.
we could continue with:
However, parts/much of the literature uses the term in a more specific/restrictive sense:
Or something like this.
Sorry for being a pain about this. But it would be great if we had Idea-section accessible to the non-specialists.
Or something like this.
I’d be happy with that phrasing, assuming everyone else is.
Re #13, I have only ever heard HOAS in sense (2), and I do think there is a point to distingishing this meaning from “logical framework”. The logical framework is the formal system in which the technique of HOAS(2) is applied (as are other techniques as well). Using the same name for both of them is a category error (in the philosophical sense).
1 to 21 of 21