Applications of Metric Coinduction
Applications of Metric Coinduction
复制标题
公制共导的应用
DOI：
10.2168/lmcs-5(3:10)2009
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Nicholas Ruozzi
中科院分区：
文献类型：
--
作者：
D. Kozen;Nicholas Ruozzi
度量共归纳是共归纳的一种形式，可用于建立构造为有限近似极限的对象的属性。我们可以证明一个共归纳步骤，表明通过近似过程的一步保留了某些属性，然后通过共归纳原理自动推断出极限对象具有该属性。这通常可以用来避免涉及极限和收敛的复杂分析论证，用更简单的代数论证代替它们。本文研究了该原理在各个领域的应用，包括无限流、马尔可夫链、马尔可夫决策过程和非良基集。这些结果表明了共归纳法作为通用证明技术的有用性。
Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One can prove a coinduction step showing that some property is preserved by one step of the approximation process, then automatically infer by the coinduction principle that the property holds of the limit object. This can often be used to avoid complicated analytic arguments involving limits and convergence, replacing them with simpler algebraic arguments. This paper examines the application of this principle in a variety of areas, including infinite streams, Markov chains, Markov decision processes, and non-well-founded sets. These results point to the usefulness of coinduction as a general proof technique.