Blockchain Cohomology? Wyatt Meldman-Floch1[0000−0001−6582−5925] Constellation Labs, San Francisco CA 94108, USA Abstract. The following explores topological models of distributed com- puting for scalability focused Blockchain technologies1 . Applications of these models are provided in terms of emerging Blockchain protocols and scalability approaches as well as programming models allowing type-level verification. Keywords: Distributed computing · Homology · Algebraic topology 1 Introduction Existing models of blockchain technology are being expanded to incorporate scalability advancements in distributed computing. However, despite their com- patibility, these new approaches lack verification methods common in large scale data processing. By connecting topological models of distributed computing to scalable distributed architectures using Homotopy type theory, we create a hy- brid topological model applicable to common architectures in Big Data and emerging scalable blockchain technology. Applications are provided across com- mon scalable architectures in distributed computing that are being adopted by new blockchain technology. 1.1 Related Work The following is a literature overview of references used in formulating this work’s main results, from a historical perspective. Topological Models in Distributed Computing Topology is a mathemat- ical field focused on higher dimensional connective properties of algebraic ob- jects. In the context of distributed computing, these objects are generalizations of graphs, and their connectivity properties related to the computability of dis- tributed algorithms. Exploiting certain topological properties of higher dimen- sional geometric objects to prove results of distributed algorithms is referred to as the topological approach to distributed computing. Techniques from combi- natorial and algebraic topology have advanced characterization of synchronous and asynchronous distributed algorithms as well as their solvability [1–4]. 1 Supported by Constellation Labs * Copyright c 2019 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0) 2 W. Meldman-Floch The first applications of topology to distributed computing were in deriving the lower bounds for solving the distributed set agreement [12], which introduced a new paradigm based on algebraic topology for reasoning about asynchronous computations, where at-most one process can fail. The framework consisted of modeling tasks and protocols as simplicial complexes, and applied homology [5, 9] theory to reason about them. A key feature in this framework is that the exponential number of possible executions can be compactly represented using a static topological object in a model independent manner. In certain systems, such as those explored below relating to blockhain technology and scalability, the simplicial complexes are manifolds [6–8], a special class of simplicial complexes that are intuitive due to their geometric nature. The application of homology theory in these models forms a direct connection to Homotopy type theory [9, 10], the basis for modern static analysis in software engineering as well as in pro- grammatic proof assistants. This connection is realized by a result known as the Curry-Howard correspondence which is an isomorphism between mathematical proofs and programs. This correspondence allows us to verify programs at com- pile time, given a type system and typesafe (type preserving) implementation, as is enforced by the functional programming paradigm. Homotopy Type Theory and Verification Homotopy type theory is an interpretation of constructive type theory that connects logic and topology [15]. Specifically, Homotopy theory is a tool for constructing models of systems of logic and constructive type theory is a formal calculus for reasoning about homotopy. Computational implementation of type theory allows computer verified proofs in homotopy theory and is the formalism from which static analysis and functional programming emerged from [10]. Proof assistants and type systems are explicit examples of tools for proofs or programs for which compilation verifies correctness. Their use in mathemat- ics and computer science is increasingly common for managing complex proofs and programs. Examples of the success of proof assistants and type systems re- spectively include the proof of the Four Color Theorem and the Feit-Thompson Odd-Order Theorem, as well as large pieces of software such as a C compiler and the Standard ML programming language. Homotopy type theory is used in strongly typed programming languages like C and functional languages like Haskell to provide compile time verification. The ability to verify a program, especially all aspects of a distributed system before deployment, has been a fun- damental advantage that ushered the emergence of Big Data over the last ten years. Functional Programming and Big Data Big Data [11, 16] refers to appli- cations pertaining to data sets so big that distributing the processing is not an optimization but a fundamental requirement. Given the exponentially increasing amount of data generated by human information systems, the field continues to grow. It is widely held that the advent of Big Data stems from the MapReduce Blockchain Cohomology 3 white paper [14], which introduced the first programming model strictly designed for processing and generating large, inherently distributed, datasets. A programming model is the style and interface used for development and the leading programming model in Big Data, MapReduce, is fundamentally a func- tional programming model as it is just the combination of .map() and .reduce() operators, which are by definition declarative functional operations on collec- tions. Functional, as opposed to procedural, programming is a paradigm in soft- ware engineering that simplifies verification and improves visibility in distributed processes due to statelessness [17]. If something fails during state transforma- tions developers have to recompile and redeploy their source code, restarting a workflow from scratch. The reason why functional languages encourage scalable software architectures is because of the fact that they eliminate as much shared state as possible from a language. This leads to scalable micro-services or com- ponents and these micro-services then scale naturally into larger components. Blockchain Technology and Scalability The first Blockchain was formu- lated roughly 30 years ago as a way to time-stamp digital documents [13]. At its core a Blockchain is an application of a distributed consensus algorithm operat- ing on cryptographically signed data to form a secure append only log; secure in the sense that forgery is computationally intractable. Lately blockchain tech- nology has become popular due to its application in creating cryptocurrencies like Bitcoin, but wider applications in verifiable decentralized code execution (provided by Smart Contract platforms like the Ethereum protocol) and open network security (provide by the Constellation protocol) have emerged. A major limitation in adoption of blockchain applications is an inherent scal- ability issue due to the fact that traditional Byzantine Fault Tolerant consensus algorithms require serial execution across a distributed system, making con- currency difficult or impossible. New parallelizable consensus algorithms and system architectures have emerged however, based on the design of highly con- current and distributed data processing tools common in Big Data. These new approaches [20, 23] lack formal verification methods employed by similar tools in both blockchain and the Big Data space however, the creation of which is the focus of the models constructed below. 2 Consensus Protocols Recent advancements in distributed computing have adopted methods from al- gebraic topology to formally define consensus protocols [1, 2]. First define an execution space as a topological space equipped with a discrete product topol- ogy [3]. Defining a distributed process in terms of topology only requires us to care about the structure of the set of possible schedules of a distributed system [4]. By defining an execution space in terms of the homology of Protocol Com- plexes [2], define a Protocol Complex Sk : Pk ∆q as the q-dimensional standard simplex ∆q = {x ∈ R|Σxj = 1, xj ≥ ∀j} (1) 4 W. Meldman-Floch at morphism k described by the following vertex set Sk = {vi,0 . . . vi,q } (2) where P ⊂ S is the set of all admissible configurations and S is the set of all possible configurations. Define a consensus protocol P∗σ (S) : {Sk , ∂k } as the singular homology of a simplicial chain complex, carried by a group morphism implementing distributed consensus. Let Sk be a simplex configuration at step k and ∂k be the differential of a distributed consensus morphism: ∂k−1 ∂ P∗σ (S) : 0 ← . . . P σ (Sk−1 ) ←−−− P σ (Sk ) ←− k P σ (Sk+1 ) . . . (3) where Pk = ker∂k /im∂k+1 and is also an abelian group. Thus, P∗ = (Pk ) |k ∈ Z is a graded abelian group which is referred to as the homology of a Protocol Complex S. We abuse our notation of P but rectify by noting that an admissible state k is required for anther step k + 1, thus we define P as the functor carrying our consensus operator defined below. Define a consensus operator σ as the group morphism on the singular q- simplex σ : ∆q → S σk : Sk−1 × Pk → Sk (4) which are continuous on discrete topologies such as ∆q [1]. Define homology between configurations as a measure of divergence given by the differential q+1 X ∂(σ) = (−1)i−1 (σ ◦ δqi ) (5) i=1 for continuous functions δqi : ∆q−1 → ∆q |1 ≤ i ≤ q + 1 where δqi (x1 , . . . , xq ) = (x1 , . . . xi−1 , 0, xi , xi+1 , . . . , xq−1 , . . . , xq ) (6) As the graded abelian group of our Protocol Complex is the simplicial singu- lar homology group and σ is our homology preserving map, it is trivial to note that homology holds ∀k ∈ Z, i.e. ∂k ◦ ∂k+1 = 0 (7) As a corollary of the fact that the geometric realization of a simplicial complex is dually a topological space, due to the vanishing homology up to k, Pk ∆q is k-acyclic, or that there is a consistently forward moving ”arrow of time”. 2.1 Protocol Topologies It’s possible to layer Protocol Complexes defined as above with guarantees about consistency as long as continuity is preserved. Our definition of homology above is verification criteria for the ability to exchange configuration states between Protocol Complexes. Blockchain Cohomology 5 Specifically, a valid ’layering’ as the existence of a functoral vertex map be- tween singular homologies S (defined S equivalently here as the disjoint subset of Protocol Complexes) l : k Pπ → k Pπ+1 . Making use of Homotopy type theory allows us to focus on structure by treating topological characteristics called homotopy groups as primitives. Noting that simplicial complexes together with simplicial vertex maps form a category, if we redefine our k-acyclic distributed consensus protocol σ categorically as the functoral carrier Σ∗ we can form a chain complex that adheres to the homology theory of homotopy types [5]. Let us define a ’layering’ as a Protocol Topology TPΣ : Σ∗ Pπ , the singular homology of a chain complex of Protocol Complexes carried by a homotopy preserving functor Σ∗ . The Protocol Topology is given by the following chain complex ∂ ∂ TPΣ : 0 ← Σ∗ Pπ ← − ΣP0 ← − . . . ΣPi |i ≤ π ∈ Z (8) π where Σπ : ker∂kπ /im∂k+1 → ∂kπ+1 /im∂k+1 π+1 For Protocol Complex morphisms Σπ , Σπ+1 chain homotopy from Σπ to Σπ+1 is a homotopy preserving graded abelian group morphism l : Pπ → Pπ+1 yielding a vanishing homology, i.e. Σπ − Σπ+1 = ∂ π ◦ l + l ◦ ∂ π+1 (9) = ∂ π ◦ ∂ π+1 = 0 Noting that these conditions are met by the definitions of an acyclic carrier as above, it follows that a Protocol Topology as defined above is π-acyclic. 2.2 Applications: Scale out Networking Traditional Blockchains have come up short in their ability to support real world use cases, mainly due to scalability issues. In terms of scalability, sharding or partitioned approaches have taken form in improvements to Bitcoin with Light- ning [21] as well as base layer protocols like Zilliqa [22]. In these approaches, relays or subnets are deployed to ferry larger amounts of transactions into a fixed-size configuration state (block). The key to their success is the application of Scale Out Networking [11], adding another layer to the network topology to buffer and compress data which results in faster routing and query times. If we consider either base layer protocol as a Protocol Complex, then a partitioned or sharding mechanism is described by our model of Protocol Topology. A type hierarchy is enough to verify a protocol’s equivalence to a Protocol Topology due to covariance, which is a valid null differential as detailed by R. Grahm above. Specifically, given a base layer protocol Σπ with block type π, a type preserving operation Σπ+1 such as a buffering service in a multi layered (in this case L2) topology, then if there exists covariance between their data types π, π + 1 then ∂ π ◦ ∂ π+1 = 0. Specifically, consider a protocol with an L2 topology: ∂ ∂ TPΣ : 0 ← Σ∗ Pπ ← − ΣP0 ← − ΣP2 (10) 6 W. Meldman-Floch This Protocol Topology is a corresponding model to an L2 system architecture (see Fig. 1). A program implementing the above protocol is verifiable by ensuring functoral covariant state transitions which can be enforced by static analysis [10] (type checking at compile time). Fig. 1. System architecture diagram of an L2 system [11] 3 Blockchain Cohomology Distributed architectures designed topologically can be verified at the type level. In order to model distributed state, we need to design our topologies such that data locality, or the logic behind the distribution of data in distributed database is mathematically tractable. We introduce methods from Abstract Differential Geometry, namely finitary cech-deRham cohomology in order to define an ori- entable manifold from our definition of Protocol Topology. 3.1 Block Sheaves First we need to introduce the dual of homology as described above, namely cohomology. In describing our Protocol Complex it only makes sense to have an arrow moving ’forward in time’ as consensus itself is acyclic, with each iteration pointing ’backwards in time’ to its previous state. In this sense our evolution was the compounding dimensionality of the space of all configurations, as implied by the discrete product topology of a Protocol Complex. In defining an orientable manifold, we need to move ’backwards’ through our space, i.e. from higher to lower dimension. This is shown as the differential on an arrow going right instead of left. In principle, Abstract Differential Geometry (ADT) admits any topological space as a base space on which to ’solder sheaves’ for carrying out differential ge- ometry [6]. i.e. constructing a manifold. By constructing the Protocol Topology within a monoidal category, A. Malios et al. showed that the singular cohomol- ogy of a Protocol Topology is equivalent to an A-module of Z+-graded discrete differential forms, otherwise known as discrete differential manifolds. This forms an execution tree, a sequence of configurations in a poset (directed acyclic graph) Blockchain Cohomology 7 topology. A decision tree can be assigned to any set of executions that captures the decision of choosing a successive configuration. A Blockchain can be defined as an extension of an execution tree, where each block is formulated as a sheaf with a well defined tensor operation and each successive block verified by a de- cision tree. We define a sheaf  as the ’enrichment’ of any cochain A-complex of positive degree/grade, corresponding to the A-resolution of an abstract A- module d0 d1 S ∗ : 0 →  → S 0 −→ S 1 −→ . . . (11) and homomorphism given by Cartan-Kahler-type of nilpotent differential oper- ator d. We will make use of the fact that an A-module sheaf  on any arbitrary topological space (shown above with an arbitrary simplicial cochain-complex) admits an injective resolution. Blockchains are naturally equipped with a sheaf, known as a block hash, which contains topological state data about the configuration of the system. Ev- ery abelian unital ring (of which this sheaf theortic construction derives from) admits a derivation map [7], allowing us to ’unpack’ data within a block re- cursively under the product operation. By noting the equivalence of Sorkin’s fintoposets to simplicial complexes, A. Mallios et al. showed that the Gelfand duality implies that a manifold can be constructed from simplicial complexes [6]. Thus if we reformulate our definition of a consensus protocol above as a sheaf with semigroup operations carried by right derived functors with monadic bind, we can form a manifold. For a fintoposet (the topological equivalent of a directed acyclic graph), it’s incidence algebra can be broken down into a direct sum of vector subspaces M Ω(P ) = Ω i = Ω 0 ⊕ Ω 1 · · · := A ⊕ R (12) i∈Z+ where Ω(PL )s are Z+ graded linear spaces, A is a commutative sub algebra of Ω and R := i≥1 Ω i is a linear (ringed) subspace. It is trivial to notice that Ω(P ) is an A-module of a Z+-graded discrete differential form. A manifold can be constructed by organizing the incidence algebras of our Protocol Complexes into algebra sheaves. The n-th (singular) cohomolgy group Hn (X, ) of an A-module sheaf (X) over topological space X, can be described by global sections ΓX () ≡ Γ (X, ) Hn (X, ) := Rn (Γ (C, ) := H n [Γ (C, S ∗ )] := kerΓX (dn )/imΓX (dn−1 ) (13) where Rn Γ is the right derived functor of the global section functor Γx (.) ≡ Γ (X, .). Note that Rn is equivalent to the ith linear ringed subspace above. These dual definitions of gamma correspond to out definitions of σ and Σ∗ with respect to our functoral vertex map l in our definition of a Protocol Topology. The sheaf cohomology of a topological space is the cohomology of any ΓX - acyclic resolution of  [15]. The corresponding abstract A-complex S ∗ can be directly translated by the functor Γx to the ’global section A-complex’ ΓX (S ∗ ) d0 d1 ΓX (S ∗ ) : 0 → − ΓX () −→ ΓX (S 0 ) −→ . . . (14) 8 W. Meldman-Floch which is the abstract de Rham complex of a discrete manifold X. The action of d is to effect transitions between the linear subspaces Ωi of Ω(P ), as follows: d: Ωi → Ωi+1 . The finitary de Rham theorem defines a finitary equivalent of the typical c∞ Pm smooth manifold. Noting Γm is fine by construction, Mallios et al. show that finsheaf-cohomology differential tetrads M τ := (Pm , ΩM , d, ΩdeR ) (15) is equivalent to the c∞ -smooth Cech-de Rham complex. In our definition of τ , ΩM is the categorically dual finsheaf (finitary sheaf) of Sorkin’s fintoposets Pm , M d is an exterior product, and ΩdeR is the abstract de Rahm complex. 3.2 Protocol Manifold We’ve shown how to create a manifold from the cohomology of a discrete topo- logical space. We now show how to construct a manifold from of a Protocol Topology. Define a cochain-complex within the cohomology theory of homotopy types under the cup product. Making note of the existence of a tensor product in the cohomology theory of homotopy types by E. Cavallo [9] define the protocol manifold as the ringed vector space formed by the direct sum over all protocol sheaves M ΓΣ = Σ∗ i (16) 0≤i≤π 3.3 Applications: Data Locality and Dynamic Partitioning Data locality refers to the ability to move a query close to node where actual data resides within a distributed system as opposed to moving data over network to the process executing the query. This minimizes network overhead, increases overall throughput and is a best practice in the development of distributed appli- cations. A Protocol Manifold is a construction that forms the total state space of data across nodes implicitly respective of the network topology of a state- ful distributed system such as a Consensus Protocol. For elastic or dynamically partitioned systems, where data storage needs to be rebalanced across nodes in the system when nodes join or leave, it provides a convenient consistency check for the state of the network and an implicit way to organize the rebalancing of data across nodes. A prime example of a distributed data store that corresponds to the Protocol Manifold is the Hadoop Distributed File System (HDFS)(see Fig. 2), which stores data across nodes with an optimal data locality and mini- mal redundancy to prevent data loss in the case of partial system failure. This allowed for creation of high level strongly typed APIs managing implicit orches- tration of distributed data storage in tools such as Apache Spark and is key to the ability to form MapReduce APIs across stateful systems as demonstrated by the Poincare Complex below. Blockchain Cohomology 9 Consider an enrichment of a type hierarchy  . . . n , and a state transition   J(t) : ΓΣ(t) → ΓΣ(t+1) (17) where the number of nodes increase or decrease, if all  commute and M M Σ(t)∗ i = Σ(t + 1)∗ i (18) 0≤i≤π 0≤i≤π then the total configuration space is consistent under the state transition of nodes joining or leaving. Such an  implemented as a type with a product operation [19] would allow us to verify the state transition J by an ’unpacking’ operation across block sheaves under the product operation, allowing for verification at the type level both at compile time and run time). Fig. 2. HDFS replication system architecture [24]. A state transition adding or remov- ing nodes maintains the total set of data. 4 Typesafe Poincare Duality Up until now we have not explicitly defined functoral group homomorphisms that can construct the complexes described above. We show that the dual na- ture of the hylomorphic and metamorphic recursion schemes maintain vanishing differentials and thus Poincare duality for all π. If we define a catamorphism and anamorphism with the same f-algebra and f-coalgebra, we can show by construction that the resulting co/chain-complexes are valid definitions of Protocol Topologies/Manifolds and that Poincare duality of the protocol manifold is maintained up to π isomorphism. We define in terms of Σ and , noting that our functor Σ is a valid f-algebra and sheaf  a co-algebra. Let us define a hylomorphism  ← P × Σ : Ω T (, P ) (19) and metamorphism ΩΓ (P, ) : ΓΣ ×  → P (20) 10 W. Meldman-Floch we formally verify by the construction of the following geometric cw-complex ∂ ∗ ∂ ΩΓT : 0 ← → ΩΓT ∗ () ← → ΩΓT ((P0 )) . . . ΩΓT ((Pπ )) (21) that T and Γ form a Poincare complex, clearly satisfying the Poincare duality as ∂ vanishes in our construction of T and ΓΣ . The fundamental class of our ∗ corresponding space is ΩΓT ∗ which carries the type signatures of our hylo and metamorphisms. Formally define ΩΓT as a Poincare protocol. 4.1 Applications: MapReduce APIs The design of tools in the data engineering and data science space often employ principles from functional programming and type theory due to the benefits they have at verifying code at compile time. Network queries can be implemented with guarantees around correct access governed at the type level, as functoral oper- ators such as .map() and .reduce(). This is largely a source of the origins of scalable data processing tools for analysis and modeling like Hadoop and Spark. Distributed data stores and microservice architectures employ monadic design patterns for improvements on concurrency, static type checking, testing, design patterns, cluster management, training models etc. One benefit is the develop- ment of convenient API’s with Map/Reduce operations simplifying queries by abstracting low level data locality management [16], a key example would be Spark’s RDD [18]. Monadic execution models allow complex data pipelines (see Fig. 3) to be implemented and governed declaratively, providing distributed data stores constructed with high level API’s. As such, if we follow their construction at the type level in architecture and code design we can develop increasingly complex distributed systems with greater guarantees. A Poincare Protocol is a Fig. 3. Example of a data pipeline with a micro-service architecture.  corresponds to indices within a Poincare Complex for each micro-service. consensus protocol with a monadic execution model like the Big Data tools dis- cussed above. It describes a distributed data store of topological data formed of configuration data across blocks. An example of this is the Constellation pro- tocol, the design of which is also its origin. Constellation was designed with a monadic execution model [23] that can be layered like a Protocol Topology and has the consistency guarantees of a Protocol Manifold. In this model, multiple independent consensus operations can coexist across heterogeneous data types, allowing for complex queries to be performed across concurrent or composite ser- vices, like common data pipelines (see Fig. 3). Each of these consensus operations Blockchain Cohomology 11 is referred to as a state channel, an operates on its own corresponding data type . By constructing a Poincare Protocol, Constellation defined a high level MapRe- duce API [20] for constructing new state channels out of API callbacks across existing state channels (see Fig. 4). Using an algebraic representation of these APIs in the callback tree, common in functional programming [17], each step in the call back tree is governed by the respective ’s f-algebra and f-coalgebra and we can verify correctness at the type level both at compile time and runtime. The end result is a consensus protocol with the same model and guarantees of the functional programming paradigm, allowing for interoperability between the Blockchain and Big Data ecosystems. Fig. 4. Callback tree across Constellation state channels (denoted by their , indices within a Poincare Complex. The tree is defined by algebra/coalgebra of a recursion scheme and is transitively its own state channel. 5 Remarks We have successfully constructed topological models of scalability focused Blockchain technologies and Big Data architectures. The protocol models above can be ex- panded to other distributed systems that undergo finite state transitions. The key advantage of these models is that they can be designed within functional languages with strong type systems that allows for verification at compile time. Future work can apply these models to systems undergoing more complex and possibly differentiable state transitions. References 1. Nowak T., Schmid U.: Topology in Distributed Computing, Master’s Thesis, Vienna University of Technology, (2010) 2. Herlihy M., Rajsbaum S.: Algebraic topology and distributed computing a primer. In: van Leeuwen J. (eds) Computer Science Today. Lecture Notes in Computer Science, vol 1000. Springer, Berlin, Heidelberg. (1995) 3. Alpern, B., Schneider F.: Defining liveness. Information Processing Letters 21, 4 (October 1985), 181–185. Cornell University, (1985) 4. Saks, M., Zaharoglou, F.: Wait-free k-set agreement is impossible: the topology of public knowledge. SIAM J. Comput. 29(5), 1449–1483 (2000) 5. Grahm R.: Synthetic Homology in Homotopy Type Theory Robert Graham. arXiv:1706.01540 (2017) 12 W. Meldman-Floch 6. Mallios A., Raptis I.: Finitary Cech-de Rham Cohomology: much ado without smoothness. Int.J.Theor.Phys. 41 1857-1902 (2002) 7. Mallios, A.: Geometry of Vector Sheaves: An Axiomatic Approach to Differential Geometry, vols. 1-2, Kluwer Academic Publishers, Dordrecht (1998) 8. Mallios, A.: On an Axiomatic Treatment of Differential Geometry via Vector Sheaves. Applications, Mathematica Japonica(International Plaza), 48, 93. (1988) 9. Cavallo, E.: Synthetic cohomology in Homotopy Type Theory. Master’s thesis, Carnegie-Mellon University (2015) 10. Nielson F. Nielson H. R.: Type and Effect Systems. In: Olderog ER., Steffen B. (eds) Correct System Design. Lecture Notes in Computer Science, vol 1710. Springer, Berlin, Heidelberg 114-136, (1999) 11. A. Vahdat, M. Al-Fares, N. Farrington, R. N. Mysore, G. Porter, and S. Radhakr- ishnan, Scale-out networking in the data center, IEEE Micro, vol. 30, no. 4, pp. 29–41, https://doi.org/10.1109/MM.2010.72 12. Herlihy M. and Shavit. N.: The asynchronous computability theorem for t-resilient tasks. In: Proceedings of the twenty-fifth annual ACM symposium on Theory of computing, STOC, (1993) 13. Haber, S. and Stornetta, W.S. J. Cryptology 3: 99. https://doi.org/10.1007/BF00196791 (1991) 14. Dean J., Ghemawat, S.: MapReduce: Simplified data processing on large clusters, In: Proc. 6th USENIX Symposium on Operating Systems Design and Implementa- tion, OSDI 2004, San Francisco, USA, Dec. (2004) 15. Gallier J., Quaintance J.: A Gentle Introduction to Homology, Cohomology, and Sheaf Cohomology. Preprint (2016) 16. Wu D., Sakr S., Zhu L.: Big Data Programming Models. In: Zomaya A.Y, Sakr S. (eds) Handbook of Big Data Technologies, Springer International Publishing, AG,https://doi.org/10.1007/978-3-319-49340-4 2 (2017) 17. Chuisano P., Bjarnason R.:Functional Programming in Scala, Manning Publica- tions Co., Greenwich, CT, (2014) 18. Apache Spark RDD documentation, https://spark.apache.org/docs/latest/r dd-programming-guide.html\#resilient-distributed-datasets-rdds. Last ac- cessed 15 Oct (2019) 19. Product operator from functional programming library Cats, http://eed3si9n.c om/herding-cats/Cartesian.html. Last accessed 18 April (2019) 20. Constellation Protocol repository, MapReduce interface via recursion schemes ht tps://github.com/Constellation-Labs/constellation/blob/7aeaa786d42e019 4e31cd8fd0c6b99462cb63f33/src/main/scala/org/constellation/Cell.scala. Last accessed 18 April (2019) 21. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. Joseph Poon, Thaddeus Dryja https://lightning.network/lightning-network-paper. pdf Last accessed 18 April (2019) 22. The ZILLIQA Technical Whitepaper, The Zilliqa Team. https://whitepaper.i o/document/16/zilliqa-whitepaper Last accessed 18 April (2019) 23. Constellation Protocol repository, Validation Monad https://github.com/Const ellation-Labs/constellation/blob/dev/src/main/scala/org/constellation/ util/Validation.scala. Last accessed 18 April (2019) 24. Hadoop Distributed File System design documentation https://hadoop.apache. org/docs/r1.2.1/hdfs\ design.html Last accessed 18 April (2019)