Cette thèse propose trois contributions aux preuves mathématiques assistées par ordinateur. On s'intéresse non seulement aux preuves reposant sur le calcul, mais aussi aux preuves formelles, qui sont àla fois produites et vérifiées à l'aide d'un logiciel appelé assistant à la preuve.Dans la première partie, nous illustrons le thème de l'expérimentation au service de la preuve en nous intéressant au problème de la complexité des algorithmes de multiplication matricielle. Cette question a historiquement été posée de manière de plus en plus abstraite: les approches modernes ne construisent pas d'algorithmes explicites mais utilisent des résultats théoriques pour améliorer la borne inférieure sur la célèbre constante oméga. Nous sommes revenus à une approche plus pratique en essayant de programmer certains des algorithmes impliqués par ces résultats théoriques. Cette approche expérimentale a révélé un motif inattendu dans des algorithmes existants. Alors que ces algorithmes contiennent une nouvelle variable epsilon dont la présence est réputée les rendre impraticables pour des tailles de matrices raisonnables, nous avons découvert que nous pouvions construire des algorithmes de multiplication matricielle en parallèle sans epsilon avec une complexité asymptotique qui peut théoriquement battre l'algorithme de Strassen pour les multiplications. Un sous-produit de cette exploration est un outil symbolique en Ocaml qui peut analyser, composer et exporter des algorithmes de multiplication matricielle. Nous pensons aussi qu'il pourrait être utilisé pour construire de nouveaux algorithmes pratiques de multiplication matricielle.Dans la deuxième partie, nous décrivons une preuve formelle de l'irrationalité de la constante zeta(3), en suivant la démonstration historique due à Apéry. L'étape cruciale de cette preuve est d'établir que deux suites de nombres rationnels satisfont une surprenante récurrence commune. Il est en fait possible de "découvrir"cette récurrence en utilisant des algorithmes symboliques, et leurs implémentations existantes dans un système de calcul formel. De fait,ce travail constitue un exemple d'une approche dite sceptique de la démonstration formelle de théorèmes, dans lequel des calculs sont principalement réalisés par un logiciel efficace de calcul formel puis vérifiés formellement dans un assistant à la preuve. Incidemment, ce travail questionne la valeur des certificats de télescopage créatif comme preuves complètes d'identités. Cette preuve formelle est également basée sur de nouvelles bibliothèques de mathématiques,formalisées pour ses besoins. En particulier, nous avons formalisé et simplifié une étude du comportement asymptotique de la suite ppcm(1,.., n). Ce travail est conduit dans l'assistant à la preuve Coq et prolonge les bibliothèques Mathematical Components.Dans la dernière partie, nous présentons une procédure qui calcule les approximations d'une classe d'intégrales propres et impropres tout en produisant simultanément un preuve formelle Coq de la correction du résultat de ce calcul. Cette procédure utilise une combinaison d'arithmétique d'intervalles et d'approximations polynomiales rigoureuses de fonctions. Ce travail utilise crucialement les possibilités de calculer efficacement à l'intérieur de la logique sous-jacente au système Coq. Il s'agit d'une extension de la bibliothèque CoqInterval d'approximation numérique d'une classe d'expressions réelles. Sa mise en œuvre a également donné lieu à des extensions de la bibliothèque Coquelicot d'analyse réelle, notamment pour améliorer le traitement des intégrales impropres. Nous illustrons l'intérêt de cet outil et ses performances en traitant des exemples standards mais non triviaux de la littérature, sur lesquels d'autres outils se sont en certains cas révélés incorrects. / This thesis proposes three contributions to computer-aidedmathematical proofs. It deals, not only with proofs relying oncomputations, but also with formal proofs, which are both produced andverified using a piece of software called a proof assistant.In the first part, we illustrate the theme of experimentation at theservice of proofs by considering the problem of the complexity ofmatrix multiplication algorithms. This problem has historically beenapproached in an increasingly abstract way: modern approaches do notconstruct algorithms but use theoretical results to improve the lowerbound on the famous omega constant. We went back to a more practicalapproach by attempting to program some of the algorithms implied bythese theoretical results. This experimental approach reveals anunexpected pattern in some existing algorithms. While these algorithmscontain a new variable epsilon whose presence is reputed to renderthem inefficient for the purposes of reasonable matrix sizes, we havediscovered that we could build matrix multiplication algorithms inparallel without epsilon's with an asymptotic complexity which cantheoretically beat Strassen's algorithm in terms of the number ofmultiplications. A by-product of this exploration is a symbolic toolin Ocaml which can analyze, compose and export matrix multiplicationalgorithms. We also believe that it could be used to build newpractical algorithms for matrix multiplication.In the second part, we describe a formal proof of the irrationality ofthe constant zeta (3), following the historical demonstration due toApéry. The crucial step of this proof is to establish that twosequences of rational numbers satisfy a suprising commonrecurrence. It is in fact possible to "discover" this recurrence usingsymbolic algorithms, and their existing implementations in a computeralgebra system. In fact, this work is an example of a skepticalapproach to the formal proof of theorems, in which computations aremainly accomplished by an efficient computer algebra program, and thenformally verified in a proof assistant. Incidentally, this workquestions the value of creative telescoping certificates as completeproofs of identities. This formal proof is also based on newmathematical libraries, which were formalised for its needs. Inparticular, we have formalized and simplified a study of theasymptotic behaviour of the sequence lcm(1,..., n). This work isdeveloped in the Coq proof assistant and extends the MathematicalComponents libraries.In the last part, we present a procedure which computes approximationsof a class of proper and improper integrals while simultaneouslyproducing a Coq formal proof of the correction of the result of thiscomputation. This procedure uses a combination of interval arithmeticand rigorous polynomial approximations of functions. This work makescrucial use of the possibility to efficiently compute inside Coq'slogic. It is an extension of the CoqInterval library providingnumerical approximation of a class of real expressions. Itsimplementation has also resulted in extensions to the Coquelicotlibrary for real analysis, including a better treatment of improperintegrals. We illustrate the value of this tool and its performanceby dealing with standard but nontrivial examples from the literature,on which other tools have in some cases been incorrect.

