All Questions

Filter by
Sorted by
Tagged with
1 vote
0 answers
66 views

Do game semantics for logic have Curry-Howard-like correspondence with game semantics for programming languages?

Both for logic and PLs do have notion of game semantics. Both are defined by two-player dialogue game, but players are different. In first case it is game between Verifyer and Falsifyer and in second ...
uhbif19's user avatar
  • 295
2 votes
2 answers
277 views

How to prove `(∀(M : Monad). ∀a. a → M a) ≅ 𝟙`

Just like the title says, how to prove that equation? The equation basically says that there is only one function a -> M a parametric in both ...
Russoul's user avatar
  • 209
0 votes
0 answers
78 views

Can lambda-calculus, or other formal systems / calculi, be represented using set theory?

Background: I'm a fresh grad student looking into interesting ideas I have. I do not have any theoretical computer science background beyond basic Theory of Computation stuff from undergrad. If I have ...
The Pointer's user avatar
1 vote
0 answers
36 views

First-order linear mu-calculus?

There is linear $\mu$-calculus (see e.g. [1]) and first-order $\mu$-calculus (see e.g. here). Has anybody studied first-order linear $\mu$-calculus? [1]: Christian Dax, Martin Hofmann, Martin Lange: A ...
Nicola Gigante's user avatar
0 votes
2 answers
147 views

Bottom up TSP solution?

I'm not sure if this is something new or if I'm just not getting previous efforts. TSP can be thought of as a list of weighted links and nodes. If one takes the Nearest Neighbor (NN) of every node and ...
Maub Nesor's user avatar
5 votes
0 answers
125 views

Do fast satisfiability algorithms imply fast algorithms for parity SAT?

$\oplus$SAT is the problem of deciding if the number of satisfying assignments to a CNF formula is odd (and is the standard complete problem for the class $\oplus$P, or Parity-P). Suppose we have a ...
Michael Lampis's user avatar
0 votes
0 answers
29 views

Is Maximum monotone NAE3SAT APX-hard?

I know that monotone NAE3SAT is NP-complete. I also know that MAXNAE3SAT is APX-complete. Note that I am using a monotone formula to mean with with no negated literals anywhere. Anyway, my question is ...
Anand Subramani's user avatar
1 vote
0 answers
51 views

Pfaffian orientation algorithm for planar graphs

I was studying finding a pfaffian orientation of a planar graph in $NC$. In Vazirani's Paper on NC Algorithms for Computing the Number of Perfect Matchings in $K_{3,3}$-Free Graphs and Related ...
Soham Chatterjee's user avatar
0 votes
0 answers
62 views

How to reduce a code down to its configuration

I have built a system where from atomic information of a UI code I could generate a framework specific code. Here is the concept https://github.com/imvetri/ui-editor. For example, the user of this ...
Vetrivel's user avatar
2 votes
1 answer
171 views

Do pseudo-random number generator test batteries have any theoretical grounding?

There are a lot of PRNG test batteries, like DieHarder. They do check that some statistical tests expected for random sequence are indeed present. But is there any theoretical motivation, why this ...
uhbif19's user avatar
  • 295
6 votes
0 answers
83 views

Certifying the promise in hard promise problems

Do we happen to know of any promise problems where the problem is both conditionally hard (say, NP-hard) while simultaneously being able to certify that the instance satisfies the given promise? For ...
Noel Arteche's user avatar
7 votes
0 answers
104 views

Why is showing lower bounds for AM communication complexity difficult?

