How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

That a formula is not provable can essentially be done in two ways. With some luck we might be able to show within type theory that the formula implies one which is already known to be not provable. The other way is to find a model in which the formula is invalid, and this can be quite hard. For example, it took a very long time to find the groupoid model of dependent type theory, which was the first to invalidate uniqueness of identity proofs.

The question "what is a model of dependent type theory?" has a somewhat complicated answer. If you ignore certain properties of substitution, a model is a locally cartesian closed category, and that might be the simplest answer. If you want a "real" model, then there are several options, see the nLab page on categorical models of dependent type theory. In any case, the answer is always a bit complicated because dependent type theory is a fairly complex formal system.

If I were to suggest just one article on the subject, I would probably recommend the original paper by Robert Seely, "Locally cartesian closed categories and type theory". If I were to suggest another one, it would probably be one that explains what needs to be corrected in Seely's paper, e.g., Martin Hoffman's "On the Interpretation of Type Theory in Locally Cartesian Closed Categories".

A recent important advance in this area is the realization that homotopy-theoretic models are also models of dependent type theory, see homotopytypetheory.org references. This provides a wealth of possibilities, but one must now learn homotopy theory to get hands on the models.


There's a nice compilation of definitions of related NP-complete planar satisfiability problems at http://courses.csail.mit.edu/6.890/fall14/scribe/lec7.pdf

One of them, planar monotone 3-sat, allows you to split each terminal into positive and negative, with the terminals placed along a line with the positive part on one side of the line and the negative part on the other side of the line. The clauses have only positive or only negative terminals and are placed on the positive or negative side of the line respectively.


When can partial spectral sparsifiers be combined?

Regarding your 1st question: no, this would not hold in general.

Rather (answering your 2nd question), the right way to interpret the approach by Spielman and Teng is as follows: let $G'$ be a vertex-induced subgraph of $G$, and $H'$ a spectral sparsifier of $G'$. Then the graph $G-G'+H'$ (replace all edges in $G'$ by those in $H'$) will be a spectral sparsifier of $G$. This easily follows by combining the Laplacians of $G$ and $H'$. As a result, we can sparsify $G$ by subsequently sparsifying subgraphs.

And finally, you are asking about ways to amplify the success probability of a sparsification algorithm. For spectral sparsification, there is a rather easy way: construct one with constant success probability, check whether it is indeed a spectral sparsifier (this amounts to checking whether a certain matrix is PSD, which can be done efficiently), if not, reiterate. After $O(\log(1/\epsilon))$ iteration this outputs a spectral sparsifier with probability at least $1-\epsilon$. Note that this cannot be done for say cut sparsification, as there is no efficient "verification procedure" to check whether a graph is a cut sparsifier of another graph.


Algorithm Design for only Mutual Information Sharing

What you want to do is called "Private Set Intersection". You can think of Alice and Bob as each holding sets (the indices for which their strings are "1"), and they want to compute the intersection (the bitwise AND) so that neither of them learns anything about the other's set except what is implied by the intersection itself.

This problem is well studied. See, for example, Freedman, Nissim, and Pinkas: http://www.pinkas.net/PAPERS/FNP04.pdf


Your definition of $D$ is not clear, if it is $D = \max_f (R(f) - ER(f))$, then it is exponential.

There are DNFs whose shortest proofs in ER is exponentially shorter than their shortest proofs in R e.g. PHP (pigeon hole principle) has polynomial size ER-proofs but only exponential size R-proofs.

Unsatisfiability of $f$ is the same as $\lnot f$ being a tautology. Let $\lnot f$ be as PHP. Then $R(f)$ is exponential where as $ER(f)$ is polynomial, so the difference is exponential. Also it cannot be more than exponential.

Addendum:

If $D =  \min_f (R(f) - ER(f))$ then it is 0. Take $\lnot f=\top$ and it has one line proof in both. (R is included in ER so it cannot be less than 0.)


Can one efficiently uniformly sample a neighbor of a vertex in the graph of a polytope?

Edit 2: Embarrassingly, there is a two line proof of the $NP$-hardness, if one starts with the right polytope.

First, recall the circulation polytope of a graph on the bottom of page 4 of Generating all vertices of a polyhedron is hard.

It's vertices are in bijective correspondence with the directed simple cycles. Therefore, they are hard to sample or count by JVV Proposition 5.1. :-D

Equipped with these keywords, I was able to find the hardness of sampling result as theorem 1 of Transversal Hypergraphs and Families of Polyhedral Cones by Khachiyan.

Edit: I wrote up the argument below, and it appears correct. However, there is a much simpler argument, which I'll outline here:

a) By Analysis of backtrack algorithms for listing all vertices and all faces
of a convex polyhedron (Fukuda et al.) it is strongly NP-hard to solve the following problem on polytopes:

Input: A polytope $Ax = b , x \geq 0$ in $\mathbb{R}^n$ a subset $S \subseteq n$

Output: Whether there is a vertex $v$ of $P$ that is nonzero on each of the coordinates in $S$.

b) Given this, one can make the following construction: introduce new variables $y_{ik}$ for $i \in S$ and $k = 1, \ldots, d$, and introduce the inequality $0 \leq y_{ik} \leq x_i$. Call the resulting polytope $P_{S,d}$. The point of this construction is to introduce a hypercube above each vertex, of dimension $d |supp(x) \cap S|$.

c) One can check that the vertices of this polytope all lie above the vertices of the old polytope, and that the number of vertices over a vertex is $2^{d | supp(x) \cap S|}$, where $supp$ is the function that sends a vertex to the coordinates where it is nonzero.

d) By a usual chain of bigons type argument it follows that by taking $d$ sufficiently large, a uniform sample from the vertices of $P_{S,d}$ would (with high probability) give a sample from the vertices maximizing the size of their intersection with $S$.

There appear to be various extensions of this. I will update with a link when the writing is done.

(The old argument used to be here -- it is in the edit history. I've removed it because it's very long and will interfere with finding the correct answer to the question.)


To prove that every tree with two or more internal nodes gives you a 3-colorable graph, use induction on the number of nodes of the tree. If you orient the tree from an arbitrarily chosen root node, there always exists an internal node $v$ whose children are all leaves. Now split into cases:

If $v$ has one child, then the graph can be reduced down to nothing by repeatedly removing vertices of degree at most two, and three-colored by reinserting the vertices in the reverse order and giving them a color distinct from their two neighbors.
If $v$ has three or more children, then the tree can be reduced in size by removing two consecutive children, forming the graph by connecting the remaining leaves into a cycle, and then coloring the smaller graph. The remaining children of $v$ must alternate in color and reinserting the removed children maintains the same alternation.
If $v$ has exactly two children, and there are three or more internal nodes, then remove $v$ and its two children from $T$, form  the graph by connecting the remaining leaves into a cycle, and then color it. Let $p$, $q$, and $r$ be the parent of $v$, the node to the left of $v$'s left child in the leaf cycle, and the node to the right of $v$'s right child in the leaf cycle; $q$ and $r$ are adjacent in the smaller graph, so must have different colors. There are two subcases. If $p$, $q$, and $r$ use only two colors among them, then the two children of $v$ can be colored in alternation with $q$ and $r$ using the same two colors, and $v$ can be given the remaining third color. On the other hand, if $p$, $q$, and $r$ use three different colors, then $v$ can be given $q$'s color, the left child of $v$ can be given $r$'s color, and the right child of $v$ can be given $p$'s color.
In the remaining base case, $T$ has exactly two internal nodes, each adjacent to two leaves. The graph is the graph of a triangular cylinder, which can be three-colored.

Incidentally, if $T$ has no degree two vertices, then $G(T)$ is called a Halin graph; with or without the degree two restriction, it has bounded treewidth, so an alternative method for finding an optimal coloring in linear time is to use dynamic programming. However, this method does not tell you ahead of time which trees require only three colors.


Graph (Forest) representation that supports edge deletion and efficient traversal

This problem is known as Decremental Connectivity. In general, decremental connectivity is where you need to support the operations:

Connected($u$,$v$) : Check whether vertex $u$ is connected to vertex $v$
Delete($e$): Remove an edge $e$

Given $n$ queries of the first kind and $m$ queries of the second, Even and Shiloach [1] gave an $O(n\log{n} + m)$ algorithm and later, Alstrup et al. gave an $O(n+m)$ algorithm in [2].

There is a simple way to do the former using a data-structure known as the Euler Tour Trees or the approach taken in [1] could also be used. If you wish to implement [1], the tree is stored as a set of connected components. It is then enough to determine which component each vertex belongs to answer the connected-ness query. There is a breadth-first seach used to answer the deletion process. But it is $O(\log{n})$ amortized. This would achieve $O(n\log{n} + m)$.

If the $\log{n}$ factor must be removed, then a leaf-trimming approach would work. You trim all subtrees with size $\geq\log{n}$. Then, you can use the Euler Tour Trees (or the approach in [1]) to perform queries in the untrimmed portion. Some cases could need to be seperately handled. This is the approach given in [2].

[1] S. Even and Y. Shiloah. An on-line edge-deletion problem. Journal of the Assoiation for
Computing Mahinery, 28:1-4, 1981.

[2] Stephen Alstrup and Jens Peter Secher and Maz Spork. Optimal On-line Decremental Connectivity in Trees, IPL, 65:64-8, 1997


Mathematical explanation of recursion and lambda (referenced in The Little Schemer)

What Sam said.

Also, it's really well under a page.  If you're familiar with evaluation contexts, you can specify the call-by-value lambda calculus like this:

Terms

$$M ::= x \mid (M \, M) \mid (\lambda x . M)$$

Values

$$V = (\lambda x . M)$$

Evaluation contexts

$$E ::= [\:] \mid ([\:] M) | (V [\:])$$

The (only) reduction rule:

$$E[((\lambda x . M) V)] \to E[M.\mathrm{subst}(V,x)]$$

where $.\mathrm{subst}$ denotes capture-avoiding substitution.

Again, though, the background knowledge involved in reading this definition is by no means self-evident. There are many free places on the web to read about it. For a tidy and well-typeset presentation, you might also be interested in Felleisen/Flatt/Findler's book, Semantics Engineering with Redex.

Holey Moley! I just googled for it, and got the full PDF online. Well, that won't last...


Abstract machine or algorithm for line solving a Nonogram

... or if you just want to have fun you can simply grab a lot of useful tips from other (powerful) Nonogram solvers; you can start from here:

http://webpbn.com/pbnsolve.html which will teleport :-) you to:

http://webpbn.com/survey/ and ...

http://www.comp.lancs.ac.uk/~ss/nonogram/ ...

http://www.comp.lancs.ac.uk/~ss/nonogram/list-solvers

You can find detail descriptions of single-line / multi-line solving techniques and descriptions of more complex strategies.

When switching to 3D Nonograms single-line and multi-line strategies are still valid (apply 2D multi-line strategies on each section of your 3D puzzle); but if the 3D puzzle is difficult (or random), an iterated loop with those strategies ends up with many unknown pixels and to proceed you must apply specific 3D strategies.

If your question is more TCS oriented  then there are plenty of references in some public downloadable articles: http://www.google.it/search?as_q=nonogram+np&as_filetype=pdf


Do algorithms for solving parity games ignore other possible strategies for player V after finding one?

Parity games can be reduced to discounted payoff games. See, e.g.,

Marcin Jurdziński (1998). Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters 68:3 119-124.

As explained in that paper (and first observed by Zwick and Paterson, I believe), there are min/max optimality equations for discounted payoff games with a unique solution that assigns a "value" to each state. From these values, it is easy to read off all optimal strategies of the players.

