Mutual Coinduction

TL;DR

This paper introduces and formalizes mutual coinduction as a dual to mutual induction, providing proof principles, conditions for fixed points, and discussing its relation to standard induction and coinduction.

Contribution

It offers the first formal definitions and proof principles for mutual (co)induction, highlighting the importance of monotonicity over continuity for fixed point existence.

Findings

Mutual coinduction is a dual of mutual induction.

Monotonicity of generators is sufficient for fixed points.

Formal definitions and proof principles for mutual (co)induction are established.

Abstract

In this paper we present mutual coinduction as a dual of mutual induction and also as a generalization of standard coinduction. In particular, we present a precise formal definition of mutual induction and mutual coinduction. In the process we present the associated mutual induction and mutual coinduction proof principles, and we present the conditions under which these principles hold. In spite of some mention of mutual (co)induction in research literature, but the formal definition of mutual (co)induction and the proof of the mutual (co)induction proof principles we present here seem to be the first such definition and proof. As such, it seems our work is the first to point out that monotonicity of mutual generators seems not sufficient for guaranteeing the existence of least and greatest simultaneous fixed points in complete lattices, and that continuity on the other hand is sufficient for guaranteeing their existence. [The paper has been responsively updated so as to not require the continuity of generators but only require their monotonicity, and it now includes a proof of the sufficiency of monotonicity. A full revision of the paper to reflect the relaxed requirement is currently underway.] In the course of our presentation of mutual coinduction we also discuss some concepts related to standard (also called direct) induction and standard coinduction, as well as ones related to mutual (also called simultaneous or indirect) induction. During the presentation we purposely discuss particular standard concepts so as to help motivate the definitions of their more general counterparts for mutual/ simultaneous/ indirect (co)induction. Greatest simultaneous post-fixed points, in particular, will be abstractions and models of mathematical objects (e.g., points, sets, types, predicates, etc.) that are defined mutually-coinductively.

Figures

Equations

$$F\left(P\right)\le P.$$

$$P\le F\left(P\right).$$

$$P=F\left(P\right).$$

$$F\left(O\right)⊑P\text{ and }G\left(P\right)\le O.$$

$$PreF{P}_{F,G}\left(O\right)=\left\{P\in \mathbb{P}|F\left(O\right)⊑P\text{ and }G\left(P\right)\le O\right\},\text{ and}$$

$$PreF{P}_{G,F}\left(P\right)=\left\{O\in \mathbb{O}|F\left(O\right)⊑P\text{ and }G\left(P\right)\le O\right\}.$$

$$P⊑F\left(O\right)\text{ and }O\le G\left(P\right).$$

$$F\left(O\right)=P\text{ and }G\left(P\right)=O.$$

$$\sqcap F\left(\mathbb{M}\right)=F\left(\wedge \mathbb{M}\right)\text{ and }\wedge G\left(\mathbb{N}\right)=G\left(\sqcap \mathbb{N}\right),\text{ and}$$

$$\bigsqcup F\left(\mathbb{M}\right)=F\left(\vee \mathbb{M}\right)\text{ and }\vee G\left(\mathbb{N}\right)=G\left(\bigsqcup \mathbb{N}\right).$$

$$F\left(\wedge \mathbb{M}\right)⊑\sqcap F\left(\mathbb{M}\right)\text{ and }G\left(\sqcap \mathbb{N}\right)\le \wedge G\left(\mathbb{N}\right),\text{ and}$$

$$\bigsqcup F\left(\mathbb{M}\right)⊑F\left(\vee \mathbb{M}\right)\text{ and }\vee G\left(\mathbb{N}\right)\le G\left(\bigsqcup \mathbb{N}\right).$$

$$O_1\le O_2⟹F\left(O_1\right)⊑F\left(O_2\right)$$

$$P_1⊑P_2⟹G\left(P_1\right)\le G\left(P_2\right).$$

$$\text{bigsqcap}F\left(\left\{O_1,O_2\right\}\right)=\text{bigsqcap}\left\{F\left(O_1\right),F\left(O_2\right)\right\}⊑F\left(O_2\right).$$

$$O_1\le O_2⟹F\left(O_1\right)⊑F\left(O_2\right)⟹G\left(F\left(O_1\right)\right)\le G\left(F\left(O_2\right)\right),$$

$$P_1⊑P_2⟹G\left(P_1\right)\le G\left(P_2\right)⟹F\left(G\left(P_1\right)\right)⊑F\left(G\left(P_2\right)\right),$$

$$F\left(O\right)⊑P\text{ and }G\left(P\right)\le O.$$

$$G\left(F\left(O\right)\right)\le G\left(P\right)\le O.$$

$$G\left(F\left(O\right)\right)\le O$$

$$F\left(G\left(P\right)\right)⊑F\left(O\right)⊑P.$$

$${\mathbb{P}}_O=PreF{P}_{F,G}\left(O\right)=\left\{P\in \mathbb{P}|F\left(O\right)⊑P\text{ and }G\left(P\right)\le O\right\}.$$

$$\sqcap {\mathbb{P}}_O=F\left(O\right),$$

$$F\left(O\right)⊑\sqcap \mathbb{N}\text{ and }G\left(\sqcap \mathbb{N}\right)=\wedge G\left(\mathbb{N}\right)\le O,\text{ and}$$

$$F\left(O\right)⊑\bigsqcup \mathbb{N}\text{ and }G\left(\bigsqcup \mathbb{N}\right)=\vee G\left(\mathbb{N}\right)\le O.$$

$$\mathbb{C}=\left\{O\in \mathbb{O}|\exists P\in \mathbb{P}.F\left(O\right)⊑P\text{ and }G\left(P\right)\le O\right\},\text{ and}$$

$$\mathbb{D}=\left\{P\in \mathbb{P}|\exists O\in \mathbb{O}.F\left(O\right)⊑P\text{ and }G\left(P\right)\le O\right\}$$

$$\mathbb{B}=\left\{B\in \mathbb{P}|\exists A\in \mathbb{A}.F\left(A\right)⊑B\text{ and }G\left(B\right)\le A\right\}$$

$$F\left(\bigwedge \mathbb{A}\right)⊑\text{bigsqcap}\mathbb{B}\text{ and }G\left(\text{bigsqcap}\mathbb{B}\right)\le \bigwedge \mathbb{A}.$$

$$\mathbb{C}=\left\{O\in \mathbb{O}|\exists P\in \mathbb{P}.F\left(O\right)⊑P\text{ and }G\left(P\right)\le O\right\}$$

Full text

In spite of some mention of mutual (co)induction in research literature, but the formal definition of mutual (co)induction and the proof of the mutual (co)induction proof principles we present here seem to be the first such definition and proof. As such, to the best of our knowledge, it seems our work is the first to point out that, unlike the case for standard (co)induction, monotonicity of generators seems not sufficient for guaranteeing the existence of least and greatest simultaneous fixed points in complete lattices, and that continuity on the other hand is sufficient for guaranteeing their existence.111This paper has been updated so as to not require the continuity of generators but only require their monotonicity. See Appendix C. A full revision of the paper to reflect the relaxed requirement is currently underway.

In the course of our presentation of mutual coinduction we also discuss some concepts related to standard (also called direct) induction and standard coinduction, as well as ones related to mutual (also called simultaneous or indirect) induction. During the presentation we purposely discuss particular standard concepts (namely, fixed points, least and greatest fixed points, pre-fixed points, post-fixed points, least pre-fixed points, and greatest post-fixed points) so as to help motivate the definitions of their more general counterparts for mutual/simultaneous/indirect (co)induction (namely, simultaneous fixed points, least simultaneous fixed points, greatest simultaneous fixed points, least simultaneous pre-fixed points and greatest simultaneous post-fixed points). Greatest simultaneous post-fixed points, in particular, will be abstractions and models of mathematical objects (e.g., points, sets, types, predicates, etc.) that are defined mutually-coinductively.

1 Introduction

Induction and coinduction, henceforth called *standard *(co)induction, present mathematical models for (standard) recursive definitions (also called direct recursive or self-recursive definitions). In the same way, mutual induction and mutual coinduction, henceforth called *mutual *(co)induction, present mathematical models for mutually-recursive definitions, which are sometimes also called indirect recursive definitions or simultaneous recursive definitions.

In other concurrent work we present, first, some practical motivations from programming languages theory for defining mutual (co)induction [10] (included in Appendix B of this paper temporarily), then we present some intuitions for their mathematical definitions as well as examples of their use in [9], and we also present possible formulations of mutual (co)induction in other mathematical disciplines in [8]. In that concurrent work we conclude that: if mutually-recursive functional programs can be reasoned about mathematically, then also imperative and object-oriented programs (even the worst such programs) can be reasoned about mathematically. Interested readers are invited to check this concurrent work.

This paper is structured as follows. We first motivate the formal definition of mutual (co)induction by presenting in $\mathsection$2 the formal definitions of standard (co)induction, in the context of order theory. Then we present in $\mathsection$3 the order-theoretic definitions of mutual (co)induction and we present the mutual (co)induction proof principles. (We present proofs for the lemmas and theorems of $\mathsection$3 in Appendix A.) We briefly discuss some related work in $\mathsection$4, then we conclude and discuss some possible future work in $\mathsection$5.

Our work here is a followup on our earlier introductory work in [2, 6, 5]. In addition to the practical motivations mentioned above (whose interest in we started in [1]), the work presented here has also been motivated by that earlier introductory work.

2 Standard Induction and Standard

Coinduction

The formulation of standard induction and standard coinduction, and of related concepts, that we present here is a summary of the formulation presented in [2, $\mathsection$2.1].

Let $\leq$ (‘is less than or equal to’) be an ordering relation over a set $\mathbb{O}$ and let $F:\mathbb{O\rightarrow\mathbb{O}}$ be an endofunction over $\mathbb{O}$ (also called a self-map over $\mathbb{O}$, i.e., a function whose domain and codomain are the same set, thus mapping a set into itself).

Given a point $P\in\mathbb{O}$, the point $F\left(P\right)$ is called the $F$-image of $P$.

