The proof of P2b in Paxos made simple I am reading Paxos Made Simple. I am quite confused about the proof of P2b. It said

  We would make the proof easier by using induction on n, so we can prove that proposal number n has value v under the additional assumption that every proposal issued with a number in m..(n - 1) has value v.

How can he add the additional assumption? Is it reasonable? In reality, proposal numbered in m..(n - 1) can have value other than v, isn't it?

I am really confused about that, please help! Thanks

Note: I have had a similar question about the correctness proof of Paxos and Fast Paxos before and posted it here. Wish the excellent answer to it be helpful to you.

A few words about this paper:

Leslie Lamport has his own, very impressive writing style. He is not satisfied with the common pattern of stating a theorem, proving it, moving on to another theorem, and so on. He is good at demonstrating the way how to solve a problem. In his paper, you will see that proof does not follow a theorem; instead, it comes along with a theorem. The paper "Paxos Made Simple" is a typical example of this style.

About your questions:

  Your question (1): How can he add the additional assumption? Is it reasonable?

Leslie Lamport is using strong induction. The goal here is to prove

  $P2^{b}:$ If a proposal with value $v$ i chosen (say, with number $m$), then every higher-numbered proposal issued by any proposer has value $v$.

We apply strong induction to natural number $\mathbb{N}$. I summarize the proof as follows and explain it later.

The base case is "some proposal with number $m$ and value $v$ is chosen".
The strong induction hypothesis is "every proposal issued with a number in $m .. (n-1)$ has value $v$".
The induction step to prove $P2^{b}$: Combining the premise of "$m$ is chosen (with value $v$)" with the above induction hypothesis, we get (for reference, I call it $C$-condition):

  $C$-condition: Every acceptor in $C$ (defined in the paper) has accepted a proposal with number in $m .. (n-1)$, and every proposal with number in $m .. (n-1)$ accepted by any acceptor has value $v$.

Now, Lamport introduces $P2^{c}$, which, along with the above $C$-condition, is sufficient for $P2^{b}$.

You can think of this induction process step by step:

The base case $m$ is trivially valid.
Given that step 1 is valid, the argument in "The induction step" above (of course with $P2^{C}$) shows that the proposals numbered $m+1$ has value $v$.
Given both step 1 and step 2 are valid, the same argument shows that the proposals numbered $m + 2$ has value $v$.
And so on.

This also answers your second question.

  Your question (2): In reality, proposal numbered in $m..(n - 1)$ can have value other than v, isn't it?

No, it isn't. The Paxos algorithm guarantees that all the proposals with larger numbers than $m$ must have value $v$, given that $m$ is chosen with value $v$.


Graph-theoretic properties of the Wiener index The Wiener index of a graph is the sum of the lengths of the shortest paths between all pairs of its vertices.

Are there useful graph-theoretic properties of this index?

