Picture of person typing on laptop with programming code visible on the laptop screen

World class computing and information science research at Strathclyde...

The Strathprints institutional repository is a digital archive of University of Strathclyde's Open Access research outputs. Strathprints provides access to thousands of Open Access research papers by University of Strathclyde researchers, including by researchers from the Department of Computer & Information Sciences involved in mathematically structured programming, similarity and metric search, computer security, software systems, combinatronics and digital health.

The Department also includes the iSchool Research Group, which performs leading research into socio-technical phenomena and topics such as information retrieval and information seeking behaviour.

Explore

Views of pi : definition and computation

Bertot, Yves and Allais, Guillaume (2014) Views of pi : definition and computation. Journal of Formalized Reasoning, 7 (1). pp. 105-129. ISSN 1972-5787

[img]
Preview
Text (Bertot-Allais-JFR2014-Views-of-PI-definition-and-computation)
Bertot_Allais_JFR2014_Views_of_PI_definition_and_computation.pdf - Final Published Version
License: Creative Commons Attribution 3.0 logo

Download (335kB) | Preview

Abstract

We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library.  In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the inverse of odd natural numbers (known as Leibnitz' formula).We give a formal description of the arctangent function and its expansion as a power series.  We then study other possible descriptions of pi, first as the surface of the unit disk, second as the limit of perimeters of regular polygons with an increasing number of sides.In a third section, we concentrate on techniques to effectively compute approximations of pi in the proof assistant by relying on rational numbers and decimal representations.