Discounted payoff games can in turn can be solved as a P-matrix Linear Complementarity Problem (LCP), where the reduction uses the optimality equations and from a solution to the LCP one could again read off all optimal strategies. See,

Marcin Jurdziński and Rahul Savani (2008). A simple P-matrix linear complementarity problem for discounted games. Computability in Europe (CiE), 283-293.

Now in the following paper a discrete strategy improvement algorithm for parity games is given that essentially defines and uses optimality equations.

Jens Vöge and Marcin Jurdziński (2000). A Discrete Strategy Improvement Algorithm for Solving Parity Games. Computer-aided Verification (CAV).

It's very possible you could read off all strategies from a "solution" to those optimality equations, e.g., obtained via their algorithms - but, I am not sure.


Constructively efficient algorithms without efficient correctness and efficiency proof

This is the same idea as Andrej's answer but with more details.

Krajicek and Pudlak [LNCS 960, 1995, pp. 210-220] have shown that if $P(x)$ is a $\Sigma^b_1$-property that defines primes in the standard model and $$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 < y_1, y_2 < x \land x = y_1y_2)$$ then there is a polynomial time factoring algorithm. This gives a bunch of examples since any NP algorithm for primality testing basically yields such a $\Sigma^b_1$ formula. In particular, the AKS primality test gives such a formula (when appropriately recast in the language of $S^1_2$). The paper by Krajicek and Pudlak gives more cryptography related examples of this kind but predates AKS and related advances by a few years.


A quick informal algorithm to prove that the problem is decidable:

suppose that there are $n$ Input/Outputs $I_1,...I_n$;
build a graph $G$ where each $I_i$, the $MINUS$ and the $PLUS$ are nodes, and replace each nested maze $Mj$ with a $K_n$ subgraph (complete graph); add the edges between $I_i, MINUS, PLUS, Mj_{I_k}$ according to the maze; keep "extern" $Mj_{I_i} \rightarrow Mj_{I_k}$ edges distinct from the corresponding "internal" edges $I_i \rightarrow I_k$ of $Mj$ as a complete subgraph;
enumerate all paths from MINUS to PLUS in $G$ (avoiding cycles);
if you find a path that doesn't traverse a nested copy, then it is a solution; otherwise expand each "internal" traversals of the nested mazes $Mj$ of each path:

Suppose that a path in the first enumeration is $MINUS \rightarrow A_{I_i} \rightarrow A_{I_j} \rightarrow B_{I_k} \rightarrow B_{I_h} \rightarrow PLUS$, then the path is a valid solution iif there is a path from $I_i \rightarrow I_j$ and from $I_k \rightarrow I_h$ in the original maze (graph $G$).

So we must expand the $A_{I_i} \rightarrow A_{I_j}$ and $B_{I_k} \rightarrow B_{I_h}$ traversals enumerating all the paths from $I_i$ to $I_k$ and from $I_k$ to $I_h$ in $G$.

Infinite loops are detected when we are enumerating all paths from $I_i$ to $I_k$ in an expansion of a path that in a previous stage already contained $... \rightarrow M_{I_i} \rightarrow M_{I_k} \rightarrow ...$ for some submaze $M$ (there are only $n^2$ possible expansions).

A solution is found if we find a path expansion that contains only inputs/outputs $I_i$; the maze has no solution if we cannot further expand the paths without loops.


I'm not aware of a general rule to convert centralized bounds to the distributed setting. In the distributed setting, local computation is given for free but the difficulty lies in breaking the symmetry - a node needs to accumulate enough information about it's neighborhood to make a decision about being part of the output set, e.g. being in the MIS. (Taking this a step further, we can think of an $r$-round algorithm as a function mapping $r$-neighborhoods to a yes/no decision.)

For example, for certain $n$-node graphs with max degree $\Delta$ there is an $\Omega(\sqrt{\log n}+\log \Delta)$ lower bound [2] known on the number of distributed rounds, that holds for (the distributed version of) computing a constant approximation of a minimum vertex cover or of a minimum dominating set.

While the above problems are known to be NP-complete, the same lower bound also holds for problems for which there are polynomial time centralized algorithms like computing a maximal independent set or finding a maximal matching.

For most of these problems the lower bound is almost tight; there are distributed algorithms that run in polylogarithmic rounds (see [2] and references therein).

On the other hand, some NP complete problems even allow constant time solutions in the distributed setting! In [1] there's an $O(1)$ round distributed algorithm for $O(n^{1/2+\varepsilon} \chi)$-coloring, which itself is NP complete.

[1] Leonid Barenboim. On the Locality of Some NP-Complete Problems
http://arxiv.org/abs/1204.6675

[2] Fabian Kuhn, Thomas Moscibroda, Roger Wattenhofer. Local Computation: Lower and Upper Bounds.
http://arxiv.org/pdf/1204.6675v1.pdf


I think I proved it yesterday. Thus here goes the sketch of the proof.
At first, the following lemma is proved.

Lemma. Let $\mathcal{P}$ - a partial order, $G(\mathcal{P})$ - its linear extension graph and $v_1,v_2$ - two adjacent vertices of $G(\mathcal{P})$. Then $|deg(v_1)-deg(v_2)|\leq 2$.

The sketch of the proof.

At the same time, $v_1,v_2$ are linear extensions of $\mathcal{P}$ such that one of them, say $v_1$, can be transformed into $v_2$ by one transposition of adjacent elements (adjacent transposition). It is easy to see (consider, for instance, $d$ and $e$ from the above figure) that any element $x_i$ of any linear extension $L=x_1x_2\dots x_n$ can change the number of incomparable adjacent elements on at most two:

If $x_i$ can be transposed at all then at least one its neighbor, say $x_{i+1}$, is incomparable to it ($x_i\parallel x_{i+1}$, if comparable then $x_i\perp x_{i+1}$). Note: before transposing we have $L_1=\dots x_{i-1}x_ix_{i+1}x_{i+2}\dots$ and immediately after - $L_2=\dots x_{i-1}x_{i+1}x_{i}x_{i+2}\dots$.
Let us consider how the number of incomparabilities (degree of the linear extension as the vertex in $G(\mathcal{P})$) in $L$ could change. We consider at first the pair $x_ix_{i+2}$. For $x_{i-1}x_{i+1}$ the same conclusion follows by symmetry.

If $x_{i+1}\parallel(\perp) x_{i+2}\land x_{i}\parallel(\perp) x_{i+2}$, then $deg(L)$ doesn't change.
If $x_{i+1}\perp(\parallel) x_{i+2}\land x_{i}\parallel(\perp) x_{i+2}$, then $deg(L)$ increases (decreases) by one.The sketch of the proof is completed.

Theorem. Let $G(\mathcal{P})$ - a linear extension graph. If $G(\mathcal{P})$ contains vertices $v_1,v_2$ with $deg(v_1)=k,deg(v_2)=k+2$, then there is $v_3\in G(\mathcal{P})$ such that $deg(v_3)=k+1$.

The sketch of the proof.

Suppose $v_1,v_2,deg(v_1)=k,deg(v_2)=k+2$ are adjacent in $G(\mathcal{P})$, otherwise any vertex with degree $k$ in $G(\mathcal{P})$ is adjacent with some vertex if such exists with degree $k+1$.

Let us consider the case where we have $L_1,L_2$ from the previous lemma such that

$$x_{i+1}\perp x_{i+2}\land x_{i}\parallel x_{i+2},$$
and
$$x_{i-1}\perp x_{i}\land x_{i-1}\parallel x_{i+1},$$

Thus $deg(L_2)=deg(L_1)+2$.

Let us now start transpose $x_{i+1}$ in the direction of $x_1$. It is easy to see that eventually we could stop at the position where

$$x_{j}\perp x_{i+1}\land x_{i+1}\parallel x_{j+1},$$ for some $j<i-1$.
The sketch of the proof is completed.


Reasons to believe $P \ne NP \cap coNP$ (or not)

Theorem 3.1 of One-Way Permutations and Self-Witnessing Languages C. Homan and M. Thakur, Journal of Computer and System Sciences, 67(3):608-622, November 2003. [ as .pdf ] states that $P≠UP∩coUP$ if and only if ("worst-case") one-way permutations exist. Theorem 3.2 recalls 10 further hypotheses that have been shown to be equivalent to $P≠UP∩coUP$.

Also, we have strong reason to conjecture that $UP \ne NP$. Therefore, the above theorem and the conjecture result in a strong reason to believe that $P \ne NP ∩ coNP$.

Disclaimer: I moved Mohammad Al-Turkistany's edit of my answer to this community wiki answer. He believes that it perfectly answers the question since the existence of one-way permutations is widely believed. I myself haven't yet sufficiently understood the difference between "worst-case" and "average-case" one-way functions to claim that it really answers the question.


Finding simple fixed length paths in directed graphs

The color coding technique for deciding if a graph contains a $k$-path, presented for example in the book Parameterized Algorithms, can be turned into output-sensitive enumeration algorithm for such paths.

The algorithm works in iterations in which a random coloring of $k$ colors is assigned to the vertices of the graph, and then the paths with distinctly colored vertices are identified by dynamic programming.
In each iteration, compute by dynamic programming the function $P(S, u)$ denoting the number of paths that use the subset $S$ of colors and end in the vertex $u$. Then trace the positive values in this dynamic programming backwards to enumerate the paths. In this way the paths identified by this coloring can be enumerated in $O(2^km + Pm)$, where $P$ is the number of such paths and $m$ is the number of edges.

A path of length $k$ is identified with probability at least $e^{-k}$, so by the coupon collector analysis $O(e^k k \log n)$ iterations is enough to identify all (possibly $n^k$) paths with constant probability. A path of length $k$ is identified with probability at most $O(e^{-k} k)$, so the total expected time complexity of the algorithm is $O((2e)^k km \log n + P k^2 m \log n)$, where $P$ is the number of paths of length $k$.


Can machine learning algorithms be trained to discard nonsense?

The problem you're describing can perhaps be treated as "anomaly detection". Google the term in quotes, you'll get a ton of references. So the idea would be to first train an anomaly detector to separate the "apples, oranges, and other fruits" from non-fruits (or "nonsense" in OP terminology). Then train a classifier on the fruits.

Update. In light of additional answers -- and too long for a comment.
The problem with declaring a "non-fruit" category highlights the distinction between classification and anomaly detection. In classification, we assume 2 or more coherent classes. Apples, oranges, bananas -- these all have well-defined common characteristics. On the other hand, "non-fruit" is not a coherent category. It can only be meaningfully defined as something like "not fulfilling enough of the fruit characteristics". Anomalous objects are not a coherent class; they are by definition anything that is not sufficiently close to a "normal" object. We do not expect examples of anomalous objects to be informative for training. After all, you can just generate random pixel-images and get tons of anomalous examples for free!

This is why anomaly detection requires techniques distinct from classification.


The undirected version is NP-hard. More specifically, the following problem, known as Partial Feedback Edge Set is NP-complete: given an undirected graph $G$, and positive integers $K$ and $L$, is there a set of at most $K$ edges that contains at least one edge from every cycle of length at most $L$ in $G$.  This is still NP-complete for any fixed $L\geq 3$, and if $G$ is restricted to be bipartite (in which case, $L$ may also be fixed to any value of at least $4$).

For the directed case, Karp's proof that Feedback Arc Set is NP-complete  actually shows that it's NP-complete to determine if you can remove all directed $4$-cycles from an oriented graph by deleting at most $k$ edges. (His reduction from Vertex Cover produces an oriented, triangle-free graph in which deleting all $4$-cycles deletes all cycles.) But that's not what you're asking.

