What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?

I've already answered somewhat, but I'll try to give a more detailed overview of the type theoretical horizon, if you will.

I'm a bit fuzzy on the historical specifics, so more informed readers will have to forgive me (and correct me!). The basic story is that Curry had uncovered the basic correspondence between simply-typed combinators (or $\lambda$-terms) and propositional logic, which was extended by Howard to cover first-order logic, and IIRC independently discovered by de Bruijn in investigations around the hugely influential Automath system.

The Automath system was a refinement of Church's simple type theory which itself was a dramatic simplification of Russel and Whitehead's type theory with universes and the axiom of reducibility. This was relatively well-known logical terrain by the 1960s.

However, giving a coherent, simple, foundational system that encompassed both proof and term systems was still a very open question by 1970, and a first answer was given by Per Martin-Löf. He gives a very philosophical overview On the Meaning of the Logical Constants and the Justification of Logical Laws. He reasons that both in logic and mathematics, the meaning of constructions can be given by examining the introduction rules which allow the formation of those constructions as judgements, e.g. for conjunction
$$ \frac{\vdash A\quad \vdash B}{\vdash A\wedge B}$$

Determines the corresponding elimination rule. He then gave a very powerful foundational system based on such judgements, allowing him to give a foundational system similar to Automath using very few syntactic constructions. Girard found that this system was contradictory, prompting Martin-Löf to adopt "Russel-style" predicative universes, severely limiting the expressiveness of the theory (by effectively removing the axiom of reducibility) and making it slightly more complex (but had the advantage of making it consistent).

The elegant constructions allowing for the definition of the logical symbols didn't work anymore though, which prompted M-L to introduce them in a different form, as inductively defined families. This is a very powerful idea, as it allows defining everything from judgmental equality and logical operators to natural numbers and functional data-types as they appear in computer science. Note that each family we add is akin to adding a number of axioms, which need to be justified as consistent in each instance. This system (dependent types + universes + inductive families) is usually what is referred to as ITT.

However there was some lingering frustration, as the powerful but simple foundational system was inconsistent, and the resulting system was more complex, and somewhat weak (in the sense that it was difficult to develop much of the modern mathematical framework in it). Enter Thierry Coquand, who with his supervisor Gerard Huet, introduced the Calculus of Constructions (CoC), which mostly solved these issues: a unified approach to proofs and data-types, a powerful (impredicative) foundational system and the ability to define "constructions" of the logical or mathematical variety. This eventually matured into an actual implementation of a system designed as a modern alternative to Automath, culminating in the Coq system we know and love.

I highly suggest this foundational paper on CoC, as Thierry knows a ridiculous amount about the historical development of type theory, and probably explains this much better than I. You might also want to check out his article on type theory, though it doesn't explain the C-H correspondence in much detail.


Complexity: simulated annealing vs. quantum annealing

In Rough Large Deviation Estimates for Simulated Annealing: Application to Exponential Schedules a theoretical justification for the exponential cooling schedule was given. The results there basically state that for a fixed computation time N you can always choose an appropriate constant $ C= f(N)$  for an exponential cooling schedule $ \beta = \beta_0 \cdot \exp \left( n f(N) \right) $ with $ f(N) \sim N^{-1} \ln\left(N\right) $, such that simulated annealing will converge. So in light of these results I would say it is clear that simulated annealing can converge faster than quantum annealing, at least for the quantum annealing schedule result you cited. Although, it seems you have to tweak the cooling schedule to the computation time.

A nice overview of theoretically grounded acceleration of simulate annealing is given here Theoretically Grounded Acceleration Techniques for Simulated Annealing


The following paper answers the question in the affirmative – the variant remains NP-hard using a reduction from Monotone Planar 3-SAT:
http://epubs.siam.org/doi/abs/10.1137/1.9781611976465.105
(arXiv: http://arxiv.org/abs/2009.12369)
The paper presents a slightly more restricted variant, Monotone Planar 3-SAT with Neighboring Variable Pairs, which requires each clause with three variables to contain two variables that are adjacent on the line on which all variables are embedded.
If there is a bi-enclosing clause in this variant, it must enclose a redundant clause due to monotonicity, so we can assume no bi-enclosing clauses.


Generalizing Brzozowski's DFA minimization algorithm to finite automata with different classes of accepting states?

The answer to your question is yes.

See Bonchi, Bonsangue, Rutten and Silva's papers Brzozowski's algorithm (co)algebraically (shorter conference version) and Algebra-Coalgebra Duality in Brzozowski’s Minimization Algorithm (longer journal version with more generalizations).

They give a (lightly) categorical presentation of Brzowzowski's algorithm, and use it to derive versions of it for more general classes of automata, including Moore automata (which gives an affirmative answer to your question).


Minor closed properties that are explicitly MSO expressible

I had an answer here involving apex graphs but it fails the definition of not having an explicit obstruction set given in this question: there is a published algorithm for finding the obstruction set, even though is too slow to run so we don't actually know what the obstruction set is.

So here's another parameterizable family of answers without that flaw (at least, as far as I know). Given a minor closed family $F$, and an integer $k\ge 1$, does the given graph $G$ have a $k$-ply covering graph in $F$? Much about this sort of question remains unknown: in particular, Negami's conjecture, which would characterize the graphs that have a planar covering graph, remains unproven. And it's minor-closed because any steps that you take to make a minor from $G$ can be copied in the cover.

To test for the existence of a $k$-ply cover of $G$ in $F$, in MSO$_2$, do the following steps:

Use the depth-first-search-tree trick to get an (arbitrary) orientation of $G$.
For each pair $(i,j)$ with $0\le i,j<k$, choose a set of edges in $G$, supposedly the ones that have a covering edge that goes from ply $i$ to ply $j$.
Check that each vertex in each ply has exactly one copy of each incident edge, and thus that this information represents a valid covering graph of $G$.
Emulate the obstruction set based formula for membership in $F$ on the covering graph.


Correctness of AKS algorithm for shortest vector problem

What you seem to be missing is that $\tau$ is not applied to all "green" vectors. Instead, think of every point $x_i$ as having a coin attached to it. Before you use $x_i$ in the algorithm, you toss the coin to decide whether to keep $x_i$ as $x_i$ or to replace it by $\tau(x_i)$. This is done independently for each $x_i$, so, with very high probability, the fraction of green vectors that $\tau$ is applied to will be very close to $\frac12$.

I have always found this analysis mysterious, but let me try to give some intuition. I think the analysis tries to exploit the fact that the sieving step only uses $y_i$, and $y_i$ does not distinguish between $x_i$ and $x_i\pm v$ for any lattice vector $v$. Since the sieving step does not need this information, you can think of the analysis as "hiding" from the algorithm which point in the pair $\{x_i, \tau(x_i)\}$ was actually sampled, until the algorithm absolutely must know this information. This is sometimes called the principle of deferred decisions. With this trick, you can argue that there are many possible random choices that would've led to the same set of points surviving to step 3 of the algorithm, and then you argue that at step 3 many of these random choices lead to a correct output. On the other hand, if you applied $\tau$ to every point, then you wouldn't "hide" anything from the algorithm, i.e. you wouldn't be taking advantage of the fact that there is randomness that's not used by the sieving step 2, and is "free" to be used at step 3.


Machine Learning: Calibrating SubGroups of Probability Predictions inside a Dataset which should sum to 100%

Let $p_i=\Pr[F_i]$ be the probability that flower $i$ is a daffodil, according to your model (without taking into account the group structure).
Now you are given a group of 10 flowers, with probabilities $p_1,\dots,p_{10}$, and you're given the promise that exactly one of them is a daffodil.  To update your probabilities based on this additional promise, you can use Bayes rule.  Let $E$ be the event that exactly one in the group is a daffodil.    Then
$$\begin{align*}
\Pr[F_i|E] &= {\Pr[F_i \land E] \over \Pr[E]}\\
&= {\Pr[F_i \land E] \over \sum_j \Pr[F_j \land E]}.
\end{align*}$$
Note that
$$\Pr[F_i \land E] = \Pr[\neg F_1 \land \cdots \land \neg F_{i-1} \land F_i \land \neg F_{i+1} \land \cdots] = (1-p_1) (1-p_2) \cdots p_i \cdots (1-p_{10}) = {p_i \over 1-p_i} \prod_j (1-p_j).$$
Therefore,
$$\Pr[F_i|E] = {{p_i \over 1-p_i} \over \sum_j {p_j \over 1-p_j}}.$$
This is the probability you wanted to compute; so, use that.


How do database aggregations form a monoid?

You ask why database aggregations have monoidal structure.

Say we want to combine data values $a$ and $b$, but want to keep things general -- these may be integers, strings, floating point numbers, vectors, matrices, probability distributions, sets, or anything else we want to store and manipulate.  So we denote the "aggregation" of $a$ and $b$ by $a.b$.

The operation $.$ is usually associative, since we don't want the order in which it is applied to affect the result: we want $(a.b).c = a.(b.c)$.  So we have a semigroup.

Almost always there is some kind of identity, whether it is the number 0 or 1, the empty string, an identity matrix, a uniform distribution, or the empty set, which depends on the operation.  So in fact data usually forms a monoid.

The practical point about thinking of data as forming a monoid is that it provides a way to discuss operations on different kinds of data using a common algebraic language.  This then translates into generic code libraries that can deal with any monoids, by simply passing an appropriate aggregation operation as an argument.

Note that many kinds of data do not have inverses, so a group structure is too much to hope for.  If you have group structure then some additional ways of manipulating the data become possible, but since neither matrices with multiplication, nor the positive integers with addition have inverses, non-group-structured data is quite common.

We don't usually want to just store data, but to run queries over the database.  So we need some notion of what to do when a query generates many answers.  Often this requires a combining operation $+$ (which may be the same as $.$), and which should be compatible with $.$ in the way they interact.  So some kind of distributivity is needed.  Commutativity of $+$ and sometimes also of $.$ is also often natural.  We then have a semiring or a commutative semiring.  Again inverses are usually too much to hope for, so semirings are a better fit than rings.

A semiring model of data aggregation has been around in the constraint satisfaction community for some time.  Note that a constraint satisfaction problem instance is a conjunctive query over a particular database of facts, so this is pretty general: most practical queries over data are conjunctive.

Stefano Bistarelli, Ugo Montanari, and Francesca Rossi,
Semiring-based constraint satisfaction and optimization,
JACM
44(2),
1997,
201–236.
doi:10.1145/256303.256306

The current spurt of theoretical analysis of the semiring model of data aggregation was kick-started in 2007, in the context of provenance.  Provenance is a fancy term for annotating data.  Since any database tuple can be seen as annotations applied to some unique tuple identifier, aggregation of data can be seen as just combination of annotations.  Provenance is therefore a generalization of the idea of aggregating data, and it has explicitly been argued that the right theoretical model of combining annotations is a semiring.  The most general semiring, of provenance polynomials, actually allows one to keep track of the entire history of how a piece of data was obtained from constituent parts.  As an example, a p-value in the analysis of a clinical trial can keep track of how it was calculated from each of the individual trial results.  If some of them turn out to be wrong (or fake) then one can simply recalculate without the bad data.

Todd J. Green, Grigoris Karvounarakis, and Val Tannen, Provenance semirings, PODS 2007, 31–40.
doi:10.1145/1265530.1265535

There has been a lot of further work using semirings to aggregate data, see the papers citing this one.

From the more immediately practical perspective that you cite, see for instance the GDL framework for how one can effectively parallelise a computation by grouping the underlying semiring expression appropriately.

Srinivas M. Aji and Robert J. McEliece,
The generalized distributive law,
IEEE Transactions on Information Theory
46(2),
2000,
325–343.
doi:10.1109/18.825794


No and in a sense yes.

No - this question is strongly reminiscent of those about SQL and the conclusion that it isn't (Turing complete). Despite its many capabilities, Redis does not provide looping or recursion for via native API, so that pretty much nails it.

However, you can easily run Lua scripts in Redis and Lua is in fact Turing complete, so in a sense so is Redis (similarly to how SQL becomes so once you allow the use of PL/SQL or the likes).


Is $\{0,1\}$-Vector bin packing NP-Hard when vectors have constant dimension?

EDIT: Merged the two answers.

Here's the problem statement:

The input is $(V, \mathbf b, \ell)$, where $V=\{x_1,x_2,\ldots,x_n\}$ with each $x_i\in\{0,1\}^d$ (where $d$ is constant), vector $\textbf{b}=(b_1,b_2,\ldots,b_d)\in \mathbb{Z}_+^d$, and $\ell$ is an integer.
The problem is to decide whether $V$ can be partitioned into $\ell$ parts $V_1,V_2,\ldots,V_\ell$ such that $\forall~j,\sum_{x_i\in V_j} x_i \leq \textbf{b}$.

Lemma 1. The problem (with $d=O(1)$) reduces to a sparse language, so is not NP-hard unless P=NP.

Lemma 2. For $d=O(1)$ and $\ell=O(1)$, the problem can be solved in polynomial time via dynamic programming (EDIT: or an ILP of constant dimension).

Lemma 3. For $d=O(1)$ and $\max_j b_j=O(1)$, the problem can be solved in linear time (in the real RAM model) via an ILP of constant dimension.

This leaves open the complexity of the case when $\ell$ and $\max_j b_j$ are both allowed to grow (while $d=O(1)$).  This case could be in P, or not in P but not NP-hard.

Proof of Lemma 1. One can faithfully re-encode any problem instance given in the form above into a representation that uses only $O(\log n)$ bits, as follows. For each of the $2^d$ possible vectors in $\{0,1\}^d$, write down the number of times that vector occurs in $V$.  Write down $\ell$ and each entry of $\mathbf b$.

There are $2^d + d + 1$ numbers written, and each number is at most $n$, so the encoding size is $\Theta(2^d\log n)$ bits.)  It follows that (for fixed $d$) the number of distinct instances of size $n$ is polynomial in $n$.  This implies (details next) that the decision problem cannot be NP-hard unless P=NP.

