We develop a constructive theory of finite multisets, defining them as free commutative monoids in Homotopy Type Theory. We formalise two algebraic presentations of this construction using 1-HITs, establishing the universal property for each and thereby their equivalence. These presentations correspond to equational theories including a commutation axiom. In this setting, we prove important structural combinatorial properties of singleton multisets arising from concatenations and projections of multisets. This is done in generality, without assuming decidable equality on the carrier set. Further, as applications, we present a constructive formalisation of the relational model of differential linear logic and use it to characterise the equality type of multisets. This leads us to the introduction of a novel conditional equational presentation of the finite-multiset construction.

0
下载
关闭预览

相关内容

We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak $\omega$-categories, and we formalise this theory in the language of homotopy type theory. Most of the studies about this type theory assume that it is well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and thorough about what these properties are exactly. We use the formalisation that we provide to list and formally prove all of these meta-properties, thus filling a gap in the foundational aspect. We discuss the key aspects of the formalisation inherent to the theory CaTT, in particular that the absence of definitional equality greatly simplify the study, but also that specific side conditions are challenging to properly model. We present the formalisation in a way that not only handles the type theory CaTT but also all the related type theories that share the same structure, and in particular we show that this formalisation provides a proper ground to the study of the theory MCaTT which describes the globular, monoidal weak $\omega$-categories. The article is accompanied by a development in the proof assistant Agda to actually check the formalisation that we present.

0
0
下载
预览

Signature-based algorithms have become a standard approach for computing Gr\"obner bases in commutative polynomial rings. However, so far, it was not clear how to extend this concept to the setting of noncommutative polynomials in the free algebra. In this paper, we present a signature-based algorithm for computing Gr\"obner bases in precisely this setting. The algorithm is an adaptation of Buchberger's algorithm including signatures. We prove that our algorithm correctly enumerates a signature Gr\"obner basis as well as a Gr\"obner basis of the module generated by the leading terms of the generators' syzygies, and that it terminates whenever the ideal admits a finite signature Gr\"obner basis. Additionally, we adapt well-known signature-based criteria eliminating redundant reductions, such as the syzygy criterion, the F5 criterion and the singular criterion, to the case of noncommutative polynomials. We also generalize reconstruction methods from the commutative setting that allow to recover, from partial information about signatures, the coordinates of elements of a Gr\"obner basis in terms of the input polynomials, as well as a basis of the syzygy module of the generators. We have written a toy implementation of all the algorithms in the Mathematica package OperatorGB and we compare our signature-based algorithm to the classical Buchberger algorithm for noncommutative polynomials.

0
0
下载
预览

This paper introduces meta-factorization, a theory that describes matrix decompositions as solutions of linear matrix equations: the projector and the reconstruction equation. Meta-factorization reconstructs known factorizations, reveals their internal structures, and allows for introducing modifications, as illustrated with the example of SVD, QR, and UTV factorizations. The prospect of meta-factorization also provides insights into computational aspects of generalized matrix inverses and randomized linear algebra algorithms. The relations between the Moore-Penrose pseudoinverse, generalized Nystr\"{o}m method, and the CUR decomposition are revealed here as an illustration. Finally, meta-factorization offers hints on the structure of new factorizations and provides the potential of creating them.

0
0
下载
预览

The maximum matching problem in dynamic graphs subject to edge updates (insertions and deletions) has received much attention over the last few years; a multitude of approximation/time tradeoffs were obtained, improving upon the folklore algorithm, which maintains a maximal (and hence $2$-approximate) matching in $O(n)$ worst-case update time in $n$-node graphs. We present the first deterministic algorithm which outperforms the folklore algorithm in terms of {\em both} approximation ratio and worst-case update time. Specifically, we give a $(2-\Omega(1))$-approximate algorithm with $O(m^{3/8})=O(n^{3/4})$ worst-case update time in $n$-node, $m$-edge graphs. For sufficiently small constant $\epsilon>0$, no deterministic $(2+\epsilon)$-approximate algorithm with worst-case update time $O(n^{0.99})$ was known. Our second result is the first deterministic $(2+\epsilon)$-approximate weighted matching algorithm with $O_\epsilon(1)\cdot O(\sqrt[4]{m}) = O_\epsilon(1)\cdot O(\sqrt{n})$ worst-case update time. Our main technical contributions are threefold: first, we characterize the tight cases for \emph{kernels}, which are the well-studied matching sparsifiers underlying much of the $(2+\epsilon)$-approximate dynamic matching literature. This characterization, together with multiple ideas -- old and new -- underlies our result for breaking the approximation barrier of $2$. Our second technical contribution is the first example of a dynamic matching algorithm whose running time is improved due to improving the \emph{recourse} of other dynamic matching algorithms. Finally, we show how to use dynamic bipartite matching algorithms as black-box subroutines for dynamic matching in general graphs without incurring the natural $\frac{3}{2}$ factor in the approximation ratio which such approaches naturally incur.

