Abstract We study the parameterized complexity of the problem to decide whether a given natural number n satisfies a given $\Delta _0$ -formula $\varphi (x)$ ; the parameter is the size of $\varphi $ . This parameterization focusses attention on instances where n is large compared to the size of $\varphi $ . We show unconditionally that this problem does not belong to the parameterized analogue of $\mathsf {AC}^0$ . From this we derive that certain natural upper bounds on the complexity of our parameterized problem imply certain separations of classical complexity classes. This connection is obtained via an analysis of a parameterized halting problem. Some of these upper bounds follow assuming that $I\Delta _0$ proves the MRDP theorem in a certain weak sense.

Abstract We study the first-order consequences of Ramsey’s Theorem fork-colourings ofn-tuples, for fixed $n, k \ge 2$ , over the relatively weak second-order arithmetic theory $\mathrm {RCA}^*_0$ . Using the Chong–Mourad coding lemma, we show that in a model of $\mathrm {RCA}^*_0$ that does not satisfy $\Sigma ^0_1$ induction, $\mathrm {RT}^n_k$ is equivalent to its relativization to any proper $\Sigma ^0_1$ -definable cut, so its truth value remains unchanged in all extensions of the model with the same first-order universe. We give a complete axiomatization of the first-order consequences of $\mathrm {RCA}^*_0 + \mathrm {RT}^n_k$ for $n \ge 3$ . We show that they form a non-finitely axiomatizable subtheory of $\mathrm {PA}$ whose $\Pi _3$ fragment coincides with $\mathrm {B} \Sigma _1 + \exp $ and whose $\Pi _{\ell +3}$ fragment for $\ell \ge 1$ lies between $\mathrm {I} \Sigma _\ell \Rightarrow \mathrm {B} \Sigma _{\ell +1}$ and $\mathrm {B} \Sigma _{\ell +1}$ . We also give a complete axiomatization of the first-order consequences of $\mathrm {RCA}^*_0 + \mathrm {RT}^2_k + \neg \mathrm {I} \Sigma _1$ . In general, we show that the first-order consequences of $\mathrm {RCA}^*_0 + \mathrm {RT}^2_k$ form a subtheory of $\mathrm {I} \Sigma _2$ whose $\Pi _3$ fragment coincides with $\mathrm {B} \Sigma _1 + \exp $ and whose $\Pi _4$ fragment is strictly weaker than $\mathrm {B} \Sigma _2$ but not contained in $\mathrm {I} \Sigma _1$ . Additionally, we consider a principle $\Delta ^0_2$ - $\mathrm {RT}^2_2$ which is defined like $\mathrm {RT}^2_2$ but with both the $2$ -colourings and the solutions allowed to be $\Delta ^0_2$ -sets rather than just sets. We show that the behaviour of $\Delta ^0_2$ - $\mathrm {RT}^2_2$ over $\mathrm {RCA}_0 + \mathrm {B}\Sigma ^0_2$ is in many ways analogous to that of $\mathrm {RT}^2_2$ over $\mathrm {RCA}^*_0$ , and that

Karaoke machines have become a popular choice for many people’s daily entertainment. In this paper, we address a novel task of recommending a suitable key for a user to sing a given song to meet his or her vocal competence, by proposing the Personalized Competence-based Rating Prediction (PCRP) model. Specifically, we learn the song embedding vectors from the sequences of songs’ notes, and then design a history encoder with recurrent units to extract users’ vocal information from the history rating records and utilize a rating decoder based on the Transformer. The experimental results on a real world karaoke rating dataset demonstrate the effectiveness of the proposed approach.

Abstract The Jordan decomposition theorem states that every function $f \colon \, [0,1] \to \mathbb {R}$ of bounded variation can be written as the difference of two non-decreasing functions. Combining this fact with a result of Lebesgue, every function of bounded variation is differentiable almost everywhere in the sense of Lebesgue measure. We analyze the strength of these theorems in the setting of reverse mathematics. Over $\mathsf {RCA}_{0}$ , a stronger version of Jordan’s result where all functions are continuous is equivalent to $\mathsf {ACA}_0$ , while the version stated is equivalent to ${\textsf {WKL}}_{0}$ . The result that every function on $[0,1]$ of bounded variation is almost everywhere differentiable is equivalent to ${\textsf {WWKL}}_{0}$ . To state this equivalence in a meaningful way, we develop a theory of Martin–Löf randomness over $\mathsf {RCA}_0$ .

For short distance traveling in crowded urban areas, bike share services is becoming popular owing to the flexibility and convenience. To expand the service coverage, one of the key tasks is to seek new service ports, which requires to well understand the underlying features of the existing service ports. In this paper, we propose a new model, named for Efficient and Semantic Location Embedding (ESLE)1, which carries both geospatial and semantic information of the geo-locations. To generate ESLE, we first train a multi-label model with a deep Convolutional Neural Network (CNN) by feeding the static map-tile images and then extract location embedding vectors from the model. Compared to most recent relevant literature, ESLE is not only much cheaper in computation, but also easier to interpret via a systematic semantic analysis. Finally, we apply ESLE to seek new service ports for NTT DOCOMO’s bike share services operated in Japan. The initial results demonstrate the effectiveness of ESLE, and provide a few insights that might be difficult to discover by using the conventional approaches.

The complexity of the parameterized halting problem for nondeterministic Turing machines p-Halt is known to be related to the question of whether there are logics capturing various complexity classes [10]. Among others, if p-Halt is in para-AC0, the parameterized version of the circuit complexity class AC0, then AC0, or equivalently, (+, x)-invariant FO, has a logic. Although it is widely believed that p-Halt ∉. para-AC0, we show that the problem is hard to settle by establishing a connection to the question in classical complexity of whether NE ⊈ LINH. Here, LINH denotes the linear time hierarchy.

Abstract In this article, we will show that ${\rm{R}}{{\rm{T}}^2} + WK{L_0}$ is a ${\rm{\Pi }}_1^1$ -conservative extension of ${\rm{B\Sigma }}_3^0$ .

In this paper we continue the study, from Frittaion, Steila and Yokoyama (2017, Theory and Applications of Models of Computation 14th Annual Conference, Bern, Switzerland, April 20–22, 2017), on size-change termination (SCT) in the context of Reverse Mathematics. We analyse the soundness of the SCT method. In particular, we prove that the statement ‘any programme which satisfies the combinatorial condition provided by the SCT criterion is terminating’ is equivalent to WO(ω3) over RCA0.

Abstract In this paper, we introduce the systems ns-ACA0and ns-WKL0of non-standard second-order arithmetic in which we can formalize non-standard arguments in ACA0and WKL0, respectively. Then, we give direct transformations from non-standard proofs in ns-ACA0or ns-WKL0into proofs in ACA0or WKL0.