Productivity of Edalat-Potts Exact Arithmetic in Constructive Type Theory

摘要

In this work we focus on a formalisation of the algorithms of lazy exact arithmetic a la Edalat-Potts in type theory. We choose the constructive type theory extended with coinductive types as our formal verification tool. 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. Furthermore, we show how to employ this semantic information to formalise a restricted case of normalisation algorithm in our type theory.