首页    期刊浏览 2024年07月08日 星期一
登录注册

文章基本信息

  • 标题:Applications of Metric Coinduction
  • 本地全文:下载
  • 作者:Dexter Kozen ; Nicholas Ruozzi
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2009
  • 卷号:5
  • 期号:03
  • DOI:10.2168/LMCS-5(3:10)2009
  • 出版社:Technical University of Braunschweig
  • 摘要:

    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.

国家哲学社会科学文献中心版权所有