Advertisement

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

  • Henning BasoldEmail author
  • Ekaterina KomendantskayaEmail author
  • Yue Li
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11423)

Abstract

We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.

Keywords

Horn clause logic Coinduction Uniform proofs Intuitionistic logic Coalgebra Fibrations Löb modality 

1 Introduction

Horn clause logic is a Turing complete and constructive fragment of first-order logic, that plays a central role in verification [22], automated theorem proving [52, 53, 57] and type inference. Examples of the latter can be traced from the Hindley-Milner type inference algorithm [55, 73], to more recent uses of Horn clauses in Haskell type classes [26, 51] and in refinement types [28, 43]. Its popularity can be attributed to well-understood fixed point semantics and an efficient semi-decidable resolution procedure for automated proof search.

According to the standard fixed point semantics [34, 52], given a set P of Horn clauses, the least Herbrand model for P is the set of all (finite) ground atomic formulae inductively entailed by P. For example, the two clauses below define the set of natural numbers in the least Herbrand model.
$$\begin{aligned} \kappa _{\mathbf {nat}0}&: \mathbf {nat}\, 0 \\ \kappa _{\mathbf {nat}s}&: \forall x. \, \mathbf {nat}\, x \rightarrow \mathbf {nat}\, (s\, x) \end{aligned}$$
Formally, the least Herbrand model for the above two clauses is the set of ground atomic formulae obtained by taking a (forward) closure of the above two clauses. The model for \(\mathbf {nat}\) is given by Open image in new window .
We can also view Horn clauses coinductively. The greatest complete Herbrand model for a set P of Horn clauses is the largest set of finite and infinite ground atomic formulae coinductively entailed by P. For example, the greatest complete Herbrand model for the above two clauses is the setobtained by taking a backward closure of the above two inference rules on the set of all finite and infinite ground atomic formulae. The greatest Herbrand model is the largest set of finite ground atomic formulae coinductively entailed by P. In our example, it would be given by Open image in new window already. Finally, one can also consider the least complete Hebrand model, which interprets entailment inductively but over potentially infinite terms. In the case of \(\mathbf {nat}\), this interpretation does not differ from Open image in new window . However, finite paths in coinductive structures like transition systems, for example, require such semantics.

The need for coinductive semantics of Horn clauses arises in several scenarios: the Horn clause theory may explicitly define a coinductive data structure or a coinductive relation. However, it may also happen that a Horn clause theory, which is not explicitly intended as coinductive, nevertheless gives rise to infinite inference by resolution and has an interesting coinductive model. This commonly happens in type inference. We will illustrate all these cases by means of examples.