Sources: The undirected version is problem GT9 of Garey and Johnson, Computers and Intractability (Freeman, New York, 1979). The original paper was Yannakakis, Node- and edge-deletion NP-complete problems (Proceedings of STOC 1978) but it doesn't seem to contain a proof. Karp's Feedback Arc Set proof is on page  of the "21 problems" paper: Reducibility among combinatorial problems (Proceedings of symposium on Complexity of Computer Computations, 1972).


Faster join of treap-like data structures with approximately the same size

Nope, it's not possible to do this with ordinary Treaps if the priorities are random.

The precise claim I'll make is that to perform such a merge on two equally sized treaps with random priorities requires updating $\Theta(\log n)$ pointers in expectation.

Here's a rough proof sketch:

Consider the number of pointers you have to change in expectation to perform the operation.  It's easier to prove a $\Theta(\log n)$ bound if we don't insert $t_r$ but just merge $T_1$ and $T_2$.
Consider the right spine $S_1$ of $T_1$ and the left spine $S_2$ of $T_2$.
Color the elements of $S_1$ red and those of $S_2$ blue.
Order $S_1 \cup S_2$ by priority.  We have to change a pointer each time the color changes in this sequence.  Since both spines have size $\Theta(\log n)$ with high probability, and
the priorities are random, it's not too hard to see that the # of color changes in the sequence is also $\Theta(\log n)$.  So we need to update $\Theta(\log n)$ pointers for the merge (without adding $t_r$).

Now, adding $t_r$ while doing the merge doesn't really help much.
The number of pointer changes in that case can be lower bounded as follows:
Order $S_1 \cup S_2 \cup \{t_r\}$ by priority.  Delete everything less than $t_r$ in the sequence.  Then # of color changes in the resulting sequence is our lower bound.
Since $t_r$ has random priority, the expected height of the subtree rooted at it in the final treap is $O(1)$, so it only has $O(1)$ nodes of $S_1 \cup S_2$ with lower priority than it in expectation, so we lost only $O(1)$ pointer changes in our lower bound when adding $t_r$.

Now, that said, there's probably a way to get a "treap-like" data structure which allows for constant expected time merges.


Can the "mutual independence" condition in the Lovász local lemma be weakened?

The Lopsided Lovasz Local Lemma relaxes the mutual independence condition to negative dependence. We assume we have events $A_1, \ldots, A_n$, with a lopsidependency graph $G$ defined on $[n]$ s.t. for every event $A_i$ and every $S \subseteq [n] \setminus \Gamma^+(i)$,
$$
\Pr\left(A_i \mid \bigwedge_{j \in S}{\bar{A_j}}\right) \le \Pr(A_i).
$$
As you (sort of) suggest, the classical inductive proof of LLL works fine with the lopsidependency graph in place of the depdendency graph. This answers your question because the negative dependence condition is only weaker than the equality you wrote. See these notes by Vondrak for some applications.

The tightness of the constant $e$ (in the limit) was shown by Shearer, who characterized the smallest probabilities that guarantee a local lemma-type statement for any given dependency graph. There are fascinating connections with statistical mechanics, covered in a paper of Scott and Sokal.


Determining the number of clusters using property testing algorithm

First. One can do better as far as the sampling - at least if $d$ is large - $O(\frac{kd \log k}{\epsilon} \log \frac{1}{\epsilon})$ should follow easily from relative approximations http://sarielhp.org/p/06/relative/ and combining range spaces of bounded VC dimension (if you send me email I would email you a pdf containing this combining result you need - its well known, but i dont know a ref for that). Secondly, relative approximation sample in this case, guarantees that if the sample fails, then $k$ is too small. So, do exponential search for the right value of $k$, specifically, start with $k_i = 2^i$, and let $R_i$ be the the $i$th sample of size $n_i = O( \frac{kd \log k}{\epsilon} \log \frac{i}{\epsilon} )$ (the $i$ is not a typo).

Let $\alpha$ be the minimum $i$ for which the sample succeeds using the black box. Now, use brute force (on the sample) to find the minimum $k\leq k_\alpha$ for which the sample works. And this is your desired $k$. You need to carefully account for the probability of success, but thats why the $i$ is there - its one of these standard geometric summation stuff.

The $i$ can be avoided -- indeed, the probability that $\alpha$ is bigger by $\Delta$ than its correct value is smaller than $2^{-\Delta}$. If you do that, then the sample you are going to use is of the right size with good probability. That is, if the minimum $k$ for which you can cover more than $(1-\epsilon)n$ of the points is $\kappa$, then the sample the algorithm uses is $O\left( \frac{\kappa d \log \kappa}{\epsilon} \log \frac{1}{\epsilon} \right)$.

There is some added fuzzyness in the answer of this algorithm. The returned answer $\kappa$ is the minimum such that any value of $k < \kappa$, is say $(1-\epsilon/2)$-far from from being k-clustered. I assume this is OK.

In practice you would do something different. Hmm. Something to think about....


Warning: This is not yet a complete answer. If plausibility arguments make you uncomfortable, stop reading.

I will consider a variant where we want to multiply (x - a_1) ... (x - a_n) over the complex numbers.

The problem is dual to evaluating a polynomial at n points. We know this can be done cleverly in O(n log n) time when the points happen to be nth roots of unity. This takes essential advantage of the symmetries of regular polygons that underlie the Fast Fourier Transform. That transform comes in two forms, conventionally called decimation-in-time and decimation-in-frequency. In radix two they rely on a dual pair of symmetries of even-sided regular polygons: the interlocking symmetry (a regular hexagon consists of two interlocking equilateral triangles) and the fan unfolding symmetry (cut a regular hexagon in half and unfold the pieces like fans into equilateral triangles).

From this perspective, it seems highly implausible that an O(n log n) algorithm would exist for an arbitrary set of n points without special symmetries. It would imply that there is nothing algorithmically exceptional about regular polygons as compared to random sets of points in the complex plane.


What are theoretically sound programming languages for graph problems?

You might want to look at The Graph Programming Language GP. From the linked page:

  GP (for Graph Programs) is a rule-based, nondeterministic programming language for solving graph problems at a high level of abstraction, freeing programmers from handling low-level data structures. The core of GP consists of four constructs: single-step application of a set of conditional graph-transformation rules, sequential composition, branching and iteration.

Sandra Steinert devoted her PhD thesis to the topic.

There's also a Hoare logic for reasoning about the correctness of such programs.


You need to identify the lattices involved in each case.

Let $(\wp(S),\subseteq)$ be the lattice of all subsets of a set $S$ ordered by subset inclusion. A function $f:\wp(S) \to \wp(S)$ is monotone if for every pair of sets $x$ and $y$, if $x \subseteq y$ it also holds that $f(x) \subseteq f(y)$. The definition applies more generally to functions $f: L \to M$ between partially ordered sets $L$ and $M$.

Let $Stmt$ be the set of statements occurring in a program and let $(\wp(Stmt),\subseteq)$ be the lattice of subsets of statements ordered by subset inclusion. Let us assume for simplicity that a statement in $Stmt$ is either an assignment $x:= e$ or a Boolean expression $b$ (representing the entry of a conditional or head of a loop).

A control flow graph has the form $G = (Stmt,E)$ where $E$ is an edge relation over statements. The following definitions are extremely standard:

$succ: \wp(Stmt) \to \wp(Stmt)$ maps a set of statements to their successors.

$succ(X) = \{ y \in Stmt | \text{ there exists } x \text{ in } X \text{ such that } (x,y) \text{ is in } E\}$

$pred: \wp(Stmt) \to \wp(Stmt)$ maps a set of statements to their predecessors.

$pred(X) = \{ y \in Stmt | \text{ there exists } x \text{ in } X \text{ such that } (y,x) \text{ is in } E\}$

It is a standard exercise to show that these are monotone functions.

Consider the set $Exp$ of all arithmetic and Boolean expressions occurring in a program. The structure $(\wp(Exp),\subseteq)$ is a lattice with the subset inclusion order.

For the available expressions analysis, we can define two functions $Gen$ and $Kill$ in two steps as follows.

First define $Gen: Stmt \to \wp(Exp)$ as a function that maps a statement to the set of expressions generated by that statement. We can define $Gen$ inductively and lift it to sets as follows.

$Gen(x := e) = \{e\}$ and  $Gen(b) = \{b\}$

The lifted function $Gen: \wp(Stmt) \to \wp(Exp)$  is obtained in a standard manner by taking the union of $Gen$ sets for every statement in a given set.

$$ Gen(S) = \bigcup_{s \in S} Gen(s) $$

You can now ask whether this function is monotone.

A note about the slides

The slides you are studying do not contain sufficient information to deduce everything I have said here from first principles and I doubt they are meant to be read that way. I would consult the lecture notes or the section on data flow analysis in a  standard compilers textbook for a thorough treatment with complete definitions.


A boolean function $f: \{0,1\}^n \rightarrow \{0,1\}$ is chosen at random from all $2^{2^n}$ such $f$. What do the Fourier coefficients look like?

Here's one way of attacking the problem.
Any boolean function $f: [2]^n \rightarrow [2]$ can be written as
\begin{equation}
f(\alpha) = \sum_{\beta \in [2]^n} \chi_{\beta}\delta_{\beta} (\alpha)
\end{equation}
where $\chi_{\beta} \in [2]$ and $\delta_{\beta}$ is defined as
\begin{equation}
\delta_{\beta} (\alpha) = \begin{cases} 1 & \text{if } \alpha = \beta \\ 0 & \text{o.w.} \end{cases}.
\end{equation}
Choosing an $f$ at random is equivalent to independently and identically giving each $\chi_{\beta}$ the probability $p(\chi_{\beta} = i ) = 1/2$; i.e. each $\chi_{\beta}$ is an uniformly random i.i.d. binary random variable and $f$ is the sum of these random variables. The Fourier transform of this function is
\begin{equation}
 \widehat{f} (\gamma) = \frac{1}{2^n}\sum_{\alpha \in [2]^n} f(\alpha)e^{ \left\langle \gamma , \alpha \right\rangle  \pi i}
\end{equation}
where $ \left\langle \gamma , \alpha \right\rangle $ is the dot product in $\mathbb{F}^n_2$.
However, plugging in our previous definition/identity for $f$ we have that
\begin{equation}
 \widehat{f} (\gamma) = \frac{1}{2^n}\sum_{\alpha \in [2]^n} \sum_{\beta \in [2]^n} \chi_{\beta}\delta_{\beta} (\alpha)e^{ \left\langle \gamma , \alpha \right\rangle  \pi i} = \frac{1}{2^n}\sum_{\alpha \in [2]^n}  \chi_{\alpha} e^{ \left\langle \gamma , \alpha \right\rangle  \pi i};
\end{equation}
therefore the expected value of $\widehat{f}$ can be written as
\begin{equation}
 \mathbb{E}[\widehat{f} ]  = \frac{1}{2^n} \sum_{\gamma \in [2]^n} \widehat{f}(\gamma) = \frac{1}{2^n} \sum_{\gamma \in [2]^n} \left(\frac{1}{2^n}\sum_{\alpha \in [2]^n}  \chi_{\alpha} e^{ \left\langle \gamma , \alpha \right\rangle  \pi i}\right) \end{equation}
\begin{equation}
= \frac{1}{2^n} \sum_{\alpha \in [2]^n}  \chi_{\alpha} \left(\frac{1}{2^n}\sum_{\gamma \in [2]^n} e^{ \left\langle \gamma , \alpha \right\rangle  \pi i}\right) ;
\end{equation}
which we can simplify that as
\begin{equation}
 \mathbb{E}[\widehat{f} ]  = \sum_{\alpha \in [2]^n} \frac{\chi_{\alpha} }{2^n}  \mathbb{E}[ e^{ \left\langle \gamma , \alpha \right\rangle  \pi i}]  ;
