By adapting Salomaa's complete proof system for equality of regular expressions under the language semantics, Milner (1984) formulated a sound proof system for bisimilarity of regular expressions under the process interpretation he introduced. He asked whether this system is complete. Proof-theoretic arguments attempting to show completeness of this equational system are complicated by the presence of a non-algebraic rule for solving fixed-point equations by using star iteration. We characterize the derivational power that the fixed-point rule adds to the purely equational part $\text{Mil$^{\boldsymbol{-}}$}$ of Milner's system $\text{$\text{Mil}$}$: it corresponds to the power of coinductive proofs over $\text{Mil$^{\boldsymbol{-}}$}$ that have the form of finite process graphs with the loop existence and elimination property $\text{LEE}$. We define a variant system $\text{cMil}$ by replacing the fixed-point rule in $\text{Mil}$ with a rule that permits $\text{LEE}$-shaped circular derivations in $\text{Mil$^{\boldsymbol{-}}$}$ from previously derived equations as a premise. With this rule alone we also define the variant system $\text{CLC}$ for merely combining $\text{LEE}$-shaped coinductive proofs over $\text{Mil$^{\boldsymbol{-}}$}$. We show that both $\text{cMil}$ and $\text{CLC}$ have proof interpretations in $\text{Mil}$, and vice versa. As this correspondence links, in both directions, derivability in $\text{Mil}$ with derivation trees of process graphs, it widens the space for graph-based approaches to finding a completeness proof of Milner's system. This report is the extended version of a paper with the same title presented at CALCO 2021.
相關內容
The Stochastic Extragradient (SEG) method is one of the most popular algorithms for solving min-max optimization and variational inequalities problems (VIP) appearing in various machine learning tasks. However, several important questions regarding the convergence properties of SEG are still open, including the sampling of stochastic gradients, mini-batching, convergence guarantees for the monotone finite-sum variational inequalities with possibly non-monotone terms, and others. To address these questions, in this paper, we develop a novel theoretical framework that allows us to analyze several variants of SEG in a unified manner. Besides standard setups, like Same-Sample SEG under Lipschitzness and monotonicity or Independent-Samples SEG under uniformly bounded variance, our approach allows us to analyze variants of SEG that were never explicitly considered in the literature before. Notably, we analyze SEG with arbitrary sampling which includes importance sampling and various mini-batching strategies as special cases. Our rates for the new variants of SEG outperform the current state-of-the-art convergence guarantees and rely on less restrictive assumptions.
Micro-expressions (MEs) are involuntary facial movements revealing people's hidden feelings in high-stake situations and have practical importance in medical treatment, national security, interrogations and many human-computer interaction systems. Early methods for MER mainly based on traditional appearance and geometry features. Recently, with the success of deep learning (DL) in various fields, neural networks have received increasing interests in MER. Different from macro-expressions, MEs are spontaneous, subtle, and rapid facial movements, leading to difficult data collection, thus have small-scale datasets. DL based MER becomes challenging due to above ME characters. To date, various DL approaches have been proposed to solve the ME issues and improve MER performance. In this survey, we provide a comprehensive review of deep micro-expression recognition (MER), including datasets, deep MER pipeline, and the bench-marking of most influential methods. This survey defines a new taxonomy for the field, encompassing all aspects of MER based on DL. For each aspect, the basic approaches and advanced developments are summarized and discussed. In addition, we conclude the remaining challenges and and potential directions for the design of robust deep MER systems. To the best of our knowledge, this is the first survey of deep MER methods, and this survey can serve as a reference point for future MER research.
An influential 1990 paper of Hochbaum and Shanthikumar made it common wisdom that "convex separable optimization is not much harder than linear optimization" [JACM 1990]. We exhibit two fundamental classes of mixed integer (linear) programs that run counter this intuition. Namely those whose constraint matrices have small coefficients and small primal or dual treedepth: While linear optimization is easy [Brand, Kouteck\'y, Ordyniak, AAAI 2021], we prove that separable convex optimization IS much harder. Moreover, in the pure integer and mixed integer linear cases, these two classes have the same parameterized complexity. We show that they yet behave quite differently in the separable convex mixed integer case. Our approach employs the mixed Graver basis introduced by Hemmecke [Math. Prog. 2003]. We give the first non-trivial lower and upper bounds on the norm of mixed Graver basis elements. In previous works involving the integer Graver basis, such upper bounds have consistently resulted in efficient algorithms for integer programming. Curiously, this does not happen in our case. In fact, we even rule out such an algorithm.
Given a graph whose nodes may be coloured red, the parity of the number of red nodes can easily be maintained with first-order update rules in the dynamic complexity framework DynFO of Patnaik and Immerman. Can this be generalised to other or even all queries that are definable in first-order logic extended by parity quantifiers? We consider the query that asks whether the number of nodes that have an edge to a red node is odd. Already this simple query of quantifier structure parity-exists is a major roadblock for dynamically capturing extensions of first-order logic. We show that this query cannot be maintained with quantifier-free first-order update rules, and that variants induce a hierarchy for such update rules with respect to the arity of the maintained auxiliary relations. Towards maintaining the query with full first-order update rules, it is shown that degree-restricted variants can be maintained.
We study substitution tilings that are also discrete plane tilings, that is, satisfy a relaxed version of cut-and-projection. We prove that the Sub Rosa substitution tilings with a 2n-fold rotational symmetry for odd n greater than 5 defined by Kari and Rissanen are not discrete planes, and therefore not cut-and-project tilings either. We then define new Planar Rosa substitution tilings with a 2n-fold rotational symmetry for any odd n, and show that these satisfy the discrete plane condition. The tilings we consider are edge-to-edge rhombus tilings. We give an explicit construction for the 10-fold case, and provide a construction method for the general case of any odd n.
We study the complexity of small-depth Frege proofs and give the first tradeoffs between the size of each line and the number of lines. Existing lower bounds apply to the overall proof size -- the sum of sizes of all lines -- and do not distinguish between these notions of complexity. For depth-$d$ Frege proofs of the Tseitin principle where each line is a size-$s$ formula, we prove that $\exp(n/2^{\Omega(d\sqrt{\log s})})$ many lines are necessary. This yields new lower bounds on line complexity that are not implied by H{\aa}stad's recent $\exp(n^{\Omega(1/d)})$ lower bound on the overall proof size. For $s = \mathrm{poly}(n)$, for example, our lower bound remains $\exp(n^{1-o(1)})$ for all $d = o(\sqrt{\log n})$, whereas H{\aa}stad's lower bound is $\exp(n^{o(1)})$ once $d = \omega_n(1)$. Our main conceptual contribution is the simple observation that techniques for establishing correlation bounds in circuit complexity can be leveraged to establish such tradeoffs in proof complexity.
We present algorithms for computing the reduced Gr\"{o}bner basis of the vanishing ideal of a finite set of points in a frame of ideal interpolation. Ideal interpolation is defined by a linear projector whose kernel is a polynomial ideal. In this paper, we translate interpolation condition functionals into formal power series via Taylor expansion, then the reduced Gr\"{o}bner basis is read from formal power series by Gaussian elimination. Our algorithm has a polynomial time complexity. It compares favorably with MMM algorithm in single point ideal interpolation and some several points ideal interpolation.
Given a graph $G$ of degree $k$ over $n$ vertices, we consider the problem of computing a near maximum cut or a near minimum bisection in polynomial time. For graphs of girth $L$, we develop a local message passing algorithm whose complexity is $O(nkL)$, and that achieves near optimal cut values among all $L$-local algorithms. Focusing on max-cut, the algorithm constructs a cut of value $nk/4+ n\mathsf{P}_\star\sqrt{k/4}+\mathsf{err}(n,k,L)$, where $\mathsf{P}_\star\approx 0.763166$ is the value of the Parisi formula from spin glass theory, and $\mathsf{err}(n,k,L)=o_n(n)+no_k(\sqrt{k})+n \sqrt{k} o_L(1)$ (subscripts indicate the asymptotic variables). Our result generalizes to locally treelike graphs, i.e., graphs whose girth becomes $L$ after removing a small fraction of vertices. Earlier work established that, for random $k$-regular graphs, the typical max-cut value is $nk/4+ n\mathsf{P}_\star\sqrt{k/4}+o_n(n)+no_k(\sqrt{k})$. Therefore our algorithm is nearly optimal on such graphs. An immediate corollary of this result is that random regular graphs have nearly minimum max-cut, and nearly maximum min-bisection among all regular locally treelike graphs. This can be viewed as a combinatorial version of the near-Ramanujan property of random regular graphs.
Current multi-physics Finite Element Method (FEM) solvers are complex systems in terms of both their mathematical complexity and lines of code. This paper proposes a skeleton generic FEM solver, named MetaFEM, in total about 5,000 lines of Julia code, which translates generic input Partial Differential Equation (PDE) weak forms into corresponding GPU-accelerated simulations with a grammar similar to FEniCS or FreeFEM. Two novel approaches differentiate MetaFEM from the common solvers: (1) the FEM kernel is based on an original theory/algorithm which explicitly processes meta-expressions, as the name suggests, and (2) the symbolic engine is a rule-based Computer Algebra System (CAS), i.e., the equations are rewritten/derived according to a set of rewriting rules instead of going through completely fixed routines, supporting easy customization by developers. Example cases in thermal conduction, linear elasticity and incompressible flow are presented to demonstrate utility.
Most of the existing work on automatic facial expression analysis focuses on discrete emotion recognition, or facial action unit detection. However, facial expressions do not always fall neatly into pre-defined semantic categories. Also, the similarity between expressions measured in the action unit space need not correspond to how humans perceive expression similarity. Different from previous work, our goal is to describe facial expressions in a continuous fashion using a compact embedding space that mimics human visual preferences. To achieve this goal, we collect a large-scale faces-in-the-wild dataset with human annotations in the form: Expressions A and B are visually more similar when compared to expression C, and use this dataset to train a neural network that produces a compact (16-dimensional) expression embedding. We experimentally demonstrate that the learned embedding can be successfully used for various applications such as expression retrieval, photo album summarization, and emotion recognition. We also show that the embedding learned using the proposed dataset performs better than several other embeddings learned using existing emotion or action unit datasets.
小貼士
登錄享
注冊地址： 北京市海淀區羊坊店路18號2幢3層301-191