# The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

arXiv: https://arxiv.org/abs/1605.00371 · HTML: https://mlsanity.com/paper/1605.00371/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 May 2016.

## Built on by (most cited first, 1 of 1)

- [Directed Regular and Context-Free Languages](https://mlsanity.com/paper/2401.07106/) (2024)

## Abstract (arXiv)

A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.