Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn Clauses

TL;DR

This paper introduces a coinductive extension of higher-order constrained Horn clauses (HoCHC) and encodes higher-order recursion schemes into HoCHC, linking their equivalence problems to semi-decidability in logic.

Contribution

It presents a coinductive version of HoCHC with a greatest model property and encodes higher-order recursion schemes into HoCHC, connecting their equivalence to semi-decidability.

Findings

Encoding of higher-order recursion schemes into HoCHC

Reduction of HoRS equivalence to semi-decidability of coinductive HoCHC

Establishes a link between program equivalence and logic semi-decidability

Abstract

Higher-order constrained Horn clauses (HoCHC) are a semantically-invariant system of higher-order logic modulo theories. With semi-decidable unsolvability over a semi-decidable background theory, HoCHC is suitable for safety verification. Less is known about its relation to larger classes of higher-order verification problems. Motivated by program equivalence, we introduce a coinductive version of HoCHC that enjoys a greatest model property. We define an encoding of higher-order recursion schemes (HoRS) into HoCHC logic programs. Correctness of this encoding reduces decidability of the open HoRS equivalence problem -- and, thus, the LambdaY-calculus B\"ohm tree equivalence problem -- to semi-decidability of coinductive HoCHC over a complete and decidable theory of trees.