All Questions
12,683
questions
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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, ...
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. ...
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|)$:
$...
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 ...
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$ (...
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 ...
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 ...
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 ...
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 ...
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 ...
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.
...
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 ...
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 ...
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 ...
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 ...
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 ...
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$...
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. ...
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 ...
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 ...
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 ...
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 ...
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. ...
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 ...
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 ...
-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 ...
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\...
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)$ ...
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)
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 ...
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
\...
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-...
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 ...
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 ...
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 ...
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, ...
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 ...