Best approximation for a HYPERGRAPH-MAXDICUT problem

This is perhaps not entirely satisfactory since you asked for an approximation rather than a hardness result but there is no constant independent of $a$ for which the problem can be approximated to within via an FGLSS-like reduction.

Unless P=NP, for every $\epsilon > 0$, there exists $c_0$ such that there is no poly-time $\epsilon$-approximation for Hypergraph-DiCut (HDC) instances on $c_0 \le c$-uniform hypergraphs.

Note that this covers the original question since for any $c > 1$, one can take $a$ sufficiently large so that $c^a \ge c_0$; if $a$ grows with $n$, the problem only becomes harder to approximate. It is also easy to artificially increase $c$ in the sense that if one has approximation hardness for any $c$, then one also has an approximation hardness for $c' \ge c$ (ignoring rounding). (see below for details)

Let me tell you the basic idea first and then do it properly.

Example Reduction from 3SAT

We know that it is NP-hard to distinguish satisfiable 3SAT instances from, say, 88%-satisfiable instances.
3SAT can be reduced to your problem like this: for each clause $C$, such as $(x_3 \lor \lnot x_5 \lor x_6)$, we introduce seven vertices - one for each of the seven satisfying assignments to these three variables, such as $(x_3=1, x_5=0, x_6=1)$. For each of these vertices $v$, we have a hyperedge where $v$ is the head and the tail consists of the six other assignments. This way, we force a solution to include in $S$ at most one of the assignments (for simplicity, we may assume that $S$ only contains vertices such that they are the head of a satisfied hyperedge). We also include in the tail of the hyperedge every other vertex that shares a variable with the clause $C$, and where the assignments of shared variables are inconsistent.

As an example, if we also have the clause $(x_3 \lor x_8 \lor x_9)$, we include in the tail of the hyperedge where $(x_3=1, x_5=0, x_6=1)$ is the head, the vertices corresponding to $(x_3=0, x_8=0, x_9=1), (x_3=0, x_8=1, x_9=0)$, and $(x_3=1, x_8=1, x_9=1)$. Note that these are added to the tail, so the hyperedge both rules out inconsistent assignments to the original clause as well as inconsistent assignments of clauses with common variables.

This way, we can now only choose cuts $S$ where the assignments to variables are consistent and each cut hyperedge corresponds to one satisfied clause. In fact, the optimal cuts will correspond precisely to the optimal simultaneously satisfiable clauses. If we reduced from a 3SAT instance where each variable appeared in a bounded number of clauses, then the size of the constructed hyperedges will also be bounded by some constant. If the 3SAT instance was hard to approximate within, say, 0.88, then the Hypergraph DiCut problem, for sufficiently large $c$, is also hard to approximate within 0.88.

Finally, we could have done precisely the same reduction but with each vertex representing the assignment to some $r$ number of clauses with the effect that the problem becomes hard to approximate to within any constant for sufficiently wide hyperedges.

Label Cover Reduction in Detail

More carefully now, the hardness reduction is from Label Cover (LC) and is similar to the FLGSS reduction from SAT to Clique (see references).

Let $u \sim v$ indicate that the vertices $u$ and $v$ are neighbors. If a hyperedge is $k$-uniform, I will also refer to $k$ as the width of the hyperedge.

We know that for every $\epsilon > 0$, there exists fixed $L$, $R$, $d$, $\Delta$, such that for Label Cover with label sets $L$ and $R$, projection degrees at most $d$, and bipartite constraint graphs with degrees at most $\Delta$, it is NP-hard to distinguish perfectly satisfiable instances from $\epsilon$-satisfiable.