\end{equation}
so that we can consider the subproblem $ \mathbb{E}[ e^{ \left\langle \gamma , \alpha \right\rangle  \pi i}] $ instead.
Now we use the following fact from combinatorics

Lemma $\mathcal{E}$=(The number of binary strings with even number of ones) = (The number of binary strings with odd number of ones)=$\mathcal{O}$
(Proof): Binary strings in $[2]^m$ are in 1-to-1 correspondence with subsets of $[m]$; but by the binomial theorem $(1-1)^m = \sum_{k} \binom{m}{k}(-1)^{k} = \mathcal{E} - \mathcal{O} = 0 $. QED

Therefore we have the following (if $\alpha \neq 0^n$)

Corrollary $e^{ \left\langle \gamma , \alpha \right\rangle  \pi i}$ is equal to 1 as often as it is equal to -1; i.e. $ \mathbb{E}[ e^{ \left\langle \gamma , \alpha \right\rangle  \pi i}] = 0 $
(Proof): If the support of the string $\alpha$ has $m$ 1's then we can break up the sum by the substrings on the support. In particular there are $[2]^{n-m}$ possible strings that are equal on the $[2]^m$ different strings on the support, then apply the previous lemma. QED

We, therefore, have that $ \mathbb{E}[\widehat{f} ]  = \sum_{\alpha \in [2]^n} \frac{\chi_{\alpha} }{2^n}  \mathbb{E}[ e^{ \left\langle \gamma , \alpha \right\rangle  \pi i}]  = 2^{-n}\chi_0 $ for any fixed $f$. Therefore $\mathbb{E}_{\chi}[\mathbb{E}_{\gamma }[\widehat{f} ]]=2^{-(n+1)}$ for a random $f$ or more simply put we have that:
For a random $f$ we have that the mean value of $\mathbb{E}[\widehat{f} ]$ is equal to $2^{-(n+1)}$.
If we wanted a more precise answer we could have gone an alternate route:
What is $p(\widehat{f} (\gamma)= i )$?
We can split this up into two sets like in the proof of the lemma; i.e.
\begin{equation}
\frac{1}{2^n}\sum_{\alpha \in [2]}\chi_{\alpha}e^{ \left\langle \gamma , \alpha \right\rangle  \pi i} = \frac{1}{2^n}\sum_{\alpha \in \mathcal{E} }\chi_{\alpha} - \frac{1}{2^n}\sum_{\alpha \in \mathcal{O} }\chi_{\alpha}
\end{equation}
But the $\chi_{\alpha}$ are i.i.d. and therefore this looks just like a random walk that is normalized by $2^{n}$.
The $\widehat{f} $ follows the binomial distribution of the form
\begin{equation}
p\left(\widehat{f} (\gamma)= \frac{i}{2^{n-1}} \right) =  \binom{2^n}{2^{n-1}+i}\frac{1}{2^n}
\end{equation}
if $\gamma \neq 0^n$;
i.e. the distribution on $\widehat{f} $ looks like what would happen if you took a binomial distribution on $[2^n]$ and shited it to the left by $2^{n-1}$ and then divided by $2^{n}$.


If I understand your question correctly you aren't looking for a tree, or an arborescence, but rather a minimum weight set of arcs that suffice to keep the graph strongly connected.

Your problem is NP-complete by reduction from Hamiltonian cycle problem. Given an input undirected graph that you wish to find the Hamiltonian cycle of create a directed graph by replacing each edge with a pair of oppositely directed arcs. Give all arcs weight 1. This directed graph has a set of arcs that leave the graph strongly connected with weight at most the number of vertices if and only if it has a Hamiltonian cycle.

You can get a two-approximation by picking an arbitrary root, finding the minimum weight spanning tree with arcs pointing towards the root, finding the minimum weight spanning tree with arcs pointing away from the root, and then unioning the two sets of arcs.

I don't recognize this problem off the top of my head but have you tried looking in the various NP-complete problem directories for it?


Does the existence of PH-complete problems relativize?

Yao showed, in 1985, that there exist oracles relative to which the Polynomial Hierarchy is infinite. Relative to such an oracle, there don't exist PH-complete problems.

Also, you are right that with a TQBF oracle, PH equals PSPACE. In fact, even P = PSPACE in the presence of a TQBF oracle.


Efficient algorithm for a particular graph closure property

I suggest you use a fixpoint algorithm, using a worklist implementation.  I'll start by providing an intuitive, English-language description of an algorithm for this problem; then a more formal presentation.

Intuitive algorithm. Basically, we'll apply the following closure rules to the graph as many times as possible, until they don't produce anything new:

If there is an edge $u\to v$ with clobber set $S$ and an edge $v\to w$ with clobber set $T$, then add an edge $u\to w$ with clobber set $S\cup T$.
If there is an edge $u \to v$ with clobber set $S$ and an edge $u \to v$ with clobber set $T$, where $S \subset T$, then remove the edge with clobber set $T$.

Intuitively, we'd like to keep applying these in all possible ways until the graph doesn't get any bigger; then you're done.  Note that I'm treating the graph as a multigraph, so there can be multiple edges between any pair of vertices.

