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.
展开▼
机译：在这项工作中，我们专注于懒惰精确算术A La Potts和Edalat算法的正式化。我们选择建设性类型理论作为我们的正式验证工具。我们讨论了具有调控类型的建设性类型理论的延伸，使一个人能够正式化和有关无限物体的原因。我们展示了诸如流和表达树等无限物体的示例可以被形式化为配合类型。我们研究了生产率的理论概念，可确保在无限物体上的算法结果的无限度。语法方法并不总是足以确保生产力。但是，如果提供了关于函数复杂性的一些信息，则可以能够显示该功能的生产率。在归一化算法的情况下，我们示出了这种信息可以从用于表示输入和输出的实数表示的选择获得。
展开▼