A point $P\in\mathbb{O}$ is called a pre-fixed point of $F$ if its $F$-image is less than or equal to it, i.e., if

[TABLE]

Dually, a point $P\in\mathbb{O}$ is called a post-fixed point of $F$ if it is less than or equal to its $F$-image, i.e., if

[TABLE]

A point $P\in\mathbb{O}$ is called a *fixed *point of $F$ if it is equal to its $F$-image, i.e., if

[TABLE]

(A fixed point of $F$ is simultaneously a pre-fixed point of $F$ and a post-fixed point of $F$.)

Now, if $\leq$ is a complete lattice over $\mathbb{O}$ (i.e., if $\leq$ is an ordering relation where meets $\wedge$ and joins $\vee$ of all subsets of $\mathbb{O}$ are guaranteed to exist in $\mathbb{O}$) and if $F$ is a monotonic* *endofunction over $\mathbb{O}$ ($F$ is then called a generator), then the *least pre-fixed point *of $F$, called $\mu_{F}$, exists in $\mathbb{O}$, by the Knaster-Tarski Fixed Point Theorem [20, 33], $\mu_{F}$ is also the least fixed point (lfp) of $F$, and the greatest post-fixed point of $F$, called $\nu_{F}$, exists in $\mathbb{O}$ and, again by the Fixed Point Theorem, $\nu_{F}$ is also the greatest fixed point (gfp) of $F$.

Further, for any element $P\in\mathbb{O}$ we have:

• •

(standard induction)co if $F\left(P\right)\leq P$, then $\mu_{F}\leq P$,

which, in words, means that if $P$ is a pre-fixed/inductive point of $F$, then point $\mu_{F}$ is less than or equal to $P$ (since $\mu_{F}$, by definition, is the least $F$-inductive point), and,

• •

(standard coinduction) if $P\leq F\left(P\right)$, then $P\leq\nu_{F}$,

which, in words, means that if $P$ is a post-fixed/coinductive point of $F$, then point $P$ is less than or equal to point $\nu_{F}$ (since $\nu_{F}$, by definition, is the greatest $F$-coinductive point).

References

See [16, 31, 2].

3 Mutual Induction and Mutual Coinduction

In this section we first present some intuition for mutual (co)induction as generalizations of standard (co)induction, then we present their formal definitions and formulate the associated proof principles. Our illustrated presentation includes a discussion of the continuity of generators, which seems necessary for proving the existence of simultaneous fixed points (but see Appendix C). In Appendix A we present proofs for the lemmas and theorems we present here.

Intuition

Intuitively, compared to standard (co)induction which involves one self-map from a poset to itself, mutual (co)induction involves two or more mappings between two or more ordered sets (i.e., posets). That’s all. In this paper, for simplicity, we focus only on the case involving just two mappings (also called generators) between two posets. As we define it below, our definition of mutual induction can be extended easily to involve more than two orderings, more than two underlying sets, and more than two mappings between the ordered sets. Also, it should be noted that in some practical applications of mutual (co)induction the two orderings, and their underlying sets, may happen to be the same ordering and set. For proper mutual (co)induction, however, there has to be at least two mutual generators/mappings between the two ordered sets.222Standard induction can then obtained as a special case of mutual induction by having one ordering and one underlying set and also having one of the two generators—or, more accurately, all but one of the generators—be the identity function. See also Footnote 5.

Also intuitively, the mutual induction and mutual coinduction proof principles are expressions of the properties of two points (i.e., elements of the two ordered sets) that are together (i.e., simultaneously) least pre-fixed points of each of the two generators and of two points that are together greatest post-fixed points of each of the two generators. As such mutual induction and mutual coinduction generalize the standard induction and standard coinduction proof principles. Further, in case the two orderings are complete lattices and the mappings are continuous (thereby called* generators* or mutual generators), the two least simultaneous pre-fixed points and the two greatest simultaneous post-fixed points will also be mutual fixed points (sometimes also called *simultaneous *or *reciprocal *fixed points) of the generators. (For a glimpse, see Figures 3.1, 3.2, and 3.3.)

Formulation

Let $\leq$ be an ordering relation over a set $\mathbb{O}$ and let $\sqsubseteq$ be a second ordering relation over a second set $\mathbb{P}$. Further, let $F:\mathbb{O\rightarrow\mathbb{P}}$ and $G:\mathbb{P\rightarrow\mathbb{O}}$ be two mutual endofunctions over $\mathbb{O}$ and $\mathbb{P}$ (also called *indirect *or reciprocal self-maps over $\mathbb{O}$ and $\mathbb{P}$, i.e., two functions where the domain of the first is the same as the codomain of the second and vice versa, such that each of the two posets is mapped into the other).333As in [2], we are focused on unary functions in this paper because we are interested in discussing fixed points and closely-related concepts such as induction and coinduction, to which multi-arity seems to make little difference. For more details, see the brief discussion on arity and currying in [2]. Note that given two mutual endofunctions $F$ and $G$ we can always compose $F$ and $G$ to get the (standard) endofunctions $G\circ F:\mathbb{O}\rightarrow\mathbb{O}$ and $F\circ G:\mathbb{P}\rightarrow\mathbb{P}$.444Upon seeing these compositions, readers familiar with category theory may immediately suspect a possible connection with adjunctions. That possibility of a connection will increase when readers check the definitions below, of simultaneous pre-fixed points and simultaneous post-fixed points. We intend to dwell on the possibility of such a connection in future work (or in later versions of this paper).,555Note that if we have $\mathbb{P}=\mathbb{O}$ (the two underlying sets are the same), $\sqsubseteq=\leq$ (with the same orderings), and if $G=\mathbf{1}$ (or $F=\mathbf{1}$, where $\mathbf{1}$ is the identity function), then we obtain standard (co)induction as a special case of mutual (co)induction. In particular, all definitions presented below will smoothly degenerate to their standard counterparts (i.e., will correspond to ones for standard (co)induction. See $\mathsection$2).

Given points $O\in\mathbb{O}$ and $P\in\mathbb{P}$, the point $F\left(O\right)\in\mathbb{P}$ and the point $G\left(P\right)\in\mathbb{O}$ are called the $F$-image of $O$ and the $G$-image of $P$, respectively.

Two points $O\in\mathbb{O}$, $P\in\mathbb{P}$ are called simultaneous (or mutual or reciprocal) pre-fixed points of $F$ and $G$ if the $F$-image of $O$ is less than or equal to $P$ and the $G$-image of $P$ is less than or equal to $O$ (that is, intuitively, if “the images of the two points are less than the two points themselves”), i.e., if

[TABLE]

Simultaneous pre-fixed points are also called mutually-inductive points of $F$ and $G$. See Figure 3.1 for an illustration of simultaneous pre-fixed points.

• •

It should be immediately noted from the definition of simultaneous pre-fixed points that, generally-speaking, a single point $O\in\mathbb{O}$ can be paired with more than one point $P\in\mathbb{P}$ such that $O$ and $P$ form a single pair of simultaneous pre-fixed points of $F$ and $G$. Symmetrically, a single point $P\in\mathbb{P}$ can also be paired with more than one point $O\in\mathbb{O}$ to form such a pair. (See Figure 3.2 for an illustration.)

• •

As such, two functions $PreFP_{F,G}:\mathbb{O}\rightarrow\wp\left(\mathbb{P}\right)$ and $PreFP_{G,F}:\mathbb{P}\rightarrow\wp\left(\mathbb{O}\right)$ that compute these sets of points in $\mathbb{P}$ and $\mathbb{O}$, respectively, can be derived from $F$ and $G$. In particular, we have

[TABLE]

[TABLE]

Note that for some points $O\in\mathbb{O}$, the set $PreFP_{F,G}\left(O\right)$ can be the empty set $\phi$, meaning that such points are not paired with any points in $\mathbb{P}$ so as to form simultaneous pre-fixed points of $F$ and $G$. Symmetrically, the same observation holds for some points $P\in\mathbb{P}$ and their images $PreFP_{G,F}\left(P\right)$.666Note that in standard induction—or, more accurately, in the encoding of standard induction using mutual induction—(ultimately due to the transitivity of $\leq$ and $\sqsubseteq$) it can be said that a standard pre-fixed point $O\in\mathbb{O}$ is “paired” with one point, namely itself, to form a pair of simultaneous pre-fixed points that encodes the standard pre-fixed point. In other words, standard pre-fixed points in standard induction, when encoded as mutual induction, correspond to simultaneous pre-fixed points (e.g., using the encoding we mentioned in Footnote 5), and vice versa (i.e., simultaneous pre-fixed points, in such an encoding, will correspond to standard pre-fixed points).

Dually, two points $O\in\mathbb{O}$, $P\in\mathbb{P}$ are called simultaneous (or mutual or reciprocal) post-fixed points of $F$ and $G$ if $P$ is less than or equal to the $F$-image of $O$ and $O$ is less than or equal to the $G$-image of $P$ (that is, intuitively, if “the two points are less than their two own images”), i.e., if

[TABLE]

Simultaneous post-fixed points are also called mutually-coinductive points of $F$ and $G$.

• •

Like for simultaneous pre-fixed points, a point $O\in\mathbb{O}$ or $P\in\mathbb{P}$ can be paired with more than one point of the other poset to form a single pair of simultaneous post-fixed points of $F$ and $G$. (Similar to $PreFP_{F,G}$ and $PreFP_{G,F}$, two functions $PostFP_{F,G}:\mathbb{O}\rightarrow\wp\left(P\right)$ and $PostFP_{G,F}:\mathbb{P}\rightarrow\wp\left(O\right)$ that compute these sets can be derived from $F$ and $G$.)

Two points $O\in\mathbb{O}$, $P\in\mathbb{P}$ are called simultaneous (or mutual or reciprocal) fixed points of $F$ and $G$ if the $F$-image of $O$ is equal to $P$ and the $G$-image of $P$ is equal to $O$, i.e., if

[TABLE]

(As such, two simultaneous fixed points of $F$ and $G$ are, simultaneously, simultaneous pre-fixed points of $F$ and $G$ and simultaneous post-fixed points of $F$ and $G$.)

• •

