Back to Search
Start Over
Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn Clauses
- Source :
- Electronic Proceedings in Theoretical Computer Science. 344:36-64
- Publication Year :
- 2021
- Publisher :
- Open Publishing Association, 2021.
-
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.<br />Comment: In Proceedings HCVS 2021, arXiv:2109.03988
- Subjects :
- FOS: Computer and information sciences
Discrete mathematics
Computer Science - Logic in Computer Science
Computer Science - Programming Languages
Correctness
Horn clause
Formal Languages and Automata Theory (cs.FL)
Modulo
Coinduction
Recursion (computer science)
Computer Science - Formal Languages and Automata Theory
Logic in Computer Science (cs.LO)
Decidability
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Logic in Computer Science
Tree (set theory)
Equivalence (measure theory)
Programming Languages (cs.PL)
Mathematics
Subjects
Details
- ISSN :
- 20752180
- Volume :
- 344
- Database :
- OpenAIRE
- Journal :
- Electronic Proceedings in Theoretical Computer Science
- Accession number :
- edsair.doi.dedup.....8a877b8ab55667e6bdc4a883f2ee4b1e