In practice, you need to implement this carefully (you don't want to add an edge that would be immediately removed by the other closure rule).  So, here is an algorithm that applies the above idea, in a reasonable way:

Initially, mark all of the edges of the graph.
While there exists at least one marked edge:

a. Pick any marked edge; suppose it is $u \to v$ with clobber set $S$.  Remove the mark on this edge.

b. For each edge $v\to w$ with clobber set $T$, call $\text{MaybeAddEdge}(u,w,S\cup T)$.

Here the subroutine $\text{MaybeAddEdge}(u,v,S)$ is defined to do the following steps:

For each edge $u \to v$ with clobber set $T$:

a. If $T \subseteq S$, return immediately (without adding any edges).

b. If $S \subset T$, remove the edge with clobber set $T$.
Add an edge $u \to v$ with clobber set $S$, and mark it.

At the end of execution, after we've finished applying the closure rules, the set of clobber sets on all of the edges from $u$ to $v$ gives the set of minimal clobber sets for all paths from $u$ to $v$.  This is effectively a worklist/fixpoint algorithm, and it follows pretty directly from the problem statement.

If you prefer a more formal treatment of this problem, see below.

Notation. Let $V$ denote the set of variables.  Define a partial order $\mathcal{L}$ as follows: Consider the pre-order $(2^{2^V},\le)$, where an element $\ell \in 2^{2^V}$ is a set of clobber sets, and we define $\ell \le \ell'$ iff for every clobber set $S \in \ell$, there exists a clobber set $S' \in \ell'$ such that $S' \subseteq S$.  Now we can define the equivalence relation $\equiv$ by $\ell \equiv \ell'$ iff $\ell \le \ell'$ and $\ell' \le \ell$.  Modding out by $\equiv$ yields a partial order $(\mathcal{L},\le) = (2^{2^V},\le)/\equiv$.  In other words: every set $\ell \in 2^{2^V}$ of clobber sets is equivalent to one where there is no pair of sets $S,S' \in \ell$ such that $S \subset S'$ and $S\ne S'$ (if there is such a pair of sets, we can remove $S'$ from $\ell$ and get another equivalent set), so we let $\mathcal{L}$ denote the set of elements $\ell$ that are in this canonical form.

As it happens, $\mathcal{L}$ is a meet semi-lattice with a meet operation $\wedge$.  In particular, the join operation is defined by $\ell \vee \ell' \equiv \ell \cup \ell'$.    Let $\bot = \{2^V\}$ denote the bottom element in this lattice and $\top = \{\emptyset\}$ denote the top element.  Of course, if $S$ is a clobber set (i.e., $S \subseteq V$), then $\{S\}$ is a lattice element of $\mathcal{L}$ (corresponding to the single clobber set $S$).

Notice that a lattice element $\ell \in \mathcal{L}$ corresponds to a set of minimal clobber sets.  Thus, the lattice will be helpful for recording this kind of information as the algorithm progresses.

Define the binary operation $\circ$ by $\ell \circ \ell' \equiv \{S \cup S : S \in \ell, S' \in \ell'\}$.  Conceptually, this is going to represent the effect of concatenating two paths (where $\ell$ is the set of minimal clobber sets for some path $u\to v$ and $\ell'$ is the set for some path $v \to w$).

Approach.  We are going to build a 2-dimensional table $T[\cdot,\cdot]$.  At any point in the algorithm, for each pair of variables $u,v \in V$, $T[u,v]$ will hold an element of $\mathcal{L}$ that denotes an over-approximation of the desired set of minimal clobber sets for all paths from $u$ to $v$.

If $u,v \in V$ are variables, at the end of the algorithm $T[u,v]$ will contain the set of all minimal clobber sets for all paths from $u$ to $v$.  We'll find a least fixpoint for $T[\cdot,\cdot]$, subject to the following condition:

For all vertices $u$ and all edges $v\to w$ (with clobber set $S$), $T[u,v] \circ \{S\} \le T[u,w]$.
For all vertices $u$, $T[u,u] = \top$.

To find the least fixpoint, we'll use a standard worklist approach.

Algorithm. Let $W$ denote a set data structure that can hold pairs of vertices.  Then the algorithm is as follows:

Initialize $T[u,v] \gets \{S\}$ for each edge $u\to v$ with clobber set $S$ in the graph, $T[u,u] \gets \top$ for each vertex $v \in V$, and otherwise $T[u,v] \gets \bot$.  Initialize $W$ to contain the set of pairs $(u,v)$ such that there is an edge $u\to v$ in the graph together with the set of pairs $(u,u)$ such that $u$ is a vertex in the graph.
While $W \ne \emptyset$, do:

a. Pop an arbitrary vertex-pair $(u,v)$ from $W$.

b. For all edges $v \to w$ (with clobber set $S$) out of $v$, do:

Let $o \gets T[u,w]$. Set $T[u,w] \gets T[u,w] \vee (T[u,v] \circ \{S\})$.  If $o \le T[u,w]$, insert $(u,w)$ into $W$.

The final value of $T[\cdot,\cdot]$ will have the desired form (it is a minimal fixpoint subject to all of the conditions above), and thus will be a valid solution to your problem.  Each $T[u,v]$ contains the set of minimal clobber sets, taken over all paths from $u$ to $v$.

Notice that the above algorithm does not specify the order in which you pull items out of the worklist.  Good scheduling algorithms can improve the performance of this scheme.  One standard heuristic is to use reverse post-order (derived from a DFS on the graph) to prioritize which elements to pull out of the worklist.

Also note that the running time of this algorithm could be exponential, if your graph is unfortunate.  This is unavoidable: there might be exponentially many clobber sets, so the output size might be exponential in the size of the input in the worst case.


Are there specific examples of integral polyhedra that are neither Totally Unimodular nor Total Dual Integral?

I'm only going to talk about the constraint matrix part of the problem, I don't know much about the linear system (TDI) part.

Call a matrix $A$ good if $\{x|Ax\leq b,x\geq 0\}$ is a integral polytope for all integral $b$.
TUM is precisely the set of good integral matrices. This is a result by Hoffman and Kruskal. see this for how the theorem comes about and the original paper.

If we relax the requirement that $A$ is integral, then we get a larger class of matrices. Call a good matrix $A$ trivial, if it is a scaling of a TUM matrix (i.e. $A=\frac{1}{k}B$ for some TUM matrix $B$ and integer $k$).

Sadly, I don't know of any natural non-trivial good matrices.

But there is a characterization of good matrices. A matrix $A$ is $1$-regular if for all non-singular square submatrix $R$, $R^{-1}$ is integral. We have the following by Appa and Kotnyek.

  A rational matrix $A$ is good iff $A$ is $1$-regular.

Here is an example of a non-trivial good matrix.

$$\left(
\begin{array}{cc}
 \frac{1}{2} & -\frac{1}{2} \\
 -\frac{1}{2} & -\frac{1}{2} \\
\end{array}
\right)$$


First, a streaming algorithm running in space $s(n)$ for a problem $C$ implies a communication protocol for $C$ using $s(n)$ bits of communication: Alice, on input $x$, runs the streaming algorithm on $x$ and then hands the configuration of the machine at the end of the stream to Bob ($s(n)$ bits), and then Bob, who has input $y$, runs the streaming algorithm starting from the provided configuration, and returns the result. Therefore, communication lower bounds imply streaming lower bounds.

Second, consider the following problem, called INDEX: Alice gets an $n$-bit string $x$ and Bob gets an integer $i \in [n]$, and they want to determine value of the $i$th bit of $x$, $x_i$. I'll quote the following result, which can be proved using an information statistics argument.

Claim 1: Any randomized (1/3-error, say) protocol for INDEX requires $\Omega(n)$ communication.

Now we can reduce from INDEX to the triangle-free problem. In particular, given and instance $(x, i)$ of INDEX we can build edge sets $E_A$ and $E_B$ over $V = L \cup R \cup \{s\}$ where $L = \{y_1, ..., y_{\sqrt{n}}\}$, $R = \{z_1, ..., z_{\sqrt{n}}\}$, and $s$ some constant node (so $2\sqrt{n} + 1 = O(\sqrt{n})$ nodes) with the property that the resulting graph $G$ is triangle-free iff $x_i = 1$. Additionally, Alice can compute $E_A$ herself and Bob can compute $E_B$ himself. To do this, pick some pairing function $p: [n] \to [\sqrt{n}] \times [\sqrt{n}]$ and say $p_L(k)$ is the first element in the pair corresponding to $p(k)$ and $p_R(k)$ is the second. We'll use this to map bit positions to edges. Then let $E_A = \{(y_{p_L(k)}, z_{p_R(k)})\ |\ x_k = 1\}$. Note that this is a bipartite graph. Now let $E_B = \{(s, y_{p_L(i)}), (s, z_{p_R(i)})\}$. $E_A$ has no triangles, and $E_B$ forms a triangle with $E_A$ only when theres an edge between $y_{p_L(i)}$ and $z_{p_R(i)}$, which only happens when $x_i = 1$.

An $o(n^2)$ communication-protocol for determining if a graph is triangle-free readily contradicts the INDEX lower bound: Alice gets $x$ and Bob gets $i$. Alice and Bob compute $E_A$ and $E_B$ respectively with no communication. They use the triangle-free protocol as a subroutine, using $o(\sqrt{n}^2) = o(n)$ communication.


(Cryptographic) problems solvable in a polynomial number of arithmetic steps

I did not read the paper as well but the abstract seems to say that an exponenial number of bit operations are required.

Chebyshev's work on congruences and its reformulation in the AKS algorithm show that prime generation is in P. Therefore trial division yields non-trivial factors. In that case, for some number N, you can expect a density of primes of 1/ln(N).

Furthermore, you can have a look at Turing's 1937 PhD thesis on the subject.


This was conjectured by R. Jozsa in Section 8 of arXiv:quant-ph/0508124. If you are already familiar with quantum computing and quantum complexity theory, you can start by reading that section.

An important reading is arXiv:quant-ph/0006004, where Cleve and Watrous show that Shor's algorithm is in that class.


What parts of homotopy type theory are not possible in Agda or Coq?

If you look at Notes on Chapter 8 you will see what has already been formalized, and I think that's a lot. There are the Coq HoTT library and the Agda HoTT-Agda library which formalize large chunks of Homotopy Type Theory.

To get things done in Coq we needed a special version of Coq that was patched just for the purposes of HoTT. However, Coq is moving in the direction of supporting homotopy type theory, so before long we might be able to do it with standard Coq.

In Agda one has to turn on the --without-K option, otherwise Agda thinks all types are 0-types. There are some lingering doubts as to whether --without-K really gets rid of the assumption that everything is a 0-set, or perhaps one could reintroduce it into Agda with tricky uses of pattern matches.

The following aspects of Coq and Agda formalizations are not satisfactory:

The Univalence axiom is stated as a hypothesis. It would be better if it were built into the system. In particular we would like Coq and Agda to understand the computation rules about the Univalence axiom.
Likewise, we have to use hacks to get workable higher-inductive types. Again, it would be better to have direct support.

The trouble with the above deficiencies is that nobody knows how to fix them even in theory. This is an active area of research.

Other than that, I think it's fair to say that HoTT can be mostly done in Coq and Agda, just not in the optimal way.


Is there an expressiveness hierarchy for type systems?

There are several senses of "expressiveness" that you might want for a type system.

What mathematical functions can you express in a particular type system.  For example, in the simply typed lambda calculus, not all computable functions can be expressed.  The same is true of System $F$, but strictly more functions can be expressed.  This is not very interesting once you get to type systems for Turing-complete languages.
Can system $A$ typecheck every program written in system $B$.  This is basically what cody's first notion of strength is about for PTSs.  Again, System $F$ is stronger than the STLC in this ordering, since every STLC program types in System $F$.  Similarly, a system with subtyping will be stronger than a system without.
Are there local transformations (in the sense of Felleisen's paper On the expressive power of programming languages) that allow a program that types in system $A$ to type in system $B$, but not vice versa.
Does one type system guarantee stronger properties than another.  For example, linear type systems just reject more programs, but that allows them to make stronger statements about the programs they do accept.

Unfortunately, I don't believe that there's been work on categorizing or formalizing these notions, with the exception of Barendregt's lambda-cube, as @cody discusses.


Practically speaking, what are examples of languages or grammars that regex can always parse successfully?

A short answer is: Probably nothing that you call a language.

In theoretical computer science (TCS), a language simply means a set of words.  But in most cases, what people call a “language” outside TCS has some recursive structure.  “Recursive structure” is ambiguous here, but intuitively regular expressions cannot parse them because regular expressions even cannot parse balanced parentheses.

Many compilers use regular expressions for lexical analysis before parsing.  For example, you can decide whether a certain string is a valid identifier in C++ or not by using a regular expression.  This is possible because the language consisting of valid identifiers in C++ is a regular language.  But the set of valid C++ identifiers is usually not called a language outside TCS.

Disclaimers:

Some people distinguish “regular expression” and “regex.”  In this answer, I am talking about regular expressions, not regexes, if we use this convention.
Actual C++ compilers do not probably use a regular expression for valid identifiers because excluding keywords makes the regular expression unmanageable.  They use a different technique to cope with this, but that is not the main point here.


Can the Banach-Tarski paradox be "realized" by floating-point round-off?

This seems to have little to do with Banach-Tarski.
In your setting, f is simply not an isometry due to floating-point errors, and in particular there must be a single piece $i$ such that $\mathrm{Vol}(f(P_i))>\mathrm{Vol}(P_i)$, so no need to cut into several pieces.

Banach-Tarski works because the notion of volume is not well-defined on the pieces. This clashes with your requirement that the pieces are defined by "a finite amount of geometric data", and with your writing of $\mathrm{Vol}(P_1)+\dots+\mathrm{Vol}(P_n)$.


Standard Name for a vertex removal like operation

This operation is called vertex elimination. See for example: "Triangulated Graphs and the Elimination Process", by Rose (1970).
This type of operation is well-studied, among others, in the context of chordal graphs (see Wikipedia entry about perfect elimination orderings). A related problem of finding an optimal ordering for applying this operation is called Minimum Fill-in.


Can Suffix trees be used to find all common substrings?

Yes, suffix trees can be used to find all common substrings. I would say to use a suffix array instead, but if you already have a suffix tree, building a suffix array from a suffix tree takes linear time by DFS. So the rest of my answer will assume we are working with a suffix array.

Given a text $S = s_1 , ..., s_n$, a suffix array for $S$ is an array of integers of range $0$ to $n$ specifying the lexicographic ordering of the $n+1$ suffixes of the string $S$\$

We want to couple the suffix array with the $LCPs$, the longest common prefixes. We can construct the array of $LCPs$ in linear time as mentioned in the paper by Kasai et al. Suffix arrays and their lcp arrays line up together in a way that given an index into the lcp array say $lcp[k]$ where $k$ is the index number, then $sa[k]$ will be the start of one instance of the common substring and $sa[k-1]$ will be the start index of the second instance. The length is of course the value in the lcp array.


Matrix Coloring under Vertical and Horizontal Constraints

A1) The problem remains NP-complete even for fixed $|\Sigma|=3$

A reduction from planar 1-3-SAT is the following; suppose $\Sigma = \{0,1,2\}$

use a sequence of $M_{ij} = \{0,1\}$ pairs of horizontal/vertical cells as "wire" gadgets to "carry" the truth values ($0=true$, $1,2 = false$) of the variables (the horizontal and vertical rules of the wires forbid switching between $true \leftrightarrow false$)
the beginning of a wire acts as "variable assignment"
the clauses are simulated using a circular pattern in which the horizontal and vertical rules force a sequence of $012\;012....$ along the circuit
each clause has 3 incoming wires; the wires are arranged to "touch" the circuit in three distinct places modulo 3; in this way only one of the three wires can have the value of true.

The following figure should be self-explanatory.

If instead of "local" horizontal/vertical rules you want to use "global" rules (a set of rules that are common to all cells) then you must add another extra "blank" color to "isolate" the wires and the reduction above still holds.

With $|\Sigma| = 2$ the problem is polynomial time solvable (each cell is represented with a binary variable, and the rules can be expressed with a 2-SAT formula).

A2) The game is also very similar to a "relaxed" version of the game Binary Puzzle: a puzzle game played on a $n \times n$ grid. Intially some of the cells contain a zero or a one; the aim of the game is to fill the empty cells according to the following rules:

Each cell should contain a zero or a one and no more than two similar numbers next to or below each other are allowed
Each row and each column should contain an equal number of zeros and ones
Each row is unique and each column is unique

Using a set of eight colors you can "simulate" the rule #1 of binary puzzle (which is NPC even without rules #2 and #3 ). This is a quick idea for a reduction.

Each one of the eight colors has 3 bits $b_0b_1b_2$;

bit 0 $b_0$ represents the $0$ or $1$ of the binary puzzle grid
bit 1 $b_1$ is $1$ if and only if the cell on the left has the same color
bit 2 $b_2$ is $1$ if and only if the cell above has the same color

If a cell $i,j$ of the initial board of binary puzzle is empty then you set $M_{ij} = \Sigma$

If a cell $i,j$ of the initial board of binary puzzle is a forced $1$ then you set $M_{ij} = \{ 1** \}$ (100,101,110,111)

If a cell $i,j$ of the initial board of binary puzzle is a forced $0$ then you set $M_{ij} = \{ 0** \}$ (000,001,010,011)

The horizontal rules are:

00* -> 01*  : allow another 0 on the right only if the previous was 1
0** -> 1**  : always allow a 0->1 transition
10* -> 11*  : allow another 1 on the right only if the previous was 0
1** -> 0**  : always allow a 1->0 transition

The vertical rules are:

0*0 -> 0*1  : allow another 0 below only if the above one was 1
0** -> 1**  : always allow a 0->1 transition
1*0 -> 1*1  : allow another 1 below only if the above one was 0
1** -> 0**  : always allow a 1->0 transition