One of the major open problems in communication complexity is to show interesting lower bounds for the Arthur-Merlin (AM) communication complexity of some natural problems (i.e., lower bounds of the ...
Naysh's user avatar
  • 576
3 votes
0 answers
68 views

FPRAS to estimate the probability to get a cyclic subgraph of a directed graph

Consider a directed graph $G = (V, E)$ whose edges are annotated with independent probabilities of existence. This gives a probability distribution on the subgraphs of $G$; for instance, if each edge ...
a3nm's user avatar
  • 8,896
1 vote
0 answers
91 views

Equivalence between GNFA and NFA/DFA

In Section 1.3 of the 3rd edition of Michael Sipser’s Introduction to the Theory of Computation, it is proven that regular expressions are equivalent to deterministic finite automatas (DFAs). That is, ...
Abced Decba's user avatar
3 votes
2 answers
167 views

Assignment problem for forming pairs of real numbers

Suppose I have two sets of real numbers, $X$ and $Y$, each of cardinality $N$. I would like to assign these points to pairs $(X_i, Y_j)$ such that the sum of squared intra-pair distances is minimized. ...
calmcc's user avatar
  • 161
6 votes
1 answer
228 views

Fast algorithms for time bounded Kolmogorov complexity

For a universal Turing machine $U$, the time bounded Kolmogorov complexity of a string $x$ is silmilar to the usual Kolmogorov complexity but limited to programs $p$ running in time at most $t(|x|)$: $...
agemO's user avatar
  • 187
1 vote
0 answers
47 views

Elimination of monadic second-order quantifiers

I'm trying to understand what is currently known to be possible regarding the elimination of monadic second-order quantifiers. Many sources cite that monadic second-order logic supports elimination of ...
Nicola Gigante's user avatar
0 votes
0 answers
46 views

Amplifying success probability for PTMs with $poly(n) / \exp(n)$ gap?

The following is a well-known result of BPP in complexity theory, e.g., Theorem 1 and its proof from here: Consider a probabilistic Turing Machine (PTM) $M$, and a language $L \in BPP$: If $x \in L$ (...
hedgehog0's user avatar
57 votes
10 answers
18k views

Recent advances in computer science since 2010?

Since I left school (early 2010s) a couple of recently developed techniques were widely adopted by the industry. For example, Asymmetric numeral systems for compression (e.g. Ubuntu ships with ...
user12344567's user avatar
6 votes
0 answers
172 views

Could a quantum computer prove theorems with infeasibly long proofs?

The mathematician Andrew Granville recently published a "philosophical" article, Accepted proofs: Objective truth, or culturally robust?. At the end, he mentions in passing a suggestion by ...
Timothy Chow's user avatar
  • 7,465
1 vote
0 answers
79 views

Tractability of computing generalized hypertreewidth on bounded arity hypergraphs

Generalized hypertreewidth is a generalization of treewidth to hypergraphs. Unlike treewidth, it is not tractable, for a fixed width $k \in \mathbb{N}$, given a hypergraph $H$, to determine if $H$ has ...
a3nm's user avatar
  • 8,896
6 votes
2 answers
273 views

What are the consequences of $BPP \neq P$?

I have seen a lot of people assume, $BPP = P$ . But to me, this seems false intuitively.(Though math is not without unintuitive results) And, to my admittedly limited understanding of the topic, the ...
Colonizor48's user avatar
0 votes
0 answers
46 views

Using Simplex for Difference Logic

I'm interested in what happens when using the Simplex algorithm on Difference logic, inspired by problem 5.4 in Kroening and Strichman's Decision Procedures. Clearly, in this case, all constraints of ...
Jova's user avatar
  • 161
1 vote
0 answers
77 views

What complexity class is characterized by having PSPACE verifiers?

Inspired by the 2 definitions (theorems) I am aware of, that are as follows. A language L belongs to QMA if there exists a BQP verifier V. A language L belongs to NP if there exists a P verifier V. ...
Ilk's user avatar
  • 900
0 votes
0 answers
123 views

Could we build PSPACE-based cryptography - more secure post-quantum?

It seems not safe to exclude possibility of e.g. some next generation quantum computers being able to attack NP problems (e.g. 2WQC) - so maybe it is worth to start thinking of shifting the ...
Jarek Duda's user avatar
3 votes
1 answer
146 views

is SUBEXP contained within PSPACE?, NP?

Let SUBEXP is the complexity class of all problems solvable in sub-exponential time in the length of the input. What are the known properties of this class? Is it known to be contained in PSPACE, if ...
Colonizor48's user avatar
1 vote
0 answers
84 views

Generalization of the Hamiltonian path problem on Grid Graphs

Fix a cost to each of these actions: move up, move down, move left, move right. I.e. fix some function $f: \{\text{move up, move down, move left, move right}\} \to \mathbb N$. Define the following ...
TRP's user avatar
  • 31
0 votes
1 answer
65 views

Is this edge-partitioning NP-Hard?

Let $G = (V,E)$ be an undirected graph with $m = |E|$ edges (assume that $m = 3t$ for some $t \in \mathbb{N}$). Problem: Partition $E$ to $q = \frac{m}{3}$ sets $S_1,S_2,\ldots, S_q \subseteq E$ sets ...
John's user avatar
  • 173
2 votes
0 answers
53 views

Approximately sampling from a discrete unimodal distribution with large support

I have an algorithmic problem and I am curious if a solution is known in the literature, because I cannot find it. I came up with an algorithm of my own, but would be curious if something is known. I ...
user2316602's user avatar
2 votes
1 answer
73 views

Second-order reachability in second-order logic

By second-order reachability I mean a second-order lifting of the reachability problem on first-order structures. So let $R(X,Y)$ be a second-order binary predicate (i.e. it links a set of elements $X$...
Nicola Gigante's user avatar
0 votes
2 answers
66 views

Inexpressibility results for first-order logic that fail extending the language

Think of the classical inexpressivity results that one studies in early courses about first-order logic, e.g. that on a signature with a binary predicate $R$ one cannot express that $R$ is connected. ...
Nicola Gigante's user avatar
3 votes
1 answer
174 views

Permanent of doubly stochastic matrix

Is there a faster ($O(a^n)$ at $a<2$ or quasiP or poly) algorithm for permanent of doubly stochastic matrix compared to an arbitrary $0/1$ permanent? Is there at least a deterministic polynomial ...
Turbo's user avatar
  • 12.8k
2 votes
0 answers
57 views

Complexity measures for semi-decidable problems

Is there any sensible complexity measure that makes sense to compare the "hardness" of undecidable semi-decidable problems? Time and space are of course not suitable, because they cannot be ...
Nicola Gigante's user avatar
3 votes
0 answers
103 views

How does NP-completess of decision problems relate to NP-completeness of search problems?

Background Oded Goldreich differentiates in his textbook (Computational Complexity: A Conceptual Perspective) between the "decision" variant of NP problems and "search" variant of ...
Anton Ehrmanntraut's user avatar
13 votes
1 answer
895 views

Law of the Excluded Middle in complexity theory

A recent blog post by Lance Fortnow discusses non-constructive proofs, where "non-constructive" here means that the law of the excluded middle is used in a substantive way. That is, one ...
Timothy Chow's user avatar
  • 7,465
1 vote
0 answers
39 views

Encoding of continuous functions in PPAD

I'm studying the complexity class PPAD (from the seminal 1994 work by Papadimitriou) which contains complete problems such as computing Nash equilibria or finding the fixed point of a Brouwer map. ...
ntrstd11's user avatar
  • 111
1 vote
1 answer
140 views

A contradiction in the realm of quantum digital and analog computation

It is a well known result that the circuit model of Quantum Computing (QC) is equivalent to the adiabatic model. Furthermore, the former is nothing more than a "slightly" more powerful ...
Marion's user avatar
  • 183
0 votes
0 answers
63 views

What is the meaning of the additive epsilon term in the definition of a time constructible function?

There is a well-known theorem that states that a function $f$ is time constructible if and only if $f$ can be computed in time $O(f)$. But this theorem comes with some conditions: $f$ must be a ...
user70015's user avatar
-1 votes
1 answer
74 views

What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?

I was given an exercise that asked me to assign a simple type to the lambda term: $$ \lambda a.a(\lambda yt.t)(ya) $$ but I couldn't find one, furthermore, the lambda term seems untypable to me ...
Domiziano Scarcelli's user avatar
9 votes
1 answer
328 views

Is P=NP relative to the halting oracle?

Consider the following variant $\mathscr{H}$ of the halting oracle: given the code $e$ for an ordinary Turing machine and an input $n$ to it, we let $\mathscr{H}(\langle e,n\rangle) = \langle 0,0\...
Gro-Tsen's user avatar
  • 609
3 votes
0 answers
162 views

Is $\mathsf{NP}\subseteq\mathsf{NSPACE}(n)$?

It is well-known that $\mathsf{P}\neq\mathsf{SPACE}(n)$, either for $\mathsf{SPACE}=\mathsf{DSPACE}$ or $\mathsf{NSPACE}$, and it is conjectured that both $\mathsf{P}\not\subseteq\mathsf{DSPACE}(n)$ ...
plm's user avatar
  • 131
7 votes
0 answers
164 views

Project management

What book or MOOC would you recommend on work organisation / management of academic research projects? (Does not have to be academic project management specifically, but as close as possible)
Tatiana Starikovskaya's user avatar
7 votes
1 answer
293 views

Is there a well-defined notion of an “R/poly” complexity class?

This would be the complexity class of all problems that are decidable in finite time with a polynomial length advice string that can be arbitrarily hard to compute. But potentially undecidable without ...
Colonizor48's user avatar
6 votes
0 answers
270 views

Techniques for solving huge linear programs

During the solution of some computational problem, we have arrived at a linear program of the following form: \begin{align*} \text{maximize} ~~ c x \\ \text{subject to} ~~ A x \leq b, x \geq 0 \...
Erel Segal-Halevi's user avatar
7 votes
1 answer
278 views

Is is true that every monad transformer is equivalent to its underlying/base monad?

Question originally asked in proofassistants.stackexchange Just like the title says, is it true (in some sensible model)? And if so, how to prove it? Something tells me it should be true and higher-...
Russoul's user avatar
  • 209
4 votes
1 answer
97 views

Power of non-implicationally-complete Frege systems and Boolean equational calculus

We know that Frege systems are required to be implicationally complete -- namely, if a set of formulas $B_1,B_2,\cdots,B_t$ imply formula $C$, then this implication can be proven in the system. I'm ...
Soha's user avatar
  • 145
1 vote
0 answers
38 views

Understanding David Pisinger's balanced algorithm for the subset-sum problem with bounded weights

I'm trying to understand David Pisinger's balanced algorithm for the subset-sum problem with bounded weights, which can be found on page 5 of his paper Linear Time Algorithms for Knapsack Problems ...
Pablo Messina's user avatar
4 votes
1 answer
84 views

Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas

Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. I am intersting in finding the minimal width of some certain ...
Jxb's user avatar
  • 315
0 votes
0 answers
50 views

Product types: algebraic structure for modeling product types with commutative and associative product operation

Is there a known algebraic structure over set of Types (however they are defined) which is equipped with: commutative and associative product operation for building product types from simpler types, ...
Bogdan Nikolic's user avatar
2 votes
0 answers
51 views

Formal semantics of a simple object oriented language without inheritance but with self-referential objects

Would you please point me to some papers or textbooks that describe rigorously a formal semantics/computational model of a simple object-oriented language? The language needs not accommodate ...
Evan Aad's user avatar
  • 354

15 30 50 per page