Higher-order recursion schemes

A higher-order recursion schemes, or HOCS, is a grammar-like abstraction of a functional program.

More specifically, a HOCS is a "typed" grammar over the set of simple types

  A, B \Coloneqq \omicron\ |\ A \to B

where \omicron is an unspecified base type, and A \to B is a function type.

It consists of:

A set \Sigma of terminals. These are "final symbols" or "tree constructors", that refer to calls to not-yet-provided functions (or libraries). Each f \in \Sigma has type of the form f : \omicron \to ... \to \omicron, where the arity \textsf{ar}(f) is the number of \omicron's minus 1.
A set \mathcal{N} of non-terminals. These are calls-to-be-evaluated, and are also typed.
A distinguished start symbol S \in \mathcal{N}.
A set of rewrite rules of the form

F\ x_1 \ldots x_n \to e

where F : A_1 \to \ldots \to A_n \to \omicron is a non-terminal, and e : o is a term of the simply-typed \lambda-calculus generated from \Sigma, \mathcal{N}, the variables \{ x_i : A_i \}, and application. Note: no abstraction can be used in e!

The order of a recursion scheme is the highest order of its non-terminals, which in turn is the order of its type. It is known that

Order 0 terms generate regular trees
Order 1 terms generate algebraic trees, i.e. those of context-free tree grammars.
Order 2 terms generate hyperalgebraic trees.

Relationship to other formalisms

This calculus may be considered as a subsystem of the \lambda\mathbf{Y}-calculus, i.e. the simply-typed \lambda-calculus equipped with a fixpoint combinator at each type. (Note that this slightly less than PCF, which also requires some base type, e.g. booleans of natural numbers.)

References

An introduction to model checking HOCS can be found in a LICS 2015 invited talk by Luke Ong:

Ong, Luke. 2015. ‘Higher-Order Model Checking: An Overview’. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–15. Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.9.

@inproceedings{ong_2015,
	address = {Kyoto, Japan},
	title = {Higher-{Order} {Model} {Checking}: {An} {Overview}},
	doi = {10.1109/LICS.2015.9},
	booktitle = {2015 30th {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science} ({LICS})},
	publisher = {IEEE},
	author = {Ong, Luke},
	year = {2015},
	pages = {1--15},
}