CLP(H): Constraint Logic Programming for Hedges

TL;DR

CLP(H) introduces a constraint logic programming framework over hedges, enabling reasoning with sequences of unranked terms, and provides a sound, terminating solver with completeness in specific fragments.

Contribution

This paper formalizes the algebraic semantics of CLP(H), develops a sound and terminating constraint solver, and identifies fragments with complete solutions, advancing logic programming with hedge constraints.

Findings

The solver is sound and terminating.

Certain constraint fragments yield complete solutions.

Classes of programs generating these constraints are characterized.

Abstract

CLP(H) is an instantiation of the general constraint logic programming scheme with the constraint domain of hedges. Hedges are finite sequences of unranked terms, built over variadic function symbols and three kinds of variables: for terms, for hedges, and for function symbols. Constraints involve equations between unranked terms and atoms for regular hedge language membership. We study algebraic semantics of CLP(H) programs, define a sound, terminating, and incomplete constraint solver, investigate two fragments of constraints for which the solver returns a complete set of solutions, and describe classes of programs that generate such constraints.