Given an LC instance $(U, V, E, \Pi)$, we consider introducing for each LC vertex $v \in V$ and label $i \in R$, an HDC vertex $(v, i)$ which represents assigning $v$ the label $i$. For each HDC vertex $(v, i)$, let $A(v, i)$ be the set of HDC vertices with conflicting assignments to $v$. That is, $A(v, i) = \{ (v, j) : i \neq j \}_{j \in R}$. Similarly, let $N(v, i)$ be the set of neighbor-of-neighbor assignments conflicting with $(v, i)$. That is, $N(v, i) = \{ (w, j) : \forall_{u \in U: v \sim u \sim w} \pi_{vu}(i) \neq \pi_{v'u}(j) \}_{w \in W, j \in R}$.
For each HDC vertex $(v, i)$, we introduce an hyperedge with head $(v, i)$ and tail consisting of $A(v, i) \cup N(v, i)$.
From the assumptions of the reduced-from LC instances, the cardinality of $A(v, i)$ is at most $|R|-1$ and of $N(v, i)$ at most $(|R| - d) \Delta^2$. Hence the hyperedges have width at most $|R| \Delta^2$; the hyperedges may also have smaller width but it easy to add extra variables to pad the hyperedges (see below).
The tail elements $A(v,i)$ of $(v,i)$ ensure that we cannot simultaneously satisfy two hyperedges giving different assignments to $v$. The elements $N(v, i)$ ensure that we may assign a label to the neigbors $u \in U$ of $v$ such that all neighbors $w \in V$ of $u$ have projected labels which are consistent with the projection of $v$'s label; in effect, all LC edges incident $v$ are satisfied by the projected label.

For any set of HDC vertices $S$, let $H(S)$ be the set of hyperedges which have a head in $S$. Again, wlog, we may assume that a cut $S$ only contains HDC vertices which are heads of satisfied hyperedges.

Analysis

Completeness claim: if the LC instance has value 1, then the HDC instance has a cut of size $|V|$.
Proof: Simply take a satisfying labeling $\lambda$ of the LC instance and let $S$ consist of the vertices $(v, \lambda(v))$ for each $v \in V$. Note that since we only take one assignment per vertex, the tail $A(v, i)$ has an empty intersection with $S$. Similarly, since the labeling satisfies all LC edges, for every $v, v' in V$ with a common neighbor $u \in U$, we have $\pi_{vu}(\lambda(v)) = \lambda(u) = \pi_{v'u}(\lambda(v'))$ and hence none of the elements in $S$ appear in the tails of the hyperedges of $H(S)$.

Soundness claim: if the LC instance has value at most $\epsilon$, then the HDC instane has no cut larger than $\epsilon |V|$.
Proof: since we assume that $S$ only contains heads of satisfied hyperedges, we know that for every LC vertex $v \in V$, there is at most one label $j \in R$ such that $(v, j) \in S$. We also know that for every $u \in U$, all neighbors $v \in V$ of $u$, which have an assignment in $S$ are consistent about the projected label of $u$. Consequently, we can define the partial labeling $\lambda$ by choosing $j$ as the label for $V$ if $(v, j) \in S$ and for every neighbor $u \in U$, the label $\lambda(u) = \pi_{v,u}(j)$. This labeling satisfies at least a fraction $|S| / |V|$ of LC constraints since for each labeled $v \in V$, we satisfy all incident constraints and the LC instance is regular.

Conclusion: it is NP-hard to distinguish $|V|$-satisfiable instances from $\epsilon |V|$, i.e., it is NP-hard to approximate the problem to within a constant better than $\epsilon$ for sufficiently large hyperedge widths.

--
Caveat: The hardness result assumes that $c$ can be a large constant, i.e., $a$ reasonably large, and is therefore chiefly only of theoretical interest.

--
To reduce instances with hyperedges of width $c$ to width $c' < 2c$, introduce a copy $v'$ of each variable $v$ and call the two duals of one another. Also introduce the corresponding copy of each hyperedge. Next, replace augment every - original and copy - hyperedge $v_1 \rightarrow v_2, \dotsc, v_c$ by adding $c'-c$ dual variables as tail: $v_1 \rightarrow v_2, \dotsc, v_c, v'_2, \dotsc, v'_{c'-c}$; the new instance will have the same value (=maximum fraction of simultaneously satisfied hyperedges). To see this, suppose the original instance had value $x$ and the augmented value $y > x$. Let $S \cup S'$ be a value-$y$ solution to the augmented instance where $S$ is the set of included original vertices and $S'$ the set of included copied vertices. Then the fraction of satisfied original hyperedges or the fraction of satisfied copied hyperedges must be at least $y$. Suppose it is $S$, then we choose $S$ as the assignment to the original instance as well. Since we only added more vertices to the hyperedges, if an original edge was satisfied by $S, S'$ in the augmented instance, it is also satisfied in the original instance by $S$. In effect, the value of the original instance must have been at least $y$.

P.S. Sorry about the wall of text.

References

Johan Håstad. Some Optimal Inapproximaility Results. In JACM'01.
Feige, Goldwasser, Lovasz, Safra, and Szegedy. Approximating clique is almost NP-complete. In FOCS'91.


One million nodes is far too much for any exact method that I know. This being said, I expect your graph does not have a very large number of edges, so the best is to begin by applying repeatedly this algorithm :

If you have a vertex in your graph that has not outgoing edge, or that has no incoming edge, remove it from your graph as no cycle can go through it. Take care, as removing such vertices can lead to remove other vertices that had edges in both direction before !

This should reduce dramatically the size of your graph (look at what is called "topological sort"). Once this is done, you can compute the different strongly connected componets, as your cycle is included in one of them. Then, you can do the computations separatedly. Perhaps the splitting of your graph will have created new vertices that you can remove.

Iterate through these two algorithms until you can do no other operation in your graph. When it is done, come back here and ask your question again giving the new number of vertices.

When you do so, do not count the number of vertices having exactly one incoming edge and one outgoing edge. They do not change the complexity of the problem.

If after all this your graph is still 1M vertices large, it begins to really be desperate :-)

Nathann


Proof of an Ising model representation of graph isomorphism problem

The counterexamples you give are not correct. I suspect your bug is this: when doing the sums over edges in (or not in) $E_1$ and $E_2$, you need to consider both orderings of each pair.

Consider your first false positive. One of the mismatched edges corresponds to (the lack of) $(2,4)$ in $G_1$, which maps to $(3,1)$ in $G_2$ (which is present). This makes the third term in the sum non-zero: consider $(i,j)$=$(2,4)$ and $(u,v)$=$(3,1)$; $x_{3,2}x_{1,4}$ is non-zero. If you only consider the edge pairs $(u,v)$ where $u<v$, you miss counting these non-zero terms and get the incorrect zero result.


This should be indeed NP-hard. And the construction is very similar to one that already worked for a similar question: Many-one reduction from inequality problem to equality problem.

From a graph $G=(V,E)$ and $k$ construct the graph $G'$ with vertex set $V \times \{1,\dots,k\}$ and edges between $(v,i)$ and $(w,j)$ if $(i \ne j)$ and $(v \ne w)$ and $(v,w) \in E$. It is easy to see that $G'$ is $k$-partite and it has a $k$-clique if and only if $G$ has.


Which graph parameters are NOT concentrated on random graphs?

Many parameters  of the largest connected component are not concentrated for $G(n,p)$ if $p=1/n$ and more generally if $p$ is in the critical window. Examples are the diameter and the size of the largest component, the size of the second largest component, the number of leaves the component has, etc.

See e.g.

Aldous, David. "Brownian excursions, critical random graphs and the multiplicative coalescent." The Annals of Probability (1997): 812-854.

Nachmias, Asaf, and Yuval Peres. "Critical random graphs: diameter and mixing time." The Annals of Probability 36, no. 4 (2008): 1267-1286.

Addario-Berry, Louigi, Nicolas Broutin, and Christina Goldschmidt. "The continuum limit of critical random graphs." Probability Theory and Related Fields 152, no. 3-4 (2012): 367-406.


That is tightly equivalent to CNF-SAT.

CNF-SAT  $\to$  your problem    :

The subscripts are the variables and the superscripts indicate whether the

literal is positive or negative.    If you want to preserve the number of solutions, then insert

clauses of the form  x or not x  for each variable x.    Other than that, the elements are

the clauses, and each set is the set of clauses in which the corresponding literal occurs.

your problem  $\to$  CNF-SAT    :

There is one variable per pair-of-sets, and one clause per element.

For each element x and variable i,        not i  is in x's clause if and only if x is in $S^i_0$

and    (the positive literal) i  is in x's clause if and only if x is in $S^i_1$    .


Combinatorial algorithm for optimization over semimetric polytope

Yes: the dual is a multicommodity flow problem which can be solved using the Garg-Koenemann algorithm http://dx.doi.org/10.1137/S0097539704446232.


Dependent types over Church-encoded type in PTS/CoC

You can't do this using the traditional Church encoding for Bool:

#Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool

... because you can't write a (useful) function of type:

#Bool → *

The reason why, as you noted, is that you can't pass in * as the first argument to #Bool, which in turn means that the True and False arguments may not be types.

There are at least three ways you can solve this:

Use the Calculus of Inductive Constructions.  Then you could generalize the type of #Bool to:

#Bool = ∀(n : Nat) → ∀(Bool : *ₙ) → ∀(True : Bool) → ∀(False : Bool) → Bool

... and then you would instantiate n to 1, which means you could pass in *₀ as the second argument, which would type-check because:

*₀ : *₁

... so then you could use #Bool to select between two types.
Add one more sort:

* : □ : △

Then you would define a separate #Bool₂ type like this:

#Bool₂ = ∀(Bool : □) → ∀(True : Bool) → ∀(False : Bool) → Bool

This is essentially a special case of the Calculus of Inductive constructions, but produces less reusable code since now we must maintain two separate definitions of #Bool, one for each sort that we wish to support.
Encode #Bool₂ directly within the Calculus of Constructions as:

#Bool₂ = ∀(True : *) → ∀(False : *) → *

If the goal is to use this directly within unmodified morte then only approach #3 will work.


The most general result known is by Grohe.  A summary was presented in July 2010:

Martin Grohe, Fixed-Point Definability and Polynomial Time on Graphs with Excluded Minors, LICS 2010.  (PDF)

In short, any statement that is expressible in fixed-point logic with counting has a polynomial-time algorithm on classes of graphs with at least one excluded minor.  (FP+C is first-order logic augmented with a fixed-point operator and a predicate that gives the cardinality of definable sets of vertices).  The key idea is that excluding a minor allows the graphs in the class to have ordered treelike decompositions that are definable in fixed-point logic (without counting).

So a large class of answers to your question can be obtained by considering properties that are definable in FP+C but that are hard to count.

Edit: I'm not sure this actually answers your question, even less so for your update.  The pointer to and statement of Grohe's result are correct, but I don't think the struck out text is relevant for your question.  (Thanks to Stephan Kreutzer for pointing this out.)  It might be worth clarifying: do you want a counting problem that is difficult in general but easy on minor-excluded classes, or a decision problem?


What is a probabilistic function and where can I learn more about them?

The definition you give is essentially the one you need. A probabilistic function from $X$ to $Y$ assigns to each $x\in X$ a subdistribution of elements of $Y$ (rather than a single $y\in Y$). Such a subdistribution is a function $\delta:Y\to[0,1]$ such that

$\sum_{y\in Y}\delta(y)\leq 1$.

In other words, a probabilistic function $X\to Y$ is a function $f:X\to(Y\to [0,1])$, i.e. $f:X\times Y\to [0,1]$, such that for all $x\in X,$

$\sum_{y\in Y}f(x,y)\leq 1$.

In your case, both domain and codomain are $X^M$; a probabilistic function from $X^M$ to $X^M$ then is a function $f:X^M\times X^M\to [0,1]$ such that for all $x\in X^M$,

$\sum_{y\in X^M} f(x,y)\leq 1$.

The intended meaning of this is that the function still returns a single point when given some input, but this point is chosen randomly according to the relevant distribution. For example, if $M=2$, and $f(1,2) = \{(1,1)\mapsto 0.5,(2,2)\mapsto 0.5\}$ (all others being $0$), then when you call $f(1,2)$, you will get $(1,1)$ or $(2,2)$ each with probability $0.5$.


Yes, but most of the work so far (except very recently, see below) has focused on turning irreversible computations into reversible ones, thereby hoping to avoid any entropy generation. (Note: there is an important difference between energy needed to make a computation run, and entropy generated by the computation and put out into the environment, typically in the form of heat.)
Based on Landauer and Bennett's original analysis that erasing a bit "must" generate $kT \ln(2)$ entropy (see below for why there are scare-quotes), several researchers have pursued various questions along these lines. One line of research was to simulate irreversible Turing machines by reversible ones, which, it was suggested, would generate no entropy. There are several works showing space-time tradeoffs for how to simulate irreversible TMs by reversible ones, e.g.:

Bennett, Time/Space Trade-Offs for Reversible Computation. SICOMP 1989

Levine & Sherman. A Note on Bennett’s Time-Space Tradeoff for Reversible Computation. SICOMP 1990.

Li & Vitanyi. Reversible simulation of irreversible computation. CCC 1996

Lange, McKenzie, and Tapp. Reversible Space Equals Deterministic Space. JCSS 2000.

More recently,

Demaine, Lynch, Mirano, and Tyagi. Energy-Efficient Algorithms, 2016.

studied partially reversible algorithms - that is, if you are willing to pay some entropy, for standard algorithmic tasks can one improve upon the general irreversible-to-reversible simulations mentioned above. Reversible computing has a whole community of researchers devoted to it, viz. the Reversible Computing conference, now in its 10th year.
It has actually been known for a long time, going all the way back to Landauer and Bennett, that the relationship between computational irreversibility and entropy generation is more subtle than is suggested by the tagline "erasing a bit generates $\ln(2)$ entropy." However, in the past 20 years or so nonequilibrium statistical mechanics has advanced to the point that this more subtle relationship can be captured by precise numerical equations involving not just entropy difference, but also a difference of KL divergences, see

Kolchinsky & Wolpert, Dependence of dissipation on the initial distribution over states. J. Stat. Mech. 2017 (arXiv link)

(and references therein).
We hosted a workshop on this at the Santa Fe Institute in August 2017 (where you can see the names of some researchers and talk titles of relevance), and it raises a whole new set of questions in both physics and thermodynamic computational complexity.


Balanced partitioning of a set of axis-parallel 2D rectangles

This seems like a hard problem. You might be able to do something if the rectangles have some packing property. For example, if no point is covered more than $t$ times (for some constant T), and the rectangles are not too long and narrow. Then one can probably prove that a curve intersects $O( \sqrt{n})$ rectangles, using some $k$-ply planar separator argument.


It is NP-hard. Here is a reduction from the minimum bisection problem. Let $G = ([n],E)$ be a graph on $n$ vertices with $m$ edges (assume that $n$ is even). Let $N=2m$. Let $y= (1,\dots, 1,-1,\dots,-1)$ consist of $n/2$ ones and $n/2$ minus ones. For every edge $(i,j)$ introduce two columns: one with ones at positions $i$ and $j$, the other with $-1$ at positions $i$ and $j$. Each permutation $P$ defines a bisection $(S,\bar S)$ and vice versa:
$$S=\{i:1\leq P(i) \leq n/2\} \qquad \bar S=\{i:n/2+1 \leq P(i) \leq n\}.$$
($P$ is not uniquely defined by $S$; but all permutations corresponding to $S$ are equivalent).

If an edge $(i,j)$ is not cut by $(S,\bar S)$ then it contributes $C_1 = \sqrt{n-2}+\sqrt{n+6}$ to the objective function. If $(i,j)$ is cut then it contributes $C_2 = \sqrt{n+2}+\sqrt{n+2}$. Let $\Delta = C_2 - C_1 > 0$.
Observe that the value of the problem equals $m C_1 + \Delta\cdot |E(S,\bar S)|$. That is, the optimal solution to this problem corresponds to the minimum bisection and vice versa.


I think this somehow “uneasy feeling” comes from the fact that human beings consider natural numbers only with a semantic—if I see 2001, e.g., I immediately think of 9/11 or Stanley Kubrick or something, that is, you interpret the number. In terms of inputs for an algorithm, however, it is merely a string of characters, and could just as well be such nonsense as ¨*^! or anything. What we as algorithm analyzers care about is only the length of the string, and absolutely not what it contains or represents. You really have to get this into your mind because otherwise you could e.g. say that $PRIMES$ is obviously in $\mathsf{P}$ as you can just try to divide a number $x$ by all numbers between 1 and $x,$ and this algorithm has obviously polynomial runtime. I hope you see the pitfall.


Is there good open source project that apply semantic web, modal logics, and similar technologies

Not open source, but the AI engines of some successful computer games are based on modal logic, see e.g. "Using Exclusion Logic to Model Social Practices" and "Introducing Exclusion Logic as a Deontic Logic"  by Richard Evans.


Catalog of NP-complete problems, more up-to-date than Garey&Johnson?

The book http://www.csc.kth.se/~viggo/approxbook/ on which the site http://www.csc.kth.se/~viggo/wwwcompendium/ is based.


Are there problems that can be solved in time $2^{n-q^c}$ with $q$ qubits?

I think the scaling $2^{n/q^c}$ is too much to ask for. Even $poly(q) 2^{O(n-q)}$ would represent an exponential speedup for each additional qubit.

And indeed, such a problem is known: simulating a quantum circuit of $n$ logical qubits on a small hybrid quantum-classical computer with only few (perfect) physical qubits $q\leq n$ has this scaling. See: https://arxiv.org/abs/1506.01396


Who proved that a triangulation is 3-colourable implies its dual is bipartite

This result is included in Ore's book The Four-Colour Problem (see Theorem 7.4.3).
I saw a paper that states this as a folklore result and cites Ore. Interestingly, the book gives a different proof for (ii)$\implies$(i). It seems that at that time, it wasn't known that the mapping $f\longmapsto f^*$ is a bijection.
Sorry to disappoint; but that's the best I could trace back.


I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS.

In particular see the thesis of Ann-Christin Knoll, On Resolution
Decision Procedures
for the Monadic Fragment and Guarded Negation
Fragment. This implements what you want, though I couldn't find the implementation online.


Subgraph of G whose maximum degree and minimum degree are of the same order

If you want to find an induced subgraph of "sufficient size" i.e not of constant size, then this is not possible. Consider the star $K_{1, n}$, which has average degree $2-1/n$.  Take any subset of the vertices.

if the subset contains the central node, then the max degree equals the size of the subset. If this subset is more than a constant size, then it violates your condition.
if the subset does not contain the central node then the max degree is zero, which again violates your condition.


Conditional entropy: $H(X | Y)$ large implies $H(X | Y, X \neq Y)$ large?

This might be a partial answer to your question:

Let $X$ and $Y$ be random variables with the same range. Let $Z$ be the indicator of the event $X \ne Y$. By the chain rule,
$$H(X|Y,Z) = H(X,Z|Y)-H(Z|Y).$$
Since $Z$ is determined by $X$ and $Y$, we have $H(X,Z|Y)=H(X|Y)$. Now, by the definition of conditional entropy, $$H(X|Y,Z) = \underset{z \leftarrow Z}{\mathbb{E}}[H(X|Y,Z=z)] = \mathbb{P}[X \ne Y] \cdot H(X|Y, X \ne Y) + \mathbb{P}[X = Y] \cdot H(X|Y, X = Y).$$ Clearly $H(X|Y, X = Y)=0$. Combining the above gives $$\mathbb{P}[X \ne Y] \cdot H(X|Y, X \ne Y) = H(X|Y) - H(Z|Y).$$
Now we have an equation linking the quantities we want. We have $$0 \leq H(Z|Y) \leq H(Z) = H_2(p) \leq 1,$$ where $p = \mathbb{P}[X \ne Y]$. In particular, $$p \cdot H(X|Y,X \ne Y) \leq H(X|Y) \leq p \cdot H(X|Y,X \ne Y) + H_2(p).$$


Suppose to the contrary that
$$ P(x^2 \geq n_i) \geq C/n_i^2 $$ for some infinite sequence $n_1$, $n_2$, $\ldots$, $n_i$, $\ldots$, with $P(x^2 > n_i) > 2P(x^2 > n_{i+1})$. Then we have $$ Var(x) = \int_{x=0}^\infty x^2 d \mu.$$
But now, let's set $n_0 = 0$ and break this integral up into
$$ Var(x) = \sum_{j=0}^\infty \int_{n_j}^{n_{j+1}}x^2 d \mu.$$
We have$$ \int_{n_j}^{n_{j+1}} x^2 d\mu \geq n_j^2 \int_{n_j}^{n_{j+1}} d\mu = n_j^2(P(x\geq n_j)-P(x \geq n_{j+1})) \geq C/2.$$
This shows that the integral diverges, contradicting the variance being 1.


The "permutation game" is isomorphic to the following game:

  Disconnect. Players alternately remove vertices from a graph $G$.  The player that produces a fully disconnected graph (i.e., a graph with no edges) is the winner.

The graph $G_{\pi}$ corresponding to a particular initial permutation $\pi\in S_n$ contains just those edges $(i,j)$ for which $i-j$ and $\pi(i)-\pi(j)$ have opposite signs.  That is, each pair of numbers in the wrong order in the permutation is associated with an edge.  Clearly the allowed moves are isomorphic to those in the permutation game (remove a number = remove a node), and the winning conditions are isomorphic as well (no pairs in descending order = no edges remaining).

A complementary view is obtained by considering playing a "dual" game on the graph complement $G^{c}_\pi = G_{R(\pi)}$, which contains those edges $(i,j)$ for which $i$ and $j$ are in the correct order in the permutation.  The dual game to Disconnect is:

  Reconnect. Players alternately remove vertices from a graph $G$.  The player that produces a complete graph is the winner.

Depending on the particular permutation, one of these games may seem simpler than the other to analyze.  The advantage of graph representation is that it is clear that disconnected components of the graph are separate games, and so one hopes for some reduction in complexity.  It also makes the symmetries of the position more apparent.  Unfortunately, the winning conditions are non-standard... the permutation game will always end before all moves are used up, giving it something of a misère character.  In particular, the nim-value cannot be calculated as the nim-sum (binary XOR) of the nim-values of the disconnected components.

For Disconnect, it is not hard to see that for any graph $G$ and any even $n$, the game $G \cup \bar{K}_n$ is equivalent to $G$ (where $\bar{K}_n$ is the edgeless graph on $n$ vertices).  To prove it, we need to show that the disjunctive sum $G + G\cup\bar{K}_n$ is a second-player win.  The proof is by induction on $|G|+n$.  If $G$ is edgeless, then the first player loses immediately (both games are over).  Otherwise, the first player can move in either $G$, and the second player can copy his move in the other one (reducing to $G' + G'\cup \bar{K_n}$ with $|G'|=|G|-1$); or, if $n\ge 2$, the first player can move in the disconnected piece, and the second player can do the same (reducing to $G + G\cup\bar{K}_{n-2}$).

This shows that any graph $G$ is equivalent to $H \cup K_p$, where $H$ is the part of $G$ with no disconnected vertices, and $p=0$ or $1$ is the parity of the number of disconnected vertices in $G$.  All games in an equivalence class have the same nim-value, and moreover, the equivalence relation respects the union operation: if $G \sim H \cup K_p$ and $G' \sim H' \cup K_{p'}$ then $G \cup G' \sim (H \cup H')\cup K_{p\oplus p'}$.  Moreover, one can see that the games in $[H \cup K_0]$ and $[H \cup K_1]$ have different nim-values unless $H$ is the null graph: when playing $H + H \cup K_1$, the first player can take the isolated vertex, leaving $H+H$, and then copy the second player's moves thereafter.

I do not know any related decomposition results for Reconnect.

Two special types of permutations correspond to particularly simple heap games.

The first is an ascending run of descents, e.g., $32165487$.  When $\pi$ takes this form, the graph $G_{\pi}$ is a union of disjoint cliques, and the game of Disconnect reduces to a game on heaps: players alternately remove a single bean from a heap until all heaps have size $1$.
The second is a descending run of ascents, e.g., $78456123$.  When $\pi$ takes this form, the graph $G^{c}_{\pi}$ is a union of disjoint cliques, and the game of Reconnect reduces to a game on heaps: players alternately remove a single bean from a heap until there is only one heap left.

A little thought shows that these two different games on heaps (we can call them 1-Heaps and One-Heap, at some risk of confusion) are, in fact, themselves isomorphic.  Both can be represented by a game on a Young diagram (as initially proposed by @domotorp) in which players alternate removing a lower-right square until only a single row is left.  This is obviously the same game as 1-Heaps when columns correspond to heaps, and the same game as One-Heap when rows correspond to heaps.

A key element of this game, which extends to Disconnect and Reconnect, is that the duration is related to the final game state in a simple way.  When it is your turn, you will win if the game has an odd number of moves remaining, including the one you're about to make.  Since a single square is removed each move, this means you want the number of squares remaining at the end of the game to have the opposite parity that it has now.  Moreover, the number of squares will have the same parity on all of your turns; so you know from the outset what parity you want the final count to have.  We can call the two players Eve and Otto, according to whether the final count must be even or odd for them to win.  Eve always moves in states with odd parity and produces states with even parity, and Otto is the opposite.

In his answer, @PeterShor gives a complete analysis of One-Heap.  Without repeating the proof, the upshot is the following:

Otto likes $1$-heaps and $2$-heaps, and can tolerate a single larger heap.  He wins if he can make all heap sizes except one $\le 2$, at least without giving Eve an immediate win of the form $(1,n)$.  An optimal strategy for Otto is to always take from the second-largest heap except when the state is $(1,1,n>1)$, when he should take from the $n$.  Otto will lose if there are too many beans in big heaps to start with.
Eve dislikes $1$-heaps.  She wins if she can make all heap sizes $\ge 2$.  An optimal strategy for Eve is to always take from a $1$-heap, if there are any, and never take from a $2$-heap.  Eve will lose if there are too many $1$-heaps to start with.

As noted, this gives optimal strategies for 1-Heaps as well, although they are somewhat more awkward to phrase (and I may well be making an error in primary-to-dual "translation").  In the game of 1-Heaps:

Otto likes one or two large heaps, and can tolerate any number of $1$-heaps.  He wins if he can make all but the two largest heaps be $1$-heaps, at least without giving Eve an immediate win of the form $(1,1,\dots,1,2)$.  An optimal strategy for Otto is to always take from the third-largest heap, or from the smaller heap when there are only two heaps.
Eve dislikes a gap between the largest and second-largest heaps.  She wins if she can make the two largest heaps the same size.  An optimal strategy for Eve is to always take from the largest heap, if it is unique, and never if there are exactly two of the largest size.

As @PeterShor notes, it isn't clear how (or if) these analyses could be extended to the more general games of Disconnect and Reconnect.


Why is it sometimes easier to achieve $\epsilon$-additive accuracy than $\epsilon$-multiplicative?

Consider a problem where the objective value OPT is guaranteed to lie in a constant non-negative real interval such as $[0, c]$. For example, the paper you mention is about computing approximation solutions to two-player zero-sum matrix games in which the payoffs (and hence the value, OPT) is in the $[0,1]$ interval, as originally considered by Grigoriadis and Khachiyan.

In this type of setting, any $(1+\epsilon/c)$-approximate solution has value $v$ satisfying $$v \le (1+\epsilon/c)OPT = OPT + \epsilon OPT/c \le OPT + \epsilon.$$
So, to compute an additive-$\epsilon$ approximate solution, it suffices to compute any multiplicative $(1+\epsilon/c)$-approximate solution.  So, computing an additive $O(\epsilon)$-approximation is no harder than computing a multiplicative $(1+\epsilon)$-approximation.

The converse is not generally true, because when OPT is near zero, an additive error of $\epsilon$ is relatively large (e.g., consider the case when OPT$ < \epsilon$.  (On the other hand, if, say OPT is guaranteed to be in some range $[c_1, c_2]$ with constant $c_1 > 0$, then the two notions of approximation are equivalent up to constant factors.)
When is one type of accuracy more important or relevant than the other?

Historically most (?) optimization problems studied in theoretical computer science are (informally speaking) "scale-free".  For example, consider the Minimum Spanning Tree problem (or any other problem where the objective is a sum of given weights).  Doubling the edge weights gives an equivalent instance.  In this setting, if you could give an $\epsilon$-additive approximation algorithm, the algorithm would also have to be a $\epsilon/2$-additive approximation algorithm (double the weights of the given instance, then compute an additive $\epsilon$-approximate solution for the modified instance --- it has to give an $\epsilon/2$-approximate solution to the original instance).  So generally speaking additive-$\epsilon$ approximation is awkward in this setting.  You might see it occasionally, but with an additive error term that depends on, say, the maximum edge weight.  In contrast, multiplicative approximation is natural in this setting.

Note that unweighted problems can also be "scale-free".  For example, consider unweighted Set Cover.  Given any instance, you could construct a new instance with two independent copies of the original instance.  This has essentially the same effect as doubling the weights.

Of course there are also problems that aren't naturally scale free, such as Minimum-Degree Spanning Tree.  In this setting, additive approximation can make more sense (such as the additive-1 approximation algorithm for Min-Degree Spanning Tree).

In the other extreme, consider finding a spanning tree that minimizes the product of the edge weights.  Here neither notion of approximation fits well.
How can one one translate between the two? For instance, if you tell me an algorithm solves a problem to $\epsilon$-additive accuracy in time $T$, is it possible to say how fast it will be for $\epsilon$-multiplicative accuracy? (and vice versa)?

See the answer to Question 1.  If $OPT$ is in $[0,1]$, any multiplicative $(1+\epsilon)$-approximate solution will be an additive $\epsilon\,OPT \le \epsilon$-approximation.  Conversely, any additive-$(\epsilon\,OPT)$ solution will be a multiplicative $(1+\epsilon)$-approximate solution, so the running time to compute the multiplicative solution (using an additive-error algorithm with additive error $\epsilon'=\epsilon OPT$) will grow with $1/(\epsilon\,OPT)$ (note $OPT\le 1$).

FWIW, I've noticed that, historically, Chernoff bounds tended to be stated in terms of additive error (where "error" = deviation from the mean).  Perhaps that's because Chernoff bounds generally concern sums of $[0,1]$ random variables.  But when used in TCS they tend to be stated multiplicatively, probably for the reasons outlined above.


I am not sure how you measure distance between eigenspaces, but I do not think you can say anything non-trivial here without some assumption that the eigenvalues of $A$ are separated. For example, let $u$ and $v$ be two arbitrary unit vectors, and define $A = I + \varepsilon uu^\intercal$ and $B = I + \varepsilon vv^\intercal$. Then $(1-\varepsilon)B \preceq A \preceq (1+\varepsilon)B$. However, the leading eigenvector of $A$ is $u$ and the leading eigenvector of $B$ is $v$, and, since they were arbitrary, they can be as far apart as you want.


Can a polynomial sized arithmetic ciruits perform integer division?

See Eric Allender's survey of "recent" breakthroughs (circa more than a decade ago) in the complexity of division. The bottom line is that

  Division is complete for DLOGTIME-uniform $\mathsf{TC}^0$

so in particular there is a poly-sized circuit (of constant depth) that takes $x$ and $y$ as input and produces $x/y$. Notice that this circuit doesn't even need to be arithmetic (it only needs MAJORITY gates in addition to boolean gates)


Why can't a left-recursive, non-deterministic, or ambiguous grammar be LL(1)?

I have done some more research, and I think I've found a solution for the 1st and 2nd questions, as for the 3rd one, I found an existing solution on StackOverflow for it, the proof attempts are written below:

We start by writing the three rules of the definition of an LL(1) grammar:

For every production A -> α | β with α ≠ β:

FIRST(α) ∩ FIRST(β) = Ø.
If β =>* ε then FIRST(α) ∩ FOLLOW(A) = Ø (also, if α =>* ε then FIRST(β) ∩ FOLLOW(A) = Ø).
Including ε in rule (1) implies that at most one of α and β can derive ε.

Proposition 1: A non-factored grammar is not LL(1).

Proof:

If a grammar G is non-factored then there exists a production in G of the form:

A -> ωα1 | ωα2 | ... | ωαn

(where αi is the i-th α, not the symbols α and i), with α1 ≠ α2 ≠ ... ≠ αn. We can then easily show that:

∩(i=1,..,n) FIRST(ωαi) ≠ Ø

which contradicts rule (1) of the definition, thus, a non-factored grammar is not LL(1). ∎

Proposition 2: A left-recursive grammar is not LL(1).

Proof:

If a grammar is left-recursive then there exists a production in G of the form:

S -> Sα | β

Three cases arise here:

If FIRST(β) ≠ {ε} then:

    FIRST(β) ⊆ FIRST(S)

=>  FIRST(β) ∩ FIRST(Sα) ≠ Ø

which contradicts rule (1) of the definition.
If FIRST(β) = {ε} then:

2.1. If ε ∈ FIRST(α) then:

ε ∈ FIRST(Sα)

which contradicts rule (3) of the definition.

2.2. If ε ∉ FIRST(α) then:

    FIRST(α) ⊆ FIRST(S) (because β =>* ε)

=>  FIRST(α) ⊆ FIRST(Sα) ........ (I)

we also know that:

FIRST(α) ⊆ FOLLOW(S) ........ (II)

by (I) and (II), we have:

FIRST(Sα) ∩ FOLLOW(S) ≠ Ø

and since β =>* ε, this contradicts rule (2) of the definition.

In every case we arrive at a contradiction, hence, a left-recursive grammar is not LL(1). ∎

Proposition 3: An ambiguous grammar is not LL(1).

Proof:

While the above proofs are mine, this one is not, it's by Kevin A. Naudé which I got from his answer that is linked below:

https://stackoverflow.com/a/18969767/6275103


If a set $A$ is Turing reducible to a set $B$ then we say that $B$ computes $A$.

Every noncomputable set $A$ computes an immune set, namely $\hat A = \{\sigma: \sigma \text{ is a prefix of }A\}$.

(If $A$ is a set of strings then we first turn it onto a [i.e. replace it by a Turing equivalent] set of integers or equivalently an infinite binary sequence before applying the hat operation.)

For instance if $A$ is the set of prime numbers then we may write
$$A=A(0)A(1)A(2)\dots=00110101000101000101\dots$$
and then $\sigma=0011010$ is a prefix of $A$ whereas $010011$ is not.

Therefore the complexity class of sets that compute only non-immune sets is just the computable sets $\mathsf{R}$.


Weighted furthest point voronoi diagrams

There's something on the multiplicatively weighted farthest neighbor query problem (but not on the associated Voronoi diagram) in my paper

Approximate weighted farthest neighbors and minimum dilation stars.
J. Augustine, D. Eppstein, and K. Wortman.
arXiv:cs.CG/0602029.
Proc. 16th Annual International Computing and Combinatorics Conference (COCOON 2010), Nha Trang, Vietnam.
Lecture Notes in Comp. Sci. 6196, Springer-Verlag, 2010, pp. 90-99.
Discrete Mathematics, Algorithms and Applications 2(4): 553-656, 2010.


There's a polynomial-time dynamic programming algorithm in section 3.2 of https://ajc.maths.uq.edu.au/pdf/28/ajc_v28_p225.pdf (Albert et al, "Longest subsequences in permutations", Australas. J. Combin. 28 (2003), 225–238)


Symbolic Execution of the Quine-McCluskey Algorithim

Since you stated your purpose is considering circuit bounds:

Taking a boolean function and "minimizing" using Karnaugh maps or the Quine–McCluskey algorithm, then converting the formula to AND and OR gates will give you a circuit calculating that function.  This however does not actually give you a minimum sized circuit.  Karnaugh maps minimize the number of product terms in the sum of products form of specifying a function, this is NOT the same as minimizing the number of gates in a circuit.

Consider for instance the $N$ input parity function. The sum of products form will have $2^{N-1}$ minterms, which means you'd need an exponential number of gates using this method.  However if it takes us $M$ of whatever gates are your basis to make a 2-input XOR gate, we can make the $N$ input parity function with only $M(N-1)$ gates: a linear bound.


A basic question about bitcoin's anti double spending mechanism

The correct answer was given to me here: http://forum.bitcoin.org/index.php?topic=27979.msg352498#msg352498.

The gist: The entire value of the output contributes to the subsequent transaction, so if you wish to transfer smaller amount, you must add an additional output on the second transaction to send the remainder back to yourself.

Note that the accounting is done for transactions outputs and inputs. The block concept is not necessary for the verification process and is only used for technical convenience.


What evidence is there that Graph Isomorphism is not in $P$?

Before this question, my opinion was that Graph Isomorphism might be in P, i.e. that there is no evidence to believe that GI is not in P. So I asked myself what would count as evidence for me: If there were mature algorithms for $p$-group isomorphism that fully exploited the available structure of $p$-groups and still would have no hope to achieve polynomial runtime, then I would agree that GI is probably not in P. There are known algorithms that exploit the available structure like Isomorphism testing for $p$-groups. by O'Brien (1994), but I haven't read it in sufficient detail to judge whether it fully exploits the available structure, or whether there is any hope to improve this algorithm (without exploiting additional non-obvious structure of $p$-groups) to achieve polynomial runtime.

But I knew that Dick Lipton called for action near the end of 2011 to clarify the computational complexity of the group isomorphism problem in general, and of the $p$-group isomorphism problem specifically. So I googled for

site:https://rjlipton.wordpress.com group isomorphism

in order to see whether the call for action had been successful. It was indeed:

The Group Isomorphism Problem: A Possible Polymath Problem?
Advances on Group Isomorphism
Three From CCC: Progress on Group Isomorphism

The last post reviews a paper which achieves $n^{O(\log \log n)}$ runtime for certain important families of groups, exploits much of the available structure, and acknowledges the above mentioned paper from 1994. Because the $n^{O(\log \log n)}$ runtime bound is both compatible with the experience that graph isomorphism is not hard in practice, and with the experience that nobody is able to come up with a polynomial time algorithm (even for group isomorphism), this can be counted as evidence that GI is not in P.


Connecting vertices after struction operation in J.Chen, I.Kanj, G.Xia vertex cover algorithm

I'll try to track myself what I have been able to establish so far as an empirically working solution.

  Remove vertices {v0,v1,...,vp} and introduce a vertex vij for each (vi,vj)∉E in G, where 0

It is practical to have a function $lookup(x)$ for the supplementary vertices at your disposal, such that $lookup(i) = \{ v_{ij}| j: (v_i, v_j) \notin E\}$.

  Add an edge (vir,vjs) if i=j and (vr,vs)∈E in G.

In practice, each new supplementary vertex $v_{ij}$  in $G\prime=(V\prime, E\prime)$ must be connected to every supplementary vertex $v_{rs} \in lookup(i) \cup lookup(j)$ such that $r \neq i \land s \neq j$.

  Add an edge (vir,vjs) if i≠j.

This is the more straightforward case- for each supplementary vertex $v_{ij}$, and every edge $e_1=(v_i, v_r), e_2=(v_j, v_r); e_1,e_2 \in E$, create edge $e\prime=(v_{ij}, v_r); e\prime \in E\prime$.
∀u∈∖{v0,v1,...,vp} add the edge (vij,u) if (vi,u)∈E or (vj,u)∈E.

Result:

Still, any review of the correctness of my musings or guidance as to how to interpret and adhere to the original paper better is much appreciated!


Is there a planar 4-regular graph that is 3-acyclic colourable?

I can prove that no 4-regular graphs are 3-acyclic colorable.

Consider a 4-regular graph with a 3-coloring. If we call the colors $a, b, c$, then one of the three subgraphs generated by restricting to either $a$ and $b$ colored vertices, $a$ and $c$ vcertices, or $b$ and $c$ vertices must have as many edges as vertices. But all graphs with as many edges as vertices contain a cycle, so the coloring is not acyclic.

Let the graph have $k$ vertices. The graph must have $2k$ edges, because it is 4-regular. Let the number of $a$ colored vertices be $k_a$, and similarly for $k_b$ and $k_c$. Call $e_{ab}$ the number of edges between $a$ and $b$ colored vertices, and the same for $e_{ac}$ and $e_{bc}$. If we assume that none of the restricted graphs have as many edges as vertices, we must have
$$
e_{ab} < k_a + k_b \\
e_{ac} < k_a + k_c \\
e_{bc} < k_b + k_c \\
$$
Summing over all edges, we find that $e_{ab} + e_{ac} + e_{bc} < 2(k_a + k_b + k_c)$, and so $e < 2k$. But this contradicts the fact that 4-regular graphs have twice as many edges as vertices, mentioned above. Thus, the assumption is false, and some color-restricted subgraph has as many edges as vertices, and hence has a cycle.


Unlike the question you threaten for inference rule, this has a nice, simple answer:

  Robinson (1965) A machine-oriented logic based on the resolution principle. Journal of the ACM.

Resolution only applies to a subfragment of FOL, the Horn clauses, that lack disjunction and existential quantification, but combined with Herbrandisation, this is sufficient to encode satisfiability in the following sense: for any formula of FOL, we can find a Horn clause such that each is satisfiable if the other is.

Resolution is related to cut-elimination, but is more efficient.

Extending resolution to the whole of FOL requires a more sophistcated approach to unification than Robinson's algorithm.  Uniform provability offers a technique for reading off such a computational mechanism from a cleaned-up proof theory of intuitionistic logic, higher-order unification, and the double-negation translation.


The problem can be solved at least in $O(M \cdot T \log T)$ which is theoretically better, but may be slower than $O(M\cdot T\cdot L)$ in practice if $L$ is comparable to $\log T$.

Let's show how to find a score of each $v_i$ independently in $O(T \log T)$. For any (possibly gapped) string $W = w_0 w_1 \ldots w_{n-1}$ define two polynomials $zeros_W(x)$ and $ones_W(x)$ as follows:

$$ zeros_W(x) = \sum_{i=0}^{n-1} [w_i = ''0'']x^i$$
$$ ones_W(x) = \sum_{i=0}^{n-1} [w_i = ''1'']x^i$$

where $[P]$ is Iverson notation.

For example, $zeros_{01...01}(x) = 1 + x^5$, $ones_{01...01}(x) = x + x^6$, $zeros_{0001100}(x) = 1+x+x^2+x^5+x^6$ and $ones_{0001100}(x) = x^3 + x^4$.

Then compute coefficients of the following polynomial $$c(x) = zeros_S(x) \cdot ones_{rev(v_i)}(x) + ones_{S}(x) \cdot zeros_{rev(v_i)}(x) = \sum_{j}c_j x^j$$ where $rev(W) = w_{n-1} \ldots w_1 w_0$ is just reversed $W$. It's easy to see that $c_{L-1+k}$ will be equals exactly to the difference between $s_k s_{k+1} \ldots s_{k+L-1}$ and $v_i$. For example, for $S=''0100''$ and $v_i = ''10''$ $c(x)$ will be equal to $(1+x^2+x^3)\cdot x + x \cdot 1 = 2x + x^3 + x^4$ which gives us all interesting differences (2, 0, 1) so we can calculate score in linear time. Thus the problem is reduced to polynomial multiplication, which can be done in $O(T \log T)$ using FFT.

The possible disadvantage of such approach is that FFT has essential constant hidden in its big-O, so using $O(T^{1.585})$ Karatsuba multiplication or something similar may work better in practice for not very large $T$.


What, in simple terms, are the restrictions imposed by Elementary Affine Logic?

The terms "stratification" and "boxes" come from proof nets.  Elementary linear logic ($\mathbf{ELL}$) was originally introduced by Girard as a variant of light linear logic ($\mathbf{LLL}$) and its execution was formulated in terms of proof nets.  It is on proof nets that the elementary bound is satified, i.e., every $\mathbf{ELL}$ proof net $\pi$ may be reduced to its cut-free form in a number of steps bounded by
$$\left.2^{\vdots^{2^s}}\right\}d$$
where $s$ and $d$ are the size and the depth of $\pi$ (maybe the height of the tower is not exactly $d$, it is linear in $d$ I guess).

The size of a proof net is similar to the size of a $\lambda$-term.  The depth, on the other hand, is the maximum number of nested boxes in $\pi$. A box is basically a sub-proof net which may be duplicated or erased: remember that in linear logic there is no free contraction or weakening, which means that proofs in general may not be duplicated or erased; those that can must be marked with a special construct, called box.

Stratification refers precisely to the depth.  It is an informal word that people in the linear logic community use to describe the restricted cut-elimination dynamics that is typical of systems like $\mathbf{ELL}$.  In full linear logic proof nets, cut-elimination may completely alter the depth: if $\pi\to\pi'$ by means of a cut-elimination step and $a$ is a node of $\pi$ at depth $i$ which has a residue $a'$ in $\pi'$, the depth of $a'$ may be anything between $0$ ($a$ is "pulled out" of all boxes) and $2d$, where $d$ is the depth of $\pi$ ($a$ is at maximal depth and it "enters" inside a box which is also at maximal depth).  On the contrary, $\mathbf{ELL}$ proof nets, because of the structural constraints that define them, have the remarkable property that the depth is invariant under cut-elimination: in the above case, the depth of $a'$ is exactly $i$.  This stratification property is essential in proving the complexity bounds of light logics (elementary for $\mathbf{ELL}$ and polynomial for $\mathbf{LLL}$).

From the point of view of Lamping's algorithm, the depth corresponds to the integer label of fan nodes.  Stratification means that a sharing graph corresponding to an $\mathbf{ELL}$ proof net will need no brackets and croissants to be evaluated, because the labels of fan nodes do not change.

After Girard, people started applying the principles of light and elementary linear logic to define type systems for usual $\lambda$-terms (instead of proof nets) which would ensure interesting normalization properties.  The paper you mention falls in this line of work, which explains the terminology they use.  Informally, typing a simply-typed $\lambda$-term amounts to decorating it with "boxes", which is what their so-called pseudo-terms are for.

For the rest, $EAL^\star$ is just like any other non-trivial type system for $\lambda$-terms: there is no simple description of what a typable term looks like; the shortest description is its type derivation!


Automated transformation into spigot algorithm?

Deforestation is a technique for eliminating intermediate data structures when composing functions together (in a lazy language). It improves the memory usage of programs, and is used by the GHC Haskell compiler.

A more general notion is fusion, which combines multiple traversals of a data structure into a single traversal. Fusion rules have been developed for programs written in terms of map and fold.  (If this is the kind of thing you are looking for, I can provide some references (as can google).)

Other transformations can be found on the program transformation wiki.


What is the difference between arrows and exponential objects in a cartesian closed category?

One is internal and the other is external.

A category $\mathcal{C}$ consists of objects and morphisms. When we write $f : A \to B$ we mean that $f$ is a morphism from object $A$ to object $B$. We may collect all morphisms from $A$ to $B$ into a set of morphisms $\mathrm{Hom}_{\mathcal{C}}(A,B)$, called the "hom-set". This set is not an object of $\mathcal{C}$, but rather an object of the category of sets.

In contrast, an exponential $B^A$ is an object in $\mathcal{C}$. It is how "$\mathcal{C}$ thinks of its hom-sets". Thus, $B^A$ must be equipped with whatever structure the objects of $\mathcal{C}$ have.

As an example, let us consider the category of topological spaces. Then $f : X \to Y$ is a continuous map from $X$ to $Y$, and $\mathrm{Hom}_{\mathsf{Top}}(X,Y)$ is the set of all such continuous maps. But $Y^X$, if it exists, is a topological space! You can prove that the points of $Y^X$ are (in bijective correspondence with) the continuous maps from $X$ to $Y$. In fact, this holds in general: the morphisms $1 \to B^A$ (which are "the global points of $B^A$") are in bijective correspondence with morphisms $A \to B$, because
$$\mathrm{Hom}(1, B^A) \cong
\mathrm{Hom}(1 \times A, B) \cong
\mathrm{Hom}(A, B).
$$

Sometimes we get sloppy about writing $B^A$ as opposed to $A \to B$. In fact, often these two are synonyms, with the understanding that $f : A \to B$ might mean "oh by the way here I meant the other notation, so this means $f$ is a morphism from $A$ to $B$." For example, when you wrote down the currying morphism
$$\textit{curry}: (A \times B \to C) \to (A \to C^B)$$
you really should have written
$$\textit{curry}: C^{A \times B} \to {(C^B)}^A.$$
So we cannot really blame anyone for getting confused here. The inner $\to$ is used in the internal sense, and the outer in the external.

If we work in simply typed $\lambda$-calculus then everything is internal, so to speak. We have just a basic typing judgment "$t$ has type $B$", written as $t : B$. Because here $B$ is a type, and types correspond to objects, then we clearly have to interpet any exponentials and arrows in $B$ in the internal sense. So then, if we understand
$$\textit{curry}: (A \times B \to C) \to (A \to C^B)$$
as a typing judgment in the $\lambda$-calculus, all arrows are internal, so this is the same as
$$\textit{curry}: ((C^B)^A)^{C^{A \times B}}.$$
I hope by now it is clear why people use $B^A$ and $A \to B$ as synonyms.


About the position of side conditions in an inference rule

An inference rule is a symbolic representation of an entire family of closure rules. A side condition cuts down such a family to a subfamily. It is perhaps best to show an example.

We consider the following toy variant of the propositional calculus. The language of expressions is built from primitive constants $\top$ and $\bot$, and a binary connective $\land$. Let $\mathscr{E}$ be the set of all expressions we can build in this language (they correspond to binary trees whose leaves are labeled with $\bot$ and $\top$).

There is only one judgement form $\vdash A$ and only two judgement rules
$$
\frac{ }{\vdash \top}
\qquad
\frac{\vdash A \qquad \vdash B}{\vdash A \land B}
$$
It should be clear that $\vdash A$ is derivable if, and only if, $A$ is an expression which contains no $\bot$'s. Now, how precisely do we read the above inference rules? Bare with me while I describe closure rules and closure operators. These provide an order-theoretic explanation of what rules of inference are and what derivability is about.

Each rule determines a family of closure rules. A closure rule is a pair $(S, A)$ where $S \subseteq \mathscr{E}$ and $A \in \mathscr{E}$. In our case we get the following family of closure rules $\mathscr{C}$:
$$\mathscr{C} = \{(\emptyset, \top)\} \cup \{(\{A,B\},A \land B) \mid A, B \in \mathscr{E}\}$$
Such a family then induces a closure operator $F_\mathscr{C} : P(\mathscr{E})
\to P(\mathscr{E})$ on the powerset of expressions, defined by
$$F_\mathscr{C}(X) = \{A \mid \exists S \subseteq X . (S, A) \in \mathscr{C}\}.$$
The set of all derivable judgements is precisely the least fixed point of $F_\mathscr{C}$. The least fixed point exists by Tarski's theorem because $F_\mathscr{C}$ is a monotone operator on a complete lattice.

Suppose we place a side condition $\phi$ on the second rule:
$$
\frac{ }{\vdash \top}
\qquad
\frac{\vdash A \qquad \vdash B}{\vdash A \land B} \ \text{if $\phi(A,B)$}
$$
Here $\phi$ can be any condition on the expressions. For instance, it could be $A \neq B$ (but in that case there will be a better way of writing the rule without a side condition), or perhaps it says that $A$ has fewer occurrences of $\bot$ than $B$, or whatever. The side condition limits the family of closure rules determined by the rule:
$$\mathscr{C} = \{(\emptyset, \top)\} \cup \{(\{A,B\},A \land B) \mid A, B \in \mathscr{E} \ \text{and}\ \phi(A,B)\}.$$
Thus we see that the side-condition lives at the "meta-level", because it does not appear inside the closure rules, but instead gives an additional condition on the closure rules themselves.

In the example of the variable rule that you mention,
$$\frac{ }{\Gamma \vdash x : T} \ \text{if $(x:T) \in \Gamma$},$$
we clearly have a side-condition.

It is called a side-condition because it is written on the side. And it is so written for a reason, namely to make it clear that it is not a premise of the rule. This is especially important when the object-language described by the rule uses the same symbols as the meta-level language and confusion could ensue. However, it has become fashionable in certain circles to write side-conditions above the line. I am not sure it is a good idea to write side-conditions above the line, as it confuses students and newcomers, but it is stylistically a bit more pleasing.


Pairing algorithm for simple speed dating problem

This is simply the Stable Marriage Problem, where rankings go from -1 to 2 instead of 1 to n. Thus it's almost a subset of the problem solved by the Gale–Shapley algorithm. Quoting from Wikipedia:

  The Gale–Shapley algorithm involves a number of "rounds" (or
  "iterations").

  In the first round, first a) each unengaged man proposes to the woman
  he prefers most, and then b) each woman replies "maybe" to her suitor
  she most prefers and "no" to all other suitors. She is then
  provisionally "engaged" to the suitor she most prefers so far, and
  that suitor is likewise provisionally engaged to her.

  In each subsequent round, first a) each unengaged man proposes to the
  most-preferred woman to whom he has not yet proposed (regardless of
  whether the woman is already engaged), and then b) each woman replies
  "maybe" to her suitor she most prefers (whether her existing
  provisional partner or someone else) and rejects the rest (again,
  perhaps including her current provisional partner).

  The provisional nature of engagements preserves the right of an
  already-engaged woman to "trade up" (and, in the process, to "jilt"
  her until-then partner).

  This algorithm guarantees that:

  Everyone gets married.

  Once a woman becomes engaged, she is always engaged to someone. So, at
  the end, there cannot be a man and a woman both unengaged, as he must
  have proposed to her at some point (since a man will eventually
  propose to everyone, if necessary) and, being unengaged, she would
  have had to have said yes.

  The marriages are stable.

  Let Alice be a woman and Bob be a man who are both engaged, but not to
  each other. Upon completion of the algorithm, it is not possible for
  both Alice and Bob to prefer each other over their current partners.
  If Bob prefers Alice to his current partner, he must have proposed to
  Alice before he proposed to his current partner. If Alice accepted his
  proposal, yet is not married to him at the end, she must have dumped
  him for someone she likes more, and therefore doesn't like Bob more
  than her current partner. If Alice rejected his proposal, she was
  already with someone she liked more than Bob.

