In the indexing problem Alice has a vector $x \in \{0,1\}^d$ and Bob has a number $i$, and Bob wants to learn $x_i$. The randomized one-way communication complexity of this problem is $\Omega(d)$ (see Section 3 of this paper), and it can be solved by approximating $x_i = \langle x, e_i\rangle$ up to any multiplicative factor where $e_i$ is the vector with $1$ in the $i$-th coordinate and $0$'s everywhere else. So your problem has $\Theta(d)$ randomized one-way communication complexity for $r=1$.


Reference request: complexity of $k$-partite $k$-SAT

Claim: If there exists an $\epsilon > 0$ such that for every $k'$, $k'$-partite $k'$-SAT can be solved in $2^{n(1-\epsilon)}$ time, then SETH fails.

Proof:
Suppose such an algorithm exists. We give an algorithm that, for every $k$ solves $k$-SAT in time $2^{n(1-\epsilon/2)}$.
Consider a $k$-SAT instance with $n$ variables, apply the sparsification lemma so that it produces $2^{n(\epsilon/2)}$ instances where, in every instance, every variable occurs in at most $(k/\epsilon)^{O(k/\epsilon)}$ clauses.
Each of these instances are $(k/\epsilon)^{O(k/\epsilon)}$-partite in the sense that one can find a coloring of the variables into $k' = (k/\epsilon)^{O(k/\epsilon)}$ colors such that no clause contains variables with the same color. If you want clauses of size exactly $k'$ you can replace clauses of size $k$ by $2^{k'-k}$ clauses of size $k'$.
Running the $2^{n(1-\epsilon)}$ time algorithm on each of the $2^{n(\epsilon/2)}$ instances of $k'$-partite $k'$-SAT gives an algorithm for $k$-SAT with running time $2^{n(1-\epsilon/2)}$ as claimed.

Note that the above proof essentially reduces $k$-SAT to $k^k$-partite $k^k$-SAT. So an algorithm with running time $2^{n(1-\frac{\log \log k}{\log k})}$ could still be possible, if very surprising.


Is it possible to have a 4-coloring for a non-planar graph ?

Obviously not. A graph is bipartite if and only if it is 2-colorable, but not every bipartite graph is planar ($K_{3,3}$ comes to mind).


Examples of problems where exponential algorithms run faster than polynomial algorithms for practical sizes?

How bout the simplex algorithm for linear programming?
In many occasions it is used in practice.
Edited to add:
I think it's more of a "worse-case exponential algorithm" which runs efficiently on practical instances/distributions rather than runs faster on practical sized adversarial instances.


Knapsack problem. It can be solved in polytime by dynamic programming if you give the target weight in unary.

Similarly other problems which are weekly polynomial time (pseudo-polynomial time) but not strongly polynomial time would need some part of input to be in unary. (You may also want to search for weakly NP-complete.)


Is Biological Computation a theme covered by the Theoretical Computer Science?

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


Simply typed lambda calculus and higher order logic

The distinction is this: if STLC is taken as a primitive language at the type-level adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL.

Taking $\iota$ as the base type of numbers ans $\omicron$ as the base type of propositions, you can add the constants
$$ \forall_\tau:(\tau\rightarrow \omicron)\rightarrow \omicron\quad \supset:\omicron\rightarrow\omicron\rightarrow \omicron$$

where $\tau$ is an arbitrary type (so one $\forall$ constant for each type). One possible set of axioms:

$$ \frac{\phi(x)}{\forall_\tau(\lambda x.\phi(x))}\mbox{$x:\tau$ not free in the hypotheses}$$

$$ \frac{\Large{\substack{[\psi]\\ \\ .\\ .\\ .\\ \\ \phi}}}{\psi\supset \phi}$$

where $[\psi]$ means that the hypothesis $\psi$ is discharged. Interesting fact: the other connectives $\exists_\tau, \vee$... can be derived from just those 2.

The subtlety is distinguishing between $\lambda$-terms as a way to represent proofs, as predicated by the Curry-Howard-de Bruijn (Martin-Löf) correspondence, or as a way to represent the terms you reason upon. The two views are not incompatible, of course.

In particular there is a typed $\lambda$-calculus that faithfully represents HOL (minus various axioms of course). This happens to be a sub-system of the Calculus of Constructions, and is described in detail by Geuvers in The Calculus of Constructions and Higher Order Logic. He also details the differences between the two (the CoC is not a conservative extension of HOL).


On the notion of positive rank of a matrix

There are examples of $n\times n$ real matrices of rank at most $3$ and non-negative rank at least $\sqrt{2n}$. So the non-negative rank cannot be bounded by any function of the rank in general. The construction I am aware of goes through extension complexity. An explanation follows.

The extension complexity $xc(K)$ of a convex set $K$ in $\mathbb{R}^d$ is the smallest possible number of facets of a (higher-dimensional) polytope that projects to $K$. (Equivalently the smallest possible number of constraints in a linear program for $K$). A famous theorem of Yannakakis shows that if there exist $A$, $b$ and $v_1, \ldots, v_n$ such that $K = \{x: Ax \leq b\} = \mathrm{conv}(v_1, \ldots, v_n)$, then
$$
xc(K) = \mathrm{rank}^+(S),
$$
where $S$ is the slack matrix, defined by $S = b1^T - A^TV$ for $V = (v_1, \ldots, v_n)$, i.e. the matrix whose columns are the $v_i$.

A result by Fiorini, Rothvoss, and Tiwari shows that there exist two-dimensional $n$-gons with extension complexity at least $\sqrt{2n}$. Since any $n$-gon $P$ in $\mathbb{R}^2$ can be written as $P = \{x: Ax \leq b\} = \mathrm{conv}(v_1, \ldots, v_n)$ for $A$ an $n\times 2$ matrix, $b$ an $n\times 1$ vector and $V = (v_1, \ldots, v_n)$ a $2\times n$ matrix, the slack  matrix $S = b1^T - A^TV$ of $P$ is the sum of a rank $1$ and a rank $2$ matrix, and therefore is of rank at most $3$. On the other hand by Yannakakis's and Fiorini et al.'s results $\mathrm{rank}^+(S) = xc(P) \geq \sqrt{2n}$.


Reductions between languages of different densities?

Let $A$ be any language not in $L$, such that $A$ has density $2^{o(n)}$, and define
$$B = \{s \circ 1 | s \in \{0,1\}^*\} \cup \{s \circ 0 | s \in A\}.$$
Here $\circ$ is concatenation. The language $B$ has density $\Omega(2^n)$, which is superpolynomial in $2^{o(n)}$. On the other hand, $A$ and $B$ log-space reduce to each other ($A$ to $B$ by concatenating $0$, and $B$ to $A$ by reducing all strings ending in $1$ to the smallest yes instance of A, and removing the last bit from all strings ending in $0$). Hence $B \notin L$ as well.


What is the complexity of this graph problem?

This is a reduction from Clique to your problem .

We start with an instance of Clique: a graph $G$ and an integer $k$, let $V = \{ v_1, v_2,...,v_n\}$.

Clique remains NPC even under the constraint that $max(deg(v_i)) \leq 2(k-1)$ (proof sketch: if $max(deg(v_i) > 2(k-1)$ then add a $K_t$ where $t = 2(k-1) - max(deg(v_i))$ and connect it to all nodes of $G$ and ask for a clique of size $k' = k + t$ in the new graph).

So we assume that in $G$, $max(deg(v_i)) \leq 2(k-1)$. For each node $v_i$ for which $deg(v_i) < 2(k-1)$ we create an "external" clique $C_i$ of size $2(k+1)+1$ (every node of $C_i$ clique has at least $2(k+1)$ neighbours).

If $deg(v_i)$ is the degree of $v_i$, we connect $v_i$ to $2(k-1) - deg(v_i)$ nodes of $C_i$.

In the resulting $G'$, each $v_i$ has degree $2(k-1)$; so $|A| \geq k$ because at least one vertex must be selected.

It is clear that if one of the vertex of $C_i$ is included in $A$ then at least $2(k+1)/2 = k+1$ nodes must also be inserted in it. Note that if an original node has $deg(v_i) < k-1$ then at least one node of the linked $C_i$ must be included, leading to $|A| > k$.

So we can build a set $A$ of minimum size $|A| = k$ if and only if $G$ contains a clique of size $k$.

An example of the reduction in which we ask if the graph $G$ represented by the yellow nodes and bold edges contains a clique of size $k = 3$ (a triangle).

The blue nodes (grouped for better readability) are $K_9$, the red edges are the links between nodes of $G$ with $deg(v_i) < 2(k-1)$ .


Yes, exactly what you suggested is true: if there is a sparse $\mathbf{P}$-complete set under log-space many-one reductions, then $\mathbf{P} = \mathbf{L}$. This was conjectured by Hartmanis in 1978 and proven by Cai and Sivakumar in 1995. See this paper.

Hartmanis also conjectured that if there is a sparse $\mathbf{NL}$-complete set under log-space many-one reductions, then $\mathbf{NL} = \mathbf{L}$. This was also proven by Cai and Sivakumar in 1997; see this other paper.


Where is the quote "Informal proofs are algorithms, formal proofs are code" from?

He doesn't cite any references for it and
Google doesn't return any results so
I don't think he is really quoting from anywhere.

The idea that a proof is a "construction"
(a term in intuitionistic/constructive mathematics
with a very close meaning to what we call algorithm nowadays)
goes back to at least Luitzen Egbertus Jan Brouwer.
Note that Brouwer was talking about informal proofs
as typically stated by mathematicians,
not formalized proofs which are a very recent phenomenon.

The idea that a formal proof is a like a program in a programming language
can be traced back to at least to
the BHK interpretation of intuitionistic logic by Arend Heyting.
The formal correspondence is Curry-Howard isomorphism.


Great question! I have also had thoughts along similar lines, but not found anything in the literature that fully answers all of these questions. However, for this part of your question, I think a satisfactory answer is given by Berman & Hartmanis:

  what prevents us from adding some (polynomial amount of) structure to our NP-Complete problems so that reductions from one NP-Complete problem to another converge in size?

In some sense, nothing: Berman & Hartmanis showed that if two languages have one-to-one, polynomial-time invertible, length-increasing reductions between them in both directions, then the languages are p-isomorphic. (Here a one-to-one function $f$ is poly-time invertible if there is a poly-time function $g$ such that $g(f(x)) = x$ for all $x$, and $g(y)=\bot$ if $y$ is not in the image of $f$.) Two languages being p-isomorphic basically just means that one is a re-encoding of the other, and thus preserves the "structure" of the other in some sense, that I think is similar to what you're talking about. All known natural $\mathsf{NP}$-complete problems are p-isomorphic. The idea of the proof is a ping-pong-type argument.

Finally, as another pointer to the literature: Although the notion of $\mathsf{NP}$-complete is not sensitive to the size of the reduction (so long as it's bounded by a polynomial), the Exponential Time Hypothesis (ETH) and its variants are sensitive to super-linear blow-ups in size. So there may be some work on ETH that addresses parts of your question.


Number of subgraphs with a given number of nodes

Let $f(G, k_1, k_2)$ be the counting problem that you have defined. Then
$$g(G) = \sum_{k_1 = 0}^{|V_G| / 2} f(G, k_1, 2 k_1)$$
counts the number of matchings in $G$, which only uses a linear number of oracle calls to your problem.

Since counting matchings in 3-regular planar graphs is #P-hard (see ref below), your questions (1), (2), and (3) all give a #P-hard problem. Your last question (4) probably gives a #P-hard problem as well because counting matchings in 3-regular biparitie planar graphs is probably #P-hard, but I don't know if anyone has proved this.  The closest that I know of is that

counting matchings in 2,3-regular biparitie planar graphs is #P-hard and
counting matchings in biparitie planar graphs of max degree 6 is #P-hard.

The reference that I promised above is Holographic Algorithms with Matchgates Capture Precisely Tractable Planar #CSP by Jin-Yi Cai, Pinyan Lu, Mingji Xia. Theorem 6.1 proves that counting matchings in 3-regular planar graphs is #P-hard in the special case that $[y_0, y_1, y_2] = [1,0,1]$ and $[x_0, x_1, x_2, x_3] = [1,1,0,0]$.


Permanent as projection of determinant and another permanent

A way to have such an explicit example is the following: Consider a matrix $A$ full of indeterminates (you can specialize the entries if you wish). Then use some formula for the permanent of this matrix (Ryser's or Glynn's for example). From this formula, you can build another matrix $B$, of quite huge dimensions, whose determinant equals the formula, thus the permanent of $A$.

Another thing you can do is to consider a matrix A whose determinant and permanent are the same (adjacency matrix of a graph whose cycles are of odd length). Then you can use different constructions to build a new matrix B with the same determinant. For instance, in our paper Symmetric Determinantal Representation of Formulas and Weakly-Skew Circuits, we give an algorithm that given a matrix $A$ builds a symmetric matrix $B$ such that $\det A=\det B$ (Section 3.2).

You can have a look at our paper for the classical techniques to do what you want (if I am not mistaken). For the second part, it is easy to change the constructions giving a matrix $B$ whose determinant equals some other determinant or formula, in such a way that you obtain another matrix $C$ such that $\operatorname{per} C=\det B$.

A last word to be more explicit:

$$\operatorname{per}\begin{pmatrix} x&y\\ 1&1\end{pmatrix}
   = \det\begin{pmatrix} x&0&0&1 \\ 0&y&0&1 \\ 0&0&1&0 \\ 1&1&0&0\end{pmatrix}$$

I hope this helps, even though I am not quite sure to exactly understand what you mean by "explicit example". If you are looking for an explicit example where for some $(n\times n)$ matrix $A$, the smallest matrix $B$ such that $\operatorname{per} A=\det B$ has dimensions $>n$, then you should look at Mignon & Ressayre's paper "A quadratic bound for the determinant and permanent problem" or subsequent works by Jin-Yi Cai and coauthors.


It turns out that $m=2n$ is possible, and this can be done explicitly in a very related fashion to your idea. It's not hard to see that this is basically optimal. In essence, what you are asking for is an injective map $E:\mathbb{F}_2^n\to \mathbb{F}_2^m$ such that the set of elements $\{E(\mathbf{x})\}_{\mathbf{x}\in \mathbb{F}_2^n}$ forms a Sidon set in the group $(\mathbb{F}^m_2,+)$ (a Sidon set of an abelian group $(G,*)$ is a set of elements $A$ such that $\vert A + A\vert$ is maximal, meaning that for $i\neq j$, $a_i+a_j=a_{i'}+a_{j'}$ if and only if $\{i,j\}=\{i',j'\}$).
It turns out that the size of the largest Sidon set in $\mathbb{F}_2^{2k}$ is at least $2^k$, and can be explicitly obtained from the following construction of Lindström (see also this more recent paper by Sidorenko on related topics): consider all elements of the form $(\mathbf{x},\mathbf{x}^3)$ where we express $\mathbf{x}\in GF(2^k)$ as a $k$-dimensional vector over $\mathbb{F}_2$ with respect to some basis. It turns out that this forms a Sidon set, and moreover, given $(\mathbf{x},\mathbf{x}^3)+(\mathbf{y},\mathbf{y}^3)=(\mathbf{u},\mathbf{v})$, one can solve for $\mathbf{x}$ (and therefore $\mathbf{y}$) by solving a quadratic equation in $GF(2^k)$. I'm guessing this can be done in $\text{poly}(k)$ time if you're principled about the construction/representation of $GF(2^k)$, but note that this isn't super trivial because the field has characteristic two so the quadratic formula won't help (see this for potentially more info).
Moving back to your case, this means that the encoding $\mathbf{x}\mapsto (\mathbf{x},\mathbf{x}^3)$ when interpreting $\mathbf{x}\in GF(2^n)$ should give you what you want.


Approximating non-trivial graph automorphism?

I don't understand the motivation very well. However, let me provide an answer to a related question. In the property testing framework, you are given two graphs $G$ ad $H$ and wish to distinguish two cases based on parameter $\epsilon$:

$G$ and $H$ are isomorphic
Any bijection from $G$ to $H$ causes error on at least $\epsilon \binom{n}{2}$ edges.

The complexity metric is the number of probes to the adjacency matrices, and the goal is to distinguish the two cases with high probability using a sublinear number of probes.

Eldar Fischer and Arie Matsliah (thanks, arnab) have a paper in SODA 2006 on precisely this problem. While it doesn't directly connect to your problem, it may be a way to a possible problem formulation, and might even provide useful techniques for you.


Getting an automaton from set of words in and out of a language

If I understand your question correctly, it is shown in the following paper that it is an NP-complete problem:

E. Mark Gold: Complexity of Automaton Identification from Given Data Information and Control 37(3): 302-320 (1978)


It depends how the polytope is represented. In the V-polytope presentation (i.e. $P$ is given in terms of its vertices), the problem is trivial, as Tim mentioned in the comments. In the H-polytope presentation (i.e. $P$ is given as an intersection of halfspaces defined by inequalities), Brieden  proved that a constant factor approximation is impossible unless P=NP. You can check that his proof indeed uses a polytope contained in the positive orthant.

As far as approximation algorithms, I believe the best known result is a factor $O(\sqrt{n/\log n})$ approximation ($n$ is dimension). The algorithm only needs a separation oracle, and this is the best possible approximation achievable in the oracle model, even by randomized algorithms. The same factor is achievable if the $\ell_2$ norm is replaced by an $\ell_p$ norm for $1\leq p \leq 2$. A better approximation may be possible for H-polytopes, but I am not aware of any such result.

EDIT: Actually I am now realizing that for the very similar problem of approximating the radius of a centrally symmetric H-polytope with $m$ facets, there is a simple SDP rounding that gives $O(\sqrt{\log m})$ approximation.

Let's say the problem is given as $\max\{\|x\|_2: -b \leq Ax \leq b\}$, where $A$ is an $m\times n$ matrix and $b \geq 0$ is an $m$-dimensional vector. The following vector program, which can be turned into an SDP in the usual way, is a relaxation:

$$
\begin{align}
&\max \sqrt{\sum_{j = 1}^n \|v_j\|_2^2} \text{ s.t.}\\
&\left\|\sum a_{ij} v_j\right\|_2 \leq b_i \ \ \ \ \ \forall 1 \leq i \leq m
\end{align}
$$
where $v_1, \ldots, v_n$ range over $n$-dimensional vectors. A Gaussian projection now gives an approximation. Let $g$ be a standard $n$-dimensional Gaussian, and define a random $x$ by $x_i = \frac{1}{C\sqrt{\log m}} g^Tv_i$ for a big constant $C$. Then $\mathbb{E}\|x\|_2 = \frac{SDP}{C\sqrt{\log m}}$, where $SDP$ is the value of the relaxation, and for $C$ sufficiently big,
$$
\mathbb{E} \max_{i = 1}^m \frac{|(Ax)_i|}{b_i} \leq 1.
$$
The last inequality comes from the fact that $(Ax)_i/b_i$ is a Guassian random variable with variance $(C^2\log m)^{-1}$, and the maximum of $m$ such random variables is no more than 1 in expectation by a standard concentration argument.

I very much doubt that I am the first one to think of this approximation: does anyone know of a reference?


I don't have access to the original paper, but this is an alternate reduction from SUBSET PRODUCT. The decision version of the WEAPON TARGET ASSIGNMENT (WTA) problem is:

Input: Given an integer $k$, $W_i$ weapons of type $i = 1,...,m$, $n$ targets $j=1,...,n$ having values $V_j$; each weapon type has a certain probability of destroying each target, given by $p_{i,j}$.
Question: Does there exist an assignment of the available weapons such that:

$$D = \sum_{j=1}^n V_j \prod_{i=1}^m q_{i,j}^{x_{i,j}} \leq k  $$

where $x_{i,j} = 1$  if weapon $i$ is assigned to target $j$ ($x_{i,j} = 0$ otherwise), and $q_{i,j} = 1 - p_{i,j}$ (survival probability of target $j$ when hit by weapon $i$).

Given a set of positive integers $A= \{a_1, a_2, ..., a_m\}$, and a target product $b$; the SUBSET PRODUCT problems asks for a subset $X \subseteq \{1,2,...,m\}$ such that $\prod_{i \in X} a_i = b$. Let $P = \prod a_i$, note that if $b \nmid P$ then the subset product problem doesn't have a solution.

We can build a WTA instance with two targets ($n=2$) having the same value $V_1 = V_2= P$ and $m+2$ weapons $W_1,W_2,...,W_m,W_{\alpha},W_{\beta}$:

    weapons $W_1,W_2,...,W_m$ can destroy both targets with probability $p_{i,1} = p_{i,2} = 1 - \frac{1}{a_i}$ (the survival probability is $q_{i,1} = q_{i,2} = \frac{1}{a_i}$);
    weapon $W_{\alpha}$ can destroy both targets with probability $p_{i,1} = p_{i,2} = 1 - \frac{b}{2P}$ (the survival probability is $q_{i,1} = q_{i,2} = \frac{b}{2P}$);
    weapon $W_{\beta}$ can destroy both targets with probability $p_{i,1} = p_{i,2} = 1 - \frac{1}{2b}$ (the survival probability is $q_{i,1} = q_{i,2} = \frac{1}{2b})$

We set $k = 1$.

($\Rightarrow$) Suppose that the original subset sum problem has a solution $X$; let $Y=\{1,\ldots,m\} \setminus X$.
Then
$$\prod_{i \in X} \frac{1}{a_i}=\frac{1}{b},\quad \prod_{y \in Y} \frac{1}{a_y} = \frac{b}{P}$$

If we assign weapons $W_x, x \in X$ and $W_{\alpha}$ to target 1; weapons $W_y, y \in Y$ and $W_{\beta}$ to target 2 we get:

$$ D= V_1 * \frac{b}{2P}* \frac{1}{b}  + V_2 * \frac{1}{2b}* \frac{b}{P} = P * \frac{b}{2P}* \frac{1}{b}  + P * \frac{1}{2b}* \frac{b}{P}  = 1$$

($\Leftarrow$) Suppose that the WTA instance has a solution and let $X',Y'$ be the indices of the weapons assigned to target 1 and 2 respectively ($X',Y'\subseteq \{1,\ldots,m,\alpha,\beta\}$). We must have:

$$ D = P \prod_{x \in X'} q_{x,1} + P \prod_{y \in Y'} q_{y,2} \leq 1$$

$W_{\alpha}$ and $W_{\beta}$ cannot both belong to $X'$ (or $Y'$), otherwise:

$$P \frac{1}{2b}*\frac{b}{2P}*\frac{1}{ \prod_{x \in X'\setminus \{\alpha,\beta\}} a_x} + \frac{P}{ \prod_{y \in Y'} a_y} \geq \frac{1}{4 \prod_{x \in X'\setminus \{\alpha,\beta\}} a_x}+1 > 1$$

So suppose that weapon $W_{\alpha}$ is assigned to target 1 and $W_{\beta}$ to target 2; let $X = X' \setminus \{ \alpha \}, Y = Y' \setminus \{ \beta \}$; we must have:

$$ P \frac{b}{2P} \prod_{x \in X} \frac{1}{a_x} + P\frac{1}{2b} \prod_{y \in Y} \frac{1}{a_y} \leq 1$$

$$\mbox{if } z = \prod_{x \in X} a_x, \quad \frac{b}{2z} + \frac{z}{2b} \leq 1$$

Multiplying both sides by the positive quantity $2bz$ we get:

$$ b^2 + z^2 \leq 2bz$$

$$(b - z)^2 \leq 0$$

So we must have $b = z = \prod_{x \in X} a_x$, so $X$ is a valid solution for the original SUBSET PRODUCT problem.

(P.S. Unfortunately, despite the hardness of this problem, the war between peoples seems to be a lot easier to start ..."The day the power of love overrules the love of power, the world will know peace." [Mahatma Gandhi] ):


Regarding question (1):
As long as $k$ is $\Omega(n^c)$ for some $c > 0$, then the problem is $PSPACE$-complete.  See this paper by Klaus-Jörn Lange and Peter Rossmanith (1992) for some related results.
https://doi.org/10.1007/3-540-55808-X_33
Regarding question (2):
Say that the intersection problem is parameterized by the number of FSA's.  If this parameterized problem is in $FPT$, then $PTIME \neq NLOGSPACE$.
In fact, the result is quite a bit stronger than that.  Essentially, it says that if for every $\alpha > 0$, there exists $k$ sufficiently large such that the $k$th slice of the parameterized problem is solvable in $O(n^{\alpha \cdot k})$ time, then $PTIME \neq NLOGSPACE$.
See here and here.
Regarding question (3):
I am still trying to understand this question.
Regarding last question:
Both the DFA and NFA parameterized intersection problems (when parameterized by the number of automata) are fpt-equivalent.  In fact, the fpt-equivalence is very strong and preserves the parameter (I called it an LBL-equivalence).  Regarding your question, this implies that if one of them is in $FPT$, then the other is in $FPT$ too.
Additional information:
Part of the reason why we have these hardness results for the parameterized FSA intersection problem is because it is $XNL$-complete under a strong form of fpt-reduction.  $XNL$ is a parameterized complexity class that is related to $k \cdot log(n)$ binary space nondeterministic Turing machines.


Zero knowledge verification of an encryption protocol

For symmetric-key encryption:

If Alice and Bob know a proof that $D_K(E_K(x))=x$ for all $x,K$, then they should be able to prove this fact in zero knowledge.  In particular, they can produce boolean circuits for $D_\cdot(\cdot)$ and $E_\cdot(\cdot)$, publish a commitment to each boolean circuit, and then turn their proof into a zero-knowledge proof.  In particular, verifying that $D_K(E_K(x))=x$ for all $x,K$ is in co-NP, and thus in IP, and there are zero-knowledge proofs for all of IP (and all of PSPACE).

Now if Alice wants to encrypt a message, she can give a zero-knowledge proof that she has encrypted some message correctly by doing the following: publish commitments $C(x),C(K)$ to her message $x$ and her key $K$; publish a commitment $C(y)$ to her ciphertext $y=E_K(x)$; and now give a zero-knowledge proof that all the commitments are consistent (the ciphertext corresponding to $C(y)$ is a correct encryption, under the boolean circuit for encryption that was committed to earlier, under the key corresponding to $C(K)$ of the message corresponding to $C(x)$).  Whether this is a useful thing to prove is another matter entirely -- it's not clear exactly what you are looking for or how you would use a solution to your problem, but hopefully this will give you some ideas.

For public-key encryption:

See Sadeq Dousti's comment.  The exposition above can be readily adjusted to fit the public-key encryption setting, along the lines Sadeq Dousti suggests.


An example of a totally computable function that is not definable in system T?

Interpreters for T are not definable in T, thanks to the incompleteness theorem.

Concretely, fix a Godel encoding, and then let $f$ be the function which takes a pair consisting of a Godel-encoding of a closed term of type $\mathbb{N} \to \mathbb{N}$, and a natural number in $\mathbb{N}$, and returns the value of the application. This function is not definable in T. It's a worthwhile exercise to work out how you can use a self-interpreter to define an infinitely looping program.


Reference for a class of graphs that preserve subgraph distances when ordered

I don't have an answer for your whole class of graphs, but three subclasses of graphs that have this property are the distance-hereditary graphs, chordal graphs, and median graphs.

Distance-hereditary graphs are defined by the property that every connected induced subgraph has the same distances. So you can pick an arbitrary starting vertex $v_1$ and then choose each successive vertex to be any not-already-chosen vertex that is adjacent to a previously-chosen vertex.

The chordal graphs are the graphs that have an ordering with the property that each successive vertex, when added, has a clique for its neighbors. This ordering is obviously distance-preserving.

Similarly, median graphs (including your grid example) have the property that, for any breadth-first ordering, each vertex has a hypercube neighborhood at the time it is added. (See pages 76–77 of Eppstein et al, "Media Theory", Springer, 2008). Again, this property means that the addition cannot change the distances among the previous vertices.

There's a class of graphs that I don't know a name for, generalizing both chordal and distance-hereditary graphs, that can be recognized in polynomial time and that have your property. They are the connected graphs that can be built up from a single vertex by adding vertices one by one, where the neighbors of each new vertex are a subset of one of the closed neighborhoods of the previous graph. They are almost (but not quite) the same as the dismantlable graphs, the difference being that the new vertex does not have to be adjacent to the vertex whose neighborhood is being copied. An elimination ordering of a chordal graph is a construction of this type where each new vertex chooses a clique subset of a neighborhood. Similarly distance-hereditary graphs have a construction of this type where the neighbors of each new vertex are an entire closed neighborhood, an open neighborhood, or a single vertex. Each new vertex can't change the distances of the previous vertices, so this construction sequence has the property you're looking for.

If you define a vertex v to be "removable" if it could be the last one in this sequence (it has an open neighborhood that is a subset of someone else's closed neighborhood) then removing other removable vertices doesn't change the removability of v: if v's neighborhood is a subset of u's, and we remove u as having a neighborhood that is a subset of w's, then v is still removable because its neighborhood is still a subset of w's. Therefore, the sequences of removal steps that we can follow to take a graph back down to nothing form an antimatroid, and one such sequence can be found in polynomial time by a greedy algorithm that repeatedly removes a removable vertex whenever it can find one. Reversing the output of this algorithm gives the construction sequence for the given graph. The graph of the cube gives an example of a graph that has your property (a median graph) but is not constructible in this way. I think the median graphs that can be constructed in this way are exactly the squaregraphs (which include the regular grids). The graphs that have a construction sequence of this type also include all graphs that have a universal vertex, such as the wheel graphs, so (unlike chordal graphs and distance-hereditary graphs) they are not perfect and not closed under induced subgraphs.


Complexity of computing the discrete Fourier transform?

This answer is a variant of the analysis of the first algorithm
("Methode A") by Schönhage and Strassen for multiplication of long integers.

Assume we want to compute an FFT of length $K = 2^k$.
Scale your input such that all values are smaller than 1.
Let us first assume that we compute with $m$-bit fixed point arithmetic
($m$ bits after the binary point). Let $\delta = 2^{1/2 -m}$ be the
("complex") unit of least position. Let $\omega =  \exp(2\pi i/K)$.

1) One can compute approximations $\omega_j'$ such that
$|\omega_j' - \omega^j| \le (2k-1)\delta$ for all $0 \le j \le K-1$.
This can be done in time $O(K M(m))$ where $M(m)$ is the time needed
to multiply $m$-bit numbers. (see Knuth Vol. 2, 3rd ed., page 309).

If standard integer RAM means logarithmic cost, then $M(m) = O(m \log m)$.
If standard integer RAM means word RAM, then $M(m) = O(m)$. (Schönhage and Strassen show in "Methode A" how to reduce in linear time the multiplication of $m$-bit numbers to $m$ multiplication of $O(\log m)$ bit numbers. The latter can be done at unit costs.)

2) The classical Cooley-Tukey FFT computes operations of the form
$a = b + \omega^j c$. We use $m$-bit fixed point arithmetic,
these opertions become $a' = truncate(b' + \omega_j' c')$.
If we know $b'$ and $c'$ up to an error of $\epsilon$, we get $a'$ up to an error of $2\epsilon + 2k\delta$.

3) Using induction, it is easy to see that we get the final result
with error $(2^k - 1) \cdot 2k\delta$. To get precision $b$ in the end,
$m \ge k + \log k + b + O(1)$.

4) Thus the final running time is $O(K k M(k+b))$.

This should also work with floating point numbers: 1) can still be done with fixed point arithmetic, 2) is also true for floating point numbers.

