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

Jerome Jochems

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öhm tree equivalence problem - to semi-decidability of coinductive HoCHC over a complete and decidable theory of trees.

In Hossein Hojjat and Bishoksan Kafle : Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021), Virtual, 28th March 2021, Electronic Proceedings in Theoretical Computer Science 344, pp. 36–64.
Published: 13th September 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.344.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org