Simple example for Higher Order Abstract Syntax (λ-tree syntax)

Question

I am reading https://www.cs.cmu.edu/~fp/papers/pldi88.pdf and https://en.wikipedia.org/wiki/Higher-order_abstract_syntax for trying to understand encoding of linear logic using HOAS into Coq. But I still cannot grasp whats going on? Is there simple concrete example available for using HOAS? E.g. exmaple in concrete syntax, example of abstract syntax and example of encoding in HOAS? Or maybe there is available good in-depth explanation of HOAS with multiple examples?

Answer 1

Well, this is a bit broad but the basic idea is the following. In First-order abstract syntax (FOAS) we model lambda terms following their syntax tree. E.g., in Coq we would write

(* FOAS *)
Definition variable := string .
Inductive term: Set :=
  | var: variable -> term
  | app: term -> term -> term
  | lam: variable -> term -> term
.

Definition example: term := lam "x" (app (var "x") (var "x")) .

Note how we model $\lambda x. xx$ by storing the name "x" explicitly. In a sense, a lambda is represented as a pair (variable name, body).

In FOAS we need to carefully handle alpha-conversion and capture-avoiding substitutions.

In HOAS, we model lambdas as functions, not pairs, exploiting the functions in the host language.

(* HOAS *)
Inductive term: Set :=
  | var: variable -> term    (* vars are usually removed in HOAS *)
  | app: term -> term -> term
  | lam: (term -> term) -> term

Definition example: term = lam (fun x: term => app x x) .

(Note that this won't type check in Coq since it does not use positive recursion, as Mario Carneiro points out below. Still, you get the idea.)

No need to handle alpha-conversion (or substitutions) here since the name "x" is no longer stored in the term.

What we lose in HOAS is the ability to dissect the term representation (e.g. structural induction on the syntax tree) as easily as we could in FOAS.