Is quantum annealing faster than simulated annealing/genetic/other state-of-the-art optimization algorithms? There's the idea of quantum annealing being used to solve optimization problems in terms of a QUBO problem for D-Wave's quantum algorithm. I understand that the advantage of quantum annealing as opposed to classical simulated annealing is that quantum annealing allows the particle/search point to tunnel through high barriers with probability as a function of barrier width, instead of having to climb all the way over the barrier (which in some cases wouldn't be possible because there wouldn't be enough energy). This is my understanding from here: http://en.wikipedia.org/wiki/Quantum_annealing

If quantum annealing is better than simulated annealing in this fundamental way, would it not be faster to implement QA instead of SA or GA's for solving optimization problems on a classical computer? If so, why aren't people using it? Or are they, and I'm just unaware (in which case I'd love to see references)?

D-Wave seems to be banking on the practicality of their quantum computer, not so much insane accuracy or other more "scientific" pursuits. If it just so happens that D-Wave's computers aren't really quantum, shouldn't we be able to find a fast classically implemented quantum annealing algorithm to compete with the quantumly implemented version also?

Quantum annealing essentially offers a square-root speed-up over classical simulated annealing in many circumstances. So, yes, it is potentially a faster approach for some optimization problems, but the speed-up isn't enough to make most hard problems tractable.

Unfortunately, you cannot efficiently simulate quantum annealing classically, because any approaches we know of require you to keep track of the state of the system, which requires keeping track of exponentially many parameters (the amplitude of each possible classical state). Thus any attempt to simulate quantum annealing incurs a huge overhead which kills any advantage.


What's the definition of join on iso-recursive types? In languages with subtyping, there is often a "join" operation defined to compute the least upper bound of two types. It's used in type-checking, for example to find the smallest type that covers both the "then" and "else" branches of an if-statement.

What should the definition of join be for iso-recursive types such as $\mu X.\tau$? I started to write it myself, but realized it gets a little tricky if the recursion in each type is unrolled to a different depth.

If there's a standard reference for this, even better. Benjamin Pierce's "Types and Programming Languages" lists the necessary subtype rules near the end of chapter 21, but doesn't define the join rules.

I thought a bit about this and I am afraid that it is harder than it
looks -- as you suspected! In the spirit of encouraging discussion,
I'll write my chain of thoughts.

The subtyping rules are often defined as judgments of the form t1 <:
t2, where --- is an inductive rule (you can only use them finitely
many times along each path in the derivation tree) and === is
a coinductive rule (you can use it infinitely many times).

t1 <: t2
t'1 <: t'2
=================
t1*t'1  <: t2*t'2

t1 :> t2
t'1 <: t'2
======================
t1 -> t'1 <: t2 -> t'2

========
t <: top

========
bot <: t

------
t <: t

t1 <: t2
t2 <: t3
--------
t1 <: t3

t1[a \ mu a. t1] <: t2
----------------------
(mu a. t1) <: t2

t1 <; t2[a \ mu a. t2]
----------------------
t1 <: (mu a. t2)

I would think you can define the /\ and \/ by turning this into
a three-place judgment. Only showing one half:

t1 /\ t2 = t3
t'1 /\ t'2 = t'3
=========================
t1*t'1 /\ t2*t'2 = t3*t'3

t1 \/ t2 = t3
t'1 /\ t'2 = t'3
==================================
t1 -> t'1 /\ t2 -> t'2 = t3 -> t'3

===============
t1 /\ top <: t1

================
top /\ t2 <: tt2

================
t1 /\ bot <: bot

================
bot /\ t1 <: bot

----------
t /\ t = t

t1 /\ t2 = t12
t12 /\ t3 = t23
-----------------------
(t1 /\ t2) /\ t3 = t123

t1 /\ t23 = t123
t2 /\ t3 = t23
-----------------------
t1 /\ (t2 /\ t3) = t123

(The two halves, /\ and \/, can be factorized with a parametrized
presentation where /\^{-1} is \/ and top^{-1} is bot.)

The problem here are the mu-unfolding rules:

t1[a \ mu a. t1] /\ t2 = t3
---------------------------
(mu a. t1) /\ t2 = t3

t1 /\ t2[a \ mu a. t2] = t3
---------------------------
t1 /\ (mu a. t2) = t3

Clearly there should be a rule that allows to build a (mu a. t3) on
the right-hand side; I think the rules above are probably not
complete.

Some presentations of recursive subtyping have rules of the form:

Gamma, a <: b |- t1 <: t2
---------------------------------
Gamma |- (mu a. t1) <: (mu b. t2)

-------------------------------
Gamma ∋ (t1 <: t2) |- t1 <: t2

(Technically these interact with the induction/coinduction
presentation: you may not use an hypothesis in Gamma without using one
of the coinductive/productive rules first.)

I guess that those could be adapted to:

Gamma, a /\ b = c |- t1 /\ t2 = t3
-----------------------------------------------
Gamma |- (mu a. t1) /\ (mu b. t2) = (mu c . t3)

----------------------------------------
Gamma ∋ (t1 /\ t2 = t3) |- t1 <: t2 = t3