You can find the proof of NP-completeness of binary puzzle on my blog (soon or later I'll find the time to submit it somewhere).

A3) Furthermore if you add the constraint that each color can be used only once, then the problem is still NPC even on $n \times 1$ grids with only horizontal constraints.

The reduction is from 3-PARTITION which is strongly NPC: given a set $X = \{x_1, ..., x_{3q}\}$ and a target sum $B = (\sum x_i)/3$; use (new) colors $c^i_1,...,c^i_i$ for each $x_i$. Start with a grid $G$ of length $Bq+q + 1$ with  the following sets of allowed colors:

$S E^B T_1 E^B T...E^B T_q$

Where

$S$ (the set $M_1$) represents the starting color $\{ c_S \}$
$T_i$ represents a breaking block that contain $q$ special colors $\{ c_{Ti} \}$
$E^B$ is a sequence of $B$ "blocks" that can contain any color from $\Sigma \setminus \{ c_S, c_{Ti}\}$

The horizontal constraints are:

$(S,c^i_1)$ for $i = 1...n$: that allows to start from $S$ and start using a color sequence from $c^i$
$(c^i_j, c^i_{j+1})$ for $j = 1...i-1$: that forces the complete color sequence of each $c^i$ (once started)
$(c^i_i, c^j_1)$ for $i \neq j$ that allows to start another color sequence once ended the previous one
$(c^i_i, c_{Tj})$ for $i = 1...n, j=1..q-1$: that "align" the color sequences to the break blocks (that guarantee that the "unary" sum is equal to $B$)
$(c_{Tj}, c^i_1, )$ for $i = 1...n, j=1..q-1$: that allows another color sequence after a breaking block $T_j$

The $n \times 1$ grid $G$ can be properly colored if and only if the original 3-PARTITION problem has a solution.

This is an example: given the 3-PARTITION instance:

$A = \{ 3,3,2,2,2,2 \}\; (B=7, q=2)$

We can use $2B + 2$ distinct colors and build a coloring game instance on a $2B + 2 + 1 = 17 \times 1$ grid like in the figure.


Is there a theory of computation that takes failure and decay of the computation substrate into account?

I'm not 100% sure what the question is about, but the title seems to ask about computation that allows failure. There is a lot of work on noisy (erroneous) computation in the sense that I think you are asking about. I don't have time to give a complete overview, but here are some pointers that may be of interest.

Distributed systems. This is probably by far the most developed field because the very definition of a distributed system is based on the possibility of (partial) faults. There are elaborate theories of DS depending on the chosen fault model, e.g. fail/stop or byzantine failure. See also the work on failure detectors.
Cryptography. This may seem a bit bizarre, but I think much of the field of cryptography can be seen as a form of extreme failure, with the adversary trying to undermine (in a general sense) the working of the system. You can think of the usual polynomially bound attacker as an case of failure model. This lead to things like secure multi-party computation as an algorithmic tool in the face of extreme adversity.
π-calculus: see (1) for a generalisation of Shannon-style information theory to interacting processes. I think the error model in (1) is unrealistic, because it does not cater for the situation where an error converts a free into a bound name or vice versa.
Turing machines: see (2, 3, 4).
Cellular automata: various researchers have added failure models, sorry no references at the moment, maybe look at work by  P. Gacs.
λ-calculus: see (6).
Assembly language: see (5, 7).
Quantum computation: is all about error correction, I'm not qualified to say more on this.
An increasingly important subfield of computation is the use of probabilistic process calculi to model chemical reactions. Have a look at Luca Cardelli's recent work.

Note also that this line of thinking is very old: J. von Neumann wrote about this in 1956 [8]. Maybe even more impressive C.-A. Petri invented Petri-nets in August 1939 at the age of 13 for the purpose of describing chemical processes.

M. Ying, Pi-Calculus With Noisy Channels.
I. Capuni, P. Gacs, A Turing Machine Resisting Isolated Bursts Of Faults.
I. Capuni, Fault-tolerant Turing Machine.
E. Asarin, P. Collins, Noisy Turing Machines.
J. Chang, G. A. Reis, D. I. August, Automatic Instruction-Level Software-Only Recovery.
D. Walker, L. Mackey, J. Ligatti, G. A. Reis, D. I. August, Static Typing for a Faulty Lambda Calculus.
F. Perry, L. Mackey, G. Reis, J. Ligatti, D. I. August, D. Walker, Fault-tolerant Typed Assembly Language.
J. von Neumann, Lectures on Probabilistic Logics and the Synthesis of Reliable Organisms From Unreliable Components.


There are many ways to define the semantics of a program. If we consider operational semantics, a simple imperative program defines a relation $R \subseteq \mathit{State}\times \mathit{State}$. I'm using "simple imperative" here to mean something that does not modify itself. There is a standard way to view $R$ as a function $\wp(\mathit{State}) \to \wp(\mathit{State})$ that maps a set of states to their successors in $R$.

If a program can modify itself you can consider a pair $\wp(\mathit{State})\times(\wp(\mathit{State})\to \wp(\mathit{State}))$, in which each element $(S,F)$ represents a current set of states in $S$ and a transformer $F$ representing the behaviour of the program. A program of the form you describe can modify either $S$ or $F$.

You may find the following paper useful.

  Multi-Stage Programs are Generalized Arrows, Adam Megacz.

If you are interested in a formalisation oriented towards automatic analysis of such programs, the following paper may interest you.

  Modelling Metamorphism by Abstract Interpretation, Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray, Kevin Coogan, Gregg M. Townsend


How to define the _regret_ in multiagent systems? Any good definition please?

It does appear to be a mistake in this pdf version of the book, where the authors are dealing with rewards: The regret should be the reward that would have been gained for playing s minus the actual gain.

Note that often this is set up with losses (rather than rewards) so that the regret would be the incurred loss minus the loss that would have been incurred under some pure strategy.

For a given pure strategy s, the regret for not having played s should be 0 if one's choice gave the same payoff as s, positive if it was worse (i.e., lower in a rewards setting, higher in a losses setting) than s, and negative if it was better than s.

Commonly one defines the regret as the regret for not having played the best pure strategy (given the choices of others). This will be non-negative, and 0 if and only if the current choice is optimal.


Vehicle routing problem over Manhattan distances

The Hamiltonian cycle problem on grid graphs (a node induced subgraph of the infinite grid) is NP-complete.

To prove NP-hardness of $VRP$ on grid graphs you can use a direct reduction: given a grid graph $G = (V, E)$ with $|V|= n$ nodes, it easy to see that it has an hamiltonian cycle if and only if the corresponding Vehicle Routing Problem on grid graphs (all edges have cost 1) has a solution with total cost $\leq n$. The weighted edges case is a generalization, so the reduction is immediate:

HAM CYCLE on grid graphs (NP-complete) $\leq$ VRP on grid graphs with cost 1 edges $\leq$ VRP on grid graphs with weighted edges.

EDIT:
Other stuff: Euclidian (planar) TSP is NP-complete (see Hamilton paths in grid graphs), from this result it follows that TSP with distances measured in Manhattan norm is NP-complete, too (see for example this survey). VRP on grid graphs with weighted edegs is a generalization of it.

But if we consider VRP on solid grid graphs (no holes allowed) I suspect that the problem is open because it is directly connected to this: "Problem 54: Traveling Salesman Problem in Solid Grid Graphs"


How close can we get to linear multiply, add, and compare (on integers)?

Probably not the best answer, but perhaps this is a useful starting point. If we wish to represent a non-negative integer, we can store it as a set of residues modulo sequential prime numbers starting from 2. In this form comparison is potentially hard, but multiplication and addition can be done pretty quickly. The product of the first $n$ primes is approximated by $$p_n\# =\exp((1+\mathcal{o}(1) )n\log n).$$
Hence to represent an integer $N$ you require residues modulo the first $n$ primes, where $N<\exp((1+\mathcal{o}(1) )n\log n)$. Since we can represent any $N<p_n\#$ using residues modulo the first $n$ prime residues, we can take $n \log n \propto \log(N)$. Addition and multiplication can be done directly between pairs of residues. There are $n$ such pairs, with the maximum prime being around $n\log(n)$. Thus addition should be in $O(n\log\log(N))$, while multiplication via Schonhage-Strassen should be in $O(n\log\log(N)\log\log\log\log(N)\log\log\log(N))$. Since $n \log n \propto \log N$, then a rough approximation gives $n$ in $O(\log N/\log\log N)$. This would give the complexity of addition and multiplication as approximately $O(\log N)$ and $O(\log N \log\log\log N \log\log\log\log N)$.


Maybe the keyword you are looking for is "Implicit Complexity". It is more general than Curry-Howard correspondence, but several lines of research investigate along the axis you are interested in. You can check for instance the publications of Patrick Baillot for many references and pointers.
For a little self-promotion, here are for instance two recent papers [KPP1,KPP2] characterizing via the Curry-Howard correspondence on certain cyclic proofs the following complexity classes, depending on the logical rules incorporated or not in the cyclic proof system:

Regular languages (no contraction, no cut) [KPP1]
DLogSpace (contraction, no cut) [KPP1]
Primitive recursive functions (cut, no contraction) [KPP2]
Gödel's System T (cut, contraction) [KPP2]

[KPP1] Cyclic Proofs and Jumping Automata. Kuperberg, Pinault, Pous, FSTTCS 2019
[KPP2] Cyclic Proofs, System T and the power of Contraction. Kuperberg, Pinault, Pous, POPL 2021


Subspace-evasive set performance in the random case

Here's a quick calculation.

For a fixed affine subspace $H$ of dimension $k$, the probability that a random point falls in  $H$ is $1/q^{n-k}$. The probability that at least $c$ points in $S$ fall in $H$ is at most:
$${q^{(1-\epsilon)n} \choose c} \cdot \frac{1}{q^{(n-k)c}}\leq
 \frac{q^{(n-\epsilon n) c}}{q^{(n-k)c}} = \frac{1}{q^{(\epsilon n -k)c}}$$
A trivial bound on the number of subspaces of dimension $k$ is $q^{n(k+1)} < q^{2kn}$. So, by the union bound, the probability that there exists a subspace $H$ containing at least $c$ points of $S$ is at most:
$$q^{2nk} \cdot \frac{1}{q^{(\epsilon n -k)c}} < 1$$
if $c = 4k/\epsilon$ and $k<\epsilon n/3$.


If you want to include a fixpoint combinator in the language, you don't need to change anything to the syntax of types or the rules to type existing expressions. All it takes is adding one constant, a rule to type it and a rule to reduce expressions containing it:
$$
  \dfrac{}{\mathsf{fix} : (\tau \rightarrow \tau) \rightarrow \tau} \qquad
  \mathsf{fix} \, f \to f (\mathsf{fix} f)
$$

If you want to be able to define a fixpoint combinator in terms of the core lambda-calculus syntax, that's a different matter. There are a lot of type systems, some of them allowing arbitrary recursion, some of them not. There isn't a simple way of telling by looking at a type system whether it allows arbitrary recursion. For example, some very sophisticated type systems (e.g. the calculus of inductive constructions which Coq is based on) include a $\mathsf{fix}$ combinator with a typing rule that limits the types at which it can be used in such a way that only terminating functions can be defined. Here are a few ways arbitrary recursion can be added to a typed lambda calculus:

Intersection types: they allow any lambda-term to be typed, in a way that you can read from the type whether the term is strongly normalizing and whether it has a normal form. See Does there exist a Turing complete typed lambda calculus?
If you add (sufficient) recursion to the type language, this adds recursion to the term language as well. In ML, this leads to a recursive function definition without using let rec, by relying instead on a type definition of the form type t = Constructor of (t -> …).
The typing rules for ML-like languages are based on defining a typing rule for let rec that allows the variable to be used in its own definition. This makes let rec not syntactic sugar for a lambda-expression, unlike plain let.

