<p>Re: "why encodings for binding-introducing constructs are considered third-order", the conventions are a bit arbitrary, and I've usually heard these encodings described as "second-order". For example, although in <a href="http://who.rocq.inria.fr/Gilles.Dowek/Publi/unification.ps%E2%80%8E" rel="noreferrer">these notes by Gilles Dowek</a>, the order $o(T)$ of a simple type $T$ (Definition 2.3) is defined as</p>

<p>\begin{align}
o(p) &amp;= 1 \tag{$p$ atomic} \\
o(S \to T) &amp;= \max(1+o(S),o(T))
\end{align}</p>

<p>on the other hand in <a href="http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf" rel="noreferrer">these notes by Herman Geuvers</a>, the order $h(T)$ of a simple type $T$ (Definition 22/Exercise 7) is defined as</p>

<p>\begin{align}
h(p) &amp;= 0 \tag{$p$ atomic} \\
h(S \to T) &amp;= \max(1+h(S),h(T))
\end{align}</p>

<p>I'm not sure why Pfenning &amp; Elliott chose the 1-indexed numbering scheme, but I suppose it might be the influence of the literature on higher-order matching/unification.</p>

CC BY-SA 3.0
2013-12-04T13:04:57.907Z
2013-12-04T15:37:38.643Z
2013-12-04T15:37:38.643Z
Noam Zeilberger
<p>You can think of $\lambda$-abstraction as an operator $\Lambda$ which takes a <em>function</em> from terms to terms into a term:
$$\Lambda : (\mathsf{Term} \to \mathsf{Term}) \to \mathsf{Term}.$$
The type of $\Lambda$ is <em>higher-order</em> because it maps <em>functions</em> to <em>objects</em>, so it is a <em>functional</em> of rank 2. This is where the name comes from.</p>

<p>For example, if $\mathsf{id}$ is the identity map then $\Lambda(\mathsf{id})$ is the term $\lambda x . x$.</p>

<p>Constructors, for example $\mathsf{succ}$ as a constructor for the type of natural numbers, can naturally be viewed as <em>first-order</em> because they take terms to terms.</p>

<p>Of course, for the above to make sense, we need to be able to speak about functions between terms at the meta-level. And there are various subtleties: in principle one can have weird functions between terms that do not correspond to anything that can be written down in the syntax (consider a non-computable map). So if you're not careful, you're going to end up with "exotic terms" $\Lambda(f)$ that create a lot of trouble.</p>

<p>The usual solution is to somehow limit $\mathsf{Term} \to \mathsf{Term}$ to only "nice" functions. One possibility is <a href="http://adam.chlipala.net/papers/PhoasICFP08/">PHOAS</a>, another is to use a meta-theory such as Logical Frameworks in which only nice functions exist.</p>

CC BY-SA 3.0
2013-12-03T08:21:52.013Z
2013-12-03T08:21:52.013Z
Andrej Bauer
<p>I understand that using higher-order abstract syntax essentially means using host (meta) language abstraction facilities to represent binders in embedded (object) language. But, Why exactly is it higher-order? Why is traditional abstract syntax called first-order abstract syntax?</p>

