We give an adequate, concrete, categorical-based model for Lambda-${\mathcal S}$, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-${\mathcal S}$ is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables and to consider all lambda-terms as algebraic linear functions. The type system of Lambda-${\mathcal S}$ has a superposition constructor S such that a type A is considered as the base of a vector space, while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over $\mathbb C$. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

Modal logic enjoys topological semantics that may be traced back to McKinsey and Tarski, and the classification of topological spaces via modal axioms is a lively area of research. In the past two decades, there has been interest in extending topological modal logic to the language of the mu-calculus, but previously no class of topological spaces was known to be mu-calculus definable that was not already modally definable. In this paper, we show that the full mu-calculus is indeed more expressive than standard modal logic, in the sense that there are classes of topological spaces (and weakly transitive Kripke frames), which are mu-definable but not modally definable. The classes we exhibit satisfy a modally definable property outside of their perfect core, and thus we dub them imperfect spaces. We show that the mu-calculus is sound and complete for these classes. Our examples are minimal in the sense that they use a single instance of a greatest fixed point, and we show that least fixed points alone do not suffice to define any class of spaces that is not already modally definable.

Consider a locally cartesian closed category with an object $\mathbb{I}$ and a class of trivial fibrations, which admit sections and are stable under pushforward and retract as arrows. Define the fibrations to be those maps whose Leibniz exponential with the generic point of $\mathbb{I}$ defines a trivial fibration. Then the fibrations are also closed under pushforward.

Alternating direction method of multipliers (ADMM) receives much attention in the field of optimization and computer science, etc. The generalized ADMM (G-ADMM) proposed by Eckstein and Bertsekas incorporates an acceleration factor and is more efficient than the original ADMM. However, G-ADMM is not applicable in some models where the objective function value (or its gradient) is computationally costly or even impossible to compute. In this paper, we consider the two-block separable convex optimization problem with linear constraints, where only noisy estimations of the gradient of the objective function are accessible. Under this setting, we propose a stochastic linearized generalized ADMM (called SLG-ADMM) where two subproblems are approximated by some linearization strategies. And in theory, we analyze the expected convergence rates and large deviation properties of SLG-ADMM. In particular, we show that the worst-case expected convergence rates of SLG-ADMM are $\mathcal{O}\left( {{N}^{-1/2}}\right)$ and $\mathcal{O}\left({\ln N} \cdot {N}^{-1}\right)$ for solving general convex and strongly convex problems, respectively, where N is the iteration number, similarly hereinafter, and with high probability, SLG-ADMM has $\mathcal{O}\left ( \ln N \cdot N^{-1/2} \right ) $ and $\mathcal{O}\left ( \left ( \ln N \right )^{2} \cdot N^{-1} \right ) $ constraint violation bounds and objective error bounds for general convex and strongly convex problems, respectively.

In this paper, we present a constructive and proof-relevant development of graph theory, including the notion of maps, their faces and maps of graphs embedded in the sphere, in homotopy type theory (HoTT). This allows us to provide an elementary characterisation of planarity for locally directed finite and connected multigraphs that takes inspiration from topological graph theory, particularly from combinatorial embeddings of graphs into surfaces. A graph is planar if it has a map and an outer face with which any walk in the embedded graph is walk-homotopic to another. A result is that this type of planar maps forms a homotopy set for a graph. As a way to construct examples of planar graphs inductively, extensions of planar maps are introduced. We formalise the essential parts of this work in the proof assistant Agda with support for HoTT.

Monads prove to be useful mathematical tools in theoretical computer science, notably in denoting different effects of programming languages. In this paper, we investigate a type of monads which arise naturally from Keimel and Lawson’s $\mathbf{K}$-ification.

A subcategory of $\mathbf{TOP}_{\mathbf{0}}$ is called of type $\mathrm{K}^{*}$ if it consists of monotone convergence spaces and is of type $\mathrm K$ in the sense of Keimel and Lawson. Each such category induces a canonical monad $\mathcal K$ on the category $\mathbf{DCPO}$ of dcpos and Scott-continuous maps, which is called the order-$\mathbf{K}$-ification monad in this paper. First, for each category of type $\mathrm{K}^{*}$, we characterize the algebras of the corresponding monad $\mathcal K$ as k-complete posets and algebraic homomorphisms as k-continuous maps, from which we obtain that the order-$\mathbf{K}$-ification monad gives the free k-complete poset construction over the category $\mathbf{POS}_{\mathbf{d}}$ of posets and Scott-continuous maps. In addition, we show that all k-complete posets and Scott-continuous maps form a Cartesian closed category. Moreover, we consider the strongness of the order-K-ification monad and conclude with the fact that each order-K-ification monad is always commutative.

