2021/09/10 by Jerome Jochems
Computer Science · #cs.FL #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.344.4
published as EPTCS 344, 2021, pp. 36-64 · In Proceedings HCVS 2021, arXiv:2109.03988
arxiv created 2021/09/10 · arxiv updated 2021/09/13
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.