0
0
下载
预览

Weak $\omega$-categories are notoriously difficult to define because of the very intricate nature of their axioms. Various approaches have been explored, based on different shapes given to the cells. Interestingly, homotopy type theory encompasses a definition of weak $\omega$-groupoid in a globular setting, since every type carries such a structure. Starting from this remark, Brunerie could extract this definition of globular weak $\omega$\nobreakdash-groupoids, formulated as a type theory. By refining its rules, Finster and Mimram have then defined a type theory called CaTT, whose models are weak $\omega$-categories. Here, we generalize this approach to monoidal weak $\omega$-categories. Based on the principle that they should be equivalent to weak $\omega$-categories with only one $0$-cell, we are able to derive a type theory MCaTT whose models are monoidal categories. This requires changing the rules of the theory in order to encode the information carried by the unique $0$-cell. The correctness of the resulting type theory is shown by defining a pair of translations between our type theory MCaTT and the type theory CaTT. Our main contribution is to show that these translations relate the models of our type theory to the models of the type theory CaTT consisting of $\omega$-categories with only one $0$-cell, by analyzing in details how the notion of models interact with the structural rules of both type theories.

0
0
下载
预览

Survival outcomes are common in comparative effectiveness studies and require unique handling because they are usually incompletely observed due to right-censoring. A "once for all" approach for causal inference with survival outcomes constructs pseudo-observations and allows standard methods such as propensity score weighting to proceed as if the outcomes are completely observed. For a general class of model-free causal estimands with survival outcomes on user-specified target populations, we develop corresponding propensity score weighting estimators based on the pseudo-observations and establish their asymptotic properties. In particular, utilizing the functional delta-method and the von Mises expansion, we derive a new closed-form variance of the weighting estimator that takes into account the uncertainty due to both pseudo-observation calculation and propensity score estimation. This allows valid and computationally efficient inference without resampling. We also prove the optimal efficiency property of the overlap weights within the class of balancing weights for survival outcomes. The proposed methods are applicable to both binary and multiple treatments. Extensive simulations are conducted to explore the operating characteristics of the proposed method versus other commonly used alternatives. We apply the proposed method to compare the causal effects of three popular treatment approaches for prostate cancer patients.

0
0
下载
预览

For points $(a,b)$ on an algebraic curve over a field $K$ with height $\mathfrak{h}$, the asymptotic relation between $\mathfrak{h}(a)$ and $\mathfrak{h}(b)$ has been extensively studied in diophantine geometry. When $K=\overline{k(t)}$ is the field of algebraic functions in $t$ over a field $k$ of characteristic zero, Eremenko in 1998 proved the following quasi-equivalence for an absolute logarithmic height $\mathfrak{h}$ in $K$: Given $P\in K[X,Y]$ irreducible over $K$ and $\epsilon>0$, there is a constant $C$ only depending on $P$ and $\epsilon$ such that for each $(a,b)\in K^2$ with $P(a,b)=0$, $$ (1-\epsilon) \deg(P,Y) \mathfrak{h}(b)-C \leq \deg(P,X) \mathfrak{h}(a) \leq (1+\epsilon) \deg(P,Y) \mathfrak{h}(b)+C. $$ In this article, we shall give an explicit bound for the constant $C$ in terms of the total degree of $P$, the height of $P$ and $\epsilon$. This result is expected to have applications in some other areas such as symbolic computation of differential and difference equations.

0
0
下载
预览

