Distant Decimals of $$\pi $$ π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation

2017 ◽  
Vol 61 (1-4) ◽  
pp. 33-71
Author(s):  
Yves Bertot ◽  
Laurence Rideau ◽  
Laurent Théry
Keyword(s):  
Formal Proofs ◽  
Exact Computation

scholarly journals Extremal Values of the Sackin Tree Balance Index

2021 ◽  
Author(s):  
Mareike Fischer
Keyword(s):  
Phylogenetic Trees ◽  
Theoretical Computer Science ◽  
Search Trees ◽  
Formal Proofs ◽  
Birth Process ◽  
Ordered Trees ◽  
Research Areas ◽  
New Findings ◽  
Mathematical Phylogenetics ◽  
Extremal Values

AbstractTree balance plays an important role in different research areas like theoretical computer science and mathematical phylogenetics. For example, it has long been known that under the Yule model, a pure birth process, imbalanced trees are more likely than balanced ones. Also, concerning ordered search trees, more balanced ones allow for more efficient data structuring than imbalanced ones. Therefore, different methods to measure the balance of trees were introduced. The Sackin index is one of the most frequently used measures for this purpose. In many contexts, statements about the minimal and maximal values of this index have been discussed, but formal proofs have only been provided for some of them, and only in the context of ordered binary (search) trees, not for general rooted trees. Moreover, while the number of trees with maximal Sackin index as well as the number of trees with minimal Sackin index when the number of leaves is a power of 2 are relatively easy to understand, the number of trees with minimal Sackin index for all other numbers of leaves has been completely unknown. In this manuscript, we extend the findings on trees with minimal and maximal Sackin indices from the literature on ordered trees and subsequently use our results to provide formulas to explicitly calculate the numbers of such trees. We also extend previous studies by analyzing the case when the underlying trees need not be binary. Finally, we use our results to contribute both to the phylogenetic as well as the computer scientific literature using the new findings on Sackin minimal and maximal trees to derive formulas to calculate the number of both minimal and maximal phylogenetic trees as well as minimal and maximal ordered trees both in the binary and non-binary settings. All our results have been implemented in the Mathematica package SackinMinimizer, which has been made publicly available.

scholarly journals Isotropic Remeshing with Fast and Exact Computation of Restricted Voronoi Diagram

2009 ◽  
Vol 28 (5) ◽  
pp. 1445-1454 ◽  
Author(s):  
Dong-Ming Yan ◽  
Bruno Lévy ◽  
Yang Liu ◽  
Feng Sun ◽  
Wenping Wang
Keyword(s):  
Voronoi Diagram ◽  
Exact Computation

From sequential to distributed formal proofs

1997 ◽  
pp. 499-513
Author(s):  
Víctor M. Gulfas ◽  
J. Santiago Jorge ◽  
Juan J. Quintela ◽  
José L. Freire
Keyword(s):  
Formal Proofs
Sign in / Sign up

Export Citation Format

Share Document