It's not greedy, so I'm not totally answering the question, but it works. It's probably easier if you convert the problem to the marriage problem by changing the -1...2 to 1-n (by picking randomly higher preferences in the case of ties) before processing, I think.

Edit: Nevermind, this doesn't have the least number of talks either I think, but I figured it was still worth bringing up. Really it depends on whether those talking preferences are known beforehand (and we are optimizing the pairings, in which case this algorithm works), or whether those talking preferences aren't known until a talking session begins - in which case this algorithm isn't applicable at all. I mean you could just set everyone up with everyone else, compute these values, then run the algorithm above, but it's certainly not optimal.


The $\Omega(n^2)$ worst-case lower bound of Comb sort (or Dobosiewicz sort) has also been proved using the incompressibility method based on Kolmogorov complexity. See for example the survey by Vitanyi, page 16. If you are also interested in the average-case lower bound on the running time, the paper gives that as well. Moreover the proofs obtained with the method are natural, easy-to-follow and usually quite short.


Consequences/existence of problems without any "optimal" algorithm

Blum's speedup theorem, proved in 1967, shows that there is such a problem $P$ that has no optimal algorithm.

The problem $P$ doesn't look all that much like addition or graph coloring - it's defined in terms of sets of machines $Z_i$, the primitive recursive functions $\phi_i(n)$ computed by the $i$th machine, and "step-counting functions" $\Phi_i(n)$ (which count how many steps the $i$th machine took to execute its function), and involves search over the latter in order to achieve the desired properties :).

