An official website of the United States government
It was recently argued by Nguyen, Tanizaki and Ünsal that two-dimensional pure Yang–Mills theory is equivalent to (decomposes into) a disjoint union of (invertible) quantum field theories, known as universes. In this paper, we compare this decomposition to the Gross–Taylor expansion of two-dimensional pure [Formula: see text] Yang–Mills theory in the large-[Formula: see text] limit as the string field theory of a sigma model. Specifically, we study the Gross–Taylor expansion of individual Nguyen–Tanizaki–Ünsal universes. These differ from the Gross–Taylor expansion of the full Yang–Mills theory in two ways: a restriction to single instanton degrees, and some additional contributions not present in the expansion of the full Yang–Mills theory. We propose to interpret the restriction to single instanton degrees as implying a constraint, namely that the Gross–Taylor string has a global (higher-form) symmetry with Noether current related to the worldsheet instanton number. We compare two-dimensional pure Maxwell theory as a prototype obeying such a constraint, and also discuss in that case an analogue of the Witten effect arising under two-dimensional theta angle rotation. We also propose a geometric interpretation of the additional terms, in the special case of Yang–Mills theories on 2-spheres. In addition, also for the case of theories on 2-spheres, we propose a reinterpretation of the terms in the Gross–Taylor expansion of the Nguyen–Tanizaki–Ünsal universes, replacing sigma models on branched covers by counting disjoint unions of stacky copies of the target Riemann surface, that makes the Nguyen–Tanizaki–Ünsal decomposition into invertible field theories more nearly manifest. As the Gross–Taylor string is a sigma model coupled to worldsheet gravity, we also briefly outline the tangentially related topic of decomposition in two-dimensional theories coupled to gravity.
more »
« less
Stratified Type Theory
A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type axiom. In this work, we argue that a universe hierarchy is not the only option for universes in type theory. Taking inspiration from Leivant’s Stratified System F, we introduce Stratified Type Theory (StraTT), where rather than stratifying universes by levels, we stratify typing judgements and restrict the domain of dependent functions to strictly lower levels. Even with type-in-type, this restriction suffices to enforce consistency. In StraTT, we consider a number of extensions beyond just stratified dependent functions. First, the subsystem subStraTT employs McBride’s crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where global definitions with concrete levels can be displaced uniformly to any higher level. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full StraTT includes a separate nondependent function type with a floating domain whose level matches that of the overall function type. Finally, we have implemented a prototype type checker for StraTT extended with datatypes and inference for level and displacement annotations, along with a small core library. We have proven subStraTT to be consistent and StraTT to be type safe, but consistency of the full remains an open problem, largely due to the interaction between floating functions and cumulativity of judgements. Nevertheless, we StraTT believe to be consistent, and as evidence have verified the ill-typedness of some well-known type-theoretic paradoxes using our implementation.
more »
« less
- Award ID(s):
- 2327738
- PAR ID:
- 10650830
- Publisher / Repository:
- Springer Nature Switzerland
- Date Published:
- Page Range / eLocation ID:
- 236 to 263
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Abstract We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an ordered linear restriction on standard predicate logic, which guarantees that all functions between categories are functorial, all relations are profunctorial, and all transformations are natural by construction, with no separate proofs necessary. Important category-theoretic proofs such as the Yoneda lemma and Co-yoneda lemma become simple type-theoretic proofs about the relationship between unit, tensor and (ordered) function types, and can be seen to be ordered refinements of theorems in predicate logic. The type theory is sound and complete for a categorical model invirtual equipments, which model both internal and enriched category theory. While the proofs in our type theory look like standard set-based arguments, the syntactic discipline ensure that all proofs and constructions carry over to enriched and internal settings as well.more » « less
-
The Dependent Calculus of Indistinguishability (DCOI) uses dependency tracking to identify irrelevant arguments and uses indistinguishability during type conversion to enable proof irrelevance, supporting run-time and compile-time irrelevance with the same uniform mechanism. DCOI also internalizes reasoning about indistinguishability through the use of a propositional equality type indexed by an observer level. As DCOI is a pure type system, prior work establishes only its syntactic type safety, justifying its use as the basis for a programming language with dependent types. However, it was not clear whether any instance of this system would be suitable for use as a type theory for theorem proving. Here, we identify a suitable instance DCOIω, which has an infinite predicative universe hierarchy. We show that DCOIω is logically consistent, normalizing, and that type conversion is decidable. We have mechanized all results using the Coq proof assistant.more » « less
-
Information technologies enable programmers and engineers to design and synthesize systems of startling complexity that nonetheless behave as intended. This mastery of complexity is made possible by a hierarchy of formal abstractions that span from high-level programming languages down to low-level implementation specifications, with rigorous connections between the levels. DNA nanotechnology presents us with a new molecular information technology whose potential has not yet been fully unlocked in this way. Developing an effective hierarchy of abstractions may be critical for increasing the complexity of programmable DNA systems. Here, we build on prior practice to provide a new formalization of ‘domain-level’ representations of DNA strand displacement systems that has a natural connection to nucleic acid biophysics while still being suitable for formal analysis. Enumeration of unimolecular and bimolecular reactions provides a semantics for programmable molecular interactions, with kinetics given by an approximate biophysical model. Reaction condensation provides a tractable simplification of the detailed reactions that respects overall kinetic properties. The applicability and accuracy of the model is evaluated across a wide range of engineered DNA strand displacement systems. Thus, our work can serve as an interface between lower-level DNA models that operate at the nucleotide sequence level, and high-level chemical reaction network models that operate at the level of interactions between abstract species.more » « less
-
We study notions of generic and coarse computability in the context of computable structure theory. Our notions are stratified by the Σβ hierarchy. We focus on linear orderings. We show that at the Σ1 level, all linear orderings have both generically and coarsely computable copies. This behavior changes abruptly at higher levels; we show that at the Σα+2 level for any α ∈ ωCK 1 the set of linear orderings with generically or coarsely computable copies is Σ1 1-complete and therefore maximally complicated. This development is new even in the general analysis of generic and coarse computability of countable structures. In the process of proving these results, we introduce new tools for understanding generically and coarsely computable structures. We are able to give a purely structural statement that is equivalent to having a generically computable copy and show that every relational structure with only finitely many relations has coarsely and generically computable copies at the lowest level of the hierarchy.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Book Chapter:
- https://doi.org/10.1007/978-3-031-91118-7_10
