For instance, in first-order abstract syntax (FOAS) trees, as commonly used in compilers, the tree structure implies the subexpression relation, meaning that no parentheses are required to disambiguate programs (as they are, in the concrete syntax).
Second, programs that are alpha-equivalent (differing only in the names of bound variables) have identical representations in HOAS, which can make equivalence checking more efficient.
One mathematical object that could be used to implement HOAS is a graph where variables are associated with their binding sites via edges.
The term λ-tree syntax has been introduced to refer specifically to the style of representation available in the logic programming setting.
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.
As a concrete example, we would construct the object level expression (assuming the natural constructors for numbers and addition) using the HOAS signature above as where [y] e is Twelf's syntax for the function
This specific representation has advantages beyond the ones above: for one, by reusing the meta-level notion of binding, the encoding enjoys properties such as type-preserving substitution without the need to define/prove them.