<p>I read the paper (Frank Pfenning, and Conal Elliott, Higher-Order Abstract Syntax, PLDI'88) that introduced HOAS as we use today. I could not quite understand the following paragraph ($\S$ 3.2) that describes encoding in HOAS:</p>

<blockquote>
  <p>In this first generalization, simply typed lambda terms represent programs. .. . The lexical terminals and the operators that do not introduce variable bindings are, respectively, first-order and second-order constants of the $\lambda$-calculus. Another crucial change occurs for the variables. Operators in the object language that are binding constructs are now explicitly encoded as third-order constants. As the following examples will show, this requires that bound object language variables actually become variables in the typed lambda calculus.</p>
</blockquote>

<p>Particularly, I am not convinced why encodings for binding-introducing constructs like let (shown in Figure 1 of the paper) are considered third-order.</p>

CC BY-SA 3.0
2013-12-02T21:32:11.907Z
http://en.wikipedia.org/wiki/Higher-order_abstract_syntax
Chad Brewbaker
<functional-programming>
What is higher-order in higher-order abstract syntax?
Gowtham Kaki
# What is higher-order in higher-order abstract syntax?

(Asked by: username_0 on 2013-12-02)

I understand that using higher-order abstract syntax essentially means using host (meta) language abstraction facilities to represent binders in embedded (object) language. But, Why exactly is it higher-order? Why is traditional abstract syntax called first-order abstract syntax?

I read the paper (Frank Pfenning, and Conal Elliott, Higher-Order Abstract Syntax, PLDI'88) that introduced HOAS as we use today. I could not quite understand the following paragraph ($\S$ 3.2) that describes encoding in HOAS:

> In this first generalization, simply typed lambda terms represent programs. .. . The lexical terminals and the operators that do not introduce variable bindings are, respectively, first-order and second-order constants of the $\lambda$-calculus. Another crucial change occurs for the variables. Operators in the object language that are binding constructs are now explicitly encoded as third-order constants. As the following examples will show, this requires that bound object language variables actually become variables in the typed lambda calculus.

Particularly, I am not convinced why encodings for binding-introducing constructs like let (shown in Figure 1 of the paper) are considered third-order.

**Tags:** functional-programming
> **Comments:**
> **username_1**: http://en.wikipedia.org/wiki/Higher-order_abstract_syntax  

---

## 2 answers

### Answer by username_2 on 2013-12-04. Score: 7 | Accepted answer

Re: "why encodings for binding-introducing constructs are considered third-order", the conventions are a bit arbitrary, and I've usually heard these encodings described as "second-order". For example, although in [these notes by Gilles Dowek](http://who.rocq.inria.fr/Gilles.Dowek/Publi/unification.ps%E2%80%8E), the order $o(T)$ of a simple type $T$ (Definition 2.3) is defined as

\begin{align}
o(p) &= 1 \tag{$p$ atomic} \\
o(S \to T) &= \max(1+o(S),o(T))
\end{align}

on the other hand in [these notes by Herman Geuvers](http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf), the order $h(T)$ of a simple type $T$ (Definition 22/Exercise 7) is defined as

\begin{align}
h(p) &= 0 \tag{$p$ atomic} \\
h(S \to T) &= \max(1+h(S),h(T))
\end{align}

I'm not sure why Pfenning & Elliott chose the 1-indexed numbering scheme, but I suppose it might be the influence of the literature on higher-order matching/unification.


---

### Answer by username_3 on 2013-12-03. Score: 17

You can think of $\lambda$-abstraction as an operator $\Lambda$ which takes a *function* from terms to terms into a term:
$$\Lambda : (\mathsf{Term} \to \mathsf{Term}) \to \mathsf{Term}.$$
The type of $\Lambda$ is *higher-order* because it maps *functions* to *objects*, so it is a *functional* of rank 2. This is where the name comes from.

For example, if $\mathsf{id}$ is the identity map then $\Lambda(\mathsf{id})$ is the term $\lambda x . x$.

Constructors, for example $\mathsf{succ}$ as a constructor for the type of natural numbers, can naturally be viewed as *first-order* because they take terms to terms.

Of course, for the above to make sense, we need to be able to speak about functions between terms at the meta-level. And there are various subtleties: in principle one can have weird functions between terms that do not correspond to anything that can be written down in the syntax (consider a non-computable map). So if you're not careful, you're going to end up with "exotic terms" $\Lambda(f)$ that create a lot of trouble.

The usual solution is to somehow limit $\mathsf{Term} \to \mathsf{Term}$ to only "nice" functions. One possibility is [PHOAS](http://adam.chlipala.net/papers/PhoasICFP08/), another is to use a meta-theory such as Logical Frameworks in which only nice functions exist.


---

