The worldʼs shortest correct exact real arithmetic program?

In this paper we present what is thought to be the worldʼs shortest correct exact real arithmetic program. The aim is to provide a tractable starting point for formal analysis and further development. In addition the program presented here allows beginners to the field to easily experiment with a practical implementation in order to understand some of the issues involved. The algorithms used have been validated using PVS which provides some grounds for believing them to be correct. However, as neither PVS nor Haskell have been similarly validated, semantic problems in either PVS or Haskell might still undermine the work. A slightly shorter program with the same functionality could be written, but there would be a significant degradation in performance. By performing better range reduction, the performance could be increased. However, we would lose the correctness proofs and the program would become a bit longer and even more opaque.

Authors

• David R. Lester

Keywords

• Computable reals
• Exact arithmetic
• Haskell
• Higher-order logic
• PVS