{'fraction_non_alphanumeric': 0.048819554151307704, 'fraction_numerical': 0.02119536598209584, 'mean_word_length': 4.5635986328125, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 16, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Coinduction Plain and Simple

Coinduction refers to both a technique for the definition of infinite streams, so-called codata, and a technique for proving the equality of coinductively specified codata. This article first reviews coinduction in declarative programming. Second, it reviews and slightly extends the formalism commonly used for specifying codata. Third, it generalizes the coinduction proof principle, which has been originally specified for the equality predicate only, to other predicates. This generalization makes the coinduction proof principle more intuitive and stresses its closeness with structural induction. The article finally suggests in its conclusion extensions of functional and logic programming with limited and decidable forms of the generalized coinduction proof principle.

A data stream, short stream, is a possibly never ending sequence of data. A stream is observed when its data result from observations or measurements of natural or artificial systems. An observed data stream might for example convey temperatures, the reproduction rates of a disease, or energy consumption or traffic volumes. A stream is constructed when its data are synthetic. Constructed streams are useful as encoded models of observed streams. Using streams, an early detection of critical situations can be specified as the continuous comparison of the data of an observed stream with that of a constructed stream modelling some behavior. Constructed streams are finitely defined from non-stream data and operations on such data.
Thus, two disjoint data types are considered in the following: Non-stream data the type of which is called data and stream data the type of which is called codata. Constructed streams, or codata, are finitely defined for, otherwise, they could not be used in programming. Codata express repetitions by recursion. As a consequence, recursive functions like the Fibonacci function can be expressed as codata. The specification of recursive functions as codata is interesting in its own right, independently of stream-related applications, because recursive codata yield iterative computation processes like tail recursive functions do but without the recourse to accumulators.
Streams are related to processes. An observation process operating on an observed stream might be unpredictable, or only partly predictable, while a process operating on a constructed stream, even though it might never end, can be given a finite definition derived from that of the constructed stream it refers to. Coinduction in declarative programming has been used for the specification of both constructed streams and processes operating on constructed streams.
This article first reviews coinduction in declarative programming. Second, it reviews and slightly extends the formalism commonly used for specifying codata. Third, it generalizes the coinduction proof principle to other predicates than equality. The article finally suggests in its conclusion extensions of functional and logic programming with limited and decidable forms of the generalized coinduction proof principle.

Coinduction in Declarative Programming
Coinduction was introduced in 1971 by Robin Milner in an investigation of the correctness of terminating or non-terminating imperative programs (Milner 1971). More precisely, the article (Milner 1971) introduced simulation relations and a precursor of the coinductive proof principle consisting in exhibiting finitely many pairs of related states and verifying that a simulation relation holds of each pair. David Park defined in 1981 bisimilarity as a greatest fixpoint, derived from fixpoint theory the bisimulation proof method (Park 1981) which is now also called coinductive proof principle. Bisimulation and the coinductive proof principle soon became cornerstones of process algebra (Hoare 1978;Fokkink 2007) and of the theory of communicating concurrent processes (Milner 1980). Davide Sangiorgi gives in (Sangiorgi 2009) an extensive account of the origins of coinduction, bisimulation and of related precursor concepts and methods in philosophical and mathematical logic, mathematics and computer science which, however, does not address coinduction in declarative programming and does not mention inductionless induction (Comon 2006).
Coinductive definitions, or codata, have been introduced in 1982 by Alain Colmerauer in logic programming under the name of rational trees (Colmerauer 1982), "tree" meaning finite or infinite term. A rational tree is a finite or infinite tree the set of subtrees of which is finite. The name "rational tree" which, puzzlingly, is not explained in (Colmerauer 1982;Colmerauer 1984), was chosen in reference to the fact that a real number is a rational number if and only if its decimal expansion is finite or repeating (Colmerauer 1988). The name "rational tree" appropriately stresses that, by Georg Cantor's diagonal argument (Cantor 1891), the set of (rational and non-rational) trees over a finite or denumerable alphabet is not denumerable 1 while the set of rational trees of course is denumerable. Following Courcelle (Courcelle 1983), rational trees are also named regular trees. In the 1980s rational trees were easily expressed in Prolog because, for efficiency reasons at a time processors were slow, Prolog did not perform the occurs-check during unification: An infinite list of 1s could for example be finitely expressed as X = [1|X] or, redundantly, as X = [1,1,1|X] and an infinite list of alternating 0s and 1s as X = [0,1|X]. Colmerauer systematized this observation and designed a variant of Prolog, Prolog II (Colmerauer 1984;van Emden and Lloyd 1984), which supported rational trees. Michael Maher gave in 1988 in (Maher 1988) an axiomatization of the algebras of rational trees. Unification algorithms for rational trees were proposed in (Mukai 1983;Jaffar 1984;Martelli and Rossi 1984). A meta-interpreter for a logic programming language supporting rational (or regular) trees (or terms) is described in (Ancona 2013). 2 Coinductive definitions in logic programming are possible not only with rational trees defined using unification without occurs-check, but also through non-terminating SLD derivations based on unification with occurs-check. This approach has been first investigated in 1983 by Nait Abdallah in (Abdallah 1983), further investigated in (Abdallah 1984;van Emden and Abdallah 1985;Palamidessi et al. 1985) 3 and popularized in 1987 by John Lloyd with the chapter on perpetual processes of the second edition of his Foundations of Logic Programming (Lloyd 1987). Each stage of a non-terminating SLD derivation like that resulting from the evaluation of ?-p(Y). against the clause p(X) :-p(f(X)). is seen as a finite approximation of an atom containing an infinite term f(f(f(...))). Nait Abdallah formalized such infinite terms as follows.
The Herbrand universe H is first equipped with a metric: where a n (t) is the "cut at depth n" of a term t. Thus, inf{n|a n (t 1 ) = a n (t 2 )} is the smallest depth at which t 1 and t 2 differ. Using this metric, Cauchy sequences of elements of H are defined, 4 the standard equivalence relation on Cauchy sequences is considered, 5 and the complete Herbrand universe H is defined as the set of equivalence classes of Cauchy sequences of elements of H. Thus, H ⊂ H. 6 It is then observed that, by a result of (Mycielski and Taylor 1976), H is compact 7 if its terms are defined from finitely many symbols. This is the case of the ground (or closed) terms of H because programs are finite. Thus, an infinite sequence of elements of H like for example f n (a) has a limit in H which is denoted f ( f (. . .)) or f (ω).
The complete Herbrand base B is defined as the set of ground atoms built from terms in the complete Herbrand universe H, an immediate consequence operator T ′ is defined in reference to the complete Herbrand base B in the same manner as the standard immediate consequence operator T is defined in reference to the Herbrand base B (van Emden and Kowalsi 1976). The greatest fixpoint semantics of a definite (that is, negation-free) logic program is defined as the greatest fixpoint of T ′ for that program. The greatest fixpoint semantics of logic programs is extended 2 The article does not clarify in which cases unification is performed with, respectively without, occurs-checks. 3 The "completion of a program" mentioned in (van Emden and Abdallah 1985) is Clark's completion semantics of negation in logic programming (Clark 1978). Thus, it is not related to the metric-based completion of the Herbrand universe introduced in (Abdallah 1983). 4 A Cauchy sequence is such that the distance between two successive elements tends to zero when the rank tends to infinity. 5 Two Cauchy sequences are equivalent if the difference between their elements of same ranks tends to zero when the rank tends to infinity. 6 Like Q ⊂ Q = R. 7 The compactness of H means that every Cauchy sequence of elements of H has a limit in H.
Some approaches to coinduction in logic programming make use of ancestor subsumption (Socher-Ambrosius 1992), a technique for avoiding redundant derivations in resolution theorem proving: If a resolvent R is subsumed (without occurs-check) by one of its ancestors A, then further derivations from R can be avoided without compromising completeness. Indeed, if R is subsumed (without occurs-check) by A, then every derivation from R is also possible from A and therefore redundant.
In the 1980s, as coinductive definitions began to be considered in logic programming, it was folklore knowledge in the community that ancestor subsumption (without occurs-check) can be used for preventing redundant non-terminating SLD derivations ( ?-X = [0|X], allp(X).
In Example 2.1, X = [0|X] refers to unification without occurs-check and ancestor subsumption avoids that a Prolog system not performing the occurs-check repeatedly proves p(0) and tries to prove allp(X). Without reasoning by induction, the proof of the goal X = [0|X], allp(X) cannot be completed. By induction, it can of course be proved.
In the Example 2.2, ancestor subsumption (without occurs-check) avoids that a Prolog system (performing the occurs-check or not) endlessly attempts to prove p, q(Y), r(f(Y)), and s(f(...f(Y)...)). Even by induction, none of these four goals can be proved. Example 2.3 is similar to Example 2.2: With ancestor subsumption (without occurs-check), a Prolog system not performing the occurs-check does not endlessly attempt to prove member(1, T). Even by induction, the goal member(1, T) cannot be proved because 1 does not occur in the cyclic list specified by T = [0|T].
Summing up, Examples 2.1, 2.2 and 2.3 illustrate that ancestor subsumption (without occurscheck) (Socher-Ambrosius 1992) is a pruning rule (that is, a rule for discarding redundant parts of a proof), not an inference rule (that is, a rule for deriving logical consequences).
The downside of ancestor subsumption is its cost what led Rolf Socher-Ambrosius to give in (Socher-Ambrosius 1992) syntactic characterizations of clause sets giving rise to ancestor subsumption. In (Socher-Ambrosius 1992) , such clause sets are said to "roughly correspond to sets of logical equivalences". Luke Simon, Ajay Bansal, Ajay Mallya and Gopal Gupta proposed in 2006in (Simon et al. 2006Simon et al. 2007) coinductive logic programming, a form of logic programming which is the first of its kind for two reasons: First, it combines the two kinds of codata so far proposed for logic programming, rational (or regular) terms like X = [0|X] based on unification without occurs-check, and infinite terms like f(ω) defined as limits of an infinite sequence finite terms constructed during the steps of non-terminating SLDF derivations based, according to the greatest fixpoint semantics of logic programs (Abdallah 1983;Abdallah 1984;van Emden and Abdallah 1985;Lloyd 1987), on unification with occurs-check. Second, it introduces into logic programming a proof principle named coinductive hypothesis rule which resembles the coinduction proof principle. Applications of coinductive logic programming are presented in (Gupta et al. 2011). Implementations of coinductive logic programming languages are described in (Moura 2013;Mantadelis et al. 2014).
The declarative and operational semantics of coinductive logic programming given in (Simon et al. 2006;Simon et al. 2007) have confusing aspects. One of them is the claim that coinductive logic programming's operational semantics is sound and complete with respect to the greatest fixpoint semantics of logic programs (Simon et al. 2006;Simon et al. 2007). No explanations are given of how this relates to the downward approximation sequence T p ↓ n of the immediate consequence operator T P , the limit of which specifies the greatest fixpoint semantics of a logic program (van Emden and Kowalsi 1976), not reaching a fixpoint before ω + 1 with some (finite and definite) programs P and even not before ω CK 1 with some others (finite and definite) programs (Fitting 2002, p. 8). 9 Another confusing aspect of coinductive logic programming is its "coinductive hypothesis rule of the form ν(n)" (Simon et al. 2006, p. 336) 10 which is defined as follows in (Simon et al. 2007, p. 472): "The operational semantics is given in terms of the coinductive hypothesis rule which states that during execution, if the current resolvent R contains a call C ′ that unifies with a call C encountered earlier, then the call C ′ succeeds." The 9 ω is the ordinal defined as the set of all finite ordinals and thus the smallest limit ordinal and ω CK 1 , the Church-Kleene ordinal, is defined as the set of all recursive ordinals and thus a limit ordinal and the smallest non-recursive ordinal (Church and Kleene 1937;Church 1938;Kleene 1938). 10 The coinductive hypothesis rule and ν(n) do not seem to be defined in (Simon et al. 2006). articles (Simon et al. 2006;Simon et al. 2007) do not explain how that coinductive hypothesis rule relates to the coinduction proof principle. The following examples cast a shadow over the coinductive hypothesis rule:
In Example 2.4, the SLD derivation from the goal ?-p(Y, a). is stopped at the subgoal ?-p(Y, Z). by the coinductive hypothesis rule what prevents the derivation of the subgoal p(s(Y), b) and therefore prevents that the rational term Y = s(Y) (which expresses s(ω)) be returned as answer. Example 2.4 suggests that the coinductive hypothesis rule of coinductive logic programming should not be based on ancestor unification (without occurs-check) but instead on ancestor subsumption (without occurs-check) (Socher-Ambrosius 1992).
In Example 2.5, since the predicate qc is declared coinductive, the goal ?-qc(f(Y), Y). is unified (without occurs-check) with the fact qc(X, f(X)). yielding as an answer the rational term Y = f(Y) even though no clauses in the program specify non-terminating SLD derivations.
Example 2.6 is like Example 2.5 except that the predicate, now called qi instead of qc, is declared inductive instead of coinductive. Since qc is declared inductive, a unification with occurs-check of ?-qi(f(Y), Y). with qi(X, f(X)). is attempted which fails because of the occurs-check. The articles (Simon et al. 2006;Simon et al. 2007) give no clues about the intentions behind treating differently cases like Examples 2.5 and 2.6. In Example 2.7, the goal ?-X = f(X), pi(X). probably fails because pi is declared inductive. Indeed, to the best of the author's understanding, that implies that unifications involving the variable X perform the occurs-check. In contrast, the goal ?-Y=f(Y),pc(X). probably succeeds returning the answer Y = f(Y) because pi is declared inductive what, as the author understands, means that unifications involving Y do not perform the occurs-check. Note that, according to the examples of (Simon et al. 2007, Section 2.5), in coinductive logic programming the system predicate = is both inductive and coinductive. The three goals of Example 2.7 are therefore licit. Example 2.7 suggests that whether a unification involving a term t performs the occurs-check or not should depend on the type of t, data or codata, not on a type inductive or coinductive of predicates in which t occurs. Example 2.7 raises the question whether with coinductive logic programming as defined in (Simon et al. 2006;Simon et al. 2007) a same term t might occur as an argument of both inductive or coinductive predicates, in which case the third goal ?-Z = f(Z), pi(Z), pc(Z). is licit but does not seem to be covered by the semantics given in (Simon et al. 2006;Simon et al. 2007), or whether inductive and coinductive predicates (except =) cannot share arguments, in which case coinductive logic programming as defined in (Simon et al. 2006;Simon et al. 2007) would be a rather limited approach.
Coinductive definitions have entered functional programming with lazy evaluation (Henderson and Morris 1976;Friedman and Wise 1976). The infinite list of Fibonacci numbers can for example be coded in Haskell as (f 0 1) and the finite list of its 43 first elements as take 43 (f 0 1) where the function f is coded as f a b = a : f b (a+b). A type system for coinductively defined data objects, or codata, has been proposed in (Jeannin et al. 2017). The use of the coinduction proof principle for the analysis of functional programs with codata is discussed in (Gordon 1994). The lazy evaluation of infinite objects has entered logic programming through logic-functional languages (Giovannetti et al. 1991;Hanus 1994).
Coinductive definitions have been elegantly formalized in 2005 by Jan Rutten as behavioural differential equations (Rutten 2005). Rutten's behavioural differential equations are further used in (Kupke et al. 2011;Hansen et al. 2017). In their term-based form, behavioural differential equations are close to, and extend, the aforementioned representation of rational trees in Prolog II. In the following, coinductive definitions are given in the term-based form of Rutten's behavioural differential equations.
The coinduction proof principle relates to mathematical induction 11 because it relates to structural induction which itself derives from mathematical induction. Structural induction has been formalized in 1959 East of the Iron Curtain by Rózsa Péter in (Péter 1961) and in 1969 West of it by Rod M. Burstall (Burstall 1969). 12 Proof by (mathematical or structural) induction cannot be completely automated because finding a suitable induction hypothesis is neither decidable, nor semi-decidable: "In contrast to first-order inference, inductive inference is incomplete in the sense that any axiomatization which includes a non-trivial form of induction, there are formulas both true and unprovable" (Bundy 2006) which follows from Kurt Gödel's first incompleteness theorem (Gödel 1931). Proofs by induction have nonetheless be (incompletely) automated (Boyer and Moore 1988;Bundy 2006;Comon 2006;Avenhaus et al. 2003) in two manners: Explicitly (Bundy 2006) and implicitly after the approach called "inductive completion" or "inductionless induction" (Comon 2006). The later approach consists in assuming the conjecture to prove, in attempting to derive an inconsistency using the Knuth-Bendix completion algorithm (Knuth and Bendix 1967), and if no inconsistency is derived to consider the conjecture proved. Observe that inductive completion (or inductionless induction) resembles the coinduction proof principle. 13 Proofs by induction are supported by proof assistants (Geuvers 2009), that is, proof systems requiring the participation of their human users. Coinduction as a proof method is usually described as dual of induction, a description referring to the coalgebras of category theory (Jacobs and Rutten 1997). Like proofs by induction and for the same reason, proofs by coinduction cannot be completely automated. Coinduction as a proof method has been formalized in higher-order logic and automated with the proof assistant Isabelle as reported in (Paulson 1997) and in terms of Labelled Transition Systems (LTSs) in (Pous and Sangiorgi 2011). Like proofs by induction, proofs by coinduction have been partly automated in proof assistants (Paulson 1997).
A proof method which resembles the coinduction proof principle has been proposed for logic programming in 2008 by Joxan Jaffar, Andrew Santosa and Rȃzvan Voicu in (Jaffar et al. 2008). The authors stress in this article that the proof method they propose refers to the least fixpoint semantics, not to the greatest fixpoint semantics of of logic programs: "we would like to clarify that the use of the term coinduction pertains to the way the proof rules are employed for a proof obligation G |= H, and has no bearing on the greatest fixed point of the underlying logic program P. In fact, our proof method, when applied successfully, proves that G is a subset of H wrt. the least fixpoint of (the operator associated with) the program" (Jaffar et al. 2008). In contrast to standard induction and coinduction proof methods, the proof method proposed in (Jaffar et al. 2008) can be completely automated: "a search-based method [. . . ] automatically discovers the opportunity of applying induction instead of the user having to specify some induction schema", "our method is amenable to automation" and "the unfolding process and the application of the coinduction principle require no manual intervention" (Jaffar et al. 2008). The generalized coinduction proof principle (see Section 7 below) precises how the proof method of (Jaffar et al. 2008) relate to the coinduction proof principle. Jan Rutten gives in (Jacobs and Rutten 1997;Rutten 2000;Rutten 2005) coalgebraic treatments of coinduction. Davide Sangiorgi's book (Sangiorgi 2012) is a comprehensive introduction to coinduction, bisimulation and the coinduction proof principle which, however, does not address coinduction in declarative programming and does not mention inductionless induction (Comon 2006).

Coinductive Definitions
This section introduces terms of type codata, short codata terms after one of the formalisms which have been proposed for the finite representation of constructed streams (Rutten 2005;Kupke et al. 2011). Codata terms rely on corecursive definitions which are introduced in the next section.
Two disjoint data types are considered in the following: Data for the representation of nonstream objects and codata for the representation of streams the elements of which are of type data. Considering only the two types data and codata is a convenient simplification. In practice, the type data consists of several pairwise disjoint types like integer, floating-point number, character, etc. and structured types like finite list of integers, finite list of floating-point numbers, finite list of characters, etc. Streams of streams could be considered, though, since such streams might make sense for example in specifying stream processing operations but such streams and the issues they raise are not addressed in this article.
The type codata encompasses codata terms and their names. The following illustrates on the Fibonacci function the concept of codata term and of name, base cases and defining expression of a codata term: This expression is a codata term. Its name is fib, its base cases are 0 and 1 and its defining expression is fib^0 + fib^1. In contrast to (Rutten 2005), the keyword as is used instead of = for avoiding a confusion with the the Prolog fashion's use of = in the former section of this article for denoting unification. Codata terms as illustrated above and defined below slightly generalise those of (Rutten 2005) by allowing compound codata names which are needed for expressing mutual corecursion.
It is convenient to think of the codata term fib as a definition of an infinite list, a view which is justified below in Section 5. fib^0 denotes fib and for all natural number n, fib^(n+1) denotes the tail of fib^(n). Thus, fib^1 denotes the tail of fib.
If f and g respectively represent  Even though the codata term fib is a recursive definition of the Fibonacci function, it specifies an iterative computation, as does a tail recursive definition (Friedman and Wise 1974;Steele 1977), but it does not require accumulators, in contrast to a tail recursive definition. This is an essential aspect of coinductive definitions which can be expressed in logic programming parlance as follows: Codata are meant to express forward chaining inferences as defined by the immediate consequence operator T (van Emden and Kowalsi 1976).
In the following, Data denotes the set of terms of type data and Codata denotes the set of terms of type codata. In Section 5 below, it is shown that a codata term s as [s 0 , s 1 , ..., s n | E] with s a constant induces the definition of a function:   • for all n ∈ N s^n is the nth-tail of s It follows from Definition 3.2 by mathematical induction that for all n ∈ N and m ∈ N s^n^m = s^(n+m).

Definition 3.3 (Codata term)
A codata term or codata definition is an expression of the form s as [s 0 , s 1 , ..., s n | E] where: • s is an atomic or compound codata name.
• the s i , 0 ≤ i ≤ n, are terms of sort data called the base cases.
• E is a codata expression. s as [s 0 , s 1 , ..., s n | E] is a definition of s and s is called the name of the codata term.
Codata expressions are defined below in Section 4.

Example 3.1
The following mutually recursive functions for n ≥ 1 g(n) = 2 × f (n − 1) for n ≥ 1 can be expressed by the following codata term:  2. If s is atomic, then E defines an atomic codata, else E defines a tuple of the size of s. 3. All atomic names occurring in the defining expression E also occur in the codata name s. 4. If the defining expression E refers to a kth tail t^k, then n ≥ k + 1.
The first two conditions ensure that the name, the base cases and the defining expression of a codata term are consistent in their sizes. The third conditions ensures that every name referred to in a codata term is defined in that codata term. The fourth and last condition ensures that the number of base cases in a codata term and the references to tails in that codata term's defining expression are consistent.

Example 3.2
Using nat, a codata term expressing the sequence of natural numbers, Douglas Hofstadter's female and male sequences (Hofstadter 1979): can be expressed by the following codata term: (nat,f,m) as [(0,1,0) | (1+nat,nat-m^f,nat-f^m)] This example shows that codata terms can express non-linear recurrence relations. Such a definition requires a more involved notion of well-formedness than that given above in Definition 3.4, though. This more involved notion of well-formedness is out of the scope of this article.

Corecursive Definitions
The qualifier "inductive" ("coinductive", respectively) refers to data (codata, respectively) definitions while the qualifier "recursive" ("corecursive", respectively) refers to the definitions of functions or predicates on data (codata, respectively). In most cases, the pedantic distinction (co)inductive/(co)recursive can be ignored. Furthermore, this distinction is blurred in the presence of codata which can be seen both as infinite lists and function definitions. The distinction is nonetheless used in the titles of this section and of the former section because it provides a convenient structuring of the exposition.
In the following, pointwise means element-wise and refers to the interpretation of codata terms as infinite lists which is justified below in Section 5. In the following, all corecursive definitions refer to natural numbers. Example of corecursive referring to other data types (like Boolean, characters, strings of characters, etc.) can easily be derived from the following "number-based" examples.
If a d is a data constant, then the codata constant a c is defined by: The sum of a data constant a d and a codata s is defined by: a d +s as [a d + s(0) | a d + s^1] The pointwise product of codata s and t is defined by: s*t as [s(0) * t(0) | s^1 * t^1] The codata nat (natural numbers) is defined by: nat as [0 | 1 d + nat].
The pointwise sum s+t of codata s and t is defined by: s+t as [s(0) + t(0) | s^1 + t^1] The codata nat (natural numbers) can also be defined by: nat as [0 | 1 c + nat] The product of a data constant a d and a codata s is defined by: The pointwise pairing of codata s and t is defined by: (s, t) as [(s(0), t(0)) | (s^1, t^1)] The pointwise application of data term constructor f to codata s is defined by: Right-side sums and products with data constants are defined similarly to the left-side sums and products with data constants specified above. The codata fact (factorial numbers) is defined by: fact as [1 | nat^1 * fact]

Definition 4.1 (Codata expression)
A codata expression is a codata n-th tail (including a codata name) or the application of a corecursive function to codata expression(s). Let s as [s 0 , s 1 , ..., s n | E] be a codata term with an atomic name. s immediately depends on every codata constant and every codata name occurring in the codata expression E. Depends is used for the transitive closure of directly depends.
Immediate dependency extends component-wise to compound codata names.

Definition 4.2 (Structural codata expression)
A codata expression is structural if it contains neither sums, nor products.

More generally, a function definition is structural if its does not involve expressions determining values of which requires reductions (that is, computations).
Observe that the corecursive function definitions given above are all pointwise. Observe also that the codata constants, the codata pairing and grouping and the pointwise data term application are the only structural cases of structural corecursion given above.

Interpretation of Codata as Infinite Streams
This section shows that a codata term s as [s 0 , s 1 , ..., s n | E] specifies an infinite list in the sense that it induces the definition of a function s: N m → Data where m is the dimension of s, that is, m = 1 if s is atomic, and m is the tuple size of s otherwise. The overloading of the symbol s used both as a codata name and a function name is intentional and justified by Definition 3.2 of Section 3.
The notation E[s 0 , ..., s n ] expresses that the set of atomic codata names occurring in expression E is {s 0 , . . . , s n }, that is, for all 0 ≤ i ≤ n, s i = s(i).
E^0 denotes E and if k ∈ N \ {0}, then E^k denotes the expression obtained from expression E by replacing every nth-tail t^n in E by t^n^k. obtained from s by repeatedly applying the codata term defining expression E. Recall that for all 0 ≤ i ≤ k, s i = s(i).
Section 3 above gives examples of expansions of the codata term fib. The following shows that the applications mentioned in Definition 5.2 terminate if the codata term considered is wellformed.

Proposition 5.1 (Expansion Theorem)
For all well-formed codata terms s as [s 0 , s 1 , ..., s k | E] and all n ∈ N such that n ≥ k, the nth expansion s[n] of s is uniquely defined.

Proof
First observe that if s as [s 0 , s 1 , ..., s k | E] is a well-formed codata term, then s (directly or indirectly) depends on finitely many codata names all occurring in s. Second, observe that [s 0 , s 1 , ..., s k | E] is its kth expansion of s. The result follows by structural induction. and the concepts of Definition 3.2 from Section 3 above are well-defined.

Proof
By structural induction and the Expansion Theorem 5.1.
A few remarks are worthwhile. First, even though the set of infinite lists on a finite alphabet is not enumerable, 14 the set of codata terms on a finite alphabet is recursively enumerable. Indeed, like a data term, codata terms are finite expression which can be inductively defined. Thus, using the terminology of the introduction, not all observed streams can be specified as constructed streams.
Third, let s and t be the names of two well-formed codata terms. Whether for all n ∈ N s(n) = t(n) (that is, s and t specify the same infinite list) is neither decidable nor semidecidable. Algorithms are possible, though, which in some cases will decide whether, or recognize that, two codata terms specify a same infinite list or whether all elements of the infinite list specified by a codata term has a certain property.
Fourth and finally, it is worth stressing that one of the interests of codata terms is to (corecursively) define functions f : N → Data without having to give an equation on n for f (n). There are indeed cases in which this is desirable. The Fibonacci function for example has a simple recursive definition, fib as [0, 1 | fib + fib^1], but a significantly more complicated definition as an equation on n: In other cases, however, an equation on n is simpler than a recursive definition: For all n ∈ N f (n) = n is for example simpler than: nat as [0 | 1 + nat]

First Generalized Coinduction Theorem
In this section and the following, a predicate is called a data predicate if all its arguments are of type data and a predicate is called a codata predicate if all its arguments are of type codata, data predicates are denoted by identifiers beginning with lower case characters and codata predicates are denoted by identifiers beginning with upper case characters, codata terms are implicitly assumed to be well-formed and the phrase "the codata term s" refers to a (well-formed) codata term of the form s as [d 1 , ... , d k | E] with k ≥ 1.

Definition 6.1 (Pointwise-defined and hereditary codata predicate)
Let p be a unary data predicate and s a codata name. The unary codata predicate P p defined by: For all codata term s, P p (s) iff for all n ∈ N p(s(n)) is called the pointwise-derived from p. A unary codata predicate H which fulfills the following condition is said to be hereditary with respect to p, short p-hereditary: If H(s) holds of some codata s, then 1. p(s(0)) holds.

H(sˆ1) holds.
Lemma 6.1 Let p be a unary data predicate. The pointwise-derived P p from p is p-hereditary.

Proof
Let p be a unary data predicate and let s be a codata name. By definition of the pointwise-derived P p from p, P p (s) iff for all n ∈ N p(s(n)). Thus, if P p (s) holds, then p(s(0)) holds and P p (sˆ1) holds.
Observe that the concept of p-hereditary codata predicate generalises that of bisimulation relation (Park 1981;Rutten 2005;Sangiorgi 2012) since a bisimulation relation B is defined as a binary relation such that s 1 B s 2 if More precisely, a bisimulation relation B is an =-hereditary predicate applying of pair codata (s 1 , s 2 ). Thanks to codata pairing defined above in Section 4, a binary codata predicate can be seen as a unary codata predicate the argument of which is a pair of codata.
Observe also that if p is a unary data predicate and P 1 and P 2 are p-hereditary codata predicates, then the codata predicates A and O defined as follows are also p-hereditary: For all codata names s: • A(s) iff (P 1 (s) ∧ P 2 (s)) • O(s) iff (P 1 (s) ∨ P 2 (s)) Definition 6.2 (Maximal p-hereditary codata predicate) Let p be a unary data predicate. The maximal p-hereditary codata predicate Max p is defined by: If H is a p-hereditary codata predicate and s is as codata name such that H(s) holds, then Max p (s) holds.
Observe that Max p is the greatest p-hereditary predicate in the sense that it expresses the union of all unary relations on codata which are defined by unary p-hereditary codata predicates. Observe also that Max p generalizes the bisimilarity relation (Park 1981;Rutten 2005;Sangiorgi 2012) which, in the terminology of Definition 6.2, is Max = .
Theorem 6.1 (First Generalized Coinduction Theorem) Let s be the name of a codata term and let p a unary data predicate. The following statements are equivalent: 1. There is a unary p-hereditary codata predicate H such that H(s) holds. 2. There is a unary p-hereditary codata predicate H such that: ∀n ∈ N H(sˆn) 3. ∀n ∈ N p(s(n)) Proof Let s be a codata term, p a unary data predicate and H a unary codata predicate.
(1) ⇒ (2): Assume H is p-hereditary and H(s) holds. The proof is by induction. Since by hypothesis H is p-hereditary and H(s) holds, H(sˆ1) holds. Let n ∈ N and assume that H(sˆn) holds. Since by hypothesis H is p-hereditary and H(sˆn) holds, H(sˆ(n + 1)) holds.
(3) ⇒ (1): If for all n ∈ N p(s(n)), then P p (s) holds where P p is the pointwise-derived from p defined in Definition 6.1. By Lemma 6.1, P p is p-hereditary.

Generalized Coinduction Proof Principle
Recall that all codata terms considered are implicitly assumed to be well-formed.

Corollary 7.1 (Generalized Coinduction Proof Principle)
Let p be a unary data predicate and let s be the name of a codata term. For proving ∀n ∈ N p(s(n)) 1. it suffices to exhibit a unary codata predicate H such that: (That is, for all codata names t, p(t(0)) and H(tˆ1) holds.) 2. it suffices to exhibit a unary p-hereditary codata predicate H such that ∀n ∈ N H(sˆn).
The generalized coinduction proof principle extends to every unary data predicate the coinduction proof principle formulated in (Park 1981;Rutten 2005;Sangiorgi 2012) for equality.
If several codata terms mutually depend on each other (in the sense of Definition 4.1, that is, are mutually corecursive), then a proof by strong coinduction referring to one of these codata names s must, of course, also refer to the codata names s depends on. This stresses the necessity for the codata terms considered to be well-formed.
For a better understanding, the following examples of proofs by (generalized) coinduction are detailed (and possibly over-detailed).
The singleton set consisting of this codata term is well-defined. Let P be the codata predicate defined by: For all codata name s, P(s) if s(0) > 0 and sˆ1 = s. Thus, P is (> 0)-hereditary and P(1 c ) holds. By the generalized coinduction proof principle, ∀n ∈ N 1 c (n) > 0.
The singleton set consisting of this co-data term is well-defined. Proof by generalized coinduction of ∀n ∈ N (n > 0 ⇒ fib(n) > 0).
The result follows by the generalized coinduction principle.

Example 7.3
This example is adapted from (Rutten 2005 This set of codata terms is well-defined. Proof by coinduction for all codata name s and t even(zip(s, t)) = s. Let P be the binary codata defined by: (⋆) for all codata names s and t, P(even(zip(s, t)), s).
The proof by coinduction of zip(even(s), odd(s)) = s of Example 7.3 given above stresses an aspect of some proofs by coinduction. A codata predicate P is constructed as the closure over tails of codata, what is often described as the computation of a greatest fixpoint (Rutten 2005;Sangiorgi 2012). This view is recalled in the following.
Let p be a unary data predicate and consider the following operator Φ p on the unary codata relations: If s is a codata name, a proof by generalized coinduction of ∀n ∈ N p(n) consists in establishing the existence of a unary p-hereditary predicate R, which defines a unary relation on P(Codata), such that R(s) holds, that is, that R ⊆ Φ p (R) that means that R is a postfixpoint of Φ p . By a theorem of Knaster (Knaster 1928;Tarski 1930;Tarski 1955) commonly called the Knaster-Tarski theorem, the greatest fixpoint of Φ p is the unary relation on Codata characterized by the predicate Max p defined above in Definition 6.2. 15 The need for a strengthening of the definition of the predicate to be proven p-hereditary in a proof by coinduction, as in the proof given in Example 7.3 above, is not specific of coinduction proofs. Such strengthening are common in induction proofs where they are called "induction loading". A traditional example of induction loading is that a proof by induction of which is impossible without strengthening that statement for example into: Proof by coinduction of: Consider the following well-formed codata terms: 1617 (nat, sum1) as [(0, 0)|(1+nat, 1+nat+sum1)] (nat, sum2) as [(0, 0)|(1+nat, (1/2)*nat*(1+nat))] First, a codata predicate P is defined as follows: For all codata names s and t, P(s,t) if 1. s(0) = t(0) 2. ∀n ∈ N (s(n) = t(n) ⇒ s(n + 1) = t(n + 1)) Second, it is proved that P is =-hereditary. Let s and t be codata names such that P(s,t) holds. By (1) of the definition of P, s(0) = t(0). If follows now from (2) of the definition of P that s(1) = t(1). If also follows from (2) of the definition of P that ∀n ∈ N 0 (s(n) = t(n) ⇒ s(n + 1) = t(n + 1)). This means that P(sˆ1,tˆ1) what completes the proof that P is =-hereditary.
Under certain notational assumption, the proof of ∀n ∈ N (n > 0 ⇒ fib(n) > 0) given in Example 7.2 can be shortened as follows. From Thus, if fib^1 > 0 and fib^2 > 0, then fib^1 + f^2 > 0. Since fib^1(0) = fib^1(1) = 1, the result holds by the generalized coinduction proof principle The notational assumption giving sense to the above proof is that if p denotes a data predicate, then the pointwise-derived from p, P p , defined in 6.1, is also denoted p, the context allowing to disambiguate. The first sentence above states that the expression defining fib^1, fib^1 + fib^2, preserves the pointwise-derived of (> 0), P (>0) . This is indeed the case because so does the "down-lifted" of that expression to the data: If s and t are data names such that s > 0 and t > 0, then s + t > 0. The second sentence states that each of the finitely many initial values defining fib^1 does satisfy the data predicate (> 0).
It is similar shortened bisimulation proofs that have made the coinduction proof principle "seem a bit magical" (Kozen and Silva 2016, p. 2).
Example 7.4 suggests the following theorem.

Theorem 7.1 (Second Generalized Coinduction Theorem)
The principle of mathematical induction and the generalized coinduction proof principle follow from each other.

Proof
Since the First Generalized Coinduction Theorem 6.1, from which generalized coinduction proof principle is derived, is proved above by induction, it suffices to show that the principle of mathematical induction follows from the generalized coinduction proof principle. Assume that p is a unary data predicate such that p(0) holds and ∀n ∈ N (p(n) ⇒ p(n + 1)). We show that the generalized coinduction proof principle implies that ∀n ∈ N p(n).
Let P be a codata predicate defined by: For all codata names s, P(s) holds if 1. p(s(0)) 2. ∀n ∈ N p(s(n)) ⇒ p(s(n + 1)) Let s be a codata name. Assume P(s)) holds. it follows from the definition of P that p(s(1)) holds and that ∀n ∈ N \ {0} p(s(n)) ⇒ p(s(n + 1)), that is, by definition of P, P(sˆ1) holds. Thus, P is p-hereditary. By the generalized coinduction proof principle, ∀n ∈ N p(n), what completes the proof.

Perspectives and Conclusion
An observed stream is a possibly never ending sequence of observations or measurements of natural or artificial systems like temperatures, the reproduction rates of a disease, and energy consumption or traffic volumes. Observed streams are compared with behavioral models, typically for detecting situations of interest like critical raises of a stream's data.
Behavioral models of observed streams can be expressed as constructed, or synthetic, streams specified as codata terms (as defined in Sections 3 and 4). Functions or predicate on codata then give rise to express properties of such models which can be established using the generalized coinduction proof. A proof similar to that of Example 7.1 for example establishes that s1 = s2 if s1 and s2 are defined by: For a less trivial example, consider the following codata terms which specify repeating oscillations over respectively 2, 3 and 6 states denoted 0 to 5: o2 as [0, 1 | o2] o3 as [0, 1, 2 | o3] o6 as [0, 1, 2, 3, 4, 5 | o6]
Consider now the codata term n as [0 | s(n)] which specifies the stream: [0, s(0), s(s(0)), s(s(s(0))), ...] Recall the following codata term from Section 4 which specifies the stream of natural numbers: nat as [0 | 1 + nat] A proof by generalized coinduction that n ∼ f nat does not essentially differ from the proof given in Example 7.1 and from the above-mentioned proof of (o2,o3) ∼ f o6. The aforementioned proofs by generalized coinduction have in common that they refer either to structurally defined codata (in the sense of Definition 4.2) or, for the last one, to a decidable first-order theory, Presburger arithmetic (Presburger 1929). As a consequence, such proofs can be automated. More precisely, proofs of the finite equivalence (in the sense of ∼ f defined above) of structurally defined codata terms (in the sense of Definition 4.2) and of codata terms defined in terms of decidable theories can be completely automated and therefore supported by a declarative, functional or logic, programming language. 18 A declarative programming language providing automated proofs by generalized coinduction for codata terms defined in terms of decidable theories would be a useful tool for processing observed streams. This article has first given an extensive review of coinduction in declarative programming. Second, it has reviewed and slightly extended the codata formalism. Third, it has generalized to any predicate the coinduction proof principle which was originally specified for the equality predicate only. This generalization has been shown to make the coinduction proof principle more intuitive by making better visible its closeness with structural induction. The article has finally suggested to extend declarative, functional or logic, programming with a limited, decidable form of the generalized of the coinduction proof principle based upon structural codata definitions or upon codata definitions referring to decidable theories.