In fixed point arithmetic, I think, it can even be done faster.
First we reduce the computation of the FFT to the multiplication of
polynomials using Bluestein's trick.
The length of the coefficients needed to get the desired precision
should be $O(k + b)$.
Then we reduce the multiplication of polynomials to the multiplication
of long integers. (Append the coefficients to a long number and separate them by blocks of zero of length $O(k+b)$.) The length of the integers is $O(K(k+b))$.


Is an algorithm with an approximation factor of 4000 useful?

A very good question! While I think a feasible solution which is 4000 times worse than the optimum is often not very practical, if you have several approximation algorithms to choose from, I would rather implement the one with a better performance guarantee. Well, maybe not always. At the very least, the feasible solutions found are often of much better quality than the guarantee. That is, if an algorithm performs better than terribly in the worst case, it often performs very well in practice. At least I've read something along those lines.

Apart from that, you can think of the result as a mathematical theorem, which may be of interest in its own right. Citing the wikipedia article on approximation algorithm:

  The desire to understand hard optimization problems from the perspective of approximability is motivated by the discovery of surprising mathematical connections and broadly applicable techniques to design algorithms for hard optimization problems. One well-known example of the former is the Goemans-Williamson algorithm for Maximum Cut which solves a graph theoretic problem using high dimensional geometry.