In more detail, let $L$ denote the language for the problem encoded as first defined.  Assume that $L$ is NP-hard.  Define $L' = \{(f(V, \mathbf b, \ell), 1^{|V|}) : (V, \mathbf b, \ell) \in L\}$, where $f(V, \mathbf b, \ell)$ is the re-encoding of the instance as described above (into $O(\log |V|)$ bits), and $1^{|V|}$ is $|V|$ in unary.

$L$ reduces in poly-time to $L'$, so $L'$ is also NP-hard.  But $L'$ is sparse (the number of elements of size $n$ is polynomial in $n$), so P=NP (by Mahaney's theorem). $~~~\Box$

Proof of Lemma 2.
The algorithm will solve the following more general problem.
The input is $(V, \mathbf B)$ where $V=\{x_1,\ldots,x_n\}$ (as before) and $\mathbf B = (B_1, B_2, \ldots, B_\ell)$ is a collection of $\ell$ vectors,
where each $B_j$ is in $\{0,1,\ldots,n\}^d$.
The problem is to decide whether there is a partition of $V$ into parts
$(V_1, V_2, \ldots, V_\ell)$ such that $\forall j,~\sum_{x_i\in V_j} x_i = B_j$.

This differs from the original problem in two ways.  First, each part $V_j$ in the partition can have a different required sum $B_j$ (instead of $\mathbf b$).  Second, equality must hold (the sum must equal $B_j$, rather being $\le \mathbf b$).

A given instance $(V, \mathbf b, \ell)$ of the original problem poly-time reduces to this one by considering all instances of this one of the form $(V, \mathbf B)$ where each $B_i$ is in $\{0,1,\ldots,n\}^d$ and $B_i \le b$.  There are $O(n^{d\ell})$ such instances, which is polynomial since $d$ and $\ell$ are constant.  The original instance will have a solution if and only if at least one of the latter instances does.

The algorithm solves the variant using the following dynamic program.  Fix an instance $(V,\mathbf B)$ of the problem.  Let $V=\{x_1,\ldots,x_n\}$ and $\mathbf B = (B_1,\ldots,B_\ell)$. So $x_i\in\{0,1\}^d$ and $B_j\in \{0,1,\ldots,n\}^d$ for each $i$ and $j$.

Define the signature of the instance $(V, \mathbf B)$ (following the proof of Lemma 1) to be obtained by replacing $V$ by the natural encoding of the function $f_V$ such that, for each $x\in\{0,1\}^d$, $f_V(x)$ is the number of times $x$ occurs in $V$.  Note that any two instances with the same signature are equivalent, in that they have the same answer.

The signature is determined by $2^d + d\ell$ numbers, each in $\{0,1,\ldots,n\}$, so the number of possible signatures (among instances with the given parameters $d,\ell, n$) is $O(n^{2^d+d\ell})$, which (given that $d$ and $\ell$ are constant) is polynomial in $n$.  Furthermore, the number of possible signatures of all "smaller" instances (meaning those where $n$ is smaller than the given $n$) is at most a factor of $n$ larger, so also polynomial in $n$.

Now we can proceed via dynamic programming.  Fix the given instance $(V, \mathbf B)$. For the base case, if $V=\emptyset$ (that is, $n=0$), then the instance is feasible iff each $\mathbf B \equiv \mathbf 0$.  Otherwise $x_n$ can go into one of the parts $V_j$ for $j\in\{1,2,\ldots,\ell\}$, such that removing $x_n$ from that part gives a solution to the problem obtained by subtracting $x_n$ from $\mathbf B_j$ (as long as $x_n\le \mathbf B_j$; if not $x_n$ cannot go in $V_j$).

For each of the (at most) $\ell$ possible ways of placing $x_n$, recursively determine whether the resulting subproblem has a solution.  The original problem will have a solution if and only if one of these subproblems does.

Furthermore, memoize -- keep a cache of the answers to already-solved subproblems, indexed by signature.  When encountering a given subproblem, check whether any subproblem with the same signature has already been answered, and if so use that answer instead of recursing.  Because there are only polynomially many distinct signatures of smaller subproblems, the dynamic-programming algorithm will solve only polynomially many subproblems, so will run in time polynomial in $n$. $~~\Box$.

EDIT: As pointed out in the comments, an easier approach is (similarly to the proof of Lemma 3 below) to formulate an ILP of constant dimension, with a variable $y_{xj}$ for each $x\in\{0,1\}^d$ and $j\in\{1,\ldots,\ell\}$ representing the number of vectors in $V$ that are equal to $x$ and are assigned to part $V_j$.

The proof above raises the question of whether the variant defined in the proof is NP-hard when $\ell$ is not constant.  (It might be, even if the original problem is not.)

Proof of Lemma 3.
The proof is an elaboration of @Gamow's answer in the comments.

Use the following equivalent problem formulation: Given a collection $V=(S_1, S_2, \ldots, S_n)$ of subsets of $\{1,2,\ldots, d\}$, where $d$ is constant, partition $V$ into a minimum number of parts, such that within each part each element $j$ occurs in more than $b_j$ subsets.  Here is the algorithm.

Fix an input $V=(S_1, \ldots, S_n)$ of subsets of $\{1,2,\ldots, d\}$.
Let $\mathcal S_d$ denote the set of non-empty subsets of $\{1,2,\ldots,d\}$.
Let $\mathcal P_d$ denote the set of possible parts, that is, multi-subsets of $\mathcal S_d$ in which each element $j$ occurs at most $b_j$ times.
The goal is to partition the input $V$ into a minimum number of parts, each of which is in $\mathcal P_d$.

Note that $|\mathcal S_d| < 2^d$ and $|\mathcal P_d| \ll (bd)^{bd}$, so (as $b$ and $d$ are constant) there are constantly many possible subsets, and constantly many possible parts.

For each subset $S\in\mathcal S_d$ and possible part $p\in\mathcal P_d$, let $n(S, p)$ (either 0 or 1) denote the number of times that $S$ occurs in $p$.

For each possible subset $S\in\mathcal S_d$, count the number of times that $S$ occurs in the input $V$. Let $n(S, V)$ denote this number.

Finally, construct and solve the following integer linear program (ILP), with an integer-valued variable $x_p$ for each possible part $p\in\mathcal P_d$:

$$\text{minimize} \sum_{p\in\mathcal P_d} x_p \text{ subject to }$$

$$\begin{align}
(\forall S\in \mathcal S_d) && \sum_{p\in\mathcal P_d} n(S, p)\,x_p &{} = n(S, V) \\
(\forall p\in \mathcal P_d) && x_p &{} \in \{0,1,2,\ldots\} \\
\end{align}$$

