# All Questions

12,683 questions
Filter by
Sorted by
Tagged with
1 vote
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 ...
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 ...
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
36 views

### First-order linear mu-calculus?

There is linear $\mu$-calculus (see e.g. ) and first-order $\mu$-calculus (see e.g. here). Has anybody studied first-order linear $\mu$-calculus? : Christian Dax, Martin Hofmann, Martin Lange: A ...
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 ...
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 ...
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
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 ...
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 ...
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 ...
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 ...
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 ...
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
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, ...
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. ...
228 views

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)$ ...
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)
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 ...
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 \...
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-...
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
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 ...
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 ...
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, ...