Program for computing Tree decomposition of a graph

Some of these software might help you. (Not all of them are open-source though.)

*TreeD http://www.itu.dk/people/sathi/treed/

*dlib http://dlib.net/

*QuickBB http://www.cs.washington.edu/homes/vgogate/quickbb.html

*Hypertree http://www.dbai.tuwien.ac.at/proj/hypertree/downloads.html

*LibTW http://www.treewidth.com/treewidth/


Decidability

It's decidable.  There are only finitely many possible functions $f:Q \to Q$, so you can model this as a graph reachability problem, with one vertex per function and an edge $g \to h$ if there exists $a \in \Gamma$ such that $h = f_a \circ g$.  Then, testing whether a function $g$ is in $G$ reduces to testing whether $g$ is reachable in the graph from $f_\epsilon$.  You can find the shortest such word using breadth-first time.  The running time might be exponential in $Q$, though.

Length of the word

The shortest such word might be exponentially long.  Here is an example of such a DFA.  Let $p_1,\dots,p_k$ be the first $k$ primes.  Then a state will be of the form $(i,x)$ where $i \in \{1,\dots,k\}$ and $x_i \in \{0,1,\dots,p_i-1\}$.  Define a DFA with unary alphabet $\Gamma=\{0\}$ and the transition function $\delta((i,x),0 = (i,x+1 \bmod p_i)$.  The function $f_0 :Q \to Q$ is given by

$$f_0(i,x) = (i,x+1 \bmod p_i).$$

Now consider the function $g:Q \to Q$ given by

$$g(i,x) = (i,x-1 \bmod p_i).$$

It is possible to use the Chinese remainder theorem to show that $g = f_{0^n}$ where $n=p_1 \times p_2 \times \cdots \times p_k -1$, and that $0^n$ is the shortest such word.  Moreover, $|Q|= p_1 + \dots + p_k$, so $n$ is exponentially large in $Q$.

Consequently, there is no hope for a polynomial-time algorithm that outputs such a word.  This still leaves open the possibility of a polynomial time algorithm for deciding whether $g$ is in $G$, though.


How is the inner ring chosen in the Schönhage–Strassen algorithm?

This answer is taken from the paper "Asymptotically fast algorithms for the numerical muitiplication and division of polynomials with complex coefficients" that Markus linked in the comments.

You want to square an $n$-bit number, modulo $2^n + 1$. Here's what you do:

Find $p$ and $s$ that satisfy $n = (p-1) 2^s$ and $s \leq p \leq 2s$.
Pick the number of pieces $2^m$ to split the $n$ bits into, and the corresponding parameters for the piece sizes:

$$\begin{align} m &= \lfloor s/2 \rfloor + 1 \\s_2 &= \lceil s/2 \rceil + 1 \\ p_2 &= \lceil p/2 \rceil + 1 \end{align}$$

Note that $s_2$ and $p_2$ continue to satisfy the $s_2 \leq p_2 \leq 2 s_2$ invariant. Also note that $2^m 2^{s_2} p_2 \geq 2n + m + 1$ is satisfied, so the input fits with room for carries.
Perform the FFT-based negacyclic convolution on the pieces, and the rest, as usual.

So that's the overarching idea: a logarithmic padding factor $p$. Now for the complexity analysis. The FFT will take $n m$ work to do, and we're recursing on $2^m$ pieces of size $(p_2-1) 2^{s_2}$, so now we can do extremely rough math with the recurrence relation w.r.t. $s$:

$$\begin{align}
F(s)
&(\leq)\; (p-1)2^sm + 2^m F(\lceil s/2\rceil+1)
\\
&(\leq)\; 2s2^s (\lfloor s/2\rfloor+1) + 2^{\lfloor s/2\rfloor+1} F(\lceil s/2\rceil+1)
\\
&(\leq)\; s^2 2^s + 2 \cdot 2^{s/2} F(s/2+1)
\\
&(\leq)\; s^2 2^s + 4 (s/2)^2 2^s + 16(s/4)^2 2^s + ...
\\
&(\leq)\; 2^s s^2 \lg(s)
\\
&(\leq)\; \frac{n}{\lg n} \left(\lg \frac{n}{\lg n}\right)^2  \lg \lg \frac{n}{\lg n}
\\
&(\leq)\; \frac{n}{\lg n} (\lg^2 n) \lg \lg n
\\
&(\leq)\; n \;(\lg n) \lg \lg n
\end{align}$$

Which seems about right, although I cheated quite a lot in those steps.

The 'trick' seems to be the fact that we end up with $s^2$ instead of $s$ in the base cost. There's still two multiplications by two per recursive level, like I was complaining about in the question, but now the halving of $s$ is paying double-dividends so it all works out. Then, at the end, we cancel the extra factor of $s$ (which is actually a factor of $\log n$) thanks to making $p$ logarithmically large relative to $s$ initially.


Fast algorithm to find a maximum connected subgraph of k vertices

This is a self-plug but in the paper An algorithmic framework for fixed-cardinality optimization in sparse graphs applied to dense subgraph problems we consider exactly problems such as the one that you describe. The running time of the algorithm is $O((e\cdot (\Delta-1))^k\cdot (\Delta+k)\cdot n)\cdot T(n,k)$ where $T(n,k)$ is the time needed for evaluating the objective function $f$. Here, $\Delta$ is the maximum degree in the input graph. The algorithm is based on enumeration of connected subgraphs of order $k$. Observe that a graph may have $\Omega((e\cdot (\Delta-1))^k\cdot n/k)$ such induced subgraphs. The bounds for the number of connected induced subgraphs are based on a result of Bollobás in The Art of Mathematics - Coffe Time in Memphis.

Thus, to further improve on the running time above, one either needs to consider other structural properties of the input graph or to exploit some properties of $f$ that make it possible to avoid enumerating all connected induced subgraphs.


A decision problem related to the problem of counting Hamiltonian cycles

This is in PP.

Let $N$ be the size of the larger graph.  We will define a predicate $f(P, b)$ where $P$ is a permutation of the numbers from 1 to $N$ and $b$ is a single bit.

First, define a predicate $H(G, P)$ where $G$ is a graph (with nodes labeled from 1 to $n \leq N$) and $P$ is a permutation of the numbers from 1 to $N$.  Set $H$ to be true if and only if $P$ fixes the numbers from $n + 1$ to $N$ and if the permutation it induces of the numbers from 1 to $n$ defines a Hamiltonian cycle on $G$.  The number of $P$ for which $H(G, P)$ holds is then the number of Hamiltonian cycles in the graph.

Now, let $f(P, 0) = H(G_1, P)$ and $f(P, 1) = \overline{H(G_2, P)}$.  The number of $P, b$ pairs making $f$ 0 is then the number of Hamiltonian paths in $G_2$ plus the number of "Hamiltonian non-paths" in $G_1$, and vice versa holds for the number of pairs making $f$ 1.  Thus, whichever of these values is more common tells you which graph has more cycles, and this is precisely what PP allows you to do.


Closure of unambiguous context-free languages under pre- and postfix.

The set $\mathit{ppc}(L)$ is certainly context-free, but I think it can be inherently ambiguous: consider
$$L=\{a^mb^mc^nd\mid m,n\geq 0\}\cup\{da^mb^nc^n\mid m,n\geq 0\}\;,$$ then $\mathit{ppc}(L)$ includes the classical inherently ambiguous language $$L'=\{a^mb^mc^n\mid m,n\geq 0\}\cup\{a^mb^nc^n\mid m,n\geq 0\}\;,$$ and one can prove $\mathit{ppc}(L)$ is also inherently ambiguous by the usual argument (apply Ogden's Lemma to both $a^{n+n!}b^nc^n$ and $a^nb^nc^{n+n!}$ to deduce the existence of two distinct trees for $a^{n+n!}b^{n+n!}c^{n+n!}$).