The need to write let rec in ML is unrelated, or at least only loosely related, to the type theory. Here are a few reasons to annotate recursive definitions differently:

ML started out as the metalanguage for a theorem prover, and the designers may have felt that it was best programming practice to explicitly mention the use of unbounded recursion (which has the potential to make the proof building process not terminate).
Having the rec indication can make compiler design and type theory design slightly simpler, because there are cases where let can have a more generalizable type than let rec, and different kinds of terms that can or cannot be defined recursively.
There are cases where it's useful in programs to have a non-recursive let, which defines a new variable of the same name as an existing one: when an object undergoes a series of transformation, but they're intuitively different stages of the same object.

let widget = read_widget_source () in
let widget = parse_widget widget in
let widget = compile_widget widget in
execute_widget widget


Minimizing the maximum dot product among k unit vectors in an n-dimensional space

Answer: $\alpha = - 1/(k-1)$. This value is attained when vectors $v_i$ are the vertices of a regular simplex, centered at the origin.

This follows from symmetry: given a set of vectors $u_i$ consider new vectors $u_i'= \frac{1}{\sqrt{k}}\left( u_i \oplus u_{i+1} \oplus \dots \oplus u_{i-1} \right)$ (where we add up all vectors $u_i$ in the cyclic order starting from $u_i$). It is easy to show that vectors $u'_i$ form a better (or equal) solution than vectors $u_i$, and that vectors $u_i$ are vertices of a regular simplex (not necessarily centered at $0$). Symmetry arguments (like this one) are very useful in general for finding extreme configurations of vectors. In this case, it is very easy to find the value of $\alpha$ directly.

I. Let us first prove that $\alpha \geq -\frac{1}{k-1}$. We have,
$$0 \leq \|v_1 + \dots + v_k\|^2 = \sum_i \|v_i\|^2 + 2\sum_{i < j} v_i \cdot v_j \leq \sum_i 1 + 2\sum_{i<j} \alpha = k + k(k-1) \alpha.$$
We get that $\alpha \geq - 1/(k-1)$.

II. Now we prove that  $\alpha \leq -\frac{1}{k-1}$. Consider a $k\times k$ matrix $A = (a_{ij})$ with $a_{ii} = 1$ and $a_{ij} = {-1/(k-1)}$ for $i\neq j$. This matrix is (non-strictly) diagonally dominant and thus is positive semidefinite. (Note also that $A$ is the normalized Laplacian matrix of $K_k$.) Therefore, there exist a set of vectors $v_i$ with $v_i \cdot v_j = a_{ij}$. We get that
$$\alpha \leq \max_{i\neq j} a_{ij}  = -1/(k-1).$$

We proved that $\alpha = -1/(k-1)$. Note that vectors $v_i$ are vertices of a regular simplex since the distance $\|v_i - v_j\| = \sqrt{2- 2v_i \cdot v_j} = \sqrt{2k/(k-1)}$ is the same for all pairs $i,j$ (where $i\neq j$), and $\sum v_i =0$ since $\|\sum v_i\|^2 = 0$.

What we computed equals
$$-\frac1{\vartheta(\text{empty graph on } k \text{ vertices})-1},$$
where $\vartheta$ is the  Lovász Theta Function;
see the Wikipedia article on the Lovász Theta Function for details.


If I naively generalize the homeomorphic embedding relation for labeled finite trees in this way, do I still have a wqo?

Here's a nice property of WQOs:

  If $R$ is a WQO on terms, and $S$ is another transitive relation such that
  $$ R\ \subseteq\ S$$
  Then $S$ is a WQO

Proof: Let $t_1,\ldots, t_n,\ldots$ be an infinite sequence of terms. Because $R$ is a WQO, there are $i, j$ with $i<j$ such that $t_i\ R\ t_j$. But this implies $t_i\ S\ t_j$, so $S$ is a WQO as well.

This (somewhat counter-intuitive) result means you can always make your relation more permissive while preserving the WQO property.


The problem you describe is a generalization of the equal flow problem first proposed by Sahni.  In addition to the flow network, the input specifies several disjoint sets $R_1, R_2, \dots, R_k$ of arcs; the goal is to find a maximum flow such that for each $i$, all arcs in $R_i$ have the same flow value.

While the fractional version of the equal flow problem can be solved in polynomial time by linear programming, the integer version is NP-hard, even if the capacity of each arc is $1$ and all arcs in each set $R_i$ leave the same vertex $v_i$.  Worse, Meyers and Schulz recently proved that there is no polynomial-time $2^{n(1-\epsilon)}$-approximation algorithm, for any fixed $\epsilon>0$, unless $P=NP$.  (The integrality gap of the fractional LP can be arbitrarily large.)

Carol Meyers and Andreas Schulz.  Integer equal flows.  Operations Research Letters 37(4):245-249, 2009.


Are there subexponential algorithms for PLANAR SAT known?

Well, you can apply the planar separator theorem together with dynamic programming and get running time $2^{O(\sqrt{n})}$, where $n$ is the number of vertices in the graph. The idea being that you try all possible assignments for the variable vertices on the separator, and all variables mentioned in clauses in the separator (assuming each clause has a constnat number of variables).

If a clause node is large, then you have to be a bit more clever - you have to guess whether to assign it to the left side or right side subproblem. The details for such things tends to be messy and not immediate, so I am not going to give more details. I think the original papers by Lipton and Tarjan solved similar problems using similar ideas, if my memory serves me right.


Generating graphs of girth $g$ such that the minimum cycles form a double edge cover

My half-baked idea was a little too ambitious.  I'm including it below for reference, but the distance condition I specified is not actually sufficient to guarantee large girth.

There are arbitrarily large highly symmetric surface maps with large girth, but published existence proofs are largely based on group theory rather than topology or geometry per se.

Specifically, for any integers $g$, $d$, and $r$ such that $1/g + 1/d < 1/2$, there is a regular surface map in which every face has $g$ edges, every vertex has degree $d$, and every non-contractible cycle on the surface crosses at least $r$ edges.  Here "regular" means both that every vertex has the same degree and that for any pair of directed edges, there is an automorphism of the embedding that sends directed edge to the other.  Setting $r$ large enough in this construction guarantees that the girth of the graph is $g$.  See, for example:

Roman Nedela and Martin Škoviera.  Regular maps on surfaces with large planar width.  European J. Combinatorics 22(2):243--262, 2001.
Jozef Širáň.  Triangle group representations and constructions of regular maps. Proc. London Math. Soc. 82(3):513-532, 2001.

Once you have one such surface map, larger maps with the same girth and degree can be generated by constructing covering spaces.

Here is one (half-baked) way to generate such graphs. Let $G$ be a plane graph with the following properties:

Every bounded face of $G$ has exactly $g$ edges.
The outer face of $G$ has an even number of edges; call these the boundary edges of $G$.   (This condition holds automatically when $g$ is even; if $g$ is odd, $G$ must have an even number of bounded faces.)
It is possible to pair the boundary edges of $G$, so that the distance in $G$ from any boundary edge to its partner is at least $g$.  This condition is not actually enough; the exact condition needed here is unclear.

Arbitrarily large plane graphs with these properties can be constructed by taking a sufficiently large finite portion of a regular tiling of the hyperbolic plane by $g$-gons.

Finally, to obtain a surface graph $G'$ where every face has length $g$, identify pairs of boundary edges in $G$ according to the pairing described above.  The bounded faces of $G$ become the faces of a cellular embedding of $G'$ on some closed surface without boundary.  The distance condition on the pairing guarantees that the girth of $G'$ is $g$.

By choosing both $G$ and the pairing more carefully, once can construct arbitrarily large $d$-regular graphs satisfying your girth condition, for any integers $d$ and $g$ such that $1/d + 1/g < 1/2$.  Even within these constraints, the construction has lots of degrees of freedom.


Is it decidable that a computable analytic function over $\mathbb{R,C} ,$ equals $0$

No, it is not decidable. A good heuristic to answer such questions is the following: every computable map is continuous. If you could decide whether $f(x) = 0$ for all $x \in \mathbb{C}$, then the characteristic map $d$ of such a decision procedure, namely
$$d : f \mapsto \begin{cases}
1 & \text{if $\forall x \in \mathbb{C} . f(x) = 0$}\\
0 & \text{otherwise}
\end{cases}
$$
would be a non-constant computable map from the vector space of all such functions to the discrete space $\{0,1\}$, but such a map is discontinuous. By the same reasoning you cannot even decide whether $f(x) = 0$ at a single given $x \in \mathbb{C}$. And for the same reason still it is impossible to decide whether $y = 0$ where $y \in \mathbb{R}$.

A similar heuristic in a slightly different form: computable maps are continuous, therefore in any computable procedure a small perturbation of the input must create only a small perturbation of the output. From this you can see immediately that the map which takes $f$ to one of its roots (assuming $f$ has one) is not computable, because it is easy to make roots jump around wildly with arbitrarily small perturbations of $f$. (This heuristic would not work if you know someting extra about $f$, for instance if you are guaranteed that it is an odd-degree polynomial).

Of course, you need to know what topology to put on the vector space, but as a heuristic it is good enough to just imagine "the usual" topology, whatever that is. (There are theorems in computable analysis which say that an admissible representation of a separable metric space gives induces the metric topology, so the heuristic is pretty safe.)


Has a proof checker bug ever invalidated a major proof?

To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted.

As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up in these systems (though usually not silently, as Andrej suggests), and the fix to that bug involves some changes to existing proofs, or, more likely, of the standard library of the proof system involved.

Some examples of such library breaking proofs in Coq:

https://coq.inria.fr/bugs/show_bug.cgi?id=4294

https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html

It's hard to say whether the established proofs depended on the inconsistency, since after the fix, they required minor tweaks to be accepted by the proof checker. But this happens at each non-trivial update!

My personal opinion is that such mistakes are unlikely to happen, since the paper proof needs to be well polished before machine formalization can even be attempted.

Inconsistencies in proof frameworks usually require the heavy use of strange combinations of esoteric features, and so very rarely crop up "by accident".


Approximating distributions from samples

I think it's a simple application of Hoeffding's inequality. Using your notation, let $Q_i = \frac1m C_i$, i.e. $Q$ is the empirical distribution that approximates $P$. The total variation distance between $P$ and $Q$, i.e. half the $\ell_1$ distance, is
$$
\max_{S \subseteq [n]} \left| \sum_{i \in S}{P_i} - \sum_{i \in S}{Q_i}\right|.
$$

Let $P(S):= \sum_{i \in S}{P_i}$ and define $Q(S)$ analogously. The expectation of $Q(S)$ is $P(S)$ and by Hoeffding,
$$
\mathbb{P}(|Q(S) - P(S)| > \epsilon) \leq 2e^{-\epsilon^2 m}
$$

If we take $m$ a large enough multiple of $n/\epsilon^2$, we have that $\mathbb{P}(|Q(S) - P(S)| > \epsilon) < 2^{-n}/3$ and by a union bound

$$
\mathbb{P}(\max_S |Q(S) - P(S)| > \epsilon) < 1/3.
$$
So with probability at least 2/3, the total variation distance is at most $\epsilon$.


What is the complexity of minimum weight odd T-join?

Geelen and Kapadia appear to have a randomized algorithm for this problem.
http://arxiv.org/abs/1504.07647


Algorithm for Max Network Flow with lower bounds and its complexity

http://jeffe.cs.illinois.edu/teaching/algorithms/notes/25-maxflowext.pdf

