Solvable Tuple Patterns and Their Applications to Program Verification
Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka
TL;DR
This paper introduces solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel tools for inferring invariants in recursive data structures, significantly advancing automated program verification capabilities.
Contribution
It presents the formalism, inference algorithms, and integration of STPs and CSTPs into a CHC solver, improving verification of recursive data structures.
Findings
CSTP inference can be efficiently derived from positive samples only.
Incorporating CSTPs into a CHC solver enhances verification of list-like data structures.
The solver won the ADT-LIN category of CHC-COMP 2025 by a large margin.
Abstract
Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We introduce solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel formalisms for expressing and inferring invariants between list-like recursive data structures. A distinguishing feature of STPs is that they can be efficiently inferred from only a small number of positive samples; no negative samples are required. After presenting properties and inference algorithms of STPs and CSTPs, we show how to incorporate the CSTP inference into a CHC (Constrained Horn Clauses) solver supporting list-like data structures, which serves as a uniform backend for automated program verification tools. A CHC solver incorporating the (C)STP inference has won the ADT-LIN category of CHC-COMP 2025 by a significant margin.
| Solver | Solved (SAT) | Solved (UNSAT) | Solved (all) |
|---|---|---|---|
| CHoCoL | 180 ( 97) | 80 ( 0) | 260 ( 97) |
| RInGen | 64 ( 23) | 37 ( 4) | 101 ( 27) |
| Spacer | 20 ( 2) | 90 ( 0) | 110 ( 2) |
| Eldarica | 20 ( 0) | 84 ( 0) | 104 ( 0) |
| HoIce | 25 ( 6) | 45 ( 0) | 70 ( 6) |
| Catalia | 87 ( 11) | 87 ( 0) | 174 ( 11) |
| CHoCoL+Catalia | 194 | 84 | 278 |
| Mode | Solved SAT instances | Uniquely solved SAT instances |
|---|---|---|
| list-stp-mode | 89 | 50 |
| set/multiset-mode | 9 | 5 |
| list-len-mode | 78 | 42 |
| refutation | 4 | 0 |
| Total | 180 | 97 |
| Properties | Required Properties |
|---|---|
| Soundness (Theorem 2.1) | Lemma A.2 |
| Soundness 2 (Theorem 3.1) | Lemmas A.1, A.3, and A.10 |
| Completeness (Theorems 3.2 an 3.3) | Lemmas A.1 and A.11 and Theorem 2.1 |
| Minimality (Theorem 3.4) | Lemmas A.1, A.3, A.4, A.6, A.7, Lemma A.8, and A.10 |
| Characteristic Data (Theorem 3.5) | Lemmas A.14 and A.15, in addition to all the lemmas above |
| Learnability of STPs (Theorems 3.6 and 3.8) | Soundness and the existence of characteristic data (Theorems 2.1 and 3.5) |
| Learnability of CSTPs (Theorems 3.6 and 3.7) | Soundness, completeness and Lemma A.16 |
| Complexity of Decision Problems (Theorem 3.9) | Lemmas A.4, A.6, and A.7 |
| Decidability of Satisfiability (Theorem 3.10) | Lemma A.4 and decidability of word equations |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Solvable Tuple Patterns and Their Applications
to Program Verification
Naoki Kobayashi The University of Tokyo
Ryosuke Sato Tokyo University of Agriculture and Technology
Ayumi Shinohara Tohoku University
Ryo Yoshinaka33footnotemark: 3
Abstract
Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We introduce solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel formalisms for expressing and inferring invariants between list-like recursive data structures. A distinguishing feature of STPs is that they can be efficiently inferred from only a small number of positive samples; no negative samples are required. After presenting properties and inference algorithms of STPs and CSTPs, we show how to incorporate the CSTP inference into a CHC (Constrained Horn Clauses) solver supporting list-like data structures, which serves as a uniform backend for automated program verification tools. A CHC solver incorporating the (C)STP inference has won the ADT-LIN category of CHC-COMP 2025 by a significant margin.
1 Introduction
1.1 Background
Although a lot of progress has recently been made in automated program verification techniques, fully automated verification of programs involving algebraic data types (ADTs) such as lists and trees remains difficult. In the case of programs manipulating only integers, key invariants on loops and recursive functions can often be expressed by linear integer arithmetic, and good techniques (such as interpolants [28, 49] and counterexample-guided abstraction refinement [13]) for automatically finding them have been developed. In contrast, in the case of programs manipulating ADTs, key invariants often involve inductive predicates, which are difficult to find automatically.
To see the difficulty of automated verification of programs involving ADTs, let us consider the following OCaml program:111This example has been taken from https://github.com/chc-comp/chc-comp24-benchmarks/blob/main/ADT-LIA/chc-comp24-ADT-LIA-140.smt2.
let rec reva l1 l2 = match l1 with [] -> l2 | x::l1’ -> reva l1’ (x::l2) let main l1 l2 = assert(reva (reva l1 l2) [] = reva l2 l1)
The function reva takes two lists and as arguments, and returns a list obtained by appending the reverse of to ; for instance, . The function main takes two lists and and asserts that holds.
Suppose we wish to prove that the assertion in the function main does not fail for any and . That amounts to proving the proposition:
[TABLE]
where intuitively means that may return ; it is defined as the least predicate that satisfies the following clauses:
[TABLE]
Equivalently, it suffices to prove that there exists a predicate that satisfies all the three clauses (1)–(3); in other words, it suffices to find an invariant among the arguments and the return value of reva that is strong enough to satisfy (1).
Automatically proving the above property is non-trivial. One can easily see that directly trying to prove (1) by induction on , or would get stuck. Unfold/fold transformations [55, 16, 6] are often used for reasoning about relational properties (ones between multiple function calls, in the above case), but they would not directly apply either, because the two recursive calls and induct over different variables. A reasonable way to prove (1) is to find a lemma ,222Here, we identify lists with sequences. We write for the reverse of , and for the concatenation of two sequences (or lists) and . but how to automatically find such a lemma remains a challenge. In fact, the satisfiability of the clauses (1)–(3) is an instance of the CHC satisfiability problem [8], and there are various CHC solvers supporting ADTs [29, 41, 11, 68], but to our knowledge, none of them (except the one proposed in this paper) can automatically find the model of that satisfies the clauses (1)–(3).
1.2 Our Approach
1.2.1 Solvable Tuple Patterns for Automated Invariant Discovery
To enable automated inference of invariant relations among list-like (functional) data structures (like the relation above), we introduce the notion of solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), and apply a data-driven approach to infer them. A tuple pattern is of the form , where consists of constants (representing elements of a sequence), variables, concatenations, and the reverse operation. The pattern represents the set of all tuples of sequences obtained by instantiating the variables to sequences. For example, the invariant on the relation above is expressed as , where and are variables representing sequences. The tuple pattern expresses the set of tuples where and are respectively a prefix and a suffix of , and and overlap with each other in (as represented by ); thus 333Here, we denote elements by letters. belongs to , but does not. The tuple patterns have been inspired from Angluin’s pattern language [4] (in fact, by using a special symbol , a tuple pattern can be expressed as a pattern ). Pattern languages have a good property that they can be learned from only positive samples (in the sense of Gold [23]), but dealing with them are computationally costly: even the membership problem is NP-complete [3] and the inclusion is undecidable [53]. We thus introduce a subclass of tuple patterns called solvable tuple patterns. As we discuss later, the solvable tuple patterns have several pleasant properties:444The definition of solvability and the precise meaning of the properties (i)–(iv) will be given later in Section 3. (i) like pattern languages, they can be learned from only positive samples; (ii) there is a (non-deterministic) polynomial-time algorithm for inferring a solvable tuple pattern, given positive samples; (iii) only a small number of positive samples are required for learning a solvable tuple pattern (for example, to infer , only two samples: and are sufficient); and (iv) the satisfiability of quantifier-free formulas consisting of word equations and membership constraints on solvable patterns is decidable. Both of the patterns and above belong to the class of solvable patterns.
The learnability from only positive samples is attractive in the context of program verification. Positive samples (such as input/output pairs of a function, and states at the beginning of a loop) can be easily collected by random executions of a program. In contrast, negative samples (states that would lead to errors) are also required by many of the recent data-driven approaches to invariant discovery for automated program verification [22, 10, 75, 76], but collecting negative samples is often harder, since it requires backward executions of a program. Some of the approaches require even “implication constraints” [22, 10, 21].
To apply STPs to automated verification of list-manipulating programs, we consider CHCs on words, which are Horn clauses extended with word equality/inequality constraints. The clauses on above may be considered CHCs on words, by viewing lists as words. We show (i) given a set of CHCs on words consisting of definite clauses, there exists an algorithm to compute the least model describable by conjunctive STPs (i.e., a conjunction of a finite number of STPs),555Stated without using the terminology of CHCs, this means that there exists an algorithm that, given a list-manipulating program with loops and first-order recursive functions, computes the strongest inductive invariant expressible in CSTPs, . and (ii) it is decidable whether a given system of CHCs over words has a model describable by conjunctive STPs. We can directly apply these results to the example, and automatically obtain the invariant: .
1.2.2 Combination with Arithmetic Reasoning
Whilst CSTPs have attractive features as mentioned above, invariants expressed by CSTPs are not always strong enough for the purpose of program verification, especially for programs using a combination of lists and integers. For example, consider the following program.
let rec take n l = if n=0 then [] else match l with [] -> [] | x::l’ -> x::(take (n-1) l’)
let rec drop n l = if n=0 then l else match l with [] -> [] | _::l’ -> drop (n-1) l’
Given an integer and a list as arguments, the function take returns the list consisting of the first (at most) elements of , and drop returns the list obtained by removing the first (at most) elements from . Suppose we wish to prove that holds for every (non-negative) integer and list (where @ denotes the list append function). By using solvable tuple patterns, we can infer the properties that and respectively return a prefix and a suffix of , but they are not strong enough to derive .
To address the issue above, we combine STP inference with existing automated verification tools (more specifically, CHC solvers over integer arithmetic [29, 41, 11]). For the example above, we construct the following integer program by abstracting lists to their lengths.666As discussed in Section 5, we actually apply this kind of transformation to CHCs, rather than source programs.
let rec take’ n l = if n=0 then 0 else if l=0 then 0 else let l’=l-1 in 1+(take’ (n-1) l’)
let rec drop’ n l = if n=0 then l else if l=0 then 0 else let l’=l-1 in drop’ (n-1) l’
Here, the second argument of take’ and drop’ is an integer, representing the length of the second argument of the original functions take and drop. We then try to prove that the abstract version of the property: holds for all integers and . State-of-the-art CHC solvers can quickly solve that verification problem, and can infer invariants like:
[TABLE]
Here, (, resp.) represents the relationship between the arguments and of take’ (drop’, resp.) and the return value . By combining them with the output of solvable tuple pattern inference, we obtain the invariant candidates:
[TABLE]
These are indeed invariants strong enough to satisfy .
The above method is somewhat reminiscent of methods (such as Nelson-Oppen combination procedure [52]) for deciding combinations of theories; indeed, it combines a method for reasoning about lists (based on STP inference) with one for verifying integer programs. Various techniques to combine static analyses have also been proposed [14, 26, 15]. To our knowledge, however, the way we combine methods for solving problems in individual domains also seems novel.
1.3 Contributions and the Organization of This Paper
The contributions of this paper are summarized as follows.
- •
Development of the theory and algorithms for solvable tuple patterns (STPs) and conjunctive STPs (CSTPs). To the best of our knowledge, the notions of STPs and CSTPs are novel and of independent interest even outside the context of automated program verification, for example in algorithmic learning theory.
- •
Applications of solvable tuple patterns to automated verification of list-manipulating programs.777This paper targets programs manipulating functional (i.e., immutable) lists. Handling programs manipulating mutable linked lists and other mutable data structures would require combining our method with other techniques [48]; see Remark 5.2. To this end, we introduce CHCs over words and show that it is decidable whether a given system of CHCs over words has a model describable by CSTPs. We also consider CHCs over multisets and sets, and show that it is decidable whether a given system of CHCs over multisets or sets has a model describable by the corresponding multiset or set version of CSTPs. We further propose a method to strengthen this approach by combining it with verification methods for integer-manipulating programs.
- •
Implementation and experiments. Based on the results above, we implemented a new CHC solver called CHoCoL, which supports list-like data structures. We evaluated CHoCoL on the benchmark set of the CHC-COMP 2025 ADT-LIA category, and found that CHoCoL significantly outperformed other CHC solvers. A combination of CHoCoL with another solver called Catalia [37] won the CHC-COMP 2025 ADT-LIA category by a large margin.
The rest of the paper is structured as follows. In Sections 2–4, we introduce the notion of solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), present algorithms for inferring them from positive samples, and prove that the classes of STPs and CSTPs satisfy desired properties. Section 5 shows how to apply CSTPs to CHC solving (and hence also automated program verification). Section 6 reports an implementation and experimental results. Section 7 discusses related work and Section 8 concludes the paper.
2 Tuple Patterns and Inference Algorithm
In this section, we introduce the notions of tuple patterns and conjunctive tuple patterns, and provide inference algorithms. In the next section, we will introduce a subclass of tuple patterns called solvable tuple patterns as the sound and complete characterization of the class of tuple patterns inferable by the algorithm.
2.1 Tuple Patterns and Conjunctive Tuple Patterns
Let be a set of letters, and a (countably infinite) set of variables. We assume that contains at least two distinct letters. For the purpose of representing a relation among lists, is the set of possible list elements; for example, if we consider integer lists, then we let be the set of integers. Below we often write for elements of . We write for the domain of a map .
The sets of tuple patterns and conjunctive tuple patterns, ranged over by and respectively, are defined by:
[TABLE]
A tuple pattern represents a set of -tuples of -sequences, i.e., a -ary relation between sequences, obtained by replacing each variable with a sequence of letters in . For example, represents the set of triples of the form where . Formally, we define as: where are the variables occurring in , and denotes the simultaneous substitution of for . A conjunctive tuple pattern (where ) represents the intersection of the sets of tuples represented by , as defined by: . For example, represents the set of triples where both and are prefixes of ; here, note that variables are implicitly bound in each conjunct: the two occurrences of in and may be distinct. We write for a sequence. By abuse of notation, we write for a sequence and also for a tuple pattern , depending on the context; similarly for sequences and of variables and strings respectively.
We identify tuple patterns up to variable renaming. For example, we identify with . We write and for the sets of variables occurring in and respectively. We write for the concatenation of two patterns sequences and , and often omit , writing . We write for the length of a pattern . For a tuple pattern , we write and respectively for and .
We will later (in Section 4) extend tuple patterns with the pattern (which represents the reverse of ), to accommodate the example in Section 1.
Remark 2.1**.**
In the case of a singleton tuple pattern , our definition of coincides with the definition of a variation of pattern languages [4, 3] called E-pattern languages (or erasing pattern languages) [64]. In the definition of original pattern languages [4, 3] (called NE-pattern languages), ; empty strings cannot be substituted for variables. In view of the application to program verification discussed in Section 5, we allow substitutions of empty strings, which correspond to empty lists. ∎
2.2 Tuple Pattern Inference Problem
Learning data, denoted by , is an -matrix consisting of elements of . We write for the element in the -th row and -th column. We also write for , and for . We write for , for , for , and for , where denotes the length of string . We sometimes regard learning data as the set , and write when is a subset of as sets.
Let and . If and , we write for the learning data such that and . For example, if M^{\prime}=\left(\begin{array}[]{cc}a&b\\ bb&a\end{array}\right) and , then [M^{\prime}/(x,y)]t=\left(\begin{array}[]{ccc}a&b&ab\\ bb&a&bba\end{array}\right). We use the metavariable for a substitution . We sometimes use the matrix notation:
[TABLE]
for the substitution such that .
When holds, we write . We also write if and there exists no variable such that (i.e., if no variable is always mapped to ). We write (, resp.) if there exists such that (, resp.), and we call a witness substitution for (, resp.). For a conjunctive tuple pattern , we write (, resp.) if (, resp.) holds for every .
Example 2.1**.**
Let be: \left(\begin{array}[]{ll}a&aaa\\ b&abb\end{array}\right) and be . Then , where \Theta=\left(\begin{array}[]{c}x\\ a\\ b\end{array}\right) is a witness substitution. We also have for \Theta=\left(\begin{array}[]{cc}x&y\\ a&\epsilon\\ b&\epsilon\end{array}\right), but as always maps to . ∎
Example 2.2**.**
Let be: \left(\begin{array}[]{rrr}a&\ b&\ ab\\ aa&\epsilon&aa\end{array}\right). Then, . In fact, for \Theta=\left(\begin{array}[]{cc}x&y\\ \epsilon&b\\ a&\epsilon\end{array}\right), we have . In this case, we also have , with the same witness substitution. ∎
The tuple pattern inference problem is the problem of, given learning data , finding a tuple pattern such that . For instance, for in Example 2.1, is an answer to the inference problem.
2.3 Inference Algorithm
We now present a (non-deterministic) algorithm for tuple pattern inference. We formalize it by using a rewriting relation . Starting with the initial state (where ), the algorithm repeatedly applies the rewriting rules below until no further rule is applicable. When the final pair is , then is the inferred tuple pattern. In other words, given , our algorithm for tuple pattern inference (non-deterministically) outputs such that . As we will see later (in Theorem 2.1), implies , because the rewriting relation maintains the invariant .
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][i]\neq\widetilde{\epsilon}\quad\quad M[*][j]=M[*][i]\cdot\widetilde{s}\quad\quad x_{j}^{\prime}\mbox{ fresh}\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/(x_{1},\ldots,x_{m})])\longrightarrow([x_{i}x_{j}^{\prime}/x_{j}]t,[M\{j\mapsto\widetilde{s}\}/(x_{1},\ldots,x_{j-1},x_{j}^{\prime},x_{j+1},\ldots,x_{m})])\end{array}} (R-Prefix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][j]=a\cdot\widetilde{s}\quad\quad a\in\Sigma\quad\quad x_{j}^{\prime}\mbox{ fresh}\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/(x_{1},\ldots,x_{m})])\longrightarrow([ax_{j}^{\prime}/x_{j}]t,[M\{j\mapsto\widetilde{s}\}/(x_{1},\ldots,x_{j-1},x_{j}^{\prime},x_{j+1},\ldots,x_{m})])\end{array}} (R-CPrefix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][i]\neq\widetilde{\epsilon}\quad\quad M[*][j]=\widetilde{s}\cdot M[*][i]\quad\quad x_{j}^{\prime}\mbox{ fresh}\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/(x_{1},\ldots,x_{m})])\longrightarrow([x_{j}^{\prime}x_{i}/x_{j}]t,[M\{j\mapsto\widetilde{s}\}/(x_{1},\ldots,x_{j-1},x_{j}^{\prime},x_{j+1},\ldots,x_{m})])\end{array}} (R-Suffix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][j]=\widetilde{s}\cdot a\quad\quad a\in\Sigma\quad\quad x_{j}^{\prime}\mbox{ fresh}\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/(x_{1},\ldots,x_{m})])\longrightarrow([x_{j}^{\prime}a/x_{j}]t,[M\{j\mapsto\widetilde{s}\}/(x_{1},\ldots,x_{j-1},x_{j}^{\prime},x_{j+1},\ldots,x_{m})])\end{array}} (R-CSuffix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][j]=\widetilde{\epsilon}\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/(x_{1},\ldots,x_{m})])\longrightarrow([\epsilon/x_{j}]t,[M\mathbin{\uparrow_{j}}/(x_{1},\ldots,x_{j-1},x_{j+1},\ldots,x_{m})])\end{array}} (R-Epsilon)
Here, denotes the matrix obtained from by removing the -th column, and denotes the matrix obtained from by replacing the -th column with . We write for the sequence obtained from by appending to the head of each element of .
The rule R-Prefix is for the case where the -th column of is a prefix of the -th column. In this case, we replace the -th column with its suffix obtained by removing the prefix , and instantiate in accordingly to . The rule R-CPrefix is for the case where a constant is a prefix of the -th column, and the rule R-Epsilon is for the case where every element of the -th column is an empty sequence. In the latter case, the -th column is removed.
Example 2.3**.**
Recall the data in Example 2.1: M=\left(\begin{array}[]{ll}a&aaa\\ b&abb\end{array}\right). The pattern is inferred (up to variable renaming) as follows.
[TABLE]
Actually, the patterns such as and obtained in intermediate steps are also valid solutions of the inference problem, but the final pattern describes a smaller relation than them. ∎
Example 2.4**.**
Recall the data in Example 2.2: M=\left(\begin{array}[]{rrr}a&\ b&\ ab\\ aa&\epsilon&aa\end{array}\right). The pattern is inferred (up to variable renaming) as follows.
[TABLE]
∎
The following example shows that the result of tuple pattern inference may not be unique.
Example 2.5**.**
Consider the data: M=\left(\begin{array}[]{rrr}aa&\ a&\ aac\\ b&\ bb&\ bbd.\end{array}\right). Here, both the first and second columns are prefixes of the third column. We obtain or depending on which column is chosen in R-Prefix.
[TABLE]
[TABLE]
The first pattern obtained describes that the first element is a prefix of the third element, while the second pattern describes that the second element is a prefix of the third element. The conjunctive pattern subsumes both patterns. ∎
Definition 2.1** (Algorithms and ).**
We write for a non-deterministic algorithm that takes data as input, applies the rewriting rules to until no further rule is applicable, and outputs some tuple pattern such that . We write for a deterministic algorithm that takes data as input and outputs the conjunctive tuple pattern .
Note that the set of such that is finite; thus we can indeed compute by an exhaustive search. Note, however, that runs in time exponential in in the worst case.
We now state some key properties of the algorithm ; other important properties are discussed in Section 3. Proofs omitted below are found in Appendix A. The theorem below states the soundness of the algorithm, which follows immediately from the fact that implies . See Appendix A for more details.
Theorem 2.1** (soundness).**
Suppose are mutually distinct variables and . If returns , then .
Our non-deterministic algorithm can find a pattern in time polynomial in the size of given data.
Theorem 2.2**.**
Given as input, runs in time polynomial in .
Proof.
In each step of rewriting, an applicable rule can be found and applied in polynomial time, if there is any. Since each step of the rewriting strictly decreases , the length of the rewriting sequence is linear in . ∎
3 Solvable Tuple Patterns
In this section, we introduce the notions of solvable tuple patterns (STPs) and conjunctive solvable tuple patters (CSTPs), which characterize the classes of (conjunctive) tuple patterns that can be inferred by our algorithms. The pattern on a singleton tuple is obviously non-inferable by our algorithm, and it is indeed deemed non-solvable in the characterization below. In contrast, the pattern is solvable.
Remark 3.1**.**
Instead of restricting the class of tuple patterns, one may expect to obtain an extension of the algorithm that can infer arbitrary tuple patterns. Unfortunately, learning arbitrary tuple patterns from positive samples is computationally infeasible. As mentioned in Remark 2.1, singleton tuple patterns coincide with E-patterns [64], and the full class of E-pattern languages is not learnable from positive data in general (more precisely, it is not learnable when the alphabet size is 2, 3, or 4 [59, 60] and the learnability is unknown when the alphabet size is larger). Also, the inclusion problem is undecidable for both NE- and E-pattern languages [32, 53]. In contrast, STPs have good algorithmic properties, as discussed in Section 3.4. ∎
3.1 Solvability
We define the notion of solvability via a reduction relation on tuple patterns. Just as the rewriting relation in Section 2 detects prefix/suffix relationships in data and simplifies the data accordingly, the reduction detects prefix/suffix relationships in patterns and simplifies the patterns. The reduction relation is defined by:
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=p_{i}\cdot p^{\prime}_{j}\quad\quad p_{i}\neq\epsilon\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p^{\prime}_{j},p_{j+1},\ldots,p_{n})\end{array}} (PR-Prefix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=a\cdot p^{\prime}_{j}\quad\quad a\in\Sigma\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p^{\prime}_{j},p_{j+1},\ldots,p_{n})\end{array}} (PR-CPrefix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=p^{\prime}_{j}\cdot p_{i}\quad\quad p_{i}\neq\epsilon\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p^{\prime}_{j},p_{j+1},\ldots,p_{n})\end{array}} (PR-Suffix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=p^{\prime}_{j}\cdot a\quad\quad a\in\Sigma\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p^{\prime}_{j},p_{j+1},\ldots,p_{n})\end{array}} (PR-CSuffix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=\epsilon\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p_{j+1},\ldots,p_{n})\end{array}} (PR-Epsilon)
Each rule of name PR-xx corresponds to the rule R-xx; while the rule R-xx manipulates data , the rule PR-xx applies the corresponding operation to a tuple pattern, and simplifies the pattern. We define the set of -ary solvable tuple patterns (STPs, for short) as: \{t\mid t\leadsto^{*}(x_{1},\ldots,x_{n}),|t|=k,\mbox{ and x_{1},\ldots,x_{n} are distinct from each other}\}, and write for . In other words, a tuple pattern is solvable if can be reduced to a trivial pattern consisting of distinct variables. A conjunctive tuple pattern is solvable if for some . We call the pattern modified or removed in the rewriting (i.e., in the above rules) a principal pattern. We also call the pattern in PR-Prefix or PR-Suffix an auxiliary pattern.
Example 3.1**.**
, but . In fact, is obvious, as no rule is applicable to . The latter follows by:
[TABLE]
where PR-Prefix is applied in the first three steps, and PR-Epsilon is applied in the last step.
Remark 3.2**.**
In the definition of , we can actually drop the requirement that the variables are distinct from each other. Indeed, if , for example, then we can erase by:
[TABLE]
Thus, does not change even if we do not require that are distinct from each other. ∎
Remark 3.3**.**
The name “solvable tuple patterns” comes from the following fact. Suppose . Then, the general solution for a system of equations can be expressed by using (i) , (ii) constants , (iii) the (partial) operation , which is defined as such that if is a prefix of , and (iv) the (partial) operation , which is defined as such that if is a suffix of . For example, is solvable in the sense that the system of equations has a general solution provided (or, equivalently ).
As in the case of ordinary pattern languages, the class of languages described by solvable tuple patterns (where a tuple pattern is identified with the language described by ) is incomparable with the class of context-free languages, but is subsumed by the class of indexed languages [2]. Note that the language , described by the solvable tuple pattern , is not context-free. ∎
3.2 Properties of the Inference Algorithm
As stated in the following theorems, the algorithms and defined in Definition 2.1 indeed infer STPs and CSTPs, respectively. Moreover, modulo a minor condition, they are complete for these classes.
Theorem 3.1** (inferred patterns are solvable).**
If returns , then .
Theorem 3.2** (completeness of ).**
Let be mutually distinct variables.
- (I)
If and , for some .888Recall that tuple patterns are identified up to variable renaming. 2. (II)
If and , then there exists such that and is a possible output of , i.e., .
The following theorem, obtained as a corollary of Theorems 2.1 and 3.2, says that returns the least CSTP such that .
Theorem 3.3** (completeness of ).**
Let be learning data. Then , and for every CSTP such that .
Remark 3.4**.**
Theorem 3.2 (I) would not hold if the assumption were weakened to . In fact, let and . Then and , but we can only obtain by rewriting. In fact, the only possible reduction sequences are:
[TABLE]
The rule R-Prefix is inapplicable because of the side condition . The pattern could be obtained if we removed the condition, but then we would obtain unboundedly many patterns, such as . If we add one more sample, like to above, then we can infer as expected. ∎
As observed in Example 2.5, the output of is not unique due to non-determinism (whereas is), but the following theorem states that always outputs a minimal solvable pattern.
Theorem 3.4** (minimality).**
Suppose returns . If with , then implies .
The minimality property above is important for learning from positive samples only. Suppose that we are trying to learn the language described by a tuple pattern . In learning from positive samples, we are given data consisting of only a (finite) subset of . Thus, our non-deterministic algorithm may output a “wrong” pattern such that but . Thanks to the theorem above, in such a case, there exists data . Thus, by adding the new positive sample to and running our algorithm again, the wrong pattern will not be encountered again. Without the minimality property, it could be the case , and then the pattern would not be refutable with only positive samples.
For each STP , there exist polynomial-size data that uniquely characterize . This property ensures convergence of the learning process (cf. Theorem 3.6).
Theorem 3.5** (Characteristic Data).**
Let be an STP such that . Then, there exists such that (i) , (ii) for any such that , there exists such that , and (iii) for any such that , implies . Furthermore, given , can be constructed in polynomial time.
3.3 Learnability
We have so far considered an algorithm for inferring (, resp.) such that (, resp.), given . In the whole learning process, we need to repeatedly invoke the algorithm for gradually increasing learning data , until a true STP (or CSTP) is found. In Gold’s learning model [23], a class of languages is identifiable in the limit if there exists an algorithm such that, for any language and any infinite sequence s.t. , the sequence eventually converges to (a representation of) . Both the class of STPs and that of CSTPs are learnable in this sense, and our algorithms and serve as above, as stated below.
Theorem 3.6**.**
Suppose is an STP, , and . Then, there exists such that for all . Similarly, if is a CSTP, , and , then there exists such that for all .
In applications to program verification discussed later, we use CSTPs to represent and infer inductive invariants. To that end, we need to consider a different learning model where the goal is to find the strongest inductive invariant among those describable by a CSTP, given an oracle to check the inductiveness of a CSTP. This can be regarded as a kind of active learning framework where the oracle is a teacher. The following theorem states that our algorithm can also be used in this learning framework.
Theorem 3.7**.**
Let be a monotonic function, and suppose that there exists an algorithm that, given a CSTP , returns “None” if holds, and returns for some if the inclusion does not hold. Then the procedure below eventually terminates and returns the least CSTP such that .
[TABLE]
The algorithm above first sets to so that . It then repeatedly adds to the element returned by the oracle and invokes . A crucial property to guarantee the theorem is that always returns the least CSTP such that . See Appendix for more details.
Example 3.2**.**
Consider the function append defined by:
let rec append l1 l2 = match l1 with [] -> l2 | x::l1’ -> x::(append l1’ l2).
A ternary relation is an inductive invariant describing the input-output relation of append if and only if satisfies for the following function :
[TABLE]
Here, we identify lists with words. We wish to find the strongest CSTP such that is such an , that is, the strongest satisfying . Using the procedure above, we can derive as the strongest . See also Example 5.2, where the same procedure is used to solve the example in Section 1. ∎
Theorem 3.7 above would not hold if CSTPs were replaced with STPs, because there is no guarantee that there exists a least such that . For example, suppose that is a constant function that always returns . Then, and hold for and , but there is no STP such that and . We can, however enumerate all the minimal ’s such that .
Theorem 3.8**.**
Let be a monotonic function, and suppose that there exists an algorithm that, given an STP , returns “None” if holds, and returns for some if the inclusion does not hold. Suppose also that , and an element such that is computable. Then there exists an algorithm that enumerates all the STPs such that and, for every , implies .
3.4 Decision Problems
This section investigates decision problems on STPs. We first study the membership and inclusion problems for STPs, which is useful for . Note that the membership and inclusion problems are respectively NP-complete and undecidable for both NE-pattern languages and E-pattern languages [53].
Theorem 3.9**.**
The following decision problems can be solved in polynomial time.
Given a tuple pattern , decide whether is solvable. 2. 2.
Given an STP and a tuple , decide whether . 3. 3.
Given an STP and a tuple pattern , decide whether . 4. 4.
Given two STPs and , decide whether .
To solve (1), it suffices to reduce by and check whether it ends up with a trivial pattern . Since the reduction strategy does not matter (as shown in Lemma A.6 in Appendix, is weakly confluent up to permutations), and each reduction strictly decreases , it can be checked in time polynomial in . For (3), it suffices to observe that if and , then we can find a corresponding reduction such that in polynomial time (cf. Lemma A.4 in Appendix A). If there exists no such corresponding reduction, we can conclude ; otherwise is eventually reduced to a trivial pattern , at which point we can conclude . (2) and (4) are immediate consequences of (3). More details are found in Appendix A.
We next prove the decidability of the theory of quantifier-free formulas containing formulas of the form . This decidability is important for constructing the oracle in Theorem 3.7, and plays an important role in the applications to program verification discussed in Section 5.
Definition 3.1**.**
The set of (quantifier-free) STP formulas, ranged over by , is given by:
[TABLE]
Here, ranges over the set of STPs.
For example, (which is the negation of “ implies ”), where is an STP formula. The semantics of STP formulas is defined in an obvious manner, and is therefore deferred to the Appendix. The only point to note is that the variables occurring in are implicitly bound within ; for example, is equivalent to (although we usually avoid variable overloading to prevent confusion).
Remark 3.5**.**
The definition of quantifier-free STP formulas above can be actually simplified to:
[TABLE]
because and can be expressed by and respectively. ∎
According to the result on word equations [57, 36], the satisfiability of STP formulas without STP membership constraints (i.e., Boolean combinations of formulas of the form ) is in PSPACE. Thus, we have:
Theorem 3.10**.**
Given an STP formula , one can effectively construct an equi-satisfiable STP formula such that contains no subformulas of the form or , and the size of is polynomial in that of . Therefore, the satisfiability of STP formulas is in PSPACE.
Encoding of a formula into word equations relies on the solvability of . In fact, if we allowed arbitrary tuple patterns, then the satisfiability would become undecidable, because if and only if and the latter is undecidable [32, 53].
4 Extensions and Variations of Solvable Tuple Patterns
This section discusses extensions and variations of STPs. Section 4.1 extends STPs with the reverse pattern , which is needed to handle the example in Section 1. Section 4.2 discusses variations of STPs to reason about sets and multisets.
4.1 Reverse
Let us extend the set of pattern expressions (ranged over by ) to , where . Here, represents the set of the reverse of strings represented by . We extend to the operation on patterns, by , , and , so that the set of extended pattern expressions is closed under substitutions. For example, .
We extend the tuple pattern inference algorithm with the following rules:
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][i]\neq\widetilde{\epsilon}\quad\quad M[*][j]=M[*][i]^{R}\cdot\widetilde{s}\quad\quad x_{j}^{\prime}\mbox{ fresh}\quad\quad\widetilde{x}=(x_{1},\ldots,x_{m})\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/\widetilde{x}])\longrightarrow([x_{i}^{R}\cdot x_{j}^{\prime}/x_{j}]t,[M\{j\mapsto\widetilde{s}\}/(x_{1},\ldots,x_{j-1},x_{j}^{\prime},x_{j+1},\ldots,x_{m})])\end{array}} (R-RPrefix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][i]\neq\widetilde{\epsilon}\quad\quad M[*][j]=\widetilde{s}\cdot M[*][i]^{R}\quad\quad x_{j}^{\prime}\mbox{ fresh}\quad\quad\widetilde{x}=(x_{1},\ldots,x_{m})\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/\widetilde{x}])\longrightarrow([x_{j}^{\prime}\cdot x_{i}^{R}/x_{j}]t,[M\{j\mapsto\widetilde{s}\}/(x_{1},\ldots,x_{j-1},x_{j}^{\prime},x_{j+1},\ldots,x_{m})])\end{array}} (R-RSuffix)
Here, denotes the pointwise extension of the reverse operation. Accordingly, we extend solvable tuple patterns by adding the following rules:
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=p_{i}^{R}\cdot p^{\prime}_{j}\quad\quad p_{i}\neq\epsilon\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p^{\prime}_{j},p_{j+1},\ldots,p_{n})\end{array}} (PR-RPrefix)
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=p^{\prime}_{j}\cdot p_{i}^{R}\quad\quad p_{i}\neq\epsilon\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p^{\prime}_{j},p_{j+1},\ldots,p_{n})\end{array}} (PR-RSuffix)
The theorems in Sections 2 and 3 continue to hold for this extension. For the decidability and complexity of the satisfiability problem (Theorem 3.10), we rely on known results on the satisfiability of equations over free monoids with involution [18].
Example 4.1**.**
Let be \left(\begin{array}[]{rrr}ab&\ cd&\ bacd\\ bc&da&cbda\end{array}\right). The pattern is inferred as follows.
[TABLE]
Remark 4.1**.**
One may also be tempted to extend patterns with , which represents the sequence obtained by sorting . This is problematic, however, because does not commute with concatenation: . One way to reason about sorted sequences is to introduce a new class of patterns called sort patterns, given by: and . Here, denotes the set of sorted sequences obtained by merging sorted sequences represented by and . Sort patterns can naturally be extended to tuple sort patterns. For example, denotes the set of pairs, whose second element is obtained by sorting the first element, and denotes the set of triples , where is obtained by sorting and merging it with . We can then design an inference algorithm for (solvable) tuple sort patterns in a manner similar to ordinary tuple patterns. The details will be described in a separate paper. ∎
4.2 Beyond Sequence Patterns
We have so far considered tuple patterns consisting of words, which form a free monoid. Almost the same technique can be applied to represent and infer relations among other similar algebraic structures such as multisets and sets. Note that multisets form a free commutative monoid, while sets are obtained by further imposing idempotency on the binary operation.
To deal with multisets, we just need to interpret the empty pattern and the pattern concatenation as the empty set and the multiset union, respectively, and identify patterns up to permutations (for example, ). The inferences and reduction rules for tuple patterns can be adjusted accordingly, as follows.
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][i]\neq\widetilde{\epsilon}\quad\quad\forall k.M[k][j]\supseteq M[k][i]\quad\quad\widetilde{s}=M[*][j]\setminus M[*][i]\quad\quad x_{j}^{\prime}\mbox{ fresh}\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/(x_{1},\ldots,x_{m})])\longrightarrow([x_{i}x_{j}^{\prime}/x_{j}]t,[M\{j\mapsto\widetilde{s}\}/(x_{1},\ldots,x_{j-1},x_{j}^{\prime},x_{j+1},\ldots,x_{m})])\end{array}} (R-Subset)
\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall k.a\in M[k][j]\quad\quad\widetilde{s}=M[*][j]\setminus\{a\}\quad\quad a\in\Sigma\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/(x_{1},\ldots,x_{m})])\longrightarrow([ax_{j}^{\prime}/x_{j}]t,[M\{j\mapsto\widetilde{s}\}/(x_{1},\ldots,x_{j-1},x_{j}^{\prime},x_{j+1},\ldots,x_{m})])\end{array}} (R-CSubset)
\displaystyle\frac{\begin{array}[]{@{}c@{}}M[*][j]=\widetilde{\emptyset}\end{array}}{\begin{array}[]{@{}c@{}}(t,[M/(x_{1},\ldots,x_{m})])\longrightarrow([\epsilon/x_{j}]t,[M\mathbin{\uparrow_{j}}/(x_{1},\ldots,x_{j-1},x_{j+1},\ldots,x_{m})])\end{array}} (R-Empty)
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=p_{i}p^{\prime}_{j}\quad\quad p_{i}\neq\epsilon\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p^{\prime}_{j},p_{j+1},\ldots,p_{n})\end{array}} (PR-Subset)
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=ap^{\prime}_{j}\quad\quad a\in\Sigma\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p^{\prime}_{j},p_{j+1},\ldots,p_{n})\end{array}} (PR-CSubset)
\displaystyle\frac{\begin{array}[]{@{}c@{}}p_{j}=\epsilon\end{array}}{\begin{array}[]{@{}c@{}}(p_{1},\ldots,p_{n})\leadsto(p_{1},\ldots,p_{j-1},p_{j+1},\ldots,p_{n})\end{array}} (PR-Empty)
Most of the results for STPs and CSTPs carry over to their multiset versions (called SMTPs and CSMTPs), including the soundness and completeness of the inference algorithm, Theorem 3.7, and Theorem 3.10 (where word equations are replaced with multiset equations, and the complexity of satisfiability is changed to NP). A notable exception is that the minimality property (Theorem 3.4) fails, but it is not an obstacle to the application to program verification discussed in the next section. Similarly, we can deal with sets by interpreting concatenation as disjoint union.
Example 4.2**.**
Let be: \left(\begin{array}[]{rrr}\{a,a\}&\ \{a,b\}&\ \{a,a,b\}\\ \{a,b\}&\ \{b,c\}&\{a,b,c\}\end{array}\right). The pattern (which means that the third set is a superset of the first and second sets, where is the intersection of the first and second sets) is inferred as follows.
[TABLE]
Remark 4.2**.**
Similar techniques can also be applied to binary trees, which are obtained by dropping associativity of the binary operation and thus form a free magma. Using the tree version of STPs, we can, for example, represent and infer tree relations such as , where is the binary tree constructor; this means that the first element is the left subtree of the second. The formalization and applications of this tree version of STPs to automated program verification are left for future work. ∎
Remark 4.3**.**
While the theory of STPs can be applied to other similar free algebraic structures as discussed above, freeness is important for STPs. Many of the theorems in Section 3 rely on properties such as the following: if , then with for some ; and if , then with for some .999See the longer version [39] for a table summarizing the properties used in the proof of each main theorem. Such properties do not necessarily hold for arbitrary monoids. For example, consider a monoid generated by , and with identity element , subject to the equation and . In this monoid, holds, but there is no pattern such that .
One may wonder whether it is possible to develop a general, unifying theory of STPs for a certain class of free algebraic structures, and then instantiate the theory to each structure. That does not seem straightforward, however. The proof of minimality (Theorem 3.4) relies on word-specific properties, such as the fact that implies and are in a prefix relation. Such properties do not hold for free commutative monoids, and that is why minimality fails for multisets. Moreover, the forms of characteristic data differ between words and multisets. Thus, developing such a unifying theory is outside the scope of this paper and left for future work. ∎
5 Applications to Automated Verification of List-Manipulating Programs
This section discusses how to apply the (C)STP inference to automated verification of programs manipulating list-like data structures. We focus on CHC-based automated program verification [9], where program verification problems are reduced to the satisfiability problem for constrained Horn clauses (CHCs, a.k.a. constraint logic programs), and passed to an automated CHC solver. The CHC satisfiability problem is undecidable in general, but a number of CHC solvers that automatically solve it have been developed, though they are inevitably incomplete. These solvers typically support integer and real arithmetic, arrays, and ADTs. An annual competition on CHC solvers called CHC-COMP is held. The CHC-based approach provides a uniform, language-agnostic approach to automated verification. It has recently been studied extensively and applied to various languages, ranging from low-level languages like C and LLVM [27, 66], to high-level languages like Java [34], Rust [48], and OCaml [67, 10]. As noted in Section 1, however, CHC solvers over ADTs have so far been unsatisfactory.
Below we first introduce a class of CHCs with word constraints, and show that it is decidable whether a system of CHCs (i.e., a finite set of CHCs) in that class has a model describable using CSTPs in Section 5.1. This result is directly applicable to the example in Section 1. Sections 5.2 and 5.3 discuss further enhancement of the STP-based CHC solving.
5.1 Constrained Horn Clauses over Words
A constrained Horn clause (CHC) is a Horn clause extended with constraints. It is of the form: , or , where may be [math]. We call a clause of the former form a definite clause, and one of the latter form a goal clause. Here, and are predicate variables, and ranges over the set of constraint formulas over certain domains; the first-order variables and are assumed to be implicitly universally quantified in each clause. A clause that can be normalized to the above form is also called a CHC. For example, is also a CHC, as it is equivalent to . We often just write for the clause , by eliminating redundant variables and omitting “”.
The CHC satisfiability problem (or, the CHC problem) asks, given a set of CHCs, whether there exists a model (i.e., an interpretation of predicate variables) that makes all the clauses valid. For example, consider the following system of CHCs over integer arithmetic.
[TABLE]
It is satisfiable. Indeed, satisfies all the clauses. Henceforth, we often use a formula to express a model, like . A model is not unique in general; for the example above, is also a model.
In this section, instead of CHCs over integer arithmetic, we consider CHCs on words over . Thus, each variable ranges over the set of words, and constraints are drawn from the set of quantifier-free STP formulas as defined in Definition 3.1.
Example 5.1**.**
The example in Section 1 is expressed as the following system of CHCs .
[TABLE]
Here, the constraint can be expressed by , assuming that the alphabet is finite.
Let . Then is a model of the CHCs above. ∎
We say that a system of CHCs on words has a CSTP-model if there exist such that is a model of . The following is the main result of this section.
Theorem 5.1**.**
Given a system of CHCs on words, it is decidable whether has a CSTP-model.
Proof Sketch..
Let , where and respectively consist of definite and goal clauses. By Theorem 3.7, the least CSTP-model of exists and it is computable (note that the algorithm for can be constructed by using Theorem 3.10). Then, has a CSTP-model if and only if is a model of . The latter is decidable by Theorem 3.10. ∎
An analogous result holds also when restricted to STP-models. We say that a system of CHCs on words has an STP-model if there exist STPs such that is a model of . Here, we add a special STP that denotes the empty set (i.e., ).
Theorem 5.2**.**
Given a system of CHCs on words, it is decidable whether has an STP-model.
To prove the theorem, it suffices to use Theorem 3.8 instead of Theorem 3.7.
Proof Sketch..
Let , where and respectively consist of definite and goal clauses. By Theorems 3.8 and 3.10, we can enumerate all the minimal STP-models of . Then, it suffices to check whether one of the minimal STP-models is also a model of . ∎
The unsatisfiability of CHCs (where models are not restricted to CSTPs) is also semi-decidable:
Theorem 5.3**.**
There exists a procedure which, given a system of CHCs on words, eventually outputs “Unsat” whenever is not satisfiable.
Proof.
This follows from the fact that is unsatisfiable if and only if there is a resolution proof. Thanks to the decidability of word equations, we just need to enumerate a candidate resolution proof, and check whether it is a valid proof. ∎
Note, however, that the satisfiability of CHCs is undecidable in general if models are not restricted to CSTPs. To see this, notice that a natural number can be encoded as the word .
Below, we demonstrate how we can automatically obtain a CSTP-model for the -example. For the sake of simplicity, we omit constant patterns.
Example 5.2**.**
Recall the CHCs in Example 5.1. We first compute the least model of the definite clauses (i.e., the first two clauses) , based on the algorithm in Theorem 3.7. First, we set and , and check whether satisfies . Using the algorithm in Theorem 3.10, we obtain an element that should belong to the least model.
Then, we set , and get . This does not satisfy the second clause. Indeed, the formula obtained by negating the second clause: has a model , from which we obtain a new element . By setting , we obtain . Since has a model , we obtain the new element: .
By setting , we obtain . Now, is a model of . Since is also a model of the goal clause, we can conclude that is satisfiable, and hence also that the reva program in Section 1 does not suffer from assertion failures. ∎
In Appendix B, we extend CSTP-models to piecewise CSTP-models, and apply them to verification of functional queues.
Remark 5.1**.**
In Example 5.2 above, if we replace used inside the algorithm of Theorem 3.7 with , then the inference may fail. Consider the state above. If is invoked instead of , we may obtain as a minimal (but not the least) such that . Then, as a model of , we may obtain , which yields .
By setting , we obtain . Note that . Thus, we have failed to infer the least model of , and therefore, we have also failed to prove that is satisfiable.
We can still prove the satisfiability of by using only STPs, based on Theorem 5.2 (which relies on Theorem 3.8 instead of Theorem 3.7). ∎
Remark 5.2**.**
The results above can be directly applied to automated verification of programs manipulating functional lists. To handle programs manipulating mutable linked lists, we can use the technique of RustHorn [48] to convert mutable linked lists into functional lists, and then apply our technique. Other mutable data structures can be mapped to (functional) trees using the technique of RustHorn [48]. We can then either (i) apply the tree version of STPs mentioned in Remark 4.2, or (ii) abstract trees to lists and then apply our results on CHCs over words. We expect, for example, that programs over binary search trees can be verified using the latter approach, by abstracting a binary search tree to the list of its elements. Skip lists [58] could also be handled in a similar manner: despite the name “lists,” they would first be mapped to trees reflecting their physical structure, and then abstracted to a tuple of lists , where is the list of elements at level . The structural properties of a skip list—namely, that each is a sorted sequence and that is a subsequence of for any —can be described using the pattern of sorted sequences mentioned in Remark 4.1. At present, however, these applications remain speculative. A concrete formalization and implementation are left for future work. ∎
5.2 Combination with CHC Solving for Integer Arithmetic
The CHCs obtained from list-manipulating programs typically contain integer constraints in addition to word (or list) constraints. The CSTPs alone are not always sufficient to express appropriate invariants for such CHCs. Let us recall the second example (involving take and drop) in Section 1. It can be expressed as the satisfiability of the following CHCs:
[TABLE]
Here, we have omitted the clauses for . As before we have encoded lists into words, but the resulting CHCs also contain integer constraints. Ignoring the integer constraints, the least CSTP model of the definite clauses obtained by is: , , and . It is not strong enough to satisfy the goal clause (i.e., the last clause above).
To address the issue, we use a CHC solver over integers to strengthen the model of definite clauses. We abstract lists to their lengths and obtain the following abstract version of the CHCs.
[TABLE]
In general, given a system of CHCs over lists , (i) the list constructors and are replaced with their length abstractions [math] and , (ii) the list equalities (which implicitly occur in the clause bodies) are replaced with integer equalities; and (iii) the list inequalities in the body of goal clauses are replaced with the integer inequalities, and those in the bodies of definite clauses are replaced with .
The above abstraction ensures that a model of the abstract version of definite clauses yields that of the original definite clauses : if satisfies , then satisfies (where we assume are integer arguments and are list arguments); this follows from the soundness of the catamorphism-based abstraction of CHCs [37].
In contrast, there is no such guarantee for the goal clauses: because of the replacement of and with and , the abstract version of goal clauses is neither stronger nor weaker than the original goal clauses. (Notice that is an over-approximation of , while is an under-approximation of .) The abstract goal clauses, however, tend to help a CHC solver to find an appropriate invariant. In the case above, if were replaced with , we would obtain , which is so strong that the abstract CHCs would become unsatisfiable.
Suppose a CHC solver yields the following model for the abstract CHCs above:
[TABLE]
Then we have the following model for the definite clauses of the original CHCs.
[TABLE]
By conjoining them with the candidate model obtained by using STP inference, we obtain:
[TABLE]
This satisfies the goal clause, and thus we have proved that the original system of CHCs is satisfiable.
In general, in parallel to running the least CSTP model, we apply the length abstraction and use a CHC solver over integer arithmetic to solve the abstract CHCs and obtain a model . (Here, we assume that is the length abstraction of the original predicate , where and are integer and list arguments respectively.) Then when checking whether the least CSTP model satisfies the goal clause, we strengthen the candidate model by conjoining .
Remark 5.3**.**
Instead of just using the information obtained from the length abstraction, it is possible to propagate information gathered from STP inference and length abstraction to each other, as in Nelson-Oppen procedure [52] for theory combinations. For example, suppose that is found to imply by STP inference. Then, each occurrence of in the body of a clause can be replaced by , before applying the length abstraction. Then, a clause of the form is abstracted to . ∎
Remark 5.4**.**
In theory, the above method for utilizing CHCs over integer arithmetic is not restricted to the length abstraction: any sound abstraction of lists to integers [37] would work. Our restriction to the length abstraction comes from the following practical motivation. As in the example above, the final candidate model involves both sequence constraints and constraints on integers obtained by abstracting lists. The state-of-the-art SMT solvers like CVC5 and Z3 work fairly well for a combination of sequences and length functions, but do not work well for a combination of sequences and arbitrary recursive functions on sequences, to our knowledge. ∎
5.3 Beyond Sequence and Integer Constraints
The (conjunctive) solvable set/multiset tuple patterns discussed in Section 4.2 are also applicable to CHC solving, as stated in the theorem below. Here, CHCs over multisets refer to those whose constraint formulas are drawn from those on multisets [56]. The theorem follows from the set/multiset versions of Theorems 3.7, 3.8, and 3.10.
Theorem 5.4**.**
Given a system of CHCs over multisets, it is decidable whether has a CSMTP-model. Similarly, given a system of CHCs over sets, it is decidable whether has a CSSTP-model.
Theorem 5.5**.**
Given a system of CHCs over multisets, it is decidable whether has an SMTP-model. Similarly, given a system of CHCs over sets, it is decidable whether has an SSTP-model.
Example 5.3**.**
Let us consider the following insertion sort program:
let rec insert x l = match l with [] -> [x] | y::l’ -> if x<y then x::l else y::(insert x l’) let rec isort l = match l with [] -> [] | x::l’ -> insert x (isort l’) let main l = assert(eq_as_multiset (isort l) l).
The function main takes a list as input, sorts it, and asserts that the result is equivalent to as multisets; here, for the sake of simplicity, we assume that eq_as_multiset is a primitive. By abstracting lists to multisets and overapproximating the formula by , we obtain the following CHCs over multisets, whose satisfiability implies the lack of assertion failures.
[TABLE]
By running the multiset version of the procedure of Theorem 3.7, we obtain the following least CSMTP-model for definite clauses:
[TABLE]
Since it satisfies the goal clause , we can conclude that the system of CHCs above is satisfiable, and hence also that the program does not suffer from assertion failures. In the same manner, we can also verify that the merge and quick sort programs preserve the multiset of elements, fully automatically (without any invariant annotations for auxiliary functions such as merge and partition). ∎
6 Implementation and Experiments
We have implemented a tool called TupInf for (C)STP inference based on the algorithm in Section 3, and a new CHC solver called CHoCoL based on the method in Section 5, using TupInf as a backend. Section 6.1 gives an overview of those tools, and Section 6.2 reports experimental results.
6.1 Implementation
6.1.1 TupInf: a Solvable Tuple Pattern Inference Tool
TupInf has been implemented in OCaml. TupInf takes learning data in the csv format, and outputs STPs or CSTPs with the extensions described in Sections 4.1 (reverse), and 4.2 (set and multiset patterns). The alphabet used in the learning data consists of digits and uppercase and lowercase English letters. TupInf provides options to (i) enable or disable constant patterns (i.e., R-CPrefix and R-CSuffix), (ii) choose between STPs and CSTPs, and (iii) select between sequence, multiset, and set patterns. The option for constant patterns was disabled in the experiments reported below.
6.1.2 CHoCoL: a CHC Solver for List-like Data Structures
CHoCoL (Constrained Horn Clauses over Lists) is also implemented in OCaml and uses TupInf for CSTP inference, Z3 [17] and CVC5 [7] for SMT solving, and HoIce [10] for CHC solving over integer arithmetic, as backend solvers. Currently, CHoCoL supports only list-like data structures as ADTs, i.e., ADTs that have two constructors: one with no arguments and the other with two arguments whose types are some element type and the ADT itself. CHoCoL also supports natural numbers represented as lists with unit elements. CHoCoL has five internal modes: list-stp-mode, set-mode, multiset-mode, list-len-mode, and list-cstp-mode. Given a system of CHCs as input, CHoCoL tries five modes (in the order listed above) one by one until it finds that the CHCs are satisfiable. In the list-stp-mode and list-cstp-mode, the tool infers tuple patterns for list-like data structures as described in Section 5.1, but the inferred patterns are restricted to STPs in the former for the sake of efficiency. (Experimental results suggest that CSTP inference itself can be performed efficiently in practice, but it sometimes outputs a large CSTP, which can impose significant overhead on the underlying SMT solver when checking its validity.) In the list-len-mode, it additionally infers invariants on the lengths of lists as described in Section 5.2 by using the backend CHC solver for integer arithmetic.
The procedure explained so far can only prove the satisfiability of the CHCs. Thus, CHoCoL also runs in parallel a procedure based on symbolic execution to prove the unsatisfiability. Given a CHC whose goal clause is , CHoCoL searches for an assignment to variables that makes the body () of the goal clause valid by recursively unfolding the predicates in the goal in a breadth-first manner. The details of this procedure are omitted, since it is rather straightforward and contains few novel ideas. It would be possible to utilize the result of tuple pattern inference also to speed-up the refutation process, but that is left for future work.
6.2 Experiments
We have conducted experiments on a benchmark set selected from CHC-COMP 2025 ADT-LIN category. The benchmark set consists of 445 instances of the CHC satisfiability problem, which are all the instances of the ADT-LIN category where the used ADTs are only list-like data structures. The experiments were conducted on a machine with AMD Ryzen 9 5900X CPU and 32GB RAM. The cpu and wallclock time limits were 3 minutes, and the memory limit was 8GB. The number of CPU cores was limited to 4.
We compared CHoCoL with the state-of-the-art CHC solvers that support ADTs: RInGen [42], Spacer/Racer [41, 33], Eldarica [29], HoIce [10, 11], and Catalia [37]. The results are shown in Table 1 and Figure 1. To confirm that our method serves as a complement to previous methods, we have also prepared a combination of CHoCoL and Catalia, shown as CHoCoL+Catalia in the table and figure; it runs CHoCoL and Catalia in parallel.101010A combination of CHoCoL (without seq-cstp-mode) and Catalia, called “ChocoCatalia” won the ADT-LIN category of CHC-COMP 2025; the configuration of CHoCoL+Catalia reported in this submission slightly differs from “ChocoCatalia”.
Table 1 shows the numbers of solved instances by CHoCoL and the other CHC solvers. For each solver, the column Solved (SAT) (resp. Solved (UNSAT)) shows the number of satisfiable (resp. unsatisfiable) instances solved, and the column Solved (all) shows the total number of instances solved. The numbers in parentheses indicate instances uniquely solved by the solver, i.e., those that no other solver (except CHoCoL+Catalia) could solve within the time limit.
The experimental results demonstrate the effectiveness of CHoCoL. CHoCoL achieved the highest total number of solved instances (260) among all compared solvers, showing its overall superiority in handling CHCs with list-like data structures. A key strength of CHoCoL is its performance on satisfiable instances, where it solved 180 instances compared to 87 by Catalia and 64 by RInGen. More importantly, CHoCoL uniquely solved 97 satisfiable instances,111111A increase of the time limit would not significantly change the situation, because the benchmark set contains a number of instances that require reasoning about list equalities, as in the examples in Section 1, which cannot be solved by Catalia and RInGen, which abstract lists to integers or elements of a finite domain. demonstrating the effectiveness of the STP inference approach for CHC solving.
The result of CHoCoL+Catalia, though, shows that CHoCoL also has a limitation, and that it is better to use it as a complement to other solvers. Also, in contrast with the strong performance of CHoCoL for SAT instances, CHoCoL showed slightly lower performance than other solvers (except RInGen) for UNSAT instances. This is unsurprising because our current refutation procedure is quite naive. We plan to apply STP inference also to improve the refutation procedure.
Figure 1 gives cactus plots, showing how many instances were solved within a given time. The left subfigure (a) shows the numbers of solved instances for all instances, and the right subfigure (b) shows the numbers of solved instances for SAT instances. It is remarkable that, for the successful instances, CHoCoL solved many of them almost instantly, within one second.
Table 2 shows the numbers of solved SAT instances by each mode of CHoCoL. The row “refutation” shows the number of instances found to be satisfiable only by finite unfolding. Remarkably, the list-stp-mode alone solved more SAT instances than the other solvers. As shown in the row “list-len-mode”, the combination of STPs and CHC solving over integer arithmetic was also effective. There were no uniquely solved instances for list-cstp-mode; this suggests that although CSTPs are required in theory (cf. Theorem 5.4), STPs often suffice in practice.
We have also manually inspected some of the SAT instances that could not be solved by CHoCoL. They typically involve functions such as sort, filter, map, and fold, whose input/output relations cannot be expressed by STPs. We plan to extend our framework to support those list functions, along the line suggested in Remark 4.1.
7 Related Work
7.1 Learning Languages from Positive Samples
The problem of learning a language from only positive samples [23] has been actively studied, and various language classes have been found to be learnable. As already mentioned, most closely related to our notion of tuple patterns is Angluin’s pattern languages [4, 3] and its variations [64, 65]. Indeed, “erasing” pattern languages [64, 65] (in which empty strings may be substituted for variables, as opposed to Angluin’s original pattern languages) can be considered singleton tuple patterns, and conversely, if we introduce a special symbol (which must not occur in strings substituted for variables; such a restriction may be expressed by patterns with regular constraints [[64](#bib.bib64)]), then a tuple pattern(p_{1},\ldots,p_{n})p_{1}\mathdollar\cdots\mathdollar p_{n}. No polynomial time learning algorithm is known for the full class of pattern languages (and in fact, the existence of such an algorithm is highly unlikely given the result of [[3](#bib.bib3)]). Various subclasses of pattern languages are known to be polynomial time learnable from positive data [[3](#bib.bib3), [63](#bib.bib63), [59](#bib.bib59), [64](#bib.bib64), [50](#bib.bib50)]. Among others, Angluin [[3](#bib.bib3)] and Shinohara [[65](#bib.bib65)] gave polynomial time algorithms respectively for patterns consisting of a single variable and for “regular” (erasing) patterns where each variable may occur only once. Mitchell [[50](#bib.bib50)] extended the latter result to quasi-regular patterns, where variables must occur the same number of times. Those subclasses are not large enough to express tuple patterns like (xy,xyx)$ (which contains two variables, each of which occurs a different number of times).
Other classes of languages learnable only from positive samples (i.e., “identifiable in the limit” [23]) include: reversible languages [5], strictly locally testable languages [71], “very simple grammars” [70, 72], substitutable context-free languages and their variations [12, 73, 74], and length-bounded elementary formal systems [65]. Except the length-bounded elementary formal systems [65], those classes are not expressive enough to subsume solvable tuple patterns. In fact, most of them are subclasses of regular or context-free languages. For length-bounded elementary formal systems [65], there exists no efficient learning algorithm.
Gulwani et al. [25, 24] invented a method for inferring string functions from translation examples and applied it to spreadsheets. Although their method is heuristic and does not satisfy good learning-theoretic properties like ours to our knowledge, it would be interesting to integrate their technique with ours to infer invariants for functional relations.
7.2 Data-Driven Approaches to Program Verification
Various data-driven approaches to program verification have recently been proposed, especially for automated discovery of program invariants. Some of them require only positive samples [62, 30, 77], some require negative samples as well [76, 75, 61], and some require even implication examples of the form , which means “if are positive samples, then is also positive” [22, 10, 21, 40]. The used techniques vary from algebraic ones [62, 30], SVM [76, 75], and neural networks [61, 40]. Most of those techniques have been used mainly for the discovery of invariants on integers, and it is unclear how they can be adopted to discover invariants on list-like data structures.
Among them, the techniques of Sharma et al. [62] and Ikeda et al. [30] are technically closest to ours (although they are for discovering numerical equality constraints), in that those methods can also quickly infer equality constraints only from a small number of examples. In fact, our STP inference algorithm, which repeatedly simplifies learning data in matrix form, has been inspired by those techniques. Ikeda et al. [30] applied that technique to CHC solving. The application to CHC solving is less trivial in our context, however. In the case of Ikeda et al. [30], which finds equality constraints on integers, it is sufficient to insert those invariants as a part of preprocessing, and then invoke an off-the-shelf CHC solver. For example, if we can find an invariant , then we can provide that information to a CHC solver, just by replacing every occurrence of in CHC with . In contrast, since there are no CHC solvers that can directly reason about sequence equality constraints, we had to develop a more sophisticated method for applying the result of CSTP inference to CHC solving, as discussed in Section 5. Actually, Theorem 5.1 can also be adopted for the method of Ikeda et al. [30] as follows: given a system of CHCs over linear integer arithmetic, it is decidable whether has a model that can be described solely by conjunctions of linear integer equalities of the form .
Zhu et al. [77] proposed a data-driven approach to learning invariants of (immutable) data structures. Their technique learns relations between two nodes of a data structure (e.g., “for every cons-cell in a list, the value of every cell reachable from is no less than that of ”), and can therefore reason about properties such as the sortedness of a list. To our knowledge, however, their technique cannot be applied to reasoning about the logical equivalence of lists; in fact, their abstraction for lists cannot distinguish [1;1;1;2;2] from [1;1;2;2;2]. Therefore, their technique cannot handle either of our motivating examples in Section 1. Related techniques have been developed for verifying programs that manipulate mutable data structures [35, 31], but these techniques also cannot reason about the logical equality of lists.
7.3 CHC Solving for Algebraic Data Types
Solving CHCs over algebraic data types (or, automated verification of programs manipulating ADTs) often require finding and reasoning about inductive properties. To this end, Unno et al. [69] introduced an automated method for applying induction in CHC solving. De Angelis et al. [16] later proposed a method to achieve similar effects without explicit induction, by using unfold/fold transformations. Mordvinov and Fedyukovich [51] also proposed a variation of unfold/fold transformations. Losekoot et al. [44, 45] applied automata-based techniques to reason about relational properties of ADTs, which also have a similar effect to unfold/fold transformation-based techniques. These methods tend to be fragile, requiring a lot of heuristics to automatically decide how and when to apply induction, unfold/fold transformations, etc.
Several methods for CHC solving have also been proposed, which abstract ADTs to elements of a finite domain or integers. Kostyukov [42] proposed a method for abstracting ADTs using automata, while the Eldarica CHC solver [29] abstracts ADTs by their size. Govind V. K. et al. [33] proposed a method that uses recursively defined functions (RDTs) over ADTs for abstraction, but those RDTs must be explicitly specified. Katsura et al. [37] proposed a method for automatically finding a catamorphism-based abstraction for ADTs. While these methods are effective for certain CHCs, they are not effective for proving the equality of ADTs; although the abstraction by using an abstraction map may be used for proving , it does not imply in general. Thus, those methods cannot be used to prove neither of the examples in Section 1. As confirmed in our experiments, our method using CSTPs is complementary to those methods; in fact, the combination of our method with Catalia achieved the best performance in the experiments in Section 6, and also in the competition CHC-COMP 2025.
7.4 Combination of Static Analyses
In Section 5.2, we have shown how to strengthen our STP inference-based CHC solving procedure by combining it with an off-the-shelf CHC solver for integer arithmetic. There have been studies on how to combine static analyses [14, 26, 15] in the context of abstract interpretation. The particular way of combining CHC solving methods, however, appears to be novel. As discussed in Section 5.2, the CHCs obtained by the length abstraction is neither sound nor complete with respect to the original CHCs (the satisfiability of the abstract CHCs neither implies nor is implied by the satisfiability of the original ones), but we can still obtain useful information from a solution of the abstract CHCs, for solving the original CHCs. Our combination method treats a CHC solver for integer arithmetic as a black box, allowing any CHC solvers to be used, including those based on PDR [41], predicate abstraction [29], and data-driven methods [11, 75]. We have discussed only a specific combination in Section 5.2; it would be an interesting direction for future work to further generalize and formalize the idea of combining CHC solvers over different domains.
8 Conclusions
We have introduced the new notions of solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), and developed their theories. In particular we have shown that both STPs and CSTPs are learnable from only positive samples, and that the satisfiability of quantifier-free formulas is decidable. We have applied those theories to prove that it is decidable whether a system of CHCs over words has a CSTP-describable model. We have implemented a new CHC solver called CHoCoL based on the proposed approach, and confirmed the effectiveness of the approach through experiments.
Future work includes: (i) generalizing STPs to trees and other algebraic structures (cf. Remark 4.2) to handle tree-like data structures and support reasoning about other list operations (cf. Remark 4.1); (ii) extending STPs to infer Boolean combinations of STPs, such as , meaning that either the first or second element is a prefix of the third; (iii) applying other classes of languages learnable from positive samples to CHC solving; and (iv) extending and generalizing the method for combining CHC solvers over different domains.
Acknowledgment
We thank the anonymous reviewers for their useful feedback. This work was supported by JSPS KAKENHI Grant Number JP20H05703 and JP26H02486.
Data Availability Statement
The artifact of this paper is available on Zenodo [38]. It includes the instructions, software, benchmark set, and scripts to reproduce the experiments in the paper.
Appendix
Appendix A Proofs
A.1 Proofs and Additional Definitions for Sections 2 and 3
This section provides proofs omitted in Sections 2 and 3.
We first show basic properties in Sections A.1.1–A.1.3. The dependency of each main property on basic properties is summarized in Table 3, so that it is easy to discuss properties of the extensions and variations of STPs considered in Section 4.
A.1.1 Properties of
Lemma A.1**.**
Let be mutually distinct variables. If , then there exists such that and .
Conversely, if , then for any tuple pattern .
Proof.
This follows by a straightforward (simultaneous) induction on the length of the rewriting sequence, with case analysis used in the first step. Note that in the rules for , there is no condition on in the premise. ∎
Lemma A.2**.**
If , then .
Proof.
This follows by a straightforward case analysis on the rule used for deriving . ∎
A.1.2 Properties of
Lemma A.3**.**
If , then .
Proof.
Trivial by the definition of . We have actually or , and the latter occurs only when empty sequences are substituted for some variables. For example, when and , . ∎
When holds, we define a partial function on tuple patterns as follows.
Definition A.1** ().**
Let and be tuple patterns such that . We define the tuple pattern such that as follows, by case analysis on the rule used for deriving :
- •
Case PR-Prefix: In this case, and with and for some and for . If is of the form and is a prefix of , then where and for . (Recall that denotes such that . We have if , and if .) Otherwise, is undefined.
- •
Case PR-Suffix: In this case, and with and for some and for . If is of the form and is a suffix of , then where and for . Otherwise, is undefined.
- •
Case PR-CPrefix: In this case, and with for some and for . If is of the form and is a prefix of , then where and for . Otherwise, is undefined.
- •
Case PR-CSuffix: In this case, and with for some and for . If is of the form and is a suffix of , then where and for . Otherwise, is undefined.
- •
Case PR-Epsilon: In this case, and . If is of the form , then . Otherwise, is undefined.
Note that above depends on which rule has been used for deriving ; for example, if has been derived by R-Prefix and if has been derived by R-CPrefix. Thus, when we write , we assume that carries information about the rule used for deriving .
We defined above so that the reduction “simulates” the reduction in the following sense.
Lemma A.4**.**
If and , then is well defined and . 2. 2.
If is well defined, then if and only if ; and if and only if .
Proof.
Case analysis on the rule used for deriving . Since the other cases are similar or simpler, we discuss only the case for PR-Prefix. We may assume, without loss of generality, and with . To show (1), assume . Then for any , must be a prefix of . Thus must also be of the form . (To see this, suppose and is not a prefix of . Then either (i) with (i.e., is a strict prefix of ) or (ii) and with and (i.e., are the first letters or variables that differ between and ). In case (i), let be a substitution such that , and in case (ii), let be a substitution such that . Then is not a prefix of . Thus, must be a prefix of . ) Therefore, is well defined, and .
To show (2), suppose is well defined. Then, and where may be . Thus, we have:
[TABLE]
from which the required properties follow immediately. ∎
Next, we will prove the weak confluence of (up to permutations). To that end, we prepare the following lemma.
Lemma A.5**.**
Suppose for . Then, there exists such that (q_{1},p)\leadsto^{*}t\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}(q_{2},p).
Proof.
This follows by induction on . If , then . Therefore, the property holds for . Otherwise, by the assumption , either is a prefix of , or is a prefix of .
In the former case, with . Thus, we have (q_{1},p)\leadsto t\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}(q_{2},p) for .
In the latter case, . We may assume that , since otherwise. Thus, we have . By the induction hypothesis, there exists such that (q_{1},p^{\prime})\leadsto^{*}t\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}(q_{2},p^{\prime}). Thus, we have (q_{1},p)\leadsto(q_{1},p^{\prime})\leadsto^{*}t\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}(q_{2},p^{\prime})\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}(q_{2},p) as required. ∎
Remark A.1**.**
The lemma above also follows immediately from the following property of words (cf. [46], Proposition 12.1.2): “If , and , then there exists and an integer such that , and .” By using this property, we obtain (q_{1},p)\leadsto^{*}(sr,r)\leadsto(s,r)\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}(rs,r)\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}(q_{2},p). ∎
We write if is a permutation of . For example, . The following lemma states that is weakly confluent up to .
Lemma A.6** (weak confluence of up to ).**
If and , then there exist and such that t_{1}\leadsto^{*}t_{1}^{\prime}\sim t_{2}^{\prime}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}t_{2}.
Proof.
It is sufficient to consider the cases where and the parts involved in the two reductions overlap. Without loss of generality, we may assume that the first element is principal in . We thus need to consider only the following cases; due to the symmetry between prefix and suffix, the cases involving only suffixes are omitted.
- •
Case and (i.e., both reductions use PR-Prefix, and is principal in both reductions).
By , and are in the prefix relation. By symmetry, we may assume that , with . Then we have:
[TABLE]
as required. In the second reduction step for , if and otherwise.
- •
Case and (i.e., both reductions use PR-Prefix, and is auxiliary in ).
In this case, we have and . Then we have:
[TABLE]
as required. In the second reduction step for , if and otherwise.
- •
Case and (i.e., uses PR-Prefix, while uses PR-CPrefix, and is principal in both reductions).
In this case, with . Thus, we have:
[TABLE]
as required. In the second step for , if and otherwise.
- •
Case and (i.e., uses PR-Prefix, while uses PR-CPrefix, and the auxiliary element in the former reduction is principal in the latter).
In this case, . Thus, we have:
[TABLE]
as required. In the second step for , if and otherwise.
- •
Case where and (i.e., is principal and is auxiliary in both reductions, and uses PR-Prefix while uses PR-Suffix). In this case, . Thus, by Lemma A.5, there exists such that t_{1}\leadsto^{*}t_{3}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}t_{2}.
- •
Case where and (i.e., is principal in both reductions, and is auxiliary in the former reduction while is auxiliary in the latter; uses PR-Prefix, uses PR-Suffix). In this case, ; so, either (i) and , or (ii) and . In case (i), we have:
[TABLE]
In case (ii), we have:
[TABLE]
as required. Here, notice that reductions are confluent only up to the permutation relation .
- •
Case where and (i.e. the auxiliary element in the former reduction is principal in the latter, and uses PR-Prefix while uses PR-Suffix). In this case, we have and . Then, we have:
[TABLE]
as required.
∎
Recall that .
Lemma A.7**.**
If , then .
Proof.
This follows immediately by the case analysis on the rule used for deriving . ∎
Lemma A.8**.**
If , then .
Proof.
This follows immediately from the definition of . ∎
Lemma A.9** (Church-Rosser property of up to ).**
If t_{L,1}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}t_{L}\sim t_{R}\leadsto^{*}t_{R,1}, then there exist and such that t_{L,1}\leadsto^{*}t_{L,2}\sim t_{R,2}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}t_{R,1}.
Proof.
This follows immediately from the standard fact that weak confluence (Lemma A.6) and strong normalization (implied by Lemma A.7) implies the Church-Rosser property. For completeness, we provide a proof. We show the lemma by induction on . Suppose t_{L,1}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}t_{L}\sim t_{R}\leadsto^{*}t_{R,1}. If or , the result follows immediately by Lemma A.8. Otherwise, we have and . By Lemma A.6, there exist and such that t_{L,1}^{\prime}\leadsto^{*}t^{\prime\prime}_{L,1}\sim t_{R,1}^{\prime\prime}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}t_{R,1}^{\prime}. By the induction hypothesis, we also have:
[TABLE]
By applying the induction hypothesis to t^{\prime}_{L,3}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}t^{\prime\prime}_{L,1}\sim t^{\prime\prime}_{R,1}\leadsto^{*}t^{\prime}_{R,3}, we obtain t^{\prime}_{L,3}\leadsto^{*}t^{\prime}_{L,2}\sim t^{\prime}_{R,2}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}t^{\prime}_{R,3}. As and , by Lemma A.8, there exist and such that and . Thus, we have
[TABLE]
as required. ∎
A.1.3 Correspondence between and
Lemma A.10**.**
If , then .
Proof.
This follows by a straightforward case analysis on . ∎
Lemma A.11**.**
Suppose . If , then for some , , and . Furthermore, if , then and .
Proof.
Suppose and . We perform case analysis on the rule used for deriving .
- •
Case PR-Prefix: We may assume, without loss of generality, and , with . By , we have where . If , then R-Epsilon is applicable to . Otherwise, let with and . Then, we have . Furthermore, if , then . Therefore, the latter case applies and we have and as required.
- •
Case PR-CPrefix: In this case and . By , we have . Thus, R-CPrefix is applicable to obtain
[TABLE]
for , with and for . Thus, we also have , and implies .
- •
Cases for PR-Suffix and PR-CSuffix: analogous to the cases for PR-Prefix and PR-CPrefix respectively.
- •
Case PR-Epsilon: We may assume, without loss of generality, and . The required result holds for , and .
∎
A.1.4 Proof of Soundness (Theorems 2.1 and 3.1)
Theorem 2.1 is a trivial consequence of Lemma A.2.
Proof of Theorem 2.1.
Suppose . By Lemma A.2, we have , i.e., as required. ∎
Proof of Theorem 3.1.
This follows by induction on the length of the rewriting sequence . The base case where follows immediately. Suppose
[TABLE]
By Lemma A.1, there exist such that with . By the induction hypothesis, . By Lemma A.10, we have . By Lemma A.3, we have . Thus, we have as required. ∎
A.1.5 Proofs of Completeness (Theorems 3.2 and 3.3)
Proof of Theorem 3.2.
For (I), suppose and . By the latter condition, there exists a rewriting sequence for mutually distinct variables . We show for some by induction on the length of the rewriting sequence . The base case where follows immediately. Suppose
[TABLE]
By Lemma A.11, we have
[TABLE]
By the induction hypothesis, we have
[TABLE]
for some . By Lemma A.1, we have . Thus, we have as required.
For (II), suppose . Let be the variables such that . Then we have , i.e., . By (I), we have for some . Let be an STP such that . Then as required. ∎
Proof of Theorem 3.3.
The condition follows immediately from Theorem 2.1.
Suppose is a CSTP and . Then there exists such that for each . Let be the variables such that . Then we have , i.e., . By Theorem 3.2, we have . Let be an STP such that . Then is a conjunct of and . Thus, we have for every , which implies . ∎
A.1.6 Proof of Minimality (Theorem 3.4)
We prepare a few lemmas.
Lemma A.12**.**
If and with , then is of the form where are mutually distinct variables.
Proof.
If is not of the given form, then for some . By Lemma A.11, for some and , which contradicts the assumption . ∎
The following is a key lemma.
Lemma A.13**.**
Suppose . Then, if and only if .
Proof.
The ’if’ direction follows immediately from the definition. To show the converse, suppose and is solvable, i.e., for some mutually distinct variables . By Lemma A.9, there exist and such that (p^{\prime}_{1},\ldots,p^{\prime}_{m})\leadsto^{*}t_{3}\sim t_{4}\mbox{\rotatebox[origin={c}]{180.0}{\leadsto}}^{*}(x_{1},\ldots,x_{k}). The last condition implies , and thus, is solvable. ∎
Proof of Theorem 3.4.
The proof proceeds by induction on the length of the rewriting sequence .
In the base case, . By Lemma A.12, must be a tuple of mutually distinct variables . Thus, as required.
In the induction step, we have . By Lemma A.10, we have . By Lemma A.1, there exists such that and . By the assumption and Lemma A.4 with , we have (i) is well-defined; (ii) ; and (iii) implies . Furthermore, by and Lemma A.13, is also solvable. By (ii) and , we can apply the induction hypothesis to obtain , and by (iii), we obtain as required. ∎
A.1.7 Proof of the Existence of Characteristic Data (Theorem 3.5)
To prove Theorem 3.5, we first define characteristic learning data for each solvable tuple pattern . Let be a solvable tuple pattern. Since is solvable, contains at most distinct variables with . (Note that, at each reduction step by , the set of variables occurring in the tuple pattern does not change, and the number of elements may only monotonically decrease.) Let be two distinct variables of , and be binary codewords for using such that and for all , is neither a prefix nor a suffix of . Let be . We define as:121212The characteristic data depends on the choice of and binary prefix coding, but the choice does not matter for the discussion below.
[TABLE]
For example, let be and . Then,
[TABLE]
We use the following properties of characteristic data.
Lemma A.14**.**
Let and be solvable tuple patterns. If , then .
Proof.
This follows by induction on . If , then must be mutually distinct variables. Thus, . Suppose and . We perform case analysis on the rule used in the reduction .
- •
Case PR-Prefix: We may assume without loss of generality that and , with . By the assumption , must be of the form . By the definition of , must be of the form , and for . Since (by Lemma A.7), by the induction hypothesis, we have . Thus, we have .
- •
Cases PR-CPrefix, PR-Suffix, and PR-CSuffix: Similar to the above case.
- •
Case PR-Epsilon: We may assume without loss of generality that and . By the assumption , . Therefore, must be of the form , with for . By the induction hypothesis, we have . Thus, we have as required.
∎
Lemma A.15**.**
Let be a solvable tuple pattern, and be \left(\begin{array}[]{ccc}x_{1}&\cdots&x_{k}\\ \alpha_{1}&\cdots&\alpha_{k}\\ \beta_{1}&\cdots&\beta_{k}\\ \end{array}\right), where are the codewords for as defined above. If , then for every .
Proof.
Since is solvable, . We prove the required property by induction on the length of the reduction sequence . If , the result follows immediately, since . Otherwise, we have . We perform the case analysis on the rule used for deriving . Since the other cases are simpler or simpler, we discuss only the case for PR-Prefix, where we may assume and . By the assumption , we have . By the induction hypothesis, for every , as required. ∎
Proof of Theorem 3.5.
Let be a solvable tuple pattern such that . We show satisfies the required properties. By the definition of , . Suppose . We can assume that the first two rows of (as a matrix) coincide with . By and Theorem 3.2, we have for some . For (ii), it remains to show . By Theorem 2.1, we have . By Lemma A.15, must be:
[TABLE]
Because there exist no and such that is a prefix or suffix of , the rules R-Prefix and R-Suffix are inapplicable. Since and are swapped between ’s and ’s, the rules R-CPrefix and R-CSuffix are also inapplicable. Thus, we have as required. To show (iii), suppose . By Theorem 2.1, . By Lemma A.14, we have . By Theorem 3.4, we have as required. Obviously, the size of the characteristic data is , and it can be computed also in time . ∎
A.1.8 Proofs for Section 3.3
Lemma A.16**.**
Suppose and . Then there exist and such that and for some variables .
Proof.
This follows by induction on the length of the reduction sequence . If , then . Thus, the required result holds for the empty sequence of variables .
If , then we have . By Lemma A.1, we have with .
We perform case analysis on the rule used for deriving . Since the other cases are similar or easier, we discuss only the cases for R-Epsilon and R-Prefix.
- •
Case R-Epsilon: In this case, we have:
[TABLE]
Since , we have . Thus, we can apply the same rule to obtain: . Since , we can apply induction hypothesis to obtain such that and . Thus, the required result holds for .
- •
Case R-Prefix: In this case, We have:
[TABLE]
For simplicity, we assume and below. If , then we can apply the same rule to and obtain the required result. If , then we have . Thus, by the induction hypothesis, we have with for some . Let . Since and , for every variable occurring in , . Thus, by applying R-Epsilon for such variables, we obtain such that , , and for . Let . Then . Since , we have , as required.
∎
For data such that , we define as where:
[TABLE]
For example, for M=\left(\begin{array}[]{rrr}a&ab&abab\\ bb&b&bb\end{array}\right), is:
[TABLE]
(Note that we also have , but is subsumed by , as .)
We claim:
Lemma A.17**.**
Suppose . If , then .
Proof.
To show , suppose is a conjunct of . Since contains at most variables, by the definition of , there exists such that . Thus, . Therefore, we have , as required.
For the converse, suppose . Then, we have for some . Let be a tuple pattern such that . Then, is a conjunct of , and therefore, we have . Thus, we have , as required. ∎
We define the order by: iff . Note that is well-founded.
Lemma A.18**.**
Suppose is an infinite, strictly decreasing sequence of non-empty data, i.e., . Then, there exists such that for all , .
Proof.
By Lemma A.16, we have:
[TABLE]
Since is well-founded, there exists such that for all , . By Lemma A.17, we have for all . ∎
Proof of Theorem 3.6.
Suppose is an STP, and with . By Theorem 3.5, there exists such that always returns an STP equivalent to for any , and by the soundness of (Theorem 2.1), we have . Since , there exists such that . Therefore, for every , always returns an STP equivalent to .
To show the case for CSTPs, suppose is a CSTP and with . By Lemma A.18, there exist and such that for all , . By the soundness of (Theorem 2.1), we have . By Theorem 3.3, we also have . Therefore, we have , as required. ∎
Proof of Theorem 3.7.
We first show the termination of the procedure by contradiction. Suppose the procedure does not terminate. Then, there exist infinite sequences and such that:
[TABLE]
These , , and are the values of , , and at the -th iteration of the loop in the procedure. By the last condition and the assumption on , we have . By the soundness of (Theorem 2.1), we have . Therefore, , and hence, is a strictly increasing sequence. By Lemma A.18, there exist and such that for all . This however, contradicts and .
Next, we show that the procedure returns the least CSTP such that . Suppose for a CSTP . Let , , and be the values of , , and at the -th iteration of the loop in the procedure, as given above. It suffices to show by induction on . The case is obvious, as . For the induction step, suppose and returns . By the monotonicity of , we have
[TABLE]
Thus, . Therefore, we have
[TABLE]
By Theorem 3.3, we have , as required. ∎
Proof of Theorem 3.8.
Let be the procedure defined as below, and suppose . Then outputs a superset of all the minimal ’s such that . We can then filter out non-minimal STPs by using the algorithm of Theorem 3.9 (3).
Note that in the above algorithm is a local variable, prepared for each recursive call.
We first show the termination of the algorithm. Suppose does not terminate. Since is a finite set, there must be an infinite chain of recursive calls where and for . Let be the value of initialized at the beginning of the call , and be the value of when is called. Thus, and . By Theorem 3.6, there exists and such that for all . But this contradicts the conditions but .
Next, suppose that is a minimal STP such that . It suffices to show that for any such that , outputs (an STP equivalent to) , or makes a recursive call for such that (as we have already shown the termination of the algorithm).
By the completeness (Theorem 3.2) and minimality (Theorem 3.4), the value of initialized at the beginning of the call of must contain such that . We perform case analysis on whether is picked up in the while-loop.
- •
Suppose is eventually picked up in the while-loop. Then if , then returns and is output. If , then returns such that . Thus, is called for , as required.
- •
Suppose is never picked up in the while-loop. Then must have been removed by the assignment . But then it must be the case that . Therefore, is called for , as required.
∎
A.1.9 Proofs for Section 3.4
Proof of Theorem 3.9.
(1): By Lemma A.6, if , then is solvable if and only if is solvable. By Lemma A.7, the length of a reduction sequence is bounded by . Thus, to check whether is solvable, it suffices to repeatedly reduce (in a non-deterministic manner) until no reduction is applicable, and check whether the resulting tuple pattern is of the form . As each step can be performed in polynomial time, the algorithm runs in polynomial time.
(3): Based on Lemma A.4, we can use the algorithm in Algorithm 1.
Here, we assume ; otherwise, we can immediately conclude that . The algorithm repeatedly reduces and checks whether the reduction of can be “simulated by” the corresponding reduction of . If is of the form , we can immediately conclude that holds, as . Otherwise, we can always pick such that by the assumption that is solvable. By Lemma A.4, if is well defined, then it suffices to check whether ; otherwise, we can immediately conclude that (on the last line).
Each operation can be clearly performed in time polynomial in the size of the initial inputs and . Since , the depth of the recursive call is bounded by . Thus, the algorithm runs in polynomial time. (As this proof shows, need not be solvable.)
(2): This is a special case of (3), where and is the constant pattern (whose language is a singleton set ).
(4): This is an immediate consequence of (3), as . ∎
Before proving Theorem 3.10, we define the semantics of formulas. A valuation is a map from the set of variables to . For a valuation and such that , we define by:
[TABLE]
For a valuation and a quantifier-free STP-formula , the relation is defined by induction on , as follows.
[TABLE]
We say a formula is satisfiable if for some . Without subformulas and , it is known that the satisfiability of quantifier-free formulas is decidable [47, 57, 36].
Proof of Theorem 3.10.
Since the satisfiability of word equations is decidable and in PSPACE [47, 57, 36], it suffices to show that atomic formulas of the form , , or can be encoded into formulas using only word equations of polynomial size. We can assume, without loss of generality, that the alphabet is finite: note that if is satisfiable for an infinite alphabet, then is also satisfiable for where is the set of letters occurring in and are distinct letters not occurring in , and vice versa. First, we encode the relation , which means “ is not a prefix of .” It can be expressed by , where are fresh variables. (This encoding of is standard; see, e.g. [18, 36].) We can then express as .
The encoding of is straightforward. Suppose . If , then can be replaced with (which can be expressed as ). If , then is expressed as , where are obtained from by -renaming, so that the variables in are fresh.
Now we consider , where . If , then it can be replaced with (which can be expressed as ). Thus, we assume . Since is solvable, there exists a reduction sequence . We encode the formula by induction on the length of the reduction sequence. If , then . Thus, can be replaced with . If , then . We perform case analysis on the rule used for deriving . Since the other cases are similar, we discuss only the cases for PR-Prefix and PR-Epsilon.
- •
Case PR-Prefix: In this case, there exist such that with and for all . Thus, can be replaced with , where is a fresh variable, , and for all . By the induction hypothesis, can also be encoded into word equations.
- •
Case PR-Epsilon: In this case, there exists such that and . Thus, can be replaced with . By the induction hypothesis, can also be encoded into word equations.
The size of the resulting formula is polynomial in the size of the original formula, as the length of the reduction sequence is linear in and the increase of the formula size in each step of the encoding above is polynomial in the size of . ∎
Remark A.2**.**
The encoding of above for the inductive case is actually based on a special case of Lemma A.4 where is a constant pattern . By Lemma A.4, if and only if is undefined or . The (un)definedness of can be expressed in terms of the prefix/suffix relations, which can further be expressed by word equations, as discussed above.
A.2 Additional Definitions and Proofs for Section 4
A.2.1 The Extension in Section 4.1
First, we extend (used in Lemma A.6) to the least equivalence relation closed under not only the permutations and but also the rule , and slightly relax the requirement for solvability: a tuple pattern is solvable if for some mutually distinct variables . Thus, is also solvable, as . Without the reverse pattern constructor, the definition of solvability is the same.
All the main properties are preserved by the extension of patterns with the reverse constructor. This can be intuitively understood by noting that the rules R-RPrefix and R-RSuffix can be emulated by R-Prefix and R-Suffix, if we augment the data by adding, for each column of , a new column consisting of the reverse of elements of . For example,
[TABLE]
can be emulated by:
[TABLE]
It should be obvious that the extended pattern (consisting of variables ) is inferable if and only if is inferable from the augmented data, where and .
A little more formally, we can confirm that the main properties listed in Table 3, by checking that all the lemmas in the table remain to hold (modulo a minor adjustment due to the extension of solvability). The lemmas required for soundness and completeness (Theorem 2.1, Theorem 3.1 and Theorem 3.2) trivially hold. More care is necessary for minimality (Theorem 3.4). For Lemma A.4, we extend the definition of (Definition A.1) by the following cases:
- •
Case PR-RPrefix: In this case, and with and for some and for . If is of the form and , then where for . Otherwise, is undefined.
- •
Case PR-RSuffix: In this case, and with and for some and for . If is of the form and , then where for . Otherwise, is undefined.
Then Lemma A.4 holds as required.
Lemma A.6 (weak confluence of up to ) also remains to hold. We discuss only one new case; the other cases are similar.
- •
Case and (i.e., the two reductions use PR-Prefix and PR-RPrefix respectively, and is principal in both reductions).
By , and are in the prefix relation. Let us consider the case where is a prefix of ; the other case is similar. In that case, we have:
[TABLE]
For the existence of characteristic data (Theorem 3.5), it suffices to strengthen the requirement for the codewords , by further requiring that for all , is neither a prefix nor a suffix of . Note that we can still choose such codewords such that . (For example, for the codewords of the same length that satisfy the original conditions, let .) Then, we have a slightly weakened version of Lemma A.15, where “ for every ” is replaced with “ is or for every ”, which is sufficient for proving Theorem 3.5.
The lemmas for learnability in Table 3 remain to hold, and therefore, Theorems 3.6 and 3.7 also remain to hold.
For Theorem 3.10 (the decidability of quantifier-free STP formulas), the set of word expressions are extended to , and the definition of is extended in an obvious manner. Then, Theorem 3.10 remains to hold, thanks to the decidability of word equations with involution [20, 19].
A.2.2 The Extensions with Multisets and Sets
We now discuss the extensions sketched in Section 4.2.
We first provide more precise definitions of multiset patterns. The sets of multiset tuple patterns (MTPs) and conjunctive multiset tuple patterns (CMTPs), ranged over by and respectively, are defined by:
[TABLE]
Patterns are identified up to permutations; e.g., (thus, a pattern may actually be viewed as a multiset consisting of elements of and ). A multiset tuple pattern is solvable if for some mutually distinct variables . A conjunctive multiset tuple pattern is solvable if is solvable for every . Solvable multiset tuple patterns and conjunctive multiset tuple patterns are abbreviated as SMTP and CSMTP respectively.
For a map from to the set of multisets over , and a pattern such that , we define by:
[TABLE]
where denotes the multiset union.
For an MTP and a CMTP , and are defined by:
[TABLE]
Among the properties listed in Table 3, the minimality property (Theorem 3.4) fails. For example, consider the data: . We can reduce in the following two ways:
[TABLE]
Thus, outputs or non-deterministically, but the latter is not minimal; in fact, .
The failure of the minimality is attributed to the failure of weak confluence of (Lemma A.6). In fact, the reductions and are not confluent, because .
Due to the failure of minimality, Theorem 3.5 (about characteristic data) and the first part of Theorem 3.6 (about the learnability of SMTPs) fail. However, the following weaker version of Theorem 3.5 (obtained by weakening the condition (iii)) holds.
Theorem A.19** (Characteristic Data (Weaker Version)).**
Let be an STP such that . Then, there exists such that (i) is polynomial in , (ii) for any such that , there exists such that , and (iii) for any such that , implies . Furthermore, given , can be constructed in polynomial time.
Proof Sketch.
For an SMTP , we construct the characteristic data as follows. Let , with . Let be the map such that and for every . Let be:
[TABLE]
For example, the characteristic data for above is
[TABLE]
Then, satisfies the conditions required in Theorem A.19. ∎
The class of SMTPs is still learnable if is modified so that it outputs a minimal STP such that . To do so, it suffices for to first compute the set , filter out non-minimal STPs by computing , and output an element of non-deterministically. Then Theorem 3.6 holds for the modified version of .
As for Theorem 3.9, the decidability remains to hold, but the complexity of deciding whether a given multiset tuple pattern is solvable may not belong to P, due to the failure of weak confluence of . The membership and inclusion problems can still be solved in polynomial time if we are given a witness for the solvability of (i.e., a reduction sequence ).
The other properties—soundness (Theorem 2.1), completeness (Theorems 3.2 and 3.3), learnability of CSTPs (the second part of Theorem 3.6 and Theorems 3.7 and 3.8), and the decidability of quantifier-free formulas (Theorem 3.10)—remain to hold. Indeed, we can confirm that the required lemmas listed in Table 3 remain to hold. In the proof of Theorem 3.8, the first line of the procedure :
[TABLE]
should be replaced with:
[TABLE]
to filter out non-minimal STPs.
The decidability of (the satisfiability of) quantifier-free formulas relies for the multiset-case relies on that of linear integer arithmetic, instead of word equations. First, let us fix the syntax of quantifier-free SMTP formulas:131313We can further add primitive constraints accommodated by [56].
Definition A.2**.**
The set of (quantifier-free) SMTP formulas, ranged over by , is defined by:
[TABLE]
Here, , where the empty sequence is interpreted as the empty multiset, and the concatenation is interpreted as the multiset union. denotes the size of the multiset (expressed by) .
The semantics of quantifier-free SMTP formulas is defined as follows. Let be a map from to the set of finite multisets over . We define (where we assume ) and by:
[TABLE]
We say that a quantifier-free SMTP formula is satisfiable if for some . The following is a multiset version of Theorem 3.10.
Theorem A.20**.**
Given a quantifier-free SMTP formula , one can effectively construct an equi-satisfiable SMTP formula that contains no subformulas of the form , or . Therefore, the satisfiability of quantifier-free SMTP formulas is decidable.
Proof.
It suffices to show encodings of and (by considering the negation normal form). Let and . If , then and can be replaced by and respectively. Suppose . Then, can be replaced by , where is obtained by -renaming of and all the variables in are fresh. can be encoded by induction on the sequence , in the same manner as the case for STPs. For example, if , then can be replaced by: .
By the decidability of multiset constraints [56], we can conclude that the satisfiability of quantifier-free SMTP formulas is decidable. ∎
Analogous results hold for the case of sets, where the conjunction is interpreted as the disjoint union. The decidability of quantifier-free SSTP formulas follows from the decidability of set constraints (e.g., see [43]).
A.3 Additional Definitions and Proofs for Section 5
A.3.1 Additional Details on Section 5.1
As defined in Section 5.1, a CHC over words is of the form , where is a predicate variable, is a quantifier-free STP-formula, and is of the form or . (Here, may be viewed as an STP formula .)
An interpretation for predicate variables is a function that maps each -ary predicate variable to a subset of . Let be an interpretation for predicates, and be a map from to . We write if and if (recall Section A.1.9 for the definition of the latter). Let be a CHC . We write if holds for every such that and for each . Let be a system of CHCs . We write , and call a model of if for every . A system of CHCs is satisfiable if there exists a model of .
A CSTP-interpretation for predicates is a map where ’s are CSTPs. A CSTP-interpretation is a CSTP-model of , written , if . By abuse of notation, we often just write for .
Lemma A.21**.**
Given a CSTP-interpretation and a system of CHCs, it is decidable whether is a CSTP-model of . Furthermore, there is an algorithm which, given and a finite set of definite clauses, outputs “” if , and otherwise outputs such that there exists a valuation and a clause in , with and for every , but .
Proof.
This follows immediately from Theorem 3.10. Note that is a CSTP-model of a CHC , if and only if is unsatisfiable, where denotes the formula . Thus, if does not hold, then is satisfiable for some definite clause . We can construct a model for the formula and return . ∎
To prove Theorem 5.1 for the case where CHCs have multiple predicates, we need to extend Theorem 3.7. Let be the set of interpretations for predicate variables.
Theorem A.22**.**
Let be a finite set of definite clauses consisting of predicates . Let be the algorithm of Lemma A.21. Then the procedure below eventually terminates and returns the least CSTP-model of .
Proof.
We first prove the termination of the procedure. Suppose that the procedure does not terminate. Let be the values of at the -th iteration of the loop. We have a strictly increasing infinite sequence . For every such that strictly increases infinitely often, by Lemma A.18, there exists such that for all . For every such that strictly increases only finitely often, let be the index such that for all . Let . Then, we have for all . But then that contradicts (which implies ) and .
By the assumption on , when the algorithm terminates at the -th step, is a model of . Suppose there exists another CSTP-model of . Then it follows by induction on that for every (by the same argument as in the proof of Theorem 3.7). ∎
We can now prove Theorem 5.1.
Proof of Theorem 5.1..
Let , where and respectively consist of definite and goal clauses. By Theorem A.22, we can compute the least CSTP-model of . Then, has a CSTP-model if and only if is also a CSTP-model of . (Note that “only if” direction holds since for any goal clause , and imply .) The latter is decidable by Theorem A.21. ∎
Theorem 5.2 is an immediate corollary of the following lemma, which is obtained as a straightforward generalization of Theorem 3.8.
Lemma A.23**.**
Let be a finite set of definite clauses consisting of predicates . Then there exists an algorithm that enumerates all the minimal STP-models of .
Proof.
Let be the procedure defined as below, and let be the predicate variables occurring in . Let be the algorithm of Lemma A.21. Then it suffices to call to obtain a superset of all the minimal STP-models of , and then filter out non-minimal models.
The correctness of the algorithm follows by the same argument as that of Theorem 3.8. ∎
Example A.1**.**
Let us apply the algorithm in the proof above to the example (cf. Example 5.2 and Remark 5.1). The computation of proceeds as follows.
is first set to and is picked. Suppose returns . 2. 2.
Then is recursively called, and is set to , and is picked. Now may return . 3. 3.
Then is recursively called, and is set to . Suppose is picked and is updated to (inside this recursive call). may return . 4. 4.
Now, is recursively called, and is set to , and is picked. Now returns . So, the algorithm outputs and returns to the middle of Step 3 above. 5. 5.
From , is picked. Since returns , the algorithm outputs . Now becomes empty in chain of recursive calls, and the algorithm terminates.
Above, we have obtained as models of . By filtering out the non-minimal model , we obtain as the set of minimal models of . Since is also a model of , we can conclude that is satisfiable. ∎
A.3.2 Additional Details on Section 5.3
A CHC over multisets (CHC over sets, resp.) is of the form , where is a predicate variable, is a quantifier-free SMTP-formula (SSTP-formula) as defined in Definition A.2, and is of the form or .
The semantics and satisfiability of CHCs over multisets (sets, resp.) is defined in the same manner as those of CHCs over words, except that maps each variable to a multiset (a set, resp.) over and maps each -ary predicate to a -ary relation on multisets (sets, resp.) over . Theorems 5.4 and 5.5 follow by the same argument as Theorems 5.1 and Theorems 5.2.
Example A.2**.**
Recall the following CHCs over multisets.
[TABLE]
We can compute the least CMTP-model for the definite clauses (i.e., the above CHCs except the last one) as follows. We write for the multiset version of , and disable the rule R-CSubset for simplicity.
We first set:
[TABLE]
By calling , we may obtain . As , we now have:
[TABLE]
By calling , we may obtain . We now have:
[TABLE]
By calling , we may get and:
[TABLE]
By calling , we may get . We now have:
[TABLE]
At this point, returns . Thus, we have obtained the least CSMTP-model . Since is a model of the goal clause , we can conclude that is satisfiable. ∎
Appendix B Verification of Functional Queues Using Piecewise Conjunctive Solvable Tuple Patterns
We have considered conjunctive STPs, but not arbitrary Boolean combinations of STPs. While inferring arbitrary Boolean combinations seems infeasible, we can allow a restricted form of them called piecewise CSTPs. Let us fix a finite set of predicates of the form where is a (quantifier-free) STP-formula such that . We call the arity of the predicate , and write for it. We sometimes omit “” when it is clear from context. A (-ary) piecewise CSTPs over is an expression of the form
[TABLE]
where are -ary predicates, and are -ary CSTPs. The language represented by a -ary piecewise CSTPs is defined by:
[TABLE]
Here, for , denotes . For example, if where and . then is a piecewise CSTP. It represents the set of triples of the form or where .
Typically, the set of predicates would be . CSTPs can be considered a special case of piecewise CSTPs where .
Theorem 5.1 can be extended for piecewise CSTPs.
Theorem B.1**.**
Given a finite set of predicates as defined above and a system of CHCs on words, it is decidable whether has a piecewise CSTP-model over .
Proof.
This follows from the fact that has a piecewise CSTP-model if and only if obtained from by replacing each -ary predicate with has a CSTP-model. Here, ’s are fresh predicates and is the set of -ary predicates in . ∎
Below we apply the result above to the verification of functional queues.
Example B.1**.**
Let us consider the following OCaml program.
let initq = ([], []) let rec reva l1 l2 = match l1 with [] -> l2 | x::l1’ -> reva l1’ (x::l2) let enq x (l1,l2) = (l1, x::l2) let deq (l1,l2) = match l1 with [] -> (match reva l2 [] with [] -> ([], l1, l2) | x::l -> ([x], l, []) ) | x::l1’ -> ([x], l1’, l2) let rec enqall l (l1,l2) = match l with [] -> (l1,l2) | x::l’ -> enqall l’ (enq x (l1,l2)) let rec deqall (l1,l2) = match deq(l1,l2) with ([], _, _) -> [] | (l, l1’,l2’) -> l@(deqall (l1’, l2’)) let main l = assert(deqall (enqall l initq) = l)
Here, a queue is implemented as a pair of lists where is the sequence of elements in the queue, so that the amortized cost of each enqueue or dequeue operation is [54]. The dequeue function deq either returns (when the queue is empty, i.e., ) or a singleton set consisting of the first element of the queue, along with the updated queue. If , then the first element of the queue is computed by extracting the first element of the reverse of . Given a list of elements as input, the main function enqueues all the elements of , dequeues all the elements from the queue, and then asserts that the result equals .
The correctness of the above program (i.e., the lack of assertion failures) is reduced to the satisfiability problem for the following CHCs.
[TABLE]
Here, each predicate represents the relation between inputs and outputs of the corresponding function. For example, means that may return . The clauses for (which are found in Section 5.1) have been omitted.
The system of CHCs above has the following piecewise CSTP-model:
[TABLE]
Thus, if we set to where:
[TABLE]
then we can automatically prove the satisfiability of the CHCs above. We expect that necessary predicates in can typically be mined from the source program; in fact, in the above case, the function deq performs case analysis on whether and are empty lists. A general method to find an appropriate set of predicates is left for future work.∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1]
- 2Aho [1968] Alfred V. Aho. 1968. Indexed Grammars—An Extension of Context-Free Grammars. J. ACM 15, 4 (Oct. 1968), 647–671. https://doi.org/10.1145/321479.321488 · doi ↗
- 3Angluin [1980 a] Dana Angluin. 1980 a. Finding patterns common to a set of strings. J. Comput. System Sci. 21, 1 (1980), 46–62. https://doi.org/10.1016/0022-0000(80)90041-0 · doi ↗
- 4Angluin [1980 b] Dana Angluin. 1980 b. Inductive inference of formal languages from positive data. Information and Control 45, 2 (1980), 117–135. https://doi.org/10.1016/S 0019-9958(80)90285-5 · doi ↗
- 5Angluin [1982] Dana Angluin. 1982. Inference of Reversible Languages. J. ACM 29, 3 (July 1982), 741–765. https://doi.org/10.1145/322326.322334 · doi ↗
- 6Asada et al . [2017] Kazuyuki Asada, Ryosuke Sato, and Naoki Kobayashi. 2017. Verifying relational properties of functional programs by first-order refinement. Sci. Comput. Program. 137 (2017), 2–62. https://doi.org/10.1016/j.scico.2016.02.007 · doi ↗
- 7Barbosa et al . [2022] Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc 5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferenc · doi ↗
- 8Bjørner et al . [2015] Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. Mc Millan, and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (LNCS, Vol. 9300) . Springer, 24–51. https://doi.org/10.1007/978-3-319-23534-9_2 · doi ↗