We present an adapted construction of algebraic circuits over the reals introduced by Cucker and Meer to arbitrary infinite integral domains and generalize the $\mathrm{AC}_{\mathbb{R}}$ and $\mathrm{NC}_{\mathbb{R}}^{}$ classes for this setting. We give a theorem in the style of Immerman’s theorem which shows that for these adapted formalisms, sets decided by circuits of constant depth and polynomial size are the same as sets definable by a suitable adaptation of first-order logic. Additionally, we discuss a generalization of the guarded predicative logic by Durand, Haak and Vollmer, and we show characterizations for the $\mathrm{AC}_{R}$ and $\mathrm{NC}_R^{}$ hierarchy. Those generalizations apply to the Boolean $\mathrm{AC}$ and $\mathrm{NC}$ hierarchies as well. Furthermore, we introduce a formalism to be able to compare some of the aforementioned complexity classes with different underlying integral domains.

Lax extensions of set functors play a key role in various areas, including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is induced by a class of predicate liftings; we discuss several implications of this result.

In this article, we study the complexity of weighted team definability for logics with team semantics. This problem is a natural analog of one of the most studied problems in parameterized complexity, the notion of weighted Fagin-definability, which is formulated in terms of satisfaction of first-order formulas with free relation variables. We focus on the parameterized complexity of weighted team definability for a fixed formula $\varphi$ of central team-based logics. Given a first-order structure $\mathcal{A}$ and the parameter value $k\in \mathbb N$ as input, the question is to determine whether $\mathcal{A},T\models \varphi$ for some team T of size k. We show several results on the complexity of this problem for dependence, independence, and inclusion logic formulas. Moreover, we also relate the complexity of weighted team definability to the complexity classes in the well-known W-hierarchy as well as paraNP.

Given a graph G, the minimum Connected-k-Subgraph Cover problem (MinCkSC) is to find a minimum vertex subset C of G such that every connected subgraph of G on k vertices has at least one vertex in C. If furthermore the subgraph of G induced by C is connected, then the problem is denoted as MinCkSC$_{con}$. In this paper, we first present a PTAS for MinCkSC on an H-minor-free graph, where H is a graph with a constant number of vertices. Then, we design an $O((\omega+1)(2(k-1)(\omega+2))^{3\omega+3})|V|$-time FPT algorithm for MinCkSC$_{con}$ on a graph with treewidth $\omega$, based on which we further design an $O(2^{O(\sqrt{t}\log t)}|V|^{O(1)})$ time subexponential FPT algorithm for MinCkSC$_{con}$ on an H-minor-free graph, where t is an upper bound of solution size.

We give a construction of the free dcpo-cone over any dcpo. There are two steps for getting this result. Firstly, we extend the notion of power domain to directed spaces which are equivalent to $T_0$ monotone-determined spaces introduced by Erné, and we construct the probabilistic powerspace of the monotone determined space, which is defined as a free monotone determined cone. Secondly, we take D-completion of the free monotone determined cone over the dcpo with its Scott topology. In addition, we show that generally the valuation power domain of any dcpo is not the free dcpo-cone.

Learning finite automata (termed as model learning) has become an important field in machine learning and has been useful realistic applications. Quantum finite automata (QFA) are simple models of quantum computers with finite memory. Due to their simplicity, QFA have well physical realizability, but one-way QFA still have essential advantages over classical finite automata with regard to state complexity (two-way QFA are more powerful than classical finite automata in computation ability as well). As a different problem in quantum learning theory and quantum machine learning, in this paper, our purpose is to initiate the study of learning QFA with queries (naturally it may be termed as quantum model learning), and the main results are regarding learning two basic one-way QFA (1QFA): (1) we propose a learning algorithm for measure-once 1QFA (MO-1QFA) with query complexity of polynomial time and (2) we propose a learning algorithm for measure-many 1QFA (MM-1QFA) with query complexity of polynomial time, as well.

