We discuss the complexity of completions of partial combinatory algebras, in particular, of Kleene’s first model. Various completions of this model exist in the literature, but all of them have high complexity. We show that although there are no computable completions, there exist completions of low Turing degree. We use this construction to relate completions of Kleene’s first model to complete extensions of $\mathrm{PA}$. We also discuss the complexity of pcas defined from nonstandard models of $\mathrm{PA}$.

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.

The authors’ primary goal in this paper is to enhance the study of $T_0$ topological spaces by using the order of specialization of a $T_0$-space to introduce the lower topology (with a subbasis of closed sets $\mathord{\uparrow } x$) and studying the interaction of the original topology and the lower topology. Using the lower topology, one can define and study new properties of the original space that provide deeper insight into its structure. One focus of study is the property R, which asserts that if the intersection of a family of finitely generated sets $\mathord{\uparrow } F$, $F$ finite, is contained in an open set $U$, then the same is true for finitely many of the family. We first show that property R is equivalent to several other interesting properties, for example, the property that all closed subsets of the original space are compact in the lower topology. We then find conditions under which these spaces are compact, well-filtered, and coherent, a weaker variant of stably compact spaces. We also investigate what have been called strong $d$-spaces, develop some of their basic properties, and make connections with the earlier considerations involving spaces satisfying property R. Two key results we obtain are that if a dcpo $P$ with the Scott topology is a strong $d$-space, then it is well-filtered, and if additionally the Scott topology of the product $P\times P$ is the product of the Scott topologies of the factors, then the Scott space of $P$ is sober. We also exhibit connections of this work with de Groot duality.

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.

Computability on uncountable sets has no standard formalization, unlike that on countable sets, which is given by Turing machines. Some of the approaches to define computability in these sets rely on order-theoretic structures to translate such notions from Turing machines to uncountable spaces. Since these machines are used as a baseline for computability in these approaches, countability restrictions on the ordered structures are fundamental. Here, we show several relations between the usual countability restrictions in order-theoretic theories of computability and some more common order-theoretic countability constraints, like order density properties and functional characterizations of the order structure in terms of multi-utilities. As a result, we show how computability can be introduced in some order structures via countability order density and multi-utility constraints.

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.

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.

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.