Two matrices related by a permutation $B = P A P^T$ - complexity

It is equivalent to deciding whether two given multigraphs (or edge-labelled graphs) are isomorphic or not, which is known to be equivalent to the usual graph isomorphism problem.


SUBSET-SUM with binary - unary - "positional" encoding

If an instance of POSITIONAL-SUBSET-SUM has input length $N$, then each integer in the set $\{x_1, x_2, ..., x_n\}$ must satisfy $|x_i| \le N$, and the set itself must have size $n \le N$.  So the input length for the corresponding instance of UNARY-SUBSET-SUM is $O(N^2)$, and it is easy to see that mapping one input format to the other can be done in polynomial time.  Therefore, since UNARY-SUBSET-SUM $\in \text{P}$, we have POSITIONAL-SUBSET-SUM $\in \text{P}$ as well.


$\omega$-regular properties of a 2-state Markov Chain

I am not sure whether $A_f$ is an $\omega$-regular event, but for any $\delta>0$ we can pick some $\omega$-regular $A_\delta$ such that $|\mathsf P(A_\delta) - \mathsf P_\delta(A_\delta)| \geq 1-\delta$. This follows from the fact that $\omega$-regular events form an algebra that generates a $\sigma$-algebra where $A_f$ does belong to.


The paper “On Recursion, Replication and Scope Mechanisms in Process Calculi” by Jesús Aranda, Cinzia Di Giusto, Catuscia Palamidessi, and Frank D. Valencia gives an encoding of the polyadic pi-calculus with recursive definitions in terms of the polyadic pi-calculus with replication and vice versa. The essence of the encoding (in the first direction) is to replace the recursive definition by the replication of a process, so that each invocation of the recursive definition results in a new process.


The Planar Separator Theorem states that in any planar $n$-vertex graph $G$ there exists a set of $O(\sqrt{n})$ vertices whose removal leaves the graph disconnected into at least two roughly balanced components. Moreover, such a set can be found in linear time. This (tight) result, proved by Lipton and Tarjan (improving on a previous result by Ungar) is a powerful tool for designing algorithms on planar graphs. It gives many exact subexponential time algorithms for NP-hard problems and improved polynomial time approximation algorithms. Looking at the wikipedia page gives a good starting place to explore the numerous applications. An early survey with details of a number of applications was written by Lipton and Tarjan in 1980.


Decidability of rank-k polymorphism vs. System F

The conclusion of [Kfoury & Tiuryn 1992] says (emphasis mine):

  We prove that [...] for every $k\ge 3$ there is a typing of constants
  that assigns types in $S(1)$ such that the type reconstruction problem
  for $\Lambda_k$ extended by this typing is undecidable.
  Unfortunately, this result does not give any clue as to whether type
  reconstruction for $F_2$, with or without constants, is decidable.
  Our decidability/undecidability proofs use in an essential way the apriori information about the rank of types.

So, if you don't force constants to have certain pre-defined types of known rank, or if you don't have constants at all, the problem may become easier (than undecidable). The proofs rely on having constants that are forced to have certain types. (Of course, as you pointed out, Wells showed that the problem isn't easier.)


Approaches to GI inspired by knot problem

One connection is that graph isomorphism and knot isomorphism are both special cases of 3-manifold homeomorphism. In the knot case, two knots are isomorphic if their complements (manifolds formed by deleting the points of the knot from 3-space) are homeomorphic.

And in the graph case it's possible to transform graphs into manifolds in such a way that the graphs are isomorphic if and only if the manifolds are homeomorphic. I wrote a comment about this on a Google+ post last December, but unfortunately not on a post I can share. The construction is to start with a manifold for each vertex v, in the form of the complement in a 3-sphere of a bouquet of degree(v) loops (connected together at a common vertex). For each edge uv, connect the manifolds for u and v together by a surgery, and link one loop from u and one loop from v across the surgery ball. Then every isomorphism of graphs lifts to a homeomorphism of the resulting manifold (this would be true even if we just used surgery on 3-spheres without the bouquets) and the bouquets prevent the manifold from having extra homeomorphisms that don't come from the graph.


What are the compelling reasons for believing $L\neq P$?

Mulmuley's result (from Mulmuley's webpage without paywall) that, in the PRAM model without bit operations, "$\mathsf{P} \neq \mathsf{NC}$". (In the usual boolean model where $\mathsf{L}$ lives, $\mathsf{L} \subseteq \mathsf{NC}$.) This model is strong enough that the result implies any $\mathsf{L}$ algorithm for a $\mathsf{P}$-complete problem would have to look quite different from most known algorithms for $\mathsf{P}$-complete problems.

The PRAM model without bit operations is a nonuniform, algebraic model over $\mathbb{Z}$ (similar to algebraic computation trees or the Blum--Shub--Smale algebraic RAM model) in which the nonuniform program can depend not just on the number of integer inputs, but also on their total bitlength. In this way it's not a "purely" algebraic model, but lives somewhere between algebraic and boolean. This model includes poly-time algorithms for linear programming, maxflow, mincut, weighted spanning tree, shortest paths, and other combinatorial optimization problems, the logspace algorithm for tree isomorphism (see comments below), and algorithms for approximating the complex roots of polynomials, which is why I say any $\mathsf{L}$ algorithm for a $\mathsf{P}$-complete problem (which, as your question indicates you know, most people think does not exist) would have to look quite different from any of these.


Efficient algorithm to find overlapping circles of various sizes

A modified Bentley-Ottmann sweep algorithm (here, for example) will find all line segment intersections in $O((n+k)\log n + k)$ time, where $k$ is the number of intersections.  It's fairly straightforward to extend the algorithm to handle circles. A good walkthrough is here under "finding intersections".