We present algorithms and a C code to reveal quantum contextuality and evaluate the contextuality degree (a way to quantify contextuality) for a variety of point-line geometries located in binary symplectic polar spaces of small rank. With this code we were not only able to recover, in a more efficient way, all the results of a recent paper by de Boutray et al. [(2022). Journal of Physics A: Mathematical and Theoretical 55 475301], but also arrived at a bunch of new noteworthy results. The paper first describes the algorithms and the C code. Then it illustrates its power on a number of subspaces of symplectic polar spaces whose rank ranges from 2 to 7. The most interesting new results include: (i) non-contextuality of configurations whose contexts are subspaces of dimension 2 and higher, (ii) non-existence of negative subspaces of dimension 3 and higher, (iii) considerably improved bounds for the contextuality degree of both elliptic and hyperbolic quadrics for rank 4, as well as for a particular subgeometry of the three-qubit space whose contexts are the lines of this space, (iv) proof for the non-contextuality of perpsets and, last but not least, (v) contextual nature of a distinguished subgeometry of a multi-qubit doily, called a two-spread, and computation of its contextuality degree. Finally, in the three-qubit polar space we correct and improve the contextuality degree of the full configuration and also describe finite geometric configurations formed by unsatisfiable/invalid constraints for both types of quadrics as well as for the geometry whose contexts are all 315 lines of the space.

We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the ‘inner’ and the ‘outer’ type theory. In our case of interest, the inner theory is homotopy type theory (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating uniqueness of identity proofs (UIP). One point of view on it is as internalised meta-theory of the inner type theory. There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level n can be constructed in HoTT for any externally fixed natural number n. Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where n will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models. Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky’s Homotopy Type System (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be assumed by postulating that the inner and outer natural numbers types are isomorphic. After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of $(\infty,1)$-category and give some examples.

Let $T=(V,E)$ be a tree in which each edge is assigned a cost; let $\mathcal{P}$ be a set of source–sink pairs of vertices in V in which each source–sink pair produces a profit. Given a lower bound K for the profit, the K-prize-collecting multicut problem in trees with submodular penalties is to determine a partial multicut $M\subseteq E$ such that the total profit of the disconnected pairs after removing M from T is at least K, and the total cost of edges in M plus the penalty of the set of still-connected pairs is minimized, where the penalty is determined by a nondecreasing submodular function. Based on the primal-dual scheme, we present a combinatorial polynomial-time algorithm by carefully increasing the penalty. In the theoretical analysis, we prove that the approximation factor of the proposed algorithm is $(\frac{8}{3}+\frac{4}{3}\kappa+\varepsilon)$, where $\kappa$ is the total curvature of the submodular function and $\varepsilon$ is any fixed positive number. Experiments reveal that the objective value of the solutions generated by the proposed algorithm is less than 130% compared with that of the optimal value in most cases.

A game that characterizes equivalence of structures with respect to all first-order sentences containing a given number of quantifiers was introduced by Immerman in 1981. We define three other games and prove that they are all equivalent to the Immerman game, and hence also give a characterization for the number of quantifiers needed for separating structures. In the Immerman game, Duplicator has a canonical optimal strategy, and hence Duplicator can be completely removed from the game by replacing her moves with default moves given by this optimal strategy. On the other hand, in the last two of our games there is no such optimal strategy for Duplicator. Thus, the Immerman game can be regarded as a one-player game, but two of our games are genuine two-player games.

On a locally $\lambda$-presentable symmetric monoidal closed category $\mathcal {V}$, $\lambda$-ary enriched equational theories correspond to enriched monads preserving $\lambda$-filtered colimits. We introduce discrete $\lambda$-ary enriched equational theories where operations are induced by those having discrete arities (equations are not required to have discrete arities) and show that they correspond to enriched monads preserving preserving $\lambda$-filtered colimits and surjections. Using it, we prove enriched Birkhof-type theorems for categories of algebras of discrete theories. This extends known results from metric spaces and posets to general symmetric monoidal closed categories.

We introduce three measures of complexity for families of sets. Each of the three measures, which we call dimensions, is defined in terms of the minimal number of convex subfamilies that are needed for covering the given family. For upper dimension, the subfamilies are required to contain a unique maximal set, for dual upper dimension a unique minimal set, and for cylindrical dimension both a unique maximal and a unique minimal set. In addition to considering dimensions of particular families of sets, we study the behavior of dimensions under operators that map families of sets to new families of sets. We identify natural sufficient criteria for such operators to preserve the growth class of the dimensions. We apply the theory of our dimensions for proving new hierarchy results for logics with team semantics. To this end we associate each atom with a natural notion or arity. First, we show that the standard logical operators preserve the growth classes of the families arising from the semantics of formulas in such logics. Second, we show that the upper dimension of $k+1$-ary dependence, inclusion, independence, anonymity, and exclusion atoms is in a strictly higher growth class than that of any k-ary atoms, whence the $k+1$-ary atoms are not definable in terms of any atoms of smaller arity.