On the same page there was a section: relation to chemical properties (http://en.wikipedia.org/wiki/Wiener_index#Relation_to_chemical_properties) Maybe references in that section mentions more about how this index can be used for graphs. Seems like you can estimate the overall structure of the graph if it is dense (low index) or sparse. Because the lengths of all shortest pairs would be shorter in a dense graph.


Genetic Algorithm convergence test functions I was working on parallel implementation of Genetic Algorithm with MapReduce. I have found that in many papers authors are referencing OneMAX as problem they used to test scalability and convergence of their algorithm implementations.

I would like to know more about why this problem is good for testing, and if you could recommend any other exotic and nice fitness functions I could use in tests.

Kind Regards,
ZeKoU

One-max is really only suitable for testing for obvious bugs in your implementation.

There are a few widely used sets of benchmark functions, but they're of rather dubious value in general as well. You don't mention what sort of domain you're planning to work on -- there are binary problems like Knapsack problems, real-valued problems (which may or may not be represented with binary encodings in a given GA), permutation problems like TSP, QAP, and some scheduling problems, etc.

Some of the more popular benchmarks have always been real-valued function optimization problems. Griewangk's function, Rastrigin's function, Ackley's function, Rosenbrock's function, and the De Jong F1-F5 functions have all been used pretty heavily in the literature (as well as others). There are also shifted and rotated versions of several of those problems that attempt to work around some of the more obvious biases and deficiencies such as the optimum of most of them being at the origin.

There have been a few attempts at producing good sets of benchmarks. There was a 2005 CEC workshop that proposed 25 or so real-valued problems. I think there was another workshop in 2010 that might have included a different set of problems, but I'm hazy on the details now.

I haven't been able to provide you with much in the way of concrete information about particular test functions, but hopefully there's enough here to get you started with Google.


Approximating the clique size of the graph Let $G=(V,E)$ be a graph. For a given $\rho \leq |V|$ and $\epsilon$ with $(0<\epsilon<1)$, is there any sublinear query algorithm known/possible to decide if the graph has a clique of size $\rho$, or all the cliques are of size at most $\rho(1-\epsilon)$.

More precisely, for a given probability tolerance $\delta$ and error tolerance $\epsilon$, algorithm queries $f(\frac{1}{\epsilon}, \frac{1}{\delta}).o(n^2)$ many position of the corresponding adjacency matrix of the graph, and accept with probability at least $1-\delta$ if the graph has a clique of size $\rho$, or reject probability at least $1-\delta$ if all the cliques are of size at most $\rho(1-\epsilon).$

Thanks in advance.

It's not possible. The reason is that, to distinguish an $n$-vertex graph with no edges (clique size 1) from a graph with a single randomly-chosen edge (clique size 2) requires $\Theta(n^2)$ queries. So it's not possible to get sublinear queries for $\rho=2$ and $\epsilon<\frac12$, but your question asks for a parameterization that remains sublinear for all $\rho$ and all $\epsilon>0$.


Why does not the definition of NP problems care about the complexity of guessing? I have a question regarding the definition of NP problems. According to that, a problem is in NP if one can guess a certificate of polynomial size in polynomial time. However, this definition does not account for two things. First, how many certificates the problem can have? Should it be harder to deal with problems which have infinitely many certificates (even thought still in polynomial sizes) than ones that have only few? Why does not this feature affect the complexity of the underlying problem? Second, why does the size of the certificate (witness) but not the complexity of the guessing take a role in this definition?
I would really appreciate any clarification of this confusion.

According to that, a problem is in NP if one can guess a certificate of polynomial size in polynomial time.

No, there is nothing about guessing in the actual definition. It is required that a certificate exist if the answer is "yes" (and doesn't exist if the answer is "no") and that verification of a proposed certificate takes polynomial time. The definition specifically doesn't require that there is any way to obtain the certificate if one exists, so we sometimes talk about "guessing" it. But it could equally be replaced e.g. by "if an alien gives you a string and claims it's a certificate for an instance, you can verify this in polynomial time". In any case, neither "guessing" nor "being given by an alien" have any complexity we could talk about.

In fact, for any $NP$ problem there are algorithms allowing to find a certificate for any instance (if one exists, i.e. if the answer is positive). But if this algorithm is polynomial, then the problem is actually in $P$, and for $NP$-complete problems only exponential algorithms are known.

  which have infinitely many certificates (even thought still in polynomial sizes) than ones that have only few

For any $n$ and for any polynomial of $n$ there is a finite number of strings of that length. Even if all of them are certificates (such as in the proof that $P$ is a subset of $NP$), you can't have an infinite number of certificates.


Applications of MCTS/UCT MCTS/UCT is a game tree search method that uses a bandit algorithm to select promising nodes to explore. Games are played to their completion randomly and nodes leading to more wins are explored more heavily. The bandit algorithm maintains a balance between exploring nodes with high win rates and exploring unknown nodes (and in its pure form doesn't necessarily use a heuristic evaluation function). Programs based on this general technique have achieved pretty amazing results in computer Go.

Have bandit-driven monte-carlo searches been applied to any other search problems? For instance, would it be a useful approach in approximating solutions to MAX-SAT, BKP, or other combinatorial optimization problems? Are there any particular characteristics of a problem (structural/statistical/etc.) that would suggest whether or not a bandit-style approach would be effective?

Are there any known deterministic problems that would be totally resistant to bandit methods, due to the nature of the solution space?

This is not a complete answer, but some basic observations about applying this to MAX-SAT.

At a high level, it looks like this heuristic approach (when applied to MAX-SAT) would be similar to a branching algorithm based on the method of "conditional expectation", a standard method in derandomization. For example, to get a deterministic $7/8$-approximation for MAX 3-SAT (with 3 variables per clause), one sets a variable $x=0$, estimates the expected fraction of clauses that will be satisfied by a random assignment in the remaining formula, then sets $x=1$ and does the same calculation. (This looks extremely similar to "playing a game to completion randomly".) The variable setting with the higher expected fraction of clauses ($x=0$ or $x=1$) will be chosen. This polynomial time algorithm gives a $7/8$-approximation and is known to be tight (you can fool it into satisfying only $7/8$ of the clauses). This connection should make it possible to prove lower bounds on the ability of this heuristic.

It is known that approximating MAX 3-SAT better than $7/8$ is $NP$-hard, so we don't expect an efficient heuristic to do better than this. It would be interesting to show (and I conjecture it is true) that a branching algorithm based on the above variable choice heuristic requires exponentially many steps to find a better-than-$7/8$ approximation. There are already lower bounds on backtracking which say that no matter what heuristic you use, even if you guess perfectly, there are still unsatisfiable formulas for which backtracking will only conclude they're unsatisfiable after exponentially many steps. Lower bounds on the lengths of resolution proofs yield these results. One reference is:

  Pavel Pudlák, Russell Impagliazzo: A lower bound for DLL algorithms for k-SAT (preliminary version). SODA 2000: 128-136


How many instances of 3-SAT are satisfiable? Consider the 3-SAT problem on n variables.  The number of possible distinct clauses is:

$$C = 2n \times 2(n-1) \times 2(n -2) / 3! = 4 n(n-1)(n-2)/3 \text.$$

The number of problem instances is the number of all subsets of the set of possible clauses: $I = 2^C$.  Trivially, for each $n \ge 3$, there exist at least one satisfiable instance and one unsatisfiable instance.
Is it possible to calculate, or at least estimate, the number of satisfiable instance for any given n?

A long history of work on phase transitions in SAT has shown that for any fixed $n$, there's a threshold parametrized by the ratio of number of clauses to $n$ that decides satisfiability. Roughly speaking, if the ratio is less than 4.2, then with overwhelming probability the instance is satisfiable (and so a huge fraction of the number of instances with these many clauses and variables are satisfiable). If the ratio is slightly above 4.2, then the reverse holds - an overwhelming fraction of instances are unsatisfiable.

The references are way too many to cite here: one source of information is the book by Mezard and Montanari. If anyone has sources for surveys etc on this topic, they could post it in comments or edit this answer (I'll make it CW)

References:
 - Achlioptas survey
 - Where the really hard problems are
 - Refining the phase transition in combinatorial search


Educational Source or Survey on Analysis of Semidefinite Program? When designing approximation algorithms one sometimes solves a semidefinite program followed by a rounding step. An often used example to illustrate this is Max-Cut. (See e.g. Approximation Algorithms by Vijay Vazirani.)

Are there good educational sources or surveys going beyond the Max-Cut problem to explain more complex rounding algorithms and techniques used for their analysis? I'm thinking of cases when the vectors of the SDP-solution aren't distributed uniformly on a hypersphere, they have different lengths, or have other properties making the analysis harder.

Check Chapter 6 in the book "The Design of Approximation Algorithms" by Williamson and Shmoys. The book is available on-line here: http://www.designofapproxalgs.com/


Where can I find examples of error correcting codes of the following types? First, apologies if this question is in appropriate or trivial for this site. I'm a physicist looking for some help outside his comfort zone.

In PRL 87 167902 (2001) it is claimed that

"...for an arbitrarily small $\delta>0$ there exists an error-correcting code $E: \{0,1\}^n \rightarrow \{0,1\}^m$ with $m\leq n / \delta^c$ (for some constant $c$) such that the Hamming distance between any two distinct code words $E(x)$ and $E(y)$ is between $(1 - \delta)m/2$ and $(1 + \delta)m/2$."

In the paper, this is known because of non-constructive proofs of existence. I would like to know if any explicit examples of such codes (or similar ones, or even better ones) exist, given that paper was 16 years ago.

In particular, I'm interested in codes $E: \{0,1\}^n \rightarrow \{0,1\}^m$ where $m = O(n)$ and the Hamming distance between two distinct code words has a lower bound at least linear in $m$ (I'm pretty flexible about the behaviour with $\delta$, as I just need the $\delta = 1/2$ case).

I ask here becuse I'm sure this will be a very easy question to the correct person, but I am not that person and I'm not sure where best to start looking. Any hints of where to look would be much appreciated.

If you just need any code $E : \{0,1\}^n \to \{0,1\}^m$ where $m=O(n)$ and where the distance is linear in $m$, then what you are looking for is called an "asymptotically good code". There are many explicit constructions of such codes, and you can find the basic ones in lecture notes of courses about coding theory. For example, you can find a description of a classic construction in Lecture 7 here. Another example of a construction is expander codes, which are described in Lecture 14 there.

If you are looking specifically for codes where the distance between any two codewords is close to $\frac{m}{2}$, and in particular is upper bounded by $(1+\delta)\cdot \frac{m}{2}$, then things are a bit more complicated. Such codes are tightly related to objects called "$\epsilon$-biased sets", which have been studied for quite a while in TCS. You can find a very recent construction of such codes here. The earliest constructions can be found here and here (although they only give you $m = \rm{poly}(n)$).


Which formalism is best suited for automated theorem proving in set theory? Abbreviations - FOL is first-order logic; NBG is Von Neumann–Bernays–Gödel set theory; SEP is Stanford Encyclopedia of Philosophy; HOL is higher-order logic; ATP is automated theorem proving.

Context - An entire section of TPTP’s [1] axioms is devoted to set theories - for example NBG - for FOL theorem provers. Art Quaife wrote an entire book [2] on axiomatizing NBG in FOL.

It seems to me - These axioms all take membership as a sort of undefined concept, and then build subsets, power sets, union, difference, and so on.

In contrast, here is what SEP has to say on HOL (emphasis mine) -

  Second-order logic is an extension of first-order logic where, in addition to quantifiers such as “for every object (in the universe of
  discourse),” one has quantifiers such as “for every property of
  objects (in the universe of discourse).”   This augmentation of the
  language increases its expressive strength, without adding new
  non-logical symbols, such as new predicate symbols.   For classical
  extensional logic (as in this entry), properties can be identified
  with sets, so that second-order logic provides us with the
  quantifier “for every set of objects.”

It seems to me - that the concept of membership can only be represented in HOL. If that is true, how can FOL axiom schemas, taking membership as an undefined concept, prove theorems in set theory?

What I am trying to do - I need to do ATP in a theory which is FOL+sets. I was unsure whether to use an FOL prover (say, Prover9) or an HOL prover (say, HOL Light). At present, I’m using SNARK (FOL) with Quaife’s axiomatization of NBG, which is unable to prove my theorems (see below for example).

Question - Is this failure to be expected, since FOL cannot ‘understand’ membership, and hence I need an HOL prover? Or am I misunderstanding / doing something wrong?

[1] The TPTP Problem Library for Automated Theorem Proving, http://www.cs.miami.edu/~tptp/
[2] Automated Development of Fundamental Mathematical Theories, by Art Quaife, Kluwer Acadamic Publishers (1992)

Finally, an example -

Here is SNARK code representing three axioms, and a theorem, which SNARK is unable to prove. SNARK has also been given Quaife's axioms of NBG set theory. (Note member, the set membership function.) -

(assert  '(forall (x y z)
    (implies
      (and
        (part-of x y)
        (part-of y z)
      )
      (part-of x z)   ) ) :name '1point1point1)

(assert  '(forall (x y alpha t)
    (exists (z arb-part)
      (implies
        (and
          (and
            (member t alpha)
            (part-of t x)
          )
          (implies
            (part-of y x)
            (and
              (member z alpha)
              (and
                (part-of arb-part z)
                (part-of arb-part y)
        ) ) ) )
        (sum-of x alpha)   ) ) ) :name '1point1point2)

(assert  '(forall (alpha)
    (exists (arb-member sum)
      (implies
        (member arb-member alpha)
        (sum-of sum alpha)
) ) ) :name '1point1point3)

(prove  '(forall (x)
    (part-of x x)   ) :name '1point1point4)

EDIT -

Jake said - "set theories are often defined in first order logic". In fact, the question I was asking was - "Can set theories be defined in first order logic, in an automated theorem prover?". That's what I meant, when I said "is set theory equivalent to first order logic?" (which is an incorrect way of putting it, and for which I apologize).

It turns out that ZFC cannot be represented in an FOL theorem prover, since it is not finitely axiomatizable. NBG and one other set theories can, and several such axiomatizations exist in TPTP.

However, these axiomatizations seem to take the concept of membership as undefined, and build subsets, power sets, etc on that. The SEP paragraph I quoted seems to suggest that representing membership needs HOL. In such a case, it seems paradoxical to me that FOL provers are expected to prove theorems in set theory, knowing nothing of membership.

I'm sure this is not a real paradox - just something I don't understand. Hence the question. I hope that makes it clearer.

There are numerous ways of formalizing set theory:

ZFC uses first-order logic and a primitive relation $\in$
NBG uses first-order logic, a primitive relation $\in$, and a primitive predicate $S$
Church's type theory is multi-sorted and uses infintely many types
Type theory is similar to set theory, but not quite the same
Second-order arithmetic, through some coding tricks, can express many things we usually want to express in analysis
etc.

But this is all quite irrelevant to what you are doing. You seem to be using automated theorem provers as "black boxes" to prove simple theorems in set theory. This is a hit-and-miss activity: some theorem provers will prove some simple things, and others will prove other simple things, but they will all fail on statements that mathematicians consider "completely trivial". Such is the state of automated theorem proving.

Rather than worrying which particular formalism you are using, you should investigate which automated theorem prover is good for what. It is also very likely that you do not actually need set theory. It would be helpful if you described what you're doing, but not here, this should go on cstheory.stackexchange.com. There perhaps we can suggest a good way of formalizing whatever you are doing.


Explaining computer science algorithms/concepts/ideas using metaphors Recently I found an interesting algorithm book entitled 'Explaining Algorithms Using Metaphors' (Google books) by Michal Forišek and Monika Steinová. "Good" metaphors help people understand and even visualize the abstract concepts and ideas behind algorithms.

For example,

  One well-known exposition of the shortest path using the balls-and-strings model
  looks as follows: To find the shortest path between $s$ and $t$, one just grabs the corresponding two balls and tries to pull them apart.

My question:

  I would like to see as many metaphors as possible for computer science algorithms/concepts/ideas.
  Do you know any? Do you have your own ones?

B-Trees, N-ary Trees, Autocracy and Democracy

http://rkvsraman.blogspot.in/2008/08/b-trees-n-ary-trees-autocracy-and.html


Type inference for imperative statements other than assignment In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as compound operators, loops or conditionals.

So it's not clear how an imperative language with partial type inference such as http://rust-lang.org can be implemented.

The papers don't mention parametrized types such as List of a because parametrized types are a trivial extension of Hindley-Milner type system - only the unification algorithm should be extended, and the rest of inference works as is. However, assignments cannot be trivially added because paradoxes arise, so special techniques such as ML value restriction must be applied.

Can you recommend any papers or books describing a type system for a language with imperative loops, conditionals, IO and compound statements?

If you're looking for a neat, functional reference to type-inference, I'm a bit partial to Gundry, McBride, and McKinna's 2010 "Type Inference in Context", though this may not be a good guide to any actual existing implementations.

I think part of the answer is that, beyond the value restriction, there really isn't that much difficulty adapting Hindley-Milner type inference to imperative languages: if you define e1; e2 as syntactic sugar for (fn _ => e2) e1 and define while e1 do e2 as syntactic sugar for whiledo e1 (fn () => e2), where whiledo is a regular recursive function

fun whiledo g f = if g then (f (); whiledo g f) else ();

then everything will work fine, including type inference.

As for the value restriction being a special technique, I like the following story; I'm pretty sure I picked it up from Karl Crary. Consider the following code, which the value restriction will prevent you from writing in ML:

let
   val x: 'a option ref = ref NONE
in
   (x := SOME 5; x := SOME "Hello")
end

Compare it to the following code, which is totally unproblematic:

let
   val x: unit -> 'a option ref = fn () => ref NONE
in
   (x () := SOME 5; x () := SOME "Hello")
end

We know what the second example does: it creates two new ref cells containing NONE, then puts SOME 5 in the first one (an int option ref), then puts SOME "Hello" in the second one (a string option ref).

But think about the first example in terms of how we would represent x in System F (the polymorphic lambda-calculus). In such a setting, x would be a value of type "$\forall \alpha. \mbox{ref}(\mbox{option}(\alpha))$", so that means that, as a term, the value of x must be a (type) lambda: "$\Lambda \alpha. \mbox{ref}[\alpha](\mbox{NONE})$".

This would suggest that one "good" behavior of the first example is to behave exactly the same way the second example behaves - instantiate the type-level lambda two different times. The first time we instantiate x with int, which will cause x [int] to evaluate to a reference cell holding NONE and then SOME 5. The second time we instantiate x with string, which will case x [string] to evaluate to a (different!) reference cell holding NONE and then SOME "Hello". This behavior is "correct" (type-safe), but it's definitely not what a programmer would expect, and this is why we have the value restriction in ML, to avoid programmers dealing with this unexpected sort of behavior.


Looking for easy applications of fractional cascading I want to give a couple of talks on fractional cascading, one of which will focus on applications.  I'm looking for applications that make use of the full version of fractional cascading, not just the simple search-in-k-sorted-lists version.

The applications presented in the original companion paper require a lot of machinery in addition to fractional cascading and are therefore not suitable.  My audience is general CS people who don't have specialized data-structures or computational-geometry knowledge.

Any help will be much appreciated.

Chazelle and Guibas wrote a paper describing some of the good applications that can be made with Fractional Cascading: Link

Some of the most interesting applications are:

Intersection of a polygonal path $P$ and a line. Given the path $P$, pre-process it and allow queries of the form: Given a line $l$, report all the intersections of $P$ and $l$.
Orthogonal Range Search. Given points in $R^d$, and a $d$-orthotope. Return the points that lie in the orthotope.
Planar point Location. Locate a point in a planar subdivision.

You do have to give a bit more background as this problems tend to be geometrical in nature. Fractional Cascading is really only good when tackling higher dimensional problems.


Forbidden minors for bounded genus graphs It is well known that $K_5$ and $K_{3,3}$ are forbidden minors for planar graphs. There are hundreds of forbidden minors for graphs embeddable on a torus. The number of forbidden minors for graphs embeddable on surface of genus g is an exponential function of g. My question is as follows :

  Is there an explicit graph $G_t$ on t vertices (which is not a complete graph) such that $G_t$ is a forbidden minor for graphs embeddable on surface of genus g, where t is a function of g ?

EDIT : I realized that the following theorem is known :

  For every surface Σ there exists an integer r such that $K_{3,r}$ does not embed in Σ.

So, I am looking for $G_t$ that is not complete graph, not a complete bipartite graph.

The disjoint union of $n$ copies of $K_5$ (or $K_{3,3}$) is a minimal forbidden minor for the graphs of genus $n-1$; the same is true for a graph in which some of these copies share a single vertex, so that the blocks of the graph are $K_5$ or $K_{3,3}$. This follows from results in J. Battle, F. Harary, Y. Kodama and J.W.T. Youngs, "Additivity of the genus of a graph", Bull. Amer. Math. Soc. 68 (1962) 565–568, and is already enough to show that there are at least exponentially many forbidden minors.

Bojan Mohar, "An obstruction to embedding graphs in surfaces", Discrete Math. 78 (1989) 135–142, lists the graph formed from $K_8$ by removing a 4-cycle as having genus 2. Since $K_7$ is toroidal, this means that either $K_8\setminus C_4$ or one of its spanning subgraphs is an obstruction to torus embedding, and that graphs that have $n$ copies of this graph as their blocks have genus $2n$.

Mohar also shows that the graph formed from a $(2k+2)$-cycle by connecting vertex 0 to all the even vertices and vertex 1 to all the odd vertices has "relative genus" at least $\lceil k/2\rceil$. The graph is planar, but I think relative genus means that the cycle has to be a face; or you could add another vertex to the graph, connected to all of the cycle vertices, to effectively force it to be a face. Maybe this is closer to the sort of thing you want. But I don't think he shows that these graphs are minimal forbidden minors.


What arithmetical theorems can plain $\lambda \Pi$ reason about? I've read that System F cannot state or prove theorems of the First Order Theory of Arithmetic. I assume this is because we lack dependent types, so we cannot explicitly express $\forall n:\mathbb{N}.P(n)$ as an inhabitable type. Thus, $\lambda\Pi$/LF seems promising despite its lacking expressivity of functions.

My question concerns whether it is even possible to encode proofs of arithmetic in $\lambda\Pi$. I am assuming there would need to be some sense of equality, perhaps a type only inhabited when two terms are $\beta\eta$-equivalent. Some sense of induction seems necessary also. I'm not convinced that such things wouldn't require additional inference rules to the theory.

At a minimum, I'm interested in being able to encode statements like "$\forall x \forall y. x + y = y + x$", or "$\forall x\exists y.x<y\land\textrm{prime}(y)$", and I don't know if these can even be encoded as types.

Can theorems of arithmetic be encoded and proved in plain $\lambda\Pi$? If not, what's required?

As Andrej notes, $\lambda\Pi$ is a conservative extension of first-order logic which means:

  Adding the axioms of PA to $\lambda\Pi$ gives exactly the same arithmetic theorems as PA.

However, because of the more expressive system, it is possible to finitely axiomatize induction using the following (encoding of) this axiom:

$$ \forall P: {\mathbb N}\rightarrow \mathrm{Type}, P\ 0 \rightarrow (\forall n, P\ n \rightarrow P\ (S\ n))\rightarrow \forall n, P\ n$$

Note that you need a single Martin-Löf universe to be able to state this. Adding equality and the other PA axioms (definitions for $+$, $\times$, injectivity of $S$) in a similar manner, one might ask if this axiomatization is conservative over PA, or rather HA, since we don't necessarily want the Excluded Middle.

The answer is yes, though this is quite a non-trivial thing! The proof involves some somewhat deep ideas from the field of realizability.

Finally, though this is a fine axiomatic system, it may be frustrating to note that $+$ and $\times$ (and equality, I guess) do not have the computational behavior one might expect in a dependently typed theory, as one would in a system like Coq or Agda.

This is where Martin-Löf's inductive families comes in: one can give a computational content to the induction axiom, which allows one to define addition and multiplication, as well as prove injectivity of $S$ if enough power is given to the type-level computation rules (this point is probably a story for another time).

And finally one can even define existential quantifiers and equality itself using these families, which is a quite remarkable observation from the theory of inductive families.

Note that Twelf seems to frown upon these last 2 steps, preferring to keep $\beta$ equality alone in its computation, and having predicates for everything else. They have their reasons, I guess.


What is the benefit of Krivine's notation? I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus.  For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ (with the normal convention that function application associates to the left, so it actually means $\lambda f . \lambda x . \lambda y . ((f\ x)\ y)$) is written $\lambda f . \lambda x . \lambda y . (f)\ x\ y$ (with a similar convention that it actually means $\lambda f . \lambda x . \lambda y . ((f)\ x)\ y$).  I do not see the point of having another pair of parentheses around the innermost $f$.  Why do people use Krivine's notation instead of the usual one?

I'm assuming you mean Krivine's notation from Lambda Calculus: Types and Models.

This notation, used as a data representation, makes many algorithms on lambda-terms simpler to implement and prove correct. That is, given a  lambda term $f\; e_1\; e_2\; \ldots\; e_n$, you want to view it as a head $f$, together with a list of arguments $[e_1,  e_2, \ldots, e_n]$.

For example, suppose you want to compare two terms $f\;e_1\;\ldots\; e_n$ with $g\;t_1\;\ldots\;t_n$. It is often most natural to compare the heads $f$ and $g$ first, and not even look at the $(e_i, t_i)$ pairs unless that comparison succeeds. (This often comes up in implementations of higher-order unification.)

See Cervesato and Pfenning's paper A Linear Spine Calculus for a formalization of this idea.


Is there an online-algorithm to keep track of components in a changing undirected graph? Problem

I have an undirected graph (with multi-edges), which will change over time, nodes and edges may be inserted and deleted. On each modification of the graph, I have to update the connected components of this graph.

Properties

Additional properties are that no two components will ever be reconnected. Obviously, the graph can have cycles to an arbitrary amount (otherwise the solution would be trivial).
If an edge $e$ does not contain a node $n$, it will never adopt that node. However, if $n \in e$, it can change to $n \notin e$.

Approaches

I have two possible approaches so far, but as you will see they are horrible:

Slow state-less

I can search (dfs/bfs) the graph starting from the modified element(s) every time. This conserves space, but is slow as we have O(n+m) for each modification.

Stateful fast(-er) (?) approach

I can store all possible paths for each node to all possible nodes, but if I see it correctly, this will take O(n^4) memory. But I am not sure how the runtime improvement is (if there is one at all, because I have to keep the information up-to-day for every node in the same component).

Question

Do you have any pointers, how I can learn more about that problem or perhaps some algorithms I can build on?

Note

If there is a vast improvement in runtime/memory I could live with a non-optimal solution that sometimes says two components are one, but of course I would prefer an optimal solution.

There are several data structures that support edge insertions, edge deletions, and connectivity queries (Are these two vertices in the same connected component?) in polylogarithmic time.

Monika R. Henzinger and Valerie King.  Randomized fully dynamic graph algorithms with polylogarithmic time per operation.  Journal of the ACM 46(4):502—516, 1999.
Jacob Holm, Kristian de Lichtenberg, and Mikkel Thorup. Poly-logarithmic deterministic fully-dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity, Journal of the ACM 48(4):723—760, 2001.
Mikkel Thorup.  Near-optimal fully-dynamic graph connectivity.  Proc. 32nd STOC 343—350, 2000.


Channel coding results using Kolmogorov complexity Usually Shannon entropy is used to prove channel coding results. Even for source-channel separation results shannon entropy is used. Given the equivalence between Shannon (global) vs Kolmogorov (local) notions of information, has there been a study to utilize Kolmogorov complexity for these results (or atleast to replace the source coding part in source channel separation results)?

For channel capacity, it seems difficult to replace Shannon entropy by Kolmogorov complexity. The definition of channel capacity does not contain any mention of entropy.
Using the Shannon entropy gives the right formula for channel capacity (this is Shannon's theorem). If you replaced the formula with Shannon entropy by a formula with Kolmogorov complexity, it would presumably be a different formula, and so it would be the wrong answer.

If you want to send a string with Kolmogorov complexity $K$ through a channel with capacity $C$ using only slightly more than $K/C$ channel uses, this is very easy. Find the description of the Turing machine that produces the string. Then encode it with an error-correcting code so this description can be sent through the noisy channel with only a small probability of error.

The hard part of the source-channel separation theorem is showing that you can't do better than the obvious method (described in the previous paragraph) of first compressing and then encoding. I don't know whether anybody has proved this for Kolmogorov complexity and channel capacity, but it's a reasonable question to investigate.


Program Minimization Circuit Minimization is the problem to minimize the size of a given circuit. Is there anything similar for general programs?

In particular my question is -

Do there exist algorithms to minimize the # of instructions for a given program. I know it's an undecidable problem but I'm not looking for a solution that returns something optimal.

While one can apply preexisting compiler transformations to accomplish this, I'm looking for something where I don't have to define a set of very narrow transformations and algorithms to search for them beforehand.

Edit: The other question I have is whether one can have a calculus that is sound and complete that allows us to explore the whole space of such semantically equivalent programs or is that not possible.

There is a naive algorithm for programs with bounded-size inputs: enumerate all programs in order of increasing length (or execution time, which is a bounded function of the length). If you can prove that the program is equivalent to the original, stop; otherwise keep searching.

This algorithm is sound. In order for it to be complete, you need to be able to prove all rejected programs are not equivalent to the original. This is possible in finitary machine models, as long as you have a bound for the input size.

Note that when the program execution time depends on the input, there may not be an optimal solution. If you look for e.g. a worst-case bound, you'll very quickly run into undecidable equivalences when you quantify over all possible unbounded inputs, and into untractable problems if the inputs are bounded.

A decade ago, “Denali: A Goal-Directed Superoptimizer” by Rajeev Joshi , Greg Nelson and Keith Randall was able to find optimal programs of about 5 machine instructions. I haven't looked at more recent results.


Mutually exclusive replacement paths, an existing problem? A replacement path is a simple path allocated to an edge $e \in G$
that connects the endpoints of $e$ in $G \setminus \{e\}$.

The problem

An undirected graph $G$ is given and the task is to allocate a replacement path $P_e$ to each edge
$e \in G$ such that for any pair of edges $e_1$ and $e_2$ it holds:
if $e_2 \in P_{e_1}$ then $e_1 \not\in P_{e_2}$.
In words, no two edges use each other in their replacement path.
I call the paths $P_{e_1}$ and $P_{e_2}$ mutually exclusive.

The path length is not bounded and they can share edges. So any path allocation that satisfies the
mutual exclusion would be good.

Now the question: is there already any problem closely related to this?

One could reduce this problem to Maximum Independent Sets problem: a vertex for every $(e,P_e)$ and edges connecting conflicting pairs (i.e. pairs violating the ME). However, in order to get a polynomial size instance we need to restrict the model so that each edge gets a constant number of candidate paths.
However, this is not desired because the MIS instances seem to be NP-Hard (or not?).

I found a replacement path allocation for $_$ in a more general setting. Consider an edge $_1$ that uses edge $_2$ on its path. The allocation induces a dependency from $_1$ to $_2$. Mutual exclusion defined above corresponds to a cycle of 2 such dependencies. Now consider the more general setting: a cycle of $$ dependencies induced by a path allocation on $_$. Assume vertices are $0,…,−1$. On edges $,$, the path allocation $,+1,0,+1,$ induces cycles of dependencies no shorter than $$. In my application it means that $_$ can tolerate up to $−1$ edge failures (i.e. edge removal).

Same problem on hypercubes, published here:
''Local Fast Segment Rerouting on Hypercubes''

Further solutions were submitted recently. Will update soon.


Volume of elements mapped to the same codeword is $2^{H(X|\hat{X})}$ In this paper by Tishby, Pereira and Bialek they mention on page 4 in the Relevant quantization chapter the setting is the following; Given some signal space $X \sim p(x)$ and a quantized codebook $\hat{X}$. They seek a possibly stochastic mapping characterized by the pdf $p(\hat{x}|x)$ from every value $x \in X$ to a codeword $\hat{x} \in \hat{X}$.

This has made me wonder about the following:

1) They mention that the average volume of the elements of $X$ that are mapped to the same codeword is $2^{H(X|\hat{X})}$ - why is this?

2) They mention that for ease of exposition both $X$ and $\hat{X}$ are finite, so howcome $p(\hat{x}|x)$ is a p.d.f and not a p.m.f?

If I understand right what "average volume" means here, I don't think this is correct. For example, let's say you map $n$-bit strings (under uniform distribution) to $n$-bit strings as follows: Given an input $x$, if the first bit is 0, output $x$, and otherwise output "1".

The average volume would be $\frac{1}{2}(2^{n-1}+1)$, whereas the $2^{H(X|\hat{X})} = \sqrt{2^{n-1}}$.

The correct expression for the average volume should perhaps be the expectation $\sum p(\hat{x}) 2^{H(X|\hat{X}=\hat{x})}$.

You are right about p.d.f. vs p.m.f, this kind of mix-up of terminology is quite common (but shouldn't be).


Survey of transformations related to the use of SAT solvers I am starting to investigate the possibility of relying on a SAT solver to tackle an optimisation problem I'm interested in, and am currently looking for a survey that would feature examples of "clever" transformations to variants of SAT (i.e., transformations that result in a problem of reasonable size, since I'm not interested in proving hardness results but in actually solving the problem), approximately in the spirit of what can be found in the survey on cubic graphs by Greenlaw and Petreschi, if any comparison can be made between the two.

Has such a survey eluded me because it does not exist, or because I just missed it?

Not sure if that is what you're looking for but here is one: J.M. Silva, Practical applications of Boolean Satisfiability.


Natural graphs that are not scale free It is now a well known observation that many graphical structures that arise in natural settings tend to obey scale-free properties, such as the power law of degree distribution.

Are there any good example of natural graphs that are fairly random and not do not necessarily obey scale-free properties?

The connections between neurons do not form scale-free networks, I think. See e.g. Figure 1 on p.181 of http://www.indiana.edu/~cortex/Koetter_chapter_modified.pdf and observe that the vertex degrees only span a single order of magnitude.


Why must QMA complete problems be promise problems? I'm reading Watrous's excellent survey paper on paper on quantum complexity theory. In it he states that it would be surprising if a QMA -complete problem were found to have a vacuous promise (I.e. Be a language). Why is this so?

Does it have to do with the fact that the k-local Hamiltonian problem is a promise problem?

Also, this leads me to a related question: are there QMA-complete problems that aren't inherently "quantum" in nature?

On the second question: http://arxiv.org/abs/0905.4755v2 gives a classical QMA-complete eigenvalue problem related Markov chains.


Storing a bit vector in uninitialized memory and minimal space A well-known trick for storing bit vectors using uninitialized memory can allocate a bit vector of size $n$ in which all of the bits are set to $0$ by allocating $(2 n + 1)\lceil \lg n \rceil$ bits of memory and initializing only $\lceil \lg n \rceil$ of them. This representation supports setting and unsetting any bit in constant time.

This dates back to "Alfred Aho, John Hopcroft, and Jeffrey Ullman's 1974 book The Design and Analysis of Computer Algorithms . . . Chapter 2, exercise 2.12", "Jon Bentley's 1986 book Programming Pearls . . .Column 1, exercise 8; exercise 9 in the Second Edition", and "Preston Briggs and Linda Torczon's 1993 paper, 'An Efficient Representation for Sparse Sets'".

Dodis et al.'s "Changing Base without Losing Space" brings the space requirement down slightly to $\lceil (2 n + 1) \lg n \rceil + 1$ bits, though this algorithm requires the precomputation of $\Theta(\lg n)$ constants with $\Theta(\lg n)$ bits each.

How much space can be saved? Is there a representation of bit vectors in which

Bits can be set or unset in $O(1)$ time
Initializing a new bit vector of $0$s uses $o(n \lg n)$ bits of uninitialized memory and $O(\lg n)$ initialized memory

Yes, this can be done through bucketing. The representation in Briggs and Torczon can be used to store not just bits, but values associated with any set bits, by storing them next to the values in the dense array. For $k$-bit values, this leads to a total storage cost of $(2n+1)\lceil \lg n \rceil + kn$.

Now pick $k=\lceil \lg n \rceil$. Each $k$-bit value will represent a set of $\lceil \lg n \rceil$ contiguous bits in the bit array. We thus only need to track $\lceil n/\lceil \lg n \rceil \rceil$ of them with the dense and sparse arrays. This leads to a total cost of $\Theta(n)$ bits of storage, with $\Theta(\lg n)$ initialized bits.

Like the basic solution, this requires $O(1)$ operations on words of length $\Theta(\lg n)$ to set a single bit.


Proof for Upper Bound of Sum of Square Roots Problem In [1], Garey et al. identify what would later be known as the Sum of Square Roots Problem in the course of working out the NP-completeness of Euclidean TSP.

  Given integers $a_1, a_2, \ldots, a_n$ and $L$, determine if $\sqrt{a_1} + \sqrt{a_2} + \cdots + \sqrt{a_n} < L$

They observe that it is not even apparent that this problem is in NP since it is not clear what the minimum digits of precision are required in the computation of the square roots to sufficiently compare the sum to $L$. However, they do cite a best known upper bound of $O(m2^n)$ where $m$ is "the number of digits in the original symbolic expression". Unfortunately, this upper bound is attributed merely to a personal communication from A. M. Odlyzko.

  Does anyone have a proper reference to this upper bound? Or, in the absence of a published reference, a proof or proof sketch would also be helpful.

Note: I believe that this bound might be inferred as a consequence of more general results by Bernikel et. al. [2] from around 2000 on separation bounds for a larger class of arithmetic expressions. I'm mostly interested in more contemporaneous references (i.e.: what was known circa 1976) and/or proofs specialized to just the case of the sum of square roots.

Garey, Michael R., Ronald L. Graham, and David S. Johnson. "Some NP-complete geometric problems." Proceedings of the eighth annual ACM symposium on Theory of computing. ACM, 1976.
Burnikel, Christoph, et al. "A strong and easily computable separation bound for arithmetic expressions involving radicals." Algorithmica 27.1 (2000): 87-99.

Here is a rather sloppy proof sketch. Let $S = \sum_{i=1}^n \delta_i \sqrt{a_i}$ where $\delta_i \in \{\pm 1\}$. This is an algebraic number of degree at most $2^n$ and height at most $H = (max(a_i))^{n}$. Now it is easy to check if $S = 0$ (can be done even in $TC^0$ -- see this).If $S \neq 0$ then it is bounded away from $0$ by a quantity (because it is an algebraic number and hence is a non-zero root of a univariate polynomial) that is a function of the degree and height of the minimal polynomial of $S$. Unfortunately, the dependence on the degree is exponential in the number of square roots (and if the $a_i$'s are distinct primes, this degree bound is even tight, though that case of sign evaluation is easy to handle). The precision needed is hence exponential in the number of square roots, which is $2^n$-bits for $S$. It now suffices to truncate each of the $\sqrt{a_i}$ to say $2^{10n}$ bits to ensure the sign is guaranteed to be correct. This is easily done via polynomially many steps of Newton iteration). Now it is down to checking if the sum is positive, which is just addition and hence linear in the number of bits in the summands. Notice that this computation is in Polynomial time on a BSS machine. Also notice that we are not doing any computation directly with the minimal polynomial of $S$ itself, which could have huge coefficients and look ugly, we just use it to reason about the precision to which we need to truncate the square roots. For more details, check Tiwari's paper.


The significance of state complexity in automata and regular languages? I'm reading "Concatenation of Regular Languages and Descriptional Complexity" by Galina Jiraskova, 2009 on the state complexity resulting from concatenation of two regular languages ( by Galina Jiraskova), but I can't understand what the practical implications of state complexity would be. The first trivial thought that struck me was that higher complexity would require more time and space by the machine. Is this correct? Also are there any other places where state complexity is relevant and signinficant?

Edit:
The state complexity of a regular language is the smallest number of states in any
deterministic finite automaton (dfa) accepting the language. The nondeterministic
state complexity of a regular language is defined as the smallest number of states in any nondeterministic finite automaton (nfa) for the language.

State complexity is really about concise description of an object (in this case, a regular language), not about computational complexity.  The general topic is called "descriptional complexity" in the literature and draws its inspiration, in part, from the classic 1971 paper of Meyer and Fischer entitled "Economy of Expression by Automata, Grammars, and Formal Systems" (see http://people.csail.mit.edu/meyer/economy-of-description.pdf ).  This is still an active area, with a yearly conference (DCFS - Descriptional Complexity of Formal Systems).

As for applications, any place where your program essentially relies on a finite-state machine (e.g., parsers) it will be good to have this finite-state machine as small as possible.


Counting grid colorings that avoid certain features A $k$-coloring of an $m \times n$ grid is a function $C:[m] \times [n] \to [k]$. A broken rectangle in $C$ is a tuple $(i,i',j,j')$ satisfying $C(i,j) = C(i',j) = C(i,j') \ne C(i',j')$ -- that is, exactly three corners of the rectangle are the same color.

I'm interested in the following question:

  As a function of $k$, how many $k$-colorings exist (for grids of any size) that avoid duplicate rows, duplicate columns, and broken rectangles?

So far I know that the answer is finite, and the best upper bound I can prove is $k^{(1.5 k!)^2}$ (see below).

I'll also just point out that this is a different question than the one talked about by Gasarch frequently on his blog (and in this paper). He wants to avoid all monochromatic rectangles, whereas I don't mind monochromatic rectangles, it's just the "broken" ones that I want to avoid.

What is the motivation? In cryptography, we consider the problem of Alice (who has $x$) and Bob (who has $y$) both learning $f(x,y)$ for an agreed-upon function $f$, in such a way that they learn no more than $f(x,y)$. You can associate $f$ naturally with a 2-dimensional table, hence, a grid coloring. There are characterizations for this kind of problem of the following form (but with different notation): "$f$ has some cryptographically interesting property if and only if $f$ contains a broken rectangle." For examples, see Kilian91 and BeimelMalkinMicali99.

So this problem has come up in some setting of cryptography that I was investigating. For my purposes, it was enough to know that there are a finite number of grid colorings that avoid broken rectangles and duplicate rows/columns. But I thought the combinatorial problem itself is interesting and I believe better bounds should be possible.

The best bound I can prove: Define $R(2)=3$ and $R(k) = k \cdot R(k-1)$; hence $R(k) = 1.5 k!$. First, one can prove that if $C$ is a $k$ coloring with at least $R(k)$ rows, then it either has a duplicate row or a broken rectangle. Symmetrically, one can show the same thing with respect to columns. (The proof is pretty basic, following from the pigeonhole principle on the # of colors.) From this, we know that the colorings we care about all have dimensions smaller than $R(k) \times R(k)$, and we can get a very loose upper bound of $k^{R(k)^2}$ such colorings.

I think this can be improved in two ways: First, I think the optimal value of $R(k)$ is $2^{k-1}+1$. Below is a (recursively defined) family of colorings, where $C_k$ is a $k$-coloring of size $2^{k-1} \times 2^{k-1}$ that avoids these forbidden features:

$
     \qquad
     C_1 = [1];
        \qquad
     C_k = \left[ \begin{array}{ccc|ccc}
                k & \cdots & k & \\
                \vdots & \ddots & \vdots &  & C_{k-1} \\
                k & \cdots & k & \\
                    \hline
                 & & & k & \cdots & k \\
                 & C_{k-1} & & \vdots & \ddots & \vdots \\
                 & & & k & \cdots & k
            \end{array} \right].
$

I believe these to be the largest $k$-colorings that avoid these forbidden structures.

Second, even if one could improve the bound on $R(k)$ described above, we still have the fact that $k^{R(k)^2}$ is a very coarse bound for the total number of colorings. This counts all possible $R(k) \times R(k)$ grid colorings, of which a large portion presumably have the forbidden features.

If you want bounds for a fixed $k$ (rather than an asymptotic expression/formula that works for all $k$), one approach might be to use random sampling: repeatedly choose a random coloring, check whether it meets your criteria, and count how many of the trials were successful.  This gives you an estimate of the fraction of colorings that meet your criteria.  This can be converted into a rough estimate of the total number of colors that meet your criteria (just multiply by $k^{mn}$).

You can then use a Chernoff bound to get upper and lower bounds on the number of colorings that meet your criteria, where these bounds hold with probability $\ge 1-2^{-100}$ (taken over the random trials).  In other words, you would have to be extremely unlucky in your choice of random trials for those bounds to be wrong.


Is there any online lecture series that covers "Computational Complexity: A Modern Approach"? I am trying to cover the Computational Complexity :A Modern approach by Boaz Borak and Sanjeev Arora. Are there any nice lecture series that cover this material ?

These courses by Prof. Ryan O'Donnell are excellent:
https://www.youtube.com/watch?v=pRnnEOAQZF8&list=PLm3J0oaFux3b8Gg1DdaJOzYNsaXYLAOKH
https://www.youtube.com/watch?v=RxhpiYKFQd8&list=PLm3J0oaFux3YL5vLXpzOyJiLtqLp6dCW2
They cover most relevant material.


Research papers regarding disinterval analysis I'm trying to implement a disinterval analysis similiar to what is described in Clousot: Static Contract Checking with Abstract Interpretation (under section 5.2) - and I'm trying to find some papers describing the abstract operators (+, -, join, meet - etc) - however I have been unable to dig these up.

Are any of you aware of such papers and could you please link me to them?

You could give a shot at Ermedahl & Sjodin: Interval analysis of C-variables using Abstract Interpretation.


How does one extend local checkability to quantum complexity classes? How does one extend local checkability to quantum complexity classes like BQP? Or are quantum algortihms inherently holistic?

A preliminary guess at what it is you're looking for

I will give a preliminary answer, in the hopes that it might prompt you to elaborate on what promises to be quite a good question. I will assume you're referring to an idea along the lines of page 4 of [Arora+Impagliazzo+Vazirani 1993], which introduces the concept of "local checkability"  as follows:

  [...] we identify a general principle, the principle of local checkability, which appears to us to be at the root of the above-mentioned non-relativizing results [e.g. IP = PSPACE and MIP = NEXPTIME]. While this principle can be formulated in several ways, all of them express the fact that computation is a very local process, and hence checking the correctness of a computation is simpler than performing the computation itself.1 We show that "local checkability" is a fact which does not relativize.

  [...]

  1 This fact is also at the root of the Cook-Levin Theorem, and a preliminary version of this paper identified "local checkability" with the term "Cook-Levin Theorem".

Without going further into depth (awaiting a more precise description of the property which interests you), quantum computation does admit a notion of local checkability.

In the standard discrete-time models of quantum computation, all transformations are performed on small sets of bits: in this sense, computations are certainly local. So quantum computation is not any more holistic in principle than classical computation in this specific sense.

Local checkability vs. local performability

One might fear that the ability to perform local checks is undermined by the phenomenon of superposition, and in particular entanglement. If we have an operation O, which acts on a system A, how can we verify that the state of A after the operation corresponds correctly to the effect of O on the state of A before the operation, if the state of A cannot be isolated in the first place?

If we bear in mind that randomized computation is also subject to this complication — of systems not being independent of their environments — we can realise that perhaps entanglement does not cause any necessary "holisticness" to quantum computation.
As usual, entanglement has in common with probabilistic correlations the fact that they are not product distributions; so merely failing to be a product distribution cannot be something which prevents local checkability of a quantum state, if it does not also prevent probability distributions from being locally checkable. Absent this particular spectre, we may hope that there could be pertinent techniques in the quantum regime.
Of course, entanglement is more than just correlation of randomized events, because checkable properties of random correlations can be tested (with imperfect soundness) simply by sampling from the distribution, whereas this is not true in general of quantum states. Other techniques must be necessary.

The hint is provided by Arora, Impagliazzo, and Vazirani themselves in their invoking the Cook-Levin Theorem. I would suggest that we make reference to the techniques used to prove the QMA-completeness of LOCAL-HAMILTONIAN, which is the quantum analogue of the Cook-Levin Theorem. One might conjecture that any model of computation which is limited to locally performed operations, and has an analogue of the Cook-Levin theorem (i.e. complete problems for the class of constraint satisfaction problems admitting efficiently checkable certificates), is similarly subject to local checkability in some sense. A formal exploration of this idea might be an interesting subject in its own right, in the theory of computation.

Quantum local checkability via LOCAL-HAMILTONIAN

Not at all unlike the reduction of CIRCUIT-SAT to SAT, the classic proof of the NP-completeness of LOCAL-HAMILTONIAN involves testing whether or not a state satisfies local constraints imposed by simulating the evolution of a circuit.

In quantum information theory, constraints are generally presented as positive semi-definite "observable" operators, and satisfaction of all constraints amounts to the state being a ground-state for all such operators simultaneously. These "observables" correspond to events which can be measured and sampled using standard techniques.
In quantum computation (as with probability distributions), constraint testing has imperfect soundness error, but soundness can at least be tested statistically provided many copies of the distribution.

I'll elaborate later; but the specific constraints which are tested for in the proof of QMA-completeness of LOCAL-HAMILTONIAN correspond precisely to whether the state of a system A before some unitary operation, corresponds to the state of the system A after the unitary operation, this being exactly what local checkability represents.

On this basis, provided that this is what you mean, I would say that quantum computation admits a notion of local checkability.


Bipartite vertex cover with a Very Important Vertex I know that I can find the minimum vertex cover of a bipartite graph by first finding the maximum matching and then using Konig's Theorem to turn this matching into a vertex cover of the same order.

The result obtained is only one of what could be many valid vertex covers. In the following graph, {A,B}, {C,D}, and {B,C} are all valid covers. Applying the Konig method yields the cover {A,B}.*

(A)=====(C)
       /
     /
   /
(B)=====(D)

How would you check for the existence of a minimum vertex cover that includes a given important vertex, say, vertex D?

My first guess is to flip the graph and find another minimum vertex cover. In the above case, this would yield {C,D}. If neither solution contains the important vertex, it's not part of any minimum cover.  However, I haven't been able to prove this to myself.

*A little elaboration: edge AC and BD form the matching. In the algorithm described above, you start by treating the graph asymmetrically, labeling the sides L (left) and R (right). Initially, all L and none of the R vertices are part of the vertex cover. Now build a new set T of vertices by traversing according to the following rule: Start at the exposed vertices (not part of any matching) on the left side, travel right along all unmatched edges, then travel left along all matched edges, continuing back and forth until path termination. All visited vertices are added to set T.  Set T is subtracted from L and added to R to produce the vertex cover solution. In the example graph, there is NO traversal, since there are no exposed vertices on the left side.

Just delete D together with its indicent edges and check if you can find a vertex cover for the remaining graph that is one smaller than that for the whole graph. If so, you can add D to it to get a minimum vertex cover that includes D; otherwise, there is no such vertex cover. (This doesn't depend on the bipartiteness at all.)


Hyperplanes not intersecting points on a cube Consider the set of points in $\mathbb{R}^n$ with coordinates in $\{-1, 0, 1\}$. Find a hyperplane passing through the origin that contains no points in the set besides the origin.

This is simple if we don't give any constraints on the hyperplane. Even if define the hyperplane by a normal vector in $\mathbb{Z}^n$, it is simple. However, what if we require every coordinate of the normal vector to be an integer bounded in absolute value by some polynomial in $n$? Does such a hyperplane exist?

No. Let the normal vector be $(a_1,\ldots, a_n)$. If these numbers are $poly(n)$ small integers, then there is an $I$ and $J$ such that $\sum_{i\in I} a_i=\sum_{j\in J} a_j$ by the pigeon hole principle. But then we have $\sum_{i=1}^n \varepsilon_i a_i=0$ for some $\varepsilon \in \{-1,0,1\}^n$.


Social choice, arrow's theorem and open problems ? Last few months I started to lecture myself on social choice, arrow's theorem and related results.

After reading about the seminal results, I asked myself about what happens with partial order preferences, the answer is in the paper of Pini et al.: Aggregating partially ordered preferences: impossibility and possibility results. Then, I wondered if it is possible of finding a characterization of admissible social choice functions. And again someone did it (Complete Characterization of Functions Satisfying the Conditions of Arrow’s Theorem by Mossel and Tamuz). I won't give a full list, but any of the problems related to social choice I can think of where all solved in the last 5 years :(

So, do you know if there exists a survey on what was done recently in the field and what was not done?

Another question is: are you aware of complexity and social choice related problems (for instance the complexity of finding the largest subset of users that are compatible for at least one social choice function, or this kind of question).

Your question is very well timed, because the most recent issue of the CACM has an article      that does exactly this: http://cacm.acm.org/magazines/2010/11/100640-using-complexity-to-protect-elections/fulltext

In brief, there's a lot of work by Conitzer, Tovey and others on the actual hardness, both worst-case and under distributional assumptions, of cracking voting mechanisms that are in principle breakable via Arrow's theorem.


Optimal insertion times in insertion-only data structures beyond Bentley-Saxe The Bentley-Saxe trick allows us to go from a static decomposable problem to a problem admitting insertions, where the insertion time is off the optimal time by a factor of $\log n$.

Is this tight ? Or alternately, is there a more restricted subclass for which you can get insertion time $P(n)/n$ (amortized or worst-case) even if $P(n) = O(n\log n)$ ? Here, $P(n)$ is the time to compute the result statically.

Think about your question in reverse: suppose you have a dynamic data structure for some problem — does that imply that you can solve it statically, faster by a log? Why should it? And in fact it is not true.

Consider range counting in one-dimensional intervals, in a comparison model of computation. That is, the data is a set $S$ of numbers, the query is an interval $[\ell,r]$, and the answer to a query is the size of $S\cap[\ell,r]$. Statically, you can solve it in $O(\log n)$ query time by storing $S$ as a sorted array and using binary search, in preprocessing time $P(n)=\Theta(n\log n)$. Dynamically, you can still solve it in $O(\log n)$ query time by using balanced binary search trees, with insertion time $O(\log n)=O(P(n)/n)$.


Is Biological Computation a theme covered by the Theoretical Computer Science? I want to say computation realized by biological systems themselves. I'm not talking about bio-inspired algorithms, or applications in computation using living systems. This question is more about an empirical theory of computation in the natural world than applications of biological systems in the industry of the computation.

Reference:
MITCHELL, Melanie. Biological Computation.

Yes there is some overlap, for instance the conference Unconventional Computation and Natural Computation (UCNC) covers theoretical computer science topics related to biological computation.

From the call for papers, UCNC topics of interest include (but are not restricted to):

  Molecular computing
  Quantum computing
  Optical computing
  Chaos computing
  Physarum computing
  Collision-based computing
  Self-assembling and self-organizing systems
  Super-Turing computation
  Cellular automata
  Neural computation
  Evolutionary computation
  Swarm intelligence
  Ant algorithms
  Artificial immune systems
  Artificial life
  Membrane computing
  Amorphous computing
  Computational systems biology
  Computational neuroscience
  Synthetic biology
  Cellular (in-vivo) computing


Original reference for Huffman shaped Merge Sort? What is the first publication of the concept of optimizing merge sort by

identifying sequences of consecutive positions in increasing orders (aka runs) in linear time; then
repeatedly merging the two shortest such sequences and adding the result of this merging to the list of sorted fragments.

In some of my publications (e.g. http://barbay.cl/publications.html#STACS2009, http://barbay.cl/publications.html#TCS2013) I used this trick to sort faster and to generate a compressed data structure for permutation.

It seems that this trick was introduced before, just in the context of sorting faster, but neither me nor my student have been able to find back the reference?

I found the result hidden in an obscure 4p technical report: I share my results here in case others are interested.

Knuth mentions runs in his description of "natural merge sort" (page 160 of the tome 3 of the 3rd edition), but he analyzes its complexity only on average (which yields n/2 runs), not in function of the number ρ of runs
in 1985, Mannila proved that Natural Mergesort takes time within O(n(1+lg(r+1))) to sort n elements forming r runs.
in 1996, Tadao Takaoka (http://dblp.uni-trier.de/pers/hd/t/Takaoka:Tadao) introduced the notion of the entropy of the distribution of the sizes (n1,…,nρ) of the runs in an tech report  4 pages article titled "Minimal MergeSort", and proved a complexity of $n(1+2H(n1,…,nρ))$ comparisons
in 2009, the technique was presented at the symposium Mathematical Fundation of Computer Science (along with results on sorting, shortest paths and minimum spanning trees).
in 2010, it was published  in the  journal of Information Processing under the title "Entropy as Computational Complexity", with an added co-author, Yuji Nakagawa (https://www.semanticscholar.org/author/Yuji-Nakagawa/2219943).

I join the bibtex references below.

@TechReport{1997-TR-MinimalMergesort-Takaoka,
  author =   {Tadao Takaoka},
  title =    {Minimal Mergesort},
  institution =  {University of Canterbury},
  year =     1997,
  note =     {http://ir.canterbury.ac.nz/handle/10092/9676, last accessed [2016-08-23 Tue]},
  abstract =     {We present a new adaptive sorting algorithm, called minimal merge sort, which merges the ascending runs in the input list from shorter to longer, that is, merging the shortest two lists each time. We show that this algorithm is optimal with respect to the new measure of presortedness, called entropy.}
}

@InProceedings{2009-Chapter-PartialSolutionAndEntropy-Takaoka,
author="Takaoka, Tadao",
editor="Kr{\'a}lovi{\v{c}}, Rastislav
and Niwi{\'{n}}ski, Damian",
title="Partial Solution and Entropy",
bookTitle="Mathematical Foundations of Computer Science 2009: 34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings",
year="2009",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="700--711",
isbn="978-3-642-03816-7",
doi="10.1007/978-3-642-03816-7_59",
url="http://dx.doi.org/10.1007/978-3-642-03816-7_59",
abstract = {If the given problem instance is partially solved, we want to minimize our effort to solve the problem using that information. In this paper we introduce the measure of entropy H(S) for uncertainty in partially solved input data S(X) = (X 1, ..., X k ), where X is the entire data set, and each X i is already solved. We use the entropy measure to analyze three example problems, sorting, shortest paths and minimum spanning trees. For sorting X i is an ascending run, and for shortest paths, X i is an acyclic part in the given graph. For minimum spanning trees, X i is interpreted as a partially obtained minimum spanning tree for a subgraph. The entropy measure, H(S), is defined by regarding p i  = |X i |/|X| as a probability measure, that is, H(S)=−nΣki=1pilogpi, where n=Σki=1|Xi|. Then we show that we can sort the input data S(X) in O(H(S)) time, and solve the shortest path problem in O(m + H(S)) time where m is the number of edges of the graph. Finally we show that the minimum spanning tree is computed in O(m + H(S)) time.}
}

@article{2010-JIP-EntropyAsComputationalComplexity-TakaokaNakagawa,
  author    = {Tadao Takaoka and
               Yuji Nakagawa},
  title     = {Entropy as Computational Complexity},
  journal   = jip,
  volume    = {18},
  pages     = {227--241},
  year      = {2010},
  url       = {http://dx.doi.org/10.2197/ipsjjip.18.227},
  doi       = {10.2197/ipsjjip.18.227},
  timestamp = {Wed, 14 Sep 2011 13:30:52 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jip/TakaokaN10},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  abstract = {If the given problem instance is partially solved, we want to minimize our effort to solve the problem using that information. In this paper we introduce the measure of entropy, H (S), for uncertainty in partially solved input data S (X) = (X1, . . . , Xk), where X is the entire data set, and each Xi is already solved. We propose a generic algorithm that merges Xi's repeatedly, and finishes when k becomes 1. We use the entropy measure to analyze three example problems, sorting, shortest paths and minimum spanning trees. For sorting Xi is an ascending run, and for minimum spanning trees, Xi is interpreted as a partially obtained minimum spanning tree for a subgraph. For shortest paths, Xi is an acyclic part in the given graph. When k is small, the graph can be regarded as nearly acyclic. The entropy measure, H (S), is defined by regarding pi = ¦Xi¦/¦X¦ as a probability measure, that is, H (S) = -n (p1 log p1 + . . . + pk log pk), where n = ¦X1¦ + . . . + ¦Xk¦. We show that we can sort the input data S (X) in O (H (S)) time, and that we can complete the minimum cost spanning tree in O (m + H (S)) time, where m in the number of edges. Then we solve the shortest path problem in O (m + H (S)) time. Finally we define dual entropy on the partitioning process, whereby we give the time bounds on a generic quicksort and the shortest path problem for another kind of nearly acyclic graphs.}
}


What videos should everybody watch? Stanford University now has a Youtube channel, with free access to HD video of full courses on everything from dynamical systems to quantum entanglement.  More conferences and workshops are videotaping their talks.  What are videos online that you think everyone should know about?

I'll seed this with a few answers to presentations that are mostly expository, but what I'm hoping might happen is that this community wiki could turn into a resource to share excellent presentations of new research, as well as a place to learn (or reinforce) background in an unfamiliar area.

Timothy Gowers has a set of videos on Computational Complexity and Quantum Computation online.


Representation as sum of unit fractions: primitive recursive? Consider the following ternary relation $R\subseteq\mathbb{N}^3$:

  $(p,q,m)\in R$ iff $p,q>0$ and there is a set $S\subseteq \{\frac{1}{n}:n\in\mathbb{N}, n\geq 1\}$ such that $|S|=m$ and $\frac{p}{q}=\sum_{s\in S} s$.

Is $R$ primitive recursive, recursive, or recursively enumerable?

Consider $(p,q,m)\in R_k$ iff there is a set $S\subseteq \{\frac{1}{n}:n\in\mathbb{N}, n> k\}$ such that $|S|=m$ and $\frac{p}{q}=\sum_{s\in S} s$, so $R=R_0$.

It is easy to see that $(p,q,m)\in R_k$ iff there is an $k<\ell\le \frac {qm}p$ such that $(p\ell-q,q\ell,m-1)\in R_\ell$.


Simple question about pseudorandom generator I am stuck on the following question related to pseudorandom generator and any help would be appreciated.

  Let $G:\{0,1\}^k \to \{0,1\}^{k+1}$ be a pseudorandom generator. Define $G':\{0,1\}^{2k}  \to \{0,1\}^{2k+2}$ by $G'(x_1x_2)=G(x_1)G(x_2)$ where $x_1, x_2 \in \{0,1\}^k$.

  Prove that $G'$ is not a pseudorandom generator in general.

I don't think it is necessary (and feasible) to find a counter-example $G'$ since it requires us to find a pseudorandom generator $G$, (which means we will have proved the existence of pseudorandom if we can find such $G$) so normally how can we tackle this kind of problem?

Thank you very much in advance. :)

I assume you mean a cryptographic PRG.

Let's assume on the contrary that the $G'$ is not secure. So let $A$ be a probabilistic Turing machine that distinguishes the output of $G'$ from uniformly random bits.

Let $x_1,x_2$ be $k$ bit random strings, and let $z_1,z_2$ be $k+1$ bit random strings.

We have that $A$ distinguishes the distribution of strings $D_0 : G(x_1)G(x_2)$ and
$D_2: z_1z_2$.

Consider now the hybrid distribution of strings given by $D_1: G(x_1)z_2$.

By the triangle inequality $A$ also distinguishes between either $D_0$ and $D_1$ or between $D_1$ and $D_2$.

Assume without loss of generality that  $A$ distinguishes between $D_0$ and $D_1$.
Then we can break $G$ as follows. On input $y$, pick uniformly random $k$ bit string $x_1$ and give the string $G(x_1)y$ to $A$.


Mergeable Exact Order Statistics Data Structure Given $n$ sets of integers $S_1, S_2, \cdots, S_n$, it is guaranteed that
$$
x < y, \text{ for } \forall x \in S_i \text{ and } \forall y \in S_{i+1}
$$
and let's denote this relationship as $S_i < S_{i+1}$.
For each set, we want to build a data structure that supports the following two operations:

$rank(x)$: Return the rank of $x$ in $S_i$, where $x \in S_i$;
$merge(A, B)$: Let $A$ and $B$ be the structures built on two sets $S_i$ and $S_j$ with $S_i < S_j$. Merge $A$ and $B$.

One implementation is to use an order statistics tree (such as AVL tree, red-black tree), which is able to support $\mathcal{O}(\log n)$ rank operation, but fails(right?) to provide efficient (i.e., logarithmic or constant) merge operation. A linked-list implementation, however, has poor rank performance. A skip-list may be employed, but its worst time complexity is bad.

Can anyone provide a reference about such a structure or proved lower bounds for a structure that supports these two operations at the same time? Any idea is appreciated. Thanks!

Most balanced trees that have logarithmic-time insert and delete also have logarithmic time $merge$. This includes AVL trees, red-black trees, and B trees.

You can see this question on Stack Overflow for several references results. They include a paper on CGAL (red-black), a reference to the OCaml standard library (AVL), as well as the red-black tree chapter of CLRS's Introduction to Algorithms.

When I was learning about this topic, I was happy to find that $merge$ is actually usually a simpler operation than $insert$ and $delete$.


Persistant bag/set with direct access to known elements I'm looking for a bag or set data structure that will allow for the following operations:

Add an element to the set, and get a "pointer" to that element.
Add :: mystructure a -> a -> (mystructure a, myptr a)

Remove an element for which I have a "pointer".
Remove :: mystructure a -> myptr a -> mystructure a

Enumerate all the elements in the set.
Enumerate :: mystructure a -> [a]

Note that I don't really care about duplicate values (the values I enter are already unique), nor the order of elements.
A very simple implementation for this structure would be to use a doubly-linked list, with the standard Add returning a pointer to the newly created list node, the standard Remove removing such a node from the list, and Enumerate simply traversing the list.
However, I need the structure to be immutable/persistant (i.e. the Add and Remove operations don't modify the original data structure). Ideally, the operations would still be O(1), like with a doubly-linked list. I think finger trees could be used for this, but I don't know them well.

You can solve this with a dictionary, using myptr a = a.

You can get $O(\lg n)$ add and remove in an immutable data structure by using a balanced binary search tree. Enumerate will take $O(n)$ time, but the $i$th element can be made available in $O(i)$ time, so your enumerate result can keep up with any consumption of it.

"Confluently Persistent Tries for Efficient Version Control", by Erik D. Demaine, Stefan Langerman, and Eric Price provides a dictionary that is fully persistent, but not immutable. With it, you can get the same bound on enumerate, and a $O(\lg \lg n)$ bound on add and remove.


Topological sort with constraints on the relative difference between the vertex labels A topological sort of a graph $G(V,E)$ consisting of $n$ vertices assigns a label $L(v_x)$ to a vertex $v_x$ where $L$ is defined as $L:V \rightarrow \{1,\dots,n\}$.

Let additional constraints over the labels that the topological sort will assign to be defined as follows.  For every vertex pair $(v_x,v_y)$ let $d(v_x,v_y)$ be the permitted difference between $L(v_x)$ and $L(v_y)$ i.e. $L(v_x) - L(v_y) \leq d(v_x,v_y)$. $d$ is defined as $d:V \times V \rightarrow \{0,\dots,n-1\}$. A solution to this variant of Constrained Topological Sort (CTS) will compute a tolopological sort satisfying the difference constraints for all possible pairs of vertices in $G$.

Is a linear time solution to CTS possible?
Is there an existing work where I can refer to?

The problem is $\mathsf{NP}$-hard. See [GT41] DIRECTED BANDWIDTH in Garey and Johnson.


Maximal Clique partition of vertices with smallest number of cut edges I am given a simple undirected graph $G(V, E)$. I want to partition $V$ into $b$ Maximal cliques: $\{C_1, C_2, ..., C_b\}$ such that the number of edges that cut across two cliques is the minimum. $b$ is arbitrary i.e. there is no restriction on $b$.

I think the decision version of this problem is NP-Complete. It may be reduced to a weighted independent set problem. My question is:

Is there any known approximate algorithm for this problem?

Thank you for your answers!

This problem is the Cluster Edge Deletion problem.

  Given a graph $G = (V,E)$ and an integer, can we delete at most $k$ edges $F \subseteq E$ such that $G-F$ is a cluster graph?

A cluster graph here is a graph whose connected components are cliques.

The approximability of Cluster (Edge) Deletion, was studied by Shamir, Sharan, and Tsur (Cluster graph modification problems. Discrete Applied Mathematics, 144(1):173–182, 2004).  They show that the problem is NP-hard to approximate within a constant factor:

  Theorem 12. There is some constant $\epsilon > 0$ such that it is NP-hard to approximate Cluster Deletion to within a factor of $1 + \epsilon$.


What is the role of predicativity in inductive definitions in type theory? We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A := \mu F$ to be the "inductive definition" of $A$. Moreover, monotonicity of $F$ allows us to reason with the "principle of induction" to determine when a set contains $A$ (i.e. when a property universally holds on $A$).

In Coq this corresponds to writing an $\mathtt{Inductive}$ definition of $A$ with explicit introduction terms. While this definition denotes a particular function $F$, that function is not necessarily monotonic. Coq therefore employs some syntactic checks to guarantee the "well-formedness" of the definition. To some approximation, it rejects occurrences of $A$ in negative positions in the types of the introduction terms.

(If my understanding up to this point is flawed, please correct me!)

First, some questions in the context of Coq:

1) Does the syntactic check in Coq merely serve to ensure that the definition of $A$ is predicative? (If so, is impredicativity the only way in which the definition would be ill-defined?) Or is it checking for monotonicity? (Correspondingly, is non-monotonicity what might kill it?)

2) Does such a negative occurrence of $A$ necessarily imply that $A$'s definition is impredicative/non-monotonic? Or is Coq simply unable to verify that it's well-defined in that case?

And more generally:

3) What is the relation between predicativity of an inductive definition and monotonicity of that definition's generating function? Are they two sides of the same coin? Are they unrelated? Informally, which one matters more?

No, in this case, predicativity and monotonicity are not closely related.

The positivity check in Coq/Adga serves to ensure that you are taking the least fixed point of a monotonic thing, roughly.

Here's how to think of inductive types in terms of lattices and monotone operators. Recall that the Knaster-Tarski theorem says that on a complete lattice $L$, every monotone operator $f : L \to L$ has a least fixed point $\mu(f)$. Next, we can think of the types in a type theory as forming a lattice under provability. That is, type $S$ is below $T$ if the truth of $S$ entails that of $T$. Now, what we would like to do is to take a monotone operator $F$ on types, and use Knaster-Tarski to get out an interpretation of the least fixed point of this operator $\mu(F)$.

However, types in type theory aren't just a lattice: they form a category. That is, given two types $S$ and $T$, there are potentially many ways for $S$ to be below $T$, with one way for each proof $e : S \to T$. So a type operator $F$ also has to do something sensible on these proofs. The appropriate generalization of monotonicity is functoriality. That is, we want $F$ to have an operator on types, and also to have an action on proofs, such that if $e : S \to T$, then $F(e) : F(S) \to F(T)$.

Now, functoriality is preserved by sums and products (ie., if $F$ and $G$ are endofunctors on types, then $F+G$ and $F\times G$ (acting pointwise) are also functors on types (assuming we have sums and products in our algebra of types). However, it is not preserved by the function space, since the exponential bifunctor $F \to G$ is contravariant in its left argument. So when you write an inductive type definition, you are defining a functor to take a least fixed point of. To ensure that it is indeed a functor, you need to rule out occurences of the recursive parameter on the left-hand-side of function spaces --- hence the positivity check.

Impredicativity (in the sense of System F) is generally avoided, because it is a principle that forces you to choose between classical logic and set-theoretic models. You can't interpret types as sets in classical set theory if you have F-style indexing. (See Reynolds' famous "Polymorphism is Not Set-Theoretic".)

Categorically, F-style impredicativity says that the category of types and terms forms a small complete category (that is, homs and objects are both sets, and limits of all small diagrams exist). Classically this forces a category to be a poset.   Many constructivists are constructive because they want their theorems to hold in more systems than just classical logic, and so they don't want to prove anything that would be classically false. Hence they are leery of impredicative polymorphism.

However, polymorphism lets you say many conditions that are classically "large" internally to your type theory -- and positivity is one of them! A type operator $F$ is functorial, if you can produce a polymorphic term:

$$
\mathsf{Fmap} : \forall \alpha, \beta.\; (\alpha \to \beta) \to (F(\alpha) \to F(\beta))
$$

See how this corresponds to functoriality? IMO, this would be a very nice option to have in Coq, since it would let you do generic programming much more easily. The syntactic nature of the positivity check is a big hindrance to generic programming, and I would be happy to trade the possibility of classical axioms for more flexible functional programs.

EDIT: The question you are asking about the difference between Prop and Set arises from the fact that the Coq developers want to permit you think about Coq theorems in naive set-theoretic terms if you want, without forcing you to do so. Technically, they split Prop and Set, and then prohibit sets from depending on the computational content of Prop.

So you can interpret Prop as truth values in ZFC, which are the booleans true and false. In this world, all proofs of propositions are equal, and so obviously you should not be able to branch on the proof of a proposition. So the prohibition on sets depending on the computational content of proofs of Prop is totally sensible. Furthermore, the 2-element boolean lattice is obviously a complete lattice, so it should support impredicative indexing, since arbitrary set-valued meets exist. The predicativity restriction on Sets arises from the fact (mentioned above) that F-style indexing is degenerate in classical set-theoretic models.

Coq has other models (it's constructive logic!) but the point is that off the shelf it will never prove anything that a classical mathematician would be puzzled by.


Speedup from algorithmic advances vs. hardware I recall seeing a study or article a while ago claiming that most of the speedup seen in computer programs over the last several decades is from better algorithms rather than faster hardware. Does anyone know the study or article?

this is an unintentionally complex question. this idea that software gains have outpaced hardware gains is apparently rooted in a real govt report but (as your question indicates) possibly approaching minor urban legend status due to being misunderstood or misinterpreted. the summary/sound-bite headlines do not really match the actual point being made in the report.

see [1] or [2] which states

  A report by an independent group of science and technology advisers to the White House, published last December, cited research showing that performance gains in doing computing tasks that result from improvements in software algorithms often far outpace the gains attributable to faster processors.
  ...
  But the White House advisory report cited research, including a study of progress over a 15-year span on a benchmark production-planning task. Over that time, the speed of completing the calculations improved by a factor of 43 million. Of the total, a factor of roughly 1,000 was attributable to faster processor speeds, according to the research by Martin Grotschel, a German scientist and mathematician. Yet a factor of 43,000 was due to improvements in the efficiency of software algorithms.

but the issue of software vs hardware is very far from this one dimensional simplification, much more complex, and Lohrs blog has it more accurate— software and hardware form a sort of yin-yang symbiotic fusion and both have advanced very significantly, even staggeringly over the decades.

caveat/fine print: one cannot take individual gains in particular software algorithms, which in some cases have been very substantial, and generalize that across all algorithms.

the actual quote from the report is on page 71:

  Even more remarkable – and even less widely understood – is that in many areas,
  performance gains due to improvements in algorithms have vastly exceeded even the dramatic performance gains due to increased processor speed. The algorithms that we use today for speech recognition, for natural language translation, for chess playing, for logistics planning, have evolved remarkably in the past decade. It’s difficult to quantify the improvement, though, because it is as much in the realm of quality as of execution time.

so this government report is highly researched and polished, the basic claim of massive gains due to theoretical software advances in some areas is correct, and is promoting (theoretical/algorithmic) research partly on that basis.

however there are several other new/recent fundamental/massive phenomena/trends/shifts in recent years or what Intels Grove calls "inflection points" that are occuring in hardware vs software design. aka "gamechangers":

the rise of "Exascale" supercomputing may not be as readily achieved as "Petascale" due to hardware scaling constraints
clock speeds, a main drive of prior speed gains, have plateaued (partly due to heat/cooling constraints)
hardware is undergoing a massive shift toward less compute intensive, more energy efficient devices eg mobile, datacenters/virtualization/cloud etc
improving parallelism in software and hardware (eg "multicore") is therefore becoming more critical for performance improvements (where theory has a lot to say about how to parallelize algorithms)

[1] skeptic.se, does progress in algorithms beat progress in hardware

[2] Software progress beats Moores law NYT blog by Lohr

[3] REPORT TO THE PRESIDENT
AND CONGRESS
DESIGNING A DIGITAL FUTURE:
FEDERALLY FUNDED RESEARCH
AND DEVELOPMENT IN
NETWORKING AND INFORMATION
TECHNOLOGY Dec 2010


How to benchmark #2-SAT counting algorithms? Are there any libraries of #2-SAT instances that are hard to solve with state-of-the-art exact solvers (sharpSAT, cachet, ...)?

Alternatively: are there practical ways to generate hard #2-SAT instances?

I have only been able to find benchmark instances for #k-SAT for $k\ge3$.

I am not aware of any collections of 2CNF benchmark instances.

However, one practical way of constructing #2-SAT instances that are provably hard for state-of-the-art model counters is as follows: generate a $d$-regular expander for some constant $d$ (so in practice a random $d$-regular graph), then, as holf suggested, construct the 2CNF-formula that has for every edge $uv$ the clause $x_u\lor x_v$. By this paper

https://arxiv.org/abs/1411.1995

of Bova et al, the resulting formulas do not have small circuits of the form that is called DNNF in knowledge compilation, as subfield of artificial intelligence. Then by connections between DPLL-based model counting and DNNF that can be found in

Huang, Jinbo, and Adnan Darwiche. "DPLL with a trace: From SAT to knowledge compilation." IJCAI. Vol. 5. 2005.

it follows that all DPLL-based model counters will take exponential time to solve the above instances. Since all exact model counters that I am aware of (except for this knowledge compiler that can also used for counting http://www.cril.univ-artois.fr/KC/eadt.html ) are based on exhaustive DPLL, this should answer your alternative question.

Note that the results of Bova et al. are rather asymptotic (there are some small hidden constants in the analysis) but from my experience with similar problems, actual implemented model counters should fail quite early on those instances.

Note that these instances might not be the ones you are looking for: instead of challenging state-of-the-art model counters, they just outright break them provably. So to work around this, you would have to completely change the approach from DPLL to something else similarly to the compiler I linked above (which I don't think will work on these instances, either).


Is there a better than linear lower bound for factoring and discrete log? Are there any references that provide details about circuit lower bounds for specific hard problems arising in cryptography such as integer factoring, prime/composite discrete logarithm problem and its variant over group of points of elliptic curves (and their higher dimensional abelian varieties) and the general hidden subgroup problem?

Specifically do any of these problems have more than a linear complexity lower bound?

@Suresh: following your advice, here is my "answer". The status of circuit lower bounds is quite depressing. Here are the "current records":

  $4n-4$ for circuits over $\{\land,\lor,\neg\}$, and $7n-7$
for circuits over $\{\land,\neg\}$ and $\{\lor,\neg\}$
  computing $\oplus_n(x)=x_1\oplus x_2\oplus\cdots\oplus x_n$;
Redkin (1973). These bounds are tight.

 $5n-o(n)$ for circuits over the basis with all
  fanin-2 gates, except the parity and its negation; Iwama and
  Morizumi (2002).

  $3n-o(n)$ for general circuits over the basis
  with all fanin-2 gates; Blum (1984). Arist Kojevnikov and Sasha Kulikov from Petersburg have found a simpler proof of a
$(7/3)n-o(1)$ lower bound. The advantage of their proof is its simplicity, not numerical. Later they gave a simple proof of $3n-o(1)$ lower bound for general circuits (all fanin-2 gates are allowed). Albeit for very complicated functions - affine dispersers. Papers are online  here.

 $n^{3-o(1)}$ for formulas over
  $\{\land,\lor,\neg\}$; Hastad (1998).

  $\Omega(n^2/\log n)$ for general fanin-$2$ formulas,
$\Omega(n^2/\log^2 n)$ for deterministic branching programs, and
$\Omega(n^{3/2}/\log n)$ for nondeterministic branching programs;
Nechiporuk~(1966).

So, your question "Specifically do any of these problems have more than a linear complexity lower bound?" remains widely open (in the case of circuits). My appeal to all young researchers: go forward, these "barriers" are not unbreakable! But try to think in a "non-natural way", in the sense of Razborov and Rudich.