• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Conference on Computability in Europe(CiE 2005); 20050608-12; Amsterdam(NL) >Formalising Exact Arithmetic in Type Theory
【24h】

Formalising Exact Arithmetic in Type Theory

机译：类型理论中的形式化精确算法

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In this work we focus on a formalisation of the algorithms of lazy exact arithmetic a la Potts and Edalat. We choose the constructive type theory as our formal verification tool. We discuss an extension of the constructive type theory with coinductive types that enables one to formalise and reason about the infinite objects. We show examples of how infinite objects such as streams and expression trees can be formalised as coinductive types. We study the type theoretic notion of productivity which ensures the infiniteness of the outcome of the algorithms on infinite objects. Syntactical methods are not always strong enough to ensure the productivity. However, if some information about the complexity of a function is provided, one may be able to show the productivity of that function. In the case of the normalisation algorithm we show that such information can be obtained from the choice of real number representation that is used to represent the input and the output.
机译：在这项工作中，我们专注于Lats和Edalat的惰性精确算术算法的形式化。我们选择建设性类型理论作为我们的形式验证工具。我们讨论了建设性类型理论与共归类型的扩展，这种扩展使人们可以形式化和推理无限物体。我们展示了如何将无限对象（例如流和表达式树）形式化为共归类型的示例。我们研究了生产力的类型理论概念，该概念确保了无限对象上算法结果的无限性。语法方法并不总是足够强大以确保生产率。但是，如果提供了有关功能复杂性的一些信息，则可能能够显示该功能的生产率。在归一化算法的情况下，我们表明可以从选择用于表示输入和输出的实数表示中获得此类信息。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号