Horn Clause Theories as Coinductive Data Type Declarations. The following clause defines, together with \(\kappa _{\mathbf {nat}0}\) and \(\kappa _{\mathbf {nat}s}\), the type of streams over natural numbers.
$$\begin{aligned} \kappa _{\mathbf {stream}} : \forall x y. \, \mathbf {nat}\, x \, \wedge \, \mathbf {stream}\, y \, \rightarrow \mathbf {stream}\, (\mathrm {scons}\, x \, y) \end{aligned}$$
This Horn clause does not have a meaningful inductive, i.e. least fixed point, model. The greatest Herbrand model of the clauses is given byIn trying to prove, for example, the goal \((\mathbf {stream}\, x)\), a goal-directed proof search may try to find a substitution for x that will make \((\mathbf {stream}\, x)\) valid relative to the coinductive model of this set of clauses. This search by resolution may proceed by means of an infinite reduction \(\underline{\mathbf {stream}\, x} {\mathop {\rightsquigarrow }\limits ^{\kappa _{\mathbf {stream}}:[\mathrm {scons}\ y\ x'/x]}} \mathbf {nat}\, y \wedge \mathbf {stream}\, x' {\mathop {\rightsquigarrow }\limits ^{\kappa _{\mathbf {nat}0}:[0/y]}} \underline{\mathbf {stream}\, x'} {\mathop { \rightsquigarrow }\limits ^{\kappa _{\mathbf {stream}}:[\mathrm {scons}\ y'\ x''/x']}} \cdots \), thereby generating a stream Z of zeros via composition of the computed substitutions: \(Z = (\mathrm {scons}\, 0 \, x')[\mathrm {scons}\, 0 \, x''/x'] \cdots \). Above, we annotated each resolution step with the label of the clause it resolves against and the computed substitution. A method to compute an answer for this infinite sequence of reductions was given by Gupta et al. [41] and Simon et al. [69]: the underlined loop gives rise to the circular unifier \(x = \mathrm {scons}\, 0\, x\) that corresponds to the infinite term Z. It is proven that, if a loop and a corresponding circular unifier are detected, they provide an answer that is sound relative to the greatest complete Herbrand model of the clauses. This approach is known under the name of CoLP.
Horn Clause Theories in Type Inference. Below clauses give the typing rules of the simply typed \(\lambda \)-calculus, and may be used for type inference or type checking:
$$\begin{aligned} \kappa _{t1}&: \forall x \, \varGamma \, a. \, \mathbf {var}\, x \wedge \mathbf {find}\, \varGamma \, x \, a\ \rightarrow \mathbf {typed}\, \varGamma \, x \, a \\ \kappa _{t2}&: \forall x \, \varGamma \, a \, m \, b. \, \mathbf {typed}\, [x : a | \varGamma ] \, m \, b \rightarrow \mathbf {typed}\, \varGamma \, (\lambda \, x \, m)\, (a \rightarrow b) \\ \kappa _{t3}&: \forall \varGamma \, a \, m \, n \, b. \, \mathbf {typed}\, \varGamma \, m\, (a \rightarrow b) \wedge \mathbf {typed}\, \varGamma \, n\, a \rightarrow \mathbf {typed}\, \varGamma \, (\mathrm {app}\, m\, n) \, b \end{aligned}$$
It is well known that the Y-combinator is not typable in the simply-typed \(\lambda \)-calculus and, in particular, self-application \(\lambda x. \, x \, x\) is not typable either. However, by switching off the occurs-check in Prolog or by allowing circular unifiers in CoLP [41, 69], we can resolve the goal “\(\mathbf {typed}\, [] \, (\lambda \, x \, (\mathrm {app}\, x\, x)) \, a\)” and would compute the circular substitution: \(a = b \rightarrow c, b = b \rightarrow c\) suggesting that an infinite, or circular, type may be able to type this \(\lambda \)-term. A similar trick would provide a typing for the Y-combinator. Thus, a coinductive interpretation of the above Horn clauses yields a theory of infinite types, while an inductive interpretation corresponds to the standard type system of the simply typed \(\lambda \)-calculus.
Horn Clause Theories in Type Class Inference. Haskell type class inference does not require circular unifiers but may require a cyclic resolution inference [37, 51]. Consider, for example, the following mutually defined data structures in Haskell.
This type declaration gives rise to the following equality class instance declarations, where we leave the, here irrelevant, body out.
The above two type class instance declarations have the shape of Horn clauses. Since the two declarations mutually refer to each other, an instance inference for, e.g., Open image in new window will give rise to an infinite resolution that alternates between the subgoals Open image in new window and Open image in new window . The solution is to terminate the computation as soon as the cycle is detected [51], and this method has been shown sound relative to the greatest Herbrand models in [36]. We will demonstrate this later in the proof systems proposed in this paper.
The diversity of these coinductive examples in the existing literature shows that there is a practical demand for coinductive methods in Horn clause logic, but it also shows that no unifying proof-theoretic approach exists to allow for a generic use of these methods. This causes several problems.
Table 1.

Examples of greatest (complete) Herbrand models for Horn clauses \(\gamma _{1}\mathbf{,}\) \(\gamma _{2}\mathbf{,}\) \(\gamma _{3}\mathbf{.}\) The signatures are Open image in new window for the clause \(\gamma _1\) and Open image in new window for the others.

Problem 1. The existing proof-theoretic coinductive interpretations of cycle and loop detection are unclear, incomplete and not uniform. To see this, consider Table 1, which exemplifies three kinds of circular phenomena in Horn clauses: The clause \(\gamma _1\) is the easiest case. Its coinductive models are given by the finite set \(\{ p \, a\}\). On the other extreme is the clause \(\gamma _3\) that, just like \(\kappa _{\mathbf {stream}}\), admits only an infinite formula in its coinductive model. The intermediate case is \(\gamma _2\), which could be interpreted by an infinite set of finite formulae in its greatest Herbrand model, or may admit an infinite formula in its greatest complete Herbrand model. Examples like \(\gamma _1\) appear in Haskell type class resolution [51], and examples like \(\gamma _2\) in its experimental extensions [37]. Cycle detection would only cover computations for \(\gamma _1\), whereas \(\gamma _2\), \(\gamma _3\) require some form of loop detection1. However, CoLP’s loop detection gives confusing results here. It correctly fails to infer \(p\, a\) from \(\gamma _3\) (no unifier for subgoals \(p \, a\) and \(p \, (f \, a)\) exists), but incorrectly fails to infer \(p \, a\) from \(\gamma _2\) (also failing to unify \(p \, a\) and \(p \, (f \, a)\)). The latter failure is misleading bearing in mind that \(p\, a\) is in fact in the coinductive model of \(\gamma _2\). Vice versa, if we interpret the CoLP answer \(x = f \, x\) as a declaration of an infinite term \((f \, f \, \ldots )\) in the model, then CoLP’s answer for \(\gamma _3\) and \(p \, x\) is exactly correct, however the same answer is badly incomplete for the query involving \(p \, x\) and \(\gamma _2\), because \(\gamma _2\) in fact admits other, finite, formulae in its models. And in some applications, e.g. in Haskell type class inference, a finite formula would be the only acceptable answer for any query to \(\gamma _2\).

This set of examples shows that loop detection is too coarse a tool to give an operational semantics to a diversity of coinductive models.

Problem 2. Constructive interpretation of coinductive proofs in Horn clause logic is unclear. Horn clause logic is known to be a constructive fragment of FOL. Some applications of Horn clauses rely on this property in a crucial way. For example, inference in Haskell type class resolution is constructive: when a certain formula F is inferred, the Haskell compiler in fact constructs a proof term that inhabits F seen as type. In our earlier example Open image in new window of the Haskell type classes, Haskell in fact captures the cycle by a fixpoint term t and proves that t inhabits the type Open image in new window . Although we know from [36] that these computations are sound relative to greatest Herbrand models of Horn clauses, the results of [36] do not extend to Horn clauses like \(\gamma _3\) or \(\kappa _{\mathbf {stream}}\), or generally to Horn clauses modelled by the greatest complete Herbrand models. This shows that there is not just a need for coinductive proofs in Horn clause logic, but constructive coinductive proofs.
Fig. 1.

Cube of logics covered by CUP

Problem 3. Incompleteness of circular unification for irregular coinductive data structures. Table 1 already showed some issues with incompleteness of circular unification. A more famous consequence of it is the failure of circular unification to capture irregular terms. This is illustrated by the following Horn clause, which defines the infinite stream of successive natural numbers.
$$\begin{aligned} \kappa _{\mathbf {from}}: \forall x \, y. \, \mathbf {from}\, (s\, x) \, y \rightarrow \mathbf {from}\, x \, (\mathrm {scons}\, x \, y) \end{aligned}$$
The reductions for \(\mathbf {from}\, 0 \, y\) consist only of irregular (non-unifiable) formulae:The composition of the computed substitutions would suggest an infinite term as answer: \(\mathbf {from}\, 0 \, (\mathrm {scons}\ 0\ (\mathrm {scons}\ (s \, 0)\ \ldots ))\). However, circular unification no longer helps to compute this answer, and CoLP fails. Thus, there is a need for more general operational semantics that allows irregular coinductive structures.

A New Theory of Coinductive Proof Search in Horn Clause Logic

In this paper, we aim to give a principled and general theory that resolves the three problems above. This theory establishes a constructive foundation for coinductive resolution and allows us to give proof-theoretic characterisations of the approaches that have been proposed throughout the literature.

To solve Problem 1, we follow the footsteps of the uniform proofs by Miller et al. [53, 54], who gave a general proof-theoretic account of resolution in first-order Horn clause logic (fohc) and three extensions: first-order hereditary Harrop clauses (fohh), higher-order Horn clauses (hohc), and higher-order hereditary Harrop clauses (hohh). In Sect. 3, we extend uniform proofs with a general coinduction proof principle. The resulting framework is called coinductive uniform proofs (CUP). We show how the coinductive extensions of the four logics of Miller et al., which we name co-fohc, co-fohh, co-hohc and co-hohh, give a precise proof-theoretic characterisation to the different kinds of coinduction described in the literature. For example, coinductive proofs involving the clauses \(\gamma _1\) and \(\gamma _2\) belong to co-fohc and co-fohh, respectively. However, proofs involving clauses like \(\gamma _3\) or \(\kappa _{\mathbf {stream}}\) require in addition fixed point terms to express infinite data. These extentions are denoted by Open image in new window , Open image in new window , Open image in new window and Open image in new window .

Section 3 shows that this yields the cube in Fig. 1, where the arrows show the increase in logical strength. The invariant search for regular infinite objects done in CoLP is fully described by the logic Open image in new window , including proofs for clauses like \(\gamma _3\) and \(\kappa _{\mathbf {stream}}\). An important consequence is that CUP is complete for \(\gamma _1\), \(\gamma _2\), and \(\gamma _3\), e.g. \(p \, a\) is provable from \(\gamma _2\) in CUP, but not in CoLP.

In tackling Problem 3, we will find that the irregular proofs, such as those for \(\kappa _{\mathbf {from}}\), can be given in Open image in new window . The stream of successive numbers can be defined as a higher-order fixed point term Open image in new window , and the proposition \(\forall x. \, \mathbf {from}\, x \, (s_\mathrm {fr}\, x)\) is provable in Open image in new window . This requires the use of higher-order syntax, fixed point terms and the goals of universal shape, which become available in the syntax of Hereditary Harrop logic.

In order to solve Problem 2 and to expose the constructive nature of the resulting proof systems, we present in Sect. 4 a coinductive extension of first-order intuitionistic logic and its sequent calculus. This extension ( Open image in new window ) is based on the so-called later modality (or Löb modality) known from provability logic [16, 71], type theory [8, 58] and domain theory [20]. However, our way of using the later modality to control recursion in first-order proofs is new and builds on [13, 14]. In the same section we also show that CUP is sound relative to Open image in new window , which gives us a handle on the constructive content of CUP. This yields, among other consequences, a constructive interpretation of CoLP proofs.

Section 5 is dedicated to showing soundness of both coinductive proof systems relative to complete Herbrand models [52]. The construction of these models is carried out by using coalgebras and category theory. This frees us from having to use topological methods and will simplify future extensions of the theory to, e.g., encompass typed logic programming. It also makes it possible to give original and constructive proofs of soundness for both CUP and Open image in new window in Sect. 5. We finish the paper with discussion of related and future work.

Originality of the Contribution

The results of this paper give a comprehensive characterisation of coinductive Horn clause theories from the point of view of proof search (by expressing coinductive proof search and resolution as coinductive uniform proofs), constructive proof theory (via a translation into an intuitionistic sequent calculus), and coalgebraic semantics (via coinductive Herbrand models and constructive soundness results). Several of the presented results have never appeared before: the coinductive extension of uniform proofs; characterisation of coinductive properties of Horn clause theories in higher-order logic with and without fixed point operators; coalgebraic and fibrational view on complete Herbrand models; and soundness of an intuitionistic logic with later modality relative to complete Herbrand models.

2 Preliminaries: Terms and Formulae

In this section, we set up notation and terminology for the rest of the paper. Most of it is standard, and blends together the notation used in [53] and [11].

Definition 1

We define the sets \(\mathbb {T}\) of types and \(\mathbb {P}\) of proposition types by the following grammars, where \(\iota \) and \(o\) are the base type and base proposition type.
$$\begin{aligned} {\mathbb {T}}\ni \sigma ,\tau \,{:}{:}\!\!= \iota \,|\,\sigma \rightarrow \tau \qquad \qquad {\mathbb {P}}\ni \rho \,{:}{:}\!\!= o\,|\,\sigma \rightarrow \rho ,\quad \sigma \in {\mathbb {T}} \end{aligned}$$
We adapt the usual convention that \(\rightarrow \) binds to the right.
Fig. 2.

Well-formed terms

Fig. 3.

Well-formed formulae

Definition 2

A term signature \(\varSigma \) is a set of pairs \(c : \tau \), where \(\tau \in \mathbb {T}\), and a predicate signature is a set \(\varPi \) of pairs \(p : \rho \) with \(\rho \in \mathbb {P}\). The elements in \(\varSigma \) and \(\varPi \) are called term symbols and predicate symbols, respectively. Given term and predicate signatures \(\varSigma \) and \(\varPi \), we refer to the pair \((\varSigma , \varPi )\) as signature. Let \(\mathrm {Var}\) be a countable set of variables, the elements of which we denote by \(x, y, \cdots \) We call a finite list \(\varGamma \) of pairs \(x : \tau \) of variables and types a context. The set \(\varLambda _{\varSigma }\) of (well-typed) terms over \(\varSigma \) is the collection of all M with Open image in new window for some context \(\varGamma \) and type \(\tau \in \mathbb {T}\), where Open image in new window is defined inductively in Fig. 2. A term is called closed if Open image in new window , otherwise it is called open. Finally, we let \(\varLambda ^{-}_{\varSigma }\) denote the set of all terms M that do not involve Open image in new window .

Definition 3

Let \((\varSigma , \varPi )\) be a signature. We say that \(\varphi \) is a (first-order) formula in context \(\varGamma \), if \(\varGamma \Vdash \varphi \) is inductively derivable from the rules in Fig. 3.

Definition 4

The reduction relation \(\longrightarrow \) on terms in \(\varLambda _{\varSigma }\) is given as the compatible closure (reduction under applications and binders) of \(\beta \)- and Open image in new window -reduction:We denote the reflexive, transitive closure of \(\longrightarrow \) by Open image in new window . Two terms M and N are called convertible, if \(M \equiv N\), where \(\equiv \) is the equivalence closure of \(\longrightarrow \). Conversion of terms extends to formulae in the obvious way: if \(M_k \equiv M'_k\) for \(k = 1, \cdots , n\), then \(p \> M_1 \cdots M_n \equiv p \> M'_1 \cdots \> M'_n\).

We will use in the following that the above calculus features subject reduction and confluence, cf. [61]: if Open image in new window and \(M \equiv N\), then Open image in new window ; and \(M \equiv N\) iff there is a term P, such that Open image in new window and Open image in new window .

The order of a type \(\tau \in \mathbb {T}\) is given as usual by Open image in new window and Open image in new window . If Open image in new window , then the arity of \(\tau \) is given by Open image in new window and Open image in new window . A signature \(\varSigma \) is called first-order, if for all \(f : \tau \in \varSigma \) we have Open image in new window . We let the arity of f then be Open image in new window and denote it by Open image in new window .

Definition 5

The set of guarded base terms over a first-order signature \(\varSigma \) is given by the following type-driven rules.

General guarded terms are terms M, such that all Open image in new window -subterms are guarded base terms, which means that they are generated by the following grammar.
$$\begin{aligned} G\, {:}{:}\!\!= M\,\left( {\mathrm{with}\,\,{ \vdash _g}\,M:\tau \,\,\text {for some type}\,\,\tau } \right) \,|\,c \in \varSigma \,|\,x \in \,\mathrm{Var}\,|\,G\,G\,|\,\lambda x.G \end{aligned}$$
Finally, M is a first-order term over \(\varSigma \) with Open image in new window if Open image in new window and the types of all variables occurring in \(\varGamma \) are of order 0. We denote the set of guarded first-order terms M with Open image in new window by \(\varLambda ^{G,1}_{\varSigma }(\varGamma )\) and the set of guarded terms in \(\varGamma \) by \(\varLambda ^{G}_{\varSigma }(\varGamma )\). If \(\varGamma \) is empty, we just write \(\varLambda ^{G,1}_{\varSigma }\) and \(\varLambda ^{G}_{\varSigma }\), respectively.

Note that an important aspect of guarded terms is that no free variable occurs under a Open image in new window -operator. Guarded base terms should be seen as specific fixed point terms that we will be able to unfold into potentially infinite trees. Guarded terms close guarded base terms under operations of the simply typed \(\lambda \)-calculus.

Example 6

Let us provide a few examples that illustrate (first-order) guarded terms. We use the first-order signature Open image in new window .

  1. 1.

    Let Open image in new window be the function that computes the streams of numerals starting at the given argument. It is easy to show that Open image in new window and so \(s_\mathrm {fr}\; 0 \in \varLambda ^{G,1}_{\varSigma }\).

     
  2. 2.

    For the same signature \(\varSigma \) we also have Open image in new window . Thus \(x \in \varLambda ^{G,1}_{\varSigma }(x : \iota )\) and \(s \; x \in \varLambda ^{G,1}_{\varSigma }(x : \iota )\).

     
  3. 3.

    We have Open image in new window , but \((x \; 0) \not \in \varLambda ^{G,1}_{\varSigma }(x : \iota \rightarrow \iota )\).

     

The purpose of guarded terms is that these are productive, that is, we can reduce them to a term that either has a function symbol at the root or is just a variable. In other words, guarded terms have head normal forms: We say that a term M is in head normal form, if Open image in new window for some \(f \in \varSigma \) or if \(M = x\) for some variable x. The following lemma is a technical result that is needed to show in Lemma 8 that all guarded terms have a head normal form.

Lemma 7

Let M and N be guarded base terms with Open image in new window and Open image in new window . Then Open image in new window is a guarded base term with Open image in new window .

Lemma 8

If M is a first-order guarded term with \(M \in \varLambda ^{G,1}_{\varSigma }(\varGamma )\), then M reduces to a unique head normal form. This means that either (i) there is a unique \(f \in \varSigma \) and terms Open image in new window with Open image in new window and Open image in new window , and for all L if Open image in new window , then Open image in new window ; or (ii) Open image in new window for some \(x : \iota \in \varGamma \).

We end this section by introducing the notion of an atom and refinements thereof. This will enable us to define the different logics and thereby to analyse the strength of coinduction hypotheses, which we promised in the introduction.

Definition 9

A formula \(\varphi \) of the shape \(\top \) or \(p \; M_1 \cdots \; M_n\) is an atom and a
  • first-order atom, if p and all the terms \(M_i\) are first-order;

  • guarded atom, if all terms \(M_i\) are guarded; and

  • simple atom, if all terms \(M_i\) are non-recursive, that is, are in \(\varLambda ^{-}_{\varSigma }\).

First-order, guarded and simple atoms are denoted by \(\mathrm {At}_1\), Open image in new window and Open image in new window . We denote conjunctions of these predicates by Open image in new window and Open image in new window .

Note that the restriction for \(\mathrm {At}^g_{\omega }\) only applies to fixed point terms. Hence, any formula that contains terms without Open image in new window is already in Open image in new window and Open image in new window . Since these notions are rather subtle, we give a few examples

Example 10

We list three examples of first-order atoms.

  1. 1.

    For \(x : \iota \) we have \(\mathbf {stream}\; x \in \mathrm {At}_1\), but there are also “garbage” formulae like “ Open image in new window ” in \(\mathrm {At}_1\). Examples of atoms that are not first-order are \(p \; M\), where \(p : (\iota \rightarrow \iota ) \rightarrow o\) or Open image in new window .

     
  2. 2.

    Our running example “\(\mathbf {from}\; 0 \; (s_\mathrm {fr}\; 0)\)” is a first-order guarded atom in \(\mathrm {At}_1^g\).

     
  3. 3.

    The formulae in \(\mathrm {At}_1^s\) may not contain recursion and higher-order features. However, the atoms of Horn clauses in a logic program fit in here.

     

3 Coinductive Uniform Proofs

This section introduces the eight logics of the coinductive uniform proof framework announced and motivated in the introduction. The major difference of uniform proofs with, say, a sequent calculus is the “uniformity” property, which means that the choice of the application of each proof rule is deterministic and all proofs are in normal form (cut free). This subsumes the operational semantics of resolution, in which the proof search is always goal directed. Hence, the main challenge, that we set out to solve in this section, is to extend the uniform proof framework with coinduction, while preserving this valuable operational property.

We begin by introducing the different goal formulae and definite clauses that determine the logics that were presented in the cube for coinductive uniform proofs in the introduction. These clauses and formulae correspond directly to those of the original work on uniform proofs [53] with the only difference being that we need to distinguish atoms with and without fixed point terms. The general idea is that goal formulae (G-formulae) occur on the right of a sequent, thus are the goal to be proved. Definite clauses (D-formulae), on the other hand, are selected from the context as assumptions. This will become clear once we introduce the proof system for coinductive uniform proofs.

Definition 11

Let \(D_i\) be generated by the following grammar with Open image in new window .
Table 2.

D- and G-formulae for coinductive uniform proofs.

The sets of definite clauses (D-formulae) and goals (G-formulae) of the four logics Open image in new window , \(\textit{co-fohh}\), \(\textit{co-hohc}\), \(\textit{co-hohh}\) are the well-formed formulae of the corresponding shapes defined in Table 2. For the variations Open image in new window etc. of these logics with fixed point terms, we replace upper index “s” with “g” everywhere in Table 2. A D-formula of the shape Open image in new window is called H-formula or Horn clause if \(A_k \in \mathrm {At}_1^s\), and \(H^g\)-formula if \(A_k \in \mathrm {At}_1^g\). Finally, a logic program (or program) P is a set of H-formulae. Note that any set of D-formulae in fohc can be transformed into an intuitionistically equivalent set of H-formulae [53].

We are now ready to introduce the coinductive uniform proofs. Such proofs are composed of two parts: an outer coinduction that has to be at the root of a proof tree, and the usual the usual uniform proofs by Miller et al. [54]. The latter are restated in Fig. 4. Of special notice is the rule \(\textsc {decide}\) that mimics the operational behaviour of resolution in logic programming, by choosing a clause D from the given program to resolve against. The coinduction is started by the rule co-fix in Fig. 5. Our proof system mimics the typical recursion with a guard condition found in coinductive programs and proofs [5, 8, 19, 31, 40]. This guardedness condition is formalised by applying the guarding modality \({\langle \_\rangle }\) on the formula being proven by coinduction and the proof rules that allow us to distribute the guard over certain logical connectives, see Fig. 5. The guarding modality may be discharged only if the guarded goal was resolved against a clause in the initial program or any hypothesis, except for the coinduction hypotheses. This is reflected in the rule Open image in new window , where we may only pick a clause from P, and is in contrast to the rule \(\textsc {decide}\), in which we can pick any hypothesis. The proof may only terminate with the \(\textsc {initial}\) step if the goal is no longer guarded.

Note that the Open image in new window rule introduces a goal as a new hypothesis. Hence, we have to require that this goal is also a definite clause. Since coinduction hypotheses play such an important role, they deserve a separate definition.

Definition 12

Given a language L from Table 2, a formula \(\varphi \) is a Open image in new window of L if \(\varphi \) simultaneously is a D- and a G-formula of L.

Note that the Open image in new window of co-fohc and co-fohh can be transformed into equivalent H- or \(H^g\)-formulae, since any Open image in new window is a D-formula.

Let us now formally introduce the coinductive uniform proof system.
Fig. 4.

Uniform proof rules

Fig. 5.

Coinductive uniform proof rules

Definition 13

Let P and \(\varDelta \) be finite sets of, respectively, definite clauses and Open image in new window , over the signature \(\varSigma \), and suppose that G is a goal and \(\varphi \) is a Open image in new window . A sequent is either a uniform provability sequent of the form Open image in new window or Open image in new window as defined in Fig. 4, or it is a coinductive uniform provability sequent of the form Open image in new window as defined in Fig. 5. Let L be a language from Table 2. We say that \(\varphi \) is coinductively provable in L, if P is a set of D-formulae in L, \(\varphi \) is a Open image in new window in L and Open image in new window holds.

The logics we have introduced impose different syntactic restrictions on D- and G-formulae, and will therefore admit coinduction goals of different strength. This ability to explicitly use stronger coinduction hypotheses within a goal-directed search was missing in CoLP, for example. And it allows us to account for different coinductive properties of Horn clauses as described in the introduction. We finish this section by illustrating this strengthening.

The first example is one for the logic co-fohc, in which we illustrate the framework on the problem of type class resolution.

Example 14

Let us restate the Haskell type class inference problem discussed in the introduction in terms of Horn clauses:To prove \(\mathbf {eq}\ (\mathrm {odd}\ \mathrm {i})\) for this set of Horn clauses, it is sufficient to use this formula directly as coinduction hypothesis, as shown in Fig. 6. Note that this formula is indeed a Open image in new window of co-fohc, hence we find ourselves in the simplest scenario of coinductive proof search. In Table 1, \(\gamma _1\) is a representative for this kind of coinductive proofs with simplest atomic goals.
It was pointed out in [37] that Haskell’s type class inference can also give rise to irregular corecursion. Such cases may require the more general coinduction hypothesis (e.g. universal and/or implicative) of co-fohh or co-hohh. The below set of Horn clauses is a simplified representation of a problem given in [37]:
Fig. 6.

The co-fohc proof for Horn clauses arising from Haskell Type class examples. \(\varphi \) abbreviates the coinduction hypothesis \(\mathbf {eq}\ (\mathrm {odd}\ \mathrm {i})\). Note its use in the branch \(\spadesuit \).

Trying to prove \(\mathbf {eq}\; (s \; \mathrm {i})\) by using \(\mathbf {eq}\; (s \; \mathrm {i})\) directly as a coinduction hypothesis is deemed to fail, as the coinductive proof search is irregular and this coinduction hypothesis would not be applicable in any guarded context. But it is possible to prove \(\mathbf {eq}\; (s \; \mathrm {i})\) as a corollary of another theorem: \(\forall x. \,(\mathbf {eq}\; x) \rightarrow \mathbf {eq}\; (s \; x)\). Using this formula as coinduction hypothesis leads to a successful proof, which we omit here. From this more general goal, we can derive the original goal by instantiating the quantifier with \(\mathrm {i}\) and eliminating the implication with \(\kappa _{\mathrm {i}}\). This second derivation is sound with respect to the models, as we show in Theorem 34.

We encounter \(\gamma _2\) from Table 1 in a similar situation: To prove \(p \, a\), we first have to prove \(\forall x. \,p \ x\) in co-fohh, and then obtain \(p \ a\) as a corollary by appealing to Theorem 34. The next example shows that we can cover all cases in Table 1 by providing a proof in Open image in new window that involves irregular recursive terms.

Example 15

Recall the clause \(\forall x \; y. \, \mathbf {from}\; (s\; x) \; y \rightarrow \mathbf {from}\; x \; (\mathrm {scons}\; x \; y)\) that we named \(\kappa _{\mathbf {from}}\) in the introduction. Proving \(\exists y. \, \mathbf {from}\; 0 \; y\) is again not possible directly. Instead, we can use the term Open image in new window from Example 6 and prove \(\forall x. \, \mathbf {from}\; x \; (s_\mathrm {fr}\; x)\) coinductively, as shown in Fig. 7. This formula gives a coinduction hypothesis of sufficient generality. Note that the correct coinduction hypothesis now requires the fixed point definition of an infinite stream of successive numbers and universal quantification in the goal. Hence the need for the richer language of Open image in new window . From this more general goal we can derive our initial goal \(\exists \ y. \mathbf {from}\; 0 \; y\) by instantiating y with \(s_\mathrm {fr}\; 0\).

Fig. 7.

The Open image in new window proof for \(\varphi = \forall x. \, \mathbf {from}\; x \; (s_\mathrm {fr}\; x)\). Note that the last step of the leftmost branch involves \({\mathbf {from}\ c\ (\mathrm {scons}\ c\ (s_\mathrm {fr}\ (s \ c))) }\equiv {\mathbf {from}\ c\ (s_\mathrm {fr}\ c)}\).

There are examples of coinductive proofs that require a fixed point definition of an infinite stream, but do not require the syntax of higher-order terms or hereditary Harrop formulae. Such proofs can be performed in the Open image in new window logic. A good example is a proof that the stream of zeros satisfies the Horn clause theory defining the predicate \(\mathbf {stream}\) in the introduction. The goal \((\mathbf {stream}\ s_{0})\), with Open image in new window can be proven directly by coinduction. Similarly, one can type self-application with the infinite type Open image in new window for some given type b. The proof for Open image in new window is then in Open image in new window . Finally, the clause \(\gamma _3\) is also in this group. More generally, circular unifiers obtained from CoLP’s [41] loop detection yield immediately guarded fixed point terms, and thus CoLP corresponds to coinductive proofs in the logic Open image in new window . A general discussion of Horn clause theories that describe infinite objects was given in [48], where the above logic programs were identified as being productive.

4 Coinductive Uniform Proofs and Intuitionistic Logic

In the last section, we introduced the framework of coinductive uniform proofs, which gives an operational account to proofs for coinductively interpreted logic programs. Having this framework at hand, we need to position it in the existing ecosystem of logical systems. The goal of this section is to prove that coinductive uniform proofs are in fact constructive. We show this by first introducing an extension of intuitionistic first-order logic that allows us to deal with recursive proofs for coinductive predicates. Afterwards, we show that coinductive uniform proofs are sound relative to this logic by means of a proof tree translation. The model-theoretic soundness proofs for both logics will be provided in Sect. 5.

We begin by introducing an extension of intuitionistic first-order logic with the so-called later modality, written Open image in new window . This modality is the essential ingredient that allows us to equip proofs with a controlled form of recursion. The later modality stems originally from provability logic, which characterises transitive, well-founded Kripke frames [30, 72], and thus allows one to carry out induction without an explicit induction scheme [16]. Later, the later modality was picked up by the type-theoretic community to control recursion in coinductive programming [8, 9, 21, 56, 58], mostly with the intent to replace syntactic guardedness checks for coinductive definitions by type-based checks of well-definedness.
Fig. 8.

Intuitionistic rules for standard connectives

Fig. 9.

Rules for the later modality

Formally, the logic Open image in new window is given by the following definition.

Definition 16

The formulae of Open image in new window are given by Definition 3 and the rule:Conversion extends to these formulae in the obvious way. Let \(\varphi \) be a formula and \(\varDelta \) a sequence of formulae in Open image in new window . We say \(\varphi \) is provable in context \(\varGamma \) under the assumptions \(\varDelta \) in Open image in new window , if Open image in new window holds. The provability relation \(\vdash \) is thereby given inductively by the rules in Figs. 8 and 9.

The rules in Fig. 8 are the usual rules for intuitionistic first-order logic and should come at no surprise. More interesting are the rules in Fig. 9, where the rule Open image in new window introduces recursion into the proof system. Furthermore, the rule Open image in new window allows us to to distribute the later modality over implication, and consequently over conjunction and universal quantification. This is essential in the translation in Theorem 18 below. Finally, the rule Open image in new window gives us the possibility to proceed without any recursion, if necessary.

Note that so far it is not possible to use the assumption Open image in new window introduced in the Open image in new window -rule. The idea is that the formulae of a logic program provide us the obligations that we have to prove, possibly by recursion, in order to prove a coinductive predicate. This is cast in the following definition.

Definition 17

Given an \(H^g\)-formula \(\varphi \) of the shape Open image in new window , we define its guarding Open image in new window to be Open image in new window . For a logic program P, we define its guarding Open image in new window by guarding each formula in P.

The translation given in Definition 17 of a logic program into formulae that admit recursion corresponds unfolding a coinductive predicate, cf. [14]. We show now how to transform a coinductive uniform proof tree into a proof tree in Open image in new window , such that the recursion and guarding mechanisms in both logics match up.

Theorem 18

If P is a logic program over a first-order signature \(\varSigma \) and the sequent Open image in new window is provable in Open image in new window , then Open image in new window is provable in Open image in new window .

To prove this theorem, one uses that each coinductive uniform proof tree starts with an initial tree that has an application of the Open image in new window -rule at the root and that eliminates the guard by using the rules in Fig. 5. At the leaves of this tree, one finds proof trees that proceed only by means of the rules in Fig. 4. The initial tree is then translated into a proof tree in Open image in new window that starts with an application of the Open image in new window -rule, which corresponds to the Open image in new window -rule, and that simultaneously transforms the coinduction hypothesis and applies introduction rules for conjunctions etc. This ensures that we can match the coinduction hypothesis with the guarded formulae of the program P.

The results of this section show that it is irrelevant whether the guarding modality is used on the right (CUP-style) or on the left ( Open image in new window -style), as the former can be translated into the latter. However, CUP uses the guarding on the right to preserve proof uniformity, whereas Open image in new window extends a general sequent calculus. Thus, to obtain the reverse translation, we would have to have an admissible cut rule in CUP. The main ingredient to such a cut rule is the ability to prove several coinductive statements simultaneously. This is possible in CUP by proving the conjunction of these statements. Unfortunately, we cannot eliminate such a conjunction into one of its components, since this would require non-deterministic guessing in the proof construction, which in turn breaks uniformity. Thus, we leave a solution of this problem for future work.

5 Herbrand Models and Soundness

In Sect. 4 we showed that coinductive uniform proofs are sound relative to the intuitionistic logic Open image in new window . This gives us a handle on the constructive nature of coinductive uniform proofs. Since Open image in new window is a non-standard logic, we still need to provide semantics for that logic. We do this by interpreting in Sect. 5.4 the formulae of Open image in new window over the well-known (complete) Herbrand models and prove the soundness of the accompanying proof system with respect to these models. Although we obtain soundness of coinductive uniform proofs over Herbrand models from this, this proof is indirect and does not give a lot of information about the models captured by the different calculi co-fohc etc. For this reason, we will give in Sect. 5.3 a direct soundness proof for coinductive uniform proofs. We also obtain coinduction invariants from this proof for each of the calculi, which allows us to describe their proof strength.

5.1 Coinductive Herbrand Models and Semantics of Terms

Before we come to the soundness proofs, we introduce in this section (complete) Herbrand models by using the terminology of final coalgebras. We then utilise this description to give operational and denotational semantics to guarded terms. These semantics show that guarded terms allow the description and computation of potentially infinite trees.

The coalgebraic approach has been proven very successful both in logic and programming [1, 75, 76]. We will only require very little category theoretical vocabulary and assume that the reader is familiar with the category \(\mathbf {Set}\) of sets and functions, and functors, see for example [12, 25, 50]. The terminology of algebras and coalgebras [4, 47, 64, 65] is given by the following definition.

Definition 19

A coalgebra for a functor \(F :\mathbf {Set}\rightarrow \mathbf {Set}\) is a map \(c :X \rightarrow FX\). Given coalgebras \(d : Y \rightarrow FY\) and \(c :X \rightarrow FX\), we say that a map \(h : Y \rightarrow X\) is a homomorphism \(d \rightarrow c\) if \(Fh \mathbin {\circ }d = c \mathbin {\circ }h\). We call a coalgebra \(c :X \rightarrow FX\) final, if for every coalgebra d there is a unique homomorphism \(h :d \rightarrow c\). We will refer to h as the coinductive extension of d.

The idea of (complete) Herbrand models is that a set of Horn clauses determines for each predicate symbol a set of potentially infinite terms. Such terms are (potentially infinite) trees, whose nodes are labelled by function symbols and whose branching is given by the arity of these function symbols. To be able to deal with open terms, we will allow such trees to have leaves labelled by variables. Such trees are a final coalgebra for a functor determined by the signature.

Definition 20

Let \(\varSigma \) be first-order signature. The extension of a first-order signature \(\varSigma \) is a (polynomial) functor [38] Open image in new window given bywhere Open image in new window is defined in Sect. 2 and \(X^n\) is the n-fold product of X. We define for a set V a functor Open image in new window by Open image in new window , where \(+\) is the coproduct (disjoint union) in \(\mathbf {Set}\).

To make sense of the following definition, we note that we can view \(\varPi \) as a signature and we thus obtain its extension Open image in new window . Moreover, we note that the final coalgebra of Open image in new window exists because Open image in new window is a polynomial functor.

Definition 21

Let Open image in new window be a first-order signature. The coterms over \(\varSigma \) are the final coalgebra Open image in new window . For brevity, we denote the coterms with no variables, i.e. \(\varSigma ^{\infty }(\emptyset )\), by Open image in new window , and call it the (complete) Herbrand universe and its elements ground coterms. Finally, we let the (complete) Herbrand base \(\mathcal {B}^{\infty }\) be the set Open image in new window .

The construction \(\varSigma ^{\infty }(V)\) gives rise to a functor \(\varSigma ^{\infty } :\mathbf {Set}\rightarrow \mathbf {Set}\), called the free completely iterative monad [5]. If there is no ambiguity, we will drop the injections \(\kappa _i\) when describing elements of \(\varSigma ^{\infty }(V)\). Note that \(\varSigma ^{\infty }(V)\) is final with property that for every \(s \in \varSigma ^{\infty }(V)\) either there are \(f \in \varSigma \) and Open image in new window with Open image in new window , or there is \(x \in V\) with Open image in new window . Finality allows us to specify unique maps into \(\varSigma ^{\infty }(V)\) by giving a coalgebra Open image in new window . In particular, one can define for each \(\theta :V \rightarrow \varSigma ^{\infty }\) the substitution \(t[\theta ]\) of variables in the coterm t by \(\theta \) as the coinductive extension of the following coalgebra.Now that we have set up the basic terminology of coalgebras, we can give semantics to guarded terms from Definition 5. The idea is that guarded terms guarantee that we can always compute with them so far that we find a function symbol in head position, see Lemma 8. This function symbol determines then the label and branching of a node in the tree generated by a guarded term. If the computation reaches a constant or a variable, then we stop creating the tree at the present branch. This idea is captured by the following lemma.

Lemma 22

There is a map \([\![-]\!]_1 :\varLambda ^{G,1}_{\varSigma }(\varGamma ) \rightarrow \varSigma ^{\infty }(\varGamma )\) that is unique with
  1. 1.

    if \(M \equiv N\), then \([\![M]\!]_1 = [\![N]\!]_1\), and

     
  2. 2.
     

Proof

(sketch). By Lemma 8, we can define a coalgebra on the quotient of guarded terms by convertibility Open image in new window with Open image in new window and \(c[M] = x\) if Open image in new window . This yields a homomorphism \(h :{\varLambda ^{G,1}_{\varSigma }(\varGamma )}/\!{\scriptstyle \equiv } \rightarrow \varSigma ^{\infty }(\varGamma )\) and we can define \([\![-]\!]_1 = h \mathbin {\circ }[-]\). The rest follows from uniqueness of h.

5.2 Interpretation of Basic Intuitionistic First-Order Formulae

In this section, we give an interpretation of the formulae in Definition 3, in which we restrict ourselves to guarded terms. This interpretation will be relative to models in the complete Herbrand universe. Since we later extend these models to Kripke models to be able to handle the later modality, we formulate these models already now in the language of fibrations [17, 46].

Definition 23

Let \(p :\mathbf {E}\rightarrow \mathbf {B}\) be a functor. Given an object \(I \in \mathbf {B}\), the fibre \(\mathbf {E}_I\) above I is the category of objects \(A \in \mathbf {E}\) with \(p(A) = I\) and morphisms \(f :A \rightarrow B\) with \(p(f) = \mathrm {id}_I\). The functor p is a (split) fibration if for every morphism \(u :I \rightarrow J\) in \(\mathbf {B}\) there is functor \(u^{*} :\mathbf {E}_J \rightarrow \mathbf {E}_I\), such that \(\mathrm {id}_I^{*} = \mathrm {Id}_{\mathbf {E}_I}\) and \((v \mathbin {\circ }u)^{*} = u^{*} \mathbin {\circ }v^{*}\). We call \(u^{*}\) the reindexing along u.

To give an interpretation of formulae, consider the following category \(\mathbf {Pred}\).
$$\begin{aligned} \mathbf{Pred}\,= \,\left\{ \begin{array}{ll} \mathrm{objects}:&{} \left( {X,P} \right) \,\,\mathrm{with}\,X \in \mathbf{Set}\,\,\mathrm{and}\,\,P \subseteq X\\ \mathrm{morphisms}:&{} f:\left( {X,P} \right) \rightarrow \left( {Y,Q} \right) \,\text {is a map}\,\,f:\,X \,\rightarrow \, Y\,\,\mathrm{with}\,\,f(P)\, \subseteq \, Q \end{array} \right. \end{aligned}$$
The functor \(\mathbb {P}:\mathbf {Pred}\rightarrow \mathbf {Set}\) with \(\mathbb {P}(X, P) = X\) and \(\mathbb {P}(f) = f\) is a split fibration, see [46], where the reindexing functor for \(f :X \rightarrow Y\) is given by taking preimages: \(f^{*}(Q) = f^{-1}(Q)\). Note that each fibre \(\mathbf {Pred}_X\) is isomorphic to the complete lattice of predicates over X ordered by set inclusion. Thus, we refer to this fibration as the predicate fibration.

Let us now expose the logical structure of the predicate fibration. This will allow us to conveniently interpret first-order formulae over this fibration, but it comes at the cost of having to introduce a good amount of category theoretical language. However, doing so will pay off in Sect. 5.4, where we will construct another fibration out of the predicate fibration. We can then use category theoretical results to show that this new fibration admits the same logical structure and allows the interpretation of the later modality.

The first notion we need is that of fibred products, coproducts and exponents, which will allow us to interpret conjunction, disjunction and implication.

Definition 24

A fibration \(p :\mathbf {E}\rightarrow \mathbf {B}\) has fibred finite products \((\mathbf {1}, \times )\), if each fibre \(\mathbf {E}_I\) has finite products \((\mathbf {1}_I, \times _I)\) and these are preserved by reindexing: for all \(f :I \rightarrow J\), we have \(f^{*}(\mathbf {1}_J) = \mathbf {1}_I\) and \(f^{*}(A \times _J B) = f^{*}(A) \times _I f^{*}(B)\). Fibred finite coproducts and exponents are defined analogously.

The fibration \(\mathbb {P}\) is a so-called first-order fibration, which allows us to interpret first-order logic, see [46, Def. 4.2.1].

Definition 25

A fibration \(p :\mathbf {E}\rightarrow \mathbf {B}\) is a first-order fibration if2
  • \(\mathbf {B}\) has finite products and the fibres of p are preorders;

  • p has fibred finite products \((\top , \wedge )\) and coproducts \((\bot , \vee )\) that distribute;

  • p has fibred exponents \(\rightarrow \); and

  • p has existential and universal quantifiers \(\exists _{I,J} \dashv \pi _{I,J}^{*} \dashv \forall _{I,J}\) for all projections \(\pi _{I,J} :I \times J \rightarrow I\).

A first-order \(\lambda \)-fibration is a first-order fibration with Cartesian closed base \(\mathbf {B}\).

The fibration \(\mathbb {P}:\mathbf {Pred}\rightarrow \mathbf {Set}\) is a first-order \(\lambda \)-fibration, as all its fibres are posets and \(\mathbf {Set}\) is Cartesian closed; \(\mathbb {P}\) has fibred finite products \((\top , \cap )\), given by \(\top _X = X\) and intersection; fibred distributive coproducts \((\emptyset , \cup )\); fibred exponents \(\mathrel {\Rightarrow }\), given by Open image in new window ; and universal and existential quantifiers given for \(P \in \mathbf {Pred}_{X \times Y}\) byThe purpose of first-order fibrations is to capture the essentials of first-order logic, while the \(\lambda \)-part takes care of higher-order features of the term language. In the following, we interpret types, contexts, guarded terms and formulae in the fibration \(\mathbb {P}:\mathbf {Pred}\rightarrow \mathbf {Set}\): We define for types \(\tau \) and context \(\varGamma \) sets Open image in new window and Open image in new window ; for guarded terms M with Open image in new window we define a map Open image in new window in \(\mathbf {Set}\); and for a formula \(\varGamma \Vdash \varphi \) we give a predicate Open image in new window .

The semantics of types and contexts are given inductively in the Cartesian closed category \(\mathbf {Set}\), where the base type \(\iota \) is interpreted as coterms, as follows.

We note that a coterm \(t \in \varSigma ^{\infty }(V)\) can be seen as a map \((\varSigma ^{\infty })^V \rightarrow \varSigma ^{\infty }\) by applying a substitution in \((\varSigma ^{\infty })^V\) to t: \(\sigma \mapsto t[\sigma ]\). In particular, the semantics of a guarded first-order term \(M \in \varLambda ^{G,1}_{\varSigma }(\varGamma )\) is equivalently a map Open image in new window . We can now extend this map inductively to Open image in new window for all guarded terms \(M \in \varLambda ^{G}_{\varSigma }(\varGamma )\) with Open image in new window by

Lemma 26

The mapping Open image in new window is a well-defined function from guarded terms to functions, such that Open image in new window implies Open image in new window .

Since \(\mathbb {P}:\mathbf {Pred}\rightarrow \mathbf {Set}\) is a first-order fibration, we can interpret inductively all logical connectives of the formulae from Definition 3 in this fibration. The only case that is missing is the base case of predicate symbols. Their interpretation will be given over a Herbrand model that is constructed as the largest fixed point of an operator over all predicate interpretations in the Herbrand base. Both the operator and the fixed point are the subjects of the following definition.

Definition 27

We let the set of interpretations \(\mathcal {I}\) be the powerset \(\mathcal {P}({\mathcal {B}^{\infty }})\) of the complete Herbrand base. For \(I \in \mathcal {I}\) and \(p \in \varPi \), we denote by \(I{p}\) the interpretation of p in I (the fibre of I above p)Given a set P of \(H^g\)-formulae, we define a monotone map Open image in new window bywhere \([\![-]\!]_1 [\theta ]\) is the extension of semantics and substitution from coterms to the Herbrand base by functoriality of Open image in new window . The (complete) Herbrand model Open image in new window of P is the largest fixed point of Open image in new window , which exists because \(\mathcal {I}\) is a complete lattice.
Given a formula \(\varphi \) with \(\varGamma \Vdash \varphi \) that contains only guarded terms, we define the semantics of \(\varphi \) in \(\mathbf {Pred}\) from an interpretation \(I \in \mathcal {I}\) inductively as follows.

Lemma 28

The mapping Open image in new window is a well-defined function from formulae to predicates, such that \(\varGamma \Vdash \varphi \) implies Open image in new window or, equivalently, Open image in new window .

This concludes the semantics of types, terms and formulae. We now turn to show that coinductive uniform proofs are sound for this interpretation.

5.3 Soundness of Coinductive Uniform Proofs for Herbrand Models

In this section, we give a direct proof of soundness for the coinductive uniform proof system from Sect. 3. Later, we will obtain another soundness result by combining the proof translation from Theorem 18 with the soundness of Open image in new window (Theorems 39 and 42). The purpose of giving a direct soundness proof for uniform proofs is that it allows the extraction of a coinduction invariant, see Lemma 32.

The main idea is as follows. Given a formula \(\varphi \) and a uniform proof \(\pi \) for Open image in new window , we construct an interpretation \(I \in \mathcal {I}\) that validates \(\varphi \), i.e. Open image in new window , and that is contained in the complete Herbrand model Open image in new window . Combining these two facts, we obtain that Open image in new window , and thus the soundness of uniform proofs.

To show that the constructed interpretation I is contained in Open image in new window , we use the usual coinduction proof principle, as it is given in the following definition.

Definition 29

An invariant for \(K \in \mathcal {I}\) is a set \(I \in \mathcal {I}\), such that \(K \subseteq I\) and I is a Open image in new window -invariant, that is, Open image in new window . If K has an invariant, then Open image in new window .

Thus, our goal is now to construct an interpretation together with an invariant. This invariant will essentially collect and iterate all the substitutions that appear in a proof. For this we need the ability to compose substitutions of coterms, which we derive from the monad [5] \((\varSigma ^{\infty }, \eta , \mu )\) with \(\mu :\varSigma ^{\infty }\varSigma ^{\infty } \Rightarrow \varSigma ^{\infty }\).

Definition 30

A (Kleisli-)substitution \(\theta \) from V to W, written Open image in new window , is map \(V \rightarrow \varSigma ^{\infty }(W)\). Composition of Open image in new window and Open image in new window is given by
$$\begin{aligned} \theta \circledcirc \delta = U \xrightarrow {\delta } \varSigma ^{\infty }(V) \xrightarrow {\varSigma ^{\infty }(\theta )} \varSigma ^{\infty }(\varSigma ^{\infty }(W)) \xrightarrow {\mu _{W}} \varSigma ^{\infty }(W). \end{aligned}$$

The notions in the following definition will allow us to easily organise and iterate the substitutions that occur in a uniform proof.

Definition 31

Let S be a set with Open image in new window for some \(n \in \mathbb {N}\). We call the set \(S^{*}\) of lists over S the set of substitution identifiers. Suppose that we have substitutions Open image in new window and Open image in new window for each \(k \in S\). Then we can define a map Open image in new window , which turns each substitution identifier into a substitution, by iteration from the right:
$$\begin{aligned} \varTheta (\varepsilon ) = \theta _0 \quad \text {and} \quad \varTheta (w : k) = \varTheta (w) \circledcirc \theta _k \end{aligned}$$
After introducing these notations, we can give the outline of the soundness proof for uniform proofs relative to the complete Herbrand model. Given an \(H^g\)-formula Open image in new window , we note that a uniform proof \(\pi \) for Open image in new window starts with
where the eigenvariables in Open image in new window are all distinct. Let \(\varSigma ^c\) be the signature Open image in new window and C the set of variables in Open image in new window . Suppose the following is a valid subtree of \(\pi \).
This proof tree gives rise to a substitution Open image in new window by Open image in new window , which we call an agent of \(\pi \). We let \(D \subseteq \mathrm {At}_1^g\) be the set of atoms that are proven in \(\pi \):From the agents and atoms in \(\pi \) we extract an invariant for the goal formula.

Lemma 32

Suppose that \(\varphi \) is an \(H^g\)-formula of the form Open image in new window and that there is a proof \(\pi \) for Open image in new window . Let D be the proven atoms in \(\pi \) and \(\theta _0, \cdots , \theta _s\) be the agents of \(\pi \). Define Open image in new window and suppose further that \(I_1\) is an invariant for Open image in new window . If we put
$$\begin{aligned} {I_2} = \bigcup \limits _{w \in {S^{*}}} {D\left[ {\varTheta \left( w \right) } \right] } \end{aligned}$$
then \(I_1 \cup I_2\) is an invariant for Open image in new window .

Once we have Lemma 32 the following soundness theorem is easily proven.

Theorem 33

If \(\varphi \) is an \(H^g\)-formula and Open image in new window , then Open image in new window .

Finally, we show that extending logic programs with coinductively proven lemmas is sound. This follows easily by coinduction.

Theorem 34

Let \(\varphi \) be an \(H^g\)-formula of the shape Open image in new window , such that, for all substitutions \(\theta \) if Open image in new window , then Open image in new window . Then Open image in new window implies Open image in new window , that is, Open image in new window is a conservative extension of P with respect to the Herbrand model.

As a corollary we obtain that, if there is a proof for Open image in new window , then a proof for Open image in new window is sound with respect to Open image in new window . Indeed, by Theorem 34 we have that Open image in new window and by Theorem 33 that Open image in new window is sound with respect to Open image in new window . Thus, the proof of Open image in new window is also sound with respect to Open image in new window . We use this property implicitly in our running examples, and refer the reader to [15, 49] for proofs, further examples and discussion.

5.4 Soundness of Open image in new window over Herbrand Models

In this section, we demonstrate how the logic Open image in new window can be interpreted over Herbrand models. Recall that we obtained a fixed point model from the monotone map Open image in new window on interpretations. In what follows, it is crucial that we construct the greatest fixed point of Open image in new window by iteration, c.f. [6, 32, 77]: Let Open image in new window be the class of all ordinals equipped with their (well-founded) order. We denote by Open image in new window the class of ordinals with their reversed order and define a monotone function Open image in new window , where we write the argument ordinal in the subscript, byNote that this definition is well-defined because < is well-founded and because Open image in new window is monotone, see [14]. Since \(\mathcal {I}\) is a complete lattice, there is an ordinal \(\alpha \) such that Open image in new window , at which point Open image in new window is the largest fixed point Open image in new window of Open image in new window . In what follows, we will utilise this construction to give semantics to Open image in new window .
The fibration \(\mathbb {P}:\mathbf {Pred}\rightarrow \mathbf {Set}\) gives rise to another fibration as follows. We let \(\overline{\mathbf {Pred}}\) be the category of functors (monotone maps) with fixed predicate domain:The fibration \(\overline{\mathbb {P}} :\mathbf {Pred}\rightarrow \mathbf {Set}\) is defined by evaluation at any ordinal (here 0), i.e. by \(\overline{\mathbb {P}}(u) = \mathbb {P}(u(0))\) and \(\overline{\mathbb {P}}(f) = (\mathbb {P}f)_0\), and reindexing along \(f :X \rightarrow Y\) by applying the reindexing of \(\mathbb {P}\) point-wise, i.e. by \(f^{\#}(u)_\alpha = f^{*}(u_\alpha )\).

Note that there is a (full) embedding \(K :\mathbf {Pred}\rightarrow \overline{\mathbf {Pred}}\) that is given by \(K(X, P) = (X, \overline{P})\) with \(\overline{P}_\alpha = P\). One can show [14] that \(\overline{\mathbb {P}}\) is again a first-order fibration and that it models the later modality, as in the following theorem.

Theorem 35

The fibration \(\overline{\mathbb {P}}\) is a first-order fibration. If necessary, we denote the first-order connectives by \(\dot{\top }\), \(\mathrel {\dot{\wedge }}\) etc. to distinguish them from those in \(\mathbf {Pred}\). Otherwise, we drop the dots. Finite (co)products and quantifiers are given point-wise, while for \(X \in \mathbf {Set}\) and \(u,v \in \overline{\mathbf {Pred}}_X\) exponents are given by
$$\begin{aligned} (v \mathrel {\dot{\Rightarrow }}u)_{\alpha } = \bigcap \nolimits _{\beta \le \alpha } (v_\beta \mathrel {\Rightarrow }u_\beta ). \end{aligned}$$
There is a fibred functor Open image in new window with Open image in new window given on objects byand a natural transformation Open image in new window from the identity functor to Open image in new window . The functor Open image in new window preserves reindexing, products, exponents and universal quantification: Open image in new window , Open image in new window , Open image in new window , Open image in new window . Finally, for all \(X \in \mathbf {Set}\) and \(u \in \overline{\mathbf {Pred}}_X\), there is Open image in new window in \(\overline{\mathbf {Pred}}_X\).
Using the above theorem, we can extend the interpretation of formulae to Open image in new window as follows. Let Open image in new window be a descending sequence of interpretations. As before, we define the restriction of u to a predicate symbol \(p \in \varPi \) by Open image in new window . The semantics of formulae in Open image in new window as objects in \(\overline{\mathbf {Pred}}\) is given by the following iterative definition.The following lemma is the analogue of Lemma 28 for the interpretation of formulae without the later modality.

Lemma 36

The mapping Open image in new window is a well-defined map from formulae in Open image in new window to sequences of predicates, such that \(\varGamma \Vdash \varphi \) implies Open image in new window .

Lemma 37

All rules of Open image in new window are sound with respect to the interpretation Open image in new window of formulae in \(\overline{\mathbf {Pred}}\), that is, if Open image in new window , then Open image in new window . In particular, Open image in new window implies Open image in new window .

The following lemma shows that the guarding of a set of formulae is valid in the chain model that they generate.

Lemma 38

If \(\varphi \) is an H-formula in P, then Open image in new window .

Combining this with soundness from Lemma 37, we obtain that provability in Open image in new window relative to a logic program P is sound for the model of P.

Theorem 39

For all logic programs P, if Open image in new window then Open image in new window .

The final result of this section is to show that the descending chain model, which we used to interpret formulae of Open image in new window , is sound and complete for the fixed point model, which we used to interpret the formulae of coinductive uniform proofs. This will be proved in Theorem 42 below. The easiest way to prove this result is by establishing a functor \(\overline{\mathbf {Pred}} \rightarrow \mathbf {Pred}\) that maps the chain Open image in new window to the model Open image in new window , and that preserves and reflects truth of first-order formulae (Proposition 41). We will phrase the preservation of truth of first-order formulae by a functor by appealing to the following notion of fibrations maps, cf. [46, Def. 4.3.1].

Definition 40

Let \(p :\mathbf {E}\rightarrow \mathbf {B}\) and \(q :\mathbf {D} \rightarrow \mathbf {A}\) be fibrations. A fibration map \(p \rightarrow q\) is a pair \((F :\mathbf {E}\rightarrow \mathbf {D}, G :\mathbf {B}\rightarrow \mathbf {A})\) of functors, s.t. \(q \mathbin {\circ }F = G \mathbin {\circ }p\) and F preserves Cartesian morphisms: if \(f :X \rightarrow Y\) in \(\mathbf {E}\) is Cartesian over p(f), then F(f) is Cartesian over G(p(f)). (FG) is a map of first-order (\(\lambda \) -)fibrations, if p and q are first-order (\(\lambda \)-)fibrations, and F and G preserve this structure.

Let us now construct a first-order \(\lambda \)-fibration map \(\overline{\mathbf {Pred}} \rightarrow \mathbf {Pred}\). We note that since every fibre of the predicate fibration is a complete lattice, for every chain \(u \in \overline{\mathbf {Pred}}_X\) there exists an ordinal \(\alpha \) at which u stabilises. This means that there is a limit \(\lim u\) of u in \(\mathbf {Pred}_X\), which is the largest subset of X, such that \(\forall \alpha . \, \lim u \subseteq u_\alpha \). This allows us to define a map Open image in new window byIn the following proposition, we show that L gives us the ability to express first-order properties of limits equivalently through their approximating chains. This, in turn, provides soundness and completeness for the interpretation of the logic Open image in new window over descending chains with respect to the largest Herbrand model.

Proposition 41

\(L :\overline{\mathbf {Pred}} \rightarrow \mathbf {Pred}\), as defined above, is a map of first-order fibrations. Furthermore, L is right-adjoint to the embedding \(K :\mathbf {Pred}\rightarrow \overline{\mathbf {Pred}}\). Finally, for each \(p \in \varPi \) and \(u \in \overline{\mathbf {Pred}}_{\mathcal {B}^{\infty }}\), we have Open image in new window .

We get from Proposition 41 soundness and completeness of Open image in new window for Herbrand models. More precisely, if \(\varphi \) is a formula of plain first-order logic ( Open image in new window -free), then its interpretation in the coinductive Herbrand model is true if and only if its interpretation over the chain approximation of the Herbrand model is true.

Theorem 42

If \(\varphi \) is Open image in new window -free (Definition 3) then Open image in new window if and only if Open image in new window .

Proof

(sketch). First, one shows for all Open image in new window -free formulae \(\varphi \) that Open image in new window by induction on \(\varphi \) and using Proposition 41. Using this identity and \(K \dashv L\), the result is then obtained from the following adjoint correspondence.

6 Conclusion, Related Work and the Future

In this paper, we provided a comprehensive theory of resolution in coinductive Horn-clause theories and coinductive logic programs. This theory comprises of a uniform proof system that features a form of guarded recursion and that provides operational semantics for proofs of coinductive predicates. Further, we showed how to translate proofs in this system into proofs for an extension of intuitionistic FOL with guarded recursion, and we provided sound semantics for both proof systems in terms of coinductive Herbrand models. The Herbrand models and semantics were thereby presented in a modern style that utilises coalgebras and fibrations to provide a conceptual view on the semantics.

Related Work. It may be surprising that automated proof search for coinductive predicates in first-order logic does not have a coherent and comprehensive theory, even after three decades [3, 60], despite all the attention that it received as programming [2, 29, 42, 44] and proof [33, 35, 39, 40, 45, 59, 64, 65, 66, 67] method. The work that comes close to algorithmic proof search is the system CIRC [63], but it cannot handle general coinductive predicates and corecursive programming. Inductive and coinductive data types are also being added to SMT solvers [24, 62]. However, both CIRC and SMT solving are inherently based on classical logic and are therefore not suited to situations where proof objects are relevant, like programming, type class inference or (dependent) type theory. Moreover, the proposed solutions, just like those in [41, 69] can only deal with regular data, while our approach also works for irregular data, as we saw in the \(\mathbf {from}\)-example.

This paper subsumes Haskell type class inference [37, 51] and exposes that the inference presented in those papers corresponds to coinductive proofs in \(\textit{co-fohc}\) and \(\textit{co-hohh}\). Given that the proof systems proposed in this paper are constructive and that uniform proofs provide proofs (type inhabitants) in normal form, we could give a propositions-as-types interpretation to all eight coinductive uniform proof systems. This was done for \(\textit{co-fohc}\) and \(\textit{co-hohh}\) in [37], but we leave the remaining cube from the introduction for future work.

Future Work. There are several directions that we wish to pursue in the future. First, we know that CUP is incomplete for the presented models, as it is intuitionistic and it lacks an admissible cut rule. The first can be solved by moving to Kripke/Beth-models, as done by Clouston and Goré [30] for the propositional part of Open image in new window . However, the admissible cut rule is more delicate. To obtain such a rule one has to be able to prove several propositions simultaneously by coinduction, as discussed at the end of Sect. 4. In general, completeness of recursive proof systems depends largely on the theory they are applied to, see [70] and [18]. However, techniques from cyclic proof systems [27, 68] may help. We also aim to extend our ideas to other situations like higher-order Horn clauses [28, 43] and interactive proof assistants [7, 10, 23, 31], typed logic programming, and logic programming that mix inductive and coinductive predicates.

Footnotes

  1. 1.

    We follow the standard terminology of [74] and say that two formulae F and G form a cycle if \(F = G\), and a loop if \(F[\theta ] = G[\theta ]\) for some (possibly circular) unifier \(\theta \).

  2. 2.

    Technically, the quantifiers should also fulfil the Beck-Chevalley and Frobenius conditions, and the fibration should admit equality. Since these are fulfilled in all our models and we do not need equality, we will not discuss them here.

Notes

Acknowledgements

We would like to thank Damien Pous and the anonymous reviewers for their valuable feedback.

References

  1. 1.
    Abbott, M., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. TCS 342(1), 3–27 (2005).  https://doi.org/10.1016/j.tcs.2005.06.002MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: POPL 2013, pp. 27–38 (2013).  https://doi.org/10.1145/2429069.2429075
  3. 3.
    Aczel, P.: Non-well-founded sets. Center for the Study of Language and Information, Stanford University (1988)Google Scholar
  4. 4.
    Aczel, P.: Algebras and coalgebras. In: Backhouse, R., Crole, R., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297, pp. 79–88. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-47797-7_3CrossRefGoogle Scholar
  5. 5.
    Aczel, P., Adámek, J., Milius, S., Velebil, J.: Infinite trees and completely iterative theories: a coalgebraic view. TCS 300(1–3), 1–45 (2003).  https://doi.org/10.1016/S0304-3975(02)00728-4MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Adámek, J.: On final coalgebras of continuous functors. Theor. Comput. Sci. 294(1/2), 3–29 (2003).  https://doi.org/10.1016/S0304-3975(01)00240-7MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    P.L. group on Agda: Agda Documentation. Technical report, Chalmers and Gothenburg University (2015). http://wiki.portal.chalmers.se/agda/, version 2.4.2.5
  8. 8.
    Appel, A.W., Melliès, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL, pp. 109–122. ACM (2007).  https://doi.org/10.1145/1190216.1190235
  9. 9.
    Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: ICFP, pp. 197–208. ACM (2013).  https://doi.org/10.1145/2500365.2500597
  10. 10.
    Baelde, D., et al.: Abella: a system for reasoning about relational specifications. J. Formaliz. Reason. 7(2), 1–89 (2014).  https://doi.org/10.6092/issn.1972-5787/4650MathSciNetCrossRefGoogle Scholar
  11. 11.
    Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press, Cambridge (2013)CrossRefGoogle Scholar
  12. 12.
    Barr, M., Wells, C.: Category Theory for Computing Science. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Upper Saddle River (1995). http://www.tac.mta.ca/tac/reprints/articles/22/tr22abs.htmlzbMATHGoogle Scholar
  13. 13.
    Basold, H.: Mixed inductive-coinductive reasoning: types, programs and logic. Ph.D. thesis, Radboud University Nijmegen (2018). http://hdl.handle.net/2066/190323
  14. 14.
    Basold, H.: Breaking the Loop: Recursive Proofs for Coinductive Predicates in Fibrations. ArXiv e-prints, February 2018. https://arxiv.org/abs/1802.07143
  15. 15.
    Basold, H., Komendantskaya, E., Li, Y.: Coinduction in uniform: foundations for corecursive proof search with horn clauses. Extended version of this paper. CoRR abs/1811.07644 (2018). http://arxiv.org/abs/1811.07644
  16. 16.
    Beklemishev, L.D.: Parameter free induction and provably total computable functions. TCS 224(1–2), 13–33 (1999).  https://doi.org/10.1016/S0304-3975(98)00305-3MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Bénabou, J.: Fibered categories and the foundations of naive category theory. J. Symb. Logic 50(1), 10–37 (1985).  https://doi.org/10.2307/2273784MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Berardi, S., Tatsuta, M.: Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 301–317. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54458-7_18CrossRefzbMATHGoogle Scholar
  19. 19.
    Birkedal, L., Møgelberg, R.E.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS, pp. 213–222. IEEE Computer Society (2013).  https://doi.org/10.1109/LICS.2013.27
  20. 20.
    Birkedal, L., Møgelberg, R.E., Schwinghammer, J., Støvring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. In: Proceedings of LICS 2011, pp. 55–64. IEEE Computer Society (2011).  https://doi.org/10.1109/LICS.2011.16
  21. 21.
    Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 20–35. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49630-5_2. https://arxiv.org/abs/1601.01586CrossRefGoogle Scholar
  22. 22.
    Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23534-9_2CrossRefGoogle Scholar
  23. 23.
    Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for Higher-Order Logic. In: LICS 2017, pp. 1–12. IEEE Computer Society (2017).  https://doi.org/10.1109/LICS.2017.8005071
  24. 24.
    Blanchette, J.C., Peltier, N., Robillard, S.: Superposition with datatypes and codatatypes. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 370–387. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-94205-6_25CrossRefGoogle Scholar
  25. 25.
    Borceux, F.: Handbook of Categorical Algebra. Basic Category Theory, vol. 1. Cambridge University Press, Cambridge (2008)zbMATHGoogle Scholar
  26. 26.
    Bottu, G., Karachalias, G., Schrijvers, T., Oliveira, B.C.D.S., Wadler, P.: Quantified class constraints. In: Haskell Symposium, pp. 148–161. ACM (2017).  https://doi.org/10.1145/3122955.3122967
  27. 27.
    Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177–1216 (2011).  https://doi.org/10.1093/logcom/exq052MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Burn, T.C., Ong, C.L., Ramsay, S.J.: Higher-order constrained horn clauses for verification. PACMPL 2(POPL), 11:1–11:28 (2018).  https://doi.org/10.1145/3158099CrossRefGoogle Scholar
  29. 29.
    Capretta, V.: General Recursion via Coinductive Types. Log. Methods Comput. Sci. 1(2), July 2005.  https://doi.org/10.2168/LMCS-1(2:1)2005
  30. 30.
    Clouston, R., Goré, R.: Sequent calculus in the topos of trees. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 133–147. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46678-0_9CrossRefzbMATHGoogle Scholar
  31. 31.
    Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58085-9_72CrossRefGoogle Scholar
  32. 32.
    Cousot, P., Cousot, R.: Constructive versions of Tarski’s fixed point theorems. Pac. J. Math. 82(1), 43–57 (1979). http://projecteuclid.org/euclid.pjm/1102785059MathSciNetCrossRefGoogle Scholar
  33. 33.
    Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time \({\mu }\)-calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273–284. Springer, Heidelberg (2006).  https://doi.org/10.1007/11944836_26CrossRefGoogle Scholar
  34. 34.
    van Emden, M., Kowalski, R.: The semantics of predicate logic as a programming language. J. Assoc. Comput. Mach. 23, 733–742 (1976).  https://doi.org/10.1145/321978.321991MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Endrullis, J., Hansen, H.H., Hendriks, D., Polonsky, A., Silva, A.: A coinductive framework for infinitary rewriting and equational reasoning. In: RTA 2015, pp. 143–159 (2015).  https://doi.org/10.4230/LIPIcs.RTA.2015.143
  36. 36.
    Farka, F., Komendantskaya, E., Hammond, K.: Coinductive soundness of corecursive type class resolution. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 311–327. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63139-4_18CrossRefGoogle Scholar
  37. 37.
    Fu, P., Komendantskaya, E., Schrijvers, T., Pond, A.: Proof relevant corecursive resolution. In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 126–143. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-29604-3_9CrossRefGoogle Scholar
  38. 38.
    Gambino, N., Kock, J.: Polynomial functors and polynomial monads. Math. Proc. Cambridge Phil. Soc. 154(1), 153–192 (2013).  https://doi.org/10.1017/S0305004112000394MathSciNetCrossRefzbMATHGoogle Scholar
  39. 39.
    Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3–31 (2017).  https://doi.org/10.1007/s10817-016-9388-yMathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    Giménez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 397–408. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0055070CrossRefGoogle Scholar
  41. 41.
    Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive logic programming and its applications. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 27–44. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74610-2_4CrossRefzbMATHGoogle Scholar
  42. 42.
    Hagino, T.: A typed lambda calculus with categorical type constructors. In: Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 283, pp. 140–157. Springer, Heidelberg (1987).  https://doi.org/10.1007/3-540-18508-9_24CrossRefGoogle Scholar
  43. 43.
    Hashimoto, K., Unno, H.: Refinement type inference via horn constraint optimization. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 199–216. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-48288-9_12CrossRefGoogle Scholar
  44. 44.
    Howard, B.T.: Inductive, coinductive, and pointed types. In: Harper, R., Wexelblat, R.L. (eds.) Proceedings of ICFP 1996, pp. 102–109. ACM (1996).  https://doi.org/10.1145/232627.232640
  45. 45.
    Hur, C.K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: Proceedings of POPL 2013, pp. 193–206. ACM (2013).  https://doi.org/10.1145/2429069.2429093
  46. 46.
    Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Amsterdam (1999)zbMATHGoogle Scholar
  47. 47.
    Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press, Cambridge (2016).  https://doi.org/10.1017/CBO9781316823187. http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdfCrossRefzbMATHGoogle Scholar
  48. 48.
    Komendantskaya, E., Li, Y.: Productive corecursion in logic programming. J. TPLP (ICLP 2017 post-proc.) 17(5–6), 906–923 (2017).  https://doi.org/10.1017/S147106841700028XMathSciNetCrossRefzbMATHGoogle Scholar
  49. 49.
    Komendantskaya, E., Li, Y.: Towards coinductive theory exploration in horn clause logic: Position paper. In: Kahsai, T., Vidal, G. (eds.) Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2018, Oxford, UK, 13th July 2018, vol. 278, pp. 27–33 (2018).  https://doi.org/10.4204/EPTCS.278.5
  50. 50.
    Lambek, J., Scott, P.J.: Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge (1988)zbMATHGoogle Scholar
  51. 51.
    Lämmel, R., Peyton Jones, S.L.: Scrap your boilerplate with class: extensible generic functions. In: ICFP 2005, pp. 204–215. ACM (2005).  https://doi.org/10.1145/1086365.1086391
  52. 52.
    Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987).  https://doi.org/10.1007/978-3-642-83189-8CrossRefzbMATHGoogle Scholar
  53. 53.
    Miller, D., Nadathur, G.: Programming with Higher-order logic. Cambridge University Press, Cambridge (2012)CrossRefGoogle Scholar
  54. 54.
    Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51(1–2), 125–157 (1991).  https://doi.org/10.1016/0168-0072(91)90068-WMathSciNetCrossRefzbMATHGoogle Scholar
  55. 55.
    Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348–375 (1978).  https://doi.org/10.1016/0022-0000(78)90014-4MathSciNetCrossRefzbMATHGoogle Scholar
  56. 56.
    Møgelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: CSL-LICS, pp. 71:1–71:10. ACM (2014).  https://doi.org/10.1145/2603088.2603132
  57. 57.
    Nadathur, G., Mitchell, D.J.: System description: Teyjus—a compiler and abstract machine based implementation of \(\lambda \)Prolog. CADE-16. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48660-7_25CrossRefGoogle Scholar
  58. 58.
    Nakano, H.: A modality for recursion. In: LICS, pp. 255–266. IEEE Computer Society (2000).  https://doi.org/10.1109/LICS.2000.855774
  59. 59.
    Niwinski, D., Walukiewicz, I.: Games for the \(\mu \)-Calculus. TCS 163(1&2), 99–116 (1996).  https://doi.org/10.1016/0304-3975(95)00136-0MathSciNetCrossRefzbMATHGoogle Scholar
  60. 60.
    Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981).  https://doi.org/10.1007/BFb0017309CrossRefGoogle Scholar
  61. 61.
    Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977).  https://doi.org/10.1016/0304-3975(77)90044-5MathSciNetCrossRefzbMATHGoogle Scholar
  62. 62.
    Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80–98. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46081-8_5CrossRefGoogle Scholar
  63. 63.
    Roşu, G., Lucanu, D.: Circular coinduction: a proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 127–144. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03741-2_10CrossRefGoogle Scholar
  64. 64.
    Rutten, J.: Universal coalgebra: a theory of systems. TCS 249(1), 3–80 (2000).  https://doi.org/10.1016/S0304-3975(00)00056-6MathSciNetCrossRefzbMATHGoogle Scholar
  65. 65.
    Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)CrossRefGoogle Scholar
  66. 66.
    Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 357–371. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45931-6_25CrossRefzbMATHGoogle Scholar
  67. 67.
    Santocanale, L.: \(\mu \)-bicomplete categories and parity games. RAIRO - ITA 36(2), 195–227 (2002).  https://doi.org/10.1051/ita:2002010MathSciNetCrossRefzbMATHGoogle Scholar
  68. 68.
    Shamkanov, D.S.: Circular proofs for the Gödel-Löb provability logic. Math. Notes 96(3), 575–585 (2014).  https://doi.org/10.1134/S0001434614090326MathSciNetCrossRefzbMATHGoogle Scholar
  69. 69.
    Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: extending logic programming with coinduction. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 472–483. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73420-8_42CrossRefzbMATHGoogle Scholar
  70. 70.
    Simpson, A.: Cyclic arithmetic is equivalent to Peano arithmetic. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 283–300. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54458-7_17CrossRefGoogle Scholar
  71. 71.
    Smoryński, C.: Self-Reference and Modal Logic. Universitext. Springer, New York (1985).  https://doi.org/10.1007/978-1-4613-8601-8CrossRefzbMATHGoogle Scholar
  72. 72.
    Solovay, R.M.: Provability interpretations of modal logic. Israel J. Math. 25(3), 287–304 (1976).  https://doi.org/10.1007/BF02757006MathSciNetCrossRefzbMATHGoogle Scholar
  73. 73.
    Sulzmann, M., Stuckey, P.J.: HM(X) type inference is CLP(X) solving. J. Funct. Program. 18(2), 251–283 (2008).  https://doi.org/10.1017/S0956796807006569MathSciNetCrossRefzbMATHGoogle Scholar
  74. 74.
    Terese: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)Google Scholar
  75. 75.
    Turner, D.A.: Elementary strong functional programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022, pp. 1–13. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60675-0_35CrossRefGoogle Scholar
  76. 76.
    van den Berg, B., de Marchi, F.: Non-well-founded trees in categories. Ann. Pure Appl. Logic 146(1), 40–59 (2007).  https://doi.org/10.1016/j.apal.2006.12.001MathSciNetCrossRefzbMATHGoogle Scholar
  77. 77.
    Worrell, J.: On the final sequence of a finitary set functor. Theor. Comput. Sci. 338(1–3), 184–199 (2005).  https://doi.org/10.1016/j.tcs.2004.12.009MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© The Author(s) 2019

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.CNRS, ENS LyonLyonFrance
  2. 2.Heriot-Watt UniversityEdinburghUK

Personalised recommendations