Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent

Abstract

In program verification, measures for proving the termination of programs are typically constructed using (notions of size for) the data manipulated by the program. Such data are often described by means of logical formulas. For example, the cyclic proof technique makes use of semantic approximations of inductively defined predicates to construct Fermat-style infinite descent arguments. However, logical formulas must often incorporate explicit size information (e.g. a list length parameter) in order to support inter-procedural analysis.

In this paper, we show that information relating the sizes of inductively defined data can be automatically extracted from cyclic proofs of logical entailments. We characterise this information in terms of a graph-theoretic condition on proofs, and show that this condition can be encoded as a containment between weighted automata. We also show that under certain conditions this containment falls within known decidability results. Our results can be viewed as a form of realizability for cyclic proof theory.

1 Introduction

In program verification, it is well known that proving termination of a particular program depends on identifying a well-founded measure that decreases monotonically during the program’s execution. Thus, since the measure cannot decrease infinitely often, no execution of the program can be infinite. In practice, termination measures are typically derived from the data manipulated by the program itself (cf. size-change termination [14]), and in particular from notions of the size of its data structures.

For example, consider the following code, which “shuffles” a linked list with head pointer ${\mathtt {x}}$, using an auxiliary list reversal procedure ${\mathtt {rev}}$:

where the syntax $\texttt {[x]}$ denotes pointer dereferencing. The termination of the ${\texttt {shuffle(x)}}$ procedure can be deduced by taking as termination measure the length of the list from ${\mathtt {x}}$. The call to ${\mathtt {rev}}$ and the recursive call to ${\mathtt {shuffle}}$ both take place on the pointer ${\mathtt {y}}$ to the tail of the list. However, we also crucially rely upon the fact that the reversal procedure ${\mathtt {rev}}$ does not increase the size of the list. In a Hoare-style verification, this information is needed when we employ the sequential composition rule:

Here, the information that ${\mathtt {rev}}$ maintains the size of the list must be reflected in the relationship between its pre- and postconditions P and Q (which are logical formulas). Typically, this must be done by endowing these formulas with explicit size information; e.g., we could write an inductive predicate $\mathsf {list}(y,n)$ representing linked lists in memory, with an explicit length parameter (cf. [3]).

In this paper, we show that this kind of information, relating the sizes of inductively defined data, can often be extracted automatically from cyclic proofs of logical entailments. Cyclic proofs can be seen as formalising proof by regular infinite descent [7]; they are derivation trees with “backlinks” from (some) leaves to interior nodes, subject to a global soundness condition ensuring that all infinite paths correspond to sound infinite descent arguments. Cyclic proof systems have been developed for a wide variety of settings ranging from pure logic [4, 5] to Hoare-style logics for program termination [6, 17] and other temporal properties [9]; the common denominator is the presence of logical data defined using fixed points. The soundness of cyclic proofs relies on infinite descent over the semantic approximations of these fixed points, which can be seen as capturing a notion of size for the corresponding data. Suitable entailments for which to construct these cyclic proofs may be formulated by procedures for verifying the correctness of (fragments of) programs. For example, a procedure to verify the Hoare triple $\{\mathsf {list}(y)\}\ \texttt {rev(y)}\ \{\mathsf {list}(y)\}$ might result in the entailment $y \mapsto x *\mathsf {list}(x) \vdash \mathsf {list}(y)$ of separation logic [11, 16]. Such entailments are commonly referred to as verification conditions, since they must be discharged independently.

Relationships between the sizes of inductive data are reflected by inclusions between the approximations of the fixed point semantics. To infer these inclusions, we formulate a novel condition on the structure of cyclic entailment proofs (Definition 8) which is sufficient to extract this information (Theorem 2). This condition is equivalent to an inclusion between weighted automata that can be constructed from the cyclic proofs (Theorem 3), and, when the cyclic proof is suitably structurally well-behaved, this inclusion becomes decidable (Theorem 4). For simplicity, we present our results for the well-known cyclic proof system $\text {CLKID}^\omega$ for first order logic with inductive definitions [4, 7]. However, we stress that our results are not limited to this setting: in a separate technical report we formulate and prove our results for a general, abstract notion of cyclic proof [18]. Consequently our results also hold, e.g. for separation logic with inductive predicates [5, 6], and so can be deployed in our cyclic proof framework for proving program termination based on this logic [17].

The remainder of this paper is structured as follows. First, Sect. 2 gives an introductory example motivating our new structural condition for extracting size relationships from cyclic proofs. Section 3 then reprises the basics of first-order logic with inductive predicates and its cyclic proof system $\text {CLKID}^\omega$ from [4, 7]. In Sect. 4 we formulate our structural condition on cyclic proofs and prove its soundness. In Sect. 5 we show how this condition can be encoded as an inclusion between weighted automata and formulate further graph-theoretic conditions on cyclic proofs under which this is decidable. Section 6 concludes.

For space reasons, we elide the detailed proofs of the results in this paper, but they can be found in our longer technical report [18].

2 Motivating Example

Figure 1 gives inductive definitions of predicates ${\text {N}}$, ${\text {E}}$ and ${\text {O}}$ (intended to capture the properties of being a natural number, even number and odd number respectively) and a cyclic proof of the sequent ${\text {E}}{x} \vdash {\text {N}}{x}$. Note that ${\text {E}}$ and ${\text {O}}$ are mutually defined. The (${\text {N}}\text {R}_i$) rules indicate a right-unfolding of the ${\text {N}}$ predicate, and the (Case ${\text {E}}$) and (Case ${\text {O}}$) rules a left unfolding (or case analysis) on the predicates ${\text {E}}$ and ${\text {O}}$ respectively. This cyclic proof is sound since its only infinite path contains an infinite, unbroken “trace” of the ${\text {E}}$ and ${\text {O}}$ predicates in the antecedent of each sequent that “progresses” infinitely often as these predicates are unfolded.