$k$ can be $\Omega(n^2)$ in theory (in which case pairwise checking is faster), but it seems difficult to avoid the $k$ term, and in any case you seem to say $k$ will be small in your question.

Granted, this recomputes the intersections from scratch each time you run the algorithm, which may be inefficient for your purposes.  You may be able to get around this a bit by maintaining the list of circles sorted by $x$ coordinate, and modifying this list online as the circles move.  This won't help your asymptotic running time, but it avoids sorting each circle every time.  If the circles stay relatively sparse (few cross the same vertical line), the binary search tree on the $y$-coordinates will be cheap to maintain.

The other issue is that knowing two circles intersect already does not improve the running time at all.  Once two circles attach to each other, you will calculate their intersection every single time, which is a waste.


Has there been any progress in tightening the exponent in the result that polylog independence fools $AC_0$?

In his CCC'17 paper [1], Avishay Tal improved the bound to $$
\left(\log\frac{m}{\varepsilon}\right)^{O(d)}\,. \tag{1}
$$
You may want to check p.15:4 for a discussion. It also refers to (see Footnote 30 to a paper of Harsha and Srinivasan, which improves on (1)) and answers Tal's conjecture: $k$-wise independent, for
$$
k = \left(\log m \right)^{O(d)}\cdot\log\frac{1}{\varepsilon}\,. \tag{2}
$$
suffices to $\varepsilon$-fool size-$m$ depth-$d$ AC0 circuits.

[1] Tight Bounds on the Fourier Spectrum of $\mathsf{AC}_0$, A. Tal. CCC'17.

[2] On polynomial approximations to $\mathsf{AC}_0$, P. Harsha and S. Srinivasan. RANDOM 2016,


There has been a lot of work on this, usually under the heading of "memory models".  See, for example:

The Java memory model
Foundations of the C++ Concurrency Memory Model by Boehm and Adve
Lots of recent work by Peter Sewell's group on C++ concurrency and hardware memory models


Cohomological approach to boolean complexity

I corresponded with Joel Friedman about 3 years ago on this topic.  At the time he said that his approach had not led to any significant new insights into complexity theory, though he still thought it was a promising tack.

Basically, Friedman tries to rephrase the problems of circuit complexity in the language of sheaves on a Grothendieck topology.  The hope is that this process will allow geometric intuition to be applied to the problem of finding circuit lower bounds.  While it's certainly worth checking to see if this path leads anywhere, there are heuristic reasons to be skeptical.  Geometric intuition works best in the context of smooth varieties, or things that are sufficiently similar to smooth varieties that the intuition doesn't totally break down.  In other words, you need some structure in order for geometric intuition to gain a foothold.  But circuit lower bounds by their very nature must confront arbitrary computations, which are difficult to analyze precisely because they seem to be so structureless.  Friedman admits right up front that the Grothendieck topologies he considers are highly combinatorial, and far removed from the usual objects of study in algebraic geometry.

As a side comment, I'd say that it's important not to get too excited about an idea just because it uses unfamiliar, high-powered machinery.  The machinery might be very effective at solving the problems that it was designed for, but for it to be useful for attacking a known hard problem in another domain, there needs to be some compelling argument why the foreign machinery is well adapted to address the fundamental obstacle in the problem of interest.


Why spectral norms are used for computing the complexity of adiabatic Hamiltonian?

The spectral norm $||H||$ determines the maximum energy involved in driving the evolution of the quantum system and thus the quantum computation. Any quantum evolution could be sped-up by a factor of $\lambda$ by simply driving the system with Hamiltonian $\lambda H$ as a simple consequence of Schrödinger's equation. The energy involved is simply another physical resource invested into solving the problem, that needs to be considered in complexity considerations, besides time. For example, if your Hamiltonian has a tiny spectral gap, you could of course enlarge it by simply rescaling the strengths of all interactions in your system until the gap is large enough in absolute terms. Of course, after having solved the engineering challenges involved, this will linearly accelerate your computationion, similar to overclocking your classical PC. But the speed gained was only achieved by investing another resource that needs to be kept track of.


Hierarchy theorem for approximation ratios?

There is an approximation hierarchy, the main known examples: FPTAS $\subseteq$ EPTAS $\subseteq$ PTAS $\subseteq$ APX. But for inapproximability there also is NPO-PB.

There are a lot of results about the set of possible ratios, going from results like this one:

  $P||C_{max} \in$ EPTAS$\backslash$ FPTAS, unless $P=NP$,

to defining APX/NPO-PB-hard problems.

Some references:

ON PTAS: M. Cesati and L. Trevisan. On the efficiency of polynomial time approximation schemes, 1997.
On NPOPB: V. Kann. Strong lower bounds on the approximability of some NPO PB-complete maximization problems

But I suggest the best will be to check the Complexity Zoo because it has many more information and references on those examples, even Wikipedia

Furthermore, as stated in the comments the tight bound when $\alpha=O(1)$, was shown for many problems such as bin packing, machine scheduling (see iris.gmu.edu/~khoffman/papers/set_covering.html).


The problem becomes NP-complete ... this is a "graphical" :-) reduction from 3-SAT ... it should be self-explanatory (... if not let me know).

Two notes:

+X1a, -X1a, +X1b, -X1b,...,+X2a,-X2a, ...,dum1,...,dum4 are all distinct labels;
in the figure  each label appears $\leq 2$ times; but it is straightforward to make each label appears exactly 2 times adding some dum nodes+edges+labels to pair them up.


Applications of metric structures on posets/lattices in theoryCS

First, a comment. Your question sort of depends on how geometrically you intend to mean the word "metric". It's reasonably common to use ultrametrics in semantics and static analysis, but ultrametrics tend to have a combinatorial rather than a geometric interpretation. (This is a variant of the observation that domain theory has the flavor of a combinatorial rather than geometric use of topology.)

That said, I'll give you an example of how this comes up in program proofs. First, recall that in a program proof, we want to show that a formula describing a program holds. In general, this formula does not necessarily have to be interpreted with the booleans, but can be drawn from the elements of some lattice of truth values. Then a true formula is just one which is equal to the top of the lattice.

Furthermore, when specifying very self-referential programs (for example, programs that make extensive use of self-modifying code) matters can get very difficult. We typically want to give a recursive specification of the program, but there might not be an obvious inductive structure upon which to hang the definition. To solve this problem, it's often helpful to equip the truth value lattice with extra metric structure. Then, if you can show that the predicate whose fixed point you want is strictly contractive, you can appeal to Banach's fixed point theorem to conclude that the recursive predicate you want is well-defined.

The case I am most familiar with is called "step-indexing". In this setting, we take our lattice $\Omega$ of truth values to be downwards-closed subsets of $\mathbb{N}$, whose elements we can loosely interpret as "the lengths of the evaluation sequences on which the property holds". Meets and joins are intersections and unions, as usual, and since the lattice is complete we can define the Heyting implication as well. The lattice can also be equipped with an ultrametric by letting the distance between two lattice elements be $2^{-n}$, where $n$ is the smallest element in one set but not the other.

Then, Banach's contraction map thoerem tells us that a contractive predicate $p : \Omega \to \Omega$ has a unique fixed point. Intuitively, this says that if we can define a predicate which holds for $n+1$ steps using a version which holds for $n$ steps, then we actually have an unambiguous definition of a predicate. If we then show that the predicate equals $\top = \mathbb{N}$, then we know that the predicate always holds of the program.


High-level overview of Razborov's method of approximations

Let $f$ be a Boolean function on $n$-bits. Let $Z = f^{-1}(0) \subseteq 2^n$. Let $C$ be circuit on n bits and of size $m$ and gates $g_1, \ldots, g_m$. $g_i$ also denotes the function on $n$-bits computed by subcircuit with $g_i$ as the last gate. The first $n$ gates are for the input $x_1, \ldots, x_n$. The goal is to show that $C$ of size $m$ cannot compute $f$. Consider all computations of $C$ on inputs from $Z$. A computation assigns values to outputs of gates. Let $B$ be the Boolean algebra of $P(Z)$.

The idea is to consider for any function  $g$ on $n$-bits how well it approximates $f$ on $Z$. Let $||g|| = \{w \in Z \mid g(w) \neq 0 \}$.

For an ultrafilter $F \subseteq B$ we can define a new computation by ultraproduct from it: $c(g_i) = 0$ iff $||g_i|| \not\in F$. Because an ultrafilter is essentially a set of consistent computations for 0 values the resulting $c$ is a valid computation. It would follow that $f(c_1, \ldots, c_n) = 0$. We created a new computation from existing ones. Since all ultrafilters on finite sets are principal $c_1,\ldots,c_n \in Z$. This works for any circuit, we have not exploited the fact that the circuit is of size $m$.

The next idea is now to exploit the finiteness of the circuit to construct a new input that is outside $Z$ and $f(w) \neq 0$ but the circuit does not notice because of its limited size and therefore still outputs 0. So it does not compute $f$.

We need to relax the definition of ultrafilter so that we can get an input outside $Z$. In place of ultrafilters we use upward-closed subsets of $B$ ($a \in F$ and $a \subseteq b$ implies $b \in F$) that preserve meets($a,b \in F$ implies $a \cap b \in F$).

Let $W_F = \{w \in 2^n \mid w_i = 0 \to ||\lnot x_i|| \in F, w_i \neq 0 \to ||x_i|| \in F\}$. $W_F$ is the set of inputs consistent with $F$. If $F$ is prime ($a \cup b \in F$ implies $a \in F$ or $b \in F$) and nonfull ($\emptyset \not\in F$) then for each $i$, $F$ contains either  $||x_i||$ or $||\lnot x_i||$ and $W_F$ contains only a single input.

We are going to relax preservation of meets. In place of all meets in the Boolean algebra we will preserve a small number of them. Let $|f|$ be the smallest number $k$ of meets $M = (a_1 \cap b_1, \ldots, a_k \cap b_k)$ such that for all upward-closed, nonfull, $M$-preserving $F$, $W_F \subseteq Z$.

Let $m$ be the circuit complexity of $f$. Razborov proved that $\frac{1}{2}|f| \leq m \leq O(|f|^3 + n^3)$.

Note that this inequality holds for all functions. To prove a circuit size lower bound $m$ show that for all $m$-meets $M$, there is a $F$ that satisfies the conditions but its $W_F$ is not contained in $Z$. Moreover any strong circuit lower bound can be proven by this method because of the second inequality.

The actual part of a circuit lower bound proof is to show that for given $m$, for any $m$-meets there is such an $F$. In the case of monotone circuits the condition about $W_F$ simplifies to $w_i \neq 0 \to ||x_i|| \in F$ so coming up with $F$ is easier.

Alexander Razborov, On the Method of Approximation, 1989.
pdf

Mauricio Karchmer, On Proving Lower Bounds for Circuit Size, 1995.

Tim Gowers, Razborov's method of approximation, 2009. pdf


Does Pattern Calculus represent a step forward in languages or are we just going back to LISP?

I'm not familiar with Barry Jay's recent work, but his older work includes things that you cannot do in Lisp, because the types give additional information.

For example, suppose you want to define the size of a Lisp data structure. It's 1 for an atom, and n for a list of n atoms, and more generally size(x)+size(y) for (cons x y).

Now throw in types into the mix. The size of a list would be its length. Now what's the size of a list of lists of atoms? If you consider this data structure as a list (whose elements happen to be lists of atoms), the answer is the length of the list. If you consider this data structure as containing atoms that happen to be stored in a list of lists, the answer is the sum of the lengths of the element lists.