Unlike for simultaneous pre-fixed and post-fixed points, a point in $\mathbb{O}$ or in $\mathbb{P}$ can be paired with only one point of the other poset to form a pair of simultaneous fixed points of $F$ and $G$.

Continuity

Unlike the case for standard (co)induction, where the monotonicity of generators is enough to guarantee the existence of least and greatest standard fixed points, due to the possibility of multiple pairings in $PreFP$ and $PostFP$, the monotonicity of two mutual endofunctions $F$ and $G$ seems not enough for proving the existence of least and greatest simultaneous fixed points of $F$ and $G$.777It so seemed to us in earlier versions of this paper—but now see Appendix C. However (as can be seen in the proofs in Appendix A), the continuity of the mutual endofunctions $F$ and $G$ does guarantee the existence of such fixed points. Hence, before proceeding with the formulation of mutual (co)induction we now introduce the important and useful concept of continuity.

Definition 1** (Continuous Mutual Endofunctions).**

Two mutual endofunctions $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ defined over two posets $\left(\mathbb{O},\leq\right)$ and $\left(\mathbb{P},\sqsubseteq\right)$ are continuous mutual endofunctions if and only if for all subsets $\mathbb{M}\subseteq\mathbb{O}$ and $\mathbb{N}\subseteq\mathbb{P}$ whenever greatest lower bounds (also called glbs) $\wedge\mathbb{M}\in\mathbb{O}$ and $\sqcap\mathbb{N}\in\mathbb{P}$ and least upper bounds (also called lubs) $\vee\mathbb{M}\in\mathbb{O}$ and $\sqcup\mathbb{N}\in\mathbb{P}$ exist (in $\mathbb{O}$ and in $\mathbb{P}$) then the corresponding points $\sqcap F\left(\mathbb{M}\right)\in\mathbb{P}$, $\wedge G\left(\mathbb{N}\right)\in\mathbb{O}$, $\sqcup F\left(\mathbb{M}\right)\in\mathbb{P}$, and $\vee G\left(\mathbb{N}\right)\in\mathbb{O}$ also exist (in $\mathbb{O}$ and in $\mathbb{P}$), and further, more significantly, we have

[TABLE]

[TABLE]

As such, if two mutual endofunctions $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ are continuous, then they are said to preserve the glbs and lubs in $\mathbb{O}$ and $\mathbb{P}$, whenever these points exist.888In category theory jargon, if $F$ and $G$ are continuous then $F$ and $G$ are said to commute with the meet/glb ($\wedge/\sqcap$) and join/lub ($\vee/\sqcup$) operations. (Even though somewhat similar, but the notion of continuity we use here is stricter and more uniform than the notion of Scott-continuity used in domain theory, which asserts that mappings preserve only lubs/joins of only directed subsets [32, 18, 12, 17, 15].)

Figure 3.3 illustrates meet-continuous (also called semi-continuous)* *mutual endofunctions $F$ and $G$, which preserve only the glbs in $\mathbb{O}$ and $\mathbb{P}$ whenever they exist. Dually, join-continuous mutual endofunctions preserve only the lubs in $\mathbb{O}$ and $\mathbb{P}$ whenever they exist. As such, mutual endofunctions are (fully) continuous if and only if they are meet-continuous and join-continuous.

The continuity of two mutual endofunctions has a number of useful implications, some of which we use to prove that continuity guarantees the existence of least and greatest simultaneous fixed points.

• •

First, if $F$ and $G$ are continuous mutual endofunctions then $F$ and $G$ are also monotonic mutual endofunctions (Lemma 1 in Appendix A).

• –

Note that if $F$ and $G$ are monotonic but not continuous then we can only assert that the points $F\left(\wedge\mathbb{M}\right)$ and $G\left(\sqcap\mathbb{N}\right)$ are lower bounds of the sets $F\left(\mathbb{M}\right)$ and $G\left(\mathbb{N}\right)$, but not that they are necessarily the greatest lower bounds of these sets, and we can also only assert that the elements $F\left(\vee\mathbb{M}\right)$ and $G\left(\sqcup\mathbb{N}\right)$ are upper bounds of the two sets, respectively, but not that they are necessarily the least upper bounds of these sets. More precisely, if $F$ and $G$ are monotonic, but not necessarily continuous, then we only have

[TABLE]

[TABLE]

Compared to monotonicity, as such, the continuity of $F$ and $G$ can be seen as requiring or asserting the equality of these points whenever they exist, intuitively thereby “allowing no elements in between”. Continuity, thus, is said to allow functions $F$ and $G$ that “have no jumps” or “have no surprises”.

• •

Second, if $F$ and $G$ are continuous mutual endofunctions, then the compositions $G\circ F$ and $F\circ G$ are (standard) continuous endofunctions, and they are monotonic endofunctions too (Lemma 2 in Appendix A).

• –

Further, if $\mathbb{O}$ and $\mathbb{P}$ are complete lattices, then the composition functions $G\circ F:\mathbb{O}\rightarrow\mathbb{O}$ and $F\circ G:\mathbb{P}\rightarrow\mathbb{P}$ (like any standard monotonic endofunctions over complete lattices) have standard pre-fixed points and standard post-fixed points in $\mathbb{O}$ and $\mathbb{P}$ respectively. Even further, the components $O\in\mathbb{O}$ and $P\in\mathbb{P}$ of simultaneous fixed points of $F$ and $G$ are always, each component individually, among the standard fixed points of the compositions $G\circ F$ and $F\circ G$ (Lemma 3 in Appendix A). The converse, however, does not necessarily hold.

• •

Third, if $F$ and $G$ are continuous mutual endofunctions then $F$ and $G$ (and their compositions) map complete lattices to complete lattices (note that, by definition, the empty set is not a complete lattice, and that a singleton poset is a trivial complete lattice). In other words, if subsets $\mathbb{M}\subseteq\mathbb{O}$ and $\mathbb{N}\subseteq\mathbb{P}$ happen to be complete sublattices of $\mathbb{O}$ and $\mathbb{P}$ then $F\left(\mathbb{M}\right)$ and $G\left(\mathbb{N}\right)$ are either empty or are complete sublattices of $\mathbb{P}$ and $\mathbb{O}$ respectively (Lemma 4 in Appendix A).

• •

Fourth and finally, if $F$ and $G$ are continuous mutual endofunctions, then for all $O\in\mathbb{O}$ and $P\in\mathbb{P}$ the posets $PreFP_{F,G}\left(O\right)$ and $PreFP_{G,F}\left(P\right)$ are complete lattices (Lemma 5 in Appendix A). Continuity also guarantees the existence of least simultaneous pre-fixed points (Lemma 6 in Appendix A). We use continuity to prove that the least simultaneous pre-fixed points are also the least simultaneous fixed points (** (The Simultaneous Fixed Points Theorem).** in Appendix A).999Note that singleton posets are trivial complete lattices. As such, this condition is already satisfied in an encoding of standard (co)induction using mutual (co)induction. That is because in such an encoding a given pre-fixed point is an element that is paired with precisely one element, namely itself, to form a pair of simultaneous pre-fixed points. Thus, in mutual (co)induction encodings of standard (co)induction, the sets $PreFP_{F,G}\left(O\right)$, $PreFP_{G,F}\left(P\right)$, $PostFP_{F,G}\left(O\right)$, and $PostFP_{G,F}\left(P\right)$ are always either $\phi$ or singleton posets for all $O\in\mathbb{O}$ and all $P\in\mathbb{P}$.

Having made a digression to discuss the continuity of mutual endofunctions, and some of its implications, we now resume our formulation of mutual (co)induction.

Now, if $\leq$ is a complete lattice over $\mathbb{O}$ and $\sqsubseteq$ is a complete lattice over $\mathbb{P}$ (i.e., if $\leq$ is an ordering relation where meets $\wedge$ and joins $\vee$ of all subsets of $\mathbb{O}$ are guaranteed to exist in $\mathbb{O}$, and similarly for $\sqsubseteq$, $\sqcap$, and $\sqcup$ in $\mathbb{P}$) and if $F$ and $G$ are* continuous* mutual endofunctions over $\mathbb{O}$ and $\mathbb{P}$ then we have the following:

• •

$F$ and $G$ are called simultaneous generating functions (or simultaneous generators or *mutual generators *or reciprocal generators),

• •

the *least simultaneous pre-fixed points *of $F$ and $G$, called $\mu_{F}$ and $\mu_{G}$, exist in $\mathbb{O}$ and $\mathbb{P}$,

• •

together, the points $\mu_{F}$ and $\mu_{G}$ are also the least simultaneous fixed points of $F$ and $G$ (as we prove in ** (The Simultaneous Fixed Points Theorem).**),

• •

the greatest simultaneous post-fixed points of $F$ and $G$, called $\nu_{F}$ and $\nu_{G}$, exist in $\mathbb{O}$ and $\mathbb{P}$, and

• •

together, the points $\nu_{F}$ and $\nu_{G}$ are also the greatest simultaneous fixed points of $F$ and $G$ (as we prove in ** (The Simultaneous Fixed Points Theorem).**).

Further, given that $\mu_{F}$ and $\mu_{G}$ are the least simultaneous pre-fixed points* *of $F$ and $G$ and $\nu_{F}$ and $\nu_{G}$ are the *greatest simultaneous post-fixed points *of $F$ and $G$, for any element $O\in\mathbb{O}$ and $P\in\mathbb{P}$ we have:

• •

(mutual induction)co if $F\left(O\right)\sqsubseteq P$ and $G\left(P\right)\leq O$, then $\mu_{F}\leq O$ and $\mu_{G}\sqsubseteq P$,

which, in words, means that if $O$ and $P$ are simultaneous pre-fixed/inductive/large points of $F$ and $G$, then points $\mu_{F}$ and $\mu_{G}$ are less than or equal to $O$ and $P$ (i.e., $\mu_{F}$ and $\mu_{G}$ are the smallest simultaneously-large points of $F$ and $G$), and,

• •

(mutual coinduction) if $P\sqsubseteq F\left(O\right)$ and $O\leq G\left(P\right)$, then $O\leq\nu_{F}$ and $P\sqsubseteq\nu_{G}$,