1968 var Strassens algoritm en av de stora genombrotten inom matrisanalyser. I denna rapport kommer teorin av Volker Strassens algoritm för matrismultiplikationer tillsammans med teorier om precisioner att presenteras. Även fördelar med att använda denna algoritm jämfört med naiva matrismultiplikation och dess implikationer, samt hur den presterar jämfört med den naiva algoritmen kommer att presenteras. Strassens algoritm kommer också att bli bedömd på hur dess resultat skiljer sig för olika precisioner när matriserna blir större, samt hur dess teoretiska komplexitet skiljer sig gentemot den erhållna komplexiteten. Studier hittade att Strassens algoritm överträffade den naiva algoritmen för matriser av storlek 1024×1024 och större. Den erhållna komplexiteten var lite större än Volker Strassens teoretiska. Den optimala precisionen i detta fall var dubbelprecisionen, Float64. Sättet algoritmen implementeras på i koden påverkar dess prestanda. Ett flertal olika faktorer behövs ha i åtanke för att förbättra Strassens algoritm: optimera dess avbrottsvillkor, sättet som matriserna paddas för att de ska vara mer användbara för rekursiv tillämpning och hur de implementeras t.ex. parallella beräkningar. Även om det kunde bevisas att Strassen algoritm överträffade den naiva efter en viss matrisstorlek så är den inte den mest effektiva; t.ex visades detta med Strassen-Winograd. Man behöver vara uppmärksam på hur undermatriserna allokeras, för att inte ta upp onödigt minne. För fördjupning kan man läsa på om cache-oblivious och cache-aware algoritmer. / Strassen’s algorithm was one of the breakthroughs in matrix analysis in 1968. In this report the thesis of Volker Strassen’s algorithm for matrix multipli- cations along with theories about precisions will be shown. The benefits of using this algorithm compared to naive matrix multiplication and its implica- tions, how its performance compare to the naive algorithm, will be displayed. Strassen’s algorithm will also be assessed on how the output differ when the matrix sizes grow larger, as well as how the theoretical complexity of the al- gorithm differs from the achieved complexity. The studies found that Strassen’s algorithm outperformed the naive matrix multiplication at matrix sizes 1024 1024 and above. The achieved complex- ity was a little higher compared to Volker Strassen’s theoretical. The optimal precision for this case were the double precision, Float64. How the algorithm is implemented in code matters for its performance. A number of techniques need to be considered in order to improve Strassen’s algorithm, optimizing its termination criterion, the manner by which it is padded in order to make it more usable for recursive application and the way it is implemented e.g. parallel computing. Even tough it could be proved that Strassen’s algorithm outperformed the Naive after reaching a certain matrix size, it is still not the most efficient one; e.g. as shown with Strassen-Winograd. One need to be careful of how the sub-matrices are being allocated, to not use unnecessary memory. For further reading one can study cache-oblivious and cache-aware algorithms.

