Defunctionalization of Higher-Order Constrained Horn Clauses

TL;DR

This paper introduces a novel defunctionalization algorithm that reduces higher-order constrained Horn clauses to first-order ones, enabling efficient SMT solving and verified for soundness and completeness.

Contribution

The paper presents the first sound and complete defunctionalization algorithm for higher-order constrained Horn clauses, along with a prototype implementation and empirical evaluation.

Findings

DefMono successfully defunctionalizes higher-order Horn clauses.

The defunctionalization preserves solvability in both directions.

Empirical results show competitive performance with existing tools.

Abstract

Building on the successes of satisfiability modulo theories (SMT), Bj{\o}rner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic program verification. The notion of first-order constrained Horn clauses has recently been extended to higher-order logic by Cathcart Burn et al. To exploit the remarkable efficiency of SMT solving, a natural approach to solve systems of higher-order Horn constraints is to reduce them to systems of first-order Horn constraints. This paper presents a defunctionalization algorithm to achieve the reduction. Given a well-sorted higher-order constrained Horn clause (HoCHC) problem instance, the defunctionalization algorithm constructs a first-order well-sorted constrained Horn clause problem. In addition to well-sortedness of the algorithm's output, we prove that if an input HoCHC is solvable, then the result of its defunctionalization is solvable. The converse also holds, which we prove using a recent result on the continuous semantics of HoCHC. To our knowledge, this defunctionalization algorithm is the first sound and complete reduction from systems of higher-order Horn constraints to systems of first-order Horn constraints. We have constructed DefMono, a prototype implementation of the defunctionalization algorithm. It first defunctionalizes an input HoCHC problem and then feeds the result into a backend SMT solver. We have evaluated the performance of DefMono empirically by comparison with two other higher-order verification tools.