Types allow you to distinguish between these two views (shapes) of the raw data. You need a type system that lets you discriminate between (List) (List Atom) and (List List) (Atom). The most common implementation of this distinction is with type classes (as in Haskell).


Gerhard Woeginger has an up-to-date page with all attempts to (dis)prove the P vs NP question:
https://www.win.tue.nl/~gwoegi/P-versus-NP.htm


Fun question! As a base I will use this Haskell quine I found on Wikipedia:

main=putStr(p++show(p))where p="main=putStr(p++show(p))where p="

You can make it print out two copies of itself by replacing the occurrences of p++show(p) with p++show(p)++p++show(p). If you see why, the pattern to achieve variable repetition should be clear.

I will be using the following function that calculates the nth iterate of f on x:

iterateN n f x = (iterate f x) !! n

I'll assume it's available as a library function. You can easily embed its definition directly in the quine, but that would clutter the presentation without good reason. Now the rest is simple:

main=putStr(iterateN 42(++(p++show(p)))[])
  where p="main=putStr(iterateN 42(++(p++show(p)))[])where p="

The line break was inserted to aid readability; remove it if you want exact self-replication.


Constant-time bounds on offline 2-choice hashing?

You're missing the (obvious but) unstated caveat of "with high probability", I think.  If you're hashing randomly, there's some chance all items choose the same two buckets.  With high probability, you can get constant load.  I think I recall this was first shown to me by Alan Frieze, but I can't recall the reference.  Cuckoo hashing provides another way of showing this is true.


Functional Completeness of 3-valued logic

Chapters 5 and 6 of the book [Function algebras on finite sets, Dietlinde Lau, 2006] contain an in depth treatment of functional completeness in many-valued logic (including proofs). In summary: Rosenbergs [1965, 1970] characterization of maximal clones (also called precomplete clones) give a criterion for functional completeness in k-valued logic for any k.

For the special case of 3-valued logic such a characterization (consisting of 18 maximal/precomplete classes) was given by Jablonskij already in 1954. Hence, in order to verify that your set of 3-valued "operators" are functionally complete, it is enough to check that they don't fall into any of the 18 precomplete classes.


k-testable languages with non-constant k?

Locally testable languages form a subset of the first-order definable languages, where the only allowed numerical predicate is the successor  (see Straubing, page 46 [1]).

By allowing the "local" part to grow, you somehow change the predicate from successor to a length dependent predicate. In particular, the predicate is still "numerical" and thus the languages you are defining are still in $\textrm{AC}^0$ (which is equivalent to FO with the set of all predicates). It is even much lower than that, probably depth-4 wire-linear size circuits, but I didn't check this carefully. I doubt it has a good "cellular automata" variant  since it contains a mixture of local (local patterns) and global (alphabet) information. I would be interested to have some insight on the parallel complexity of cellular automata.

My bet is that your class is indeed much more expressive than regular languages, but fails to recognize more regular languages than locally testable ones. To be a bit more formal:

For a sublinear function $f\colon\mathbb{N}\to\mathbb{N}$, let $\textrm{LocTest}_f$ be the class of languages $L$ such that $L\cap A^n$ is a $k$-locally testable language for $k=\mathcal{O}(f(n))$. Then, my guess is that you should have $\textrm{LocTest}_f \cap \textrm{Reg}$ is exactly the class of (classical) locally testable language. This kind of statement can be found for logical framework at the end of Straubing Book (I like to call these properties of classes of languages "Straubing Properties" when it is known and "Straubing Conjecture" when it is open).

For this specific case, I doubt it has been studied as such but it can be seen as a restricted case of the first level of alternation hierarchy of first-order logic with any predicates (which has a known "Straubing Property"). I would bet it should not be too hard to adapt the proof but it requires some heavy semigroups theory results.

[1] Straubing, Howard. Finite automata, formal logic, and circuit complexity. Progress in Theoretical Computer Science. Birkhäuser Boston, Inc., Boston, MA, 1994.


Neither, they are domain elements.  Any two domain elements would do: $\{+1, -1\}$, $\{0,1\}$, $\{\text{cat}, \text{dog}\}$.

Physicists have wonderful imaginations and thus name certain parameters based on their physical intuition for the behavior of nature.  In this case, they interpret the states of the particles interacting in the Ising model as either spinning up or down.  Furthermore, opposite spins produce opposite effects, such as their resulting magnetic fields being the negative of each other.  Thus, the state of the particles (i.e. the spins) are succinctly represented in the model as either $+1$ or $-1$.

Another good naming example from physics is in string theory.  The equations that describe the motion of these exceedingly small "objects" reminded the physicists of the equations that describe the motion of strings.  Thus the name.

The Potts model is a generalization of the Ising model.  One of the generalizations is that each particle can take one of $q$ values (i.e. the domain size is now $q$).  By continuing the intuitive naming from the Ising model, these $q$ states are also called spins.


Teaching high school TCS - existing programs

Many countries organize summer schools for their IOI teams
(consisting of high school students aged roughly 16 IIRC).
The one we have in Iran used to have the following courses:

programming,
data structure and algorithms,
combinatorics, and
graph theory.

I think ACM's Computer Science Teachers Association has
a K12 curriculum on its Curriculum Resources page
though it is probably way too light for talented teenagers.

I think programming must definitely be part of the curriculum.
Python should be a good first language to learn.

You might want to also cover some accessible topics with applications
(the joy of building something cool can have a big effect on their interest).
I think Andrew Ng's ML course on Coursera
should be accessible for talented students
(specially for those in countries like yours where
there is a more serious K12 math curriculum ).

