结构化的一般上递归和上归纳图[扩展摘要]
Structured general corecursion and coinductive graphs [extended abstract]
摘要：
Bove和Capretta用一般递归方程来证明函数定义的流行方法是基于这样的观察：任何结构化的一般递归方程定义了一个预期域（“定义域”）的归纳子集，该方程具有唯一的解。要接受这个定义，只要证明这个子集包含整个预定域就足够了。这种方法对于“终止”定义非常有效。但是它没有考虑到“生产性”的定义，例如流值函数的典型定义。我们认为，这样的定义可以被视为在一个类似的精神，从一个不同的独特的可解性标准。任何结构化的递归方程都定义了预定域和预定余域之间的共归纳关系（“共归纳图”）。这个关系又确定了一个子集的预期域和商的预期的余域的属性，该方程是唯一解决的子集和商。因此，只要子集是全集且商是相等的，就保证方程对于预定域和预定余域有唯一解。
英文摘要：
Bove and Capretta's popular method for justifying function definitions by general recursive equations is based on the observation that any structured general recursion equation defines an inductive subset of the intended domain (the "domain of definedness") for which the equation has a unique solution. To accept the definition, it is hence enough to prove that this subset contains the whole intended domain. This approach works very well for "terminating" definitions. But it fails to account for "productive" definitions, such as typical definitions of stream-valued functions. We argue that such definitions can be treated in a similar spirit, proceeding from a different unique solvability criterion. Any structured recursive equation defines a coinductive relation between the intended domain and intended codomain (the "coinductive graph"). This relation in turn determines a subset of the intended domain and a quotient of the intended codomain with the property that the equation is uniquely solved for the subset and quotient. The equation is therefore guaranteed to have a unique solution for the intended domain and intended codomain whenever the subset is the full set and the quotient is by equality.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