Fig. 1.

Inductive definitions of ${\text {N}}$, ${\text {E}}$, and ${\text {O}}$, and cyclic proof of ${\text {E}}{x} \vdash {\text {N}}{x}$.

This condition ensures that the proof is valid because it can be related to approximations of the semantics $[\![{\cdot }]\!]$ of the predicates, which form an ordinal-indexed chain $[\![{\cdot }]\!]_{0} \le [\![{\cdot }]\!]_{1} \le \ldots \le [\![{\cdot }]\!]_{\alpha } \le \ldots \le [\![{\cdot }]\!]$. If ${\text {E}}{x} \vdash {\text {N}}{x}$ is invalid then, by local soundness of the rules, so is every sequent on the infinite path in the proof. The trace along this path then corresponds to a non-increasing subsequence of the ordinals in this chain, which strictly decreases when the trace progresses. Since the trace progresses infinitely often, we obtain an infinitely decreasing chain of ordinals, which is a contradiction.

Interestingly, it turns out that, by examining the structure of this cyclic proof more closely and also considering the (right) unfoldings of ${\text {N}}$, we can deduce that the $\alpha$ ^th approximation of ${\text {E}}$ is also included in the $\alpha$ ^th approximation of ${\text {N}}$, i.e., $[\![{{\text {E}}{x}}]\!]_{\alpha } \subseteq [\![{{\text {N}}{x}}]\!]_{\alpha }$. Intuitively, this is because on every maximally finite path in the proof along which ${\text {N}}$ is unfolded, the mutually defined ${\text {E}}$ and ${\text {O}}$ are together unfolded at least as often as ${\text {N}}$. Thus when x is included in some approximation of ${\text {E}}$, it is already included in the corresponding approximation of ${\text {N}}$. Later, in Sect. 4, we will formalise this intuition as an additional syntactic, trace-based condition on cyclic proofs. The upshot is that we may form “traces”, as described above, between instances of ${\text {E}}{t}$ and ${\text {N}}{t}$ (for any term t) in the antecedent of sequents, even though they are not related by their inductive definitions.

3 Cyclic Proofs for First Order Logic

In this section we summarise a variant of $\text {CLKID}^\omega$, a cyclic proof system for first order logic with inductive predicates [4, 7].

3.1 First Order Logic with Inductive Definitions

We assume the standard syntax and semantics of first order logic. For simplicity, we take models to be valuations of term variables to objects in the semantic domain. A sequent $\varGamma \vdash \varDelta$ comprises two sequences of formulas: an antecedent $\varGamma$ and a consequent $\varDelta$. For a sequent $S = \varGamma \vdash \varDelta$, we write $m\,{\models }\,S$ to mean that the model m satisfies at least one formula in $\varDelta$ whenever it satisfies all fomulas in $\varGamma$. Conversely, we write $m\,{\not \models }\,S$ to mean that m satisfies all fomulas in $\varGamma$ and no formula in $\varDelta$. A sequent S is valid when $m\,{\models }\,S$ for all models m.

We give the semantics of predicate symbols in the signature by means of sets of inductive productions, in the style of Martin-Löf [15].

Definition 1

(Inductive Definition Set). An inductive definition set $\varPhi$ is a finite set of productions, each of the form ${\text {P}}_{1}{\varvec{t_{1}}}, \ldots , {\text {P}}_{j}{\varvec{t_{j}}} \Rightarrow {\text {P}}_{0}{\varvec{t_{0}}}$, consisting of a finite set of predicate formulas called premises and a predicate formula called the conclusion. We say that ${\text {P}}_{1}{\varvec{t_{1}}}, \ldots , {\text {P}}_{j}{\varvec{t_{j}}} \Rightarrow {\text {P}}_{0}{\varvec{t_{0}}}$ is a production for ${\text {P}}_{0}$.

Predicate interpretations X are functions from predicate formulas to sets of models. We write $[\![{{\text {P}}{\varvec{t}}}]\!]_{X}$ to denote $X({\text {P}}{\varvec{t}})$. An inductive definition set $\varPhi$ induces a characteristic operator $\varphi _{\varPhi }$ on predicate interpretations, which applies (substitution instances of) the productions in $\varPhi$, as follows (where $\theta$ is a substition of terms for variables):

$$\begin{aligned} \varphi _{\varPhi } (X)({\text {P}}{{\varvec{t}}}\,\theta ) = \{ m&\left| \,{{\text {P}}_{1} {{\varvec{t}}}_\mathbf{1} , \ldots ,{\text {P}}_{ j} {{\varvec{t}}}_{{\varvec{j}}} \Rightarrow {\text {P}}\,{{\varvec{t}}}\,\in \varPhi } \right. \\&\quad \quad \quad \quad {\text {and}}\,\,m\, \,\in \left[ \left[ {{\text {P}}_{i}{{\varvec{t}}}_{{\varvec{i}}} \theta } \right] \right] _{X} \,{\text {for}}\,{\text {all}}\,i\, \in \{ 1, \ldots ,j\} \} \\ \end{aligned}$$

We define a partial ordering $\le$ on the set of predicate interpretations $\mathcal {I}$ by $X \le X' \Leftrightarrow \forall F .\ X(F) \subseteq X'(F)$. One can note that $(\mathcal {I}, \le )$ is a complete lattice and the least element, denoted by $X_{\bot }$, maps all predicate formulas to the empty set. Moreover, characteristic operators are monotone with respect to $\le$, thus admitting the following (standard) construction that builds a canonical interpretation via a process of approximation [1, 7]:

Definition 2

(Interpretation of Inductive Definitions). We interpret an inductive definition set $\varPhi$ as the least prefixed point of its characteristic operator, $\mu X . \varphi _{\varPhi }(X)$. This least prefixed point, denoted by $[\![{\cdot }]\!]^{\varPhi }$, can be approached iteratively being the supremum of the (ordinal-indexed) chain $X_{\bot } \le \varphi _{\varPhi }(X_{\bot }) \le \varphi _{\varPhi }(\varphi _{\varPhi }(X_{\bot })) \le \ldots \le \varphi _{\varPhi }^{\alpha }(X_{\bot }) \le \ldots$; each $\varphi _{\varPhi }^{\alpha }(X_{\bot })$ is an approximation of $[\![{\cdot }]\!]^{\varPhi }$ and is denoted by $[\![{\cdot }]\!]^{\varPhi }_{\alpha }$. When the specific inductive rule set is not of immediate relevance we leave it implicit, writing $[\![{\cdot }]\!]$ and $[\![{\cdot }]\!]_{\alpha }$.

3.2 The Cyclic Proof System

The proof system is essentially Gentzen’s sequent calculus, LK, in which derivations are permitted to contain cycles. To the standard proof rules of LK with equality and substitution we add introduction rules for the inductive predicate symbols, derived from their productions. Each predicate ${\text {P}}$ has a single left introduction rule, (Case ${\text {P}}$), which performs a case split over the full set of productions for ${\text {P}}$, and every i ^th production for ${\text {P}}$ induces a distinct right introduction rule (${\text {P}}\text {R}_{i}$). Furthermore, we remove the right introduction rules for implication and negation since they invalidate the soundness of our realizability condition (specifically, not all instances of these rules satisfy Property 1, in Sect. 4 below). Although this system is actually quite weak, we believe these particular rules do not play a crucial role in deriving entailments between inductive predicates in general. Note we do not need them in our examples.

We view a cyclic derivation (or pre-proof) as a directed graph; each sequent is a node of the graph, and edges go from conclusion to premise. To track sequences of decreasing approximations, we use the notion of a trace in a pre-proof $\mathcal {P}$.

Definition 3

(Traces).

• (i) A trace value is a predicate formula (e.g. ${\text {E}}{x}$).

• (ii) A left-hand (resp. right-hand) trace is a possibly infinite sequence $\mathbf {\tau }$ of trace values in which those of each successive pair, $(\tau _{i}, \tau _{i+1})$, occur in the antecedents (resp. consequents) of successive nodes in $\mathcal {P}$, and either:

  • (a) $\tau _{i} = \tau _{i+1}$;

  • (b) $\tau _{i}$ and $\tau _{i+1}$ occur as part of the conclusion and premise of a substitution rule and $\tau _{i}$ is the result of applying the rule’s substitution to $\tau _{i+1}$; or

  • (c) $\tau _{i}$ and $\tau _{i+1}$ occur as part of the conclusion and premise of a (Case ${\text {P}}$) or (${\text {P}}\text {R}_{i}$) rule, with $\tau _{i}$ of the form ${\text {P}}{\varvec{t}}$ and $\tau _{i+1}$ derived from the body of the production for ${\text {P}}$ associated with the premise of the rule (i.e. $\tau _{i+1}$ is derived from the unfolding of $\tau _{i}$).

  We call each pair $(\tau _{i}, \tau _{i+1})$ a trace pair. In the case that (c) holds, we say the trace progresses at point i and call $(\tau _{i}, \tau _{i+1})$ a progressing trace pair.

• (iii) For finite traces $\mathbf {\tau }$, we write ${\mid {\mathbf {\tau }}\mid }$ for the length of the trace and denote by $\mathsf {prog}(\mathbf {\tau })$ the number of progression points in $\mathbf {\tau }$, which we call the sum of $\mathbf {\tau }$.

• (iv) For an inference rule $r = \langle S_0, (S_1, \ldots , S_n) \rangle$ with trace values $\tau$ and $\tau '$ occurring in the conclusion $S_0$ and j ^th premise $S_{j}$, respectively, we write $\delta ^{\mathcal {A}}_{(r, j)}(\tau , \tau ')$ (resp. $\delta ^{\mathcal {C}}_{(r, j)}(\tau , \tau ')$) if $(\tau , \tau ')$ forms a left-hand (resp. right-hand) trace. We call $\delta$ the trace pair relation.

When the meaning is clear from the context, we may sometimes simply write $\delta _{r}(\tau , \tau ')$. In an abuse of notation we write $\delta _{r}(\tau , \tau ') = 1$ to indicate that $(\tau , \tau ')$ is a progressing trace pair, and $\delta _{r}(\tau , \tau ') = 0$ otherwise. When $\tau$ occurs in the conclusion of rule r, but there are no j and $\tau '$ such that $\delta _{(r, j)}(\tau , \tau ')$ is defined, then we say $\tau$ is terminal for r.

Example 1

