2
$\begingroup$

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?

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ I think it is worth mentioning that the Coq term for HOAS you gave does not typecheck, because of non-positivity. Indeed it's inconsistent in Coq - you can prove a contradiction using such an inductive by diagonalization. $\endgroup$ – Mario Carneiro Jun 29 '18 at 16:42
  • $\begingroup$ @MarioCarneiro Oh, right! Thanks for pointing that out. $\endgroup$ – chi Jun 29 '18 at 19:26
  • 2
    $\begingroup$ HOAS is not implementable in Coq (see Section 17.2, Certified Programming with Dependent Types, by Adam Chlipala). A variation called parametric HOAS is possible, though, and given by Adam in the same section. $\endgroup$ – xuq01 Jun 30 '18 at 6:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.