No description available.

Based on Cohn and Umans’ group-theoretic method, we embed matrix multiplication into several group algebras, including those of cyclic groups, dihedral groups, special linear groups and Frobenius groups. We prove that SL2(Fp) and PSL2(Fp) can realize the matrix tensor ⟨p, p, p⟩, i.e. it is possible to encode p × p matrix multiplication in the group algebra of such a group. We also find the lower bound for the order of an abelian group realizing ⟨n, n, n⟩ is n3. For Frobenius groups of the form Cq Cp, where p and q are primes, we find that the smallest admissible value of q must be in the range p4/3 ≤ q ≤ p2 − 2p + 3. We also develop an algorithm to find the smallest q for a given prime p.

The maximum subarray problem is to find the array portion that maximizes the sum of array elements in it. This problem was first introduced by Grenander and brought to computer science by Bentley in 1984. This problem has been branched out into other problems based on their characteristics. k-overlapping maximum subarray problem where the overlapping solutions are allowed, and k-disjoint maximum subarray problem where all the solutions are disjoint from each other are those. For k-overlapping maximum subarray problems, significant improvement have been made since the problem was first introduced. For k-disjoint maximum subarrsy, Ruzzo and Tompa gave an O(n) time solution for one-dimension. This solution is, however, difficult to extend to two-dimensions. While a trivial solution of O(kn^3) time is easily obtainable for two-dimensions, little study has been undertaken to better this. This paper introduces a faster algorithm for the k-disjoint maximum sub-array problem under the conventional RAM model, based on distance matrix multiplication. Also, DMM reuse technique is introduced for the maximum subarray problem based on recursion for space optimization.

No description available.

Today's trend in microprocessor design is increasing the number of execution cores within one single chip. Increasing the processor's clock speed reached its limit with growing power consumption. This trend brings new opportunities to software developers, as they can take advantage of real multithreading in their applications. But a lot of new problems to solve appear with threading compared to sequential programming. With proper design, threading can enhance performance by making better use of hardware resources. However, the improper use of threading can lead to performance degradation, unpredictible behavior, or error conditions that are difficult to solve. For this reason Intel developed a suite of tools, that can help software developers to analyze performance and detect coding errors in thread interactions. This thesis focuses on the examination of ways that this tools can be used in multithreaded application development.