A nonstandard topic that you might want to consider is combinational game theory,
it might be not very interesting with 16 years old (I don't have experience for it) but
it works quite well for a bit younger students in my experience.

I personally think the central and connecting theme should be around algorithms,
I think it would work better than automata theory as the central theme and
arguably the algorithmic perspective (not Turing machines, automata, etc.)
is the essence of computer science.


The complexity of Lenstra's algorithm for mixed-integer programming in his paper runs as  $2^{O(n^3)}*poly(d, \phi)$  where there are $n$ integer variables, $d$ continuos variables, and $\phi$ is the binary encoding size of the problem.  This is not stated very explicitly in his paper, but the main thing to notice is that the complexity is primarily guided by the number of subproblems, which is $2^{O(n^3)}$.  Certain improvements allow a Lentra-type algorithm to have a complexity of $2^{O(n log(n))}$.  Other techniques allow for even n^n in terms of the number of integer variables.

Note that the method of Lenstra is easily applied to convex mixed integer optimization provided certain separation oracles exist.  This dates back to a book of Gretchel, Lovasz, and Schrijver.  Other results on semi-algebraic convex optimization exist for the pure integer case as an FPT.


This new version of the answer tries to take into account the changes
 in the question, and the information exchanged in the comments.

This answer assumes that $S$ should be the set of variables that have a
content that is used in some defined fragment of the program, rather
than, at some point in the program, the variables with a content that
will be needed before the end of the program.

For the latter, the usual term is live variables, as remarked in a comment by Klaus Draeger.

The former is a generalisation of the concept of use, as appears
in dataflow analysis, and particularly in such concepts as
Use-Define or Use-Definition chains (UD chains), as well as
Definition-Use chains (DU chains). The concept of use is usually
intended for elementary program statements such as an expression
appearing in an assignment or a function call. Recall that this
originates with analysis and optimization of old Fortran programs in
the late 1960s and in the 1970s, and the was no real concept of a
compound statement at the time in the Fortran language.

But there is no reason not to extend the concept to larger program
fragments that form a meaningful whole. Thus used variable or
used set seem to be exactly the concepts and terminology that you
are looking for.

Now, there may be a difficulty in defining what is implied in the
expression "is used by". It may just mean: "syntactically appears in",
which is as simple as you can make it. This is indeed purely
syntactic, but rather non satisfactory, because the variable may well
appear only in a statement that changes its value, rather than use the
value it already has. This is too simplistic is is clearly not what
was intended by the creators of the concept.

Then a better definition will state that the occurrence of a variable
must imply that its value is actually used.  But as soon as you say
that, you are no longer in syntax since you must use some of the
meaning of the program fragment to know whether the occurrence of the
variable is for using or for changing its value (or possibly is simply
irrelevant). And when you start using the semantics of the language
construct, there is no clear limit on how much of the semantics you
can use.

The definition given in page 632 of the Dragon Book 1988 is:

  We say that a variable is used at a statement $s$ if its $r$-value may be required.

First one should note the use of if rather than iff, which clearly
indicates that some variables not meeting the condition may end up
being qualified as used. This even reinforced by the may be.

Then, this almost definition does not bring much light on the issue. What does it mean to
be required. Typically, if a variable is an argument to a subprogram
(procedure, function, method, ...), you may think it is required.  But
if further analysis shows that the value of this argument is not
actually used in the subprogram, and the argument is only used to
return a result, the $r$-value of the variable is not required.  Some
may object that this could be handled by an appropriate type system,
which they consider syntax (I do not).  But the fact that a value is
not required may depend on deeper semantic analysis (such as in
example 4 of the question). Furthermore, the evolution of type systems
and type theory tends to allow inclusion in types of most thing you
may want to say or prove about a variable, which would hardly qualify
as syntactic.

Thus the situation is that there is not really an undisputable
syntactic (?) reference definition of "used variable", and it depends
essentially on an arbitrary choice implied by the set of techniques
used to analyze the program and the level of knowledge it brings
regarding actual use of the variable value at run-time.

On the other hand it is possible to give a reference semantic
definition for a set $S$ of used variables:

  A variable is used in some program fragment iff there is a computation of that program such that the results and effects
     of executing that fragment depend on the value of that variable before execution.

This is not completely satisfactory, because there are other
parameters that could be considered, and might suggest a different
terminology, though not change the above remarks about syntax and
semantics.

For example, in a sequential context, the above definition is clear,
and refers to the value of the variable before executing the program
(fragment).  However, one may still question what is considered an
effect, what is an impact on execution. Execution time could well be
part of the semantics of a program, or not.  Then, in a parallel
execution context, you would consider more than the initial value of
the variable. But I will ignore this, as the question has not been
considering it (as far as I can see), and I will stick to the
definition above.

The set $S$ thus defined semantically is the most precise
(i.e. minimal) set of variables that can matter in any computation,
though some may not matter in some computation.

But this set is not necessarily computable. It is recursively
enumerable, since a Turing Machine could simulate in parallel all possible
computations, and enumerate all the variables that turn out to be used
effectively (in the sense of our definition) in some computation. But
determining that some variable will not be used in a computation is
undecidable.

The best we can hope for is to exhibit a superset of $S$, such that we
are sure not to miss any relevant variable. This is precisely what is
done by the various techniques that can be called upon to determine
the used variables. But they do not all produce the same result and
the results they give can be more or less precise.

If some program analysis technique $T_i$ produces a set $S_i$ of used
variable, we say that $T_i$ is correct iff $S\subseteq S_i$.

If two techniques $T_1$ and $T_2$ produce respectively the sets $S_1$
and $S_2$, then $T1$ is better, more precise than $T_2$ iff
$S\subseteq S_1\subseteq S_2$.

The only thing that has a precise definition (up to the above caveat)
is the set S, enven though possibly not computable. It is also the
reference for any other set to be considered acceptable in practice, and is the smallest, the most precise of them all.

Hence, the expressions "used set" and "used variable" should be
reserved for that set.

And I suggest that the other sets that are considered in practice,
should use the same name, qualified with the name of the technique
that produced them. If the technique is unique and unnamed, it could
be called the computed use set (what is called SYin the question),
or just used set when there is no ambiguity.


Subexponentially solvable hard graph problems

Since every planar graph on $n$ vertices has treewidth $O(\sqrt{n})$, all problems which are solvable in $O^*(2^{O(k)})$ time for graphs of treewidth at most~$k$ (there are a LOT of such problems) have subexponential-time algorithms on planar graphs by computing a constant-factor approximation to the treewidth in polynomial-time (for example by computing the branchwidth with the ratcatcher algorithm) and then running the treewidth algorithm, resulting in runtimes of the form $O^*(2^{O(\sqrt{n})})$ for graphs on $n$ vertices. Examples are Planar Independent Set and Planar Dominating Set, which are NP-complete of course.


Regarding (3), yes,
if a graph $M$ has two vertex disjoint non-planar induced subgraphs $G$ and $H$, then $G\cup H$ (and hence $M$) is not toroidal.

I don't know a reference but here's a proof sketch.

Thinking of the torus as $T=S^1\times S^1$, if a non-planar $G$ is embedded without crossing on $T$ then its edges must meet every $S^1\times\{a\}$ and $\{a\}\times S^1$, or else we cut such a circle out and realize $G$ as planar. By tracing where they so meet we obtain a subgraph of $G$ realized as homotopic to some
$$\left(\{a\}\times S^1\right)\cup \left(S^1\times\{b\}\right)$$
(so two circles meet in $(a,b)$). Similarly for the second graph $H$ and say
$$\left(\{c\}\times S^1\right)\cup \left(S^1\times\{d\}\right).$$
But then $G$ and $H$ are not disjoint (they share a vertex or have crossing edges) as the embedded graphs meet in $(a,d)$ and $(c,b)$.


Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

You should have a look at the following paper -- and the previous work by Gori and Levi:

On Polymorphic Recursion, Type Systems, and Abstract Interpretation
Marco Comini, Ferruccio Damiani, Samuel Vrech, 2008

  The problem of typing polymorphic recursion (i.e., recursive function
  definitions rec {x = e} where different occurrences of x in e are used
  with different types) has been investigated both by people working on
  type systems and by people working on abstract interpretation.
  Recently, Gori and Levi have developed an abstract interpreter that is
  able to type all the ML typable recursive definitions and interesting
  examples of polymorphic recursion. The problem of finding a type
  system corresponding to their abstract interpreter was open.

  In this paper we present a type system corresponding to the Gori-Levi
  abstract interpreter. Interestingly enough, the type system is derived
  from the system of simple types (which is the let-free fragment of the
  ML type system) by adapting a general technique for extending
  a decidable type system enjoying principal typings by adding
  a decidable rule for typing recursive definitions. The key role played
  in our investigation by the notion of principal typing suggests that
  this notion might be useful in other investigations about the
  relations between type systems and type inference algorithms
  synthesized by abstract interpretation.


BQP algorithm for two graph bisection problems and its implications on NP $\subseteq$ BQP

Another paper with the same idea by Ahmed Younes and Jonathan E. Rowe, A Polynomial Time Bounded-error Quantum Algorithm for Boolean Satisfiability. The algorithm is not polynomial time.


Can any program be implemented mechanically?

Yes, it is. Here's how you do it:

You can compile basically any program you like to circuits. See for instance the work of Dan Ghica and his collaborators on the Geometry of Synthesis, which shows how to compile programs into circuits.

Dan R. Ghica. Geometry of Synthesis: A structured approach to VLSI design
Dan R. Ghica, Alex Smith. Geometry of Synthesis II: From Games to Delay-Insensitive Circuits
Dan R. Ghica, Alex Smith. Geometry of Synthesis III: Resource management through type inference.
Dan R. Ghica, Alex Smith, Satnam Singh. Geometry of synthesis IV: compiling affine recursion into static hardware.

Circuits then turn out to reappear over and over in engineering. John Baez gives a big table of analogies of concepts, and works out a lot of connections, in This Week's Finds 288-296. So the circuit diagrams Dan's compiler generates could be instantiated as mechanical or hydraulic systems, if you really wanted to!

╔══════════════════════════════════════════════════════════════╗
║                 displacement  flow      momentum     effort  ║
╠══════════════════════════════════════════════════════════════╣
║ Mechanics      position      velocity  momentum     force    ║
║ (translation)                                                ║
║                                                              ║
║ Mechanics      angle         angular   angular      torque   ║
║ (rotation)                   velocity  momentum              ║
║                                                              ║
║ Electronics    charge        current   flux         voltage  ║
║                                        linkage               ║
║                                                              ║
║ Hydraulics     volume        flow      pressure     pressure ║
║                                        momentum              ║
╚══════════════════════════════════════════════════════════════╝

http://math.ucr.edu/home/baez/week288.html
http://math.ucr.edu/home/baez/week289.html
http://math.ucr.edu/home/baez/week290.html
http://math.ucr.edu/home/baez/week291.html
http://math.ucr.edu/home/baez/week294.html
http://math.ucr.edu/home/baez/week296.html


Why do constructivists not seem to care too much about call/cc

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive mathematician.

To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc:

We provide a function $f$ which allegedly proves $\lnot p$. In reality $f$ is a bag of tricks.
If anyone ever applies $f$ to a proof of $p$, then $f$ unleashes call/cc to roll back time, and with a proof of $p$ in hand, changes its mind about $p \lor \lnot p$: this time claiming that it is a proof of $p$.

The constructive understanding of disjunction is algorithmic decidability, but the above is hardly making any decisions. As a test, a constructive mathematician might ask you how call/cc helps prove that every Turing machine halts or diverges. And what is the program witnessing this fact? (It ought to be the Halting Oracle.)


How to calculate this string-dissimilarity function efficiently?

What you seem to be looking for is called the minimum common string partition, and it has been well studied. In particular, it's known to be NP-hard. There is also a closely related concept of edit distance with block moves, which would capture the extension you mention, where substitutions are allowed.


It's taken years but this post inspired us to write a paper which has come out today.

The answer is that n Queens Completion is NP-Complete.  However for full disclosure should mention we solve a slight variant of the problem.  In our case the set of queens doesn't have to be a prefix of the full set.  So technically we haven't resolved the exact problem asked here.  However it would be extremely surprising if the version of n Queens Completion from this query wasn't also NP-Complete.

I want to repeat the thanks we put in the paper to Jeffε for raising this question here.

The complexity of n Queens Completion
Journal of AI Research
Gent, Jefferson, Nightingale
doi:10.1613/jair.5512
http://www.jair.org/papers/paper5512.html


Finite state transducer with infinitary outputs or without emphasis on acceptance?

There are several relevant references on the subject. I just indicate a few of them. I suggest you to browse the references of these articles to get more.

Early references include the work of Françoise Gire.

[1] F. Gire, "Relations rationnelles infinitaires", Thèse de 3ème cycle, Paris VII, 1981.

[2] F. Gire, Une Extension aux Mots Infinis de la Notion de Transduction Rationnelle, 6th GI Conf., Lect. Notes in Comp. Sci., Volume 145, 1983, p. 123-139.

[3] F. Gire, M. Nivat, Relations rationnelles infinitaires. [Infinitary rational relations] Calcolo 21 (1984), no. 2, 91--125.

Interesting results can be found in

[4] Latteux, M.; Timmerman, E. Rational $\omega$-transductions. Mathematical foundations of computer science (Banská Bystrica, 1990), 407--415, Lecture Notes in Comput. Sci., 452, Springer, Berlin, 1990.

Section 4.3 of [5] is also a very good reference.

[5] L. Staiger, ω-Languages, Vol 3, Chapter 6 of the Handbook of Formal languages edited by G. Rozenberg and A. Salomaa, (1997) 339-387. Springer-Verlag, Berlin.

Finally, here is a more recent paper, where you will find other relevant references.

[6] Finkel, Olivier. On the accepting power of 2-tape Büchi automata. STACS 2006, 301--312, Lecture Notes in Comput. Sci., 3884, Springer, Berlin, (2006).


Is MALL + unrestricted recursive types Turing-complete?

If additive commutations are omited in MALL, it's easy to show that the size of a proof decreases with every cut-elimination step. If additive commutations are allowed, the proof is not as easy, but it was provided in the original “Linear Logic” paper. It's called Small Normalization Theorem (Corollary 4.22, p71), which says that as long as the contraction–promotion rule is not involved (which is the case in MALL) normalization holds. The argument does not rely on formulas themselves, they could be infinite (e.g. recursively defined).

It means that it's not possible to encode a promotion for type $\mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)$ in MALL, since it would allow for fix point combinators. Some additional recursion construct would be needed for that.

Note: I believe that it's possible to use MALL together with a coinduction principle (introduction of $\mu$'s dual) to keep the system normalizing and obtain a promotion for this encoding of $!A$. Allowing recursive types in MALL + coinduction would then make it Turing complete. But as long as MALL is considered alone, allowing recursive types is not a big deal.


Correctness proofs of classic Paxos and Fast Paxos

Why can we assume that property CP held when acceptor a0 voted for v in round k? It seems that we are using mathematical induction, therefore, what are the basis, inductive hypothesis, and inductive steps?

You're looking at an instance of strong induction. In simple induction you assume the property holds for $n=m$ and prove it holds for $n=m+1$. In strong induction you assume the property holds for $\forall n: n<m$ and prove it holds for $n=m+1$.

Basis (I believe): $j = 0$. That is, the null round (since rounds start at 1). This is trivially true, which is probably why it was not stated explicitly.

Inductive step: Assume $\forall n, n \le j : CP(v; n)$; prove $CP(v; j+1)$ where $j < i$.

Believe it or not, this is only a proof sketch. The real proof is in the Part Time Parliament paper. (Some consider the paper cryptic, others consider it humorous.)

  How is this obtained?

  In my opinion, the correctness proof of the case $j<k$ relies (recursively) on those of cases of $k<j<i$ and $j=k$.

  Therefore, how can we conclude the case $j<k$ without first proving $j=k$ completely (namely, missing the subcase of $j=k$ where $V$ contains more than one value)?

This is again strong induction, so the case $j<k$ does rely on the cases of $k<j$ and $j=k$, but through the induction hypothesis, namely from the previous Paxos round.

General tips for Lamport's proofs.

Lamport uses a technique of hierarchical proofs. For example, the structure of the proof on pages 7-8 looks somewhat like this:

Assume $\forall n, n \le j : CP(v; n)$; prove $CP(v; j+1)$ where $j < i$.

Observation 1
Observation 2
Observation 3
$k = argmax (...)$
case k = 0
case k > 0

case k < j
case k = j
case j < k

Lamport tends to use another type of hierarchy. He'll prove a simpler algorithm, and then prove that a more complex algorithm maps onto (or "extends") the simpler algorithm. This doesn't seem to be happening on page 18, but it is something to look out for. (The proof on page 18 appears to be a modification of the proof a pages 7-8; not an extension of it.)

Lamport relies heavily on strong induction; he also tends to think in terms of sets instead of numbers. So you may get empty sets where others would have zeros or nulls; or set unions where others would have addition.

Proving correctness of asynchronous message-passing systems needs an omniscient view of the system with respect to time. For example, when considering actions in round $i$, keep in mind that the actions for some round $j < i$ may not have happened temporally!. And yet Lamport states these potentially future events in past tense.

Lamports systems and proofs tend to have a variable or set of variables that are only allowed to go in one direction; only incrementing numbers and only adding to sets. This is used extensively in his proofs. For example, on page 8 Lamport shows how he neutered the future ability of $a$ to cast another vote:

  ...Since it set $rnd[a]$ to $i$ upon sending a message, $a$ could not subsequently have cast a vote in any round numbered less than $i$....

