HOAS

Stream: Type theory

[Horatiu Cheval]

I have a quick terminology question, not Lean-specific, but I imagine there are people here knowing much more about these things than I do.
I am implementing a first order logic, and I encoded the formulas as follows (I am only including the relevant case of the universal quantifier)

variable D : Type

inductive formula
| universal : (D → formula) → formula

D is some domain over which the quantification ranges, and when encoding ∀ x ∈ D, φ(x), φ is encoded as an actual Lean function of type D -> formula, and φ(x) is an actual function application. So the encoding of the syntax does not contain variables, substitutions are not dealt with explicitly, etc, and instead all of this is delegated to the existing implementation in the meta-language (e.g. Lean).
Can this be called a higher order abstract syntax? If not, is there a better name for such an encoding?

[Mario Carneiro]

Yes, this is HOAS. You should be aware that HOAS formulas are problematic in foundations as "full featured" as Coq or Lean, because they allow the creation of impossible terms that depend on choice or involve type equality or other things like that, which can make the set of formulas behave strangely. An obvious example is that the set of formulas in a language is generally countable by definition, while your HOAS formulas are provably uncountable if D is infinite

[Horatiu Cheval]

Thanks. Indeed, I did notice myself the problems you mention, but this worked mostly well so far. Do you know whether there are some conditions I could impose on the D -> formula argument that would prohibit the construction of such exotic terms?

[Mario Carneiro]

The obvious condition is that it is generated by a formula :P

[Mario Carneiro]

You can sometimes get away with some kind of parametricity or naturality condition

[Mario Carneiro]

but I think it depends on the details of the system

[Billy Price]

What's the difference between HOAS and lambda-tree syntax? I've seen the latter in https://abella-prover.org

[Horatiu Cheval]

I have never heard of this before (I am very much a beginner though). After your question I searched a little and only skimmed through this paper where they extend ML to lambda tree syntax. Honestly, I failed to understand the difference. It seems to me they introduce a new constructor => called binding abstraction, and instead of representing abstractions by plain functions in the language, they use this instead. I don't know though