In this thesis we develop exact repair schemes capable of repairing or circumventing unavailable servers of a distributed network in the context of distributed storage and secure distributed matrix multiplication. We develop the (Λ, Γ, W, ⊙)-exact repair scheme framework for discussing both of these contexts and develop a multitude of explicit exact repair schemes utilizing decreasing monomial-Cartesian codes (DMC codes). Specifically, we construct novel DMC codes in the form of augmented Cartesian codes and rectangular monomial-Cartesian codes, as well as design exact repair schemes utilizing these constructions inspired by the schemes from Guruswami and Wootters [16] and Chen and Zhang [6]. In the context of distributed storage we demonstrate the existence of both high rate and low bandwidth systems based on these schemes, and we develop two methods to extend them to the l-erasure case. Additionally, we develop a family of hybrid schemes capable of attaining high rates, low bandwidths, and a balance in between which proves to be competitive compared to existing schemes. In the context of secure distributed matrix multiplication we develop similarly impactful schemes which have very competitive communication costs. We also construct an encoding algorithm based on multivariate interpolation and prove it is T-secure. / Doctor of Philosophy / Distributed networks may be thought of as networks of computers and/or servers which are capable of transmitting and receiving data from one another. For many applications it is possible for distributed networks to perform better than the sum of their constituent parts. In this thesis we will focus on the particular applications of distributed storage and secure distributed multiplication. A distributed storage system is a system that is capable of storing a single data file over every server in a distributed network. Distributed storage systems often come with exact repair schemes which are algorithms designed to reconstruct the data from a server in the network given the data from the other servers. In particular, if a server on the network ever fails or is otherwise unavailable an exact repair scheme can be used to repair the lost data from the server and maintain the original file. A distributed matrix multiplication scheme on the other hand is a process by which two matrices stored on a source server can be multiplied using a distributed network of helper servers. Again if a helper server becomes unavailable during this process we may use an exact repair scheme to circumvent this delay. The main goal of this thesis is to develop exact repair schemes for the distributed storage and secure distributed matrix multiplication contexts utilizing a mathematical object known as an evaluation code. We will develop several families of exact repair schemes which may be finely tuned to fit particular situations within these contexts, and we will compare these schemes to the existing schemes in the field.

No description available.

Starting with the work of Volker Strassen, algorithms for matrix multiplication have been developed which are time complexity-wise more efficient than the standard algorithm from the definition of multiplication. The general method of the developments has been viewing the bilinear mapping that matrix multiplication is as a three-dimensional tensor, where there is an exact correspondence between time complexity of the multiplication algorithm and tensor rank. The latter can be seen as a generalisation of matrix rank, being the minimum number of terms a tensor can be decomposed as. However, in contrast to matrix rank there is no general method of computing tensor ranks, with many values being unknown for important three-dimensional tensors. To further improve the theoretical bounds of the time complexity of matrix multiplication, support rank of tensors has been introduced, which is the lowest rank of tensors with the same support in some basis. The goal of this master's thesis has been to go through the history of faster matrix multiplication, as well as specifically examining the properties of support rank for general tensors. In regards to the latter, a complete classification of rank structures of support classes is made for the smallest non-degenerate tensor product space in three dimensions. From this, the size of a support can be seen affecting the pool of possible ranks within a support class. At the same time, there is in general no symmetry with regards to support size occurring in the rank structures of the support classes, despite there existing a symmetry and bijection between mirrored supports. Discussions about how to classify support rank structures for larger tensor product spaces are also included. / Från och med forskning gjord av Volker Strassen har flera algoritmer för matrismultiplikation utvecklats som är effektivare visavi tidskomplexitet än standardalgoritmen som utgår från defintionen av multiplikation. Generellt sett har metoden varit att se den bilinjära avbildningen som matrismultiplikation är som en tredimensionell tensor. Där används att det finns en exakt korrespondens mellan multiplikationsalgoritmens tidskomplexitet och tensorrang. Det sistnämnda är ett slags generalisering av matrisrang, och är minsta antalet termer en tensor kan skrivas som. Till skillnad frpn matrisrang finns ingen allmän metod för att beräkna tensorrang, och många värden är okända även för välstuderade och viktiga tensorer. För att hitta fler övre begränsningar på matrismultiplikations tidskomplexitet har stödrang av tensorer införts, som är den lägsta rangen bland tensor med samma stöd i en viss bas. Målet med detta examensarbete har varit att göra en genomgång av historien om snabbare matrismultiplikation, samt att specifikt undersöka egenskaper av stödrang för allmänna tredimensionella tensorer. För det sistnämnda görs en fullständig klassificering av rangstrukturer bland stödklasser för den minsta icke-degenererade tensorprodukten av tre vektorrum. Slutsatser är bl.a. att storleken av ett stöd kan ses påverka antalet möjliga ranger inom en stödklass. Samtidigt finns i allmänhet ingen symmetri med avseende på stödstorlek i stödklassernas rangstrukturer. Detta trots att det finns en symmetri och bijektion mellan speglade stöd. I arbetet ingår även en diskussion om hur stödrangstrukturer skulle kunna klassificeras för större tensorprodukter.