-
Ext groups in Homotopy Type Theory
Authors:
J. Daniel Christensen,
Jarl G. Taxerås Flaten
Abstract:
We develop the theory of Yoneda Ext groups over a ring in homotopy type theory (HoTT) and describe their interpretation into an $\infty$-topos. This is an abstract approach to Ext groups which does not require projective or injective resolutions. While it produces group objects that are a priori large, we show that the $\operatorname{Ext}^1$ groups are equivalent to small groups, leaving open the…
▽ More
We develop the theory of Yoneda Ext groups over a ring in homotopy type theory (HoTT) and describe their interpretation into an $\infty$-topos. This is an abstract approach to Ext groups which does not require projective or injective resolutions. While it produces group objects that are a priori large, we show that the $\operatorname{Ext}^1$ groups are equivalent to small groups, leaving open the question of whether the higher Ext groups are essentially small as well. We also show that the $\operatorname{Ext}^1$ groups take on the usual form as a product of cyclic groups whenever the input modules are finitely presented and the ring is a PID (in the constructive sense).
When interpreted into an $\infty$-topos of sheaves on a 1-category, our Ext groups recover (and give a resolution-free approach to) sheaf Ext groups, which arise in algebraic geometry. (These are also called "local" Ext groups.) We may therefore interpret results about Ext from HoTT and apply them to sheaf Ext. To show this, we prove that injectivity of modules in HoTT interprets to internal injectivity in these models. It follows, for example, that sheaf Ext can be computed using resolutions which are projective or injective in the sense of HoTT, when they exist, and we give an example of this in the projective case. We also discuss the relation between internal $\mathbb{Z} G$-modules (for a $0$-truncated group object $G$) and abelian groups in the slice over $BG$, and study the interpretation of our Ext groups in both settings.
△ Less
Submitted 16 May, 2023;
originally announced May 2023.
-
Central H-spaces and banded types
Authors:
Ulrik Buchholtz,
J. Daniel Christensen,
Jarl G. Taxerås Flaten,
Egbert Rijke
Abstract:
We introduce and study central types, which are generalizations of Eilenberg-Mac Lane spaces. A type is central when it is equivalent to the component of the identity among its own self-equivalences. From centrality alone we construct an infinite deloo** in terms of a tensor product of banded types, which are the appropriate notion of torsor for a central type. Our constructions are carried out…
▽ More
We introduce and study central types, which are generalizations of Eilenberg-Mac Lane spaces. A type is central when it is equivalent to the component of the identity among its own self-equivalences. From centrality alone we construct an infinite deloo** in terms of a tensor product of banded types, which are the appropriate notion of torsor for a central type. Our constructions are carried out in homotopy type theory, and therefore hold in any $\infty$-topos. Even when interpreted into the $\infty$-topos of spaces, our main results and constructions are new.
Along the way, we further develop the theory of H-spaces in homotopy type theory, including their relation to evaluation fibrations and Whitehead products. These considerations let us, for example, rule out the existence of H-space structures on the $2n$-sphere for $n > 0$. We also give a novel description of the moduli space of H-space structures on an H-space. Using this description, we generalize a formula of Arkowitz-Curjel and Copeland for counting the number of path components of this moduli space. As an application, we deduce that the moduli space of H-space structures on the $3$-sphere is $Ω^6 \mathbb{S}^3$.
△ Less
Submitted 27 February, 2023; v1 submitted 6 January, 2023;
originally announced January 2023.
-
Non-accessible localizations
Authors:
J. Daniel Christensen
Abstract:
In a 2005 paper, Casacuberta, Scevenels and Smith construct a homotopy idempotent functor $E$ on the category of simplicial sets with the property that whether it can be expressed as localization with respect to a map $f$ is independent of the ZFC axioms. We show that this construction can be carried out in homotopy type theory. More precisely, we give a general method of associating to a suitable…
▽ More
In a 2005 paper, Casacuberta, Scevenels and Smith construct a homotopy idempotent functor $E$ on the category of simplicial sets with the property that whether it can be expressed as localization with respect to a map $f$ is independent of the ZFC axioms. We show that this construction can be carried out in homotopy type theory. More precisely, we give a general method of associating to a suitable (possibly large) family of maps, a reflective subuniverse of any universe $\mathcal{U}$. When specialized to an appropriate family, this produces a localization which when interpreted in the $\infty$-topos of spaces agrees with the localization corresponding to $E$. Our approach generalizes the approach of [CSS] in two ways. First, by working in homotopy type theory, our construction can be interpreted in any $\infty$-topos. Second, while the local objects produced by [CSS] are always 1-types, our construction can produce $n$-types, for any $n$. This is new, even in the $\infty$-topos of spaces. In addition, by making use of universes, our proof is very direct.
Along the way, we prove many results about "small" types that are of independent interest. As an application, we give a new proof that separated localizations exist. We also give results that say when a localization with respect to a family of maps can be presented as localization with respect to a single map, and show that the simplicial model satisfies a strong form of the axiom of choice which implies that sets cover and that the law of excluded middle holds.
△ Less
Submitted 28 May, 2024; v1 submitted 14 September, 2021;
originally announced September 2021.
-
2022 Roadmap on Neuromorphic Computing and Engineering
Authors:
Dennis V. Christensen,
Regina Dittmann,
Bernabé Linares-Barranco,
Abu Sebastian,
Manuel Le Gallo,
Andrea Redaelli,
Stefan Slesazeck,
Thomas Mikolajick,
Sabina Spiga,
Stephan Menzel,
Ilia Valov,
Gianluca Milano,
Carlo Ricciardi,
Shi-Jun Liang,
Feng Miao,
Mario Lanza,
Tyler J. Quill,
Scott T. Keene,
Alberto Salleo,
Julie Grollier,
Danijela Marković,
Alice Mizrahi,
Peng Yao,
J. Joshua Yang,
Giacomo Indiveri
, et al. (34 additional authors not shown)
Abstract:
Modern computation based on the von Neumann architecture is today a mature cutting-edge science. In the Von Neumann architecture, processing and memory units are implemented as separate blocks interchanging data intensively and continuously. This data transfer is responsible for a large part of the power consumption. The next generation computer technology is expected to solve problems at the exas…
▽ More
Modern computation based on the von Neumann architecture is today a mature cutting-edge science. In the Von Neumann architecture, processing and memory units are implemented as separate blocks interchanging data intensively and continuously. This data transfer is responsible for a large part of the power consumption. The next generation computer technology is expected to solve problems at the exascale with 1018 calculations each second. Even though these future computers will be incredibly powerful, if they are based on von Neumann type architectures, they will consume between 20 and 30 megawatts of power and will not have intrinsic physically built-in capabilities to learn or deal with complex data as our brain does. These needs can be addressed by neuromorphic computing systems which are inspired by the biological concepts of the human brain. This new generation of computers has the potential to be used for the storage and processing of large amounts of digital information with much lower power consumption than conventional processors. Among their potential future applications, an important niche is moving the control from data centers to edge devices.
The aim of this Roadmap is to present a snapshot of the present state of neuromorphic technology and provide an opinion on the challenges and opportunities that the future holds in the major areas of neuromorphic technology, namely materials, devices, neuromorphic circuits, neuromorphic algorithms, applications, and ethics. The Roadmap is a collection of perspectives where leading researchers in the neuromorphic community provide their own view about the current state and the future challenges. We hope that this Roadmap will be a useful resource to readers outside this field, for those who are just entering the field, and for those who are well established in the neuromorphic community.
https://doi.org/10.1088/2634-4386/ac4a83
△ Less
Submitted 13 January, 2022; v1 submitted 12 May, 2021;
originally announced May 2021.
-
Pipelines for Procedural Information Extraction from Scientific Literature: Towards Recipes using Machine Learning and Data Science
Authors:
Huichen Yang,
Carlos A. Aguirre,
Maria F. De La Torre,
Derek Christensen,
Luis Bobadilla,
Emily Davich,
Jordan Roth,
Lei Luo,
Yihong Theis,
Alice Lam,
T. Yong-** Han,
David Buttler,
William H. Hsu
Abstract:
This paper describes a machine learning and data science pipeline for structured information extraction from documents, implemented as a suite of open-source tools and extensions to existing tools. It centers around a methodology for extracting procedural information in the form of recipes, stepwise procedures for creating an artifact (in this case synthesizing a nanomaterial), from published scie…
▽ More
This paper describes a machine learning and data science pipeline for structured information extraction from documents, implemented as a suite of open-source tools and extensions to existing tools. It centers around a methodology for extracting procedural information in the form of recipes, stepwise procedures for creating an artifact (in this case synthesizing a nanomaterial), from published scientific literature. From our overall goal of producing recipes from free text, we derive the technical objectives of a system consisting of pipeline stages: document acquisition and filtering, payload extraction, recipe step extraction as a relationship extraction task, recipe assembly, and presentation through an information retrieval interface with question answering (QA) functionality. This system meets computational information and knowledge management (CIKM) requirements of metadata-driven payload extraction, named entity extraction, and relationship extraction from text. Functional contributions described in this paper include semi-supervised machine learning methods for PDF filtering and payload extraction tasks, followed by structured extraction and data transformation tasks beginning with section extraction, recipe steps as information tuples, and finally assembled recipes. Measurable objective criteria for extraction quality include precision and recall of recipe steps, ordering constraints, and QA accuracy, precision, and recall. Results, key novel contributions, and significant open problems derived from this work center around the attribution of these holistic quality measures to specific machine learning and inference stages of the pipeline, each with their performance measures. The desired recipes contain identified preconditions, material inputs, and operations, and constitute the overall output generated by our computational information and knowledge management (CIKM) system.
△ Less
Submitted 16 December, 2019;
originally announced December 2019.
-
Using deep learning to reveal the neural code for images in primary visual cortex
Authors:
William F. Kindel,
Elijah D. Christensen,
Joel Zylberberg
Abstract:
Primary visual cortex (V1) is the first stage of cortical image processing, and a major effort in systems neuroscience is devoted to understanding how it encodes information about visual stimuli. Within V1, many neurons respond selectively to edges of a given preferred orientation: these are known as simple or complex cells, and they are well-studied. Other neurons respond to localized center-surr…
▽ More
Primary visual cortex (V1) is the first stage of cortical image processing, and a major effort in systems neuroscience is devoted to understanding how it encodes information about visual stimuli. Within V1, many neurons respond selectively to edges of a given preferred orientation: these are known as simple or complex cells, and they are well-studied. Other neurons respond to localized center-surround image features. Still others respond selectively to certain image stimuli, but the specific features that excite them are unknown. Moreover, even for the simple and complex cells-- the best-understood V1 neurons-- it is challenging to predict how they will respond to natural image stimuli. Thus, there are important gaps in our understanding of how V1 encodes images. To fill this gap, we train deep convolutional neural networks to predict the firing rates of V1 neurons in response to natural image stimuli, and find that 15% of these neurons are within 10% of their theoretical limit of predictability. For these well predicted neurons, we invert the predictor network to identify the image features (receptive fields) that cause the V1 neurons to spike. In addition to those with previously-characterized receptive fields (Gabor wavelet and center-surround), we identify neurons that respond predictably to higher-level textural image features that are not localized to any particular region of the image.
△ Less
Submitted 19 June, 2017;
originally announced June 2017.
-
Counterexamples to conjectures about Subset Takeaway and counting linear extensions of a Boolean lattice
Authors:
Andries E. Brouwer,
J. Daniel Christensen
Abstract:
We develop an algorithm for efficiently computing recursively defined functions on posets. We illustrate this algorithm by disproving conjectures about the game Subset Takeaway (Chomp on a hypercube) and computing the number of linear extensions of the lattice of a 7-cube and related lattices.
We develop an algorithm for efficiently computing recursively defined functions on posets. We illustrate this algorithm by disproving conjectures about the game Subset Takeaway (Chomp on a hypercube) and computing the number of linear extensions of the lattice of a 7-cube and related lattices.
△ Less
Submitted 10 July, 2017; v1 submitted 9 February, 2017;
originally announced February 2017.
-
SROS: Securing ROS over the wire, in the graph, and through the kernel
Authors:
Ruffin White,
Dr. Henrik I. Christensen,
Dr. Morgan Quigley
Abstract:
SROS is a proposed addition to the ROS API and ecosystem to support modern cryptography and security measures. An overview of current progress will be presented, rationalizing each major advancement, including: over-the-wire cryptography for all data transport, namespaced access control enforcing graph policies/restrictions, and finally process profiles using Linux Security Modules to harden a nod…
▽ More
SROS is a proposed addition to the ROS API and ecosystem to support modern cryptography and security measures. An overview of current progress will be presented, rationalizing each major advancement, including: over-the-wire cryptography for all data transport, namespaced access control enforcing graph policies/restrictions, and finally process profiles using Linux Security Modules to harden a node's resource access. By making the community aware of the vulnerabilities in ROS, as well as the proposed solutions provided by SROS, we intend to improve the state of security for future robotics subsystems.
△ Less
Submitted 21 November, 2016;
originally announced November 2016.
-
Towards Python-based Domain-specific Languages for Self-reconfigurable Modular Robotics Research
Authors:
Mikael Moghadam,
David Johan Christensen,
David Brandt,
Ulrik Pagh Schultz
Abstract:
This paper explores the role of operating system and high-level languages in the development of software and domain-specific languages (DSLs) for self-reconfigurable robotics. We review some of the current trends in self-reconfigurable robotics and describe the development of a software system for ATRON II which utilizes Linux and Python to significantly improve software abstraction and portabilit…
▽ More
This paper explores the role of operating system and high-level languages in the development of software and domain-specific languages (DSLs) for self-reconfigurable robotics. We review some of the current trends in self-reconfigurable robotics and describe the development of a software system for ATRON II which utilizes Linux and Python to significantly improve software abstraction and portability while providing some basic features which could prove useful when using Python, either stand-alone or via a DSL, on a self-reconfigurable robot system. These features include transparent socket communication, module identification, easy software transfer and reliable module-to-module communication. The end result is a software platform for modular robots that where appropriate builds on existing work in operating systems, virtual machines, middleware and high-level languages.
△ Less
Submitted 22 February, 2013;
originally announced February 2013.
