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. 105129. ISSN 19725787

Text (BertotAllaisJFR2014ViewsofPIdefinitionandcomputation)
Bertot_Allais_JFR2014_Views_of_PI_definition_and_computation.pdf  Final Published Version License: 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.
Item type:  Article 

ID code:  60046 
Keywords:  Archimedes, arctangent, Coq, Gregory's formula, pi, Electronic computers. Computer science, Computer Science(all) 
Subjects:  Science > Mathematics > Electronic computers. Computer science 
Department:  Faculty of Science > Computer and Information Sciences 
Depositing user:  Pure Administrator 
Date Deposited:  03 Mar 2017 14:26 
Last modified:  02 Apr 2017 15:09 
Related URLs:  
URI:  http://strathprints.strath.ac.uk/id/eprint/60046 
Export data: 