In Fig. 2 we show a cyclic proof of ${\text {N}}{x} \vdash {\text {E}}{x}, {\text {O}}{x}$, i.e. that every natural number is either even or odd. Each ${\text {N}}{t}$ in an antecedent is related to the ${\text {N}}{t'}$ in its premise(s); the trace pair relation for the consequent trace values is more complex, and we indicate it visually using under- and overlines.

Fig. 2.

A cyclic proof of the entailment ${\text {N}}{x} \vdash {\text {E}}{x}, {\text {O}}{x}$; each node is numbered uniquely, and the consequent trace pairs are indicated using under- and overlines.

A pre-proof is valid if it satisfies the following condition on traces.

Definition 4

(Global Soundness). A pre-proof is globally sound when every infinite path has some tail that is followed by a left-hand trace which progresses infinitely often; when this holds we say that it is a (cyclic) proof.

The global soundness of a pre-proof can be checked using Büchi automata.

Proposition 1

([7, Proposition 7.4]). It is decidable if a pre-proof is globally sound.

Example 2

The pre-proof in Fig. 1 has only one infinite path (along the cycle), and there is a left-hand trace along this path formed by the alternating occurrences of the ${\text {E}}$ and ${\text {O}}$ predicates in the antecedent of each sequent. This progresses at two points around each cycle on traversing the (Case) rules and therefore the pre-proof is globally sound. A similar argument shows the pre-proof in Fig. 2 is also globally sound: the (unique) infinite left-hand trace progresses once each time around the loop.

We may think of models as realizers of trace values. We define a trace realization function to specify which models realize trace values and how quickly they realize them.

Definition 5

(Trace Realization Function). The trace realization function $\varTheta$ maps models to the least approximations of trace values in which they appear:

$$\begin{aligned} \varTheta (\tau , m) \overset{def}{=} \mathsf {min} \left( \{ \alpha \,\mid \, m \in [\![{\tau }]\!]_{\alpha } \} \right) \end{aligned}$$

The value assigned by $\varTheta$ corresponds to the ordinal position of this approximation in the chain constructed in Definition 2. Notice that a model may not necessarily satisfy a given predicate formula, so $\varTheta$ is partial and we write $\varTheta (\tau , m){\downarrow }$ to indicate that $\varTheta$ is defined on $(\tau , m)$.

The global soundness condition ensures the validity of cyclic proofs because the trace realization function enables us to relate traces to descending chains of approximations. If a cyclic proof were to contain invalid sequents then the trace realization function could be used to derive an infinite descending chain of ordinals and hence a contradiction.

Theorem 1

([7, Proposition 5.8]). If $\varGamma \vdash \varDelta$ has a cyclic proof then it is valid.

4 Extracting Semantic Inclusions from Cyclic Proofs

We are aiming to deduce inclusions between the semantic approximations of predicates (viz. trace values), e.g. that whenever there is a model $m \in [\![{{\text {E}}{x}}]\!]_{\alpha }$ then also $m \in [\![{{\text {N}}{x}}]\!]_{\alpha }$ (cf. Fig. 1). We can express this using the trace realization function as $\varTheta ({\text {N}}{x}, m) \le \varTheta ({\text {E}}{x}, m)$, since predicate approximations increase monotonically. We will deduce such relationships from sequents $\varGamma [\tau ] \vdash \varDelta [\tau ']$ in cyclic proofs (where $\varGamma [\tau ]$ indicates that the trace value $\tau$ occurs in $\varGamma$), and so in general we deduce such orderings within a context, $\varGamma$. Thus we will write $\varGamma : \tau ' \le \tau$ to mean:

$$\begin{aligned} \hbox {for all models { m}, if } m\,{\models }\,\varGamma \hbox { and } \varTheta (\tau ', m){\downarrow } \hbox { then } \varTheta (\tau ', m) \le \varTheta (\tau , m), \end{aligned}$$

where $m\,{\models }\,\varGamma$ denotes that m satisfies all the formulas in $\varGamma$. We formulate an additional trace condition for cyclic proofs (Definition 8, below) and show that the existence of a proof satisfying this extra condition is sufficient to guarantee this ordering. We say that such a proof realizes the ordering, and so refer to the new trace condition as the realizability condition.

This realizability condition will express that for every right-hand trace of a certain kind, we can find a left-hand trace which ‘matches’ it in a sense that we will make precise below. We specify the kinds of right-hand traces of interest using the following concepts.

Definition 6

(Maximal Right-Hand Traces). A finite right-hand trace $\mathbf {\tau }$ (${\mid {\mathbf {\tau }}\mid } = n$) following a path in a cyclic proof is called maximal when it cannot be extended any further, i.e. there is no trace value $\tau '$ and premise of the final node in the trace for which $\delta _{r}(\mathbf {\tau }_n, \tau ')$ is defined (where r is the rule used to derive the final node). If the final node in the trace is derived using an axiom, then we say the trace is partially maximal; otherwise it is called fully maximal.

Fully maximal traces are ones whose final trace value is introduced by an inference rule, e.g. weakening, as in node (6) of the proof in Fig. 2.

Definition 7

(Groundedness and Polarity). We call a trace value derivable using a base production (i.e. a production without premises) ground, e.g. ${\text {N}}{0}$ or ${\text {E}}{0}$. A grounded trace is one whose final trace value is ground. When the antecedent of a sequent contains the negation of a ground predicate instance, we say that it is negative. A positive sequent is one with no such negated predicate. A negative (resp. positive) trace is one whose final sequent is negative (resp. positive).

For example, in Fig. 2 the right-hand trace $(1, {\text {E}}{x})$, $(2, {\text {E}}{x})$, $(4, {\text {E}}{0})$, $(5, {\text {E}}{0})$ is grounded, but $(1, {\text {O}}{x})$, $(2, {\text {O}}{x})$, $(4, {\text {O}}{0})$, $(6, {\text {O}}{0})$ is not. Moreover, the latter trace is negative. Note that, by definition, all models m must satisfy ground predicate instances $\tau$ and $\varTheta (\tau , m) = 1$. Thus no models may satisfy the antecedent of a negative sequent. This means that we can exclude negative traces when considering the realizability of trace value orderings. We can now formulate the realizability condition itself.

Definition 8

(The Realizability Condition). We write $\mathcal {P}: \tau \le \varGamma [\tau ']$ when $\mathcal {P}$ is a cyclic proof containing a node $\varGamma [\tau '] \vdash \varDelta [\tau ]$ satisfying the following: for every positive maximal right-hand trace $\mathbf {\tau }$ starting at $\tau$, there exists a left-hand trace $\mathbf {\tau '}$ starting with $\tau '$ and following some prefix of the same path in the proof such that:

• 1. $\mathsf {prog}(\mathbf {\tau }) \le \mathsf {prog}(\mathbf {\tau '})$ and

• 2. either a) $\mathbf {\tau }$ is grounded; or b) $\mathbf {\tau }$ is partially maximal, ${\mid {\mathbf {\tau '}}\mid } = {\mid {\mathbf {\tau }}\mid }$, and the final trace values in $\mathbf {\tau }$ and $\mathbf {\tau '}$ match.

Consider the proof $\mathcal {P}_1$ in Fig. 2.

Example 3

( $\mathcal {P}_1 : {\text {E}}{x} \le {\text {N}}{x}$ ). The right-hand trace from ${\text {E}}{x}$ following the path (1) (2) (4) (5) is positive, maximal and grounded. The left-hand trace (1) follows this path and the sum of both traces is 0. The next longest maximal right-hand trace traverses the cycle once, following the path (1) (3) (9) ...(12) (1) (2) (4) (6) along the right-hand side of the (Cut) rule. However, this trace is negative and so we need not consider it. The other positive maximal traces are obtained by following the cycle an even number of times before ending at node (5); the progression points occur at (${\text {E}}\text {R}_2$) on the odd-numbered traversals and (${\text {O}}\text {R}_2$) on the even-numbered ones, which is matched by progressions in the corresponding left-hand trace at the (Case) rule. These traces also suffice to demonstrate that $\mathcal {P}_1 : {\text {O}}{x} \le {\text {N}}{x}$ holds.

Notice that we can obtain a globally sound cyclic proof of ${\text {N}}{x} \vdash {\text {E}}{x}, {\text {O}}{x}$ without using (Cut), by immediately closing node (4) with (${\text {E}}\text {R}_1$). In this case the now (partially) maximal right-hand trace from ${\text {O}}{x}$ in node (1) to ${\text {O}}{0}$ in node (4) is positive and so would have to be considered. Unfortunately this trace is not grounded, nor does there exist a matching left-hand trace of equal length ending with ${\text {O}}{0}$, and so this simpler (and arguably more natural) proof does not satisfy the realizability condition.

It may seem odd that we cannot use the simpler proof to realize the ordering. We must discount the right-hand traces ending with ${\text {O}}{0}$ since they have no models; yet it is not possible in general to determine syntactically when predicate instances do not have models. Our approximation, using negative traces, works at the level of entire sequents and thus the traces ending with ${\text {E}}{0}$ (which we do consider) must be separated from those ending in ${\text {O}}{0}$ (which we must not). This highlights the syntactic nature of our results.

Now consider the proof $\mathcal {P}_2$ of ${\text {E}}{x} \vdash {\text {N}}{x}$ in Fig. 3, which is a modified version of the proof in Fig. 1 that accommodates an additional production for ${\text {O}}$.

Example 4

( $\mathcal {P}_2 : {\text {N}}{x} \le {\text {E}}{x}$ ). The right-hand trace following (1) (2) (4) is maximal, positive and grounded and the left-hand trace $(1, {\text {E}}{x})$ follows (a prefix of) the same path; the sum of both of these traces is 0. Similarly, the positive right-hand trace following (1) (3) (5) (6) (7) (9) (10) is not grounded, but is partially maximal and there is a left-hand trace of equal length following this same path with a matching final trace value. The sum of both traces in this case is 2: the right-hand trace progresses once at each instance of the (${\text {N}}\text {R}_2$) rule; the left-hand one at the (Case) rules. Other maximal right-hand traces are obtained by prefixing the cycle $(1)\ldots (12)$ to the two already considered; notice the left-hand trace following the cycle progresses an equal number of times.

Fig. 3.

A cyclic proof of the entailment ${\text {E}}{x} \vdash {\text {N}}{x}$, accommodating the extra production ${\text {N}}{\mathsf {s}{\mathsf {s}{0}}} \Rightarrow {\text {O}}{\mathsf {s}{\mathsf {s}{\mathsf {s}{0}}}}$ for ${\text {O}}$.

Soundness of Realizability. To show that the realizability condition is sufficient to realize trace value orderings, we extend the concept that models realize trace values and use sequences of models to realize traces. We say that a sequence of models $\varvec{m}$ realizes a left-hand trace $\mathbf {\tau }$ when for every sequent $\varGamma _{i}[\tau _{i}] \vdash \varDelta _{i}$ in the corresponding path we have that $m_{i}\,{\models }\,\varGamma _{i}$ and $\varTheta (\tau _{i+1}, m_{i+1}) + \delta (\tau _{i}, \tau _{i+1}) \le \varTheta (\tau _{i}, m_{i})$. Dually, $\varvec{m}$ realizes a right-hand trace $\mathbf {\tau }$ when $m_{i}\,{\models }\,\varDelta _{i}$ and $\varTheta (\tau _{i+1}, m_{i+1}) + \delta (\tau _{i}, \tau _{i+1}) \ge \varTheta (\tau _{i}, m_{i})$ for every sequent $\varGamma _{i} \vdash \varDelta _{i}[\tau _{i}]$ in the path. Trace realizers guarantee the following.

Lemma 1

If $\varvec{m}$ realizes a trace $\mathbf {\tau }$ of length n then $\varTheta (\tau _{n}, m_{n}) + \mathsf {prog}(\mathbf {\tau }) \le \varTheta (\tau _{1}, m_{1})$ holds if $\mathbf {\tau }$ is a left-hand trace, and $\varTheta (\tau _{n}, m_{n}) + \mathsf {prog}(\mathbf {\tau }) \ge \varTheta (\tau _{1}, m_{1})$ if $\mathbf {\tau }$ is a right-hand trace.

We say a rule instance is valid when its conclusion and premises are all valid sequents.¹ We note the following property of the trace realization function.

Property 1

(Descending Model Property). For all valid, non-axiomatic rule instances $r = \langle \varGamma [\tau ] \vdash \varDelta [\tau '], (S_1, \ldots , S_n) \rangle$ and models $m\,{\models }\,\varGamma$, there exists some $S_j = \varSigma \vdash \Pi$ and a model $m' \models \varSigma$ such that: either $\tau '$ is terminal for r, or there exists $\tau ''$ with $\delta _{(r, j)}(\tau ', \tau '')$ defined; furthermore, for all trace values $\tau ''$:

• 1. if $\delta ^{\mathcal {A}}_{(r, j)}(\tau , \tau '') = \alpha$ and $\varTheta (\tau , m){\downarrow }$, then $\varTheta (\tau '', m'){\downarrow }$ and $\varTheta (\tau '', m')\,+\,\alpha \le \varTheta (\tau , m)$

• 2. if $\delta ^{\mathcal {C}}_{(r, j)}(\tau , \tau '') = \alpha$ and $\varTheta (\tau ', m){\downarrow }$, then $\varTheta (\tau '', m'){\downarrow }$ and $\varTheta (\tau '', m')\,+\,\alpha \ge \varTheta (\tau ', m)$

This property asserts that the trace pair relation soundly bounds the difference in how quickly models realize trace pairs. In the case of antecedents this difference is bounded from above, and for consequents from below. The descending model property guarantees every model of a consequent trace value in a globally sound cyclic proof corresponds to a realizer of a positive maximal right-hand trace.

Lemma 2

(Trace Realization). If $\mathcal {P}$ is a globally sound cyclic proof containing a node $\varGamma [\tau '] \vdash \varDelta [\tau ]$ and m is a model such that $m\,{\models }\,\varGamma$ and $\varTheta (\tau , m){\downarrow }$, then there exists a positive, maximal right-hand trace $\mathbf {\tau }$ starting from $\tau$ and a sequence of models $\varvec{m}$ with $m_{1} = m$ that realizes it; moreover, $\varvec{m}$ realizes all left-hand traces following the same path starting from $\tau '$.

As a result, the realizability condition is sufficient to guarantee trace value orderings (see the technical report for a detailed proof [18, Theorem 22]).

Theorem 2

(Soundness of Realizability). If $\mathcal {P}: \tau \le \varGamma [\tau ']$ then $\varGamma : \tau \le \tau '$.

5 Computing Realizable Orderings Using Weighted Automata

In this section, we demonstrate a close connection between cyclic proofs and weighted automata. Under this correspondence, the realizability condition can be seen to be equivalent to an inclusion between particular weighted automata, allowing us to make use of known decision procedures in the world of weighted automata for deciding the realizability condition.

Weighted automata generalise standard finite state automata, assigning to words over alphabet $\varSigma$ values from a semiring $(V, \oplus , \otimes )$ of weights (see [8]).

Definition 9

(Weighted Automata). A weighted automaton $\mathscr {A}$ is a tuple $(Q, q_{I}, F, \gamma )$ consisting of a set Q of states containing an initial state $q_{I} \in Q$, a set $F \subseteq Q$ of final states, and a weighting function $\gamma : (Q \times \varSigma \times Q) \rightarrow V$.

A run of $\mathscr {A}$ over a (finite) word $\sigma _1 \ldots \sigma _n \in \varSigma ^{*}$ is a sequence of states $q_0 \ldots q_n$ such that $(q_{j-1}, \sigma _{j}, q_{j}) \in \mathsf {dom}(\gamma )$ for each $\sigma _{j}$. We write $\rho : q_{0} \xrightarrow {w} q_n$ to denote that $\rho$ is a run over w. The value $\mathsf {V}(\rho )$ of the run is the (left-to-right) semiring product of the weight $\gamma (q_{j-1}, \sigma _{j}, q_{j})$ of each transition. If $q_0 = q_{I}$ and $q_n \in F$ then $\rho$ is called an accepting run. The value of a word is the semiring sum of the values of all the accepting runs of that word, and is undefined if there are no such runs. Sum automata are weighted automata over the max-plus semiring $(\mathbb {N}, \mathsf {max}, {+})$, which is also referred to as the arctic semiring.

The (quantitative) language $\mathcal {L}_{\mathscr {A}}$ of an automaton $\mathscr {A}$ is the (partial) function over $\varSigma ^{*}$ computed by the automaton. The standard notion of inclusion between regular languages extends naturally to quantitative languages:

Definition 10

(Weighted Inclusion). $\mathcal {L}_{1} \le \mathcal {L}_{2}$ if and only if for every word w such that $\mathcal {L}_{1}(w)$ is defined, $\mathcal {L}_{2}(w)$ is also defined and $\mathcal {L}_{1}(w) \le \mathcal {L}_{2}(w)$.

The inclusion problem for sum automata is known to be undecidable [2, 13], but has recently been shown to be decidable for finite-valued sum automata, for which a finite bound can be given on the number of distinct values for runs over a given word [10].

Fig. 4.

The left-hand trace automaton $\mathscr {A}^{{\text {E}}{x}}_{\mathcal {P}}$ for the proof of ${\text {E}}{x} \vdash {\text {N}}{x}$ in Fig. 3.

Fig. 5.

The right-hand trace automaton $\mathscr {C}^{{\text {N}}{x}}_{\mathcal {P}}$ for the proof of ${\text {E}}{x} \vdash {\text {N}}{x}$ in Fig. 3.

5.1 Cyclic Proofs as Sum Automata

Given a node $n = \varGamma [\tau ] \vdash \varDelta [\tau ']$ in a cyclic proof $\mathcal {P}$ we construct two sum automata $\mathscr {A}_{\mathcal {P}}^{\tau }$ and $\mathscr {C}_{\mathcal {P}}^{\tau '}$ called left-hand and right-hand trace automata, respectively. Each state $(n, \tau )$ of a trace automaton corresponds to a particular trace value $\tau$ in some node n of $\mathcal {P}$, and the transitions are given by the trace pair relation. That is, there is a transition from $(n, \tau )$ to $(n', \tau ')$ with weight $k \in \{ 0, 1 \}$ precisely when n and $n'$ are the conclusion and j ^th premise, respectively, of a rule instance r with $\delta _{(r, j)}(\tau , \tau ') = k$. The letter accepted on the transition is the node $n'$. Thus, a run of one of these automata corresponds to a trace in $\mathcal {P}$, and the word accepted by the run is the path followed by the trace.

For lack of space, we elide the formal definition of the automata construction (see [18, Definition 23]), but in Figs. 4 and 5 we show the trace automata corresponding to the proof in Fig. 3. Accepting states are indicated by a double circle, and for each transition we show the node accepted in parentheses and the weight of the transition in brackets. We draw attention to the following:

• The left-hand trace automaton also includes (zero-weight) transitions to a state $\top$ with a self-transition accepting any node. Thus, the weight it computes for a path is the maximum value of $\mathsf {prog}(\mathbf {\tau })$ over all traces $\mathbf {\tau }$ following a prefix of that path. In contrast, the right-hand automaton considers only traces following the full path.

• Each automaton also includes a state $\bot$, the transitions to which accept a trace value rather than a node. The effect of this is that any word $w = n_1 \ldots n_k \tau$ accepted by the right-hand automaton corresponds to a partially maximal right-hand trace ending in $\tau$. If the left-hand automaton also accepts w, then we know there is a matching left-hand trace of equal length (cf. Definition 8).

• The accepting states of right-hand trace automata (excluding $\bot$) correspond to terminal trace values in non-axiomatic rules instances; when each such trace value is ground, we say the trace automaton is grounded.

This construction results in automata polynomial in the size of the proof $\mathcal {P}$, and allows the realizability condition to be encoded by the inclusion of the right-hand trace automaton within the left-hand one.

Theorem 3

$\mathcal {P}: \tau \le \varGamma [\tau ']$ holds if and only if $\mathscr {C}_{\mathcal {P}}^{\tau } \le \mathscr {A}_{\mathcal {P}}^{\tau '}$ and $\mathscr {C}_{\mathcal {P}}^{\tau }$ is grounded.

5.2 Decidability of the Realizability Condition

We now demonstrate that under certain conditions our trace automata become finite-valued, and so we can decide inclusion between them in polynomial time [10].

Remark 1

The trace pair relation $\delta$ satisfies an injectivity property². Namely, if both $\delta _{(r,j)}(\tau ', \tau )$ and $\delta _{(r,j)}(\tau '', \tau )$ are defined, then $\tau ' = \tau ''$. This means that, along any given path, traces may only branch and never converge. Consequently, there is at most one trace along a given path between an initial and final trace value. This immediately gives the following result.

Lemma 3

Every right-hand trace automaton $\mathcal {C}_{\mathcal {P}}^{\tau }$ is finite-valued.

Unfortunately, because left-hand trace automata include the state $\top$ and associated transitions, they are not in general finite-valued. When a proof contains a (left-hand) trace cycle (of the form $(n_1, \tau _1) \ldots (n_{j}, \tau _{j})$ with nodes $n_{1} = n_{j}$ and trace values $\tau _{1} = \tau _{j}$), the resulting left-hand trace automaton will contain the following configuration of states:

That is, there are runs $(n_{j-1}, \tau _{j-1}) \xrightarrow {w} (n_{j-1}, \tau _{j-1})$, $(n_{j-1}, \tau _{j-1}) \xrightarrow {w} \top$, and $\top \xrightarrow {w} \top$ with $w = n_1 \ldots n_{j-1}$. This results in the automaton being infinitely ambiguous [19, Sect. 3] and thus when the weight of the cycle is non-zero it is also infinite-valued.

To avoid this we modify our construction to produce a series of approximate left-hand trace automata $\mathscr {A}[k]_{\mathcal {P}}^{\tau }$, where $k > 0$ is called the degree of approximation. These refine the ‘sink’ state $\top$ into a finite chain of k sink states for each node (thus, these approximate automata are a factor of k larger than the original automaton). Once a run enters a chain of sink states $\top _{n}^{1..k}$, only a finite number of further occurrences of the node n are accepted. In contrast, the full automaton accepts paths with any number of further occurrences. This construction approximates the original one and results in finite-valued automata.

Lemma 4

Every approximate left-hand trace automaton $\mathscr {A}[k]_{\mathcal {P}}^{\tau }$ is finite-valued.

Lemma 5

(Soundness of Approximate Automata). For each $k > 0$, the inclusion $\mathscr {A}[k]_{\mathcal {P}}^{\tau } \le \mathscr {A}_{\mathcal {P}}^{\tau }$ holds.

The following further restrictions on proofs allow a relative completeness result. They are expressed in terms of simple trace cycles (containing no repeated trace values other than the first and last). A binary trace cycle is a pair of trace cycles following the same path.

Definition 11

Let $S = \varGamma [\tau '] \vdash \varDelta [\tau ]$ be a node in a cyclic proof $\mathcal {P}$. We say $\mathcal {P}$ is dynamic (w.r.t. S) when $\mathsf {prog}(\mathbf {\tau }) > 0$ for every simple left- and right-hand trace cycle $\mathbf {\tau }$ reachable from $\tau '$ and $\tau$, respectively. We say $\mathcal {P}$ is balanced (w.r.t. S) when $\mathsf {prog}(\mathbf {\tau }_1) = \mathsf {prog}(\mathbf {\tau }_2)$ for every simple left-hand binary cycle $(\mathbf {\tau }_1, \mathbf {\tau }_2)$ reachable from $\tau '$.

Checking whether a proof is balanced and dynamic requires finding the simple cycles, which can be done in time $\mathsf{{O}}((N + E)(C + 1))$, where N, E, and C are the number of nodes, edges and basic cycles in the graph, respectively [12]. The number of basic cycles in a complete graph is factorial in the number of nodes, thus the worst case complexity is super-exponential. Notwithstanding, cyclic proofs are by nature sparse graphs, so we expect the average runtime complexity to be much lower. All of our example proofs are both balanced and dynamic.

When a balanced, dynamic proof satisfies the realizability condition, its positive fully-maximal right-hand traces are always matched by left-hand traces that can be recognised by an approximate left-hand automaton whose degree of approximation can be bounded by the following two graph-theoretic quantities (which are polynomially bounded in the size of $\mathcal {P}$).

• (a) The trace width $\mathbf {W}(\mathcal {P})$ is the maximum number of trace values occurring in the antecedent or consequent of any node in $\mathcal {P}$. Any trace visiting a given node more than $\mathbf {W}(\mathcal {P})$ times must contain a cycle.

• (b) The binary left-hand cycle threshold $\mathbf {C}(\mathcal {P})$ is the number of distinct pairs of left-hand trace values occurring in $\mathcal {P}$. Any pair of left-hand traces following the same path of length greater than $\mathbf {C}(\mathcal {P})$ must contain a binary cycle.

Lemma 6

(Relative Completeness). If $\mathcal {P}: \tau \le \varGamma [\tau ']$ and $\mathcal {P}$ is both dynamic and balanced with respect to $\varGamma [\tau '] \vdash \varDelta [\tau ]$, then $\mathscr {C}_{\mathcal {P}}^{\tau } \le \mathscr {A}[N]_{\mathcal {P}}^{\tau '}$ and $\mathscr {C}_{\mathcal {P}}^{\tau }$ is grounded, where $N = 2 + \mathbf {W}(\mathcal {P}) \times (\mathbf {C}(\mathcal {P}) + 1)$.

From this, a qualified form of decidability follows. Note that when $\mathcal {P}$ is not balanced and dynamic we still have a semi-decision procedure.

Theorem 4

If $\mathcal {P}$ is dynamic and balanced with respect to $\varGamma [\tau '] \vdash \varDelta [\tau ]$, then it is decidable whether $\mathcal {P}: \tau \le \varGamma [\tau ']$ holds.

6 Conclusions and Future Work

In this paper, we have demonstrated that cyclic proofs of entailments involving inductively defined predicates implicitly contain information about the relationship between the semantic approximations of these predicates. This information is useful because indexing ordinals for these approximations can be used, e.g., as (components of) ranking functions in a program termination proof. We have shown that this information can be made explicit via a novel trace condition, and furthermore we have proved this condition to be decidable via a construction using weighted automata. Although different in form, we have drawn tacit parallels between our work and the (intuitionistic) concept of realizability because we extract the semantic information directly from the proofs themselves.

Our results also increase the expressive power of the cyclic proof technique. For example, if we can deduce from the proof of $\varGamma , {\text {P}}{\varvec{t}} \vdash \varSigma , {\text {Q}}{\varvec{u}}$ that ${\text {Q}}{\varvec{u}} \le {\text {P}}{\varvec{t}}$ then we can safely form a well-founded trace across the active formula in the cut application

from ${\text {P}}{\varvec{t}}$ in the conclusion to ${\text {Q}}{\varvec{u}}$ in the right-hand premise, and therefore witness the validity of cyclic pre-proofs that do not satisfy the existing global soundness condition for cyclic proofs.

An obvious direction for future work is to implement our decision procedure and integrate it with existing cyclic proof-based program verifiers, such as [17] which currently relies on explicit ordinal variables to track approximations. A question of practical importance is whether entailment proofs typically encountered in program verification fall under the conditions for decidability of the trace condition. It is interesting to consider whether weaker conditions exist that still guarantee decidability. There are also wider theoretical questions to consider. Our trace condition is sound, but it is also natural to ask for completeness: if $\varGamma : \tau \le \tau '$ holds does there also exist a proof $\mathcal {P}$ for which $\mathcal {P}: \tau \le \varGamma [\tau ']$ holds?