There's a very simple reduction from that problem to the maximum flow problem. This is simply called "maximum flow with edge demands".


As @TsuyoshiIto suggests, there is an $O(n\log n)$-time algorithm for this problem, due to Edelsbrunner and Preparata.  In fact, their algorithm finds a convex polygon with the minimum possible number of edges that separates the two point sets.  They also prove an $\Omega(n\log n)$ lower bound for the more general problem in the algebraic decision tree model; however, it's not clear whether this lower bound applies to the triangle case.

A full description of the algorithm is too long to post here, but here's the basic idea.  Let $C$ be the convex hull of the positive points.  For each negative point $q$, consider the lines through $q$ that are tangent to $C$.  These lines split the plane into four wedges, one of which contains $C$; let $W(q)$ be the wedge opposite the one that contains $C$.  Finally, let $F$ (the "forbidden region") be the union of all wedges $W(q)$.  Any separating triangle must separate $C$ from $F$.  Both $C$ and $F$ can be constructed in $O(n\log n)$ time.

Label the edges of $F$ alternately clockwise and counterclockwise.  Edelsbrunner and Preparata further prove that if a separating triangle exists, then there is a separating triangle whose edges are collinear with clockwise edges of $F$.  In $O(n)$ additional time, we can find the (necessarily clockwise) edge of $F$ first hit by a ray from each clockwise edge $e$; call this edge the "successor" of $e$.  The successor pointers partition the clockwise edges into cycles; if there is a separating triangle, one of these successor cycles has length 3 (and none have length more than 4).

See the original paper for more details:

Herbert Edelsbrunner and Franco P. Preparata.  Minimum polygonal separation.  Information and Computation 77(3):218–232, 1988.


Detecting circuit that's similar in functionality and implementation

This is only an extended comment that came to my mind immediately after reading the question:

suppose you have a 3SAT formula $\phi$ with $n$ variables $x_1,...,x_n$ and let $C$ be the corresponding circuit;
build a new circuit $C'$, adding $m = n^k$ variables $y_1, y_2, ...,y_{n^k}$, and enough gates to AND the $m$ new variables with the output of the original $C$ ($C' = \phi \land y_1 \land ... \land y_m$);
build a new circuit $D'$ from $C'$ that simply forces its output to 0 using an AND and NOT gate ($D' = C' \land \neg C'$)

If $\phi$ is not satisfiable then $D'$ and $C'$ are equivalent, otherwise they differ when the $x_i$ satisfy the formula AND all $y_i = 1$, but you can choose $m$ large enough to make the probability that $\bigwedge y_i =  1$ very small.

So if you have an efficient algorithm for your problem, you can afficiently solve the 3SAT instance.


$x$ is a "bound variable" and $M$ is the "scope" in which it is bound.


If I got this right, $\Pi_2L$ as defined above is equal to co-NP. The co-NP-complete DNF tautology sits in $\Pi_2L$: Use z for the assignment and y to choose which clause to check. To show $\Pi_2L$ in co-NP, universally guess z and the rest can be computed in P.


VC generalization bound extended to other types of target functions

Pseudo dimension and fat shattering dimension are (some of the) analogue of VC dimension in the regression setting. See https://ttic.uchicago.edu/~tewari/lectures/lecture15.pdf (section 3)


Is this optimum travelling problem under deadlines NP-hard on trees?

For this to be true, we have to make some assumptions. See comments below

For the tree case, I believe that there is a polynomial time recursive dynamic programming algorithm parameterized by the maximum deadline time. The sub-problems are: if we enter a sub-tree by time $t_a$ and exit the sub-tree by time $t_b$, what is the maximum number of tasks we can finish in the sub-tree? The base cases at the leaves are easy and we memoize from the bottom up.

If we truly parameterized by the maximum deadline time, then the algorithm would not really be polynomial in the size of the tree. However, the length of the longest path that visits every node in the tree is only polynomial in $|V|$, and we never need to check deadline times later than that.


Can neural networks be used to devise algorithms?

According to this blog By Reza Zadeh, training a neural network to produce correct output even for just two-thirds of the training examples is computationally hard:

Indeed, in 1988 J. Stephen Judd shows the following problem to be NP-hard:
Given a general neural network and a set of training examples, does there exist a set of edge weights for the network so that the network produces the correct output for all the training examples?
Judd also shows that the problem remains NP-hard even if it only requires a network to produce the correct output for just two-thirds of the training examples, which implies that even approximately training a neural network is intrinsically difficult in the worst case. In 1993, Blum and Rivest make the news worse: even a simple network with just two layers and three nodes is NP-hard to train!


Characterization of read-once formulae over the full binary basis

there is also a method called the Krapchenko lower bound "which can be slightly larger than Nechiporuks method". see John E Savage, Models of Computation, section 9.4.2. (which is covered right after the Nechiporuk method in section 9.4.1)


To what extent is "advanced mathematics" needed/useful in A.I. research?

I do not want to sound condescending, but the math you are studying at the undergraduate and even graduate level courses is not advanced. It is the basics. The title of your question should be: Is "basic" math needed/useful in AI research? So, gobble up as much as you can, I have never met a computer scientist who complained about knowing too much math, although I met many who complained about not knowing enough of it. I remember helping a fellow graduate student in AI understand a page-rank-style algorithm. It was just some fairly easy linear algebra to me, but he suffered because he had no feeling for what eigenvalues and eigenvectors were about. Imagine the things AI people could do if they actually knew a lot of math!

I teach at a math department and I regularly get requests from my CS colleagues to recommend math majors for CS PhD's becase they prefer math students. You see, math is really, really hard to learn on your own, but most aspects of computer science are not. I know, I was a math major who got into a CS graduate school. Sure, I was "behind" on operating systems knowledge (despite having decent knowledge of Unix and VMS), but I was way, way ahead on "theory". It is not a symmetric situation.


A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

My first advice is to take a look at chapter 15 of Girard, Lafont & Taylor Proofs & Types. In it, a weaker theorem is proved, but the basic ideas are quite similar, and the exposition should be simpler.

Second: Provably type correct is a bit of a misnomer. The property looks more like definability or accessibility. In a nutshell it expresses

$$ \forall t_1,\ldots t_n,\ \mathrm{Ind}(t_1) \wedge \ldots\wedge\mathrm{Ind}(t_n) \Rightarrow \mathrm{Ind}(f(t_1,\ldots, t_n))$$
where $\mathrm{Ind}(t)$ means the term $t$ is inductive, that is, built up from constructors. Being inductive is essentially being defined as an element of the inductive type, which makes the above property a statement about definability.

Third: You are correct, if $B$ proves that $f$ is type correct, then $[B]$ is the definition of $f$. Work through an example first: If $\mathrm{add}: \mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}$, then the statement of type correctness is:

$$ \forall x\ y,\ \mathrm{Ind}_{\mathbb{N}}(x)\rightarrow\mathrm{Ind}_{\mathbb{N}}\rightarrow \mathrm{Ind}_{\mathbb{N}}(\mathrm{add}(x, y))$$
in $\lambda\mathrm{PRED}_2$, which, erased, gives
$$ \mathrm{N}\rightarrow\mathrm{N}\rightarrow\mathrm{N}$$
in $\lambda_2$ (with $\mathrm{N}=\Pi X:*.X\rightarrow(X\rightarrow X)\rightarrow X$) which is exactly the right type for $\mathrm{add}$! So at least the types add up. Checking that the proof of type correctness of $\mathrm{add}$ gives you a good definition is more tedious, but Leivant gives the details.

Fourth: you are correct that (1 way of seeing) the converse requires examining the proofs of strong normalization. For each function definition in $\lambda_2$, you can "decorate" it into a proof of type correctness in $\lambda\mathrm{PRED}_2$, essentially using the "theorem for free" that comes with the type. A really nice exposition is Wadler, The Girard-Reynolds isomorphism, which is a highly suggested read for anyone in the field.

Fifth: I think you are correct in your correction of 5.4.39.

Edit: Elaboration on the 4th point:

Wadler defines, among other things, the Reynolds embedding from $\lambda_2$ to $\lambda\mathrm{PRED}_2$ with higher-order functions (Figure 4). This embeding sends a type to a proposition (the parametricity theorem) and sends a well tyepd term to a proof of parametricity of that same term.

The theorem you get implies "type correctness" of the defined function rather trivially. In fact I think Wadler treats this in detail in Section 5, and treats the $\mathrm{add}$ example in the appendix. The only subtle point is that the function is not directly defined over the inductive type, rather it takes the type and constructors as arguments.

At this point I really have to suggest you work through some examples.


What is the difference between non-determinism and randomness?

It's important to understand that computer scientists use the term "nondeterministic" differently from how it's typically used in other sciences.  A nondeterministic TM is actually deterministic in the physics sense--that is to say, an NTM always produces the same answer on a given input: it either always accepts, or always rejects.  A probabilistic TM will accept or reject an input with a certain probability, so on one run it might accept and on another it might reject.

In more detail:  At each step in the computation performed by an NTM, instead of having a single transition rule, there are multiple rules that can be invoked.  To determine if the NTM accepts or rejects, you look at all possible branches of the computation.  (So if there are, say, exactly 2 transitions to choose from at each step, and each computation branch has a total of N steps, then there will be $2^N$ total brances to consider.)  For a standard NTM, an input is accepted if any of the computation branches accepts.

This last part of the definition can be modified to get other, related types of Turing machines.  If you are interested in problems that have a unique solution, you can have the TM accept if exactly one branch accepts.  If you are interested in majority behavior, you can define the TM to accept if more than half of the branches accept.  And if you randomly (according to some probability distribution) choose one of the possible branches, and accept or reject based on what that branch does, then you've got a probabilistic TM.


Self-organizing Sequential Search Heuristics

The self-adjusting linked lists described by Bentley have practical applications in data compression.  For example, bzip2 uses move-to-front encoding (among many other tricks).  See also this paper by Bentley et al.


Is there any relationship of hardness between the two problems?

No, you cannot infer hardness of P1. (And your question looks suspiciously close to homework.) Consider the special case where

$D$ is an undirected graph $G=(V,E)$
$x$ is a subset $E_x\subseteq E$
$y$ is a non-negative integer

The function value $F(x,y,D)$

takes the value $2$, whenever $y\ge1$;
takes the value $1$, if $y=0$ and if $E_x$ induces a Hamiltonian cycle in $G$;
takes the value $0$, if $y=0$ and if $E_x$ does not induce a Hamiltonian cycle in $G$.

  Fact. The problem P1 of maximizing $F$ for a given graph $G$ is polynomially solvable.

(Just pick $E_x=\emptyset$ and $y=1$ to reach an objective value of $2$.)

  Fact. The problem P2 of maximizing $F$ for a given graph $G$ and a given number $y$ is NP-hard.

(By fixing $y=0$, the problem becomes the NP-hard Hamilton cycle problem.)


Simplest Machine Model Accepting $L = \{ww^Rw\;|\; w\in \Sigma^*\}$

You don't need nondeterminism or multiple heads.  Even a 2DPDA can accept this language:  push 2 counters per symbol while scanning from left endmarker to right; then pop 3 per symbol while scanning left until stack empty. At this point you're at the boundary between first w and w^R.  Scan left, pushing onto stack until left endmarker.  Now stack has w^R.  Play the same game again with the counters, then move right comparing stack contents to symbols read.
If success, then first 2/3 of string is w w^R.  A similar trick can be used to ensure last 2/3 of string is w^R w.  And of course, precede all of this with a single scan to make sure input is of length == 0 (mod 3).

There is an intro to 2DPDA's in my book, A Second Course in Formal Languages and Automata Theory.