which, in words, means that if $O$ and $P$ are simultaneous post-fixed/coinductive/small points of $F$ and $G$, then points $O$ and $P$ are less than or equal to points $\nu_{F}$ and $\nu_{G}$ (i.e., $\nu_{F}$ and $\nu_{G}$ are the largest simultaneously-small points of $F$ and $G$).

4 Related Work

The work closest to the one we present here seems to be that of Paulson, presented e.g. in [26], to support the development of the Isabelle proof assistant [23]. We already mentioned in $\mathsection$1 the influence of Paulson’s work on motivating our definition of mutual coinduction (we discuss this motivation, and others, in more detail in [10]). Due to Paulson’s interest in making some form of coinduction available in systems such as Isabelle [27], Paulson was interested only in the set-theoretic definition of standard (co)induction and mutual (co)induction [24] (the set-theoretic definition, according to [27], ‘was definitely the easiest to develop, especially during the 1990s, when no general mechanisation of lattice theory was even available’).

More technically, it seems Paulson was interested in requiring generators to be monotonic (as opposed to requiring their continuity, which is sometimes viewed as an undesirably strong assumption [30, p.72]). As such, Paulson used monotonic generators over the powerset of a disjoint sum domain so as to define (or, rather, encode) mutual set-theoretic (co)induction using standard set-theoretic (co)induction101010Via noting an order-isomorphism between $\wp\left(\sum_{i}D_{i}\right)$ (the powerset of a disjoint sum) and $\prod_{i}\wp\left(D_{i}\right)$ (the product of powersets). In our opinion the use of the disjoint sum in Paulson’s definition of mutual (co)induction, while technically clever, is unnatural and unintuitive (as demonstrated, e.g., in the examples of [24, $\mathsection$4.5]).. Additionally, in [24, p.33] Paulson stated that the standard Fixed Point Theorem has been proven in Isabelle ‘only for a simple powerset lattice,’ which made Paulson limit his interests to such “simple powerset lattices,” even when the theorem applies to any complete lattice [16, 13], not just to a particular instance (i.e., not only to powerset lattices). As such, in summary, it seems to us that Paulson, for considerations related to his interests in automated theorem proving, was not interested in considering the continuity of generators in his work.

