Are there semi-decision procedures for this theory?

It looks to me that you can encode the word problem for groups within the theory of categories in the following way. Pick an object $X$, and then for each generator of the group introduce two morphisms $x,x' : X \to X$, and assume the equalities $x \circ x' = 1_X$ and $x' \circ x = 1_X$. Then you can define the unit to be the identity map, the composition to be the group multiplication, and the negation of a string $x\circ y\circ z$ to be the reverse primed string $z' \circ y' \circ x'$. Hence this problem is undecidable.

However, the word problem is solvable for many specific groups, so if you have more details about the problem this may help. In particular, one idea from the theory of groups which might help you a lot is that absolute presentations of finitely generated groups are solvable -- the inequations can prune the search space enough to make the theory decidable.

EDIT: One additional thought I had is that adding irrelations might still be a useful tool for you, even if the concrete models you're interested validate the equations. This is because in categorical situations you often only want "nice" equations, for some value of nice, and you can use the inequations to rule out solutions that are too evil for you. Your decision procedure might still be incomplete, but you might get a more natural characterization of the solutions it can find than "we search possible proof-trees to a depth of 7".

Good luck; that functor thing you're doing looks pretty cool!


Reduction of graph chromatic number to hypergraph 2-colorability

As the other answer points out, the reduction in the original paper seems to have a bug: $H$ will not be two-colorable unless $G$ is bipartite. I couldn't quite see how to prove the reduction in the other answer works, but here is one that I think does.

The vertices of $H$ will be $\{x_{i, v}: i \in [k], v \in V(G)\} \cup \{z\}$. $H$ has an edge $f_v = \{x_{1,v}, \ldots, x_{k,v}\}$ for every $v \in V(G)$,  and, for each $(u,v) \in E(G)$, and each $i \in [k]$, an edge $\{z, x_{i,u}, x_{i,v}\}$.

Given a coloring $\chi_G:V(G) \to [k]$ of $G$ you can construct a $2$-coloring $\chi_H:V(H) \to \{0,1\}$ of $H$ by setting

$$
\chi_H(z) = 1,\\
\chi_H(x_{i,v}) = 1 \iff \chi_G(v) = i.
$$

It's easy to check that no edge of $H$ is monochromatic.

In the other direction let $\chi_H$ be a proper 2-coloring of $H$, and assume that $\chi_H(z) = 1$. (If this is not the case just rename the colors.) Since no edge $f_v$ is monochromatic, for every $v \in V(G)$ there is some $i$ such that $\chi_H(x_{i,v}) = 1$. Pick an arbitrary such $i$ and set $\chi_G(v) = i$. This is a proper coloring, or otherwise there would be an $i \in [k]$ and an edge $(u,v) \in E(G)$ such that $\chi_H(x_{i,u}) = \chi_H(x_{i,v}) = 1$, which would make the edge $\{z, x_{i,u}, x_{i,v}\}$ of $H$ monochromatic.


What are the reasons that researchers in computational geometry prefer the BSS/real-RAM model?