For $\max_j b_j = O(1)$ and $d=O(1)$, the ILP has constant dimension (and a constant number of constraints) so can be solved in constant time in the real RAM model (by Megiddo's algorithm or subsequent improvements).  The optimal value is the answer for the given instance $V$. $~~\Box$

The real RAM model does not account for bit complexity of arithmetic operations.  But in each feasible solution to this ILP each coordinate has $O(\log n)$ bits, so presumably the ILP can be solved in polylog$(n)$ time in the standard RAM model,
so this approach should also yield a linear-time algorithm in the standard RAM model.


Calculating least fixed points in equations

In general, we look at fixed-points of monotone functions over lattices, i.e. with some partial ordering over your elements.

If your lattice is complete (it has a least and greatest element, called a bottom $(\bot)$ and a top $(\top)$), and the function whose fixed-point you're trying to find is monotone, then the Knaster-Tarski Theorem says that a fixed-point always exists.

However, finding this fixed-point may be undecidable. For example, in Hoare logic, there is a function whose fixed-point is the weakest-precondition of a loop. But there's no guarantee that this fixed-point can be found, since finding weakest loop invariants is undecidable.

The basic algorithm, which might not halt, is as follows:

X := bottom
while (X =/= f(X):
  X = f(X)
return X

However, you can always find a fixed-point using iteration if you have the Ascending Chain Condition, which basically means that there are no infinite increasing chains in your partial order. When you have this, and your function is monotone, the above algorithm will always halt.

If you have some other "upper bound" on a solution size, then you can use it to ensure the above algorithm halts.

In your case, where you have multiple equations, you just make your lattice contain vectors, and find a fixed-point of a multi-dimensional function.


It's not possible.  Consider the following 3x3 boolean matrix:

1 1 0

1 0 1

0 1 1

For every pair of rows {r,r'} , there exists a column c such that {r,r'} X {c} is a combinatorial rectangle.  For any particular pair, we can permute the rows such that {r,r'} are adjacent.  However, since we have a combinatorial rectangle for all pairs of rows, it's not possible to permute the rows so that all such rectangles are geometrically connected simultaneously.


On $\text{ETH}$ with $m$ as parameter: consequences of algorithm running in time $2^{\delta m}$ where $\delta \to 0$ as $k \to \infty$

This is an answer to the updated question (the original question seems harder).
Let $\mu'_k$ be the smallest constant such that $k$-SAT that has clauses of length exactly $k$ and no trivial clauses has a $O(2^{\mu'_k m})$ time algorithm.
Let $\mu_k$ be the smallest constant such that $k$-SAT with any clauses of length at most $k$ has an $O(2^{\mu_k m})$ time algorithm. I will prove that $\mu'_k = \mu_k$.
Proof: Clearly we have $\mu'_k \le \mu_k$. To prove that $\mu_k \le \mu'_k$ suppose we have an algorithm for $k$-SAT with nontrivial clauses of length exactly $k$ with time complexity $O(2^{\mu'_k m})$. To solve general $k$-SAT with $m$ clauses, we add $k$ extra variables to the input formula and $2^k-1$ extra clauses over these new variables to forbid all assignments except the all-false assignment. Now, these $k$ extra variables can be freely added to any clauses of length less than $k$ to make them length exactly $k$. Now we have a restricted instance with $m + 2^k-1$ clauses, and solve it in $O(2^{\mu'_k (m + 2^k-1)})$ time, which for constant $k$ is $O(2^{\mu'_k m})$ time.$\square$
It is easy to see that for $a \le b$ it holds that $\mu_a \le \mu_b$, and it is well-known (e.g. in section 14.1 of the book Parameterized Algorithms) that assuming ETH, $\mu_3 > 0$. Therefore showing that $\mu'_k \rightarrow 0$ as $k \rightarrow \infty$ would break ETH.


Applications of algebraic geometry in type theory/programming language theory

To my knowledge (which is definitely incomplete), there has been relatively little work on this, presumably because it requires assimilating two relatively intricate bodies of knowledge. However, little does not mean nonexistent. Thierry Coquand and his collaborators have written quite a few papers on the connections between commutative algebra and constructive logic.

Thierry Coquand, Henri Lombardi. A logical approach to abstract algebra.

This paper made a huge impression on me as a grad student -- the confident and free way that it used ideas from proof theory and model theory to do nontrivial, proper mathematics is one I greatly admired, and to which I still aspire.
Henri Lombardi and Claude Quitté have a (freely-available) textbook, Commutative algebra: Constructive methods.

As the title suggests, this is commutative algebra rather than
algebraic geometry, but since commutative algebra provides much of
the infrastructure for algebraic geometry this will still be of
interest.

There are also a number of very interesting PhD theses in the area:

Andres Mörtberg's PhD thesis Formalizing Refinements and Constructive Algebra
in Type Theory

Once you have a constructive proof, you've got an an algorithm. This thesis looks at making those algorithms efficient.
Bassel Mannaa's PhD thesis, Sheaf Semantics in Constructive Algebra and Type Theory

In this thesis, he proves the correctness of the Newton-Puiseux theorem constructively, as well as the independence of Markov's principle. It offers a nice example of how sheaf-semantic methods have applications in both geometry and logic.
Ingo Blechschmidt's PhD thesis, Using the internal language of toposes in algebraic geometry,

This thesis looks at redoing many of the usual proofs of algebraic geometry in the internal language of the little  Zariski topos associated with a scheme, yielding a kind of "synthetic algebraic geometry".  (He also does "synthetic scheme theory" using the big Zariski topos). As you would expect, since topoi are not generally Boolean, the proofs have to be done in an intuitionistic style.

It's also worth pointing out the following reference:

Saunders Mac Lane, Ieke Moerdijk. Sheaves in Geometry and Logic Sheaves in Geometry and Logic: A first introduction to topos theory.

A lot of the technology used in this work comes via the connections between topos theory, logic and geometry. This is the standard reference, though I mostly learned it via the papers of Steve Vickers instead.


How Univalence can be used for proofs about algorithm correctness

The univalence axiom is not a magic wand that solves all problems.

Univalence has an immense explanatory power because it makes mathematically precise the intuition that "isomorphic structures can be used interchangably". Mathematicians casually use this intuition to pretend that two isomorphic things are actually equal when they are not. Univalence formally justifies the practice.

In the HoTT book you will find many applications of the univalence axiom which simplify or improve the standard approaches, especially in combination with the higher-inductive types.

The computation of the fundamental group of the circle.
Development of category theory, as you observed.
The definition of cardinals is conceptually clean and well-motivated when we use truncation to define them, see chapter 10.
Some homotopy-theoretic theorems, such as Blakers-Massey and the Freudentahl suspenion theorem.

Please note that in order to measure "simplification" you have to include the background theory as well. For example, the standard treatment of the fundamental group of the circle includes: construction of real numbers, basic general topology, the topology of euclidean spaces, and the theory of covering spaces.

We do not at the moment have direct applications of the Univalence axiom in theoretical computer science because we do not have a good computational interpretation of univalence. There is the constructive cubical sets model which an important step forward, but some time will probably be needed before applications to specific problems in computer science appear.


The number of edges in the ith shortest path in a directed graph

As Igor said- Consider a directed cycle with n vertices $C=(v_1,v_2,\ldots,v_n,v_1)$.

The shortest path between $v_1$ and $v_n$ is the path $(v_1,v_2,\ldots, v_n)$ and goes through $n-1$ edges.
The second  shortest path between $v_1$ and $v_n$ completes a cycle $C$ once, and then uses the path $(v_1,v_2,\ldots, v_n)$. It uses $2n-1$ edges.

The $i^{th}$ shortest path uses $in-1=\theta(in)$ edges


Restricting entries of unitary operators to real numbers and universal gate sets

There is A Simple Proof that Toffoli and Hadamard are Quantum Universal by Dorit Aharonov which first shows how complex amplitudes can be simulated by real amplitudes over a larger Hilbert space with one more qubit.

"This is done by adding one extra qubit
to the circuit, the state of which indicates whether
the system’s state is in the real or imaginary part of
the Hilbert space, and replacing each complex gate
$U$ operating on $k$ qubits by its real version, denoted
$\tilde{U}$, which operates on the same $k$ qubits plus the
extra qubit. $\tilde{U}$ is defined by:

$\tilde{U}|i\rangle |0\rangle = [Re(U)|i\rangle]|0\rangle + [Im(U)|i\rangle]|1\rangle$
$\tilde{U}|i\rangle |1\rangle = -[Im(U)|i\rangle]|0\rangle + [Re(U)|i\rangle]|1\rangle$"

Secondly, she proofs the universality of the {Hadamard,Toffoli} gate set, which has only real amplitudes $\{0,1,\pm\frac{1}{\sqrt{2}}\}$.


Finding the point that maximizes a linear function

Another Answer:

Find the 2D maximal point set. Let us call it the set $M$.
Find the convex hull of $M$. Let us call it $co(M)$.

The preprocessing time for the two step is $O(n \log n)$.
Now, for the line: $c_i \cdot x + y = 0$, you need to find the point in $M$ that is farthest from the line. That point must lie on the boundary of $co(M)$. Note that distances of the points on the convex hull first increase and then decrease. You need to find that point on the boundary where this transition happens. It can be done in $O(\log n)$ time using binary search.


Suppose $\mathbf{P} = \mathbf{BQP}$. Then what is randomness? Would it even exist at all?

P and BQP are decision-problem classes, i.e. the correct output is always a deterministic functions of the inputs. The only question is whether randomness helps "along the way" to speed up computing this deterministic function (at the cost of sometimes being wrong), or does not. This is the key point: P=BQP says nothing about outputting random strings in general situations, but only for the situation of computing a deterministic function in polynomial time.

So for instance the statement

  if P=BQP, then there exists a classical deterministic algorithm which is able to quickly output true randomness (by just quickly simulating some Quantum Turing Machine).

is false. P=BQP only implies that if a machine with randomness can usually output the correct bit, then there is a machine with no randomness that always ouptuts the correct bit.

More comments on your question:

What is closer to true is that some form of pseudorandom generators exist (deterministic machines whose output "looks random" to other deterministic machines of bounded running time). However, again, these PRGs would be targeted to machines that always output just a single bit, not all tasks that use randomness in general.
For an example single-machine problem that can be solved by a randomized machine and provably cannot be solved by a deterministic machine, consider the problem "output a string of Kolmogorov complexity $\geq n$". This is essentially the problem of outputting a random string, and of course we can prove that no deterministic machine can do this.
As Kaveh points out, in areas like communication complexity between multiple machines, also distributed systems and probably others, we have provable differences between what can be achieved with and without randomness. The classic example is for two machines to decide if they hold the same $n$-bit string while communicating fewer than $n$ bits.
It may be that even if BQP = P, the randomized algorithm is much faster and more useful in practice. (It may even be that someday complexity theory could prove this.) Example: Miller-Rabin primality test (randomized) vs AKS (deterministic).
As I understand it, we could have P = BQP and yet cryptography is perfectly useful, one-way functions exist, etc. (Not the factoring problem, of course.) And cryptography relies completely on randomness.
I think BPP is as much a model of "true" randomness as BQP. Just a different type of randomness. How to get "truly" random bits in the real world is a different story.


Estimating the rank of a large sparse matrix

There is a very neat randomized algorithm by Cheung, Kwok, and Lau, which computes the rank of an $n\times m$ matrix $A$, $n\le m$, in time $O(\mathrm{nnz}(A) + \min\{n^\omega, n\cdot\mathrm{nnz}(A)\})$. Here $\mathrm{nnz}(A)$ is the number of nonzero elements of $A$, and $\omega$ is the matrix multiplication exponent. Not quite what you are asking for, but it does improve on fast matrix multiplication based methods for $\mathrm{nnz}(A) = o(n^{\omega - 1})$.


I realize that this is a very late reply, but the answer is yes. You can get an approximation factor of $2^{C n \log \log n/\log n}$ for any constant $C$ in polynomial time. In fact, you can do this with Babai's algorithm together with better preprocessing than LLL.

Unfortunately, I don't know of a great write up for this specific fact.

The main point is simply that the LLL algorithm is not our best polynomial-time algorithm for basis reduction. Instead, our best algorithms are generalizations of this, known as block reduction, or sometimes BKZ reduction (for Block Korkine-Zolotareff, though the name is not very helpful). The idea, originally due to Schnorr [1], is to look at various (projections of) $k$-dimensional sublattices and to find short bases for these (projections of) sublattices. LLL is just the case $k = 2$. I.e., LLL performs a bunch of simple operations on $2 \times 2$ matrices. See, e.g., [2] for a more recent version of this approach.

In polynomial time, we can take $k = C \cdot \log n$ for any constant $C > 0$ (because we can solve more-or-less any lattice problem in exponential time), and the approximation factor that falls out is $2^{C' n \log \log n/\log n}$ for more-or-less any lattice problem that might interest you. As I said, I don't know of a specific write up about this for BDD, but the fact that we can get a $2^{C' n \log \log n/\log n}$-approximation to SVP via this approach was first proven by Ajtai, Kumar, and Sivakumar [3], as a consequence of their famous sieving algorithm. (See Corollary 11 in their paper.) You can then just use a generic reduction from BDD to SVP to get the same result for SVP (see, e.g., [4]).

You can also get this via BKZ reduction together with Babai's algorithm by observing that the approximation factor of Babai's algorithm is controlled by a certain quality measure on the basis---the decay of the Gram-Schmidt vectors---that we can bound for BKZ bases. The best write up that I know of about this property of Babai's algorithm is in my own lecture notes [5].

[1] Schnorr, C. P., A hierarchy of polynomial time lattice basis reduction algorithms, Theor. Comput. Sci. 53, 201-224 (1987). ZBL0642.10030..

[2] Gama, Nicolas; Nguyen, Phong Q., Finding short lattice vectors within Mordell’s inequality, STOC’08. Proceedings of the 40th annual ACM symposium on theory of computing 2008, Victoria, Canada, May 17--20, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-047-0). 207-216 (2008). ZBL1230.11153.

[3] Ajtai, Miklós; Kumar, Ravi; Sivakumar, D., A sieve algorithm for the shortest lattice vector problem, Proceedings of the thirty-third annual ACM symposium on theory of computing, STOC 2001. Hersonissos, Crete, Greece, July 6--8, 2001. New York, NY: ACM Press (ISBN 1-581-13349-9). 601-610 (2001). ZBL1323.68561.

[4] Lyubashevsky, Vadim; Micciancio, Daniele, On bounded distance decoding, unique shortest vectors, and the minimum distance problem, Halevi, Shai (ed.), Advances in cryptology -- CRYPTO 2009. 29th annual international cryptology conference, Santa Barbara, CA, USA, August 16--20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03355-1/pbk). Lecture Notes in Computer Science 5677, 577-594 (2009). ZBL1252.94084.

[5] http://www.noahsd.com/mini_lattices/05__babai.pdf .


Are randomly generated infinite patterns computable?

In the particular way you formulated the question the probability is 0. Because there are only countably many computable sequences, it suffices to show that for each computable sequence the probability is 0. So let's lets consider the sequence 000... (our reasoning works for any computable sequence).

Suppose at some time step $s = 0^n$ for some $n$. Now, we search for a program that outputs a string starting with $0^n$ and halts. For each program outputting $0^m$ with $m>n$, there exists a program that is only $O(1)$ bits longer and also appends $1$ to this output (i.e. it outputs $0^m1$). Hence, there is a probability that $s$ is extended with "wrong" bits, and this probability does not depend on the length of $s$. Therefore, generating infinitely many zeros has 0 probability.


Two such puzzles that I know about are:

Unruly. This website has an online library of puzzles and solutions and a generator for puzzles of arbitrary size.
Masyu. This website has a library of puzzles and solutions. It also links to several variants of the puzzle.

Actually, the page where the Unruly puzzle is found lists more such puzzles, some of which satisfy your conditions, while others don't.


TCS oriented refs/survey on group theoretic word problem

One family of results not mentioned in the excellent references of @Marzio's answer is relations between the isoperimetric (Dehn) function of a group $G$ and the nondeterministic time complexity of the word problem in $G$. For example:

For finitely generated groups $G$, $WP(G) \in \mathsf{NP}$ if and only if $G$ can be embedded in a finitely presented group that has polynomial Dehn function. (In fact, if $WP(G)$ can be solved in $\mathsf{NTIME}(T(n))$, then $G$ can be embedded in a group with isoperimetric function $\leq n^2 T(n^2)^4$.) (Birget-Ol'shanskii-Rips-Sapir)
There are individual groups whose word problem is $\mathsf{NP}$-complete (corollary to the preceding), and similarly groups whose word problem is $\mathsf{coNP}$-complete (Birget, also available on the arXiv).
The collection of functions $\mathcal{D}_4$ that are Dehn functions $\geq n^4$ of finitely presented groups are closely related to the collection $\mathcal{T}_4$ of time functions $\geq n^4$ of nondeterministic Turing machines. Specifically, $\mathcal{T}^4 \subseteq \mathcal{D}_4 \subseteq \mathcal{T}_4$, where $\mathcal{T}^4$ is the set of super-additive functions that are fourth powers of time functions of nondeterministic TMs. (Sapir-Birget-Rips)

See this survey by Sapir for more.


Constrained Topological Sorting with bounded number of chains

The additional constraint amounts to saying that the input DAG has width $\leq k$, i.e., there is no antichain of size $k+1$. In this case, if $k$ is a constant, the decision version of the constrained topological sorting problem is in NL by Prop C.2 of https://arxiv.org/abs/1707.04310, which amounts to a PTIME dynamic programming algorithm. Reconstructing a matching topological sort as part of the dynamic programming algorithm will also be in PTIME


Is there a quantum NC algorithm for computing GCD?

First of all, there is a formal definition of "quantum-NC", see QNC on the zoo.

GCD is indeed a good candidate for a problem that could be shown to be in QNC, but it's not known to be in NC. However, finding a QNC algorithm for GCD is still an open problem.

The feeling for which this is believed to be true comes from the fact that the Quantum Fourier Transform can be done in QNC.

Reference: Conclusion section of "R. Cleve and J. Watrous, Fast parallel circuits for the quantum Fourier transform", arXiv:quant-ph/0006004


Time complexity for a variant of edit distance

Computing this type of edit distance is NP-complete, which I will prove below by reducing from the NP-complete problem Vertex Cover (given a graph $G$ and a number $k$, determine whether there exists a set of vertices $C$ with $|C|\le k$ such that each edge in $G$ has at least one vertex in $C$, aka a vertex cover of size at most $k$).
Helpful subproblem
Consider any sequence of edits between two strings (insertions/deletions/substitutions). This sequence of edits can be re-ordered so that the new sequence of edits has the same cost, but the substitutions happen after the insertions and deletions. We can separate the cost of the edits into two parts: an insertion/deletion cost and a substitution cost.
If you have already made a choice of what insertions/deletions to do starting at the source string, the insertion/deletion cost is already fixed, but there might be multiple different substitution strategies to get from that intermediate state to the target string. So one reasonable question is to ask what the optimal substitution strategy is at that point, and therefore what the optimal substitution cost is. Equivalently, this is asking for the edit distance using your distance metric but with only substitutions allowed.
So let's say we want to get from string $A = a_1a_2\ldots a_n$ to string $B = b_1b_2\ldots b_n$. Construct the directed graph $T_{A\to B}$, whose vertices are the characters used in these strings, and whose edges are the pairs $(u, v)$ such that $a_i = u \ne v = b_i$ for some $i$. In other words, $T_{A\to B}$ is the graph of the desired substitutions.
Then we have the following key fact: The optimal substitution cost is equal to the number of vertices in $T_{A\to B}$ minus the number of acyclic weakly connected components of that graph. This fact will be used in the analysis of the reduction. The rest of this section will prove it. If you are just interested in the NP-hardness proof, feel free to skip to the next section.
We want to know what substitutions to do, but each substitution has cost 1 no matter how many times we do it. In other words, we can look at every pair of characters $(u,v)$, and ask the question of whether we want to do the substitution of $u \to v$ at least once or not. This choice of which substitutions to do can be expressed as a directed graph, where we include edge $(u,v)$ if we plan to do the substitution of $u \to v$ at least once. Thus, the problem can be thought of as an optimization problem where we are looking for an optimal graph. What are we optimizing and what are our constraints? Well we are trying to minimize the substitution cost, so we are trying to choose a graph with a minimum possible number of edges. As for the constraints, each edge $(u,v)$ of $T_{A\to B}$ is a constraint saying that character $u$ must be converted into $v$ via a sequence of substitutions. In other words, the presence of edge $(u,v)$ in $T_{A\to B}$ means that we have the constraint that there must be a path from $u$ to $v$ in our graph.
Consider any weakly connected component of a candidate graph for this graph optimization problem. If the component is acyclic, then there must be at least $n-1$ edges where $n$ is the number of vertices in that component. On the other hand, if the component is cyclic, there must be at least $n$ edges. Therefore, the overall number of edges in a candidate graph has as a lower bound the number of vertices (which is fixed) minus the number of acyclic weakly connected components (which can vary among candidate graphs). If we could get an upper bound on the number of acyclic weakly connected components, we would have an overall lower bound on the number of edges (aka the substitution cost).
Now consider a weakly connected component of $T_{A\to B}$. If two vertices are in the same weakly connected component of $T_{A\to B}$, then they must also be in the same connected component of any candidate graph in our graph optimization problem (because edges in $T_{A\to B}$ correspond to paths in the candidate graph, thereby retaining connectivity). Therefore, each weakly connected component of our candidate graph must be a union of weakly connected components of $T_{A\to B}$. Thus, we see that the number of acyclic weakly connected components in $T_{A\to B}$ is an upper bound on the number of acyclic weakly connected components in our candidate graphs, which is exactly what we wanted. We have our lower bound on the substitution cost: it is at least the number of vertices in $T_{A\to B}$ minus the number of acyclic weakly connected components.
This is exactly the value that the key fact says is the optimal substitution cost, so all that's left is to demonstrate that this value can be achieved. We will do this as follows. Consider every acyclic weakly connected component of $T_{A\to B}$, one at a time. That component is a DAG, so we can find a topological sort. Then, we can include that topological sort as a path in our graph of substitutions (i.e. earliest element in the sort points to second earliest, etc...). This uses one fewer edge than the number of vertices in that component. It also satisfies the constraints for that component: if $u$ needs to be converted into $v$, then $(u,v)$ is an edge in the component; as a result $u$ must be before $v$ in the topological sort, and so the path of substitutions has as a subpath a path from $u$ to $v$. After doing this for all the acyclic weakly connected components, take all the other vertices, and arrange them in a cycle. This uses a number of edges equal to the number of vertices and satisfies the requirement since any of these vertices has a path to any other (by following the cycle). This graph satisfies all the requirements and has a total number of edges equal to the number of vertices minus the number of acyclic weakly connected components.
This concludes the proof of the key fact.
NP-hardness reduction
We wish to prove that computing the edit distance is NP-hard by reducing from Vertex Cover. That means our reduction starts with a given Vertex Cover instance: a graph $G$ and a number $k$. The reduction will output a pair of strings $(A, B)$ and a number $k'$ using polynomial time to compute these outputs. We will prove that the edit distance between $A$ and $B$ is at most $k'$ if and only if $G$ has a vertex cover of size at most $k$.
In particular, $k'$ will be $k + 4m$ where $m$ is the number of edges in $G$.
As for the strings $A$ and $B$, we will construct them out of several pieces $A = A_1A_2\ldots A_t, B = B_1B_2\ldots B_t$, where each pair $(A_i, B_i)$ is a gadget built for a specific purpose. The rest of this section will go over what kinds of gadgets we will use, how these gadgets will be combined together (i.e. how many of which gadget we will use and what characters will be used for the gadgets), and then a correctness proof showing that this reduction is correct (i.e. the edit distance between $A$ and $B$ is at most $k'$ if and only if $G$ has a vertex cover of size at most $k$).
Gadgets
The first kind of gadget we will use is an alignment gadget. This gadget consists of pair $(A_i, B_i)$ where $A_i$ consists of a large number of different characters that are not used anywhere else in $A$ or $B$ and $B_i = A_i$. The purpose of this gadget is to force alignment of these two sections of strings $A$ and $B$ via insertions/deletions. If these two sections don't align, then in the substitution step, there would need to be a number of different substitutions roughly equal to the number of characters in $A_i$. By making the number of characters large (much larger than $k'$), we can make it prohibitively expensive, in terms of substitution cost, to not align these sections of $A$ and $B$ during the insertion/deletion stage of the edits.
We will use alignment gadgets as separators between the other gadgets, which allows us to reason about each other gadget $(A_i, B_i)$ in isolation. That is, we will be forced, due to separator gadgets $(A_{i-1},B_{i-1})$ and $(A_{i+1},B_{i+1})$, to edit $A_i$ directly into $B_i$ (rather than possibly converting $A_i$ into some other part of string $B$ and converting some other part of $A$ into $B_i$).
The second gadget is a forced substitution gadget. This gadget simply consists of $(A_i, B_i)$ where $A_i$ and $B_i$ have the same (very large) length, $A_i$ consists entirely of copies of one character $u$ and $B_i$ consists of entirely copies of another character $v$. The duplication of these characters many times makes it so that even after using an insertion/deletion cost of up to $k'$, there is still at least one character $u$ that must be converted into a $v$. Since that conversion needs to happen anyway, the simplest way to solve this gadget is to just use a substitution cost of 1 to convert all the copies of $u$ into copies of $v$. However, it is possible to use some other substitution strategy to convert these characters (i.e. by converting to some third character before converting to $u$). All we really need to know here is that the insertion/deletion cost within this gadget can be as low as 0 and that the desired substitution $u \to v$ is forced, either directly or indirectly, by this gadget.
The final gadget is a choice gadget. Here $A_i = x_1ax_2$ and $B_i = bc$, where $x_1$ and $x_2$ are characters unique to this gadget (not used anywhere else), while $a$, $b$, and $c$ are characters potentially used elsewhere. Assuming this gadget is placed between two alignment gadgets, we need to convert $A_i$ into $B_i$. If this is done with an insertion/deletion cost of $1$, then we are left trying to convert either $x_1a$, $x_1x_2$, or $ax_2$ into $bc$. This can be accomplished with two substitutions, though the substitution cost can be anywhere between $0$ and $2$ depending on whether these substitutions can also be used elsewhere. Therefore, if using an insertion/deletion cost of $1$, the total cost in this gadget is at most $3$. On the other hand, the next smallest possible insertion/deletion cost in this gadget is $3$, which is already at least the cost of the three solutions listed above. Therefore, there is always an efficient solution of this gadget with only one deletion followed by substitutions. If we chose to delete $a$ and substitute $x_1x_2$ into $bc$, then both substitutions have cost $1$ since neither $x_1$ nor $x_2$ appear elsewhere in the strings; therefore, if we were to instead choose one of the other two possible deletions, the cost would be no worse. That is why this is a choice gadget: the remaining two choices involve either substituting $a$ into $b$ (when $ax_2 \to bc$) or into $c$ (when $x_1a \to bc$).
Arrangement of gadgets
As previously mentioned, we will use alignment gadgets as separators for all the other gadgets. In other words, every second gadget will be an alignment gadget. This leaves the question of which other gadgets should be used.
Consider every edge $e$ in $G$. We will use two characters $p_e$ and $q_e$ for this edge. For each such edge $e$, we will include two forced substitution gadgets forcing the substitution of $p_e$ into $q_e$ and the substitution of $q_e$ into $p_e$.
Next consider the vertices of $G$. If $v$ is a vertex, we will use $r_v$ as a character. For every edge $e = (u, v)$, we will create a choice gadget in which character $p_e$ must be substituted into either $r_u$ or $r_v$ (i.e. the choice gadget where $A_i = x_1p_ex_2$ and $B_i = r_ur_v$).
That concludes the actual construction of the reduction. Notably, these strings $A$ and $B$ and the value $k$ can easily be constructed from the vertex cover instance in polynomial time. What's left is to prove the correctness.
Correctness
Suppose first that we have a vertex cover $C$ of $G$ with $|C| \le k$. Then we will prove that the edit distance between $A$ and $B$ will be less than $k' = k + 4m$.
$A$ can be edited into $B$ as follows:

First, in the insertion/deletion step, delete one character from each choice gadget, for an insertion/deletion cost of $m$. In particular, for each edge $e = (u,v)$, we have the gadget $(A_i, B_i) = (x_1p_ex_2, r_ur_v)$ and we will delete either $x_1$ or $x_2$ as follows. Either $u$ or $v$ is in the vertex cover $C$. We will delete $x_1$ (thus requiring the substitution $p_e \to r_u$) if $u \in C$, and will delete $x_2$ (thus requiring the substitution $p_e \to r_v$) otherwise (in which case $v \in C$).
In the substitution step, we will do two things. First, we will look at each choice gadget, and we will convert either $x_1$ or $x_2$, whichever is still there, into the character it needs to turn into. This has a substitution cost of $m$. Second, we will take the characters $p_e$ and $q_e$ for every edge $e$ in $G$ and the characters $r_v$ for every vertex $v$ in $C$, and we will arrange these characters in a cycle, substituting each character for the next in the cycle. This has a substitution cost of $2m + |C|$, and allows any of these characters to turn into any other (by simply substituting along the cycle repeatedly).

This converts $A$ into $B$ with a total cost of $m+m+2m+|C| = 4m + |C| \le 4m + k = k'$. To confirm that this actually converts $A$ into $B$, lets consider every gadget. The alignment gadgets are successfully converted as long as the other gadgets are. The forced substitution gadgets are successfully converted since both $p_e$ and $q_e$ are in the cycle of substitutions. As for the choice gadgets, the necessary substitutions are either $x_1p_e \to r_ur_v$ (in a case where $v \in C$) or $p_ex_2 \to r_ur_v$ (when $u \in C$). The substitutions of $x_1$ or $x_2$ are explicitly handled. Therefore, we're left needing to substitute either $p_e \to r_v$ (when $v \in C$) or $p_e \to r_u$ (when $u \in C$). Note that in both cases, the character that $p_e$ needs to be converted into is in the cycle of substitutions, meaning that the above instructions successfully convert the choice gadgets as well.
This shows that if the answer to the vertex cover instance is "yes", then the edit distance between $A$ and $B$ is at most $k'$.
What about the reverse direction?
Let's say there is a way to edit $A$ into $B$ using at most cost $k'$. Suppose we have the solution with the least cost. When we analyzed the choice gadget, we saw that there is always an efficient (least cost) solution involving one deletion in that choice gadget, specifically deleting either $x_1$ or $x_2$ in the gadget. Thus we can assume WLOG that our least-cost solution has no insertions and exactly one deletion in each choice gadget and that the deletion is one of the two intended deletions. That's an insertion/deletion cost of $m$ in the choice gadgets alone. Therefore, the substitution cost must be at most $k' - m = 3m + k$.
Due to the alignment gadgets we know that the choice gadgets must be solved entirely by substitution after the one deletion in that gadget. Therefore, for each edge $e = (u,v)$, we either have a substitution of $x_1p_e \to r_ur_v$ or $p_ex_2 \to r_ur_v$. Define a set of vertices $C$ such that $v \in C$ if and only if there is a substitution $p_e \to r_v$ that needs to happen in some edge gadget. By the above, we see that $C$ must be a vertex cover (since each edge gadget contributes one of the endpoints of the edge to $C$).
We also know from the forced substitution gadgets that $p_e \to q_e$ and $q_e \to p_e$ are forced substitutions.
Let $A'$ be the state of the string after the insertion/deletion step and before the substitution step. At this point we will use the key fact from the first section to determine what the substitution cost must be. We know that there is a directed graph $T_{A'\to B}$ whose edges are the substitutions that are required to convert $A'$ into $B$. We know from the above that this graph includes the following edges:

$(p_e, q_e)$ and $(q_e, p_e)$ for every edge $e$ in $G$
Either $(x_1, r_u)$ and $(p_e, r_v)$, or $(x_2, r_v)$ and $(p_e, r_u)$ for each edge $e = (u,v)$ (where the $x_1$ and $x_2$ vertices are unique per edge $e$)

According to the key fact from the previous section, the substitution cost is equal to the number of vertices in this graph minus the number of acyclic weakly connected components. This value can never decrease if we add more vertices or edges, so computing this value for only those edges listed above is a lower bound on the substitution cost of our edit solution.
There are exactly $3m+n$ vertices listed above, where $n$ is the number of vertices in $G$ (one $p_e$ vertex per edge of $G$, one $q_e$ vertex per edge of $G$, one $x_1$ or $x_2$ per choice gadget--of which there are $m$, and one $r_v$ per vertex of $G$). What about the number of acyclic weakly connected components? Due to the cycle $p_e, q_e, p_e$, the connected components of vertices $p_e$ are never acyclic. As for each $r_v$, it either connects to some $p_e$, in the case that $v \in C$, or it does not connect to any $p_e$ if $v \not\in C$. In the former case, this vertex is not in an acyclic weakly connected component. In the latter case, the entire weakly connected component of $r_v$ is that vertex with some number of $x_1$ or $x_2$ vertices neighboring it. That is acyclic. As for the $x_1$ or $x_2$ vertices, each one neighbors an $r_v$ vertex, and its weakly connected component has therefore already been addressed one way or the other above. Thus, we see that each acyclic weakly connected component contains exactly one $r_v$ vertex and furthermore one where $v \not\in C$. Thus, the number acyclic weakly connected components is equal to the number of vertices $v$ not in $C$. This equals $n - |C|$.
The substitution cost therefore has a lower bound of $(3m+n) - (n-|C|) = 3m+|C|$. But we saw before that the substitution cost must be at most $k' - m = 3m + k$. Therefore, we see that it must be the case that $|C| \le k$. Then $C$ is a vertex cover of size at most $k$, proving that the answer to the vertex cover instance is "yes".
We have shown via the two directions that $G$ has a vertex cover of size at most $k$ if and only if $A$ and $B$ have an edit distance of at most $k'$. This proves that the reduction is correct. Since we previously noted that it runs in polynomial time, this concludes the proof that computing edit distance (as you defined it) is NP-hard.


Estimator for sum of independent and identically distributed (iid) variables

You need McDiarmid's inequality, or in particular the Hoeffding inequality, which is a simplification:

Given $n$ independent $X_i$ with the property that $X_i \in [a_i, b_i]$, and $X = (1/n)\sum X_i$, then

$$ \text{Pr}(|X - EX| \ge t) \le 2 \exp(\frac{2t^2n^2}{\sum (b_i - a_i)^2}) $$


List of (unsolved) complexity problems arising from PL

Pippenger's (1) from 1996 shows that (under some assumptions)  strict (CBV) functional programming languages are asympotically slower than imperative languages.  It is open whether Pippenger's result can be generalised to lazy functional languages, as was pointed out in (2).

Pippenger imposes two simplifying assumptions (on-line computation, and a certain atomicity of input). It is open whether
they can be removed.  Pippenger conjectures that it can be done, but warns: "[s]uch a result [...] seems far beyond the reach of currently available methods in computational complexity theory".

See also Campbell's answer in (3), and  Ben-Amram's notes (4).

 1. N. Pippenger, Pure Versus Impure Lisp.

 2. R. Bird, G. Jones, O. De Moor, More haste, less speed: lazy versus
    eager evaluation.

 3. Stack Overflow, Efficiency of purely functional programming.

 4. A. M. Ben-Amram, Notes on Pippenger's Comparison of Pure and Impure LISP.


Generating a Diffie Hellman tuple without "being able to know" one of the discrete logs involved

It looks as though the case with a fixed $g$ has shown up under the name "knowledge of exponent assumption(s)"--Googling this phrase will turn up a few papers which discuss/use it. In particular I notice "Statistically Hiding Sets" by Prabhakaran and Xue claims to show the assumption holds in the generic group model. There may be more recent information out there, but that should serve as a starting point at least. Long story short, as far as I can tell: It's a nonstandard assumption, but it's not obviously false and some people have built things with it.


Relation between edit distances over different alphabets

Obviously, $L(2^b) \leq L(2)$.

The Levenshtein distance is at most the length of the longest string, so $L(2^b) \leq \max(cn,cm) / b$ whereas $L(2) \leq \max(cn,cm)$.

You cannot avoid $L(2^b)(S_1,S_2) = L(2)(S_1,S_2)$ when $L(2)(S_1,S_2) \leq \max(cn,cm) / b$:
consider for instance $b = c = 2$, $S_1 = 0^{2n}$ and $S_2 = (01)^{p} (00)^{n-p}$.

When $L(2)(S_1,S_2) > \max(cn,cm) / b$, you cannot avoid $L(2^b)(S_1,S_2) = \max(cn,cm) / b$.
Consider for instance $b = c = 2$, $S_1 = 0^{2n}$ and $S_2 = 1^{2n}$.


Is there a logic without induction that captures much of P?

You want to have a look at what some people call Grädel's Theorem. You can find it in Papadimitriou's book "Computational Complexity" (it's Theorem 8.4 in page 176) or in Grädel's original paper.

In a nutshell, Grädel's Theorem is to P what Fagin's Theorem is to NP. It states that on the class of finite structures with a successor relation, the collection of polynomial-time decidable properties coincides with those expressible in the Horn-fragment of existential second-order logic. These are the sentences of second-order logic of the form
$$
(\exists R)(\forall x)(\phi)
$$
where $R$ is a sequence of second-order relation variables, $x$ is a sequence of first-order variables, and $\phi$ is a quantifier-free formula that, when written in CNF form, is a conjunction of $R$-Horn clauses (i.e. clauses that have at most one non-negated atom involving the variables in $R$).


Graph classes in which CLIQUE is known to be NP-hard?

It's NP-complete to find maximum cliques in claw-free graphs [Faudree, Ralph; Flandrin, Evelyne; Ryjáček, Zdeněk (1997), "Claw-free graphs — A survey", Discrete Mathematics 164 (1–3): 87–147] and in string graphs [Jan Kratochvíl and Jaroslav Nešetřil, INDEPENDENT SET and CLIQUE problems in intersection-defined classes of graphs, Commentationes Mathematicae Universitatis Carolinae, Vol. 31 (1990), No. 1, 85–93]. At least as of the 1990 paper it was open whether the problem remained hard for intersection graphs of straight line segments.

However, finding maximum cliques easy for planar graphs, for minor-closed graph families, or more generally for any family of graphs with bounded degeneracy: find the minimum degree vertex, search for the largest clique among its O(1) neighbors, remove the vertex, and repeat. It's also easy for perfect graphs and the many important subfamilies of perfect graphs.

Although maximum independent set is hard for many other interesting graph classes, that doesn't generally lead to interesting hardness results for clique, because the complement of an interesting graph class is not necessarily itself interesting.


A paper of Klawe, Paul, Pippenger, and Yannakakis gives an hierarchy theorem for constant depth monotone formulas:
http://dl.acm.org/citation.cfm?id=808717

Specifically, for every $k$ it gives a function that can be computed by a formula of depth $k$ and size $n$ but requires formulas of depth $k-1$ of size $\exp(n^{1/k})$.


Defining primitive recursive functions over general data types

In general, in a language with datatypes (like lists, trees, etc) it's easy to describe a language of functions which behave exactly like we expect primitive recursion to behave.

For example if the datatype is $D$, and the constructors $c_1,\ldots, c_n$ have type

$$ c_i : T_1^i\rightarrow T_2^i\rightarrow \ldots\rightarrow T_{k_1}^i\rightarrow D\rightarrow\ldots\rightarrow D$$

then the recursor $\mathrm{rec}_D^O$ for output type $O$ will have type

$$\mathrm{rec}^O_D:(T_1^1\rightarrow\ldots T^1_{k_1}\rightarrow D\rightarrow \ldots\rightarrow D\rightarrow O\rightarrow \ldots\rightarrow O)\rightarrow\ldots\rightarrow D\rightarrow O$$

and the operational semantics will be:

$$\mathrm{rec}^O_D\ f_1\ \ldots\ f_n\ (c_i\ t_1\ldots t_{k_i}\ d_1\ldots d_m)\rightarrow\\ f_i\ t_1\ldots t_{k_i}\ (\mathrm{rec}^O_D\ f_1\ldots\ f_n\ d_1)\ldots (\mathrm{rec}^O_D\ f_1\ldots f_n\ d_m) $$

for each $i$.

Something of a mouth-full! At least for natural numbers, we indeed get
$$\mathrm{rec}_{\mathbb{N}}^O:(\mathbb{N}\rightarrow O\rightarrow O)\rightarrow O\rightarrow\mathbb{N}\rightarrow O $$

$$\mathrm{rec}^O_{\mathbb{N}}\ f_0\ f_1\ 0 \rightarrow f_1\ 0$$
and
$$\mathrm{rec}^O_{\mathbb{N}}\ f_0\ f_1\ (S\ n)\rightarrow f_0\ n\ (\mathrm{rec}^O_{\mathbb{N}}\ f_0\ f_1\ n)$$

as hoped for (note that the zero constructor has zero arguments!).

If now we allow for constant functions and projections, and allow arbitrary uses of $\mathrm{rec}^O_D$ for non-function types $O$, then you have exactly primitive recursion.

Reassuringly, if all the $T^j_i$s are non-functional as well, then the usual Gödel encoding of the datatype gives the same primitive recursive functions.

It would be nice to have a more elegant description of this process though. That's were Carlos' answer comes in: these datatypes can be described more elegantly in category theory as the initial algebras of certain functors, often called polynomial functors. The recursor is then just (a variant of) the initial morphism of this algebra, sometimes called a catamorphism by people trying to confuse things. This morphism exists by construction of the initial algebra.

A paramorphism is just the particular variant I described above.


Program inversion algorithms for higher-order programs

There hasn't been a huge amount of work in this space, but what work there is, is pretty interesting.

Torben Mogensen has worked on this problem. Here are two papers of his.

The first paper gives an algorithm for first-order functional programs, and the second extends it to higher-order. The precise characterization of when this algorithm will succeed is left to future work.

Semi-inversion of Guarded Equations
Semi-Inversion of Functional Parameters

Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück.

This describes the RFun programming language, which inverts first-order functional programs, but enforces injectivity and backwards determinism constraints which ensure that backwards evaluation is as fast as forwards. (They have written a number of other papers on this subject, which I have had trouble getting hold of.)

Towards a Reversible Functional Language.

Stefan Bohne and Baltasar Trancón Widemann.

This is a really neat paper! It observes that (a) you can construct a category where the morphisms are functions paired with their inverse (for whatever particular notion of inverse you are using), and (b) this category has dagger compact structure. This means you can write a program with a slightly funky linear type discipline, and then read off the forwards and backwards interpretations from the semantics.

They give a functional language with a fairly wild syntax: nigh-arbitrary expressions can be used as patterns, and reversibility makes it sensible.

An Approach for Generalized Reversible Functional Programming

Francesco Tiezzia, Nobuko Yoshida

I haven't read this one, but only just discovered it when Googling for the other papers. Given the authors and the subject, I suspect this is right up your alley!

Reversible session-based pi-calculus


Embedding planar graphs (with max degree four) in an adjacency-preserving way onto a grid is NP-complete, meaning that there's unlikely to be simple necessary and sufficient conditions. Actually that's still true even for embedding trees into a grid. See:

S. Bhatt and S. Cosmodakis. The complexity of minimizing wire lengths in VLSI layouts.
Inform. Proc. Lett. 25:263–267, 1987.


Parallel algorithms to color interval graphs

I'm not really familiar with the topic, but with some searching there are some results.

For example, Efficient parallel algorithms on interval graphs by Das and Chen, and A simple optimal parallel algorithm for the minimum coloring problem on interval graphs by Yu and Yang both gave an algorithm with $O(\log n)$ time and $O(n)$ processors on the EREW PRAM model. Even for the chordal graphs (which is a superclass of the interval graphs) there is an algorithm with $O(\log^2 n)$ time and $O(n)$ processors on the CRCW PRAM model, in the paper Efficient parallel algorithms for chordal graphs by Klein. Maybe you can take a look at the papers and references, to make sure if there are any additional assumptions, like whether the interval representations are given or not.


What is the deterministic complexity of counting the number of global minimum cuts on an unweighted undirected graph?

If you want exact minimum cuts then one can construct a cactus representation of the minimum cuts deterministically in polynomial time and use that to enumerate all minimum cuts. See below for a reference. https://www.sciencedirect.com/science/article/pii/S0196677499910398

More interesting and difficult case is $\alpha$-approximation mincuts for $\alpha > 1$. One can use Karger's randomized algorithm for this purpose. Simply run it sufficiently many time. However, if you want a deterministic algorithm, one can do it via tree packings. See Thorup's paper on k-cuts. https://dl.acm.org/citation.cfm?id=365415


Why does randomness have stronger effect on reductions than on algorithms?

First, let me comment on the specific case of the Valiant-Vazirani reduction; this will, I hope, help clarify the general situation.

The Valiant-Vazirani reduction can be viewed/defined in several ways.  This reduction is "trying" to map a satisfiable Boolean formula $F$ to a uniquely-satisfiable $F'$, and an unsatisfiable $F$ to an unsatisfiable $F'$.  All output formulas are always obtained by further restricting $F$, so unsatisfiability is always preserved.  The reduction can be defined either as outputting a single $F'$, or as outputting a list of $F'_1, \ldots, F'_t$. In the latter case, "success" in the case $F \in SAT$ is defined as having at least one uniquely satisfiable $F'_i$ in the list.  Call these two variants the "singleton reduction" and "list-reduction" respectively (this is not standard terminology).

The first point it's important to note is that the success probability in the singleton reduction is quite small, namely $\Theta(1/n)$ where $n$ is the number of variables.  The difficulties in improving this success probability are explored in the paper

"Is Valiant-Vazirani's Isolation Probability Improvable?"  by Dell et al.

http://eccc.hpi-web.de/report/2011/151/#revision1

In the list-reduction, the success probability can be made large, $1 - 2^{-n}$ say, with a poly$(n)$-sized list. (One can simply repeat the singleton reduction many times, for example.)

Now, it is not at all evident or intuitive that we should be able to directly derandomize a reduction that only has success probability $1/n$.  Indeed, none of the hardness-vs-randomness results give hypotheses under which we can do so in this case.  It is much more plausible that the list-reduction can be derandomized (with a somewhat larger list).  Note though that this would not imply $NP = UP$: our output list of formulas may have many uniquely-satisfiable formulas, and perhaps some with many satisfying assignments, and it seems hopeless to try to define a uniquely-accepting computation over such a list.

Even if we could somehow give a  list-reduction in which a satisfiable $F$ always induced a list $F'_1, \ldots, F'_t$ where most of the $F'_j$'s are uniquely satisfiable, there is no clear way to turn that into a deterministic singleton reduction for isolation.  The real underlying difficulty is that we don't know of any "approximate-majority operation for uniquely-satisfiable formulas", that is, a reduction $R(F'_1, \ldots, F'_t)$ whose output is uniquely satisfiable if most $F'_j$'s are uniquely satisfiable, and unsatisfiable if most $F'_j$'s are unsatisfiable.  This also seems like a general phenomenon: reductions output more complex objects than decision algorithms, and the properties of these objects are harder to check, so it's harder to combine many of these objects into a single object that inherits some property of the majority.

For the Valiant-Vazirani case, it does not even seem likely under plausible derandomization assumptions that we'd be able to obtain $NP = FewP$, that is, to deterministically reduce satisfiable formulas to satisfiable formulas with $\leq$ poly$(n)$ solutions.  Intuitively this stems from the fact that the isolating procedure has no idea of even the rough size of the solution set of the formula $F$ it is given.


How efficiently can one find small subcovers for integer intervals?

Let me restate the first problem:

Problem: Given a set of intervals $\mathcal{S} = \{ I_1, I_2,\ldots,I_n\}$,  minimize $|\mathcal{C}|$, where $ \mathcal{C} =\{ I_{j_1}, I_{j_2},\ldots,I_{j_k}\} \subseteq\mathcal{S} $ and
$ \bigcup_{l=1}^{n}I_l = \bigcup_{m=1}^{k}I_{j_m} $

Define: Graph $G(V,E)$, $V = \{v_1, v_2, \ldots, v_n ,s ,t \}$ where,

Vertex $v_j \in V$ denotes interval $I_j$.
Vertices $v_k, v_l$ have an edge between them if their corresponding intervals $I_k,\; I_l$ overlap.
Source vertex $s$ and $v_j$ have an edge between them if $v_j$'s corresponding interval $I_j$ contains the leftmost point of $\bigcup_{l=1}^{n}I_l $.
Similarly sink vertex $t$ and $v_j$ have an edge between them if $v_j$'s corresponding interval $I_j$ contains the rightmost point of $\bigcup_{l=1}^{n}I_l $.

Answer: The intervals corresponding to the vertices in the 'shortest vertex path' between $s$ and  $t$ gives the minimum set cover!

If I have understood your 2nd question correctly, it is nothing but the weighted 1-dimensional set cover problem.

Remark 1: The intervals $I_j$ considered above might possibly have non-integer end-points.

Remark 2: One can solve this problem using dynamic programming, which I think has "lower" complexity than the shortest path solution.

EDIT-1: For the ease of exposition, I have considered only closed intervals in the above problem.


Confusion about a formal definition of PRAM consistency

When they define PRAM (page 11 of the arxiv preprint)
they actually state that vis is a partial order (in particular, transitive):

  We define PRAM consistency by requiring the visibility partial order to be a superset of session
  order:
  $$\text{PRAM} \triangleq so \subseteq vis.$$

Thus, the offending arrow in your diagram, from $w(x)0$ to $r(x)0$, is superfluous, as it is in the transitive closure of the other vis arrows.
So the $w(x)1$ write is already visible at the time when you would do $r(x)0$, so that read does not occur.


Detecting undirected cycles in logarithmic space

For the undirected cycle problem, you can traverse each connected component: at each node, when coming in through edge $k$, leave through edge $k+1$. (We can assume edges are ordered at each vertex.)

Now vou start such a traversal once from every node $v$, remembering only $v$ and the edge you left $v$ through. If the traversal returns to $v$ through a different edge, then $v$ lies on a cycle. If this is not the case for all $v$, then the graph is acyclic.

In general, in a logarithmic space algorithm you can only store constantly many pointers into the input and counters.


(This following is just my comment above migrated into solution form).

We construct a Karp reduction from Vertex Cover into your problem. Given a graph $G = (V,E)$ in which we want to find the size of a minimum vertex cover, construct the following program

minimize $\sum x_i$

subject to

$\max \left\{x_i, x_j\right\} = 1$ for $(x_i,x_j) \in E$
$x_i \geq 0$ for all $i \in \{1, 2, \cdots, |V|\}$.

This is just an instance of your linear programming variant, with $\vec a = \vec b = 1$ and $\mathcal{J} = \left\{\{u,v\} | (u,v) \in E\right\}$ along with your assumption from the comments that all variables are positive (which, as @AustinBuchanan and @SureshVenkat point out, is important).

It's easy to see that each vertex cover satisfies (1), and that anything that satisfies (1) and (2) can be transformed into a vertex cover by decreasing all variables until they hit $1$ or $0$ (whichever comes first). Thus, the two problems have the same objective value (enough to show NP-hardness), and in fact such a program immediately reveals the optimal vertex cover itself.


Unfortunately, research conferences generally do not place a premium on writing for readability. In fact, sometimes it seems the opposite is true: papers that explain their results carefully and readably, in a way that makes them easy to understand, are downgraded in the conference reviewing process because they are "too easy" while papers that could be simplified but haven't been are thought to be deep and rated highly because of it. So, if you rephrase your question to add another word, is it not just you who finds some research papers unnecessarily hard to read, then no, it is not. If you can find a survey paper on the same subject, that may be better, both because the point of a survey is to be readable and because the process of re-developing ideas while writing a survey often leads to simplifications.

As for strategies to read papers that you find hard, one of them that I sometimes use is the following: read the introduction to find out what problem they're trying to solve and some of the basic ideas of the solution, then stop reading and think about how you might try to use those ideas to solve the problem, and then go back and compare what you thought they might be doing to what they're actually doing. That way it may become clearer which parts of the paper are just technical but not difficult detail, and which other parts contain the key ideas needed to get through the difficult parts.


Why are so few natural candidates for NP-intermediate status?

As others have pointed out, it's debatable to what extent the thing you're trying to explain is even true.  One could argue that, in the 60s and 70s, theoretical computer scientists were just more interested in the sorts of problems that turn out to be either in P or else NP-complete.  Today, because of the rise of complexity-theoretic cryptography, quantum computing, lattices, etc.---as well as the simple fact that NP-completeness has become so well-understood---we've become more and more interested in the sorts of problems that turn out to be NP-intermediate.

Still, one could ask: to the extent that the thing is true---that is, to the extent that so many natural search and optimization problems "snap" to being either NP-complete or else in P---to that extent, why is it true?  Here, I think you can get a lot of intuition by looking at an earlier phenomenon from computability: that so many natural models of computation "snap" to being Turing-complete.  In that case, I'd say the explanation is that, once you have a few basic components---a read/write memory, loops, conditionals, etc.---it's hard to avoid being able to simulate a Turing machine, and therefore being Turing-complete.  In much the same way, once your search or optimization problem has a few basic components---most importantly, the ability to construct "gadgets" that mimic logic gates like AND, OR, and NOT---it's hard to avoid being able to encode SAT and therefore being NP-complete.

The way I like to think about it, problems like SAT exert a powerful "gravitational pull" on all the other computational problems in their vicinity, making them want to "snap up" to being NP-complete also.  So, it normally doesn't even require special explanation when yet another problem succumbs to that pull!  What's more striking, and more in need of explanation, is when an (apparently) hard NP problem has some property that lets it resist the gravitational pull of SAT.  We then want to know: what is that property?  Why can't you play the usual NP-completeness trick for this problem, of constructing gadgets that encode Boolean logic gates?  I made up a list of some common answers to that question in this recent CS.SE answer, but (as another commenter already pointed out) there are other possible answers that I missed.


Progress on generalized star-height problem?

Regarding your second question, an explanation why the generalized star height problem is less accessible than the star height problem is the following: Already Eggan's seminal paper in 1963 contained languages of (ordinary) star height $k$, for each $k\ge 0$. Only a few years later, McNaughton, and, independently, Déjean and Schützenberger, found examples over binary alphabets. This made clear what the problem "is about". During the years that followed, there was a more or less steady flow of published results in the area of the ordinary star height problem. This gave an ever increasing body of published examples, counterexamples and phenomena surrounding this problem.

In contrast, after some fifty years now, we don't know whether there is any regular language of star height at least two. So we do not even know whether there is a need for a decision procedure after all. This "complete lack of examples" indicates that it is extremely difficult to get a grip on this problem.


Are there natural separations in the nondeterministic time hierarchy?

As far as I know, we don't know of such languages, or if we do, there is significant controversy about the "naturalness" of them. I know this isn't really a satisfying answer, but I can say:

(a) If you prove an $\Omega(n^k)$ time lower bound for k-ISOLATED SAT for every $k$, then you have actually proved $P \neq NP$.

(b) One way you might hope to show that k-ISOLATED SAT is one of these natural problems in $NTIME[n^{k+1}] - NTIME[n^k]$ is to show that k-ISOLATED SAT problem is hard (in the usual, formal sense of having efficient reductions) for $NTIME[n^k]$. In fact this is the only way we know how to prove such results. But k-ISOLATED SAT is probably not hard in this sense, there are some very unlikely consequences.

The main reason is that k-ISOLATED SAT instances are solvable in $\Sigma_2 TIME[n]$, independently of $k$. You can existentially guess the isolated assignment, then universally verify (for all $O(\log (\sum_{i=1}^k {n \choose i}))$ ways to flip up to $k$ bits in the assignment) that none of the other "local" assignments work.

Here is the proof of part (a). Let ISOLATED SAT be the version of the problem with $k$ given as part of the input (in unary, say). Suppose we prove that ISOLATED SAT requires $\Omega(n^k)$ time for all $k$. If $P=NP$, then $\Sigma_2 TIME[n]$ is in $TIME[n^c]$ for some fixed $c$ (the proof uses an efficient version of Cook's theorem: if there is a SAT algorithm running in time $n^d$, then any $c > d^2$ suffices). But we proved that there is a language in $\Sigma_2 TIME[n]$ that is not in $TIME[n^k]$ for every $k$. This is a contradiction, so $P \neq NP$.

Here is the proof of part (b). If every $L \in NTIME[n^k]$ could be efficiently reduced to a k-ISOLATED SAT formula (e.g., all $n$ bit instances of $L$ get reduced to $k$-ISOLATED SAT formulas of at most $f(k) n^{c}$ size) then $NP=\bigcup_{k} NTIME[n^k] \subseteq \Sigma_2 TIME[n^{c+1}]$. This would immediately imply $coNP \neq NP$, but moreover it just looks very unlikely that all of $NP$ can be simulated so efficiently within the polynomial hierarchy.


Has this generalization of the vertex cover problem been researched?

This problem has been studied at least for paths. The problem is NP-complete for any $n \geq 2$ (see for example this).

It is know that the problem is hard even for very special graph classes. For example, in the case $n = 3$, it is NP-hard for cubic planar graphs of girth 3.

On the positive side, there are constant-factor approximations algorithms, at least for some special cases.


Extensionality of lambda calculus models

I presume that by extensionality you mean the law
$$(\forall x . f x = g x) \implies f = g.$$
If this is what you mean then the graph model $\mathcal{P}\omega$ is not extensional, while Dana Scott's $D_\infty$ is (I presume $D^\infty$ is Dana Scott's model of the $\beta\xi\eta\lambda$-calculus).

To see this, recall that $\mathcal{P}\omega$ is an algebraic lattice with the property that its space of continuous maps $[\mathcal{P}\omega \to \mathcal{P}\omega]$ is a proper retract of $\mathcal{P}\omega$, i.e., there are continuous maps
$$\Lambda : \mathcal{P}\omega \to [\mathcal{P}\omega \to \mathcal{P}\omega]$$
and
$$\Gamma : [\mathcal{P}\omega \to \mathcal{P}\omega] \to \mathcal{P}\omega$$
such that $\Lambda \circ \Gamma = \mathrm{id}$ but $\Gamma \circ \Lambda \neq \mathrm{id}$. Given $u, v \in \mathcal{P}\omega$, the application $u v$ is interpreted as $\Lambda(u)(v)$. Now take $u$ and $u'$ such that $u \neq u'$ but $\Lambda(u) = \Lambda(v)$ (these exist because $\Gamma \circ \Lambda \neq \mathrm{id}$). Then for all $v$ we have $u v = u v'$ yet $u \neq u'$. Extensionality is violated.

In contrast, $[D_\infty \to D_\infty]$ is isomorphic to $D_\infty$, i.e., there are continuous maps
$$\Lambda : D_\infty \to [D_\infty \to D_\infty]$$
and
$$\Gamma : [D_\infty \to D_\infty] \to D_\infty$$ which are inverses of each other. So consider any $u, u' \in D_\infty$ and suppose that $u v = u' v$ for all $v \in D_\infty$. This means that $\Lambda(u)(v) = \Lambda(u')(v)$ for all $v \in D_\infty$, hence $\Lambda(u) = \Lambda(u')$ and so $u = \Gamma(\Lambda(u)) = \Gamma(\Lambda(u')) = u'$. Extensionality is established.

We see that extensionality is a consequence of $\Gamma \circ \Lambda = \mathrm{id}$. What is the other equation $\Lambda \circ \Gamma = \mathrm{id}$ good for? For this we have to remember how $\lambda$-abstraction is interpreted:
$$\lambda X. u(X) = \Gamma (v \mapsto u(v))$$
In words, an expression $u(X)$ with a variable $X$ may be interpreted as a map which takes $v$ to $u(v)$. Then the $\lambda$-abstraction $\lambda X . u(X)$ is interpreted as the $\Gamma$-image of that function. Now from $\Lambda \circ \Gamma = \mathrm{id}$ we get
$$(\lambda X . u(X)) w = \Lambda (\Gamma (v \mapsto u(v))) (w) = (v \mapsto u(v))(w) = u(w)$$
which is just $\beta$-reduction.


Collection of failed attempts to solve X

I've idly entertained the idea of an online arxiv overlay "journal" of negative results. The idea would be to allow negative results or counterexamples that don't seem suitable for a full publication in traditional venues. It would be lightly reviewed, so that we can guarantee that every paper has at least been looked over and approved by an expert in the area. It wouldn't necessarily be archival or "official", but it would at least be citable.

I think such a resource could be very helpful for publicizing dead ends in some lines of inquiry as well as "folklore negative results" that may not be widely known. I can think of a few examples from my own experience. A main challenge would be in finding and connecting with reviewers, due to the variety of possible research areas involved.

If there seems to be enough interest in this idea from the cstheory community, particularly people saying they'd be willing to submit and to review, then I'd be willing to take a lead in organizing. I'm pretty sure I can find some colleagues willing to join and help organize for the first few years.


A PAC-like analogue for 1-class classification?

I think there is a model called "Learning from Positive Examples (Only)" or you can additionally allow unlabeled data (I don't remember the details).  A search for these terms should bring up various papers and models.  Here is one.


You are probably speaking about something like a process ontology. Lately, that research has focused (moved?) on semantic workflows, e.g. to model processes in science, related with reproducibility. Similarly, we can also find the application of ontologies to business processes.

For more classical (lower level?) approaches, you may be interested in the homoiconicity property of programming languages like Lisp. In such a case these "networks" usually take the shape of parse trees, i.e. the representation is at a syntactic level and semantics are implicit, e.g. loops and recursive calls are still just a syntactic tree, even if the execution would not result into a tree.


Fast extraction of the edges of an induced subgraph

I'm assuming you can do some preprocessing to organize your graph for this computation, since otherwise your question makes little sense.

In the $O(|W|d)$ algorithm, you can replace the average degree by the degeneracy of $G$. For an undirected graph $G$, being $d$-degenerate means there is a vertex ordering such that each vertex has at most $d$ neighbors that are later in the ordering. To extract the induced subgraph, loop over each vertex of $W$ and test, for each of its $\le d$ later neighbors in a degeneracy ordering, whether that neighbor also belongs to $W$. Each edge is extracted once, when the loop reaches its earlier endpoint.

Because it tests a subset of the same pairs, this algorithm is never worse than your average degree algorithm and could in some cases be significantly better. And if you're computing worst case bounds in terms of the numbers of vertices and edges of the original graph, the average-degree algorithm can be as bad as $\Theta(|W|n)$ (if $W$ picks out vertices of unusually high degree), even for sparse graphs, while the degeneracy algorithm is always $O(|W|\sqrt m)$ (because degeneracy is always $O(\sqrt m)$).


Reference to lower bound on separator in a grid?

Looks like the book "Graph separators, with applications" by Arnold Rosenberg and Lenwood Heath answers your question (see section 4.3.4.), but it could happen that I misunderstood their notation (please, let me know). Anyway, this book is a very comprehensive reference on separators.

EDIT. Here is a download link on Springer: http://www.springerlink.com/content/978-0-306-46464-5


P vs. NP in a logic with a random oracle

Yes on Question 1 (assuming ZFC is consistent). You don't need $f$ to be random exactly, any $f$ will do. And for the proof you need to also use the fact that there is an oracle $h$ with NP$^h=$P$^h$.


Complexity of computing the union of H-polytopes in three dimensions

Your problem is solvable in polynomial time, as the dimension is fixed (at $d=3$):

Let $h_1,\ldots,h_n$ be an enumeration of all the bounding hyperplanes of the
polytopes $P_1,\ldots,P_k$ and $Q$.
Compute the arrangement of $h_1,\ldots,h_n$ (the subdivision of three-dimensional space into vertices edges, faces, and cells). This can be done in polynomial time; see for instance "Constructing Arrangements of Lines and Hyperplanes with Applications" by H. Edelsbrunner, J. O’Rourke, and R. Seidel, SIAM Journal on Computing 15 (1986), pp 341–363.
Now check whether there exists some cell $C$ in the arrangement that is contained in $Q$ but in none of $P_1,\ldots,P_k$.
(For checking containment, it is enough to check whether the vertices of
the cell satisfy the inequalities of the polytope.)
If such a cell $C$ exists, answer NO. Otherwise answer YES.

If the dimension $d$ is given as part of the input, then your problem
("Does the union of $P_1,\ldots,P_k$ cover all of $Q$") is coNP-hard.


Problem property name where an optimal solution in a graph can be used as a solution in any subgraph

A master solution for an instance of a combinatorial problem is a solution with the property that it is optimal for any sub instance.
$~$

  Martijn van Ee, René Sitters:
  On the Complexity of Master Problems.
  Proceedings of MFCS-2015, LNCS 9235, pp 567-576
  https://link.springer.com/chapter/10.1007%2F978-3-662-48054-0_47

$~$

  Deineko, V.G., Rudolf, R., Woeginger, G.J.:
  Sometimes travelling is easy: The master tour problem.
  SIAM Journal on Discrete Mathematics 11, 1998, pp 81–93.
  https://epubs.siam.org/doi/10.1137/S0895480195281878


What are some examples of sequential-decision tasks?

One kind of sequential problem is making control decisions in real time. Consider the problem of driving a vehicle. The system will have a state, you can observe some measurements, and you must make a decision. You decision generates and input which then affect the future state of the vehicle and the whole process repeats. A problem which interacts with an external entity that changes its behavior based on a decision is sequential in nature. Other examples include things like optimally managing a stock portfolio, searching for an evading opponent, optimally playing a card game.

One non-sequential problem is classifying the fruit on a scanner in a grocery store. A measurement is taken, the data is processed and and output is determined. When the output generated does not alter the nature of of future outputs, it is non-sequential.


What is the role of the Bicolored Calculus of Constructions?

In The Implicit Calculus of Constructions
Extending Pure Type Systems with
an Intersection Type Binder and Subtyping, Alexandre Miquel introduces the basic concepts for the Implicit Calculus of Constructions, which I believe is synonymous with the Bicolored Calculus of Constructions.

The point is (among other things) to have a calculus without the clutter of explicit type annotations everywhere. Type inference is (very likely to be) undecidable though.

In this calculus, if we take $id=\lambda x. x$, then you can derive
$$ \vdash id\colon \forall X\colon Type. X\rightarrow X$$
by simply using the explicit product and the implicit product rules in succession. Then the instantiation rule for the implicit product allows
$$ \vdash id\colon Nat\rightarrow Nat $$
and so
$$ \vdash id\ 0 \colon Nat$$
The system admits subject reduction and confluence, even on untyped terms (which in fact fails for calculi with abstraction annotations). All this can be found in Alexandre's thesis, which is sadly in French. Not sure I have a better reference for these results though I'm afraid.


Computing the Levenshtein distance quickly

What you are asking about is the problem of near-neighbor search under the edit distance. You didn't mention whether you're interested in theoretical results or heuristics, so I'll answer the former.

The edit distance is somewhat nasty to deal with for building near-neighbor search structures. The main problem is that as a metric, it behaves (sort of) like other well known bad metrics like $\ell_1$ for the purpose of dimensionality reduction and approximation. There's a rather vast body of work to read on this topic, and your best source is the set of papers by Alex Andoni: by following pointers backward (for example from his FOCS 2010 paper) you'll get a good set of sources.