It's definitely a brain-stretcher to prove these kinds of systems.

(update): List out the invariants; Lamport uses a lot of invariants when developing and his proofs. They are sometimes scattered throughout the proofs; sometimes they are only present in the machine-checked proof. Reason about each invariant; why is it there? How does it interact with the other invariants? How does each step in the system keep this invariant?

Full disclosure: I hadn't read Fast Paxos until I was asked to answer this question; and only looked at the pages cited. I'm an engineer and not a mathematician; my brush with Lamport's work is based purely on the need to correctly invent and maintain large-scale distributed systems.

My answer relies heavily on my experience with Lamport's work. I have read several of Lamport's protocols and proofs; I professionally maintain a paxos-based system; I have written and proven a high-throughput consensus protocol, and again professionally maintain a system based on it (I'm trying to get my company to allow me to publish a paper). I have collaborated on an insignificant paper with Lamport, in which I met with him thrice (the paper is still pending peer review.)


Results on universal approximation for learners other than ANNs

Let me attempt to partly answer the learning part, or to at least address some connections.
In learning (distributional issues aside), we usually want our algorithms to be able to not only approximate the target function (from a class) with a hypothesis, but also to be able find such a hypothesis (efficiently).  So, even though a certain class can universally approximate a given target, we are not done.

I am not an expert in neural networks, but training a neural network is not easy.  We have algorithms for training a neural network, like backpropogation, but they won't always converge, or converge quickly enough, to meet the PAC learning criteria.
Boosting, on the other hand says (roughly) how to turn a weak "approximator" into a strong one, but it in some sense assumes the difficulty away but giving the learner access to the weak approximator.


Would an NP-complete public key cryptosystem imply NP=co-NP?

Your argument is correct about the FACTORING problem, but it does not automatically generalize to all public-key cryptosystems.

Here's an excerpt from an exercise by Dominique Unruh, showing formally that if FACTORING is NP-complete, then NP = coNP.

If you are interested in research on the relationship between crypto and NP-completeness, I suggest reading Pass's paper Parallel repetition of zero-knowledge proofs and the possibility of basing cryptography on NP-hardness.


Is anyone actively researching distributed prediction models?

There is no information about any particular prediction model in your request, therefore, I think you should look through the paper "PLDA: Parallel Latent Dirichlet Allocation for Large-scale Applications" (2009) of Google researchers. See also their project on Google Code.

Besides, Google Prediction API project might be valuable resource related to the topic, too.


Complexity of converting a boolean circuit to a boolean formula

If I understand your question correctly, I'd say you could use the standard reduction from CIRCUIT-SAT to SAT: Represent each gate as a new variable, and then represent the entire circuit in CNF form, with each clause having the form $(v\leftrightarrow\phi)$, where $v$ is the new variable, and the formula for the gate is given by $\phi$, using the variables for other gates to represent the inputs. This can be done by a simple traversal (in linear time, which is clearly optimal).

For example, if you hade three inputs, $x_1$, $x_2$, and $x_3$, with AND gates linking $x_1$ and $x_2$ as well as $x_2$ and $x_3$, and an OR gate linking their outputs, you could introduce three variables to represent the gates—$v_1$, $v_2$, and $v_3$, respectively—and rewrite the formula to $$(v_1\leftrightarrow(x_1\land x_2))\land (v_2\leftrightarrow(x_2\land x_3))\land (v_3\leftrightarrow(v_1\lor v_2))\land v_3\,.$$ Note that the output variable is included explicitly.

Introduction to Algorithms by Cormen et al. explains this in detail, in the chapter on NP-Completeness.


Why does the log-rank conjecture use rank over the reals?

The conjecture fails over $\mathbb{F}_2$. Look at $M(x, y) = \langle x, y \rangle \bmod 2$, and $x, y \in \{0, 1\}^n$. The communication complexity is $\Omega(n)$, but the rank of $M$ over $\mathbb{F}_2$ is $n$, by the linearity of inner product.


When can a convex function induce submodularity?

The notion of sub-modularity you use is non-standard. Usually you consider set functions with domain $\lbrace 0, 1\rbrace^n$. But to answer your questions, the Lovász extension establishes the following relationship between sub-modularity and convexity:

A set-function $F$ is sub-modular if and only if its Lovász extension $f$ is convex. For a proof see Proposition 6 in [1]. To go a bit further, e.g. Proposition 2.3 in [2] establishes the fact the very set function can be written as a difference of two sub-modular function. Conversely, the Lovász extension of every set function is DC (difference of convex functions).

The converse is not true: Not every convex function restricted to  $\lbrace 0, 1\rbrace^n$ is sub-modular. Form your description I assume that you matrix is positive semi-definite. But it is not clear to me how you define the convex $f(x)$? With that information, you can start checking sub-modularity.

[1] https://hal.archives-ouvertes.fr/file/index/docid/535950/filename/submodular_tutorial.pdf
[2] http://www.ml.uni-saarland.de/Publications/HeinSetzer-BeyondSC%282011%29-Supplement.pdf


What's complexity of this set problem which looks like "Linear Programming"?

If I'm not mistaken, the case you specify (with $k =2$, $k_i = 3$) is in P.

Note that the condition $|S \cup S'| \le 3$ is equivalent to saying that $S, S'$ intersect (since $k=2$). Thus, if you think of the $S_i$ as vertices, then the constraints specify a graph $G$, and your problem reduces to finding a graph $H$ such that $G$ is the line graph of $H$.

Verifying that $G$ is indeed a line graph and then finding $H$ can be done in linear time.


Can a NEXP machine simulate invalid queries to a promise problem oracle?

Let's define what P$^A$ means in the promise setting: A language L is in P$^A$ if there is a polytime oracle machine $M$ such that for all sets $B$ such that $B$ contains $A_{YES}$ and $B\cap A_{NO}=\emptyset$, $L=L(M^B)$. In other words, the polytime machine can ask queries that are not part of the promise but its output cannot depend on whether those queries are answered yes or no.
For example, consider unique SAT where $A_{YES}$ are the formula with exactly one satisfying assignment and $A_{NO}$ are the formula with no satisfying assignment. Then $P^A$ is contained in $\oplus P$. We also have $NP\subseteq BPP^A$ by Valiant-Vazirani. Both these tools are used in the proof of Toda's theorem.


Understanding non-equivalence of proof lengths according to proof systems

I believe everything you said is correct. I note that your point #3 could hold regardless of points #1 and #2 - points #1 and #2 are just a concrete example of where this has provably happened.


Theorem 1. For every $d$ and $k$, there is a graph with the desired properties.
I'll describe the construction in two stages.
First, construct a bipartite multi-graph $G_1=(L_1, R_1, E_1)$ where

$L_1=\{\ell_1,\ell_2,\ldots,\ell_k\}$

$R_1 =  \{r_1, r_2, \ldots, r_k\}$

$E_1$ is the multi-set union of $d-1$ matchings $M_1, M_2, \ldots, M_{d-1}$, where

$M_h = \{(\ell_i, r_j) : (i + j + h) \bmod k = 0\}$ for $h\in\{1,\ldots, d-1\}$

Note that there may be multiple copies of each edge in the multigraph $G_1$.  (In particular, in the case that $d-1\ge k$, we can have $M_h = M_{h+k}$.)  We add a copy of $(\ell_i, r_j)$ to $E_1$ for each occurrence in any matching, making $E_1$ a multiset and $G_1$ a multigraph.
Lemma 1. $G_1$ is $(d-1)$-edge connected.
Proof. Consider the $d-1$ edge sets $M_1 \cup M_2$, $M_2 \cup M_3$, $\ldots$, $M_{d-2} \cup M_{d-1}, M_{d-1} \cup M_1$.  Each such edge set is a hamiltonian cycle, so any cut is crossed by at least $2(d-1)$ edges in the multiset union of these $d-1$ edge sets.  But each edge (copy) occurs twice in this multiset union, so any cut is crossed by at least $(d-1)$ edge (copies). $~~\Box$
Now obtain the desired graph $G=(L, R, E)$ from $G_1$ as follows.
For each vertex $\ell_i$ in $L_1$, replace $\ell_i$ by a distinct copy of $K_{d,d}$ (the complete bipartite graph with $d$ vertices on each side),
and replace each edge copy $(\ell_i, r_j)$ in $E_1$ by an edge from a vertex on the left side of the $K_{d,d}$ to $r_j$, so that each vertex on the left side of each $K_{d, d}$ has at most one edge added in this way.  This is possible because each $\ell_i$ has degree $d-1$, and the $K_{d,d}$ that replaces it has $d$ vertices on its left side.  Note that $G$ is a graph (not a multigraph), and that $G_1$ is obtained by contracting each $K_{d, d}$ into a single vertex.
Take $L$ to contain the vertices on the left sides of the $K_{d, d}$'s (each of degree $d$ or $d+1$).  Take $R$ to contain the $k$ degree-$(d-1)$ vertices in $R_1$, together with all vertices on the right sides of the $K_{d, d}$'s (each of degree $d$).  To finish, we prove the following lemma:
Lemma 2. $G$ is $(d-1)$-edge connected.
Proof. Suppose otherwise for contradiction.  Let $C$ be a cut of $G$ with less than $d-1$ edges.  The cut $C$ respects (doesn't cut) any $K_{d, d}$, because each $K_{d, d}$ is itself $d$-edge connected.  So contracting each $K_{d, d}$ yields a cut in $G_1$ that has less than $d-1$ (multi) edges, contradicting Lemma 1.  $~~~\Box$


Most significant bit of integer multiplication and binary decision diagrams

An interesting source is D. E. Knuth: The Art of Computer Programming, Volume 4, Fascicle 1, Bitwise Tricks & Techniques; Binary Decision Diagrams, Addison-Wesley, Pearson Education 2009

On page 96, there is a BDD for all bits of z = x⋅y, where x and y have 3 bits. It shows, that in the case of 3 bits, BDD representing the most significant bit has 7 non-terminal nodes. See the image bellow, I have redraw it using your indices x = (x2,x1,x0) and y = (y2,y1,y0).

On page 140 in Knuth's book, there is a question (no. 183) about BDD representing the most significant bit for multiplication of two numbers with infinitely many bits (it is called "limiting leading bit function") - this is similar to what you are loking for! The answer on page 223 gives first levels of the resulting BDD and discusses the number of nodes on all levels, but unfortunatelly it does not give algorithm to construct such a BDD.

Fig. 1: The most significant bit for multiplication of (x2,x1,x0) * (y2,y1,y0)


Complexity of problem that can be solved by exponentially many SATs

The problem you defined is not in FNP as by definition the length of the answer should be polynomial in the length of its input.

Even if we are guaranteed that the length of "y" (output of the function) is polynomial in length of formula (i.e., there are at most polynomially many answer), this problem is not FNP except P= CoNP.

Proof:

$$\hspace{-1cm}  F(\phi)= y \Leftrightarrow  \forall A: $$
$$\hspace{5cm}                 {\huge(} A\models \phi \Rightarrow M(A,y) \land $$
$$\hspace{5cm}       A\not\models \phi \Rightarrow \lnot M(A,y){\huge )} $$

Where $M(A,y)$ is a polynomial time computable function returning true iff assignment $A$ is in the set of assignments $y$.

Definition of FNP requires us to have a polynomial time function $P$ given $\phi$ and $y$,  returns true iff $F(\phi)=y$. That is, deciding if the following formula is tautology or not should be verifiable in P:

$$\Phi (A)= {\huge(} \left(A\models \phi \Rightarrow M(A,y)\right) \land     \left(A\not\models \phi \Rightarrow \lnot M(A,y)\right){\huge )} $$