It's a good reminder that the space of algorithms is large and counterintuitive - especially when the inputs and outputs are themselves programs. But you're also not likely to see this sort of weirdness until your inputs are programs, either, and maybe not even then depending on what you're trying to do with them...

Reference:

Blum, Manuel. "A machine-independent theory of the complexity of recursive functions." Journal of the ACM (JACM) 14.2 (1967): 322-336.


Should one study undergrad TCS materials before taking grad-level ones? (soft question)

Yes.
From my experience, going back to basics teaches you new things every time.
My students tough me the most.


Chordal Graphs and maximum independent sets

There are arbitrarily long sub-path whose induced subgraph contains no three independent vertices.  See the graph below for length 4:

Indeed, vertices in a sub-path induces an interval subgraph.  So you can use standard interval models (the endpoints of the interval for a vertex $v$ are the indices of leftmost and rightmost bags that contain $v$) to construct the tight example easily.  The graph given above have intervals:
[1,1], [1,2], [1,3], [2,4], [3,4],[4,4].  Likewise, you can construct for a subpath of length n: the basic idea is that each interval either starts from 1 or ends at n.


Average-case analysis of algorithms using the incompressibility method

I think that the recent constructive proof of the Lovasz Local Lemma (http://blog.computationalcomplexity.org/2009/06/kolmogorov-complexity-proof-of-lov.html) and Patrascu's analysis of the component size in cuckoo hashing might both qualify.  These are both stated in terms of random strings, but would also work with Kolmogorov random strings (http://infoweekly.blogspot.com/2010/02/cuckoo-hashing.html).


Proof refutation: Amateur reviews of ambitious CoRR papers

If you make an arXiv trackback you will not be ignored, in the sense that future readers of the ambitious arXiv paper may check the trackbacks.

You even get a mild form of peer review for your posts, since they write:

  Because of widespread Trackback spam we have a semi-automated editorial process that approves trackbacks for display.

As for where to post your review, Recent trackbacks currently returns a mix of blogs, magazines, and news sites.


Where does the modern canonical version of the Turing machine come from?

Is it due to Sipser? Or Penrose?

Sorry, that made me laugh out loud.  Penrose?

Today's notion of formal language (a language is a set of words or strings) can be traced at least as far back as Frege in the late 1800's and Thue in the early 1900's.  Chomsky's 1956 paper was very influential, and definitely uses the term "language" for a set of strings.

There is also the 1961 paper of Bar-Hillel, Perles, and Shamir.  I would check that.

This 1963 paper by Evey (https://www.computer.org/csdl/proceedings/afips/1963/5063/00/50630215.pdf ) uses the term "language" in the modern sense in relation to machines.  Perhaps earlier explicit references can be found in the work of Emil Post.


How do conference proceedings add to academic prestige?

I don't think there is any TCS conference that would be a fast track to a permanent job.

STOC, FOCS, and SODA are the most competitive conferences, and papers in those will certainly look very good in your CV, but just one paper won't help that much with the career. To really stand out, you will need something more than that (say, lots of papers in STOC, FOCS, and SODA).


Monotone circuit complexity of computing functions on sparse inputs

specifically considering one part of the question (eg for $k_1$=1,$k_2$=2), Lokam studied "2-slice" functions in this paper & proves that strong lower bounds on them can be generalized, therefore this is a very hard open problem related to basic complexity class separation & any such construction/explicit function would be a breakthrough; from the abstract:

  A Boolean function f is called a 2-slice function if it evaluates to zero on inputs with less than two 1’s and evaluates to one on inputs with more than two 1’s. On inputs with exactly two 1’s f may be nontrivially defined. There is a natural correspondence between 2-slice functions and graphs. Using the framework of graph complexity, we show that sufficiently strong superlinear monotone lower bounds for the very special class of 2-slice functions would imply superpolynomial lower bounds over a complete basis for certain functions derived from them.

Graph Complexity and Slice Functions / Satyanarayana V. Lokam,
Theory Comput. Systems 36, 71–88 (2003)

also as in his comments SJ covers this similar case in his book in the section  exploring star complexity of graphs sec1.7.2.

Boolean function complexity: advances and frontiers, Stasys Jukna


Explanation of 1-generic to prove undecidability of halting problem

A finite prefix of  $G$ is $G \cap \{0,1,\ldots n\}$ for some $n$. It is easier if you look at the characteristic function of $G$ which can we viewed as an infinite word in $2^\omega$. Then a finite prefix is a finite initial part of $G$.

For forcing, there are many resources, depends on what you want to learn. A point to start is the Wikipedia pages and the references listed there: Forcing (set theory), Forcing (recursion theory). Timothy Chow's article A Beginner's Guide to Forcing is a good introduction.


What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?

The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of reductions, but clarify the presentation in my opinion.
Let's assume your language is given by
the following grammar.
$$
\newcommand{\PROGRAM}[1]{\mathsf{#1}}
\newcommand{\FV}[1]{\mathsf{fv}(#1)}
\newcommand{\DOM}[1]{\mathsf{dom}(#1)}
\newcommand{\VERTICAL}{\;  \mid\hspace{-3.0pt}\mid \; }
\newcommand{\CALLCC}{\PROGRAM{callcc}}
\newcommand{\CONT}[1]{\mathsf{Cont}(#1)}
\newcommand{\THROW}{\PROGRAM{throw}}
\newcommand{\infer}[2]{\frac{\displaystyle{ #1 }}{\displaystyle{ #2 }}}
\newcommand{\ZEROPREMISERULE}[1]{\infer{-}{#1}}
\newcommand{\FS}{\rightarrow}
\newcommand{\RED}{\rightarrow}
\newcommand{\ONEPREMISERULE}[2]{\infer{#1}{#2}}
\newcommand{\TYPES}[3]{#1 \vdash #2 : #3}
\newcommand{\TWOPREMISERULE}[3]{\infer{#1 \quad #2}{#3}}
   M ::= x \VERTICAL \lambda x.M \VERTICAL MM \VERTICAL ... \VERTICAL \CALLCC \VERTICAL \THROW
$$
Here $\CALLCC$ and $\THROW$ are seen as constants although we could also have defined them in different ways.
Let us denote by $\FV{M}$ the free variables of the program $M$.
Types could be something like this:
$$
        \alpha\
                ::=\
        \alpha \FS\alpha
\VERTICAL \PROGRAM{Int} \VERTICAL
        ...
                \VERTICAL
        \CONT{\alpha}
$$
Here $\CONT{\alpha}$ is the type of continuations with final answer
type $\alpha$.
The constants $\CALLCC$ and $\THROW$ are values and have the following types.
$$
        \ZEROPREMISERULE
        {
          \TYPES{\Gamma}{\CALLCC}{(\CONT{\alpha} \FS \alpha) \FS \alpha}
        }
                \qquad
        \ZEROPREMISERULE
 {
                \TYPES{\Gamma}{\THROW}{\CONT{\alpha} \FS \alpha \FS \beta}
        }
$$
Depending on your use-case, the type variables may be quantified.
Reductions are defined with the help of configurations.
A configuration is a pair $(M, \sigma)$ such that $M$ is a
program and $\sigma$, the continuation map, ranged over by
$\sigma, ...$, maps each $k \in \FV{M}$ of type $\CONT{\alpha}$ to an appropriately typed program.
Then
reductions are of the form $(M, \sigma) \RED (N,
\sigma')$. For  call-by-value, the reductions are generated as usual, with the following additions for $\CALLCC$
and $\THROW$.
$$
        \ONEPREMISERULE
        {
                k, x\ \text{fresh}
        }
        {
                (E[\CALLCC\ V], \sigma) \RED (E[V\;k], \sigma \cdot k \mapsto \lambda x.E[x])
        }
                \quad
        \ONEPREMISERULE
        {
                \sigma(k) = M
        }
        {
                (E[\THROW\ k\ V], \sigma) \RED (MV, \sigma)
        }
$$
Here $V$ over ranges over values, and
$E[\cdot]$ over the usual call-by-value reduction contexts. The two new constants give rise to the following evaluation contexts: $\CALLCC\ E[\cdot]$, $\THROW\ E[\cdot]\ M$
and $\THROW\ V\ E[\cdot]$.

Note that (1) does not use continuation maps to define the CBV semantics of $\CALLCC$
 and $\THROW$. Instead a run-time value is introoduced. The two approaches are equivalent.

As to evaluation order, $\CALLCC$ enriches the power of contexts and can distinguish  programs by application that are
  indistinguishable in the absence of continuations:

$$
  \newcommand{\ARGFC}{\PROGRAM{argfc}}
  \ARGFC  = \CALLCC\ \lambda k.(\THROW\ {k}\ {\lambda
  x.(\THROW\ {k}\ {\lambda y.x}}))
  $$

This is the classic example of calling a function once, but
  returning twice. e.g. in
  $$
  (\lambda x.(x\; 1);(x\; 2))\ \ARGFC = 1
  $$
  and
  $$
  (\lambda x.\lambda y.(x\; 1);(y\; 2))\ \ARGFC\ \ARGFC = 2
  $$

with $M;N$ being the sequential composition of $M$ and $N$, binding
more tightly than $\lambda$-abstraction.  The reason is that
continuations carry information about contexts that may be returned
(jumped) to later.

J. G. Riecke, H. Thielecke, Typed Exceptions and Continuations Cannot Macro-Express Each Other (Postscript file).
R. Harper, B. F. Duba, D. MacQueen, Typing First-Class Continuations in ML.
H. Thielecke, Continuations, functions and jumps.


Different algorithms for longest increasing subsequence

There is a $O(n \log \log n)$ time algorithm to solve the longest increasing subsequence problem. You may find this and the paper by Sergei Bespamyatnikh , Michael Segal helpful.


Computability theory in general has been somewhat under-formalized. The short answer is that most theorems of computability theory do not pass one of the three tests for formalization:

A proof that is computationally intensive or untrusted for some reason (long, complex).
A result that is relevant to undergraduate mathematics.
A result that is useful to program verification.

Reason 1 may apply in this case, but the preliminary work to build up to that result unfortunately hasn't been carried out. I found one reference to mechanized computability theory by Xu, Zhang and Urban in Isabelle. It falls significantly short of priority results though.


Max Non-overlapping Path in Weighted Graph

Yes, the Bellman-Held-Karp algorithm is not a complete enumeration and can be modified easily enough to solve your problem.

However, it still takes something over $2^n$ time (see question for details), and something exponential like that seems unavoidable since this is a variant of the traveling salesman problem.


In a resistor network, is there any relation between the shortest path and the maximum electric current path?

Just an extended comment to include the picture: if the following (random) resistor network is valid then the max current flow 33.9mA is not on the shortest path from $s$ (+5V) to $t$ (GND).


Robustness to non-uniform randomness vs. one-sidedness

Only one-sided deciders are robust to bad coins, under your definition; no other decider can be robust to bad coins.  Let $D$ be a decider that is not one-sided.  For $x \in \mathcal{Y}$, let $\mathcal{W}_x = \{r \in \{0,1\}^m : D(x,r)=\textsf{no}\}$ be the set of random strings $r$ such that $D$ outputs the wrong answer.  Consider a distribution $R$ that, with probability $1/3+\epsilon$, picks $r$ uniformly at random from $\mathcal{W}_x$, and with probability $2/3-\epsilon$, picks $r$ uniformly at random from its complement.  Then the decider is correct on $x$ with probability $2/3 - \epsilon$ when $r$ is chosen from $R$; yet $d_{TV}(R,U) = \epsilon$.  So, there is no $c \in [0,1)$ with the desired property; you'd need to take $c=1$.

If you relax your definition to allow $c \in [0,1]$, so that (non-one-sided) deciders robust to bad coins exist, then the answer to your question is yes, it is a strict subset.  It is not hard to come up with trivial examples.  For instance, suppose that $D$ is correct for all choices of $r$ except for a single bad value $r_\text{bad}$; if $r=r_\text{bad}$, then $D$ is incorrect.  This decider is robust to bad coins but is not a one-sided decider.

Moreover: with such an adjusted definition, every decider is robust to bad coins. By the definition of total variation distance and the definition of a decider,

$$\Pr_{r \in R}[\mathcal{W}_x] \le \Pr_{r \in U}[\mathcal{W}_x] + d_{TV}(R,U) \le 1/3 + d_{TV}(R,U),$$

so the probability that (1) holds is at least $2/3 - d_{TV}(R,U)$.  Thus, $D$ is robust to bad coins with $c = 1$.

So, I think you need to re-consider your definition of "robust to bad coins".  With your original formulation ($c \in [0,1)$), only one-sided deciders can ever meet it; with an adjusted formulation ($c \in [0,1]$), every decider meets it.  In both cases, it collapses to be equivalent to some other existing notion.  This suggests that we need a different definition.


As can be seen in the comments, Jukka provides a $2 \times 4$ counter example, which is further generalized by Peter to $4 \times 4$ to meet the requirements. Both analysis and program verification (use dynamic programming to calculate $\chi'$) can be performed to make sure $\chi \neq \chi'$ is possible when $n = 4$.

Actually Peter's generalization can be used to show there is an $n \times n$ matrix s.t. $\chi \neq \chi'$ for any $n$. The counter example is shown below:

$\begin{bmatrix}
1 1 0 0 0 \cdots 0 \\
0 1 1 0 0 \cdots 0 \\
0 0 0 0 0 \cdots 0 \\
0 0 0 0 0 \cdots 0 \\
\vdots \\
0 0 0 0 0 \cdots 0
\end{bmatrix}$

There's a unique column with two 1's. At least one continuous rectangle is needed to cover the 0's in this column. And this continuous rectangle doesn't cover any elements in the two rows corresponding to the two 1's. Remove this continuous rectangle and the rest will be a $2 \times n$ matrix:

$\begin{bmatrix}
1 1 0 0 0 \cdots 0 \\
0 1 1 0 0 \cdots 0
\end{bmatrix}$

which needs at least 5 continuous rectangles to cover. So $\chi' \geq 6$. However, it is easy to see $\chi \leq 5$. So $\chi \neq \chi'$.


Generalisation of the statement that a monoid recognizes language iff syntactic monoid divides monoid

Yes, these monoids have received attention in the research literature and actually lead to difficult questions.

Definition. A monoid $N$ is called projective if the following property holds: if $f:N \to R$ is a monoid morphism and $h:T \to R$ is a surjective morphism, then there exists a morphism $g:N \to T$ such that $f = h \circ g$.

You can find a long discussion on projective monoids in [1], right after Definition 4.1.33. It is shown in particular that every projective finite semigroup is a band (a semigroup in which every element is idempotent). But the converse is not true and it is actually an open problem to decide whether a finite semigroup is projective.

[1] J. Rhodes and B. Steinberg, The $q$-theory of finite semigroups. Springer Monographs in Mathematics. Springer, New York, 2009. xxii+666 pp. ISBN: 978-0-387-09780-0


Yes. See for example the stronger concentration for the occupancy problem in the following note:

http://sarielhp.org/teach/17/b/lec/10_martin_II.pdf

Theorems 10.3.1 and 10.3.2.
(This is also covered in the Randomized Algorithm book by Motwani and Raghavan).

The version stated here is the martingale version, but it is the same thing...


Structural equality of Pi Types with heterogeneous equality?

I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type:

coe : ∀{i}{A B : Set i} → A ≡ B → A → B

HEq : ∀ {i}{A B : Set i} → A → B → Set _
HEq {_}{A} {B} x y = Σ (A ≡ B) λ p → coe p x ≡ y

To do anything with HEq, it is enough to consider J and K for propositional equality. Dependent pattern matching is usually equivalent to J + K, although in Agda we can have pattern matching which is equivalent only to J.

So the question boils down to whether we can prove your lemma with J, or we need K as well. I prefer to work with uniqueness of identity proofs (UIP) instead of K (they are logically equivalent), so let's do that.

UIP : ∀ {i}{A : Set i}{x : A}{p : x ≡ x} → p ≡ refl

The answer is that we need UIP. Writing the lemma in Agda:

lem :
  ∀ (A₀ A₁ : Set)
    (A₀₁ : HEq A₀ A₁)
    (B₀ : A₀ → Set)
    (B₁ : A₁ → Set)
    (B₀₁ : HEq B₀ B₁)
  → HEq (∀ x → B₀ x) (∀ x → B₁ x)
lem A₀ A₁ (p , A₀₁) B₀ B₁ (q , B₀₁) = ?

It jumps at us that

A₀₁ : coe p A₀ ≡ A₁
p   : Set ≡ Set

In the absence of UIP, it is not provable that A₀ ≡ A₁, and therefore lem is not provable either. We can make it work with UIP. Agda code with intentionally puritan J usage:

{-# OPTIONS --without-K #-}

open import Data.Product

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

postulate
  UIP : ∀ {i}{A : Set i}{x : A}{p : x ≡ x} → p ≡ refl

J :
  ∀ {α β}{A : Set α} {x : A}(P : ∀ y → x ≡ y → Set β)
  → P x refl → {y : A} → (w : x ≡ y) → P y w
J P pr refl = pr

tr : ∀ {i j}{A : Set i}(B : A → Set j){a₀ : A}{a₁ : A}(a₂ : a₀ ≡ a₁) → B a₀ → B a₁
tr B p x = J (λ x _ → B x) x p

coe : ∀{i}{A B : Set i} → A ≡ B → A → B
coe = tr (λ x → x)

ap : ∀{i j}{A : Set i}{B : Set j}(f : A → B){a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
     → f a₀ ≡ f a₁
ap f p = tr (λ a₁ → f _ ≡ f a₁) p refl

sym : ∀ {i}{A : Set i}{x y : A} → x ≡ y → y ≡ x
sym p = tr (λ y → y ≡ _) p refl

HEq : ∀ {i}{A B : Set i} → A → B → Set _
HEq {_}{A} {B} x y = Σ (A ≡ B) λ p → coe p x ≡ y

lem :
  ∀ (A₀ A₁ : Set)
    (A₀₁ : HEq A₀ A₁)
    (B₀ : A₀ → Set)
    (B₁ : A₁ → Set)
    (B₀₁ : HEq B₀ B₁)
  → HEq (∀ x → B₀ x) (∀ x → B₁ x)
lem A₀ A₁ (p , A₀₁) B₀ B₁ (q , B₀₁) =
  tr (λ p → (A₀₁ : coe p A₀ ≡ A₁) → HEq (∀ x → B₀ x) (∀ x → B₁ x))
     (sym (UIP {p = p}))
     (λ A₀₁ →
          refl ,
          J (λ A₁ A₀₁ → ∀ B₀ B₁ (q : (A₀ → Set) ≡ (A₁ → Set))
                      → coe q B₀ ≡ B₁
                      → ((x : A₀) → B₀ x) ≡ ((x : A₁) → B₁ x))
            (λ B₀ B₁ q B₀₁ →
               tr (λ q → coe q B₀ ≡ B₁ → ((x : A₀) → B₀ x) ≡ ((x : A₀) → B₁ x))
                  (sym (UIP {p = q}))
                  (λ B₀₁ → ap (λ f → ∀ x → f x) B₀₁)
                  B₀₁)
            A₀₁ B₀ B₁ q B₀₁)
     A₀₁

This might seem a handful, but after some practice such code is a mechanical exercise which generally follows the compilation of pattern matching.

At this point we might ask if a variant of the lemma is provable only with J. The following is such, for example.

lemJ :
  ∀ (A₀ A₁ : Set)
    (A₀₁ : A₀ ≡ A₁)
    (B₀ : A₀ → Set)
    (B₁ : A₁ → Set)
    (B₀₁ : tr (λ X → X → Set) A₀₁ B₀ ≡ B₁)
  → (∀ x → B₀ x) ≡ (∀ x → B₁ x)
lemJ A₀ A₁ A₀₁ B₀ B₁ B₀₁ =
  J (λ A₁ A₀₁ → ∀ B₀ B₁ (B₀₁ : tr (λ X → X → Set) A₀₁ B₀ ≡ B₁)
              → ((x : A₀) → B₀ x) ≡ ((x : A₁) → B₁ x))
    (λ B₀ B₁ B₀₁ → ap (λ f → ∀ x → f x) B₀₁)
    A₀₁ B₀ B₁ B₀₁


Every graph G is a line graph of some hypergraph, for instance the one that has the edges of G as its vertices and the sets of edges neighboring each vertex of G as its hyperedges. Therefore, finding cliques in line graphs of hypergraphs can be no easier than finding cliques in arbitrary graphs.

Of course with your limitation of edge size $r$, one can only do this starting from a graph $G$ with degree $r$, and max clique in bounded degree graphs is not so hard, so this doesn't rule out the $n^{poly(r)}$ algorithm you're hoping for.


Is there a W[1]-hard problem that can be solved in $2^{o(n)}$ time?

How about Planar Capacitated Dominating Set? It is W[1]-hard (see the paper by Bodlaender, Lokshtanov, Penninkx in IWPEC 2009), but should be solvable in $2^{O(\sqrt{n}\log n)}$ by using the fact that planar graphs have treewidth $O(\sqrt{n})$.

In this problem we are given a graph with integer capacities on the vertices. We are asked to select a minimum size dominating set, with the added restriction that a selected vertex can dominate at most as many of its neighbors as its capacity. Even though the solution is not exactly a subset of $V$, I think it is known that, if we are given a supposed dominating set $D$ we can check if it can be turned into a valid (capacity-respecting) solution in polynomial time by reduction to Max Flow.


Graph traversal with vertex and edge deadlines/windows

It is NP-hard to decide whether your problem is soluble. That's bad news from a theoretical point of view, but in practice it is possible that a heuristic algorithm will fare quite well. Also, you're (possibly) dealing with the "promise" variant of the problem, that is, you assume that a solution exists, and want to find it.

To see that the problem is NP-hard, we reduce Hamiltonian cycle to it. All the edges are always open, and they always have unit weight. The windows for each non-zero vertex are $[1,n-1]$ and $[n+1,2n-1]$; for vertex zero they are $\{0\}$ and $\{n\}$. These constraints are satisfiable only via a Hamiltonian cycle, and the converse is also true.


The problem can be restated as a #2SAT. See

http://en.wikipedia.org/wiki/2-satisfiability

under the "Counting the number of satisfying assignments" section for some references to the currently best exact counting algorithms.


"Relatives" of the shortest path problem

Here is an answer to the first problem:

  Path with minimum weight gap: find an $s-t$ path, such that the difference between the largest  and smallest edge weights on the path is minimum.

A paper from 1984 shows that whenever we can decide
feasibility (does there exist a solution in the unweighted
case) for some combinatorial optimization problem in
polynomial time, then we can also find in polynomial
time a solution that minimizes the differenc between the
largest and smallest cost coefficient (in the weighted case):

  S. Martello, W.R. Pulleyblank, P. Toth, D. de Werra
  Balanced optimization problems
  Operations Research Letters 3, 1984, Pages 275-278

This implies a polynomial time algorithm to your question.


Intuitionistic fragments of classical logic

As requested, I'm turning my comment into an answer:

For first order logic, the term you want to search for is “Glivenko classes”. Probably, very similar characterizations and techniques apply for higher order logic. See Sara Negri's Glivenko sequent classes in the light of structural proof theory.


Scope of active substitutions in the applied $\pi$-calculus

The key to understanding scope management in $\pi$-calculi is to look at the structural congruence $P \equiv Q$ and at the notions of free name $\newcommand{\FN}[1]{\text{fn}(#1)}\FN{P}$ and free variable $\newcommand{\FV}[1]{\text{fv}(#1)}\FV{P}$. The great novelty that distinguishes $\pi$-calculi from its predecessors is the ability to extrude scope. It is guided by the following law.

$$
   P \ |\ (\nu x)Q \ \equiv\ (\nu x)(P\ |\ Q) \qquad \text{if $x \notin \FN{P} \cup \FV{P}$}.
$$

This rule is also at the heart of the applied $\pi$-calculus, otherwise it would not be a $\pi$-calculus. In order to understand the scope of active substitution in the applied $\pi$-calculus, we need to understand the free names and variables of an active substitution. This is defined in Section 2.1 of "Mobile values, new names, and secure communication", the paper that introduces the applied $\pi$-calculus:

$\FV{\{M/x\}} = \FV{M} \cup \{x\}$.
$\FN{\{M/x\}} = \FN{M}$.

The full definition of structural congruence in applied $\pi$ is a bit more elaborate because the calculus parameterises the definition of structural congruence with application-specific equations that define cryptographic primitives, e.g. $\text{decode}_k(\text{encode}_k(msg)) \equiv msg$. In other words, the algebraic laws that give the (formal) cryptography are embedded in the structural congruence. In addition, active substitution itself has associated structural congruence laws:

$(\nu x)\{M/x\} \equiv 0$.
$\{M/x\} | P \equiv \{M/x\} | P\{M/x\}$.
$\{M/x\} \equiv \{N/x\}$ whenever the equation $M = N$ holds in the paramterisation.

None of these additional structural congruences does anything 'unusual' with extrusion, so, as Damiano says, whether $M$ substitutes for $x$ in $N$ has nothing to do with restrictions 'on the outside' in $(\nu \vec{n})(\{M/x\} | N)$, but only with $x$ occurring in $N$ or not.


Connecting cells by line and column permutations in a finite grid

Let's try a similar counting argument to the one in the earlier version of my answer, more carefully.

Given an input 0-1 matrix with q nonzeros, define a "solution" to be a permutation of the rows, a permutation of the columns, and the connected 0-1 matrix that one gets as output after performing the permutations. The important observation here is that there are at most $n^2 2^{5q}$ different output matrices possible: once we make one of $n^2$ choices for the position of one of the nonzeros, we can encode the rest of the output matrix in $5q$ bits by doing a preorder traversal of a spanning tree of the nonzeros and recording for each edge in the tree whether it goes to a leaf, whether it is the last edge from its parent, and what its direction is. So the number of solutions is in total at most $n^2 2^{5q} (n!)^2$.

Now each solution works only for a single input, because we can reverse the permutations to get the input back from the output matrix. The number of inputs that have exactly $c$ nonzeros per row is $\binom{n}{c}^n$, and for $c$ constant this can be rewritten $\exp(cn\log n-O(n))$. But for $q=cn$ the number of solutions is $\exp(2n\log n+O(cn))$. For $c>2$, the inputs outnumber the solutions, so there is an unsolvable input.


Understanding the definition of a "restriction of a resolution derivation"

For the first point, it seems that $C_{j_1} := D_{j_1} \lor y$ and $C_{j_2} := D_{j_2} \lor \bar{y}$ are meant to be the clauses in $\pi$, instead of $C_{j_1} \lor y$ and $C_{j_2} \lor \bar{y}$. This may help in understanding such a definition. Furthermore, it seems that the resolution of $C'_{j_1}$ and $C'_{j_2}$ upon $y$ is taken, rather than $C'_{j_1} \lor C'_{j_2}$ (they are equivalent).
This view would explain, for example, the computation of $C_4[x=0]$: $C_1' = x_2 \lor \bar{x_3}$ and $C_2' = x_3$ are resolved upon $x_3$ to obtain $C_4' = x_2$.

For the second point: the computations are meant to produce the same output. In the paper, the final result without any computation is shown. Going through the recursive computation by pencil and paper shows how the rules are used.


Finding a graph that minimizes the number of nodes for a given number of paths

If I understand the problem properly, the answer should be $2 \log_2(n)$: make a graph with $\log_2(n) + 2$ layers, where the first layer is just $A$, the last layer is just $B$, and the intermediate layers have $2$ nodes each; we then put a directed edge from each node to the node(s) in the next layer.  We then have $2^{\log_2(n)} = n$ paths from $A$ to $B$, and the union of these paths contains $2 \log_2(n)$ intermediate nodes.

Does this fit the constraints of your problem?


$\let\mr\mathrm$There are several results in the literature stating that a certain class $C$ satisfies $C\nsubseteq\mr{SIZE}(n^k)$ for any $k$, and usually it is straightforward to pad them to show that any barely superpolynomially expanded version of $C$ is not in $\mr{P/poly}$.

Let me say that $f\colon\mathbb N\to\mathbb N$ is a superpolynomial bound if it is time-constructible, and $f(n)=n^{\omega(1)}$. For example, $n^{\log\log\log\log n}$ is a superpolynomial bound. In fact, an instructive exercise shows that if $g(n)$ is any unbounded monotone computable function, there is a superpolynomial bound $f$ such that $f(n)\le n^{g(n)}$.

First, direct diagonalization shows that $\Sigma_4^P\nsubseteq\mr{SIZE}(n^k)$ for any $k$. The same argument gives:

If $f$ is any superpolynomial bound, then $\Sigma_4\text-\mr{TIME}(f(n))\nsubseteq\mr{P/poly}$.

Proof sketch: For any $n$, let $C_n$ be the lexicographically first circuit of size $2f(n)$ that computes a Boolean function in $n$ variables not computable by a circuit of size $<f(n)$. Then, the language $L$ defined by $x\in L\iff C_{|x|}(x)=1$ works.

A well-known improvement states that $S_2\mr P\nsubseteq\mr{SIZE}(n^k)$ for any $k$. Likewise,

If $f$ is any superpolynomial bound, then $S_2\text-\mr{TIME}(f(n))\nsubseteq\mr{P/poly}$.

Proof sketch: If not, then in particular $\mr{NP}\subseteq S_2\mr P\subseteq\mr{P/poly}$, hence $\mr{PH}=S_2\mr P$. By a padding argument, $\Sigma_4\text-\mr{TIME}(f(n))\subseteq S_2\text-\mr{TIME}(f(n))\subseteq\mr{P/poly}$, quod non.

Oblivious classes do even better. Taking into account the objection raised by Apoorva Bhagwat, let $\mr{NLin=NTIME}(n)$. Then $\mr{NLin}\cup O_2\mr P\nsubseteq\mr{SIZE}(n^k)$ for any $k$, and the same argument yields:

If $f$ is any superpolynomial bound, then $\mr{NLin}\cup O_2\text-\mr{TIME}(f(n))\nsubseteq\mr{P/poly}$.

Proof sketch: If $\mr{NLin\subseteq P/poly}$, then by padding, $\mr{NP\subseteq P/poly}$, which implies $\mr{PH}=O_2\mr P$. Then we proceed as before.

There are also results involving MA. The often mentioned result that $\mr{MA\text-EXP\nsubseteq P/poly}$ is an overkill. Santhanam proved
$$\mr{promise\text-MA\cap promise\text-coMA\nsubseteq SIZE}(n^k)$$
for any $k$, and a similar argument gives:

If $f$ is any superpolynomial bound, then
$$\mr{promise\text-MA\text-TIME}(f(n))\cap\mr{promise\text-coMA\text-TIME}(f(n))\nsubseteq\mr{P/poly}.$$

Proof sketch: By Santhanam’s Lemma 11 (which is a sharpened version of the standard fact that $\mr{PSPACE=IP}$ with a PSPACE prover), there is a PSPACE-complete language $L$ and a randomized poly-time oracle TM $M$ such that on input $x$, $M$ only asks oracle queries of length $|x|$; if $x\in L$, then $M^L(x)$ accepts with probability $1$; and if $x\notin L$, then for any oracle $A$, $M^A(x)$ accepts with probability $\le1/2$.

For a suitable monotone polynomial $p$, let $A=(A_{\mr{YES}},A_{\mr{NO}})$ be the promise problem defined by
$$\begin{align}
(x,s)\in A_{\mr{YES}}&\iff\exists\text{circuit }C\,\bigl(p(|C|+|x|)\le f(|s|)\land\Pr[M^C(x)\text{ accepts}]=1\bigr),\\
(x,s)\in A_{\rlap{\mr{NO}}\phantom{YES}}&\iff\forall\text{circuit }C\,\bigl(p(|C|+|x|)\le f(|s|)\to\Pr[M^C(x)\text{ accepts}]\le1/2\bigr).
\end{align}$$
Let $h(x)$ be a polynomial reduction of $L$ to its complement, and let $B=(B_{\mr{YES}},B_{\mr{NO}})$ be the promise problem
$$\begin{align}
(x,s)\in B_{\mr{YES}}&\iff(x,s)\in A_{\mr{YES}}\land(h(x),s)\in A_{\mr{NO}},\\
(x,s)\in B_{\rlap{\mr{NO}}\phantom{YES}}&\iff(x,s)\in A_{\mr{NO}}\land(h(x),s)\in A_{\mr{YES}}.
\end{align}$$
If $p(n)$ is chosen suitably large,
$$B\in\mr{promise\text-MA\text-TIME}(f(n))\cap\mr{promise\text-coMA\text-TIME}(f(n)).$$
So, let us assume for contradiction that $B$ has polynomial-size circuits, say, $B\in\mr{SIZE}(n^k)$. Let $s(n)$ denote the size of the smallest circuit computing $L$ on inputs of length $n$, and put $t(n)=f^{-1}(p(s(n)))$; more precisely,
$$t(n)=\min\{m:p(s(n))\le f(m)\}.$$
Then $x\mapsto(x,1^{t(n)})$ is a reduction of $L$ to $B$, thus $L\in\mr{SIZE}(t(n)^k)$, which means
$$s(n)\le t(n)^k.$$
But since $f$ is superpolynomial, we have $t(n)=s(n)^{o(1)}$. This gives a contradiction for $n$ sufficiently large.

If we prefer a result with a non-promise version of MA, Miltersen, Vinodchandran, and Watanabe proved
$$\mr{MA\text-TIME}(f(n))\cap\mr{coMA\text-TIME}(f(n))\nsubseteq\mr{P/poly}$$
for a half-exponential function $f$. We can improve it in two ways: first, it holds for $\tfrac1k$-exponential bounds for any constant $k$, and second, it holds for oblivious classes. Here, a $\tfrac1k$-exponential function is, roughly speaking, a function $f$ such that $\underbrace{f\circ\dots\circ f}_k=\exp$. See the Miltersen–Vinodchandran–Watanabe paper and references therein for the precise definition; it involves a well-behaved family of well-behaved functions $e_\alpha(x)$, $\alpha\in\mathbb R_+$, such that $e_0(x)=x$, $e_1(x)=e^x-1$, and $e_{\alpha+\beta}=e_\alpha\circ e_\beta$. Also, if $f(n)\le e_\alpha(\mr{poly}(n))$ and $g(n)\le e_\beta(\mr{poly}(n))$, then $f(g(n))\le e_{\alpha+\beta}(\mr{poly}(n))$. Then we have:

$\mr{OMA\text-TIME}(e_\alpha)\cap\mr{coOMA\text-TIME}(e_\alpha)\nsubseteq\mr{P/poly}$ for any $\alpha>0$.

Proof sketch: Assume otherwise. Fix an integer $k$ such that $1/k<\alpha$. Let me abbreviate
$$\mr{OcOMT}(f)=\mr{OMA\text-TIME}(\mr{poly}(f(\mr{poly}(n)))\cap\mr{coOMA\text-TIME}(\mr{poly}(f(\mr{poly}(n))).$$
By padding, we have
$$\tag{1}\mr{OcOMT}(e_{\beta+1/k})\subseteq\mr{SIZE}(e_\beta(\mr{poly}(n)))$$
for any $\beta\ge0$. Moreover, using e.g. Santhanam’s Lemma 11 above, we have the implication
$$\tag{2}\mr{PSPACE\subseteq SIZE}(e_\beta(\mr{poly}(n)))\implies\mr{PSPACE\subseteq OcOMT}(e_\beta).$$
Since trivially $\mr{PSPACE\subseteq OcOMT}(e_1)$, a repeated application of (1) and (2) shows $\mr{PSPACE\subseteq SIZE}(e_{(k-1)/k}(\mr{poly}(n)))$, $\mr{PSPACE\subseteq OcOMT}(e_{(k-1)/k})$, $\mr{PSPACE\subseteq SIZE}(e_{(k-2)/k}(\mr{poly}(n)))$, $\mr{PSPACE\subseteq OcOMT}(e_{(k-2)/k})$, and so on. After $k$ steps, we reach
$$\mr{PSPACE\subseteq P/poly}\qquad\text{and}\qquad\mr{PSPACE=OMA\cap coOMA}.$$
Using padding once more, we get
$$\mr{DSPACE}(e_{1/k})\subseteq\mr{OcOMT}(e_{1/k})\subseteq\mr{P/poly},$$
which contradicts the results above, as $e_{1/k}$ is a superpolynomial bound.


Vertex isoperimetric number of a graph - NP-hard?

The following paper:
On an isoperimetric problem for Hamming graphs
L.H. Harper. contains the following:

  The vertex-isoperimetric problem is NP-complete [8] in
  general, so no polynomially bounded solution is known and it is unlikely that one
  exists.

Where reference [8] is
M.R. Garey, D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness,

This book usually either contains a proof or a reference to the proof.
Unfortunately I have no access to the book at the moment.


Does this bin packing problem have a name?

Your problem is the multiple knapsack problem.

Although I am not familiar with this problem, I believe you'll find some papers on your problem, since there are many papers on this problem (see for example a SODA 2009 paper)


Is there an accepted name for Ross Quinlan's adaptation of the ID3 decision algorithm to use a Pearson's chi-squared test for independence?

Unfortunately, I'm not able to get into detail of the ID3 paper you cited.

I read the Quinlan's book about C4.5 and I don't remember any quote about Chi-square splitting procedure. However, it exists a decision trees induction process that uses Chi-squares as splitting procedure, it is CHAID: http://en.wikipedia.org/wiki/CHAID.

By the way, do you really need a Chi-square splitting procedure? Good permances of C4.5 are well known, and it uses Information Gain as splitting criterion. Moreover, classical Data Mining books (such as Introduction to Data Mining by Tan et al.) state that better performances can be achieved with different pruning techniques rather than different splitting criteria.

If you really want a Chi-square splitting procedure I would suggest to use CHAID or modify the Java implementation of C4.5 in WEKA.


Simple candidates for pseudorandom permutations?

Yes.  The following paper presents a candidate for a PRF that is implementable in $NC^1$, whose security is based on a lattice assumption (hardness of LWE):

Abhishek Banerjee, Chris Peikert, Alon Rosen.  Pseudorandom Functions and Lattices.  EUROCRYPT 2012.

It also has some discussion of related literature that might be helpful.

Also, here are two trivial observations.

First, there is a PRP that can be computed in $NC^1$ if and only if there is a PRF that can be computed in $NC^1$.  The "only if" part is immediate, as any PRP with large domain is also a PRF.  The "if" part follows from the Luby-Rackoff construction (i.e., the Feistel cipher), as that shows how to build a PRP out of any PRF; it increases the depth by only a constant factor.

Second, the following paper shows that no PRF can be computed by an AC0 circuit.

Nathan Linial, Yishay Mansour, Noam Nisan.  Constant depth circuits, Fourier transform, and learnability.  Journal of the ACM, 40(3):607--620, 1993.

It follows that no PRP can be computed by an $AC^0$ circuit.


Kolmogorov Complexity applications in Number Theory

Every integer has an associated Kolmogorov complexity; the shortest program that prints that integer.

There are $\approx {x \over ln(x)}$ primes up to $x$ so primes have lower Kolmogrov complexity than composites on average; $\approx ln({x \over ln(x)})$    vs  $\approx ln(x)$.

As a side effect you have to have some large gaps between primes; otherwise you could encode every number as the previous prime plus some small number of bits.