First of all, computational geometers don't think of it as the BSS model.  The real RAM model  was defined by Michael Shamos in his 1978 PhD thesis (Computational Geometry), which arguably launched the field.  Franco Preparata revised and extended Shamos' thesis into the first computational geometry textbook, published in 1985.  The real RAM is also equivalent (except for uniformity; see Pascal's answer!) to the algebraic computation tree model defined by Ben-Or in 1983.  Blum, Shub, and Smale's efforts were published in 1989, well after the real-RAM had been established, and were almost completely ignored by the computational geometry community.

Most (classical) results in computational geometry are heavily tied to issues in combinatorial geometry, for which assumptions about coordinates being integral or algebraic are (at best) irrelevant distractions.  Speaking as a native, it seems completely natural to consider arbitrary points, lines, circles, and the like as first class objects when proving things about them, and therefore equally natural when designing and analyzing algorithms to compute with them.

For most (classical) geometric algorithms, this attitude is reasonable even in practice.  Most algorithms for planar geometric problems are built on top of a very small number of geometric primitives: Is point $p$ to the left or right of point $q$?  Above, below, or on the line through points $q$ and $r$?  Inside, outside, or on the circle determined by points $q,r,s$?  Left or right of the intersection of segments $qr$ and $st$?  Each of these primitives is implemented by evaluating the sign of a low-degree polynomial in the input coordinates.  (So these algorithms can be described in the weaker algebraic decision tree model.)  If the input coordinates happen to be integers, these primitives can be evaluated exactly with only constant-factor increase in precision, and so running times on the real RAM and the integer RAM are the same.

For similar reasons, when most people think about sorting algorithms, they don't care what they're sorting, as long as the data comes from a totally ordered universe and any two values can be compared in constant time.

So the community developed a separation of concerns between the design of “real” geometric algorithms and their practical implementation; hence the development of packages like LEDA and  CGAL.  Even for people working on exact computation, there is a distinction between the real algorithm, which uses exact real arithmetic as part of the underlying model, and the implementation, which is forced by the otherwise irrelevant limitations of physical computing devices to use discrete computation.

Within this worldview, for example, the most important open problem in computational geometry is the existence of a polynomial-time algorithm for linear programming.  No, the ellipsoid and interior-point methods don't count.  Unlike the simplex algorithm, those algorithms aren't guaranteed to terminate unless the constraint matrix happens to be rational.  (There are combinatorial types of convex polytopes that can only be represented by irrational constraint matrices, so this is a nontrivial restriction.)  And even when the constraint matrix is rational, the running times of those algorithms aren't bounded by any function of the input size (dimension$\times$#constraints).

There are a few geometric algorithms that really do rely heavily on the algebraic computation tree model, and therefore cannot be implemented exactly and efficiently on physical computers.  One good example is minimum-link paths in simple polygons, which can be computed in linear time on a real RAM, but require a quadratic number of bits in the worst-case to represent exactly.  Another good example is Chazelle's hierarchical cuttings, which are used in the most efficient algorithms known for simplex range searching.  These cuttings use a hierarchy of sets of triangles, where the vertices of triangles at each level are intersection points of lines through edges of triangles at previous levels.  Thus, even if the input coordinates are integers, the vertex coordinates for these triangles are algebraic numbers of unbounded degree; nevertheless, the algorithms for constructing and using cuttings assume that coordinates can be manipulated exactly in constant time.

So, my short, personally biased answer is this: TTE, domain theory, Ko-Friedman, and other models of “realistic” real-number computation all address issues that the computational geometry community, on the whole, just doesn't care about.


Isomorphic graph embeddings in the Euclidean Space

This is not possible in general.
The 4-cycle is actually helpful to consider: embedding it in $\mathbb{R}^k$ in the way you describe requires the images of all four vertices to be coplanar, forming a square (since the distances between adjacent vertices must be $1$ and those between the non-adjacent pairs must be $\sqrt{2}$).
Now consider the complete bipartite graph $K_{2,3}$. Let us call its vertices $a_1,a_2,b_1,b_2,b_3$. In any embedding $f$ satisfying your condition, the 4-cycles $(a_1,b_1,a_2,b_2)$, $(a_1,b_1,a_2,b_3)$ and $(a_1,b_2,a_2,b_3)$ would all have to be mapped to squares as above, but the first two of these conditions imply $f(b_2) = f(b_3)$, contradiction.


Is a quadratic nondeterminism speed-up of deterministic computation plausible?

Note that even a result along the lines of $\mathsf{DTime}(\tilde{O}(n^2)) \subseteq \mathsf{NTime}(n^{2-\epsilon})$ would violate NSETH as univariate polynomial identity testing (as defined in section 3.2) can be solved in $\tilde{O}(n^2)$ time deterministically, but there doesn't seem to be an obvious way to use nondeterminism to help prove identity.


The hardness of generating an instance of a problem that is harder than the complexity of the resulting problem

This situation comes up frequently in crypto, where you want to generate hard problem instances along with their solutions. For example, there is the work of Eric Bach (and later, Adam Kalai) on efficiently generating random integers with their prime factorizations.

One of many interesting observations of Impagliazzo and Wigderson (Randomness vs time: derandomization under a uniform assumption. J. Comput. Syst. Sci., 63:672–688, 2001) is that one can efficiently generate uniform random matrices modulo p along with their permanents. (Think about it... use self-reducibility of permanent....) Moreover, we know that the permanent is random self-reducible. So this is an example of a very hard problem for which we can efficiently generate solved instances.


Normal term of double negation of W-type

As an inhabited proposition $(W_{a:A}B(a)\to 0)\to 0$ has only one
term in normal form.

First, without function extensionality, this type cannot be proven to be propositional. Second, propositional types do not necessarily have unique normal forms. Normal forms are up to $\beta\eta$ rules, not propositional equality.
$0 \to 0$ has infinitely many normal inhabitants. Listing a few:
$$\lambda\,x. x$$
$$\lambda\,x. \text{0-elim}\,x$$
$$\lambda\,x. \text{0-elim}\,(\text{0-elim}\,x)$$
Similarly, for any inhabited $A$, $(A \to 0) \to 0$ has infinitely many normal inhabitants.


Which formal language class are XML and JSON with unique keys?

Using BNF with your unique-repetition operator, x := S^ says that an x is an instance a of symbol S, optionally followed by an instance b of set S - a, itself optionally followed by an instance c of set S - a - b, and so forth. If |S| is the number of possible S, and is finite, then 2 ^ |S|! - 1 is the number of possible S^.

It's not really meaningful to talk in terms of the computational power of the language being described, since this is about static semantics, in the twilight between syntax and ordinary (dynamic) semantics. The expressive power of the grammar is extended, since it has a formal means of expressing a particular type of input adaptation.

Specifically, it provides a means of accepting a permutation of a subset of a particular set. I don't think there is any existing name for this class of language. It's certainly not context-free, but the context requirement is at least pretty strictly controlled. If you need a term for it, just coin one. I suggest context-respecting for the class of languages that cannot be described by a context-free grammar without additional embedded information about static semantic constraints, which to be fair are vaguely syntactic in spirit.

The most useful application of this particular extension is probably just the ability to introduce unique-key constraints, but it also lets you describe such interesting sets as x := [0-7]^, which matches any octal number of 8 or fewer non-repeated digits. As for the complexity of it, determining whether an element of the set has been seen is no worse than logarithmic, and the frequency of checking is linear in the number of elements matched, so the ^ operator is indeed decidable in worst-case linearithmic time.


Why can't codes be defined over infinite fields?

Sphere packings give a nice analogue of codes over $\mathbb{R}$. A sphere packing is a set $\mathcal{P} \subset \mathbb{R}^n$ such that $d_{\mathcal{P}} := \inf_{x,y \in \mathcal{P}, x \neq y} \|x - y\| > 0$, where $\|\cdot \|$ is the Euclidean norm. This is called a sphere packing because we can place a(n open) sphere of radius $d_{\mathcal{P}}/2$ at each point in $\mathcal{P}$, and the spheres will not overlap.

There are many nice simple analogies between a code $\mathcal{C} \subseteq \mathbb{F}_q^n$ and a sphere packing $\mathcal{P} \subset \mathbb{R}^n$:

$d_{\mathcal{P}}$ is the minimum distance of the sphere packing, and it is the obvious analogue of the minimum distance of the code: $d_{\mathcal{C}} := \min_{x, y \in \mathcal{C}, x \neq y} \|x - y\|_H$, where $\|\cdot\|_H$ is the Hamming weight. In both cases, this can be viewed as a measure of "how correctable errors are when we encode messages via $\mathcal{C}$ or $\mathcal{P}$ over a noisy channel." E.g., $d_{\mathcal{P}}/2$ is the smallest Euclidean noise that we can add to a point in $\mathcal{P}$ so that we are unable to identify the original point uniquely, while $\lceil d_{\mathcal{C}}/2 \rceil$ is the minimal Hamming noise that can be added to a codeword so that we cannot identify the original codeword uniquely.
The analogue of a linear code is a lattice, $\mathcal{L} := \{ z_1 b_1 + \cdots + z_n b_n \ : \ z_i \in \mathbb{Z}\}$, where the $b_i$ are linearly independent vectors in $\mathbb{R}^n$. The minimum distance of a lattice is just the minimal length of a shortest non-zero vector in $\mathcal{P}$, just like the minimal distance of a linear code is the minimal Hamming weight of a non-zero codeword.
The analogue of the rate of the code $\alpha_{\mathcal{C}} := \log |\mathcal{C}|/\log q^n$ is $\delta_{\mathcal{P}} := \lim_{r \to \infty} \log|\mathcal{P} \cap B(r)|/\log \mathrm{vol}(B(r))$, where $B(r)$ is the Euclidean ball of radius $r$. For a lattice $\mathcal{L}$, we have $|\mathcal{L} \cap B(r)| \sim \mathrm{vol}(B(r))/\det(\mathcal{L})$, where $\det(\mathcal{L})$ is the absolute value of the determinant of the matrix given by the basis vectors $(b_1,\ldots, b_n)$. So, $\delta_{\mathcal{L}} = 1-\log \det(\mathcal{L})$.
For codes $\mathcal{C}$, we're often interested in maximizing the minimum distance $d_{\mathcal{C}}$ for a fixed rate $\alpha_{\mathcal{C}}$. For sphere packings $\mathcal{P}$, we are similarly interested in maximizing $d_{\mathcal{P}}$ for fixed $\delta_{\mathcal{P}}$. Notice that we can always scale a sphere packing $\mathcal{P}$ so that, say, $\delta_{\mathcal{P}} = 0$. So, we can assume without loss of generality that a sphere packing satisfies $\delta_{\mathcal{P}} = 0$. In contrast, it seems that codes with rate $\alpha$ and codes with rate $\alpha'$ are fundamentally distinct objects for $\alpha \neq \alpha'$.

Sphere packings are still an active area of research, both in fixed dimensions and in asymptotically large dimension. E.g., the optimal sphere packings are only known in dimensions 1, 2, 3, 8, and 24 (all achieved by lattices), with 8 and 24 dimensions solved only very recently by Viazovska et al (see http://arxiv.org/abs/1603.04246 and http://arxiv.org/abs/1603.06518). In arbitrarily high dimensions, the current record is held by Venkatesh (http://math.stanford.edu/~akshay/research/sp.pdf). A table of the densest known packings in various dimensions is available here: http://www.math.rwth-aachen.de/~Gabriele.Nebe/LATTICES/density.html.

One can also consider packings of objects other than spheres. E.g., one can replace the Euclidean norm in the definition of $d_{\mathcal{P}}$ by any norm.


The answer to your question is a bit tricky and here are good lecture notes to read to understand the various generalization error bounds. Let me try to summarize what's happening with SVMs and their generalization.  These PAC bounds are also found in "An Introduction to Support Vector Machines: And Other Kernel-Based Learning Methods" by
Cristianini and John Shawe-Taylor.

Assuming a linear classifier correctly classifies all training examples (separable case), one bound (Vapnik '95 (I think)) on the generalization error of a linear classifier is (ignoring log factors):
$$
\epsilon = \tilde{O}\left(\frac{1}{n}\left( \frac{R^2}{\gamma^2} \right)\right),
$$
where $R$ is a bound on the size of the vectors, $n$ is the number of samples, and $\gamma$ is the margin, which is the distance to the support.  This bound says that the margin (the only quantity the learner has control over if the number of training examples are fixed), is an important quantity to maximize in SVM.

However, there is an intuition the margin is maximized in sparse solutions, and the sparseness of a solution is measured by the number of support vectors, so there is a relationship between the generalization bound and the quantity you're interested in.

Another relevant bound for any classifier (not just the linear case) is the following "compression bound" (Littlestone and Warmuth '86), which basically says that if a classifier gets $n$ examples right but can be obtained by training it on just $m$ examples then you can bound its generalization error by
$$
\epsilon \approx \frac{m \log n}{n-m}.
$$
Here, you can think of $m$ as the number of support vectors.  This directly relates the number of support vectors to the generalization error.

These two bounds help explain the interplay between the margins, the number of support vectors, and the generalization ability of an SVM (in the separable case).  In the non-separable case where you do not classify all training examples correctly, you get slack variables, slightly messier bounds, etc.


Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus

Let's split it into two parts:

First let $m$ and $n$ be terms that have a normal form (but are not necessarily in normal form). Let
\begin{align*}
 \mathbf{A} &= \{x \;|\; x =_\beta m\} \\
 \mathbf{B} &= \{x \;|\; x \neq_\beta m \mbox{ and $x$ has a normal form }\}
\end{align*}
These sets are nonempty, disjoint and closed under $\beta$-equivalence, so
we can apply Scott-Curry theorem and conclude that they're inseparable. So there is no algorithm that can determine if two such terms $m$ and $n$ are equal or not.

For the second part: Intuitively, a lambda term cannot distinguish if its arguments are in normal form or not. Suppose we have $f$ that can determine if two terms in normal form $m$ and $n$ are equal or not. Now let $m'$ and $n'$ be terms that have a normal form. We can use a normalizing reduction strategy to reduce them to their normal forms (which is accomplished in a finite number of steps), apply $f$ and determine if they're equal or not, which contradict the previous part.


If you could rename dynamic programming...

Richard Bellman's autobiography suggests that he chose the term “dynamic programming” to be intentionally distracting.

  The 1950s were not good years for mathematical research. We had a very interesting gentleman in Washington named Wilson. He was secretary of Defense, and he actually had a pathological fear and hatred of the word ‘research’.  I'm not using the term lightly; I'm using it precisely.  His face would suffuse, he would turn red, and he would get violent if people used the term ‘research’ in his presence. You can imagine how he felt, then, about the term ‘mathematical’.  The RAND Corporation was employed by the Air Force, and the Air Force had Wilson as its boss, essentially.  Hence, I felt I had to do something to shield Wilson and the Air Force from the fact that I was really doing mathematics inside the RAND Corporation.

  What title, what name, could I choose?  In the first place I was interested in planning, in decision making, in thinking. But planning, is not a good word for various reasons. I decided therefore to use the word ‘programming’. I wanted to get across the idea that this was dynamic, this was multistage, this was time-varying—I thought, let’s kill two birds with one stone. Let’s take a word that has an absolutely precise meaning, namely ‘dynamic’, in the classical physical sense. It also has a very interesting property as an adjective, and that is it’s impossible to use the word ‘dynamic’ in a pejorative sense. Try thinking of some combination that will possibly give it a pejorative meaning. It’s impossible. Thus, I thought “dynamic programming’ was a good name. It was something not even a Congressman could object to. So I used it as an umbrella for my activities.

(As Russell and Norvig point out in their AI textbook, however, this story must be a creative embellishment of the truth.  Bellman first used the phrase "dynamic programming" in 1952, and Charles Erwin Wilson did not become Secretary of Defense until 1953.)

Anyway, Bellman's original motivation suggests multistage planning, but at least for algorithmic purposes, I'd prefer something like frugal bottom-up recursion, only with fewer syllables.


Intuition behind the Charikar's LP formulation for densest subgraph problem

Depending on how people interpret "research-level", this might need to be moved to cs.stackexchange.com.

The intuition becomes more apparent if you first write down an alternate similar looking but not necessarily linear mathematical program

$$\begin{eqnarray}
\textrm{maximize}\,\,&\tfrac{\sum_{(i,j) \in E} x_{ij}}{\sum_{i \in V} y_i}& \\
\textrm{subject to}\,\,& x_{ij} \leq y_i& \forall {(i,j) \in E}\\
& x_{ij} \leq y_j& \forall {(i,j) \in E} \\
& 0 \leq x_{ij} \leq 1 &\forall {(i,j) \in E} \\
& 0 \leq y_i \leq 1 &\forall {i \in V} \\
\end{eqnarray}$$

Integer solutions to this program have a simple interpretation, with $y_i = 1$ iff vertex $i$ is in a chosen subgraph, $x_{ij} = 1$ only if $(i,j)$ is an edge in the subgraph induced by the selected vertices, and the objective function coming directly from the definition of the densest subgraph. Unfortunately, the objective function as written is not valid for an LP.

The key observation is that the objective function is scale-free, in that dividing all $x_{ij}s$ and $y_i$s of a feasible solution by the same constant value $k \geq 1$ does not affect either feasibility of a solution or its corresponding objective function value. Hence, we can without loss of generality restrict our attention to the case that $\sum_{i \in V} y_i = 1$ (otherwise, we can divide all LP variables by exactly $k=\sum_{i \in V} y_i$ to ensure this). We make this restriction explicit by adding in the constraint $\sum_{i \in V} y_i = 1$. But, with this constraint in hand, the denominator of the objective function for the above program is exactly $1$. Hence, we can remove it from the objective, leaving us with something that is linear, and in particular with the LP in the original post.


Is there any justification to believe that $NL\neq L$?

First, let me cite skepticism that $L \neq NL$. As it has been shown that undirected graph connectivity is in $L$ (Reingold), and that $NL=coNL$ (Immerman-Szelepcsényi), I think that confidence in $L \neq NL$ has only decreased. Some prominent researchers have never had a strong belief. For example, Juris Hartmanis (founder of the CS department at Cornell and Turing award winner) has said:

  We believe that NLOGSPACE differs from LOGSPACE, but not with the same depth of conviction as for the other complexity classes. (Source)

I know he said similar things in the literature as far back as the 70's.

There is some evidence against $L=NL$, although it is circumstantial. There has been work on proving space lower bounds for $s$-$t$ connectivity (the canonical $NL$-complete problem) in restricted computational models. These models are strong enough to run the algorithm of Savitch's theorem (which gives an $O(\log^2 n)$ space algorithm) but are provably not strong enough to do asymptotically better. See the paper "Tight Lower Bounds for st-Connectivity on the NNJAG Model". These NNJAG lower bounds show that, if it's possible to beat Savitch's theorem and even get $NL \subseteq SPACE[o(\log^2 n)]$, one will certainly have to come up with an algorithm that's very different from Savitch.

Still, I don't know of any unlikely, unexpected formal consequences that come from $L=NL$ (except for the obvious ones). Again, this is primarily because we already know things like $NL=coNL$.


Example problems with polynomial and exponential solutions, and tiny footprint?

You could do regular expression matching. A naive backtracking matcher can easily be pushed into exponential behavior on inputs that a smarter matcher can handle in linear time.


Uniform hierarchy of problems that span complexity and computational hierarchies

[Building off of Kaveh's insight in the comments.] It seems unlikely that someone could come up with a family of problems that is significantly different from quantified boolean formula, without disproving the PH-analog of the Berman-Hartmanis isomorphism conjecture.  Without that, any problem you come up with would be not only equivalent to $QBF_k$, but in fact isomorphic to it. One way to define isomorphism between two languages here is to take a single abstract language, but encode its objects (in this case, quantified boolean formulae) using two different boolean encodings.

On the other hand, isomorphism isn't necessarily a good judge of what's useful for people to come up with proofs.  After all, in the arithmetic hierarchy, Myhill's Isomorphism Theorem proves the arithmetic analog of the BH isomorphism conjecture (in fact, that's history backwards since BH was motivated by Myhill).  Yet, as the question points out, there are several "different-looking" characterizations of various levels, some of which are more useful for proofs than others.

Although it seems unlikely that anyone will come up with such a uniform family of languages for every level of PH, the two surveys (one, two) by Schaefer and Umans discuss natural problems that at least "look different" from QBF for the first few levels of PH.


Convergence theorem for Genetic Programming?

I am not sure that there is one Theorem to point to. Anyhow, you will probably be interested in the following reference, which summarizes many more recent results than those you mention in the question, e.g., for the (1+1)-EA with linear functions, quadratic functions, and monotone polynomials as objective functions (I know these are probably much simpler functions than you care about). Anyway the citations within should give you good pointers, via Google Scholar, to even newer results.

Stefan Droste, Thomas Jansen, Günter Rudolph, Hans-Paul Schwefel, Karsten Tinnefeld, and Ingo Wegener (2002): Theory of evolutionary algorithms and genetic programming.  In H.-P. Schwefel, I. Wegener, and K. Weinert (Eds.): Advances in Computational Intelligence Theory and Practice. Springer, Berlin, Germany, pages 107-144.


Problems that are NP-complete under randomized or P/poly reductions.

As suggested by Peter, I converted my comment into an answer.

Valiant-Vazirani Theorem states that if Unique SAT $\in P$ then $NP=RP$. To prove their theorem they showed that the promise problem Unique SAT is $NP$-hard under randomized reductions.

[1] Valiant, Leslie; Vazirani, Vijay. "NP is as easy as detecting unique solutions", Theoretical Computer Science, 47: 85–93


Efficient Shamir secret sharing reconstruction

Yes. If you choose the evaluation poitns for the polynomial carefully, this problem is the same as correcting erasures in the Reed-Solomon encoding of a message, and there are faster algorithms for that problem.

http://en.wikipedia.org/wiki/Reed%E2%80%93Solomon_error_correction


No, there is no information-theoretic analog that is secure against computationally-unbounded adversaries.

To form an analog, we'd need an injection $\varphi$ that maps $x$ in fine representation to $x$ in coarse representation.  But then Diffie-Hellman involves Alice sending $\varphi(x)$ publicly, and Bob sending $\varphi(y)$ publicly.  An eavesdropper can see $\varphi(x),\varphi(y)$.  Since $\varphi$ is an injection, information-theoretically this reveals $x,y$, which is enough to reveal the negotiated key.

What if we consider a function $\varphi$ that is non-injective?  This doesn't help.  Consider the equivalence relation $\sim$ where $x \sim x'$ if $\varphi(x)=\varphi(x')$, and let $[x]$ be the equivalence class of $x$.  Then for the scheme to work, the negotiated secret has to depend only on $\varphi(x),y$, i.e., only on $[x],y$ (since Bob has to be able to compute it).  Similarly, the negotiated secret has to depend only on $x,[y]$.  It follows that the negotiated secret depends only on $[x],[y]$.  Why?  Let $f(x,y)$ denote the secret negotiated if Alice uses fine value $x$ and Bob uses fine value $y$.  Suppose $x \sim x'$ and $y \sim y'$.  Then since $[x]=[x']$, it follows that $f(x,y)=f(x',y)$ (since $f(x,y)$ depends only on $[x],y$).  Also since $[y]=[y']$, it follows that $f(x',y)=f(x',y')$ (since $f(x,y)$ depends only on $x,[y]$).  Therefore $f(x,y)=f(x',y')$ whenever $x=x'$ and $y=y'$.  In other words, the final negotiated secret depends only on $[x],[y]$.  However, the eavesdropper can observe $\varphi(x),\varphi(y)$, from which $[x],[y]$ are uniquely determined and thus the negotiated secret is uniquely determined and thus information-theoretically cannot be hidden from the eavesdropper.

Public-key exchange can only be secure computationally -- you can't achieve information-theoretically secure public-key exchange.


Enumerating all (super)orientations of an undirected graph

For complete graphs:

Order the possible-directed-edges as [[1,0],[2,0],...,[|V|-1,0],[0,1],[2,1],...,[|V|-1,1],[0,2],[1,2],...,[|V|-1,2],...,[0,|V|-1],[1,|V|-1]],[2,|V|-1],...,[|V|-2,|V|-1]], and imagine the perfect binary rooted tree whose levels correspond to initial segments of the possible-edges under that ordering,

and whose nodes correspond to which of those possible edges are/aren't present.

Do roughly a depth-first search on that tree without actually constructing the tree,

where you do ignore tree-edges that would make neither [u,v] nor [v,u] be present

and you can ignore tree-edges that would necessarily make [number_of_superorientation_edges_to_(i+1),number_of_superorientation_edges_from_(i+1)] lexicographically less than [number_of_superorientation_edges_to_(i),number_of_superorientation_edges_from_(i)].

Output the leaves that search reaches.  In Python:

n  =  number of vertices
possibilities = tuple([(i,j) for j in range(n) for i in range(n) if j!=i])

def might_be_valid_and_canonical_(choices):
 for v in range(n):
  for u in range(v):
   i = possibilities.index((v,u))
   if (i < len(choices)) and not choices[i]:
    j = possibilities.index((u,v))
    if (j < len(choices)) and not choices[j]:
     return False
 max_out_of,max_into,min_out_of,min_into = [0]*n,[0]*n,[0]*n,[0]*n
 for i in range(len(choices)):
  if choices[i]:
   u,v = possibilites[i]
   max_out_of[u] += 1
   max_into[v] += 1
   min_out_of[u] += 1
   min_into[v] += 1
 for (u,v) in possibilities[len(choices):]
   max_out_of[u] += 1
   max_into[v] += 1
 for i in range(n-1):
  if (max_into[i+1],max_out_of[i+1]) < (min_into[i],min_out_of[i]):
   return False
 return True

numedges = n*(n-1)

def superorientations():
 if n<2:
  raise NotImplemented
 choices,try_child = tuple(),0
 while True:
  LofC = len(choices)
  if LofC == numedges:
   yield [possibilities[i] for i in range(numedges) if choices[i]]
   try_child = int(choices[LofC-1])+1
   choices = choices[:LofC-1]
   continue
  if try_child == 0:
   if might_be_valid_and_canonical_(choices+(False,)):
    choices += (False,)
    continue
   try_child = 1
  if try_child == 1:
   if might_be_valid_and_canonical_(choices+(True,)):
    choices += (True,)
    try_child = 0
    continue
   try_child = 2
  if try_child == 2:
   LofC = len(choices)
   if LofC == 0:
    return
   try_child = int(choices[LofC-1])+1
   choices = choices[:LofC-1]

For nearly-complete graphs, you can do that to the subgraph consisting of the

vertices with degree |V|-1, and output the extensions of those to the whole graph.


Gaussian Elimination in terms of Group Action

In the case of determinant, Gaussian elimination can indeed be seen as equivalent to the idea that the determinant has a large symmetry group (of a particular form) and is characterized by that symmetry group (meaning any other homogeneous degree $n$ polynomial in $n^2$ variables with those symmetries must be a scalar multiple of the determinant). (And, as to @Tsuyoshi Ito's point that the symmetries of the permanent seem not to help compute it efficiently: although the permanent is also characterized by its symmetries, its symmetry group is much smaller than that of the determinant.)

You can find a write-up of this - where the symmetries of the determinant are used to do Gaussian elimination, along the way proving that the determinant is characterized by its symmetries - in Proposition 3.4.3 of my thesis (shameless self plug - but also, I've never seen it phrased quite this way before and written in full detail, as the OP was asking for, though I'm sure it's been done; I'd be happy if someone had other references).

As to the idea that symmetry always leads to complexity reduction (or not), in addition to things already in the comments, see this question and its answers.

An interesting point is that in Valiant's first papers on what is now known as Valiant's version of algebraic complexity theory, he was trying to make the point that one reason the determinant is important computationally is because roughly all the (then) known efficient algorithms could be reduced to linear algebra and thence to the computation of the determinant, e.g. the FKT algorithm for counting matchings in planar graphs. This is of course an exaggeration, but continues to be borne out by research into holographic algorithms, which often reduce to computing the Pfaffian (a close relative of the determinant). Surely Valiant knew this was an exaggeration, but here's the exact quote just to make sure I'm not misrepresenting (L. Valiant. Completeness classes in algebra. ACM STOC 1979):

  Our main conclusions can be summarized roughly as follows:

  (a) Linear algebra offers essentially the only fast technique for computing multivariate polynomials of moderate degree

  (b) ...


Are there any cases where quantum has given insight for classical algorithms?

There is at least one example that I can remember, but there are probably more that I am not aware of.

Recently, Maarten Van den Nest and Wolfgang Dürr found a  new classical algorithm (arXiv:1304.2879) to approximate certain types of partition functions (of 3-body classical Ising models on two-dimensional lattices.  Their algorithm is completely classical, but several connections to quantum physics are employed in the design (read below). The algorithm was found to be exponentially faster than previously known algorithms that solve the same problem, at the time of writing*.

*I am ignorant of whether better classical or quantum algorithms have been found a posteriori.

So, there are at least two quantum ingredients used in the design of the VdND algorithm. On the one hand, the authors use a classical-quantum connection between classical Ising models and topological quantum systems (precisely, some color codes). On the other hand, the authors use classical techniques to simulate quantum systems in the derivation of the algorithm: in their proof, they first write a small quantum algorithm for the problem of interest; then, the authors show how to simulate the former quantum  algorithm efficiently on a classical computer, obtaining a classical algorithm (this is rather remarkable, in my view).


Independent set size of a large girth graphs

Bollobas showed that for any $d$ and any $g$, there exists a $d$-regular graph $G$ of girth at least $g$ such that

$$
\alpha(G) < \frac{2n\log d}{d}.
$$

So you cannot hope for more than a factor 16 improvement. McKay gave somewhat sharper bounds.


If I don't misunderstand what you mean by AND&OR gate, it is basically a comparator gate which takes two input bits $x$ and $y$ and produces two output bits $x\wedge y$ and $x\vee y$. The two output bits $x\wedge y$ and $x\vee y$ are basically min$(x,y)$ and max$(x,y)$.

Comparator circuits are built by composing these comparator gates together but allowing no more fan-outs other than the two outputs produced by each gate. Thus, we can draw comparator  circuits using the notations below (similarly to how we draw sorting networks).

We can define the comparator circuit value problem (CCV) as follows: given a comparator circuit with specified Boolean inputs, determine the output value of a designated wire. By taking the closure of this CCV problem under logspace reductions, we get the complexity class CC, whose complete problems include natural problems like lex-first maximal matching, stable marriage, stable roomate.

In this recent paper, Steve Cook, Yuval Filmus and I showed that even when we use AC$^0$ many-one closure, we still get the same class CC. To the best of our knowledge at this point, NL $\subseteq$ CC $\subseteq$ P. In our paper, we provided evidence that CC and NC are incomparable (so that CC is a proper subset of P), by giving oracle settings where relativized CC and relativized NC are incomparable. We also gave evidence that CC and SC are incomparable.


Complexity of $\oplus$ 3-REGULAR BIPARTITE PLANAR VERTEX COVER

Ok, according to the paper Accidental algorithms by Valiant, the  problem ⊕Pl-3/2Bip-Mon-2CNF is ⊕P-complete. So ⊕ 3-REGULAR PLANAR VERTEX COVER would also have to be ⊕P-complete. So it's not in P (unless P = ⊕P-complete).
But I still don't know if ⊕ 3-REGULAR BIPARTITE PLANAR VERTEX COVER is ⊕P-complete.


Are there any parameterized problems in non-uniform FPT that are suspected (but not proven) to be in uniform-FPT?

In Downey and Fellows' 2013 book (Fundamentals of Parameterized Complexity; Section 2.2), they mention an example of a problem in non-uniform FPT (Graph Linking Number) and briefly discuss that it's open whether this problem is in uniform FPT. This problem seems fairly natural.

When considering non-uniform parameterized complexity, one can look at many different variants, and many of them do have some relations to (non-uniform) circuit complexity. As far as I know, this hasn't been explored much.

For an overview of some basic connections, you could have a look at a report that I wrote: An Overview of Non-Uniform Parameterized Complexity.


A problem that is in PSPACE but not known to be in PH?

The existential theory of the reals is known to be contained in PSPACE, but it is not known whether it is contained in PH. So take the existential theory of the reals, or any of the many equivalent problems.


Is there a theory to answer "the simplest program to solve a problem"?

This problem is studied in Algorithmic Information Theory. What you're defining is called Kolmogorov-Chaitin complexity.

http://en.wikipedia.org/wiki/Kolmogorov_complexity

And it seems that the notion of simplicity that you're requiring can be formalized via the notion of complexity measure, which is formalized by Blum's axioms.

http://en.wikipedia.org/wiki/Blum_axioms

It seems also that it is possible to generalise Kolmogorov's complexity to take
other complexity measures into consideration. See reference below. (Wikipedia's article on Kolmogorov complexity addresses this issue.)

Burgin1990- Generalized kolmogorov complexity and other dual complexity measures
Cybernetics and Systems Analysis Volume 26, Number 4, 481-490


Are both safety and liveness properties closed under finite intersection?

Safety properties are closed under finite intersection. This can be seen by following Alpern and Schneider's characterisation which showed that safety properties are limit-closed when viewed topologically.

Liveness properties as defined by Alpern and Schneider are dense. They are not closed under intersection as soon as there are two elements in the state space. Consider the two-element state space $\{0,1\}$. For state $i$ define $a_i$ as the set of infinite sequences of states that have a suffix consisting of $i$ only. Each $a_i$ is a liveness property but $a_0 \cap a_1 = \emptyset$ cannot be a liveness property because it's not dense.


The decision procedure of theory of closed real field is in NP-hard?

Yes, even in the purely existential case. See https://en.wikipedia.org/wiki/Existential_theory_of_the_reals


An exponentially-ambiguous weighted automaton without an equivalent polynomially-ambiguous automaton

Here is a natural candidate: the alphabet is $\{a,b,c\}$, and to a word $v=u_1cu_2c\dots cu_k$ with each $u_i\in\{a,b\}^*$, you want to associate $$f(v)=\sum_{i=1}^k \min(|u_i|_a,|u_i|_b)$$

There is a straigthforward exponentially ambiguous automaton for this $f$: each time you see a $c$, guess if you go to a state counting $a$'s or to a state counting $b$'s.
It should not be too hard to prove that only exponentially ambigous automata recognize this function $f$. As a very sketchy argument, consider the fact that between two $c$'s, you must either count the number of $a$ or the number of $b$, so you need two different states to do so. Since you must be able to oscillate between these states, it means that you have distinct paths of the form $p\stackrel{w}{\longrightarrow} p$ for some state $p$ and word $w$ (containing some $c$'s).


Are there descriptive complexity representations of quantum complexity classes?

Gurevich in formulating the conjecture about a logic that could capture $\mathsf{P}$ requires the logic to be computable in two ways: (1) the set of sentences legally obtainable from the vocabulary $\sigma$ has to be computable, given $\sigma$; and (2) the satisfiability relation needs to be computable from $\sigma$, i.e., ordered pairs consisting of a finite structure $M$ and a sentence $\varphi$ such that all models isomorphic to $M$ satisfy $\varphi$.  Also, significantly for comparison with this randomized logic result, the vocabulary $\sigma$ has to be finite.  (A vocabulary is a set of constant symbols and relation symbols, for example, equals sign, less-than sign, $R_1,R_2,\ldots$)  This is a paraphrase of Definition 1.14 of this paper by Gurevich, which is reference [9] in the quote Kaveh gave.

The paper about BPP and randomized logic presents a significantly different framework.  It starts with a finite vocabulary $\sigma$, and then considers a probability space of all vocabularies that extend $\sigma$ with some disjoint vocabulary $\rho$.  So a formula is satisfiable in the new randomized logic if it is satisfiable in "enough" logics based on extensions of $\sigma$ by different $\rho$.  This is my butchering of Definition 1 in the Eickmeyer-Grohe paper linked to by Robin Kothari.  In particular, the vocabulary is not finite (well, each vocabulary is, but we have to consider infinitely many distinct vocabularies), the set of sentences of this logic is undecidable, and the notion of satisfiability is different from the one put forth by Gurevich.


SAT Solution Space - Definition of Cluster of Solutions

I think a cluster of solutions is a maximal set of solutions $T$ s.t. you can reach every $\tau' \in T$ from every other $\tau \in T$ by a sequence of solutions $\{\tau_i\}_{0\leq i\leq n}$ ($\tau = \tau_0$ and $\tau' = \tau_n$) where the hamming distance between each consecutive pair of solutions is bounded, i.e. they are just connected components in the graph where two solutions are adjacent iff the hamming distance between them is less than the bound.

See these notes by Dimitris Achlioptas (or papers on statistical physics and random k-SAT).


Does There exist a particular PSPACE Complete Problem which has a FPTAS algorithm?

It is possible to define artificial PSPACE-HARD problems with an FPTAS: define $f(x)=2^{|x|}+g(x)$
where $g(x)$ is a Boolean PSPACE-hard problem whose complexity is at most $2^n$, then $f$ is also PSPACE-hard, but it has an FPTAS: if $\epsilon \gt 2^{-|x|}$ then return $2^{|x|}$ else we have enough time to compute $f$ exactly.


Examples of the use of biased estimators

In machine learning, the sample error of an ERM learner is a biased estimator of the true generalization error. Here the bias is not by choice but by necessity: we simply don't know of a way to construct an unbiased estimator of the generalization error, and I'm pretty sure it's impossible from general no-free-lunch principles.


It is an open problem in complexity theory for many years if $\mathsf{PH}^{\mathsf{\#P}}$ collapse,
where $\mathsf{PH}$ is the polynomial time hierarchy. It is also an open problem to construct
an oracle to separate $\mathsf{P}^{\mathsf{\#P}}$ from $\mathsf{PSPACE}$.


Are there any propositional proof systems which are not Cook-Reckhow proof systems?

Natural examples of propositional proof systems that do not fall under this definition are algebraic proof systems where the lines in the proof are arbitrary polynomials (not necessarily fully expanded). To verify the correctness of such proofs, among other things one has to test the identity of polynomials, which is not known to be possible in deterministic polynomial time.

Cf. the paper "Algebraic propositional proof systems" by Toni Pitassi, in  DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Volume 31, Descriptive Complexity and Finite Models, Immerman and Kolaitis (Eds.), pp. 215-244, 1996.


The PCP Theorem is a theorem about checking proofs, i.e. that there exist locally checkable proof systems, ones that don't "turn from non-accepting to accepting by changes that would be insignificant by any reasonable metric" (quote, top of page 2 here).

Simply stated, it's not directly related to "efficient computation" at all -- more of "efficient checking," for an appropriate definition of efficient.

I suppose it might be possible to use the machinery and terminology of PCPs to attack P vs NP, but it seems likely that such an argument would have a simpler statement under a different model and mode of thought to me. If nothing else -- I haven't seen any attempts in that direction.


Approximating the clique size of the graph

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


It is not possible for linear bounded automata to check whether C++ programs, and unlikely to be possible for and LBA to check whether SML programs are well-typed. C++ has a Turing-complete type system, since you can code arbitrary programs as template metaprograms.

SML is more interesting. It does have decidable type checking, but the problem is EXPTIME-complete. Hence it is unlikely an LBA can check it, unless there is a very surprising collapse in the complexity hierarchy. The reason for this is that SML requires type inference, and there are families of programs the size of whose type grows much faster than the size of the program. As an example, consider the following program:

fun delta x = (x, x)        (* this has type 'a -> ('a * 'a), so its return value
                               has a type double the size of its argument *)

fun f1 x = delta (delta x)  (* Now we use functions to iterate this process *)
fun f2 x = f1 (f1 x)
fun f3 x = f2 (f2 x)        (* This function has a HUGE type *)

For simpler type systems, such as C or Pascal's, I believe it is possible for an LBA to check it.

In the early days of programming languages research, people sometimes used van Wingaarden grammars (aka two-level grammars) to specify type systems for programming languages. I believe Algol 68 was specified in this way. However, I am told this technique was abandoned for essentially pragmatic reasons: it turned out to be quite difficult for people to write grammars that specified what they thought they were specifying! (Typically, the grammars people wrote generated larger languages than they intended.)

These days people use schematic inference rules to specify type systems, which is essentially a way of specifying predicates as the least fixed point of a collections of Horn clauses. Satisfiability for first-order Horn theories is undecidable in general, so if you want to capture everything type theorists do, then whatever grammatical formalism you choose will be stronger than is really convenient.

I know there has been some work on using attribute grammars to implement type systems. They claim there are some software engineering benefits for this choice: namely, attribute grammars control information flow very strictly, and I am told this makes program understanding  easier.


Implications of proving NP=RP on complexity theory

Prelude: the below is just one consequence of $\mathsf{RP}=\mathsf{NP}$ and probably not the most important, e.g. compared to collapse of the polynomial hierarchy. There was a great and more comprehensive answer than this, but its author removed it for some reason. Hopefully the question can continue to get more answers.
$\mathsf{P}/\mathsf{poly}$ is the set of decision problems solvable by polynomial-size circuits. We know $\mathsf{RP} \subseteq \mathsf{BPP}$ and, by Adleman's theorem, $\mathsf{BPP} \subseteq \mathsf{P}/\mathsf{poly}$. So among the only mildly shocking implications of $\mathsf{RP}=\mathsf{NP}$ would be $\mathsf{NP} \subseteq \mathsf{P}/\mathsf{poly}$.
Another way to put it is that instead of each "yes" instance of an $\mathsf{NP}$ problem having its own witness, there would exist for each $n$ a single witness string that can be used to verify, in polynomial time, membership of any instance of size $n$.


There are plenty such typing systems.

Most work is based on the linear/affine typing system introduced
in (1) and generalised in (2). Here are the main works on this subject.
In (3) the typing system ensures a precise match with PCF (int its call-by-name variant -- changing to call-by-value is easy).
In (4) the typing system gives a precise interpretation of the
simply typed λ-calculus. (5) does the same thing for System F, (6) does the same for the λμ-calculus.

The typing systems in  (3, 4, 5, 6) are precise in the sense that the inhabitants of translations of λ-calculus types
"are processes coming from lambda expressions", at least up to $\simeq$ (weak typed bisimulation). More precisely, if $\alpha$ is a type in the λ-calculus, and $\Gamma = x_1 : \beta_1, ..., x_n : \beta_n$ is a corresponding typing environment, then the processes $P$ that are typable
as

$$
   \vdash P \triangleright x_1 : \overline{\langle\beta_1\rangle}, ..., x_n : \overline{\langle\beta_n\rangle}, u : (\langle\alpha\rangle)^{\uparrow}
$$

are (up to $\simeq$) the translations of λ-terms $M$ with

$$
   \Gamma \vdash M : \alpha
$$

(Here $\langle \alpha \rangle$ is the translation of a λ-type $\alpha$ into π-types, and
$\overline{\tau}$ the dualisation of the π-type $\tau$.) The translations
are fully abstract in the sense that

$$
M =_{\beta\eta} N
\quad\text{iff}\quad
\langle M \rangle_u \simeq \langle N \rangle_u
$$
(Here $\langle M \rangle_u$ is the translation of $M$, located at $u$.) So the embedding is as precise as one can hope for. (NB, I'm skating over some details above, for ease of presentation.)  Note  that the systems in (3, 4, 5, 6) are closely related -- indeed they are in some sense the same system, although this viewpoint has not yet been published.

If you want a brief summary of how those typing systems ensure confluence, then it is this: they ensure that there is always at most one active output (i.e. an output not under a prefix). This is brutal/syntactic.

Session types (7, 8) can also be used for this purpose, but the
correspondence is not that precise, in parts because session
types are not as constraining as the types deriving
from (1). See (9) as an example where sessions are used to model
effects (such as state) in PCF.

Davide Sangiorgi and others have also worked on this problem,
see (10) for a summary.

Aside: as the question correctly guesses, λ-calculus can be seen as an especially well-behaved form of message passing, a viewpoint  put forward 1976 in Carl Hewitt's pioneering work (11) in the  actors tradition. The typing systems above essentially constrain π-calculus so only this well-behaved  message passing is typable. Coincidentally, Milner invented the π-calculus in parts to give a formal model of actors. In hindsight, as (12) explains nicely, there is a small mismatch between actors and π-calculi.

K. Honda, V. Vasconcelos, N. Yoshida: Secure Information Flow
as Typed Process Behaviour.
K. Honda, N. Yoshida, A uniform type structure for secure information flow.
M. Berger, K. Honda, N. Yoshida: Sequentiality and the Pi-Calculus
N. Yoshida, K. Honda, M. Berger: Strong Normalisation in the Pi-Calculus
M. Berger, K. Honda, N. Yoshida: Genericity and the Pi-Calculus
K. Honda, N. Yoshida, M. Berger: Control in the Pi-Calculus
K. Takeuchi, K. Honda, M. Kubo, An Interaction-based Language and its Typing System.
K. Honda, V. T. Vasconcelos, M. Kubo, Language Primitives and Type Disciplines for Structured Communication-based Programming.
D. Orchard, N. Yoshida, Effects as sessions, sessions as effects.
D. Sangiorgi, D. Walker:  The π-Calculus: A Theory of Mobile Processes
C. Hewitt, Viewing Control Structures as Patterns of Passing Messages.
S. Fowler, S. Lindley, P. Wadler, Mixing Metaphors: Actors as Channels and Channels as Actors.


For question $1$: any bidimensional parameter has this property on general graphs. A parameter $s(G)$ is bidimensional if the value of $s(G) \geq s(H)$ for every minor $H$ of $G$, and if $s$ is ``large'' on grids.
In applications to PTASes, sub exponential algorithms and kernels on minor-free classes of graphs, "large" means that there exists a constant $c$, such that the value of $s$ on a $t$ times $t$ grid is at least $ct^2$. This is what you most likely will find if you do a google search for ``bidimensionality''
However, for your question it is sufficient that $s$ grows to infinity on $t$ times $t$ grids as $t$ grows to infinity. This is because any graph with large enough treewidth will contain a large enough grid minor. So, to conclude, if $s$:

is closed under minors
is arbitrarily large on $t$ times $t$ grids for large enough $t$

Then s has the s-treewidth property. See the recent parameterized complexity book ( http://parameterized-algorithms.mimuw.edu.pl ) in the treewidth chapter for more info.


Just a partial self-answer: I think the problem is NP-complete.

I found 3 gadgets (each one occupies $16 \times 16$ cells) that allows to build a Net game equivalent to a grid graph of degree $\leq 3$ and that should have a solution iif the original graph has an Hamiltonian cycle. The figure shows four different configurations of the gadget equivalent to a node with degree 3 (the full picture can be downloaded here).

The gadget SHOULD have the following properties (I'll try to check them with a constraint solver):

it can be linked to other gadgets only through the 3 interface pairs of corner wires ($A$, $B$, $C$);
the two wires of an interface pair must be directed both outwards or both inwards (otherwise there is an open ended wire or a cycle in the inner part of the gadget);
the gadget must be entered/exited exactly twice and from exactly two interface pairs (the green zones of the first three figures show the traversals A-C, B-C, A-B);
exactly two interface pairs must be directed outward (the red zone in the figure shows what happens if the three interface pairs are all directed outward);

The gadgets equivalent to nodes of degree 2 and 1 are similar (and we can also build "fill" gadgets to fill the holes of the original grid graph).

Now replacing the two central cells of one gadget with the central unit that sends the power on one direction and a terminal at the other endpoint, the game SHOULD have a solution iif the original graph has an Hamiltonian cycle.


Is $\mathsf{MA}$ equal to $\mathsf{NP}^\mathsf{RP}$?

In the first bullet, we would need the oracle to answer

YES, if Arthur’s check succeeds with probability $1$ (assuming the MA protocol has perfect completeness),
NO, if Arthur’s check succeeds with probability $\le 1/2$.

This sounds like a coRP algorithm, but the catch is that there is no guarantee that one of these two conditions applies for every possible input to the oracle. Thus, the oracle does not compute a coRP language, but a coRP promise problem, and the whole argument only shows that $\mathrm{MA}\subseteq\mathrm{NP}^{\mathrm{promiseRP}}$.


Algorithm for 'k'' most frequently occurring numbers

There's an extensive literature on this problem. Firstly, even for $k=1$, the problem is hard: as Alon, Matias and Szegedy show, you can't get a better than constant factor approximation to the frequency of the most popular element in $o(n)$ space, even if you're willing to be randomized.

However, if you're guaranteed that one element occurs strictly more than 50% of the time, then there's a simple trick that uses constant space and will find it (this is a popular google puzzle question). More generally, you can find elements that occur more than $n/k$ times using a generalization of this trick.

A definitive survey of what's known about the problem is the paper by Cormode and Hadjileftheriou from VLDB 2008. It covers the above methods and many of the latest methods. the general idea is that you can generate an approximate list of the top $k$ items (where approximate here means that you might get items whose counts are close to the counts of the top $k$ items).


Regular relations

All of them are regular relations, assuming the rules are applied only once and assuming we don't have to deal with overlapping matches.

You have to be a bit careful when specifying these kinds of rules to determine what you want to happen if there are multiple places where the rule might apply.  I'm going to assume that the rule avoids ambiguity (e.g., always pick the leftmost match), and that the rule is applied only once, so that the rule can be implemented by scanning from left-to-right over the string in a single pass.

With that clarification, all of these are regular relations, i.e., can be implemented as a (possibly non-deterministic) finite-state transducer.  There are two rules whose intended meaning wasn't entirely clear to me, so let me discuss each in more detail:

"if the string contains a /d/ with a /g/ anywhere later than it, map that /d/ to /t/": I can see two possible meanings, both regular:

"if the string contains a /d/ with a /g/ anywhere later than it, map the leftmost /d/ to /t/": a regular relation. or,
"if the string contains a /d/ with a /g/ anywhere later than it, map all /d/'s that precede the last /g/ to /t/": also a regular relation.

"if the string contains a /w/ and a /y/ with anything intervening, swap around the /w/ and the /y/": This requires more care.  I can see two possible meanings:

Perhaps you mean to scan for the first /w/, then for the first /y/ after it, and if found swap the /w/ and /y/ and then continue scanning the rest of the string after that.  If so, that's a regular relation.
However, if you meant to pair up the /w/'s and /y/'s in a nested fashion (leftmost /w/ with rightmost /y/, and so on) and swap them all (e.g., /wwwwyyyy/ becomes /yyyywwww/), then that's not a regular relation.  Or, to put it another way, if you meant that the rule should be applied repeatedly until no further changes occur, it's not a regular relation.

I'll assume you meant the former.

Deterministic finite-state transducers

That said, the notion of regular relation might not be the notion you are looking for.  A mapping forms a regular relation if and only if it can be applied by a, possibly non-deterministic, finite-state transducer.  Unfortunately, non-deterministic finite-state transducers are not as convenient as deterministic finite-state transducers.  There are two problems:

Ambiguous output: Given a single input word and a non-deterministic finite-state transducer, there might be multiple possible outputs.  I suspect you want your rules to correspond to deterministic functions, so each input string corresponds to a single output string.  (Otherwise, there's ambiguity about what the input string should map to.)  If so, non-deterministic transducers are too powerful.  You might want to restrict attention to deterministic finite-state transducers or unambiguous finite-state transducers, which ensure that each input corresponds to just one possible output.
Efficient simulation: Given a single input string and a deterministic finite-transducer, you can very efficiently compute the corresponding output string by just simulating the transducer.  However, the same is not true for non-deterministic finite-state transducers (not even unambiguous finite-state transducers).  Therefore, you might want to restrict attention to deterministic finite-state transducers.

With that motivation, we can ask a follow-up question: which of these rules can be modelled by deterministic finite-state transducers?  The answer is that all but two of those rule can be implemented as a deterministic finite-state transducer.

The two that cannot are:

"if the string contains a /d/ with a /g/ anywhere later than it, map that /d/ to /t/"
"if the string contains a /w/ and a /y/ with anything intervening, swap around the /w/ and the /y/"

Those two cannot be implemented with a deterministic finite-state transducer, because they require unbounded memory.  After you see a /d/, you can't output anything: you have to keep scanning until you see a /g/ and meanwhile save everything you've seen.  There's no limit to how much you might need to remember, because there's no limit to how long you might have to wait until you see a /g/.  A similar reason applies for the second example above.

The remainder can be implemented as a deterministic finite-state transducer, because they only require a fixed constant amount of memory.

Those two rules can be implemented as a non-deterministic finite-state transducer.  For instance, when the transducer sees a /d/ it can non-deterministically guess whether or not there is any subsequent /g/, and follow both paths.  Those two rules can even be implemented with an unambiguous non-deterministic finite-state transducer.

If you want an overview of theoretical tools to prove that a language is/isn't regular, take a look at https://cs.stackexchange.com/q/1331/755 and https://cs.stackexchange.com/q/1031/755.  Those relate to regular languages, but similar theoretical tools can be adapted to apply to regular relations as well.  See also https://en.wikipedia.org/wiki/Finite-state_transducer.

Literature

There appears to be some literature on exactly your idea: modelling phonological rules as regular relations.  See, for example, the following paper:

Ronald M. Kaplan, Martin Kay.  Regular Models of Phonological Rule Systems.  Computational Linguistics 20(3), pp.331-378, 1994.

From a technical perspective, they model phonological rules as same-length regular relations, i.e., a regular relation $R \subseteq \Sigma^* \times \Gamma^*$ with the added property that for every $(s,t) \in R$ the length of $s$ is the same as the length of $t$.  Equivalently, they consider the class of non-deterministic finite-state transducers that have no $\epsilon$-transitions.  It looks like they work out the mathematics and its application to linguistics in considerable detail.


Is there a relationship between relational algebra/calculus and category theory?

Categorical approaches to query languages is a bit of a niche interest, but I think it's a very interesting niche!

Two of the key figures in this area are Peter Buneman and Torsten Grust. Obviously, they didn't do all the work, but if you start with their papers and trace out the citation graph, you'll get pretty good coverage of the area.

The central observation that they work from is that since a relation can be viewed as a set of tuples, the powerset functor can be interpreted as taking  a tuple type to the type of relations over that tuple. Then, the fact that the powerset functor forms a monad means that you can use ideas inspired by Philip Wadler's monad comprehension syntax to give a categorically-inspired calculus for queries with a rich equational theory.

Indeed, Buneman et al's query system Kleisli got its name from the fact that monads are sometimes called "Kleisli triples".

Grust's PhD thesis, Comprehending Queries, works this out these ideas in detail, including the use of monad morphisms to model aggregation operators (like sum and count). Grust and his group also built a system, Ferry, which studied how to integrate databases into programming languages.

One of the main issues in this work (and also in Kleisli, if memory serves), is that monadic query languages tend to be a bit more expressive than relational algebra -- they permit queries to handle sets of sets. Compiling this to SQL or relational algebra requires some care (for example, see Cheney et al's A practical theory of language-integrated query), but the basic issue has a very nice categorical formulation. Relational algebra only uses the monoidal structure of the powerset functor, i.e., the existence of a cartesian product natural transformation $(\bullet) : \mathcal{P}(X) \times \mathcal{P}(Y) \to \mathcal{P}(X \times Y)$; and monadic query languages also demand the join, $\mu : \mathcal{P}(\mathcal{P}(X)) \to  \mathcal{P}(X)$.

That's probably the primary stream of work on categorical approaches to query languages.

A new idea (which unfortunately hasn't gotten as much traction as I think it deserves) is David Spivak's work on using simplicial sets to model databases -- see Simplicial Databases. The central innovation is that the simplicial structure permits explicitly modelling the whole database schema including the relationships between tables (eg, the system of foreign keys), and this enables giving semantics to schema update operations.

Another deviation from standard query languages are restricted logic programming languages such as Datalog, which can be understood as relational algebra plus a fixed point operator. Fixed points permit expressing things like transitive closure queries, and so new databases like Datomic feature query languages based on Datalog. My PhD student, Michael Arntzenius, and I have studied the  semantics of Datalog, and come up with a functional analogue we call Datafun, which has a pretty categorical interpretation in terms of the categories of posets and semilattices.


Iterating over all stabilizer operations on $k$ qubits

Since stabilizer circuits are exactly those which map stabilizers to stabilizers, you could characterize them via their action on a basis of stabilizers, see for instance Sec 2.3 of http://home.lu.lv/~sd20008/papers/essays/Clifford%20group%20[paper].pdf.


Did "Where the really hard problems are" hold up? What are current ideas on the subject?

Here is a rough summary of the status based on a presentation given by Vardi at a Workshop on Finite and Algorithmic Model Theory (2012):

It was observed that hard instances lie at the phase transition from under- to over-constrained region. The fundamental conjecture is that there is strong connection between phase-transitions and computational complexity of NP problems.

Achlioptas–Coja-Oghlan, found that there is a density in the satisfiabe region
where the solution space shatters into exponentially many small clusters. Vinay Deolalikar based his famous attempt to proof $P \ne NP$ on the assumption that shattering implies computational hardness. Deolalikar’s Proof was refuted by the fact that XOR-SAT is in $P$ and it shatters. Therefore, shattering can not be used to prove computational hardness.

The current mainstream thinking seems to be (as stated by Vardi) that phase-transitions are not intrinsically connected to computational complexity.

Finally, Here is an article published in Nature which investigates the connection between phase-transitions and computational hardness of K-SAT.


This paper opens with an introductory survey on graph grammars and then advances two new applications. It’s dated (1992) but explains the concepts well enough that it seems like the kind of thing you’re interested in.


Extension of a partial order to a total of partitions of a weak alternating automaton

If I understand you correctly, you are asking for a linear extension of the partial order induced by the partitioning of the weak alternating automaton into its maximal strictly connected components and the transitions between the states.

Note that the "extension of the partial order" to a total order is not unique. The process of obtaining any such total order is called topologic sorting.

See the following wikipedia page for details and a link to an algorithm: http://en.wikipedia.org/wiki/Partially_ordered_set


Minimum-area orthogonal rectangle coverage

See the paper by Aronov, Ezra and Sharir. They handle the case for points. For rectangles it is not even immediately obvious that an LP relaxion is easy to do, since there might be a chaining effect, and as such the number of candidate rectangles might be large (i.e., $O(n^k)$).

A solution with $O(k \log k)$ rectangles with the same area as the optimal solution, should follow by using BSP (binary space partition) and dynamic programming in polynomial time. So searching on the web would give you refs to papers using this scheme (I dont remember the ref, sorry).

http://www.cims.nyu.edu/~esther/Publications/AronovEzraSharir.pdf


Finding shortest path while maximizing the number of overlapping edges

There is a polynomial-time algorithm for this problem in the case where $C \le 2$.  There is also a polynomial-time algorithm when $C > 2$, assuming paths are not required to be simple.  If you require paths to be simple and have $C>2$, the problem is NP-hard, as explained by Neal Young.   So in the remainder of this answer I will assume that either $C \le 2$, or $C >2$ and you allow non-simple paths.  I will describe the polynomial-time algorithm below.

First, note that in an optimal solution (wlog) the common part of the two paths must be contiguous, i.e., there is a single contiguous segment of $P_1$ that overlaps with $P_2$, and the rest does not.  In particular, if we want shortest paths between $s_1 \leadsto t_1$ and $s_2 \leadsto t_2$, then there must exist some vertices $v,w$ such that $P_1$ has the form $s_1 \leadsto v \leadsto w \leadsto t_1$ and $P_2$ has the form $s_2 \leadsto v \leadsto w \leadsto t_2$ and the $s_1 \leadsto v$ and $w \leadsto t_1$ parts have no overlap with $P_2$, and the $v \leadsto w$ is common to both.  The cost of this solution is then

$$|s_1 \leadsto v| + |w \leadsto t_1| + |s_2 \leadsto v| + |w \leadsto t_2| + (2-C) |v \leadsto w|.$$

So, compute all-pairs shortest paths and all-pairs longest paths; let $d(a,b)$ denote the distance (length of the shortest path) from $a$ to $b$, and $d^*(a,b)$ the length of the longest path.  If $C \le 2$, iterate over all possible choices for $v,w$, and compute

$$d(s_1,v) + d(w,t_1) + d(s_2,v) + d(w,t_2) + (2-C) d(v,w).$$

If $C > 2$, do the same but for the expression

$$d(s_1,v) + d(w,t_1) + d(s_2,v) + d(w,t_2) + (2-C) d^*(v,w).$$

Keep the smallest value of this obtainable (i.e., the minimum over all $v,w$).  That will be the solution to your problem.  (We don't need to enforce the lack of overlap between, say, $s_1 \leadsto v$ and $s_2 \leadsto v$ in this calculation, because any overlap will only further lower the cost of the solution.)

The running time is something like $O(n^3)$, since the time is dominated by the time to compute all-pairs shortest paths.  I make no claim that  this is optimal.

My thanks to Neal Young for showing how to solve this when $C\le 2$, and for helping me make explicit my assumptions about whether paths are required to be simple or not.


Status on circuit lower bounds for polylog-bounded depth circuits

On techniques for proving poly-log circuit-depth lower bounds, all current approaches work under restricted settings.
Like, in the work leading to GCT that you mention, the lower bound applies to a restricted PRAM model without bit operations.

Under another restriction, which is the monotone restriction for monotone boolean functions, there is a Fourier-analytic (or enumerative-combinatorial) approach for proving monotone circuit-depth lower bounds, in my joint work with Aaron Potechin (ECCC and STOC).
This improves on an earlier result by Ran Raz and Pierre McKenzie, which extends the communication game framework of Mauricio Karchmer and Avi Wigderson concerning circuit-depth.

Another line of research to extend the Karchmer–Wigderson game was proposed as a referred communication game by Scott Aaronson and Avi Wigderson, whose extension to a competing-prover protocol is suggested as an approach to separate NC from P by Gillat Kol and Ran Raz (ECCC and ITCS).

Apart from studying the syntactic restriction of monotonicity, there is an approach to study a semantic restriction related to pebble games (called thrifty branching programs) by Stephen Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam.
There is a strong lower bound under the thrifty restriction by Dustin Wehr, matching the best known upper bound for P-complete problems.
These results concern deterministic space complexity, which lower bounds parallel time or circuit-depth by known simulation results (e.g. since $\text{AlternatingTime}[t] \subseteq \text{DeterministicSpace}[t]$).

About the question relating the size and depth of circuits, the following approach may be related.
Richard Lipton and Ryan Williams show that, given a sufficiently strong lower bound on depth (i.e. $n^{1-O(1)}$), a weak size lower bound (i.e. $n^{1+\Omega(1)}$) can separate NC from P.
This result follows from a size-depth trade-off argument based on block-respecting simulations.
An earlier result on trading depth for size is due to Allender and Koucký based on the idea of self-reducibility, but it studied smaller complexity classes like NC$^1$ and NL.

Note that among the above mentioned approaches, some of them consider both the size and the depth of circuits, while other approaches consider only circuit-depth.
In particular, the semi-algebro-geometric approach of Mulmuley, the competing-prover protocol approach studied by Kol–Raz, and the size-depth trade-off approach of Allender–Koucký  and Lipton–Williams all concern both the size and the depth of circuits.
The results in Chan–Potechin, Raz–McKenzie, Cook–McKenzie–Wehr–Braverman–Santhanam, and Wehr give circuit-depth lower bounds under restricted settings regardless of size.
Also, the referred communication game of Aaronson–Wigderson concerns only circuit-depth.

It is still consistent with our knowledge that some P-complete problem cannot be computed by circuits of small depth (i.e. $\log^{O(1)}n$), regardless of size.
If size does not matter for small depth circuits (of bounded fan-in), then perhaps it makes sense to focus more on circuit-depth, than to focus on the size of small depth circuits.


Why do we need PAP (partial aplication) objects in heap?

Functions can be partially applied, so you can end up with a situation in which a function is called with "not enough" arguments. For example, consider the map functional:

(* map : ∀α,β. (α → β) → list α → list β *)
let rec map f xs =
  match xs with
  | []      -> []
  | x :: xs -> (f x) :: map f xs

This will take a function f as an argument, and then pass it one argument, once for each element of the list. Now, consider a two argument function foo:

(* val foo : int → int → int *)
let foo x y = 2*x + y

Then, if you map foo over a list of integers:

(* val bar : list (int → int → int) *)
let bar = map foo [1; 2; 3]

You get a thunk (because this paper is about lazy evaluation). To force one of these thunks, you need to scrutinize the list to get its head, and then force the evaluation of the head by applying it:

 let baz = match bar with
           | f :: fs -> f 6

Now, scrutinizing bar will get you f bound to THUNK (foo 1), and fs bound to map foo [2;3]. Then, to apply f 6, we first evaluate foo 1. This pushes 1 on the stack, and since foo is really a two-argument function, foo 1 will not evaluate further -- it will return a fresh p, bound to PAP(foo 1).

Now the result is the thunk THUNK(p 6) -- to drive evaluation further, you have to demand this thunk.


Minimum path edge-cover or minimum flow with unit capacities and DAGs

Eventually, I found an answer myself and I used it to implement this bioinformatics library:

http://bioinformatics.oxfordjournals.org/content/early/2012/05/02/bioinformatics.bts258.abstract

(see the supplementary data for a theoretical analysis on minimum covering path set).


To get the obvious out of the way first, to show that the $n\times n$ matrix $M$ is PSD, it is enough to show that it is the Gram matrix of $n$ vectors, i.e. $m_{ij} = \langle u_i, u_j\rangle$ where $u_1, \ldots, u_n \in \mathbb{R}^n$. (This is a "sum of squares" proof of positive semi-definiteness, because it shows that the bi-linear form $x^T M x$ can be written as a sum of squares of linear functions of $x$.  I am wondering if you meant something more sophisticated by "sum of squares".)

You get a useful class of PSD matrices from positive definite functions. A function $f: \mathbb{R}^d \to \mathbb{R}$ is positive definite if for all sequences $u_1, \ldots, u_n \in \mathbb{R}^d$, the $n\times n$ matrix $M$ defined by $m_{ij} = f(u_i - u_j)$ is PSD. It is not very hard to see that if $f$ is the Fourier transform of a finite measure, then $f$ is positive definite. I.e. it is sufficient that there is a finite Borel measure $\mu$  on $\mathbb{R}^d$ such that for all $x$
$$
f(x) = \int{e^{i\langle x, y\rangle} d\mu(y)}.
$$
A classical theorem of Bochner shows that this condition is necessary as well.

A special class of positive definite functions are the functions $f(x) = g(\|x\|_2)$, for which the matrix $M$ becomes $m_{ij} = g(\|u_i - u_j\|_2)$. Another classical result of Schoenberg shows that such an $f$ is positive definite if and only if there exists a finite Borel measure $\mu$ on $[0, \infty)$ so that for every $t \geq 0$
$$
g(t) = \int_{0}^\infty{e^{-t^2s}d\mu(s)}.
$$

The original motivation for Schoenberg's theorem was to determine what functions $g$ have the property that for any $u_1, \ldots, u_n \in \mathbb{R}^d$, the metric space with metric $d(u_i, u_j) = g(\|u_i - u_j\|_2)$ embeds isometrically into Euclidean space.

This blog post has a simple proof of Schoenberg's theorem and many links.


Is the MapReduce framework a type of BSP?

In section 2 of http://arxiv.org/abs/1101.1902, the authors define a model of MapReduce that is intentionally structured like BSP. They prove simulation theorems as well. May be a good place to start.


The random densification technique-JL lemma

It's not "obtained", but rather the bound the authors want on $\mathrm{Prob}[|u_1|\ge s]$. The Chernoff inequality says how large $s$ needs to be in order to guarantee the desired upper bound. As they assume $d \le n$, it suffices for $s$ to satisfy $s^2 \cdot d/2≥\ln(20n^2)$, which leads to $s=c\cdot d^{-1/2} \sqrt{\log n}$ for some appropriately chosen constant c.


karger's algorithm contracting nodes not edges

The run-time of Karger-Stein is usually represented as a function of the number of vertices $n$, not of the number of edges. Therefore, placing an edge of weight $0$ between two vertices that previously did not share an edge would make your algorithm identical to theirs and not change the run-time.


Is $CAPP \in P$ known to collapse some quantum complexity classes to classical ones?

This is a bit of a subtle point, but the reason that solving CAPP (and hence finding an approximation to $gap(f)$ with the corresponding level of accuracy) doesn't immediately give a good algorithm for approximating $\langle 0 | C | 0 \rangle$ for arbitrary quantum circuits $C$ is because of normalisation. This is discussed in Proposition 8 of the paper you mention.

But in particular, we don't have $\langle 0 | C | 0 \rangle = gap(f) / 2^n$, where $n$ is the number of variables in the polynomial; we have $\langle 0 | C | 0 \rangle = gap(f) / 2^{n-h/2}$, where $h$ is the number of internal Hadamard gates in the circuit (see Proposition 1). So this means that to get a good approximation to $\langle 0 | C | 0 \rangle$ (say, up to an additive error $1/3$, which is BQP-complete), we would need to approximate $gap(f)$ up to additive error $1/3 \cdot 2^{n-h/2}$, which can be much smaller if $h$ is large.


It seems to me that the direction you should consider looking in revolves around game semantics for general references and the related semantics for linear logic,
such as those based on Conway games.  An algebraic account of references in game semantics by Paul-André Melliès and Nicolas Tabareau is probably the best place to start. In this paper linear logic is relaxed to so-called tensor logic to get things to work, so it is not quite the setting you want. But they do rely on Conway games, so there is certainly a connection with models of linear logic. They also do not really exploit linearity as in linear types, but the machinery is there to do so if you want to, I believe.

The work of Jim Laird (such as A Game Semantics of Names and Pointers) and Guy McCusker may also contribute to your quest. The recent interesting thesis Game semantics for an object-oriented language by Nicholas Wolverson pushes these ideas further in an OO setting. He considers in detail linear threading, only one operation active at a time, and describes how to add linear classes. Both rely on linear typing.
Again, however, the underlying model is not strictly a model of linear logic, but it's close.


Looking for a particular normal form for Context-sensitive grammar

A set of grammars in Kuroda form $\mathcal{K}$ is a strict subset of grammars in the described form $\mathcal{L}$:$\mathcal{K}\subset\mathcal{L}$. This follows from the fact that the first form covers first three forms of Kuroda since $k$ and $m$ can be equal to $0$. And the last one covers '$A$ $\mathcal\rightarrow$ $a$' form since $k$ and $n$ can be equal to $0$.

Let $\mathcal{G}$ - set of all Context-sensitive grammars.
Since it's proven that for any Context-sensitive grammar $G\in\mathcal{G}$ there is a mapping $K:\mathcal{G}\rightarrow\mathcal{K}$ (i.e. there is an algorithm of transforming any CS-grammar into Kuroda form), we can say that mapping $L:\mathcal{G}\rightarrow\mathcal{L}$ also always exists and it is equal to $K$: $L$ = $K$.

Indeed, for any $G\in\mathcal{G}$ there should be satisfied the following condition: $L(G)\in\mathcal{L}$. If $L=K$, then $L(G)\in\mathcal{K}\subset\mathcal{L}$.

Q.E.D.


The structure you suggest is known as a 'semihypergroup', a notion introduced by F. Marty in 1934. According to Google, some of your questions have already been attacked by a diverse community of mathematicians involving Greeks, Iranians and Thai people. The most challenging question seems point (iv) but I'm unsure about the outcome, though a positive result in that directions would probably have far-reaching consequences -- possibly in relation with Rhodes' interest in the separation of complexity classes.


Computing Size of Set with Particular Jacobi Symbol in Poly-Time

The Jacobi symbols $(\frac{a}{n})$ which are $\pm 1$ are exactly those for which gcd$(a,n) =1$, and thus the number of these is $\phi(n)$, where $\phi$ is Euler's $\phi$-function. Now, if $n$ is not a perfect square, exactly half of these are $+1$ (this can be seen using the Chinese remainder theorem). Thus, if you know |$J_n^{+1}$|, you know $\phi(n)$. And given $\phi(n)$, you can factor $n$. So there is a polynomial-time algorithm for |$J_n^{+1}$| if and only if factoring $\in$ P.


How are Futures described in terms of category theory?

As it happens, I'm writing a paper about this now. IMO, a good way to think about futures or promises is in terms of the Curry-Howard correspondence for temporal logic.

Basically, the idea behind futures is that it is a data structure representing a computation that is in progress, and upon which you can synchronize. In terms of temporal logic, this is the eventually operator $\Diamond A$. This has a monadic structure:
$$
\begin{array}{lcl}
\mathrm{return} & : & A \to \Diamond A \\
\mathrm{bind} & : & (A \to \Diamond{B}) \to \Diamond{A} \to \Diamond{B}
\end{array}
$$
in which the $\mathrm{return}$ operation spawns a process that immediately returns its argument, and $\mathrm{bind}$ creates a new process which waits for $a$'s value, applies $f$ to that value, and then waits for the $B$-value before returning. The Promises/A proposal for CommonJS calls the monadic bind  operation then, and Scala 2.10 just gives it the standard monadic interface.

The dual to the eventually operator $\Diamond{A}$ is the always operator $\Box{A}$ of temporal logic, which says that at every instant, you get an $A$. When you pass from a Kripke semantics of temporal logic (where you just model provability) to a categorial semantics of a $\lambda$-calculus (where you model lambda-terms/proofs also), it turns out there are actually multiple ways to do this.

The simplest thing you can do is to take $\Box{A} \triangleq A$, on the grounds that once you have an $A$, you always have it. This works, but is kind of boring, IMO. :)

The most natural (IMO) thing to do is to take $\Box{A} \triangleq \mathsf{Stream}\;A$, which permits you to get a (potentially different) $A$ at each instant. Then, you can see the comonadic style of functional  reactive programming (FRP) (first proposed by Tarmo Uustalu and Varmo Vene) as the dual to monadic style of programming with futures.

However, the comonadic $\lambda$-calculus as they suggest, despite its elegance, causes a serious loss of expressiveness relative to programming explicitly with streams, since the category of free coalgebras they use turns out to have too few global elements to denote many interesting programs, especially fixed points.

Nick Benton and I have argued for programming explicitly with streams in our paper Ultrametric Semantics of Reactive Programs. Subsequently, Alan Jeffrey suggested using LTL as a type system in his paper LTL types FRP, an observation that Wolfgang Jeltsch also made in his paper Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming.

The difference between the view Nick and I take, and the one that Alan and Wolfgang take is best understood (IMO) by comparing the construction given in Birkedal et al.'s First steps in synthetic guarded domain theory: step-indexing in the topos of trees with Alan's paper. The topos of trees (presheaves over the natural numbers ordered by size) is very similar to category of ultrametric spaces Nick and I used, but much easier to compare with  Alan's category (presheaves over a discrete category of time), since these are both presheaf categories.

If you're interested in futures specifically for concurrency, then it might be a better idea to look at CTL rather than LTL, though. AFAIK, that's presently unexplored territory!

EDIT: here's a link to the draft. The paper is mostly about implementing typed FRP, so the language is synchronous. But most of the discussion of futures/events in section 3.3 should basically apply to truly concurrent languages as well.


Has this formulation of pursuit evasion been researched? Similar to Helicopter Cops and Robbers Game

My friend Bastian and I devoted our bachelor's thesis to researching this problem. So I guess the problem has been researched (at least a little bit) now which answers my original question. Here is a link to the final result: The Monk Problem.

Results include:

New kind of recursive system (EL-systems) which is used as a verifier
Connection between search number and strongly connected components
Greedy heuristics based on graph decomposition

The complexity class still remains unknown.


Is there a set theoretic way to look at SQL?

It is common wisdom that database field is firmly grounded in the two math disciplines: predicate logic and set theory. However, this is very fuzzy observation, and reality is more subtle.

The structure of the basic building block - relation - is described in set language, but that's about it. This is not really very insightful, because the whole mathematics is written in set language. The fact that probably caught your attention is that the foundation of SQL - relational algebra - has distinct Boolean flavor.

Please also note that SQL actually operates not with relations but multirelations which are bags(multisets) of tuples(rows). Therefore, its algebra is not a [boolean] algebra of sets. There were various attempts at rigorous theory of multirelations, with provenance semiring being the most recent development


Natural graph class with five excluded subgraphs?

The "split-substitute" graphs are the graphs starting with a split graph and substituting any split graph into any node.
The forbidden induced subgraphs can be obtains from the forbidden induced subgraphs of split graphs (c4, C5, co-C4), but replacing the non-prime ones (c4 and co-c4) with their minimal prime extensions... (here primality is with respect with modular decomposition.)

So the 5 forbidden induced subgraphs are the C5, P5, co-P5, H6 and co-H6. This forms a self-complementary class which strictly contains the class of cographs.

See: http://webdocs.cs.ualberta.ca/~hayward/papers/p4comp.online.pdf

The maxibrittle graphs are the perfectly orderable graphs for which a vertex sequence defined only by the degrees will produce a perfect order (more specifically, the degree sequence defines a brittle ordering). These graphs have exactly 5 minimal forbidden induced subgraphs.


Tableau method for two-variable first-order logic

You might check the FO2 solver by Tomer Kotek: https://forsyte.at/alumni/kotek/fo2-solver/ This is the only existing FO2 solver (Tony Tan with his student have a paper under submission, in which they proposed another algorithm, based on probabilistic methods).
I'm not aware of any tableaux algorithm for FO2.


What is/are the lower bounds for finding a something akin to complex residue?

So far, I've seen that Bruno Salvy's webpage hosts a "gfun" package that solves this in O(N). I'm attempting to write a more efficient algorithm than this, so I'm hoping that it's possible to do better. I imagine that a bounds related to the length of the function description may be possible...

There are different measures of polynomial sparseness in the literature and you haven't been very clear on which one you might mean. However, your optimism is likely not well founded.

Take (x-2) / x^32. It's almost maximally sparse by any reasonable measure, but the coefficients in its Laurent series grow exponentially fast. If multiplication is unit cost you can still use the binary exponentiation method to keep up with the exponential growth in sublinear time in the total degree of the series, but the example suggests that things aren't rosy. This is an area littered with hardness results for division and related problems, at least in realistic models of computation where multiplication isn't constant time.

Jacques Carette is an expert in this area, so let's hope he posts a definitive answer.


Estimating the volume of a convex polytope and the closely related task of sampling from it have applications in private data release.

Roughly, the problem you want to solve is: given a collection of numeric valued queries on a database, come up with answers to those questions that are as close as possible to the real answers, while satisfying differential privacy. In some range of parameters, the optimal algorithm for solving this problem has a geometric description, and implementing it involves sampling from a convex polytope. See here: http://arxiv.org/pdf/0907.3754v3.pdf


You may start from the connection between polynomial identity problem and exponential time classes. Polynomial identity problem has significant importance in both algorithm and
complexity theory. The recent breakthrough for faster exponential time exact algorithm for Hamiltonian cycle problem
was derived via a reduction to polynomial identity. From the complexity point of view,
derandomization of polynomial identity implies the separation of NEXP or PP from P/ploy.
Therefore, I believe that polynomial identity will continue to play an important role in both
algorithm and complexity theory. It is closely related to some exponential time algorithmes, and
also the separations between exponential time classes and non-uniform circuit classes.


Are there perceptrons that maximize the average margin, rather than the minimum?

This is what a soft-margin SVM is already doing, except that the average has a min on the inside: $\sum_i min(h,d(x_i,c_i,w))$ where $d(x_i,c_i,w)$ is the distance of the point $x_i$ from the classification hyperplane, signed with a positive sign if it is on the correct side as determined by the target $c_i$, and $h$ is the maximum distance on the correct side you're willing to give "credit" for.  If you set $h$ to a large enough value, this is what you have above.  And, this is precisely a soft-margin linear SVM.


Relation between transcendental numbers and computational complexity?

One other way to look at this, which brings in potentially all complexity classes above $\mathsf{E} = \mathsf{DTIME}(2^{O(n)})$, is to consider real numbers in their binary expansion. Any real number whose binary expansion doesn't end with $0^\infty$ or $1^\infty$ - i.e., which is not a dyadic rational - has a unique binary expansion. We can treat this binary expansion as an element of $\{0,1\}^{\mathbb{N}}$, which in turn we can view as a subset of $\mathbb{N}$, and therefore (under the standard identification of $\mathbb{N}$ with $\Sigma^*$ for $\Sigma$ a finite alphabet) a language. One can then ask about the complexity of this language. (Dyadic rationals correspond to languages which are only finitely different from $\emptyset$ or from $\Sigma^*$, so aren't all that interesting anyways...)

Note that if a language $L$ has its characteristic function $\chi_L$ being real-time computable, then $L$ itself is in $\mathsf{E}$: given input $x$ of length $n$, suppose that $x$ is the $N$-th string in length-lexicographic order (that is, the string $x \in \Sigma^*$ corresponds to the integer $N \in \mathbb{N}$ under the standard identification). To decide whether $x \in L$, use the real-time machine to output the first $N$ bits of $\chi_L$ and read off the $N$-th bit. This takes $O(N)$ time; but $|x| = \log_{|\Sigma|} N$, so this is $O(|\Sigma|^{|x|}) = 2^{O(|x|)}$ time.

(As far as I can tell the converse need not hold. Or at least, the naive proof that I was thinking of doesn't work. That is, suppose $L \in \mathsf{E}$. The naive way  decide the first $N$ bits of $\chi_L$ takes $\approx N \cdot 2^{O(\log N)} = N^{1 + c}$ time for $c > 0$.)

Using this identification, you can in principle use all complexity classes that aren't contained in $\mathsf{E}$ to try to understand the "complexity" of any non-real-time-computable transcendental numbers. However, I don't know how to relate complexity properties of the language $L$ to whether $\chi_L$ is algebraic or transcendental. Strikes me as a very interesting question. As pointed out by Emil Jerabek in the comments, using this identification, all algebraic numbers are in the linear-time version of the counting hierarchy $\mathsf{CH}$, hence also in $\mathsf{E}$. So this approach seems mainly useful for distinguishing the complexity of transcendental numbers from one another, rather than for distinguishing e.g. the complexity of real-time computable and algebraic numbers.


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


Detecting/Locating endpoints of a bridge-like structure in images using Graph Theory

I extend my comment adding an image produced with an (old) piece of software I made to automatically fill a figure with a colored gel.

The steps are:

reduce colors to black and white (1 bit)
reduce DPI
remove noise
apply a standard thinning algorithm
remove edges shorter than a fixed amount (based on the whole figure size)

I was interested in finding the center of each zone; if you are interested in the exact length of the bridge you can use various techniques.

For example:

add a "growing" white circle at the two endpoints of the longest segment found and reapply the algorithm, until the graph becomes disconnected, or
scan the longest segment with an orthogonal line and calculate the length of its intersection with the original image;  cut the bridge when you find a fast change in the length of the intersection
...

EDIT

In order to transform the image into a graph, you must scan the 1bit bitmap produced with the thinning algorithm (the skeleton).

The algorithmm I used in my program, generates at most 3 neighbours (out of 8) for each pixel. So the graph construction can be done in this way:

1. start from top left pixel P=(x,y), create a starting node N_0=(x,y)
2. mark P as processed
3. count the unprocessed neighbours neig_num of P
   3.1 if neig_num = 0 then P is an endpoint of an edge
       - check if one of its neighbours is an already created node N
       - otherwise create a new node N=(x,y)
       - add an edge from N to the last node found LASTN
   3.2 if neig_num = 1 then P is an inner point of an edge, do nothing
   3.3 if neig_num = 2 then P is a node of degree 3
       - create a new node N=(x,y)
       - add an edge from N to the last node found LASTN
6. for each unprocessed neighbour P' of P recursively call 2 (passing P as LASTN).
7. stop when all pixels have been processed
8. do some clean up stuff: merge closer nodes, remove short edges,
   check if N_0 has degree 2 (we started on an edge in a closed path)