-
Optimal circulant graphs as low-latency network topologies
Authors:
Xiaolong Huang,
Alexandre F. Ramos,
Yuefan Deng
Abstract:
Communication latency has become one of the determining factors for the performance of parallel clusters. To design low-latency network topologies for high-performance computing clusters, we optimize the diameters, mean path lengths, and bisection widths of circulant topologies. We obtain a series of optimal circulant topologies of size $2^5$ through $2^{10}$ and compare them with torus and hyperc…
▽ More
Communication latency has become one of the determining factors for the performance of parallel clusters. To design low-latency network topologies for high-performance computing clusters, we optimize the diameters, mean path lengths, and bisection widths of circulant topologies. We obtain a series of optimal circulant topologies of size $2^5$ through $2^{10}$ and compare them with torus and hypercube of the same sizes and degrees. We further benchmark on a broad variety of applications including effective bandwidth, FFTE, Graph 500 and NAS parallel benchmarks to compare the optimal circulant topologies and Cartesian products of optimal circulant topologies and fully connected topologies with corresponding torus and hypercube. Simulation results demonstrate superior potentials of the optimal circulant topologies for communication-intensive applications. We also find the strengths of the Cartesian products in exploiting global communication with data traffic patterns of specific applications or internal algorithms.
△ Less
Submitted 4 January, 2022;
originally announced January 2022.
-
Computational Paths -- An approach in the $LND_{EQ}-TRS_{2}$ system
Authors:
Tiago M. L. Veras,
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
We use a labelled deduction system ( LND$_{ED-}$TRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which allowed us to carry out in homotopic theory an approach using the concept of computational paths. From this, we show that the computational paths can be used to perform the proofs of the $LND_{EQ}-TRS_{2}$ rewriting system…
▽ More
We use a labelled deduction system ( LND$_{ED-}$TRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which allowed us to carry out in homotopic theory an approach using the concept of computational paths. From this, we show that the computational paths can be used to perform the proofs of the $LND_{EQ}-TRS_{2}$ rewriting system.
△ Less
Submitted 17 November, 2023; v1 submitted 13 July, 2020;
originally announced July 2020.
-
An alternative approach to the calculation of fundamental groups based on labeled natural deduction
Authors:
Tiago M. L. de Veras,
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
In this work, we use a labelled deduction system based on the concept of computational paths (sequence of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We use a labelled deduction system based on the concept of computational paths (se…
▽ More
In this work, we use a labelled deduction system based on the concept of computational paths (sequence of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We use a labelled deduction system based on the concept of computational paths (sequence of rewrites) to obtain some results of algebraic topology and with support of the Seifet-Van Kampen Theorem we will calculate, in a way less complex than the one made in mathematics \cite{Munkres} and the technique of homotopy type theory \cite{hott}, the fundamental group of Klein Blottle $\mathbb{K}^2$, of the Torus $\mathbb{T}^2$ and Two holed Torus $\mathbb{M}_2=\mathbb{T}^2\# \mathbb{T}^2$ (the connected sum two torus).
△ Less
Submitted 19 June, 2019;
originally announced June 2019.
-
A Topological Application of Labelled Natural Deduction
Authors:
Tiago M. L. Veras,
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We then proceed to show the main result here: using this system to obtain the calculation of th…
▽ More
We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We then proceed to show the main result here: using this system to obtain the calculation of the fundamental group of the circle, of the torus and the real projective plane.
△ Less
Submitted 9 May, 2021; v1 submitted 19 June, 2019;
originally announced June 2019.
-
Optimal Low-Latency Network Topologies for Cluster Performance Enhancement
Authors:
Yuefan Deng,
Meng Guo,
Alexandre F. Ramos,
Xiaolong Huang,
Zhipeng Xu,
Weifeng Liu
Abstract:
We propose that clusters interconnected with network topologies having minimal mean path length will increase their overall performance for a variety of applications. We approach our heuristic by constructing clusters of up to 36 nodes having Dragonfly, torus, ring, Chvatal, Wagner, Bidiakis and several other topologies with minimal mean path lengths and by simulating the performance of 256-node c…
▽ More
We propose that clusters interconnected with network topologies having minimal mean path length will increase their overall performance for a variety of applications. We approach our heuristic by constructing clusters of up to 36 nodes having Dragonfly, torus, ring, Chvatal, Wagner, Bidiakis and several other topologies with minimal mean path lengths and by simulating the performance of 256-node clusters with the same network topologies. The optimal (or sub-optimal) low-latency network topologies are found by minimizing the mean path length of regular graphs. The selected topologies are benchmarked using ping-pong messaging, the MPI collective communications, and the standard parallel applications including effective bandwidth, FFTE, Graph 500 and NAS parallel benchmarks. We established strong correlations between the clusters' performances and the network topologies, especially the mean path lengths, for a wide range of applications. In communication-intensive benchmarks, clusters with optimal network topologies out-perform those with mainstream topologies by several folds. It is striking that a mere adjustment of the network topology suffices to reclaim performance from the same computing hardware.
△ Less
Submitted 31 March, 2019;
originally announced April 2019.
-
On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths
Authors:
Tiago Mendonça Lucena de Veras,
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the equality between two terms of the same type as a collection of homotopical paths between points of the same space. Since this is only a semantical interpretation, the addition of paths to the syntax of homotopy t…
▽ More
One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the equality between two terms of the same type as a collection of homotopical paths between points of the same space. Since this is only a semantical interpretation, the addition of paths to the syntax of homotopy type theory has been recently proposed by De Queiroz, Ramos and De Oliveira . In these works, the authors propose an entity known as `computational path', proposed by De Queiroz and Gabbay in 1994, and show that it can be used to formalize the identity type. We have found that it is possible to use these computational paths as a tool to achieve one central result of algebraic topology and homotopy type theory: the calculation of fundamental groups of surfaces. We review the concept of computational paths and the $LND_{EQ}-TRS$, which is a term rewriting system proposed by De Oliveira in 1994 to map redundancies between computational paths. We then proceed to calculate the fundamental group of the circle, cylinder, M{ö}bius band, torus and the real projective plane. Moreover, we show that the use of computational paths make these calculations simple and straightforward, whereas the same result is much harder to obtain using the traditional code-encode-decode approach of homotopy type theory.
△ Less
Submitted 17 May, 2018; v1 submitted 3 April, 2018;
originally announced April 2018.
-
On the Use of Computational Paths in Path Spaces of Homotopy Type Theory
Authors:
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira,
Tiago Mendonça Lucena de Veras
Abstract:
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$, whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that establishes that $a$ is i…
▽ More
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$, whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that establishes that $a$ is indeed equal to $b$. Based on that, a proof of equality can be seen as a sequence of substitutions and rewrites, also known as a `computational path'. One interesting fact is that it is possible to rewrite computational paths using a set of reduction rules arising from an analysis of redundancies in paths. These rules were mapped by De Oliveira in 1994 in a term rewrite system known as $LND_{EQ}-TRS$. Here we use computational paths and this term rewrite system to work with path spaces. In homotopy type theory, the main technique used to define path spaces is the code-encode-decode approach. Our objective is to propose an alternative approach based on the theory of computational paths. We believe this new approach is simpler and more straightforward than the code-encode-decode one. We then use our approach to obtain two important results of homotopy type theory: the construction of the path space of the naturals and the calculation of the fundamental group of the circle.
△ Less
Submitted 2 March, 2018;
originally announced March 2018.
-
Symmetry-guided design of topologies for supercomputer networks
Authors:
Alexandre F. Ramos,
Yuefan Deng
Abstract:
A family of graphs optimized as the topologies for supercomputer interconnection networks is proposed. The special needs of such network topologies, minimal diameter and mean path length, are met by special constructions of the weight vectors in a representation of the symplectic algebra. Such theoretical design of topologies can conveniently reconstruct the mesh and hypercubic graphs, widely used…
▽ More
A family of graphs optimized as the topologies for supercomputer interconnection networks is proposed. The special needs of such network topologies, minimal diameter and mean path length, are met by special constructions of the weight vectors in a representation of the symplectic algebra. Such theoretical design of topologies can conveniently reconstruct the mesh and hypercubic graphs, widely used as today's network topologies. Our symplectic algebraic approach helps generate many classes of graphs suitable for network topologies.
△ Less
Submitted 28 June, 2017;
originally announced June 2017.
-
Explicit Computational Paths
Authors:
Arthur Freitas Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$, whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that establishes that $a$ is i…
▽ More
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$, whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that establishes that $a$ is indeed equal to $b$. Based on that, a proof of equality can be seen as a sequence of substitutions and rewrites, also known as a `computational path'. One interesting fact is that it is possible to rewrite computational paths using a set of reduction rules arising from an analysis of redundancies in paths. These rules were mapped by De Oliveira in 1994 in a term rewrite system known as $LND_{EQ}-TRS$. Here we use computational paths and this term rewrite system to develop the main foundations of homotopy type theory, i.e., we develop the lemmas and theorems connected to the main types of this theory, types such as products, coproducts, identity type, transport and many others. We also show that it is possible to directly construct path spaces through computational paths. To show this, we construct the natural numbers and the fundamental group of the circle, showing results connected to these structures.
△ Less
Submitted 25 April, 2018; v1 submitted 16 September, 2016;
originally announced September 2016.
-
On Computational Paths and the Fundamental Groupoid of a Type
Authors:
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina de Oliveira
Abstract:
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences of rewrites', computational paths can be seen as the grounds on which the propositional equality between two computational objects stand. Using computational paths and categorical semantics, we take any type $A$ of type theory and construct a…
▽ More
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences of rewrites', computational paths can be seen as the grounds on which the propositional equality between two computational objects stand. Using computational paths and categorical semantics, we take any type $A$ of type theory and construct a groupoid for this type. We call this groupoid the fundamental groupoid of a type $A$, since it is similar to the one obtained using the homotopical interpretation of the identity type. The main difference is that instead of being just a semantical interpretation, computational paths are entities of the syntax of type theory. We also expand our results, using computational paths to construct fundamental groupoids of higher levels.
△ Less
Submitted 21 September, 2015;
originally announced September 2015.
-
On the Groupoid Model of Computational Paths
Authors:
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences or rewrites', computational paths are taken to be terms of the identity type of Martin Löf's Intensional Type Theory, since these paths can be seen as the grounds on which the propositional equality between two computational objects stand. Fro…
▽ More
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences or rewrites', computational paths are taken to be terms of the identity type of Martin Löf's Intensional Type Theory, since these paths can be seen as the grounds on which the propositional equality between two computational objects stand. From this perspective, this work aims to show that one of the properties of the identity type is present on computational paths. We are referring to the fact that that the identity type induces a groupoid structure, as proposed by Hofmann \& Streicher (1994). Using categorical semantics, we show that computational paths induce a groupoid structure. We also show that computational paths are capable of inducing higher categorical structures.
△ Less
Submitted 8 September, 2016; v1 submitted 8 June, 2015;
originally announced June 2015.
-
On the Identity Type as the Type of Computational Paths
Authors:
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
We introduce a new way of formalizing the intensional identity type based on the fact that a entity known as computational paths can be interpreted as terms of the identity type. Our approach enjoys the fact that our elimination rule is easy to understand and use. We make this point clear constructing terms of some relevant types using our proposed elimination rule. We also show that the identity…
▽ More
We introduce a new way of formalizing the intensional identity type based on the fact that a entity known as computational paths can be interpreted as terms of the identity type. Our approach enjoys the fact that our elimination rule is easy to understand and use. We make this point clear constructing terms of some relevant types using our proposed elimination rule. We also show that the identity type, as defined by our approach, induces a groupoid structure. This result is on par with the fact that the traditional identity type induces a groupoid, as exposed by Hofmann \& Streicher (1994).
△ Less
Submitted 18 April, 2015;
originally announced April 2015.