I thought that the syntax/coinduction-based presentations of recursive
subtyping ("Coinductive axiomatization of recursive type equality and
subtyping", Brandt and Henglein, 1997; "Subtyping, Declaratively", Danielsson, 2010) would avoid having to think about the tree-form of mu-types,
but it looks like the syntax alone does not scale that nicely to
defining the meet/join, so maybe going back to the tree presentation
would better reveal what should happen.


Induction over a transitive relation in Coq I have the current problem when using induction with Coq:

I have states ST, which are pairs (A,B), where A are Addresses (nat) and B are Memories (A parameter)

Open Scope type_scope.

Definition Address := nat.
Parameter Memory : Set.

Definition State := ( Address *  Memory ).

and a reflexive and transitive relation between states:
    ST ==> ST',
which builds on a relation that performs the 'single step' between states:
    ST --> ST'

Reserved Notation "S '-->' S'" (at level 50, left associativity).
Inductive eval : State -> State -> Prop :=
| eval_step : forall (a a' : nat) (m m' : Memory),
  a' > a ->
  (a, m) --> (a', m')

where "S '-->' S'" := (eval S S') : type_scope.

Reserved Notation "S '==>' S'" (at level 50, left associativity).
Inductive eval_trans : State -> State -> Prop :=
| refl : forall (t : State),
  t ==> t

| trans : forall (t t' ti : State),
  t --> ti ->
  ti ==> t'->
  t ==> t'

where "S '==>' S'" := (eval_trans S S') : type_scope.

When performing induction on an hypothesis of the form
    ST ==> ST',
I should get two cases to prove.

When I introduce the various parts of a state among the hypotheses and then induce over a ST==>ST' hypothesis,
CoQ forgets the biding between a state and its component.
E.g. if ST is A,B and I have A,B among the hypotheses, induction here will forget the binding between ST and A,B.
This is a known problem (https://stackoverflow.com/questions/4519692/keeping-information-when-using-induction), that can be circumvented with a "remember A,B as ST".

However, in the transitive case, the "remember" does some wrong things, as the single step becomes
    ST --> ST'
    ST' ==> ST''
(and an inductive hypothesis of the form, if ST' = A,B , having already ST = A,B, then ST ==> ST')
The single step is performed between the same state, which should not be the case.

If I drop the "remember", the transitive case works fine, as expected,
    ST --> ST'
    ST' ==> ST''
but, alas, the state ST is a generic state and not A,B.

Lemma some_lemma :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==> (a', m') ->
    (a, m) ==> (S a', m').
Proof.
intros a a' m m' H.
induction H.
(*base case*) admit.
(*inductive case*) admit.
(*in both cases I lost that t = (a,m), but the IH is right*)
Admitted.

Lemma some_lemma_v2 :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==> (a', m') ->
    (a, m) ==> (S a', m').
Proof.
intros a a' m m' H.
remember (a,m) as t.
induction H.
(*base case*) admit.
(*inductive case*)
(* I have that t = (a,m) and the IH sais that if ti =(a,m) then have some ==>,
but ti is the state t reaches after 1 step (H)*)
Admitted.

Any help is greatly appreciated.
I have created this example by shortening the case I am working on, I believe all the important details to be present.

thank you, and sorry in case I have missed some answer being out there in the net, but I couldn't find anything useful.

It is not clear to me how induction helps with the lemma you are trying to prove, so I'll take an alternative approach.

Firstly, I prove two helper lemmas that break apart and put back together ==>  with --> at the tail, rather than at the start. Based on these lemmas, I can manipulate the result using your definition of eval to get the desired result. My impression is that the core lemma relies too heavily on the somewhat odd definition of eval, which possibly allowed me to side-step any inductive argument you had in mind.

So, although the lemma you are interested in does not require induction over the transitive relation, the two helper lemmas do.

Note: proofs have not been optimised or beautified.

The first lemma inverts instances of t ==> ti so that the single step reduction occurs at the end, rather than at the beginning. The proof relies on induction and was undemanding.

Lemma end_inversion :
  forall (t ti : State),
    t ==> ti ->
    t = ti \/
      exists t', t ==> t' /\ t' --> ti.
Proof.
  intros.
  induction H.

  left; auto.

  destruct IHeval_trans; right.

  exists t.
  subst.
  split; [apply refl | auto].

  destruct H1 as [x [H1 H2]].
  exists x.
  split; auto.
  apply trans with (ti := ti); auto.
Qed.

The second lemma plugs a single step reduction onto the end of a transitive reduction to again get a transitive reduction. The proof is by straightforward induction.

Lemma end_eval :
  forall (t ti t' : State),
    t ==> t' ->
    t' --> ti ->
    t ==> ti.
Proof.
  intros.
  induction H.
  apply trans with (ti := ti); [auto | apply refl].
  apply trans with (ti := ti0); auto.
Qed.

And now your lemma. The proof relies on end_inversion to break up ==>, does some manipulation of the result, and puts things back together using end_eval. No induction is required.

Lemma some_lemma :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==> (a', m') ->
    (a, m) ==> (S a', m').
Proof.
  intros a a' m m' H.
  apply end_inversion in H.
  destruct H.
  inversion H; subst.
  apply end_eval with (t' := (a', m')).
    apply refl.
    apply eval_step; auto.
  destruct H as [x [H0 H1]].
  apply end_eval with (t := (a, m)) (t' := x); auto.
  inversion H1; subst.
  apply eval_step; auto.
Qed.


What is known about matrix multiplication, and matrix circuits? So I'm wondering, first off, where I can read up to get a feel for state-of-the-art matrix multiplication concepts.  I'll try to be more specific:

I'm wondering if there has been research on circuits that compute a pre-defined matrix function.  For instance, if we have a function such as $(AB)+C+(DEF)(AB)$, where all the variables are matrices with given sizes, how efficient can we make a circuit that computes this function?  I've been toying with an idea in which the entries are all computed modulo $p$.  So I'm wondering, broadly, what I can read up on to be up-to-date.

While I don't know about the complexity of matrix polynomials in general, the state of the art in the complexity of matrix multiplication is nicely summarized in a recent ToC Graduate Survey by Markus Bläser.

Computing entries mod $p$ is basically the same as the question of the complexity of performing the computation over the field $\mathbb{F}_p$, which is fairly well-studied (though perhaps not as well-studied as characteristic zero).

Most matrix multiplication research works in the nonuniform setting anyways, so it should almost all be relevant to the question of circuit size.


Stable comparison sort with $O(1)$ auxiliary memory and $O(n \log n)$ average running time Does there exist a stable comparison sort using $O(1)$ auxiliary memory and achieving $O(n \log n)$ average run time?

Context: There are comparison sorts with any two of those three desirable characteristics (see this list). Is there a reason why the three cannot be achieved simultaneously? [Edit: I added the algorithm from the accepted answer to the list on Wikipedia, obviously it wasn't there when I asked the question.]

There is a sort algorithm with $O(1)$ auxiliary words and achieving $O(n\log n)$ worst-case run time, where $n$ is the length of the input array.
http://www.springerlink.com/content/d7348168624070v7/

I don't think that the question seeks an algorithm with $O(1)$ auxiliary bits, because such algorithm must be tricky.  I mean, if we cannot use even $O(\log n)$ bits, then we cannot use a simple for-loop (for(i=0, i < n, i++) {...} ) in the algorithm without introducing variable i (which require additional $O(\log n)$ bits).


Axioms for Shortest Paths Suppose we have an undirected weighted graph $G = (V, E, w)$ (with non-negative weights). Let us assume that all shortest paths in $G$ are unique. Suppose we have these $\binom{n}{2}$ paths (sequences of unweighted edges), but do not know $G$ itself. Can we produce any $G$ that would have given these paths as the shortest in polynomial time? The weaker version: can we decide in polynomial time if such $G$ exists?

The obvious necessary condition is the following: for every pair of paths their intersection is a path too. Is this condition sufficient?

You can write the problem as an LP, can't you?  For any two vertices u, v, and any path P from u to v, the weight of P is greater than or equal to the weight of the given shortest path between u and v. These are all linear inequalities, and even though there are exponentially many, the separation problem is in P (it's just an all-pairs shortest path problem).  So, you can use the Ellipsoid algorithm to solve it.


Technical issue with PCP theorem proof I am reading the proof from here and I stumbled upon a technical (yet crucial) problem. I know this is rather specific and the context is problematic, but I couldn't figure it out myself.

In pages 51 and 55, after presenting the "standard" verifiers, they turn to modify the verifiers in order to check split assignments.

In the first case (p. 51) they check that $f_1,\dots,f_k$ are $0.01$-close to the polynomial code, and then they use the Algebraization (+Zero-Testers) to construct a family of polynomials (with a Sum-Check property related to the input formula) that each can be evaluated at a point given 3 values of each of $\widetilde{f}_1,\dots,\widetilde{f}_k$ (the codewords of the polynomial code closet to $f_1,\dots,f_k$).

In the second case (p. 55) they check that $f_1,\dots,f_k$ are $0.01$-close to being linear, and then they define a function $f$ to be a special sum of $\widetilde{f}_1,\dots,\widetilde{f}_k$ such that $f$ can be evaluated at a point given values of each of $\widetilde{f}_1,\dots,\widetilde{f}_k$ (the linear functions closet to $f_1,\dots,f_k$).

Then in both cases they perform tests (Sum-Check or Tensor + Hadamard) on the values of a random polynomial in the family / $\widetilde{f}$.

My problem is that the procedure for reconstruction of the required values of each of $\widetilde{f}_i$ can provide incorrect values with some non-negligible constant probability. Moreover, the probability that all the values are reconstructed correctly is very low, only $c^k$ for some constant $c$. And this is true for both cases.

This can be bad as some of the steps of the verifiers require to obtain values of the target function $f$ / a polynomial from the family w.h.p.

So, we need to amplify the success probability by repeatedly using the "reconstruction algebraic procedure" some $O(\log k)$ times for each $\widetilde{f}_i$.

Now, this means that the blow-up in the query complexity of the sub-routine (relatively to the query complexity of the original verifiers) is slightly larger than $k$, i.e. it is $O(k\log k)$ (in contrast to the "guaranteed"-"desired" $O(k)$ blowup in the statement of the theorems).

Is this a problem or am I missing something (which I probably am)?

The query complexity used in this paper is $O(1)$ and $O(poly(logn))$.

For Lemma 3.1 there is a note that the query complexity used is $O(1)$.

If the question is how Lemma 3.1 generalizes to non-constant query complexity, this does present a problem outside of $O(poly(f(n)))$.

This problem is sidestepped by composing a verifier that reduces query complexity to $O(1)$ (Lemma 4.4).


Lower bound for triangle-free graphs I was reading a set of notes where it says

  It can be shown that $\Omega(n^2)$ space is needed for one-pass algorithms to determine if an (unweighted, undirected) graph $G$ with $n$ nodes contains a triangle, even with randomization.

I've seen communication complexity results like that randomized protocols for disjointness require $\Omega(n)$ space, but what's a sketch or reference for the result above?

First, a streaming algorithm running in space $s(n)$ for a problem $C$ implies a communication protocol for $C$ using $s(n)$ bits of communication: Alice, on input $x$, runs the streaming algorithm on $x$ and then hands the configuration of the machine at the end of the stream to Bob ($s(n)$ bits), and then Bob, who has input $y$, runs the streaming algorithm starting from the provided configuration, and returns the result. Therefore, communication lower bounds imply streaming lower bounds.

Second, consider the following problem, called INDEX: Alice gets an $n$-bit string $x$ and Bob gets an integer $i \in [n]$, and they want to determine value of the $i$th bit of $x$, $x_i$. I'll quote the following result, which can be proved using an information statistics argument.

Claim 1: Any randomized (1/3-error, say) protocol for INDEX requires $\Omega(n)$ communication.

Now we can reduce from INDEX to the triangle-free problem. In particular, given and instance $(x, i)$ of INDEX we can build edge sets $E_A$ and $E_B$ over $V = L \cup R \cup \{s\}$ where $L = \{y_1, ..., y_{\sqrt{n}}\}$, $R = \{z_1, ..., z_{\sqrt{n}}\}$, and $s$ some constant node (so $2\sqrt{n} + 1 = O(\sqrt{n})$ nodes) with the property that the resulting graph $G$ is triangle-free iff $x_i = 1$. Additionally, Alice can compute $E_A$ herself and Bob can compute $E_B$ himself. To do this, pick some pairing function $p: [n] \to [\sqrt{n}] \times [\sqrt{n}]$ and say $p_L(k)$ is the first element in the pair corresponding to $p(k)$ and $p_R(k)$ is the second. We'll use this to map bit positions to edges. Then let $E_A = \{(y_{p_L(k)}, z_{p_R(k)})\ |\ x_k = 1\}$. Note that this is a bipartite graph. Now let $E_B = \{(s, y_{p_L(i)}), (s, z_{p_R(i)})\}$. $E_A$ has no triangles, and $E_B$ forms a triangle with $E_A$ only when theres an edge between $y_{p_L(i)}$ and $z_{p_R(i)}$, which only happens when $x_i = 1$.

An $o(n^2)$ communication-protocol for determining if a graph is triangle-free readily contradicts the INDEX lower bound: Alice gets $x$ and Bob gets $i$. Alice and Bob compute $E_A$ and $E_B$ respectively with no communication. They use the triangle-free protocol as a subroutine, using $o(\sqrt{n}^2) = o(n)$ communication.


Complexity of deciding whether a family is a Sperner familiy We are given a family $\mathcal{F}$ of $m$ subsets of {1, ...,n}. Is it possible to find a non-trivial lower bound on the complexity of deciding whether $\mathcal{F}$ is a Sperner family ? The trivial lower bound is $O(n m)$ and I strongly suspect that it is not tight.

Recall that a set $\mathcal{S}$ is a Sperner family
if for $X$ and $Y$ in $\mathcal{S}$; $X \ne Y$ implies that $X \nsubseteq Y$ and $Y \nsubseteq X$.

Can't you solve this by matrix multiplication? Let the sets be $S_1$, $S_2$, $\ldots$, $S_m$. Take matrix $A$ to be the $m \times n$ matrix where $A_{ij}=1$ if $j \in S_i$ and 0 otherwise, and $B$ to be the $m \times n$ matrix where $B_{ij}=1$ if $j \notin S_i$ and 0 otherwise. Now, $AB^T$ has a $0$ entry if and only if there is one set of $\mathcal{F}$ contained in another.

So if you prove a lower bound of $\Omega(n^{2+\epsilon})$ for the case where $m = \theta(n)$, you have proven the same lower bound for matrix multiplication. This is a famous open problem.

I haven't thought much about it, but I don't see any way you could prove that this particular case of matrix multiplication is essentially as hard as the general case; if you really need a lower bound, this would seem to be the only hope you have of proving one without solving the matrix multiplication problem.

On the plus side, this gives algorithms for this problem that are better than the naive algorithm that takes $\theta(m^2n)$.


What's the difference between an invariant and an "inductive" invariant? I would like to understand this with an example. Also, are there other kinds of invariants related to these?

Thanks!

I don't know anything about the topic, so let me try to give a very simple example and let's see what others say.

Program:

Initialise: $x \gets 2$.
Iterate: $x \gets 2x - 1$.

Now "$x > 0$" is an invariant. It certainly holds initially and after each iteration.

However, it is not an inductive invariant: merely knowing that $x > 0$ before an iteration is not sufficient to guarantee that $x > 0$ after the iteration. After all, if $x > 0$ is all that we know, then we might have $x = 0.1$ before an iteration and thus $x < 0$ after the iteration.

On the other hand, something like "$x > 1$" is an invariant and also an inductive invariant. It is easy to check that if $x > 1$ before an iteration, then also $x > 1$ after the iteration.


Tarjan Strongly Connected Components Question Below is Tarjan's SCC algorithm as described in wikipedia.

Input: Graph G = (V, E)

1.  index = 0                                         // DFS node number counter
2.  S = empty                                         // An empty stack of nodes
3.  for all v in V do
4.   if (v.index is undefined)                       // Start a DFS at each node
5.     tarjan(v)                                     // we haven't visited yet

6.  procedure tarjan(v)
7.   v.index = index                                 // Set the depth index for v
8.   v.lowlink = index
9.   index = index + 1
10.  S.push(v)                                       // Push v on the stack
11.  for all (v, v') in E do                         // Consider successors of v
12.    if (v'.index is undefined)                    // Was successor v' visited?
13.        tarjan(v')                                // Recurse
14.        v.lowlink = min(v.lowlink, v'.lowlink)
15.    else if (v' is in S)                          // Was successor v' in stack S?
16.        v.lowlink = min(v.lowlink, v'.index)      // v' is in stack but it isn't in the dfs tree
17.  if (v.lowlink == v.index)                       // Is v the root of an SCC?
18.    print "SCC:"
19.    repeat
20.      v' = S.pop
21.      print v'
22.    until (v' == v)

In line 16, I could not determine why I could or could not replace line 16 with that of line 14. In other words, it seems to me that taking the min(v.lowlink, v'.lowlink) is the proper approach as opposed to min(v.lowlink, v'.index) in the above example. I have seen one other example on the web that mimics the pseudocode above.

I have considered the unusual use of stack S in the algorithm above in which S may contain items from previous "dead" stack frames. These leftover items aren't removed because they are not the roots of their own strongly connected component.

v.lowlink = min(v.lowlink, v'.index) in line 16 is indeed correct. For a full proof you can consult Tarjan's original paper which can also be found here.

  Robert Tarjan: Depth-first search and
  linear graph algorithms. In: SIAM
  Journal on Computing. Vol. 1 (1972),
  No. 2, P. 146-160.

Completely unrelated to the question, there is an amusing 1983 retrospective by Bob Tarjan here on the paper cited above.


If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? This is a naive question, out of my expertise; apologies in advance.

Goldbach's Conjecture and many other unsolved questions in mathematics can be written
as short formulas in predicate calculus.
For example, Cook's paper "Can Computers Routinely Discover Mathematical Proofs?" formulates
that conjecture as

$$\forall n [( n > 2 \wedge 2 | n) \supset \exists r \exists s (P(r) \wedge P(s) \wedge n = r + s) ]$$

If we restrict attention to polynomially-long proofs, then theorems with such proofs are in NP.
So if P=NP, we could determine whether e.g. Goldbach's Conjecture is true in polynomial time.

My question is: Would we also be able to exhibit a proof in polynomial time?

Edit. As per the comments of Peter Shor and Kaveh,
I should have qualified my claim that we could
determine if Goldbach's conjecture is true if it indeed is one of the theorems with a short proof.  Which of course we do not know!

Indeed!

If P=NP, not only we can decide whether there exists a proof of length n for Goldbach's Conjecture (or any other mathematical statement), but we can also find it efficiently!

Why? Because we can ask: is there a proof conditioned on the first bit being ..., then, is there a proof conditioned on the first two bits being ...., and so on...

And how would you know n? You'll just try all possibilities, in increasing order. When we make a step in the i'th possibility we also try a step in each of the possibilities 1..(i-1).


What is $\mathsf{NP}$ restricted to linear size witnesses? This is related to the question Is the Witness Size of Membership for Every NP Language Already Known?

Some natural $\mathsf{NP}$(-complete) problems have linear length witnesses: a satisfying assignment for $SAT$, a sequence of vertices for $HAMPATH$, etc.

Consider the complexity class "$\mathsf{NP}$ restricted to linear length witnesses". Formal definition of this complexity class, call it $\mathcal{C}$: $L\in\mathcal{C}$ if $\exists L'\in\mathsf{P}\colon (x\in L \iff \exists w\in\{0, 1\}^{O(|x|)}\colon (x, w)\in L')$.

Is this a known complexity class? What are its properties?

The class ${\cal C}$ you are proposing is probably not $NP$. (If ${\cal C} = NP$, then every $NP$ language would have linear-size witnesses, which would imply that every $NP \subseteq TIME[2^{O(n)}]$ and $NP \neq EXP$, among other things).

It is very natural to consider such classes; they arise in several settings. In this paper, Rahul Santhanam (implicitly) proposed the notation $TIGU(t(n),g(n))$ for time-$t(n)$ computation with $g(n)$-guess bits. Hence ${\cal C} = \bigcup_{k} TIGU(n^k,kn)$. In this paper, I defined an analogous class $NTIBI[t(n),b(n)]$. (NTIBI stands for "nondeterministic time and bits".) Also, Cai and Chen would call your class $GC(O(n), P)$ (GC stands for "Guess and Check", cf. L. Cai and J. Chen. On the amount of nondeterminism and the power of verifying. SIAM Journal on Computing, 1996). Finally, if you search for "bounded nondeterminism" you may find three more notations for the same class...


Characterization of problems for which sublinear time algorithms exist I was wondering if problems for which sublinear time (in the input size) algorithms exist can be characterized as possessing specific properties. This includes sublinear time (e.g. property testing, an alternative notion of approximation for decision problems), sublinear space (e.g. sketching/streaming algorithms in which the Turing machine has a read-only tape, a sublinear working space, and a write-only output tape) and sublinear measurements (e.g. sparse recovery/compressive sensing). In particular, I am interested to such a characterization for both the framework of property testing algorithms and in the classical model of randomized and approximation algorithms.

For instance, the problems for which a dynamic programming solution exist exhibit optimal substructure and overlapping subproblems; those for which a greedy solution exists exhibit optimal substructure and the structure of a matroid. And so on.
Any reference dealing with this topic is welcome.

With the exception of a few problems that admit a deterministic sub linear algorithm, almost all of the sublinear algorithms I have seen are randomized. Is there any specific complexity class related to problems admitting sublinear time algorithms ? If yes, is this class included in BPP or PCP?

For the constant-time task of testing graph properties, an interesting characterization is known. A graph property is a function from all graphs to $\{0,1\}$, and a graph property $P$ is testable if there is a randomized algorithm $A$ such that for all $\varepsilon > 0$ and all graphs $G$:

$A(G)$ reads only $g(\varepsilon)$ edges of $G$ for some function $g$
If $P(G)=1$ then $A(G)$ outputs ``yes'' with high probability (say, at least $2/3$)
If at least $\varepsilon n^2$ edges of $G$ have to be added or removed in order to get a $G'$ such that $P(G')=1$ (that is, $G$ is $\varepsilon$-far from the property) then $A(G)$ outputs ``no'' with probability at least $2/3$

That is, $A$ can distinguish between graphs which have $P$ and graphs which have high edit distance from graphs having $P$. Alon, Fischer, Newman, and Shapira proved that a property $P$ is testable in this way if and only if the property can be "reduced" to the property of checking whether a graph has an $\varepsilon$-regular partition (in the sense of Szemeredi). This shows that testing regularity is "complete" for testing, in some sense. (There is also a one-sided error version of testability, see the reference.)


Property Testing for Independent Sets Suppose we're given a graph $G$ and parameters $k,\epsilon$. Are there ranges of values for $k$ (or is it doable for all $k$) for which it is possible to test whether $G$ is $\epsilon$-far from having an independent set of size at least $k$ in time $O(n + \text{poly}(1/\epsilon))$ ?

If we use the usual notion of $\epsilon$-far (i.e at most $\epsilon n^2$ edges would need to be changed in order to obtain such a set), then the problem is trivial for $k = O(n\sqrt{\epsilon})$.  So

It seems that if $k$ is larger, some sampling ideas should work to solve the problem. Is that true ?
Are there other notions of $\epsilon$-far (i.e maybe $\epsilon |E|$ edges instead) under which there are nontrivial results ?

I'm basically looking for references at this point.

This problem has indeed been studied.  Goldreich, Goldwasser and Ron studied it in their seminal paper which kicked off graph property testing, and then, Feige, Langberg, and Schechtman also have results on it in their FOCS '02 paper "Graphs with tiny vector chromatic numbers and huge chromatic numbers".

Specifically, [FLS '02] show that one can distinguish between graphs with an independent set of size $\rho n$ from graphs $\epsilon$-far from being so (meaning, at least $\epsilon n^2$ edges need to be removed to create such an independent set) by choosing a random subgraph induced by $s = \tilde{O}(\rho^4/\epsilon^3)$ random vertices in the graph and checking whether the random subgraph has an independent set of size $\rho s$ or not.   ([GGR '98] showed a weaker bound on $s$ of $\tilde{O}(\rho/\epsilon^4)$.)  [FLS '02] also show a lower bound on $s$ of $\Omega(\rho^3/\epsilon^2)$.


Can one do quantum computing without negative amplitudes? The typical representation I see of $k$ qubits is a $2^k$ complex numbers $c_i$ for every possible combination of values of those bits, such that the sum of all the squared magnitudes of those numbers is 1. i.e.

$$\sum_i \vert c_i \vert^2 = \sum_i (a_i + i b_i)(a - ib_i) = \sum_i a_i^2 + b_i^2 = 1$$

(so with two bits, we have $\vert c_0 \vert^2 = P(00)$, $\vert c_1 \vert^2 = P(01)$,  $\vert c_2 \vert^2 = P(10)$, and $\vert c_3 \vert^2 = P(11)$)

Then gates are simply defined by complex matrices of size $2^k \times 2^k$ that preserve this requirement (formally the set of such matrices is the unitary matrices). To apply a gate we simply multiply these matrices by our current "vector of complex probabilites" and a new set of $c_i$'s. I.e., if $c \in \mathbb{C}^{2^k}$ and our unitary gate H is in $\mathbb{C}^{2^k \times 2^k}$  then we get our result $c^\prime \in \mathbb{C}^{2^k}$ via

$$c^\prime = H c $$

However, is using complex numbers necessary? What I mean is, we could instead define real $p_i = \vert c_i \vert$, and then to apply a gate we do

$$p^\prime = \vert H \sqrt{p} \vert^2 $$

(here by $\sqrt{p}$ and $|..|^2$ I mean I apply those operations to each element of the vector, and keep the vector the same size)

This answer seems to suggest we might be able to do this, and clearly this does preserve everything for one application of an operator if we pick $c_i = \sqrt{p_i} + 0i$, for example, but I don't know about a sequence of multiple gates that each output and work with rotated complex numbers with the same magnitude.

Personally I feel having a set of $0 \leq p_i \leq 1$ s.t. $\sum_i p_i = 1$ seems much more intuitive to me, so my question is simply: is a computer using these rules less powerful than a quantum computer? Or is it a separate complexity class?

As far as I can tell the main difference is gates with imaginary numbers: in this $p$ setting they result in an operation on the inputs in terms of real numbers but it may not be linear, and the order of applying the gates may now matter (try out the $\sqrt{NOT}$ gate for example), but I don't know if that actually matters in terms of what it can compute efficiently.

Edit: for example, the Hadamard gate

$$ H = \frac{1}{\sqrt{2}} \begin{bmatrix} 1 & 1 \\ 1 & -1 \end{bmatrix}$$

applied to $\begin{bmatrix} p_0 \\ p_1 \end{bmatrix}$ ($p_0$ is probability of $<0|$, $p_1$ is probability of $<1|$) would be

$$ p^\prime = \vert \frac{1}{\sqrt{2}} \begin{bmatrix} 1 & 1 \\ 1 & -1 \end{bmatrix} \begin{bmatrix} \sqrt{p_0} \\ \sqrt{p_1} \end{bmatrix} \vert^2 = \vert \begin{bmatrix} \frac{\sqrt{p_0} + \sqrt{p_1}}{\sqrt{2}} \\ \frac{\sqrt{p_0} -\sqrt{p_1}}{\sqrt{2}} \end{bmatrix} \vert^2 = \begin{bmatrix} \vert \frac{\sqrt{p_0} + \sqrt{p_1}}{\sqrt{2}}\vert^2 \\ \vert \frac{\sqrt{p_0} -\sqrt{p_1}}{\sqrt{2}}\vert ^2 \end{bmatrix} =
\begin{bmatrix} \frac{p_0 + p_1}{2} + \sqrt{p_0}*\sqrt{p_1} \\ \frac{p_0 + p_1}{2} - \sqrt{p_0}*\sqrt{p_1}\end{bmatrix} $$

This would be better suited as a comment but since I lack the reputation to comment (!), I am going to write it as an answer. Sorry for the inconvenience.

Yes, you can do quantum computing without complex numbers. As mentioned by @DmitriUrbanowicz it known that Toffoli and Hadamard are universal for quantum computing. (See this simple proof due Dorit Aharonov.)

First, I would like to point out something we all learnt in kindergarten: In quantum computing, the amplitudes can be negative (this happens if you are using Toffoli and Hadamard as your gate set) and even complex (if you are using, say, Toffoli, Hadamard, and Phase) but the probabilities are still non-negative.

Now, as pointed by @JoshuaGrochow above, if your amplitudes themselves are positive real numbers then your gates become classical---you collapse to BPP.

Finally, if you just restrict to your probabilities being positive real numbers and adding up to $1$, then you can potentially solve any problem. This is because you are not putting any restriction on the evolution.


Co-NP-completeness of minimal TSP tour? This problem came out of my recent blog post, suppose you are given a TSP tour, is it co-NP-complete to determine if it is a minimal one?

More precisely is the following problem NP-complete:

Instance: Given a complete graph G with edges weighted with positive integers and a simple cycle C that visits all the nodes of G.

Question: Is there a simple cycle D that visits all the nodes of G such that the total weight of all the edges of D in G is strictly less than the total weight of all the edges of C in G?

A sketch of a possible reduction to prove that it is NP-complete.

Informally it starts from a modified 3SAT formula used to show that 3SAT is ASP-complete (Another Solution Problem), and "follows" the standard chain of reductions 3SAT=>DIRECTED HAMCYCLE => UNDIRECTED HAMCYCLE => TSP

Start with a 3SAT formula $\varphi$ with $n$ variables $x_1,...x_n$ and $m$ caluses $C_1,...,C_m$;
Trasform it to a new formula $\varphi'$ adding a new variable $t$ ...;
... and expanding each clause $(x_{i_1} \lor x_{i_2} \lor x_{i_3})$ to $(x_{i_1} \lor x_{i_2} \lor x_{i_3} \lor t)$;
From $\varphi'$ build the diamonds structure graph $G = \{V,E\}$ used to prove that DIRECTED HAMILTONIAN CYCLE is NP-Complete; suppose that each clause $C_j$ correspond to node $N_j$ in $G$;
Modify $G$ into graph $G' = \{V',E'\}$ replacing each node $u$ with three linked nodes $u_1, u_2, u_3$  and modify the edges according to the standard reduction used to prove the NP-completeness of UNDIRECTED HAMILTONIAN CYCLE from DIRECTED HAMILTONIAN CYCLE i.e. $u_1$ is the node used for incoming edges, $u_3$ is the node used for outgoing edges;
Convert the UNDIRECTED HAMILTONIAN CYCLE instance on $G'$ to a TSP instance $T$ in which all edges of $G'$ has weight $w = 1$, except the (unique) edge in the diamond going to the "positive" assignment of $t$ which has weight $w = 2$ (red edge in the figure below); finally the edges added to make $G'$ complete have weight $w = 3$.

Clearly the TSP instance $T$ has a simple cycle that visits all nodes which corresponds to the satisfying assignment of  $\varphi'$ in which $t = true$ (and this tour can be easily constructed in polynomial time), but it has total weight $|V'|+1$ (because it uses the edge that correspond to the assignment $t = true$ that has weight 2). $T$ has another simple cycle that visits all nodes with a lower total weight $|V'|$ if and only if the edge of weight $2$ that corresponds to the assignment $t = true$ is not used; or equivalently if and only if there is another satisfying assignment of $\varphi'$ in which
$t = false$ ; but this can be true if and only if the original formula $\varphi$ is satisfiable.

I'll think more about it, and I'll write a formal proof (if it doesn't turn out to be wrong :-).
Let me know if you need further details about one or more of the above passages.

As noted by domotorp an interesting consequence is that the following problem is NP-complete: Given a graph $G$ and an Hamiltonian path in it, does $G$ have an Hamiltonian cycle?


What are theoretical computer science jobs? Beside academia which is clearly the home of theorists, I am wondering about industrial jobs related to theoretical computer science, the ones which demand pure mathematical background.

Cheers !

I have a CS Theory background and work in industry doing research at a consulting firm. We get hired by people who want to use various types of computer models and don't have the expertise to create them themselves. This is (partially) a research job because our clients typically have interests usually unaddressed in the academic literature, and so our contracts usually result in us creating new models and techniques that work in their context. I'm currently working on a poster presentation for an academic conference, though one in political science methodology rather than CS.

My group specializes in machine learning and social network analysis, also known as applied linear algebra and graph theory. Our clients tend to be interested in applying this to topics like international relations, logistics, international trade, and cyber security. My coworkers have backgrounds such as a PhD in applied math, a PhD in computational social science, and a masters in computational linguistics. I'm the theoretician in my group and was specifically hired for my pure mathematics knowledge. I primarily work on model design and validation, especially on leveraging graph theoretic structures in the phenomena being modeled to inform model design. I am also the point person for investigating new research and evaluating how it fits into what we are currently working.

I would strongly second Peter Shor's list of recommended skills. The key to being a successful theoretician in industry is to be able to be the bridge between engineers, data analysts, and developers on the one hand and academics on the other.


Accuracy rate in neural networks I've implemented a neural network (using the back-propagation algorithm) in a digital marketing application, where the algorithm classifies words according to quality, price and another characteristics in an AdWord Campaign.  I would like to know if there is a paper or book (preferably free) that discusses the accuracy rate of acceptance that a neural network should have.

What do you mean by "should have"?

In principle you could train a neural network (a multi-layer perceptron, I assume) to perfectly classify the training set (provided that it doesn't contain conflicting examples), however doing so might require a long time (exponential in the size of the training set) and more importantly will usually impair the neural network ability to generalise to unseen data points.

In practice you usually divide your training examples in a training set proper and a validation set: train on the training set and after each epoch you measure accuracy on the validation set, repeat until the accuracy on the validation doesn't increase for a small number of epochs and keep the network with the best accuracy on the validation set. You might also reiterate the whole training process a few times starting from random weights each time, in order to avoid being trapped in local optima.
Moreover, you can experiment varying parameters such as the number of hidden layers, the number of nodes in each hidden layer, and the learning rate, changing the data encoding, and carefully selecting the input features.

Eventually your neural network will reach a maximum accuracy which depends on the problem difficulty.


Are patents good sources for academic research? I'm a freshman Master's student in Computer Science and I need to write a paper for my Operating System class. While looking through research articles using google scholar I found that a lot results lead me to patents. I was wondering if patents are good sources for writing an academic paper or if I should steer clear from them?

My goal is to be able to summarize various papers from a specific topic related to operating systems. Also if possible (but not mandatory) to provide some kind of solution. Any advice would be greatly appreciated since this would be my first time writing a technical paper.

Are patents good sources for academic research?

In general, a clear NO. Typically, patents are intentionally written in a diffuse language to cover as much ground as possible (without incuring the danger of claiming something already known for oneself).  They are not written in a way that they can be used by an engineer or understood by a scholar. They are written such that the courts later can decide in favor of the patent holder or their representative.


How the hardness of hidden subgroup problem in $S_n$ changes as the order of the subgroup grows? In Normal Subgroup Reconstruction and Quantum Computation Using Group Representations by Hallgren et al. In this paper it is showed that no hidden subgroup algorithm can distinguish the trivial subgroup from an order-$2$ subgroup consisting of $\frac{n}{2}$ disjoint transpositions when the group is a symmetric group $S_n$.

My question:

How the hardness of the hidden subgroup problem changes when the order of the subgroup grows beyond $2$?
Is induction the ideal way to derive it?

My effort:

I am confused how to approach this problem. Should we find the element in the hidden subgroup with with largest absolute value of its character? If we can determine the value, would it be useful?

At worst you have to check one element of each repeated prime cycle, https://oeis.org/A186202 Smaller than n! but still large.


Natural problem arising from diagonalization? Diagonalization is a frequently used technique in complexity theory. However, the problems (sets) that are created by diagonalization rarely correspond to anything natural. It would be interesting to collect examples, when a problem was originally defined via diagonalization, but later it was found to coincide with a natural problem.

In some sense the halting problem satisfies this request (I was almost ready to say "There are no such examples!" when I thought of this one.) By doing diagonalization against computable sets, you can of course get sets of very high complexity, but the seemingly-most-natural way of diagonalizing against computable sets gives you a problem that is equivalent to the halting problem. As we now know, the halting problem is equivalent to many other computational problems, such as deciding many properties of TMs, telling whether a Diophantine equation has solutions, the word problem in finitely presented groups, telling whether a high-dimensional knot is the unknot, etc.

I am still ready to say that I would be surprised to see other examples (that aren't just, say, relativized versions of this).


Quickly finding empty-string producing nonterminals in a CFG For a given context free language G, we call a nonterminal $A_i$ nullable if $A_i \rightarrow^* \epsilon$, ie we can derive the empty string from $A_i$ after applying a finite number of productions.

There is a simple algorithm for determining which nonterminals of a grammar are nullable as can be found here:

We start by considering all nonterminals as not nullable. We mark all $A_i$ as nullable if there is a production $A_i \rightarrow \epsilon$. We then loop over all other productions $A_i \rightarrow B_1 B_2 \dots B_k$ excluding productions with a terminal in them, and mark $A_i$ as nullable if all $B_i$ are nullable. We keep doing this loop until we finish a loop without marking any nonterminals as nullable.

My problem with this algorithm is that it has a $O(n^2)$ running time: a worst case is for instance $A_1 \rightarrow A_2$, $A_2 \rightarrow A_3$, $A_3 \rightarrow A_4$, ..., $A_{n-1} \rightarrow A_n$, $A_n \rightarrow \epsilon$.

  Is there an algorithm for this problem
  with a better running time than
  $O(n^2)$?

Can't one implement that algorithm in linear time as follows? (Warning I haven't proof-read this too carefully, so bugs are likely.)

In what follows whenever I say "production" I mean to include only those that include no terminals.
Build a list, for each non-terminal, of the productions it appears in. For every production $i$ let $c_i$ count how many distinct non-terminals in the right hand side are currently marked non-nullable. Let $Q$ denote a queue of non-terminals that have been marked nullable but not yet processed. Initialize all $c_i$ to the number of distinct non-terminals in the right hand side of production $i$. Initialize all non-terminals to not nullable. For every non-terminal $Z$ generated by production $i$ with $c_i=0$ add $Z$ to $Q$ and mark $Z$ as nullable.

While $Q$ is non-empty, remove an arbitrary non-terminal $X$ from $Q$ and process it as follows. For every production $j$ that $X$ is in, decrement $c_j$. If a $c_j$ becomes zero, check to see if the corresponding non-terminal $Y$ has been marked nullable already. If not, mark $Y$ nullable and add $Y$ to $Q$.


Paxos made simple, invariant P2c I am reading
Leslie Lamport's Paxos Made Simple paper.

Can someone explain why $P2^c$ implies $P2^b$?

  $P2^b$ If a proposal with value $v$ is chosen,
  then every higher-numbered proposal issued by any proposer has value $v$.

  $P2^c$ For any $v$ and $n$,
  if a proposal with value $v$ and number $n$ is issued,
  then there is a set $S$
  consisting of a majority of acceptors such that either

  no acceptor in $S$ has accepted any proposal numbered less than $n$, or
  $v$ is the value of the highest-numbered proposal among
  all proposals numbered less than $n$ accepted by the acceptors in $S$.

We prove it ($P2^c \implies P2^b$) by strong induction (wiki). This proof has actually been given in the "Paxos Made Simple" paper (see the arguments between $P2^b$ and $P2^c$). I re-organize it in the order of "what we know, what we want to prove, and how to prove". Hope it helps.

What we know:

Base case: Some proposal with number $m$ and value $v$ is chosen.

Inductive assumption: Every proposal issued with a number in $m \ldots (n-1)$ has value $v$.

The chosen rule of a proposal: For the proposal number $m$ to be chosen, there must be some set $C$ consisting of a majority of acceptors such that every acceptor in $C$ accepted it.

The issue rule of a proposal: It is the existence of a set $S$ such that $P2^c (1)$ + $P2^c (2)$.

What we want to prove is:

Goal: Any proposal issued with number $n > m$ also have value $v$.

Proof:

Combining "base case" and "chosen-rule" with "inductive assumption", we obtain:
The $C$-condition: Every acceptor in $C$ has accepted a proposal with number in $m \ldots (n-1)$ (Note: because at least each of them has accepted a proposal with number $m$),
and every proposal with number in $m \ldots (n-1)$ accepted by any acceptor has value $v$ (Note: due to the inductive assumption and the fact that a proposal must be issued by a proposer before it can be accepted by an acceptor).

Now consider the set $S$ in $P2^c$ which consists of a majority of acceptors. Because $S \cap C \neq \emptyset$, $P2^c(1)$ cannot happen. Then $P2^c(2)$ must be true. $P2^c(2)$ is actually the "value-issued rule": the value $v'$ of the proposal with number $n$ is the value of the highest-numbered proposal among all proposals numbered less than $n$ accepted by the acceptors in $S$, therefore $v' = v$ because of the $C$-condition.

Related posts:

The proof of P2b in Paxos made simple@cstheory
Correctness proofs of classic Paxos and Fast Paxos@cstheory.


Is there a language with strong typed interfaces where types resolution are "delayed"? I know that this question it not entirely theoretical, but I think that's the place where is more probable that someone knows the answer.

The question is: is there any OO strong typed language where I could "delay" the definition of the method's arguments types?

I'll write an example. Imagine I want to model abelian additive groups, and I program the following interface:

interface AbelianAdditiveGroup
{
    public method add(b final_class) : final_class;
    public method additiveInverse() : final_class;
}

Where final_class is a keyword to tell the compiler to use the implementation class, not the AbelianAdditiveGroup or any other intermediate abstract class.

That's an example of what I'm searching. I think that using fixed interfaces or classes as argument types in these methods is a bad approach in a lot of cases because this causes that we have to do multiple runtime type checks in our code.

If there is no language with this feature... is there any good reason for this?

Thanks in advance :) .

What you are looking for are called "self types", and have been studied theoretically for ~20 years or so.

For example, see Safe Type Checking in a Statically-Typed Object-Oriented Programming Language by Kim B. Bruce, in the 1993 POPL (Principles of Programming Languages), pp. 285-298. Off the top of my head, John Mitchell and Kathleen Fisher have also worked on this, and they may also be described in Abadi and Cardelli's book A Theory of Objects.

Scala supports them, but I don't know if other mainstream OO languages do.


Linear time in-place riffle shuffle algorithm Is there a linear time in-place riffle shuffle algorithm? This is the algorithm that some especially dextrous hands are capable of performing: evenly dividing an even-sized input array, and then interleaving the elements of the two halves.

Mathworld has a brief page on riffle shuffle. In particular, I'm interested in the out-shuffle variety which transforms the input array 1 2 3 4 5 6 into 1 4 2 5 3 6. Note that in their definition, the input length is $2n$.

It's straightforward to perform this in linear time if we've got a second array of size $n$ or more handy. First copy the last $n$ elements to the array. Then, assuming 0-based indexing, copy the first $n$ elements from indices $[0,1,2,...,n-1]$ to $[0, 2, 4,...,2n-2]$. Then copy the $n$ elements from the second array back to the input array, mapping indices $[0,1,2,...,n-1]$ to $[1,3,5,...,2n-1]$. (We can do slightly less work than that, because the first and last elements in the input do not move.)

One way of attempting to do this in-place involves the decomposition of the permutation into disjoint cycles, and then rearranging the elements according to each cycle. Again, assuming 0-based indexing, the permutation involved in the 6 element case is
$$
\sigma=\begin{pmatrix} 0 & 1 & 2 & 3 & 4 & 5 \\
0 & 2 & 4 & 1 & 3 & 5\end{pmatrix}=\begin{pmatrix}0 \end{pmatrix} \begin{pmatrix}5 \end{pmatrix} \begin{pmatrix}1 & 2 & 4 &3 \end{pmatrix}.
$$

As expected, the first and last elements are fixed points, and if we permute the middle 4 elements we get the expected outcome.

Unfortunately, my understanding of the mathematics of permutations (and their $\LaTeX$) is mostly based on wikipedia, and I don't know if this can be done in linear time. Maybe the permutations involved in this shuffling can be quickly decomposed? Also, we don't even need the complete decomposition. Just determining a single element of each of the disjoint cycles would suffice, since we can reconstruct the cycle from one of its elements. Maybe a completely different approach is required.

Good resources on the related mathematics are just as valuable as an algorithm. Thanks!

The problem is surprisingly non-trivial. Here is a nice solution by Ellis and Markov, In-Situ, Stable Merging by way of the Perfect Shuffle (section 7). Ellis, Krahn and Fan, Computing the Cycles in the Perfect Shuffle Permutation succeed in selecting "cycle leaders", at the expense of more memory. Also related is the nice paper by Fich, Munro and Poblete, Permuting In Place, which gives a general $O(n\log n)$ time algorithm for the oracle model. If only an oracle for the permutation is available, the algorithm requires logarithmic space; if we also have an oracle for the inverse, it requires constant space.

Now for Ellis and Markov's solution. First, suppose $n = x+y$. Then computing the perfect shuffle of order $n$ reduces to computing the perfect shuffle of orders $x$ and $y$, with a rotation preceding them. Here is a proof by example ($n=5$, $x=3$, $y=2$):
$$
\begin{array}{cc}
012\mathbf{345} & \mathbf{67}89 \\
012\mathbf{567} & \mathbf{34}89 \\
051627 & 3849
\end{array}
$$

Ellis and Markov found an easy way to compute the perfect shuffle when $n=2^k$, using constant space and linear time. Using this, we obtain an algorithm for computing the perfect shuffle for arbitrary $n$. First, write $n = 2^{k_0} + \cdots + 2^{k_w}$ using the binary encoding of $n$, and let $n_i = 2^{k_i} + \cdots + 2^{k_w}$. Rotate the middle $n_0$ bits, shuffle the right-hand $2^{k_0}$ bits. Ignoring the righthand $2^{k_0}$ bits, rotate the middle $n_1$ bits, and shuffle the right-hand $2^{k_1}$ bits. And so on. Note that rotation is easy since the first few elements rotated function as cycle leaders. The total complexity of rotation is $O(n_0 + \cdots + n_w) = O(n)$, since $n_{t+1} < n_t/2$. The total complexity of the inner shuffles is $O(2^{k_0} + \cdots + 2^{k_w}) = O(n)$.

It remains to show how to compute the perfect shuffle when $n=2^k$. In fact, we will be able to identify cycle leaders, following classical work on necklaces (Fredricksen and Maiorana, Necklaces of beads in $k$ colors and $k$-ary de Bruijn sequences; Fredricksen and Kessler, An algorithm for generating necklaces of beads in two colors).

What is the connection? I claim that the shuffle permutation corresponds to right shifting of the binary representation. Here is a proof by example, for $n=8$:
$$
\begin{array}{cccccccc}
000 & 001 & 010 & 011 & 100 & 101 & 110 & 111 \\
000 & 100 & 001 & 101 & 010 & 110 & 011 & 111
\end{array}
$$
Therefore, to find cycle leaders, we need to find one representative out of each equivalence class of the rotation of binary strings of length $k$. The papers mentioned above give the following algorithm for generating all cycle leaders. Start with $0^k$. At each step, we are at some point $a_1 \ldots a_k$. Find the maximal index $i$ of a zero bit, divide $k$ by $i$ to obtain $k = d\cdot i + r$, and let the following point be $(a_1\ldots a_{i-1}1)^d a_1\ldots a_r$. Whenever $r = 0$, the new string is a cycle leader.

For example, when $n=16$ this generates the sequence
$$
\mathbf{0000}, \mathbf{0001}, 0010, \mathbf{0011},
\mathbf{0101}, 0110, \mathbf{0111}, \mathbf{1111}.
$$

The cycle leaders are highlighted.


Are there intermediate eta theories for the lambda calculus? There are two main, studied theories of the lambda calculus, the beta theory and its Post-complete extension, the beta-eta theory.

Do these two theories have an in-between, a kind of intermediate eta rule that gives a confluent rewrite theory?  Is there some interesting notion of partial extensionality that it corresponds to?

This is the second question I have asked in pursuit of intermediate eta, the previous being Extensions of beta-theory of lambda calculus, which led to question about an orthogonal notion of extension, Characterising invisible equivalences by confluent rewrite rules, which sought to clarify an answer to that earlier question.

For typed calculi, if you consider the negative types ($1$, $\times$, $\to$), you can turn the eta rules on or off basically at will without affecting confluence.

For positive types (sums, and pairs with the pattern-matching elimination), the situation is much messier. Basically, the question is whether the term has a closed-scope elimination form, which let contexts interact in complicated ways with eta-expansions. For example, if $e$ has type $A \times B$, then its eta-expansion is $\mathsf{let}\;(a,b) = e \;\mathsf{in}\; (a,b)$. But to get the equational theory a category theorist would expect, you need to consider contexts $\mathbb{C}[-]$, and generalize the equation to be $\mathbb{C}[e] \equiv \mathsf{let}\;(a,b) = e\;\mathsf{in}\;\mathbb{C}[(a,b)]$ (with the expected scoping restrictions).

I think that you can still prove a confluence result if you don't allow the commuting conversions. But this is hearsay -- I've never tried it myself, nor looked at papers documenting it.

I don't really know anything about untyped lambda calculus, though.

EDIT: Charles asks about eta-reductions. This is promising for the kind of example he seeks, because I think in general they won't be strong enough to model the full equality theory, which I'll illustrate with a simple example involving booleans. The eta-expansion for booleans is $\mathbb{C}[e] \mapsto \mathsf{if}(e, \mathbb{C}[\mathsf{true}], \mathbb{C}[\mathsf{false}])$. (The eta-reduction is of course the other direction.)

Now, consider the term $\mathsf{if}(e, f, g)\;\mathsf{if}(e, x, y)$. Showing that this term is equivalent to $\mathsf{if}(e, f\;x, g\;y)$ needs to go through an eta-expansion, because we have to replace the $e$ in one of the if-then-elses with $\mathsf{true}$ and $\mathsf{false}$ in order to drive a $\beta$-reduction.


One-way functions with polynomial inverting complexity Is there a trap-door-like function whose encoding complexity is polynomial time $n^{k_{1}}$ and inverting complexity(without secret key) is also a polynomial function in input length $n^{k_{2}}$ with $k_{1} << k_{2}$ (say $k_{1} = 2$ and $k_{2}$ is unconditionally provable to be bounded below by $1000$)? What are the implications of such functions if $VNP = VP$?

Some functions are conjectured to have that property, aptly called moderately hard. They were first proposed in the context of spam fighting, and then found their ways into more complicated applications, such as concurrent zero knowledge and timed commitment. They usually use a function of the form $f(x) = g^{2^{2^x}} \bmod N$, first suggested by Rivest, Shamir and Wagner:

  N is a product of two large primes. Without knowing the factorization of N, the best that is known is repeated squaring - a very sequential computation in nature.

If $VNP=VP$, then factorization can be performed efficiently, and therefore we do not have to resort to repeated squaring. However, performing factorization for someone who does not know the factors of N incurs a polynomial overhead.

You may also be interested in the concept of feebly one-way functions, though they are not exactly related to the question.

See the following references as well:

Pricing via Processing -or- Combatting Junk Mail by Dwork and Naor.
Moderately Hard Functions: From Complexity to Spam Fighting by Naor.
Concurrent Zero-Knowledge: Reducing the Need for Timing Constraints by Dwork and Sahai.
Timed Commitments by Boneh and Naor.


Does an algorithm exist to efficiently maintain connectedness information for a DAG in presence of inserts/deletes? Given a directed acyclic graph, $G(V,E)$, is it possible to efficiently support the following operations?

$isConnected(G,a,b)$: Determines if there is a path in $G$ from node $a$ to node $b$
$link(G,a,b)$: Adds an edge from $a$ to $b$ in the graph $G$
$unlink(G,a,b)$: Removes the edge from $a$ to $b$ in $G$
$add(G,a)$: Adds a vertex to G
$remove(G,a)$: Removes a vertex from G

A few notes:

If we disallowed $unlink$, it seems it would be easy to maintain the connectedness information, using a disjoint-set type data structure.
Obviously, $isConnected$ could be implemented using depth or breadth-first search, using the naive pointer-based representation of the graph. But this is inefficient.

I'm hoping for amortized constant or logarithmic time for all three operations. Is this possible?

The problem you have described is fully dynamic DAG reachability (also referred to as fully dynamic transitive closure on DAGs).
It's called fully dynamic since people also study the versions where only deletions are possible (then it's called decremental reachability), and where only insertions are possible (called incremental reachability).

There are a few tradeoffs between the update time and the query time. Let $m$ be the number of edges and $n$ the number of vertices.
For DAGs, Demetrescu and Italiano (FOCS'00) gave a randomized data structure which supports updates (edge inserts or deletes) in O($n^{1.58}$) time and reachability queries in O($n^{0.58}$) time (node inserts/deletes are also supported, in O(1) time); this result was extended by Sankowski (FOCS'04) to work for general directed graphs. Also for DAGs, Roditty (SODA'03) showed that you can maintain the transitive closure matrix in total time O($mn+I·n^2+D$), where $I$ is the number of insertions, $D$ the number of deletions and of course the query time is O($1$).

For general directed graphs, the following (update, query) times are known:
(O($n^2$), O(1)) (Demetrescu and Italiano FOCS'00 (amortized), Sankowski FOCS'04 (worst case)), (O($m\sqrt{n}$), $O(\sqrt{n}$)) (Roditty, Zwick FOCS'02), (O($m+n\log n$), O($n$)) (Roditty, Zwick STOC'04), (O($n^{1.58}$),O($n^{0.58}$)) and (O($n^{1.495}$),O($n^{1.495}$)) by Sankowski (FOCS'04).

Obtaining a polylogarithmic query time, without increasing the update time too much is a major open problem, even for DAGs.


Subexponential hardness assumption Edited
I want to read more about subexponential hardness assumption, but I didn't find any good survey on this. I just took a look at Heavy-tailed distribution and Some properties of subexponential distributions but I didn't get a good picture of it.

  Question: What is the subexponential hardness assumption? Is it a weaker hardness assumption in comparison with discrete logarithm? Do you know any good survey or article on this?

I saw this subject in this paper:
 Adaptive hardness and composable security in the plain model from standard assumptions

"Complex" problems are normally defined as problems which cannot be solved by (probabilistic) polynomial-time Turing machines.

When there are extra information available for solving the problem, the model changes to machines which take advice. That is, instead of $\rm{BPP}$ machines, we consider $\rm{P/poly}$  circuits; i.e. polynomial-size circuits (equivalently, polynomial-time Turing machines which take polynomial advice).

In some cases, we may consider even stronger solvers: Instead of poly-sized circuits, we may use circuits whose size is sub-exponential. (e.g. circuits whose size is $n^{\log n}$). One might note that, an exponential-size family of circuits can decide any language (even undecidable ones) by merely incorporating the look-up table in its code. (In particular, the size of the look-up table is $O(n2^n)$.)

Let's consider the Decisional Diffie-Hellman (DDH) assumption.
I don't go into details. Just assume that $p$ is a large prime, all computations are over $\mathbb{Z}^*_p$, and $g$ is its generator.

  DDH: Distinguishing $(g,g^a,g^b,g^{ab})$ from $(g,g^a,g^b,g^c)$ is hard for $\rm{PPT}$ machines.

A stronger assumption is:

  DDH-1: Distinguishing $(g,g^a,g^b,g^{ab})$ from $(g,g^a,g^b,g^c)$ is hard for $\rm{P/poly}$ circuits.

An even stronger assumption is:

  DDH-2: Distinguishing $(g,g^a,g^b,g^{ab})$ from $(g,g^a,g^b,g^c)$ is hard for sub-exponential circuits.

I saw both DDH and DDH-1 assumptions in the literature. DDH-2 may also exist, but I can't recall whether I ever saw it.

One example of sub-exponential hardness assumption is that, some languages in $\rm{E}$ don't have sub-exponential circuits. Such assumption is used by Impagliazzo & Wigderson in P=BPP unless E has sub-exponential circuits:
Derandomizing the XOR Lemma.

Description of Some Terms

While obvious, I'm going to define several terms here. Let $f \colon \mathbb{N} \to \mathbb{N}$ be a function. Then:

$f(n) = n^{\Theta(1)}$ is called polynomial. (e.g. $n, n^3, 7n^{100}$.)
$f(n) = n^{\omega(1)}$ is called super-polynomial. (e.g. $n^{\log n}, 2^n, 2^{2^n}$.)
$f(n) = 2^{\Theta(n)}$ is called linear exponential. (e.g. $2^n, 3^n, 10^n$.)
$f(n) = 2^{n^{\Theta(1)}}$ is called exponential. (e.g. $2^n, 3^{n^4}$.)
$f(n) = 2^{n^{o(1)}}$ is called sub-exponential. (e.g. $2^{n^{1/n}}, n^{\log n}$.)


What do we know about the phase transition of #P-Complete problems? What is known about the phase transition in #P-Complete problems? Specifically, does there exists a different phase transition for #DNF-k-SAT and #CNF-k-SAT? Update:
As we know, there is a phase transition in Random k-SAT where solving the problem goes from being easy to hard and back to easy again. I would like to know if there is such a phenomenon for #P-Complete problems as well. More importantly, if there exists a phase transition, is it same for #CNF-k-SAT and #DNF-k-SAT? I am thinking that there is some type of phase transition for #CNF-k-SAT. On the other hand, I do not think there is phase transition for #DNF-k-SAT and the problem gets harder as we add more clauses....

For counting independent sets, there is a recent proof for a computational phase transition, by Allan Sly:
http://arxiv.org/abs/1005.5584
(the algorithm is by Dror Weitz from 2006; Allan proved the matching hardness and co-won the best paper award in FOCS'10 for that)

Note that for random 3SAT and similar problems there is no proof that those problems are indeed hard in the appropriate interval. When you go to the harder counting problems, it becomes easier to prove the hardness.


Where do sublinear time algorithms fit in the picture of complexity theory? I know that there are complexity classes that are "below" P like L or NL and stuff like that. But I was curious to know where sub linear time algorithms fitted in this picture and maybe how they were related to the P vs NP problem or if they had their own version of something similar. I am aware that this question might lead to a list of open problem in sublinear time algorithms or something similar, which is a fine answer to my question. I am also curious to know what we know about this theory and what we don't know or what are open problems to tackle.

[I tried adding the tag sublinear time algorithms but I am not sure if it exists. Feel free to add a tag that might help]

Sublinear time algorithms (as well as sublinear space algorithms) are indeed an active area of research. The field of property testing covers much of the sublinear time regime, and I'll point you to the property testing blog to learn about recent work in the area.

The question about complexity theory relating to this is very interesting, and is also an active area of research. P vs NP might not exactly be the right analogy here, but you're right that the boundary between computation and verification is something where sublinearity changes things.

In particular, you can look at a PCP as "kind of" doing something sublinear, in that it only inspects a few bits of a long proof in order to check the prover's claim. More generally, there's been recent work prover-verifier systems where the verifier runs in sublinear time. Some references that are worth perusing:

Interactive proofs of proximity: delegating computation in sublinear time
Non-Interactive Proofs of Proximity


Is it possible to evaluate interaction combinators efficiently using a path-traveling strategy? Interaction combinators can be evaluated using a path traversing strategy. That is, instead of applying annihilation/commutation rules to active pairs, one simply walks through the graph using a 2-stack machine to keep track of the exit ports.

It is known that this strategy, used naively, can have an exponential slowdown in relation to the former strategy. But that doesn't consider the possibility of jumps. Suppose that, instead of merely walking through the graph, the cursor also keeps track of the nodes it passed through. It it comes back to the same node, it jumps directly to the node whose active port would-be to interact with that one.

Is it possible to use this strategy to evaluate interaction combinators? Can it be as efficient as the graph-reduction view?

This has been a subject of investigation for the Implicit Computational Complexity (ICC) community recently.

It is known that in certain cases, when the graph you want to evaluate is of a specific type (be it from typing or a global shape restriction, see references) there is a path-based evaluation strategy that is more efficient than the naive one, allowing for instance to evaluate in Logspace [1,2] or Ptime [3].

The jump approach you mention has been studied by Danos & Regnier [4]. They proved it correct (you get the same output) but do not provide an evaluation of the performance gain. I do not know of any work carrying on this analysis (in full generality) so far.

[1] http://www2.tcs.ifi.lmu.de/~schoepp/Docs/intml_long.pdf

[2] http://arxiv.org/pdf/1406.2110.pdf

[3] http://arxiv.org/pdf/1501.05104v2.pdf

[4] http://ac.els-cdn.com/S0304397599000493/1-s2.0-S0304397599000493-main.pdf?_tid=09e49fd8-768c-11e5-a270-00000aacb360&acdnat=1445278134_7609d8ba21c272fe7eab424d38c3f225


What persistent data structure for a set of partially ordered elements? I need to store sets of elements of type a. Type a is partially ordered, so comparing $a_1$ and $a_2$ can return smaller, greater, equal or incomparable.

One problem with hashtables is that two equal elements can be represented differently, and I do not have access to a hashing function consistent with equality.

Comparing two elements can be a lengthy process so it would be interesting to minimize comparisons. If needed, it is possible to memoize calls to the comparison operator. I realize now that I will only need to store antichains (or let's assume so).
More precisely, the operations I will need to perform are as follows:

Remove an element from the antichain;
Try to add an element. If the element is smaller than a member, do not add it, otherwise, add it and remove every element smaller than it.

I can also bound every element by two integers, so that if I know that $i_1 < a < i_2$ and $i_3 < b < i_4$, then knowing $i_2 < i_3$ instantly gives me $a < b$. Of course, $i_2 \not< i_3$ does not mean $a \not < b$... Finding integer bounds is a relatively cheap operation in comparison to a full blown element comparison.

The paper "Sorting and Selection in PoSets" by Daskalakis, Karp, Mossel, Risensefield, Verbin, 2008 which describes a dynamic representation of PoSets based on antichains.

You might also be interested in the paper "Succinct Posets" by Munro, Nicholson, 2012 recently released on Arxiv and in the bibliography therein. Their data-structure is static but I assume that the next step is to have a dynamical data-structure.


Lee's algorithm for synthesis of ranking functions in size-change termination proofs Consider the following statement that appeared in Lee's Ranking functions for size-change termination (SCT).

  Let $G$ satisfy the SCT condition.

  There is an effective procedure to construct a $G$-ranking function
  expressed using only min, max and lexicographic tuples of program
  parameters and constants.

I'm interested mostly in the computational side of it. Has this been implemented before? If so, in which systems?

In fact, Lee's preliminary algorithm was made more practical by subsequent revisions in joint work with Ben-Amram and Codish. There remains the question of whether their claimed complexity is aceptable in current verifiers and whether it has already been tested in practice.

The complexity is acceptable in current verifiers, and has been implemented in at least the AProVE termination analysis tool for term rewrite systems.

They describe their implementation in Lazy Abstraction for Size-Change Termination, by Codish, Fuhs, Giesl & Schneider-Kamp, basing their implementation on the papers you refer to. Performance is good both from an expressiveness point of view and a run-time perspective.

The additional (clever!) trick is to pre-process the search for an appropriate abstraction and ranking function into a SAT problem (along with other search procedures for termination analysis) and having a SAT solver try to simultaneously find an instance. This trick is common in the termination analysis community.


NFA to DFA Powerset Construction : A Partial determinization algorithm with trade-off between running time and size for the resulting automata? Given a NFA $N$ and its equivalent DFA $D$ resulting from the total determinization of $N$ (using powerset construction, for example), the following properties hold for $N$, $D$ and for any word $w$ :

$N$ reads $w$ in running time at most $O(|w|.|N|^2)$.
$D$ reads $w$ in running time at most $O(|w|)$ and its size may be $O(2^{|N|})$ (in number of states needed to represent $D$).

I wonder if there exists some partial determinization algorithm that guarantees a trade-off between the size of the result and the running time ?

For example, this partial determinization algorithm could turn an NFA into a partially deterministic automata $D'$ such that $D'$ guarantees that the word $w$ is read in $O(|w|.|N|^x)$ where $0 \leq x \leq 2$ without exceeding the size $|D'| \leq 2^{f(x)}$ where $f(x)$ is a continuous decreasing function defined on the range $[0, 2]$ such that $f(0)=|N|$ and $f(2)=log |N|$.

I did not find any method to partially determinize a NFA in such a way. In all papers : either determinization is avoided because the NFA is too large, either determinization is full and the NFA is turned into a DFA (with a possible exponential blowup). There is no compromise...

I would really appreciate any references or any answers regarding this problem. Thank you very much, Luz.

The paper [HP06] is in the spirit of your idea, although in a different direction, in the context of infinite words.
It can be adapted more easily to finite words.

In the powerset construction, we simultaneously keep track of all possible runs of the $n$-state automaton, by moving around $n$ tokens.  But we could decide to follow only $k<n$ runs, and do a partial powerset construction.
In general this will yield a non-deterministic automaton, that is not really more useful than the original one.

But it could be that building $k$ runs with a certain deterministic strategy is always enough to obtain an accepting one, if one exists. Think for instance of a big automaton where the only non-determinism is to guess whether the last letter is an $a$ or a $b$, and then branching towards two deterministic automata. Then two tokens suffice, and a $2$-powerset construction works, where subsets have size at most $2$, i.e. the resulting automaton has $\dfrac{n(n+1)}{2}$ states.

We can define the "width" of a non-deterministic automaton as the number of tokens needed to deterministically build an accepting run. The powerset construction actually assumes that we are in the worst case, i.e. width equal to number of states.
The case where the width is $1$ corresponds to the notion of good-for-games (GFG) automaton, introduced in [HP06], and further studied in [BKKS13,KS15].

We have that a NFA has width at most $k$ if and only if its $k$-powerset construction is GFG.
On finite words, it is in P to detect whether an automaton is GFG, and in this case it actually means that it is deterministic with some additional useless transitions.
This means we could increment $k$ until the resulting $k$-powerset construction is GFG, prune the useless transitions, and we get a deterministic automaton. This corresponds to emphasizing space-saving, since instead of building the big deterministic automaton and then minimizing it, we try to approach it "from below", hoping we won't have to do the full powerset construction.

[HP06]  Solving games without determinization, Henzinger, Piterman, in CSL 2006

[BKKS13]  Nondeterminism in the presence of a diverse or unknown future, Boker, Kuperberg, Kupferman, Skrzypczak, in ICALP 2013

[KS15]   On Determinisation of Good-for-Games Automata, Kuperberg, Skrzypczak, in ICALP 2015


Decomposition by Clique Separators Tarjan described a procedure for decomposing a graph using clique separators in "Decomposition by clique separators", RE Tarjan - Discrete mathematics, 1985 - Elsevier.

He also proposed different divide-and-conquer algorithms for various graph problems such as maximum clique, minimum coloring and maximum independent set. An atom is a subgraph of a graph that does not contain a separator. If one can solve the problem efficiently in the atoms (local solutions) then Tarjan describes in the same paper how to extend these local solutions to a global solution. Therefore characterization of the atoms is very important. For example an atom of a chordal graph is a clique and the atoms of an edge intersection graphs of paths in a tree are exactly line graphs of a multigraph.

I am wondering the characterization of atoms for other graph classes like for example disk graphs or AT-free graphs.

Chvátal and Sbihi (Recognizing Claw-free Perfect Graphs, JCTB 44) described the atoms for the class of claw-free perfect graphs, a.k.a. quasi-line perfect graphs.  This description was later refined by Maffray and Reed, and essentially consists of two classes: "peculiar", which are kind of a special case, and "elementary", which are constructed by modifying the line graph of a bipartite multigraph through an operation called augmentation.


Is there an algorithm that finds the forbidden minors? The Robertson–Seymour theorem says that any minor-closed family $\mathcal G$ of graphs can be characterized by finitely many forbidden minors.

  Is there an algorithm that for an input $\mathcal G$ outputs the forbidden minors or is this undecidable?

Obviously, the answer might depend on how $\mathcal G$ is described in the input.
For example, if $\mathcal G$ is given by an $M_\mathcal G$ that can decide membership, we cannot even decide whether $M_\mathcal G$ ever rejects anything.
If $\mathcal G$ is given by finitely many forbidden minors - well, that's what we're looking for.
I would be curious to know the answer if $M_\mathcal G$ is guaranteed to stop on any $G$ in some fixed amount of time in $|G|$.
I'm also interested in any related results, where $\mathcal G$ is proved to be minor-closed with some other certificate (like in case of $TFNP$ or WRONG PROOF).

Update: The first version of my question turned out to be quite easy, based on the ideas of Marzio and Kimpel, consider the following construction.
$M_\mathcal G$  accepts a graph on $n$ vertices if and only if $M$ does not halt in $n$ steps. This is minor closed and the running time depends only on $|G|$.

The answer by Mamadou Moustapha Kanté (who did his PhD under supervision of Bruno Courcelle) to a similar question cites A Note on the Computability of Graph Minor Obstruction Sets for Monadic Second Order Ideals (1997) by B. Courcelle, R. Downey, and M. Fellows for a non-computability result (for MSOL-definable graph classes, i.e. classes defined by a Monadic Second order formula) and The obstructions of a minor-closed set of graphs defined by a context-free grammar (1998) by B. Courcelle and G. Sénizergues for a computability result (for HR-definable graph classes, i.e. classes defined by a Hyperedge Replacement grammar).

The crucial difference between the computable and the non-computable case is that (minor-closed) HR-definable graph classes have bounded treewidth, while (minor-closed) MSOL-definable graph classes need not have bounded treewidth. In fact, if a (minor-closed) MSOL-definable graph class has bounded treewidth, then it is also HR-definable.

The treewidth seems to be really the crucial part for separating the computable from the non-computable cases. Another known result (by M. Fellows and M. Langston) basically says that if a bound for the maximum treewidth (or pathwidth) of the finite set of excluded minors is known, then the (finite) minimal set of excluded minors becomes computable.

It is not even known whether the (finite) minimal set of excluded minors for the union (which is trivially minor-closed) of two minor-closed graph classes each given by their respective finite set of excluded minors can be computed, if no information about treewidth (or pathwidth) is available. Or maybe it has even been proved in the meantime that it is non-computable in general.


Decomposing graphs of genus one Planar graphs are $K_{3,3}$-free. Such graphs can be decomposed into tri-connected components, which are known to be either planar or $K_5$ components.

  Is there such a "nice" decomposition of graphs of genus one ?

In their seminal work on graph minors, Roberston and Seymour showed that every minor-free graph can be decomposed into a "clique-sum" of "almost planar" graphs. This, of course, applies to bounded-genus graphs also. I am looking for decompositions specific to graphs of genus one, to better understand their structural properties.

I think that Robertson and Seymour showed that every minor-free graph can be decomposed into a "clique-sum" of "almost bounded genus" graphs. The basic building blocks are not planar graphs but graphs of bounded genus (genus depending on the excluded minor). I think that toroidal graphs are not decomposable any further.


What are the negative consequences of extending CIC with axioms? Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term will reduce to its canonical normal form, e.g. if $n : \mathbb{N}$ is true, then $n$ must reduce to a term of the form $(succ ... (succ (0)))$. But when postulating an axiom - say the function extensionality axiom funext - we just add a new constant to the system

$$ funext : \Pi_{x : A} f (x) = g (x) \to f = g$$

that will just "magically" produces a proof of $f = g$ from any proof of $\Pi_{x : A} f (x) = g (x)$, without any computational meaning at all (in the sense that we cannot extract any code from them?)

But why is this "bad"?

For funext, I read in this coq entry and this mathoverflow question that it will cause the system to either loose canonicity or decidable checking. The coq entry seems to present a good example, but I still would like some more references on that - and somehow I can't find any.

How is that adding extra axioms could cause CIC to have a worse behavior? Any practical examples would be great. (For example, the Univalence Axiom?)
I am afraid in this question is too soft, but if anyone could shed some light on those issues or give me some references would be great!

PS: The coq entry mentions that "Thierry Coquand already observed that pattern matching over intensional families is inconsistent with extensionality in the mid 90ies." Does anyone know in which paper or something?

One first reason to reject axioms is that they might be inconsistent. Even for the axioms that are proved consistent, some of them have a computational interpretation (we know how to extend definitional equality with a reduction principle for them) and some do not -- those break canonicity. This is "bad" for different reasons:

In theory, canonicity lets you prove things about the values of your language, without having to go to a specific model. This is a very satisfying property to have thinking about your system; in particular, it supports claims about the real world -- we can think of the nat type as formalized in the system as really "natural numbers" because we can prove that its closed normal inhabitants really are natural numbers. Otherwise it's easy to think that you modelled something correctly in your system, but actually be working with different objects.
In practice, reduction is a major asset of dependent type theories, because it makes proof easy. Proving a propositional equality can be arbitrarily difficult, while proving a definitional equality is (less often possible) but much easier, as the proof term is trivial. More generally, computation is a core aspect of the user experience of a proof assistant, and it is common to define things just so they reduce correctly as you expect. (You don't need axioms to make computation difficult; for example, using the conversion principle on propositional equalities can already block reductions). The entire business of proof by reflection is based on the use of computation to help proofs. This is a major difference in power and convenience with respect to other logics-based proof assistant (eg. HOL-light, which only supports equality reasoning; or see Zombie for a different approach), and using unchecked axioms, or other programming styles, can get you out of this comfort zone.


Constructing terms of function types out of the empty type If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we have the empty function in $\emptyset\to A$. This makes $\emptyset$ the initial object in the category of sets. By set extensionality, there is only this empty function and this also fits with cardinalities, where we like $|A^{\emptyset}|=|A|^{|\emptyset|}=1$.
In logic, we usually take that form absurdum follows everything, ex falso quodlibet, and in the propositions interpretation for types, if $\bf 0$ denotes the empty type (or bottom type), we want a function ${\bf 0}\to \tau$ for all types $\tau$ too.

I've been told in some programs this would be done by defining alla

definition exfalso (a : Type) (x : 0) : a := "case x of -emptyspace-"

Now I try to construct the terms for function types involving the empty type over the standard theories you'd find in books, but I can't quite reproduce the good properties, see below. I wonder

  Which type theories actually let you construct a term of a function type from the empty type, and then, is it unique?

My considerations (leading to more question) are this...

Take simply types lambda calculus. We have $(\lambda (x:\tau).x):\tau\to\tau$ and so $(\lambda (x:{\bf 0}).x):{\bf 0}\to{\bf 0}$. In any model of the type theory, this will be the empty function and so I'm okay with that. But how do I construct, from the typing rules of the theory, any type of ${\bf 0}\to{\bf \tau}$, where $\tau$ isn't ${\bf 0}$? And then, how is there only one? Depending on how the theory lets you define functions, I could imagine ${\bf 0}\to\mathrm{Nat}$ to have zero or an infinite number of terms (constant functions which can never take any input). I guess the cardinal arithmetic then only works out once we pass to the set theoretic model, where all those constant functions are, extensionally, the empty function. Is that right? In a type theory with booleans $\bf 2$, how many functions $\bf 0\to\bf 2$ are there? If $a,b:\bf 2$, are $\lambda x.a$ and $\lambda x.b$ generally two function of this type?

I already answered how to construct such terms in a related question, so let me just amend that answer with some equations.

A standard type constructor which has constructors and eliminators, for instance $A \times B$ has pairing and projections, will have:

$\beta$-rules which says how destructors operate on constructors, for instance: $\pi_1 (a,b) \equiv a$,
$\eta$-rules which say that if we take a thing apart with destructors and put it back together we get the original thing, for instance: $(\pi_1\,u, \pi_2,u) = u$.

The empty type is special because it has no constructors, so where do equations come from? We can take the idea that $\mathbf{0}$ is the initial type and express it as an equation:
$$\mathsf{absurd}_A(e_1) \equiv_A e_2 \tag{1}$$
where $\mathsf{absurd}_A : \mathbf{0} \to A$ is the eliminator (it could also be written as an empty case statement), $e_1 : \mathbf{0}$ and $e_2 : A$. The equation says that $\mathsf{absurd}_A(e_1)$ is equal to every term of type $A$, which is absurd, as it should be. The effect of the equation is that as soon as we have a variable $x : \mathbf{0}$ in the typing context, everything becomes trivial. In categorical language, slicing over $\mathbf{0}$ gives the terminal category -- which is just another way of saying that $\mathbf{0}$ is a terminal object.

We can now show that every two maps $f, g : \mathbf{0} \to A$ are equal, simply because
$$x : \mathbf{0} \vdash f\,x \equiv \mathsf{absurd}_A(x) \equiv g\,x$$
and now by congruence rule for $\lambda$ and $\eta$-rule for functions
$$f \equiv (\lambda x : \mathbf{0} \,.\, f\,x) \equiv (\lambda x : \mathbf{0} \,.\, g\,x) \equiv g.$$
Note however that (1) above is not the kind of equation that type theorists like, because it screwes up various algorithms for checking equality of terms.


Inappoximability status of Max One in Three SAT for satisfiable instances What is the inapproximability status of Max-One-in-Three SAT for satisfiable instances?

The most relevant paper I know is

"The Complexity of Making Unique Choices: Approximating 1-in-k SAT" by Guruswami and Trevisan (link)

They give an algorithm for satisfiable instances which for $k=3$ would achieve a ratio of $\frac{4}{9}$, beating the random assignment. They also mention that 1-in-3 SAT is $\frac{5}{6}$-inapproximable, but I'm not sure if that applies to satisfiable instances. They cite Guruswami's Master's thesis for this.


Most memorable CS paper titles Following a fruitful question in MO, I thought it would be worthwhile to discuss some notable paper names in CS.

It is quite clear that most of us might be attracted to read (or at least glance at) a paper with an interesting title (at least I do so every time I go over a list of papers in a conference), or avoid reading poorly named articles.

  Which papers do you remember because of their titles (and, not-necessarily, the contents)?

My favorite, while not a proper TCS paper, is "The relational model is dead, SQL is dead, and I don’t feel so good myself." .

I did a survey on Twitter about this a while back, results here. A few of my favorites:

Parametric Polymorphism through Runtime Sealing, or, Theorems for Low, Low Prices! by
Jacob Matthews and Amal Ahmed, ESOP 2008 DOI:10.1007/978-3-540-78739-6_2
F-ing Modules by Andreas Rossberg, Claudio Russo, and Derek Dreyer, TLDI 2010
Cons should not cons its arguments and Cheney on the MTA, both by Henry Baker, SIGPLAN Notices 1992 and 1995. Baker has lots of other great paper titles, too.
How to Roll a Join: Asynchronous Incremental View Maintenance by Salem, Beyer, and Lindsay, SIGMOD 2000 DOI:10.1145/342009.335393
A Very Modal Model of a Modern, Major, General Type System by Appel, Mellies, Richards, and Vouillon, POPL 2007 DOI:10.1145/1190216.1190235
Clowns to the Left of me, Jokers to the Right, Conor McBride, POPL 2008 DOI:10.1145/1328438.1328474
Linear types can change the world!, Phil Wadler, Programming Concepts and Methods 1990 (note that the ! is signficant)


Correlation between noise resilience and output distribution of Boolean circuits Given a randomly generated AND/OR tree (and negations), we can calculate the probability that the circuit will represent a specific Boolean function up to 3 input literals. Starting from 4 (or at least 5) literals, the system of equations becomes too complex to compute, and it's even questionable whether the output distribution of Boolean functions can be reliably approximated. See D. Gardy, Random Boolean Expressions, chapter 3.4.3.

Another line of research deals with the question of how robust Boolean circuits are in the presence of noise or faulty gates. See P. Gács, A. Gál, Lower Bounds for the Complexity of Reliable Boolean Circuits with Noisy Gates and A. Mozeika, D. Saad, On reliable computation by noisy random Boolean formulas who explicitly consider random Boolean formulas.

My question is if there is correlation between the probability/frequency of a certain Boolean function and the resilience of a given generating circuit (formula) against noise. In other words, can we estimate (or at least get some bounds on) the probability of a function from the circuit's noise resilience which we could try to measure by causing arbitrary perturbations to gates and see how the resulting function reacts?

My intuition is that circuits representing simple Boolean functions with high probability such as the tautology TRUE or the output of a single literal will tolerate higher noise levels since those circuits have a higher "density" in the space of all possible circuits of a given size.

I have found some hints on my question in Moshe Looks, Competent Program Evolution, p. 31:

Most local perturbations of large random formulae have no effect – 96% of them for
arity five, and 91% for arity ten (the drop is a corollary of the increase in the percentage of
unique behaviors in a fixed size sample as the arity increase). This is a consequence of such
formulae typically being highly redundant – e.g., a large formula that computes a tautology
will likely remain a tautology when randomly perturbed (similarly a large subformula which
computes a tautology, etc.).

More resources would be highly appreciated if you know of any.


Single-pass streaming quantile estimation using moments Is it possible to estimate within $\epsilon$ the quantiles of a set of integers $\{x_1, x_2, \dots, x_n\}$ given only the values $\sum x_i^0,\sum x_i^1, \sum x_i^2, \dots, \sum x_i^{f(n)}$ where $f \in o(n)$? If so, what is the most slowly growing $f$ that will suffice?

By "estimate the quantiles", I mean:

  ... for any given rank $r$, an $\epsilon$-approximate quantile summary returns a value whose rank $r'$ is guaranteed to be within the interval $[r - \epsilon n, r + \epsilon n]$.

following "Space-Efficient Online Computation of Quantile
Summaries", by Greenwald and Khanna.

I'm also interested in whether this is possible with non-integer, non-consecutive moments, so sets of values like $\sum x_i^{-1/2}, \sum x_i^\pi$ are also of interest.

I am more interested in deterministic algorithms than randomized ones.

Gan et al. address this in Moment-Based Quantile Sketches for Efficient High Cardinality Aggregation Queries. The answers are rather nuanced.