While not particularly aimed at semantics, Paulson’s work on mutual (co)induction, indirectly, provided semantics for mutual (co)inductive datatypes in functional programming languages (e.g. ML), where mutual datatype constructors were modeled by mutual generators. Functional programming languages, however, are largely structurally-typed and structurally-subtyped. Given that we have a general interest, rather, in providing semantics for datatypes in mainstream object-oriented programming languages (such as Java, C#, Scala, and Kotlin), which are typically nominally-typed and nominally-subtyped programming languages, our interest is more in the order-theoretic formulation of mutual (co)induction.111111See [7, 11], [8] and also [6, 5, 10] for a discussion of why order-theory and category-theory seem to be more suited than set-theory for modeling nominally-typed and nominally-subtyped programming languages.

Given the difference between our work and Paulson’s work regarding how mutual (co)induction is technically formulated, motivated by the different goals behind the two formulations, we anticipate that results in both works (particularly regarding the definition of simultaneous fixed points) are not in one-to-one correspondence with each other. We, however, keep a more detailed comparison of the formulation of mutual coinduction we present here to the formulation of Paulson—which may reveal more similarities and resolve some of the differences between the two formalizations—for future work.

Another work that is related to ours is the work presented in [14]. Since the work in [14] builds on that of Paulson, and has similar aims in supporting the development of Isabelle, the work in [14] adopts the same specific set-theoretic view of mutual (co)induction as that of Paulson.

5 Conclusion and Future Work

Standard induction (which includes the standard notions of mathematical induction and structural induction) is well-known, and it is relatively easy reason about. Standard coinduction is also known, but it is a bit shrouded in mystery and unreasonability121212Likely due to its strong connections with negation [21, 6].. Mutual induction is also known, if somewhat to a lesser extent than standard induction. Mutual induction is a bit harder to reason about than standard induction however. Mutual coinduction—our main interest in this paper—is, however, almost unknown, and has (so far) been perceived as being both mysterious and hard to reason about. We hope that this paper, via presenting the definition of mutual coinduction as a simple generalization of the order-theoretic definition of standard coinduction, has put mutual coinduction into more familiar light, and that, by presenting a proof of a related proof principle, it has also made mutual coinduction simpler to reason about.

While the continuity condition on generators in our formulation of mutual (co)induction is sufficient for proving the existence of least and greatest simultaneous fixed points in complete lattices (while monotonicity seems insufficient), yet it is not clear to us whether (full) continuity is necessary for such a proof. It may be useful to consider, in some future work, the possibility of relaxing the continuity condition, while still guaranteeing the existence of simultaneous fixed points. In particular, it may be useful to consider the effect of having other more liberal continuity conditions, such as Scott-continuity, on the existence of simultaneous fixed points. It may be also useful to study simultaneous pre-fixed points and simultaneous post-fixed points that are not necessarily fixed points (as is done, for example, in the study of algebras and coalgebras in category theory).

As another possible future work that can build on the definition of mutual coinduction we present here, it may be useful to consider defining infinite mutual coinduction, which, as we conceive it, generalizes mutual coinduction to involve an infinite (countable, or even uncountable!) number of orderings and generators. As of the time of this writing, we are not aware of immediate applications of infinite mutual coinduction. Given the mystery surrounding both coinduction and some particular areas of science, though, we conjecture that infinite mutual coinduction (if it is indeed reasonably definable) may have applications in areas of science such as quantum physics, e.g., by it offering mathematical models of quantum phenomena such as superposition, entanglement, and/or interference131313For example, Penrose calls in [28] for some new kind of mathematics for having an accurate understanding of our universe. Perhaps infinite mutual coinduction is a piece of such “new math.”. In agreement with this conjecture, we also intuit and conjecture that infinite mutual coinduction may have an impact on quantum computing, including reasoning about quantum programs and quantum software.

Appendix A Lemmas, Theorems and Proofs

In this appendix we present proofs for the lemmas and theorems of $\mathsection$3.

A.1 Supporting Lemmas

Lemma 1** (Continuous Functions are Monotonous).**

If $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ are continuous mutual endofunctions over posets $\left(\mathbb{O},\leq\right)$ and $\left(\mathbb{P},\sqsubseteq\right)$ then $F$ and $G$ are also monotonic, i.e., for all $O_{1},O_{2}\in\mathbb{O}$

[TABLE]

and for all $P_{1},P_{2}\in\mathbb{P}$

[TABLE]

Proof.

Let $O_{1},O_{2}\in\mathbb{O}$ such that $O_{1}\leq O_{2}$ (i.e., in Definition 1, take $\mathbb{M}=\left\{O_{1},O_{2}\right\}$ where $O_{1}\leq O_{2}$). From the definition of $\sqcap$ (as a greatest lower bound), we particularly have

[TABLE]

By the continuity of $F$, we also have $\bigsqcap F\left(\left\{O_{1},O_{2}\right\}\right)=F\left(\bigwedge\left\{O_{1},O_{2}\right\}\right)$. Given that $O_{1}\leq O_{2}$, we have $\bigwedge\left\{O_{1},O_{2}\right\}=O_{1}\wedge O_{2}=O_{1}$ and thus, further, we have $F\left(\bigwedge\left\{O_{1},O_{2}\right\}\right)=F\left(O_{1}\right)$. As such, we have $\bigsqcap F\left(\left\{O_{1},O_{2}\right\}\right)=F\left(O_{1}\right)$. Substituting for $\bigsqcap F\left(\left\{O_{1},O_{2}\right\}\right)$ (the l.h.s.) in (A.1), we get $F\left(O_{1}\right)\sqsubseteq F\left(O_{2}\right)$, as required.

Similarly for $G$. ∎

Lemma 2** (Composition Preserves Monotonicity and Continuity).**

If $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ are monotonic (continuous) mutual endofunctions over posets $\mathbb{O}$ and $P$, then the compositions $G\circ F:\mathbb{O}\rightarrow\mathbb{O}$ and $F\circ G:\mathbb{P}\rightarrow\mathbb{P}$ are monotonic (continuous) endofunctions over $\mathbb{O}$ and $\mathbb{P}$ respectively.

Proof.

By substitution, since $F\left(O_{1}\right)\in\mathbb{P}$ and $F\left(O_{2}\right)\in\mathbb{P}$ for all $O_{1},O_{2}\in\mathbb{O}$, then, by the monotonicity of $F$ then that of $G$, we have

[TABLE]

i.e., that $G\circ F$ is monotonic.

Similarly, for all $P_{1},P_{2}\in\mathbb{P}$, the monotonicity of $G$ then of $F$ implies

[TABLE]

i.e., that $F\circ G$ is monotonic.

Using a very similar but much more tedious argument we can prove that composition preserves continuity. ∎

Lemma 3** **(Components of Simultaneous Fixed Points are Standard Fixed Points

of Compositions).

If $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ are monotonic mutual endofunctions over posets $\mathbb{O}$ and $\mathbb{P}$, then the components of their simultaneous pre-/post-/fixed points are standard pre-/post-/fixed points of the compositions $G\circ F:\mathbb{O}\rightarrow\mathbb{O}$ and $F\circ G:\mathbb{P}\rightarrow\mathbb{P}$.

Proof.

For each pair of points $O\in\mathbb{O}$ and $P\in\mathbb{P}$ of simultaneous pre-fixed points of $F$ and $G$, by the definition of simultaneous pre-fixed points we have both inequalities

[TABLE]

Applying $G$ to both sides of the first inequality, the monotonicity of $G$ implies that $G\left(F\left(O\right)\right)\leq G\left(P\right)$.141414Note that continuity is not needed here. Combining this with the second inequality via the common expression $G\left(P\right)$, we have

[TABLE]

Then, by the transitivity of $\leq$,

[TABLE]

i.e., point $O$ is a standard pre-fixed point of the composition $G\circ F$.

Symmetrically, by applying $F$ to both sides of the second inequality, the monotonicity of $F$ implies that

[TABLE]

and thus, by the transitivity of $\sqsubseteq$, point $P$ is a standard pre-fixed point of the composition $F\circ G$. (See Figure A.1 for illustration.)

A dual argument implies that components of simultaneous post-fixed points of $F$ and $G$ are standard post-fixed points of $G\circ F$ and $F\circ G$ respectively.

Combining both results implies that components of simultaneous fixed points of $F$ and $G$ are also standard fixed points of $G\circ F$ and $F\circ G$. ∎

Lemma 4** (Continuous Functions Preserve Complete Lattices).**

If $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ are continuous mutual endofunctions over posets $\mathbb{O}$ and $\mathbb{P}$, then for all subsets $\mathbb{M}\subseteq\mathbb{O}$ and $\mathbb{N}\subseteq\mathbb{P}$, if $\mathbb{M}$ and $\mathbb{N}$ are complete sublattices of $\mathbb{O}$ and $\mathbb{P}$ then the images $F\left(\mathbb{M}\right)$ and $G\left(\mathbb{N}\right)$ are also complete sublattices of $\mathbb{P}$ and $\mathbb{O}$, respectively.

Proof.

First, let’s consider the case where $\mathbb{M}\subseteq\mathbb{O}$ is a complete lattice. By the definition of a complete lattice, the points $\wedge\mathbb{A}$ and $\vee\mathbb{A}$ exist in $\mathbb{M}$ for all subsets $\mathbb{A}\subseteq\mathbb{M}$. As such, the points $F\left(\wedge\mathbb{A}\right)$ and $F\left(\vee\mathbb{A}\right)$ exist in $\mathbb{P}$, and, accordingly, by the definition of $F\left(\mathbb{M}\right)$, are also members of $F\left(\mathbb{M}\right)$. By the continuity of $F$, we also have $F\left(\wedge\mathbb{A}\right)=\sqcap F\left(\mathbb{A}\right)$ and $F\left(\vee\mathbb{A}\right)=\sqcup F\left(\mathbb{A}\right)$. As such, for any image set $F\left(\mathbb{A}\right)\subseteq\mathbb{P}$ a greatest lower bound, $\sqcap F\left(\mathbb{A}\right)$, and a least upper bound, $\sqcup F\left(\mathbb{A}\right)$, exist. Further, because of the continuity of $F$, these two points are members of $F\left(\mathbb{M}\right)$. Thus, all subsets of $\mathbb{M}$ have images of their glbs and lubs in $F\left(\mathbb{M}\right)$. That by itself does not, however, prove that the set $F\left(\mathbb{M}\right)$ is a complete lattice, yet.

To prove that $F\left(\mathbb{M}\right)$ is a complete lattice, we have to prove that the points $\sqcap\mathbb{B}$ and $\sqcup\mathbb{B}$ exist in $F\left(\mathbb{M}\right)$ for all sets $\mathbb{B}\subseteq F\left(\mathbb{M}\right)\subseteq\mathbb{P}$. Given that $\mathbb{B}$ is subset of $F\left(\mathbb{M}\right)$, the image of $\mathbb{M}$, then there exists some (one or more) set $\mathbb{A}\subseteq\mathbb{M}$ such that $F\left(\mathbb{A}\right)=\mathbb{B}$. Pick one such set $\mathbb{A}$.151515Sounds like the Axiom of Choice is needed here. Then, for that particular $\mathbb{A}$, we have $\sqcap\mathbb{B}=\sqcap F\left(\mathbb{A}\right)$ and $\sqcup\mathbb{B}=\sqcup F\left(\mathbb{A}\right)$. Since we proved that for all sets $\mathbb{A}\subseteq\mathbb{M}$ the points $\sqcap F\left(\mathbb{A}\right)$ and $\sqcup F\left(\mathbb{A}\right)$ are members of $F\left(\mathbb{M}\right)$, we conclude that $\sqcap\mathbb{B}$ and $\sqcup\mathbb{B}$ are members of $F\left(\mathbb{M}\right)$ for all sets $\mathbb{B}\subseteq F\left(\mathbb{M}\right)$. As such, the set $F\left(\mathbb{M}\right)$ is a complete lattice.

Next, by a symmetric argument, if $\mathbb{N}\subseteq\mathbb{P}$ is a complete lattice then, by the continuity of $G$, the set $G\left(\mathbb{N}\right)$ is also a complete lattice, as required. ∎

Lemma 5** **(Component Images of Simultaneous Pre-/Post-Fixed Points form Complete

Lattices).

If $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ are continuous mutual endofunctions over complete lattices $\mathbb{O}$ and $\mathbb{P}$, then, for all $O\in\mathbb{O}$ and $P\in\mathbb{P}$, the component image sets $PreFP_{F,G}\left(O\right)$, $PreFP_{G,F}\left(P\right)$, $PostFP_{F,G}\left(O\right)$, and $PostFP_{G,F}\left(P\right)$, as defined in $\mathsection$3,* are either empty or are complete lattices.*

Proof.

For a point $O\in\mathbb{O}$ such that $PreFP_{F,G}\left(O\right)$ is nonempty, define

[TABLE]

Since $\mathbb{P}$ is a complete lattice, the set $\mathbb{P}_{O}$ (as a subset of $\mathbb{P}$) has a greatest lower bound $\sqcap\mathbb{P}_{O}$ and a least upper bound $\sqcup\mathbb{P}_{O}$ that are members of $\mathbb{P}$. To prove that $\mathbb{P}_{O}$ itself is a complete lattice, first we prove that these two points (i.e., the glb and lub of $\mathbb{P}_{O}$) are members of $\mathbb{P}_{O}$.

Let’s note that for all points $O$ where $\mathbb{P}_{O}$ is non-empty we always have the point $F\left(O\right)$ as a member of $\mathbb{P}_{O}$. That’s because, by the reflexivity of $\sqsubseteq$, we have $F\left(O\right)\sqsubseteq F\left(O\right)$. Further, using Lemma 3, we have $G\left(F\left(O\right)\right)\leq O$. As such, by the definition of simultaneous pre-fixed points, the points $O\in\mathbb{O}$ and $F\left(O\right)\in\mathbb{P}$ are simultaneous pre-fixed points of $F$ and $G$.161616This brings one of the most delicate points in proving the mutual (co)induction principles. Note that $O$ and $F\left(O\right)$ are not necessarily simultaneous pre-fixed points for all $O\in\mathbb{O}$, but that, according to Lemma 3, points $O$ and $F\left(O\right)$ are simultaneous pre-fixed points only whenever there is some $P\in\mathbb{P}$ (possibly equal to $F\left(O\right)$, and possibly not) such that $O$ and $P$ are simultaneous pre-fixed points of $F$ and $G$, i.e., such that $P$ witnesses, via $G\left(P\right)$, that $G\left(F\left(O\right)\right)\leq O$. In particular, it is not necessarily true that for all $O\in\mathbb{O}$ we have $G\left(F\left(O\right)\right)\leq O$ (Otherwise, all elements $O\in\mathbb{O}$ would have formed simultaneous pre-fixed points of $F$ and $G$, simply by pairing each $O$ with $F\left(O\right)$. This goes counter to intuitions about mutual (co)induction, since it would eventually lead to concluding that all points of $\mathbb{O}$—and similarly of $\mathbb{P}$—are simultaneous fixed points of $F$ and $G$!). Readers should be aware of this delicate and tricky point specific to mutual (co)induction. That’s because this point has no counterpart in standard (co)induction (or, at least, has no obvious counterpart, since in an encoding of standard (co)induction using mutual (co)induction, where say $G=\mathbf{1}$, we will have $G\left(F\left(O\right)\right)=F\left(O\right)\leq O$ only if $F\left(O\right)\leq O$). Hence, $F\left(O\right)\in\mathbb{P}_{O}$. Given that, by the definition of $\mathbb{P}_{O}$, the point $F\left(O\right)$ is less than or equal to all members of $\mathbb{P}_{O}$, we have

[TABLE]

and, as such, the greatest lower bound of $\mathbb{P}_{O}$ is a member of $\mathbb{P}_{O}$, i.e., we have $\sqcap\mathbb{P}_{O}\in\mathbb{P}_{O}$ as needed.

For $\sqcup\mathbb{P}_{O}$, we prove that it is a member of $\mathbb{P}_{O}$ more directly, using the definition of $\mathbb{P}_{O}$ and the continuity of $G$. As for any member of $\mathbb{P}$, for $\sqcup\mathbb{P}_{O}$ to be a member of $\mathbb{P}_{O}$ we must have $F\left(O\right)\sqsubseteq\sqcup\mathbb{P}_{O}$ and $G\left(\sqcup\mathbb{P}_{O}\right)\leq O$. The first condition is satisfied since we just proved that $F\left(O\right)$ is exactly $\sqcap\mathbb{P}_{O}$, and, as for any set, we have $\sqcap\mathbb{P}_{O}\sqsubseteq\sqcup\mathbb{P}_{O}$ whenever such points exist, and as such we have $F\left(O\right)\sqsubseteq\sqcup\mathbb{P}_{O}$. For the second condition (this is where continuity is needed), we have $G\left(\sqcup\mathbb{P}_{O}\right)=\vee G\left(\mathbb{P}_{O}\right)$ by continuity. Since, by the definition of $\mathbb{P}_{O}$, all members of $G\left(\mathbb{P}_{O}\right)$ are less than or equal to $O$, then $O$ is an upper bound of $G\left(\mathbb{P}_{O}\right)$. As such, we have $\vee G\left(\mathbb{P}_{O}\right)\leq O$. Hence, for $\sqcup\mathbb{P}_{O}$, we have $G\left(\sqcup\mathbb{P}_{O}\right)=\vee G\left(\mathbb{P}_{O}\right)\leq O$, as required. Hence, $\sqcup\mathbb{P}_{O}\in\mathbb{P}_{O}$ as needed.

Since the greatest lower bound of $\mathbb{P}_{O}$ and the least upper bound of $\mathbb{P}_{O}$ are members of $\mathbb{P}_{O}$, so far we can assert that the set $\mathbb{P}_{O}=PreFP_{F,G}\left(O\right)$ is a bounded poset.

To prove that $\mathbb{P}_{O}$ is not only a bounded poset but, rather, that it is a complete lattice, we have to also consider proper subsets of $\mathbb{P}_{O}$. The argument for proper subsets of $\mathbb{P}_{O}$ is very similar to the one we just used for $\mathbb{P}_{O}$ (as an improper subset of itself). In particular, let $\mathbb{N}\subset\mathbb{P}_{O}$ be some proper subset of $\mathbb{P}_{O}$ (i.e., is some set of points of $\mathbb{P}$ that, paired with $O$, are simultaneous pre-fixed points of $F$ and $G$). Again, since $\mathbb{P}$ is a complete lattice, the elements $\sqcap\mathbb{N}$ and $\sqcup\mathbb{N}$ exist. We proceed to prove that these points are also members of $\mathbb{P}_{O}$.

In particular, to be members of $\mathbb{P}_{O}$ the two points $\sqcap\mathbb{N}$ and $\sqcup\mathbb{N}$ have to satisfy the membership condition of $\mathbb{P}_{O}$, i.e., they have to form, when paired with $O$, simultaneous pre-fixed points of $F$ and $G$. Again using the continuity of $G$, we can see that this is true since, like we had for $\sqcap\mathbb{P}_{O}$ and $\sqcup\mathbb{P}_{O}$, we have

[TABLE]

[TABLE]

As such, points $\sqcap\mathbb{N}$ and $\sqcup\mathbb{N}$ are members of $\mathbb{P}_{O}$. Thus, $\mathbb{P}_{O}$ is a complete lattice.

Using a symmetric argument and the continuity of $F$, we can also prove that the set $\mathbb{O}_{P}=PreFP_{G,F}\left(P\right)$ is either empty or is a complete lattice for all $P\in\mathbb{P}$. (Figure A.1 illustrates the sets $\mathbb{P}_{O}$ and $\mathbb{O}_{P}$.)

Dually, we can also prove that, for all $O\in\mathbb{O}$ and $P\in\mathbb{P}$, the sets $PostFP_{F,G}\left(O\right)$ and $PostFP_{G,F}\left(P\right)$ are either empty or are complete lattices, as required. ∎

Lemma 6** (Components of Pre-/Post-Fixed Points form Complete Lattices).**

If $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ are continuous mutual endofunctions over complete lattices $\mathbb{O}$ and $\mathbb{P}$, then the sets

[TABLE]

[TABLE]

of all components of simultaneous pre-fixed points are complete sublattices of $\mathbb{O}$ and $\mathbb{P}$, respectively. Similarly for simultaneous post-fixed points.

Proof.

First, let’s note that the definitions of $\mathbb{C}$ and $\mathbb{D}$ mean that $\mathbb{C}$ is the set of all $O\in\mathbb{O}$ where there is some $P\in\mathbb{P}$ such that the $F$-image of $O$ is less than $P$ and the $G$-image of $P$ is less than $O$ and, symmetrically, that $\mathbb{D}$ is the set of all $P\in\mathbb{P}$ where there is some $O\in\mathbb{O}$ such that the $F$-image of $O$ is less than $P$ and the $G$-image of $P$ is less than $O$. (As such, the variables $O$ and $P$ in Equations (A.2) and (A.3) range over the set of all simultaneous pre-fixed points of $F\textrm{ and }G$.)

Note also that $\mathbb{C}=\bigcup_{P\in\mathbb{P}}PreFP_{G,F}\left(P\right)$ and $\mathbb{D}=\bigcup_{O\in\mathbb{O}}PreFP_{F,G}\left(O\right)$, but that Lemma 5 does not (by itself) imply that $\mathbb{C}$ and $\mathbb{D}$ are complete lattices, since the union of complete lattices is not necessarily a complete lattice.

We do proceed, though, similarly to first prove that $\mathbb{C}$ is a meet-complete lattice. Particularly, assuming $\mathbb{A}\subseteq\mathbb{C}$, we prove that $\bigwedge\mathbb{A}\in\mathbb{C}$. Since $\mathbb{O}$ is a complete lattice, the point $\bigwedge\mathbb{A}$ exists in $\mathbb{O}$, and since $\mathbb{A}$ is a subset of $\mathbb{C}$ then the image set $F\left(\mathbb{A}\right)$ is a subset of $\mathbb{D}$ (by the definition of $\mathbb{D}$). By continuity, we have $F\left(\bigwedge\mathbb{A}\right)=\bigsqcap F\left(\mathbb{A}\right)$. Also, let the set

[TABLE]

be the set of all points in $\mathbb{P}$ that form simultaneous pre-fixed points when paired with some point in $\mathbb{A}$. Given that for each point $B\in\mathbb{B}$ there exists a point $A\in\mathbb{A}$ such that $F\left(A\right)\in F\left(\mathbb{A}\right)$ and $F\left(A\right)\sqsubseteq B$ (by the definition of simultaneous fixed points), then the meet of all points $F\left(A\right)$ is less than or equal to the meet of all points $B$, i.e., we have $\bigsqcap F\left(\mathbb{A}\right)\sqsubseteq\bigsqcap\mathbb{B}$. Using a similar argument, we also have $\bigwedge G\left(\mathbb{B}\right)\leq\bigwedge\mathbb{A}$. By continuity, substituting for $\bigsqcap F\left(\mathbb{A}\right)$and $\bigwedge G\left(\mathbb{B}\right)$ we have

[TABLE]

As such, for all $\mathbb{A}\subseteq\mathbb{C}$, the point $\bigwedge\mathbb{A}$, when paired with the point $\bigsqcap\mathbb{B}$, forms a pair of simultaneous pre-fixed points of $F$ and $G$, and is thus a member of $\mathbb{C}$. As such, $\mathbb{C}$ is a meet-complete lattice. (Figure A.2 illustrates the proof for subsets of $\mathbb{C}$ and $\mathbb{D}$ that have two elements.)

Dually, we can prove that set $\mathbb{C}$ is also a join-complete lattice (with the point $\top_{\mathbb{O}}$, the top element of $\mathbb{O}$, at its top). Hence, set $\mathbb{C}$ is a meet-complete lattice and a join-complete lattice, i.e., is a complete lattice.

Symmetrically, or by using Lemma 4, we can prove that set $\mathbb{D}$ also is a complete lattice (with the point $\top{}_{\mathbb{P}}$, the top element of $\mathbb{P}$, at its top). As such, the sets of all components of simultaneous pre-fixed points are complete lattices.

Dually, we can also prove that the two sets $\mathbb{E}$ and $\mathbb{F}$ of all components of simultaneous post-fixed points—i.e., duals of sets $\mathbb{C}$ and $\mathbb{D}$—are complete lattices (with the points $\bot_{\mathbb{O}}$ and $\bot_{\mathbb{P}}$ at their bottom), as required. ∎

A.2 The Simultaneous Fixed Points Theorem

The following theorem, asserting the existence of least and greatest simultaneous fixed points, is the central theorem of this paper.171717To the best of our knowledge, neither mutual (co)induction as we define it in this paper nor a proof of the Simultaneous Fixed Points Theorem have been presented formally before.

Theorem 1** (The Simultaneous Fixed Points Theorem).**

If $\left(\mathbb{O},\leq,\wedge,\vee\right)$ and $\left(\mathbb{P},\sqsubseteq,\sqcap,\sqcup\right)$ are two complete lattices and $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ are two continuous mutual endofunctions (i.e., two simultaneous generators) over $\mathbb{O}$ and $\mathbb{P}$ then we have the following:

• •

the *least simultaneous pre-fixed points *of $F$ and $G$, called $\mu_{F}$ and $\mu_{G}$, exist in $\mathbb{O}$ and $\mathbb{P}$,

• •

$\mu_{F}$ and $\mu_{G}$ are also the least simultaneous fixed points of $F$ and $G$,

• •

the greatest simultaneous post-fixed points of $F$ and $G$, called $\nu_{F}$ and $\nu_{G}$, exist in $\mathbb{O}$ and $\mathbb{P}$, and

• •

$\nu_{F}$ and $\nu_{G}$ are also the greatest simultaneous fixed points of $F$ and $G$.

Proof.

Let the set

[TABLE]

and the set

[TABLE]

be the sets of all components of simultaneous pre-fixed points of $F$ and $G$, and let points $\mu_{F}\textrm{ and }\mu_{G}$ be defined as

[TABLE]

By Lemma 6, points $\mu_{F}\textrm{ and }\mu_{G}$ are guaranteed to exist as the least elements of $\mathbb{C}$ and $\mathbb{D}$. By the antisymmetry of $\leq$ and $\sqsubseteq$, we can conclude that

[TABLE]

First, we note that $F\left(\mu_{F}\right)\sqsubseteq\mu_{G}$ because $\mu_{F}$ is the least element of $\mathbb{C}$ and thus, according to the definition of simultaneous pre-fixed points (and as noted in the proof of Lemma 5), its image $F\left(\mu_{F}\right)$ is less than any element of $\mathbb{D}$, including the point $\mu_{G}$, but, second, also we note that $\mu_{G}\sqsubseteq F\left(\mu_{F}\right)$ since $\mu_{G}$ is the least element of $\mathbb{D}$ and thus is less than any point in $\mathbb{D}$, including the point $F\left(\mu_{F}\right)$. By the antisymmetry of $\sqsubseteq$, we conclude that $F\left(\mu_{F}\right)=\mu_{G}$.

Symmetrically, we also have $G\left(\mu_{G}\right)=\mu_{F}$.

As such, the points $\mu_{F}$ and $\mu_{G}$ are simultaneous fixed points of $F$ and $G$. They are also the least simultaneous pre-fixed points of $F$ and $G$ since, by Equation (A.6), less-demandingly we have

[TABLE]

meaning that points $\mu_{F}$ and $\mu_{G}$ are simultaneous pre-fixed points of $F$ and $G$, and, by the individual uniqueness and minimality of each of $\mu_{F}$ and $\mu_{G}$ (as the meets of the complete lattices $\mathbb{C}$ and $\mathbb{D}$), points $\mu_{F}$ and $\mu_{G}$ are the least such points.

Now we have established both that $\mu_{F}\textrm{ and }\mu_{G}$ form the least simultaneous pre-fixed points of $F$ and $G$, and that $\mu_{F}\textrm{ and }\mu_{G}$ are simultaneous fixed points of $F$ and $G$, so $\mu_{F}\textrm{ and }\mu_{G}$ are the least simultaneous fixed points of $F$ and $G$.

Using a dual argument, we can also prove that $\nu_{F}=\vee\mathbb{E}\textrm{ and }\nu_{G}=\sqcup\mathbb{F}$, where sets $\mathbb{E}$ and $\mathbb{F}$ are the duals of sets $\mathbb{C}$ and $\mathbb{D}$ (see proof of Lemma 6), are the greatest simultaneous fixed points of $F\textrm{ and }G$, as required. ∎

Appendix B Motivations from PL Theory

The significance of mutually-recursive definitions in programming languages (PL) semantics and PL type theory is illustrated in the following examples.

B.1 Mutual Recursion at The Level of Data Values

Lawrence Paulson, in his well-known book ‘ML for the Working Programmer’ [25, p.58], made some intriguing assertions, and presented an intriguing code example. According to Paulson, “Functional programming and procedural programming are more alike than you may imagine”—a statement that some functional programmers today are either unaware of, may oppose, or may silently ignore. Paulson further states, verbatim, that “Any combination of goto and assignment statements — the worst of procedural code — can be translated to a set of mutually recursive functions.”

Then Paulson presents a simple example of imperative code. Here it is.

• ⬇

var x := 0; y := 0; z := 0;

F: x := x+1; goto G

G: if y<z then goto F else (y := x+y; goto H)

H: if z>0 then (z := z-x; goto F) else stop

To convert this imperative code into pure functional code, Paulson then suggests: “For each of the labels, F, G, and H, declare mutually recursive functions. The argument of each function is a tuple holding all of the variables.”

Here’s the result when the method is applied to the imperative code above:

• ⬇

fun F(x,y,z) = G(x+1,y,z)

and G(x,y,z) = if y<z then F(x,y,z) else H(x,x+y,z)

and H(x,y,z) = if z>0 then F(x,y,z-x) else (x,y,z);

Calling F(0,0,0) gives x, y, and z their initial values for execution, and returns (1,1,0)—the result of the imperative code. As such, Paulson concludes that: “Functional programs are referentially transparent, yet can be totally opaque”— a statement which we read to mean that, for PL theorists in general if not also for many mathematicians, functional programs (FP) are [usually] easy to reason about, yet can [sometimes] be very hard to reason about. Then Paulson concludes his discussion by sounding the siren: “If your code starts to look [sic] like this, beware!”

We can also introduce object-oriented programming (OOP) in this discussion. In particular, a possible translation of Paulson’s imperative code to (non-imperative) OO code is as follows (in [1] we present a translation to a slightly more-succinct imperative OO code):

• ⬇

class C {

final x, y, z: int

// constructor

C(xx,yy,zz: int) { x = xx; y = yy; z = zz }

C F() { new C(x+1,y,z).G() }

C G() {

**if** y < z then **this**.F()

**else** **new** C(x,x+y,z).H() }

C H() {

**if** z > 0 then **new** C(x, y, z-x).F()

**else** **this** }

}

Now, similar to Paulson’s functional program, calling new C(0,0,0).F() gives the fields x, y, and z their initial values for execution, and returns an object equivalent to new C(1,1,0)—i.e., equivalent to the result of the imperative code.

Pondering a little over some of the “worst” imperative code and over its translations to mutually-recursive functional and object-oriented code suggests a strong similarity—if not equivalence—between OOP, mutually-recursive FP, and procedural/imperative programming. Further, this discussion implies that the mathematical-reasoning benefits of functional programming—particularly the relative simplicity of such reasoning—seem to crucially depend on not heavily using mutually-recursive function definitions (Paulson’s concluding warning can be read as an explicit warning against writing heavily mutually-recursive functional code). As the imperative code and the OOP translation illustrate, and as is commonly known among mainstream and industrial-strength software developers, however, heavily mutually recursive definitions seem to be an essential and natural feature of real-world/industrial-strength programming.

More significantly, the above translation between imperative, functional and object-oriented code seems to also tell us that:

if mutually-recursive functional programs can be reasoned about mathematically,

then also imperative and object-oriented programs (even the worst such programs)

can be reasoned about mathematically.

A main objective behind the formal definition of mutual (co)induction in this paper is to help in reasoning about mutually-recursive functional programs mathematically (possibly making it even as simple as reasoning about standard recursive functional programs is, based on using the standard (co)induction principles), and, ultimately, to thereby possibly help in reasoning about (even the worst?) imperative and object-oriented programs mathematically too.

It should be noted that sometimes it is possible to reexpress mutual recursion (also called indirect recursion) or convert it into standard recursion (also called direct recursion), e.g., using the inlining conversion method presented in [19, 34] or ‘with the help of an additional argument’ as suggested by Paulson also in [25, p.58]. From the results in [19, 34], however, not all mutual recursion can be converted to standard recursion. Extending from these results, while it is possible that some mutual (co)inductive definitions can be converted to or encoded using standard (co)inductive definitions, we conjecture that not all mutual (co)induction can be translated into standard (co)induction. Hence, the need arises for a genuine formal definition of mutual (co)induction that does not involve an encoding or translation of it into terms of standard (co)induction.

B.2 Mutual Recursion at The Level

of Data Types

The previous section discussed mutual recursion at the level of values (i.e., mutually-recursive data values, functions, or methods). As is well-known in PL type theory, mutually-recursive types are essential for typing mutually-recursive data values [22, 29]. Given the ubiquity of mutually-recursive data values in OOP (via the special variable this/self), mutually-recursive data types and mutually-recursive data type constructors (e.g., classes, interfaces, traits, … etc.) are ubiquitous in industrial-strength statically-typed OOP as well (e.g., in Java, C#, C++, Kotlin, and Scala).

Further, in generic OOP languages such as Java, variance annotations (such as wildcard types in Java) can be modeled by and generalized to interval types [4]. As presented in [4], the definition of ground types in Java depends on the definition of interval types, whose definition, circularly (i.e., mutually-recursively), depends on the definition of ground types. Further, the subtyping relation between ground types depends on the containment (also called subintervaling or interval inclusion) relation between interval types, and vice versa. As such, the set of ground types and the set of interval types in Java are examples of mutual recursive sets, and the subtyping and the containment relations over these sets, respectively, are mutually recursive relations too. (See [3, 4] for how, under an inductive interpretation, both sets—types and interval types—and both relations—subtyping and containment—can be iteratively constructed from the given set of classes of a Java program together with the subclassing relation between these classes).

To illustrate all aspects of mutual recursion in OOP (i.e., at the level of type, at the level of values, and in defining types/subtyping and interval types/containment), the following OO code, written in an imaginary Java-like language, presents a simple set of mutually recursive classes to model the mutual recursion between in the definition of types and interval types.

• ⬇

class Class {

String name; // holds the name of the class

}

class Type {

Class c;

Interval i; // the type arg of c. null if c is not generic

}

class Interval {

Type UBnd; // the upper bound of the interval type

Type LBnd; // its lower bound

}

// Note the mutual recursion (at the level of types) between

// the definitions of classes Type and Interval

And the following code adds to the code above a simple set of mutually recursive methods to model the mutual recursion in the definitions of the subtyping and containment relations.

• ⬇

class Class {

String name;

bool isSubclassOf(Class c) {

*// Handle special classes Null and Object*

**if**(**this** == NullCls || c == ObjCls) **return** **true**;

*// Else check if this class inherits from class c*

**return** inher_table.lookup(**this**, c);

}

}

⬇

class Type {

Class c;

Interval i;

bool isSubtypeOf(Type t){

*// assuming that i and t.i are not null,*

*//   ie, that c and t.c are generic*

**return** c.isSubclassOf(t.c) && i.isSubintOf(t.i)

}

}

⬇

class Interval {

Type UBnd;

Type LBnd;

bool isSubint(Interval i){

*// covar in upperbound, contravar in lower bound*

**return** UBnd.isSubtypeOf(i.UBnd) && i.LBnd.isSubtypeOf(LBnd)

}

}

// Note the mutual recursion (at the level of values) between

// the definitions of methods isSubtypeOf and isSubintOf

B.3 Mutual Coinduction in OOP

As discussed in detail in $\mathsection$B.2, mutually recursively definitions exist in OOP at two levels: at the level of values (via this) and at the level of types (i.e., between classes, and in the definition of the subtyping and containment relations). It should be noted that the subtyping relation is covariant/monotonic w.r.t. containment, and that containment is covariant w.r.t. subtyping in the first argument (i.e., w.r.t. the upper bound of an interval type) and is contravariant w.r.t. the second argument (i.e., w.r.t. the lower bound of an interval type). As such, in Java with interval types, subintervals generates subtypes, and subtypes in the upper bounds of interval types generates subintervals, while subtypes in the lower bounds of interval types generates superintervals. .

Just as for standard (co)induction, where the notions of (least) pre-fixed points and (greatest) post-fixed points have relevance and practical value even when such points do *not *correspond to fixed points, e.g., when the underlying posets are not complete lattices or when the generators are not monotonic (see, for example, [5, 2]), we expect that the notions of (least) simultaneous pre-fixed points and (greatest) post-fixed points to have relevance and practical value even when these points do not correspond to simultaneous fixed points, e.g., when the underlying posets are not complete lattices or when the generators are not continuous (and may not be even monotonic).

Appendix C Requiring Only Monotonicity

While the proofs presented in Appendix A are correct, and the continuity of simultaneous/mutual generators does indeed guarantee the existence of least and greatest simultaneous fixed points in complete lattices, but, as we suggested in Section 5, in this appendix we explain how indeed monotonicity of the generators alone is enough to prove the existence of least and greatest simultaneous fixed points, thereby relaxing the condition on generators.

The first hint that monotonicity is enough (that in fact is not just a hint but is a proof, albeit an indirect one) comes from the fact that monotonic mutual generators over complete lattices can be represented or encoded, in a standard way, as one monotonic generator over one complete lattice, for which a (standard) least and greatest fixed point is guaranteed to exist (by the standard Knaster-Tarski theorem), and in which the least fixed point and the greatest fixed point correspond directly to the least simultaneous fixed point and the greatest simultaneous fixed point of the original mutual generators.

In particular, as in Appendix A, let $F:\mathbb{O}\rightarrow\mathbb{P}$ and $G:\mathbb{P}\rightarrow\mathbb{O}$ be two monotonic mutual generators over complete lattices $\mathbb{O}$ and $\mathbb{P}$. Then the product $\mathbb{OP}\doteq\mathbb{O}\times\mathbb{P}$ is also a complete lattice under the standard component-wise ordering (i.e., where $\left(o_{1},p_{1}\right)\leq\left(o_{2},p_{2}\right)\mathrm{\,iff\,}o_{1}\leq o_{2}\wedge p_{1}\sqsubseteq p_{2}$). Further, the function $H\left(o,p\right):\mathbb{OP}\rightarrow\mathbb{OP}\doteq\left(G\left(p\right),F\left(o\right)\right)$ is a monotonic function over $\mathbb{OP}$ (given the monotonicity of $F$ and $G$). As such, by the standard Knaster-Tarski theorem, function $H$ is a generator over the complete lattice $\mathbb{OP}$ that has a least fixed point $\mu_{\mathbb{OP}}=\left(\mu_{\mathbb{O}},\mu_{\mathbb{P}}\right)$ and a greatest fixed point $\nu_{\mathbb{OP}}=\left(\nu_{\mathbb{P}},\nu_{\mathbb{P}}\right)$. Given our definition of a simultaneous pre-fixed point $\left(o,p\right)$ of $F$ and $G$ (as one where $G\left(p\right)\leq o\wedge F\left(o\right)\sqsubseteq p$) implies that $\mu_{\mathbb{OP}}$(the least fixed point of $H$) is a simultaneous pre-fixed point of $F$ and $G$, is the least such point, and, thus, is also the least simultaneous fixed point of $F$ and $G$. Similarly, we can conclude that $\nu_{\mathbb{OP}}$ (the greatest fixed point of $H$) is the greatest simultaneous fixed point of $F$ and $G$.

It should be noted, though, that while this proof does not require the continuity of $F$ and $G$, it only indirectly constructs the least and greatest simultaneous fixed points of $F$and $G$ as decodings of the least and greatest fixed points of another function ($H$). Below we present a more direct proof of the existence of these simultaneous fixed points that does not depend on the conclusion of the standard Knaster-Tarski theorem, and that also discusses the issue of multiplicity of pairings in simultaneous pre-fixed and simultaneous post-fixed points (which we discussed in Section 3, and led us to consider using continuity). We believe our next proof, while more intricate and involved that the encoding proof, does reveal a bit more about the structure and the inner workings of mutual (co)induction than a standard encoding of mutual (co)induction in terms of standard (co)induction does.

As an appetizer and source of intuition, let’s first note the following lemma.

Lemma 7** **(The lub (glb) of components of simultaneous pre(post)-fixed (post-fixed)

points forms a simultaneous pre(post)-fixed point.).

Given the definitions of Theorem (1), if $\left(o,p_{1}\right)$ and $\left(o,p_{2}\right)$ are two simultaneous pre-fixed points then, by the monotonicity of G, $\left(o,p_{1}\sqcap p_{2}\right)$ is a simultaneous pre-fixed point, and, dually, if $\left(o,q_{1}\right)$ and $\left(o,q_{2}\right)$ are two simultaneous post-fixed points then, by monotonicity of $F$, $\left(o,q_{1}\sqcup q_{2}\right)$ is a simultaneous post-fixed point.

Further, if $\left(o_{1},p_{1}\right)$ and $\left(o_{2},p_{2}\right)$ are two simultaneous pre-fixed points then, by the monotonicity of G, $\left(o_{1}\wedge o_{2},p_{1}\sqcap p_{2}\right)$ is a simultaneous pre-fixed point, and, dually, if $\left(o_{1},q_{1}\right)$ and $\left(o_{2},q_{2}\right)$ are two simultaneous post-fixed points then, by the monotonicity of $F$, $\left(o_{1}\vee o_{2},q_{1}\sqcup q_{2}\right)$ is a simultaneous post-fixed point as well.

Proof.

We have $G\left(p_{1}\right)\leq o$ and $F\left(o\right)\sqsubseteq p_{1}$ and $G\left(p_{2}\right)\leq o$ and $F\left(o\right)\sqsubseteq p_{2}$, which means $F\left(o\right)$ is a lower bound of $p_{1}$ and $p_{2}$ but $p_{1}\sqcap p_{2}$ is the greatest lower bound and hence $F\left(o\right)\sqsubseteq p_{1}\sqcap p_{2}$ (1). By the monotonicity of $G$, $p_{1}\sqcap p_{2}\sqsubseteq p_{1}\implies G\left(p_{1}\sqcap p_{2}\right)\leq G\left(p_{1}\right)$, and thus, by transitivity, we have $G\left(p_{1}\sqcap p_{2}\right)\leq o$ (2). Combining (1) and (2), the pair $\left(o,p_{1}\sqcap p_{2}\right)$ is a simultaneous pre-fixed point too. (Trying to do this for $p_{1}\sqcup p_{2}$ fails since monotonicity does not necessitate that $G\left(p_{1}\sqcup p_{2}\right)\leq o,$but continuity does … and to prove the existence of a least simultaneous fixed point this extra requirement is actually not needed).

Dually, the monotonicity of $G$ also can be used to prove that $o\leq G\left(q_{1}\right)$ and $q_{1}\sqsubseteq F\left(o\right)$ and $o\leq G\left(q_{2}\right)$ and $q_{2}\sqsubseteq F\left(o\right)$ implies that $q_{1}\sqcup q_{2}\sqsubseteq F\left(o\right)$ ($F\left(o\right)$ is greater than or equal the least upper bound of $q_{1}$ and $q_{2}$) and that $o\leq G\left(q_{1}\right)\leq G\left(q_{1}\sqcup q_{2}\right)$ and, hence, that $\left(o,q_{1}\sqcup q_{2}\right)$ is a simultaneous post-fixed point. ∎

Similarly, by the monotonicity of $F$, if $\left(n_{1},p\right)$ and $\left(n_{2},p\right)$ are simultaneous pre-fixed points then $\left(n_{1}\wedge n_{2},p\right)$ is a simultaneous pre-fixed point (but not necessarily $\left(n_{1}\vee n_{2},p\right)$), and if $\left(o_{1},p\right)$ and $\left(o_{2},p\right)$ are simultaneous post-fixed points then $\left(o_{1}\vee o_{2},p\right)$ is a simultaneous post-fixed point (but not necessarily $\left(o_{1}\wedge o_{2},p\right)$).

Given the intuitions provided by Lemma 7 and its dual we can now prove, more directly, the existence of a lsfp and gsfp as follows. In particular, we prove, now using monotonicity alone, that the points $\mu_{F}\in\mathbb{O}$ and $\mu_{G}\in\mathbb{P}$ defined in Equations (A.4) and (A.5) on page A.5 form the least simultaneous fixed point. We do so in two steps, where we first prove that $\mu_{F}$ and $\mu_{G}$ form the least simultaneous pre-fixed point, then that they form a simultaneous fixed point, from which we conclude that $\mu_{F}$ and $\mu_{G}$ define the least simultaneous fixed point of $F$ and $G$ (only assuming the monotonicity of $F$ and $G$ but not requiring their continuity).

To prove that $\mu_{F}$ and $\mu_{G}$ define a simultaneous pre-fixed point first let’s note that by the monotonicity of $G$ 181818Note that the greatest lower bound (glb) of any set is less than or equal any element of the set, and thus applying a monotonic function to the glb produces an element less than or equal to the value of the function at any element of the set, and is thus a lower bound of the set of function values. In particular, $p_{i}\leq p_{j}\implies G\left(p_{i}\right)\leq G\left(p_{j}\right)$ implies that $G\left(\sqcap p_{i}\right)\leq G\left(p_{i}\right)$ for each and all $p_{i}$ ., we have

[TABLE]

Now, from the definition of simultaneous pre-fixed points we have $G\left(P_{i}\right)\leq O_{i}\mathrm{\,for\,all\>O_{i}\in\mathbb{C}}$. As such, by the transitivity of $\leq$, we have $G\left(\mu_{G}\right)\leq O_{i}\mathrm{\,for\,all\>O_{i}\in\mathbb{C}}$. Thus, $G\left(\mu_{G}\right)$ is a lower bound of $\mathbb{C}.$Given that $\mu_{F}$is the greatest lower bound of $\mathbb{C}.$thus we have $G\left(\mu_{G}\right)\leq\mu_{F}$. Similarly, we can prove that $F\left(\mu_{F}\right)\sqsubseteq\mu_{G}$, thereby proving that $\mu_{F}$ and $\mu_{G}$ define a simultaneous pre-fixed point.

Further. the definitions of $\mu_{F}$ and $\mu_{G}$ as the least elements of $\mathbb{C}$ and $\mathbb{D}$, respectively, show that they define the least simultaneous pre-fixed point.

Now, following a reasoning much similar to that used in the proof of the standard Knaster-Tarski fixed point theorem (but not using its conclusion) (e.g., see [29, p.283]), we can prove that $\mu_{F}$ and $\mu_{G}$ also define a simultaneous fixed point.

As such, given that each simultaneous fixed point is a simultaneous pre-fixed point, then combining the conclusions of both steps lets us conclude that $\mu_{F}$ and $\mu_{G}$ define the least simultaneous fixed point (lsfp).

Using a dual argument we can prove, only assuming the monotonicity of $F$ and $G$, that points $\nu_{F}\in\mathbb{O}$ and $\nu_{G}\in\mathbb{P}$ (as defined in Theorem 1) define the greatest simultaneous fixed point (gsfp) of $F$ and $G$.