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
where is an unspecified base type, and is a function type.
It consists of:
where is a non-terminal, and is a term of the simply-typed -calculus generated from , , the variables , and application. Note: no abstraction can be used in !
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
This calculus may be considered as a subsystem of the -calculus, i.e. the simply-typed -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.)
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},
}