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, 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 is 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. 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.
翻译:在本文中,我们把相互诱导作为相互诱导的双重内容,同时也作为标准的诱导的概括性。特别是,我们提出了对相互诱导和相互诱导的准确的正式定义。在这个过程中,我们提出了相互诱导和相互诱导的证明原则,我们提出了这些原则所依据的条件。尽管在研究文献中提到了相互(共同)诱导,但相互(共同诱导)的正式定义和相互(共同诱导)证明原则似乎是第一个这样的定义和证据。就我们所知而言,我们的工作似乎首先指出,与标准(共同)诱导和相互诱导的准确性不同,发电机的单一性并不足以保证在完全隐含的最小和最大的同时固定点的存在,而另一方面的连续性足以保证它们的存在。在我们介绍相互诱导的演示过程中,我们讨论一些与标准(也称为直接的)诱导和标准性诱导,以及相互(同时或间接的)目标相关的概念。在演示期间,我们讨论共同定义的共同定义(具体的标准/间接概念,即共同定义。我们具体地讨论了共同定义中,将用来帮助相互(同时或间接的)推介。