Analogy-making is at the core of human and artificial intelligence and creativity with applications to such diverse tasks as commonsense reasoning, learning, language acquisition, and story telling. This paper introduces from first principles an abstract algebraic framework of analogical proportions of the form `$a$ is to $b$ what $c$ is to $d$' in the general setting of universal algebra. This enables us to compare mathematical objects possibly across different domains in a uniform way which is crucial for AI-systems. It turns out that our notion of analogical proportions has appealing mathematical properties. As we construct our model from first principles using only elementary concepts of universal algebra, and since our model questions some basic properties of analogical proportions presupposed in the literature, to convince the reader of the plausibility of our model we show that it can be naturally embedded into first-order logic via model-theoretic types and prove from that perspective that analogical proportions are compatible with structure-preserving mappings. This provides conceptual evidence for its applicability. In a broader sense, this paper is a first step towards a theory of analogical reasoning and learning systems with potential applications to fundamental AI-problems like commonsense reasoning and computational learning and creativity.

0
0
下载
预览

An adjunction is a pair of functors related by a pair of natural transformations, and relating a pair of categories. It displays how a structure, or a concept, projects from each category to the other, and back. Adjunctions are the common denominator of Galois connections, representation theories, spectra, and generalized quantifiers. We call an adjunction nuclear when its categories determine each other. We show that every adjunction can be resolved into a nuclear adjunction. This resolution is idempotent in a strong sense. The nucleus of an adjunction displays its conceptual core, just as the singular value decomposition of an adjoint pair of linear operators displays their canonical bases. The two composites of an adjoint pair of functors induce a monad and a comonad. Monads and comonads generalize the closure and the interior operators from topology, or modalities from logic, while providing a saturated view of algebraic structures and compositions on one side, and of coalgebraic dynamics and decompositions on the other. They are resolved back into adjunctions over the induced categories of algebras and of coalgebras. The nucleus of an adjunction is an adjunction between the induced categories of algebras and coalgebras. It provides new presentations for both, revealing the meaning of constructing algebras for a comonad and coalgebras for a monad. In his seminal early work, Ross Street described an adjunction between monads and comonads in 2-categories. Lifting the nucleus construction, we show that the resulting Street monad on monads is strongly idempotent, and extracts the nucleus of a monad. A dual treatment achieves the same for comonads. Applying a notable fragment of pure 2-category theory on an acute practical problem of data analysis thus led to new theoretical result.

0
0
下载
预览

We consider the task of learning the parameters of a {\em single} component of a mixture model, for the case when we are given {\em side information} about that component, we call this the "search problem" in mixture models. We would like to solve this with computational and sample complexity lower than solving the overall original problem, where one learns parameters of all components. Our main contributions are the development of a simple but general model for the notion of side information, and a corresponding simple matrix-based algorithm for solving the search problem in this general setting. We then specialize this model and algorithm to four common scenarios: Gaussian mixture models, LDA topic models, subspace clustering, and mixed linear regression. For each one of these we show that if (and only if) the side information is informative, we obtain parameter estimates with greater accuracy, and also improved computation complexity than existing moment based mixture model algorithms (e.g. tensor methods). We also illustrate several natural ways one can obtain such side information, for specific problem instances. Our experiments on real data sets (NY Times, Yelp, BSDS500) further demonstrate the practicality of our algorithms showing significant improvement in runtime and accuracy.

0
3
下载
预览
小贴士
相关主题
相关论文
Thibaut Benjamin
0+阅读 · 11月29日
Michał P. Karpowicz
0+阅读 · 11月29日
Mohammad Roghani,Amin Saberi,David Wajc
0+阅读 · 11月28日
Thibaut Benjamin
0+阅读 · 11月28日
Shuxi Zeng,Fan Li,Liangyuan Hu,Fan Li
0+阅读 · 11月27日
Ruyong Feng,Shuang Feng,Li-Yong Shen
0+阅读 · 11月25日
Christian Antić
0+阅读 · 11月24日
Dusko Pavlovic,Dominic J. D. Hughes
0+阅读 · 11月24日
Avik Ray,Joe Neeman,Sujay Sanghavi,Sanjay Shakkottai
3+阅读 · 2018年2月24日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
12+阅读 · 2019年5月22日
IEEE | DSC 2019诚邀稿件 (EI检索)
Call4Papers
7+阅读 · 2019年2月25日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
10+阅读 · 2018年12月24日
Disentangled的假设的探讨
CreateAMind
8+阅读 · 2018年12月10日
Hierarchical Disentangled Representations
CreateAMind
3+阅读 · 2018年4月15日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
6+阅读 · 2018年2月7日
【推荐】自然语言处理(NLP)指南
机器学习研究会
33+阅读 · 2017年11月17日
【论文】变分推断(Variational inference)的总结
机器学习研究会
24+阅读 · 2017年11月16日
Auto-Encoding GAN
CreateAMind
5+阅读 · 2017年8月4日
Top