Why is HAMILTONIAN CYCLE so different from PERMANENT?

The following is a proof over any ring of characteristic zero that the Hamiltonian cycle polynomial is not a polynomial-size monotone projection of the permanent. The basic idea is that monotone projections of polynomials with nonnegative coefficients lead to the Newton polytope of one being an extended formulation of the Newton polytope of the other, and then applying the recent lower bounds on extended formulations.

Let $f(x_1,\dotsc,x_n)$ and $g(y_1,\dotsc,y_m)$ be polynomials with nonnegative coefficients (as is the case here). Suppose that $f$ is a monotone projection of $g$ under the assignment $\pi$ (following the notation of the question). Under $\pi$, each monomial of $g$ gets mapped either to 0 (iff one of its variables gets mapped to 0) or to a monomial of $f$: there can't be any cancellations because of non-negativity.

Let $New(f)$ denote the Newton polytope of $f$, and similarly for $New(g)$.

Claim: there is an extended formulation for $New(f)$ in $\mathbb{R}^m$, using $\leq n+m$ variables, and a number of constraints that is at most $n+m$ plus the number of constraints defining $New(g)$.

Here's how: Let $e_1,\dotsc,e_m$ be the coordinates on $\mathbb{R}^m$ (in which $New(g)$ lives; viz., an integer point in $\mathbb{R}^m$ with coordinates $(e_1,\dotsc,e_m)$ corresponds to the monomial $y_1^{e_1} \dotsb y_m^{e_m}$). For those $i$ such that $\pi(y_i)=0$, intersect $New(g)$ with $\{e_i = 0\}$ (since only monomials that do not involve $y_i$ can contribute to the projection); this adds at most $m$ additional constraints. Let $P$ denote the resulting polytope. Then $\pi$ induces a linear map $L_{\pi}\colon \mathbb{R}^{m} \to \mathbb{R}^{n}$, such that $L_{\pi}(P) = New(f)$. This last part follows from the lack of cancellations. Thus we get an extended formulation for $New(f)$ by taking $n+m$ variables, the constraints for $P$ on the $m$ variables, and the constraints defining $L_{\pi}$ (of which there are at most $n$, one for each $x_i$). QED Claim

Now take $f$ to be the $n$-th Hamilton cycle polynomial and $g$ to be the $m$-th permanent, and suppose that $f$ is a monotone projection of $g$. The Newton polytope of the permanent (and determinant, incidentally), is the cycle cover polytope. This polytope is easily described by the "edge" variables $e_{ij}$ and the $m$ equations stating that every vertex has degree exactly 2.

The Newton polytope of the Ham. Cycle polynomial is the Hamiltonian cycle polytope (surprise, surprise). But this polytope is the TSP polytope, which requires $2^{n^{\Omega(1)}}$ equations to describe any extended formulation of, which, when $m$ is subexponential, contradicts the small extended formulation given by the cycle cover polytope and $L_{\pi}$ as above.

(Note that this argument fails if $f$, $g$, or $\pi$ can have negative coefficients, as then there can be cancellations, so $L_{\pi}$ need not map onto $New(f)$.)

It's interesting to note that the geometry of these polytopes is closely related to the fact that matching is in $\mathsf{P}$ while Hamilton cycle is $\mathsf{NP}$-complete, but I think the above reasoning shows how the geometric structure here really can add something beyond that complexity classification.


Why isn’t information-probability relationship linear?

So definition of self-information is chosen to be as follows (shamelessly copied from wiki page of "Information content" ) :

An event with probability 100% is perfectly unsurprising and yields no information.

The less probable an event is, the more surprising it is and the more information it yields.

If two independent events are measured separately, the total amount of information is the sum of the self-informations of the individual events.

Point 3 of the definition answers your question.
If $A$ and $B$ independent events and C is an event where both $A$ and $B$ take place then
$$P(C) = P(A \cap B) = P(A)\cdot P(B)$$
On the other hand information from $C$ is defined as follows:
$$I(C) = I(A)+I(B)$$
Let $f(\cdot)$ be the functional form of the information expression, formally $$I(E) = f(P(E))$$
Therefore,
$$f(P(C)) = f(P(A)) + f(P(B))$$
$$ = f(P(A).P(B))$$
Can you find an $f(x)$ which is of the form $k\cdot x$, such that the above properties are satisfied ? I think the answer is no.
But I would like to add that I don't recall very neat reasons for why it has to be only $k\log(x)$ as well. i.e why only $f(x) = k\log x $ satisfies $f(x\cdot y) = f(x)+f(y)$


Approximation for metric TSP: Worst case using nearest neighbor heuristic?

No, the NN heuristic does not have constant factor for metric TSP.

Rosenkrantz, Stearns, and Lewis proved in An Analysis of Several Heuristics for the Traveling Salesman Problem. SIAM J. Comput. 6(3): 563-581 (1977) that the worst case ratio of the tour obtained by the nearest neighbor method is bounded above by a logarithmic function of the number of nodes.


Correlation between noise resilience and output distribution of Boolean circuits

I have found some hints on my question in Moshe Looks, Competent Program Evolution, p. 31:

Most local perturbations of large random formulae have no effect – 96% of them for
arity five, and 91% for arity ten (the drop is a corollary of the increase in the percentage of
unique behaviors in a fixed size sample as the arity increase). This is a consequence of such
formulae typically being highly redundant – e.g., a large formula that computes a tautology
will likely remain a tautology when randomly perturbed (similarly a large subformula which
computes a tautology, etc.).

More resources would be highly appreciated if you know of any.


A partition problem with order constraints

Intuitively, the intermediate cases should be neither in P, nor NP-hard.  Perhaps it depends exactly on what we mean by "intermediate case".  Here is one interpretation for which we can prove something.

Note: The Exponential-Time Hypothesis, or ETH, is that it is not the case that, for every constant $\epsilon>0$, SAT has an algorithm running in time $2^{n^{\epsilon}}$.  See also this cs.stackexchange discussion.  As far as we know, ETH is true.

Define OP$_c$ to be the restriction of the OrderedPartition problem to instances where $d \le \log^c n$.  Equivalently, to instances where $n \ge 2^{d^{1/c}}$.  Here we intend OP$_c$ to capture what the post means by "intermediate instances".  We show that these instances are not likely to be in P, nor NP-hard.

Lemma 1. If OP$_c$ is in P for all $c$, then ETH fails.

Proof.  Suppose OP$_c$ is in P for all $c$.  That is, for some function $f$, OP$_c$ has an algorithm running in time $n^{f(c)}$. SAT inputs of size $n$ reduce (via Partition as described in the post) to OrderedPartition$[2^{n^{b/c}}, n^b]$, for some constant $b$ and any constant $c>0$.  So, SAT inputs of size $n$ reduce to OP$_c$ instances of size $2^{n^{b/c}}$, which can be solved in time $2^{f(c)n^{b/c}}$ via the algorithm for OP$_c$.  For any $\epsilon>0$, taking, say, $c=2b/\epsilon$, SAT can be solved in time $2^{c' n^{\epsilon/2}} \le 2^{n^{\epsilon}}$ (for large $n$), violating ETH.$~~~~\Box$

Note: It seems likely to me that even OP$_2$ is not in P, but showing something like that would be similar to showing, say, that SAT has no algorithm running in time $2^{\sqrt n}$.

Lemma 2. If OP$_c$ is NP-hard for some $c$, then ETH fails.

Proof.  Suppose OP$_c$ is NP-hard for some $c$.  Then SAT inputs of size $n$ reduce to OP$_c$ in time $O(n^b)$ for some $b$.  That is, to instances of OrdereredPartition$[n^b, d]$ where $d\le \log^c (n^b)$.  As observed in the post such instances can be solved in time
$n^{O(1)} 2^d = n^{O(1)} 2^{\log^c (n^b)}$, (strongly!) violating ETH.$~~~~\Box$

Probably something cleaner or stronger can be shown.  If I had to guess, I'd define NP$_{d(n)}$ to be the complexity class comprised of those languages that have a non-deterministic poly-time algorithm that, on any input of size $n$, uses at most $d(n)$ non-deterministic guesses.  (Here $d$ could be any function.)  Then OrderedPartition$[n, d(n)]$ is in NP$_{d(n)}$.  Perhaps it is complete for that class under poly-time reductions?  A natural guess for a problem that should be complete for the class would be: given a circuit of size $n$ with $d$ input gates, is there an input that makes the circuit output True?  Or something like that.  (I wonder how this compares to, say, defining SAT$_{p(n)}$ to consist of SAT instances, padded with $p(n)$ useless bits to make the input larger.  When $p(n)$ is super-polynomial but sub-exponential, the problem should be neither NP-hard nor in P.)

p.s. See also Consequences of sub-exponential proofs/algorithms for SAT .


Recent TCS publications with philosophical aspects

some of what you refer to is covered under a general heading known as "digital physics" or digital philosophy which has a continuing thread of research in physics albeit not always mainstream.

a notable example of a TCS paper/ survey with major philosophical angles/ analysis

Why Philosophers Should Care About Computational Complexity / Aaronson

another key area/ possibility you mention is AI which has generally broken off from TCS research as practiced in academia and is now regarded as either more applied or more abstract/ speculative, and few researchers cross that gap, but there are many books on the subject by respected researchers verging on the philosophical. eg, recently

The Master Algorithm: How the Quest for the Ultimate Learning Machine Will Remake Our World / Domingos (2015)


Does the infinite graph of diagonals have an infinite component?

The probability is 0.

This follows from the following theorem (see Theorem 5.33 in Grimmett's Probability on Graphs, http://www.statslab.cam.ac.uk/~grg/books/USpgs-rev3.pdf):

Theorem Consider bond percolation on $\mathbb Z^2$, where each edge between lattice points is open with probability $\frac12$. The probability that the origin is in an infinite connected component is 0.

We can reduce from our problem to this problem: basically it is just 2 disjoint (but dependent) copies of bond percolation on $\mathbb Z^2$. Consider the configuration $D_1$ where the edges form an infinite lattice of diamonds containing the origin. If we flip all edges, we get another infinite lattice of diamonds $D_2$. Consider the intersection of the actual configuration with $D_1$ and with $D_2$. Each of these is exactly the model of bond percolation on $\mathbb Z^2$, just rotated $45^{\circ}$. The probability that any point is in the infinite cluster is hence 0 (No edge in $D_1$ can be connected to an edge in $D_2$.).

To conclude, note that the sum of a countable number of events with probability 0 has probability 0; sum over the probability that any lattice point is in an infinite cluster.

(The existence of arbitrarily large components is a red herring. One should fix a point, and ask if it's in an unbounded component.)


Why are sub-normalized states studied in quantum computation?

It is often mathematically very convenient to work with sub-normalized states independently of the question whether they have a direct physical meaning.

However, you can always see them as states that are logically 'AND' with a certain event. For example, consider the c-q state

$\rho_{XB} = \sum_x |x\rangle\!\langle x|_X \otimes \rho_B^x$

where $\rho_B^x$ is sub-normalized so that the whole state is normalized. Then the trace of $\rho_B^x$ just gives the probability of finding the subsystem $B$ in the renormalized, conditional state $\rho_B^x / \text{tr}(\rho_B^x)$.

For example, the probability of measuring a certain event (POVM element) $E_B$ AND x is simply given by $\text{tr}(\rho_B^x E_B)$ and we never needed to renormalize the state to write this down.


Is the "Fewest Discriminating Bits" problem NP-complete?

This problem is NP-complete.  A proof based on reduction from 3-SAT is as follows:

Consider an instance of 3-SAT with $n$ variables and $m$ clauses.  We will construct $2n + 2m$ bit vectors ("rows") of length $2n + \lceil \log_2(n + m) \rceil$, such that the smallest number of discriminating bits is $n + \lceil \log_2(n + m) \rceil$ iff the original 3-SAT instance is satisfiable.

The first $2n$ bits will correspond to the literals $\left\{ x_1, \neg x_1, x_2, \neg x_2, ..., x_n, \neg x_n \right\}$.  With respect to these bits, the first $2m$ rows will come in pairs, the first of which will have a $1$ for each literal included in the corresponding clause, and the second of which will consist entirely of $0$'s.  The remaining $2n$ rows will also come in pairs, the first of which will have $1$'s for the corresponding literal and its negation, and the second of which will consist entirely of $0$'s.  Finally, the last $\lceil \log_2(n + m) \rceil$ bits will be used to "sign" each pair of rows with its index, from $0$ to $n+m-1$, written in binary.

In order to distinguish each "literal" row from its successor, either the bit corresponding to that literal or the bit corresponding to its negation must be retained.  Also, in order to discriminate among the $n+m$ "zero + index" rows, all $\lceil \log_2(n + m) \rceil$ index bits must be retained.  The minimum possible number of discriminating bits is therefore $n + \lceil \log_2(n + m) \rceil$.  Finally, in order to distinguish each "clause" row from its successor, at least one of the three bits corresponding to literals included in that clause must be retained.  If the 3-SAT instance is satisfiable, this last condition will not require any extra bits (in particular, we do not need to retain the bits corresponding to both $x_i$ and $\neg x_i$ for any $i$); and conversely, if there are $n + \lceil \log_2(n + m) \rceil$ bits that discriminate among all $2n+2m$ bit vectors, they must contain exactly one of $x_i$ and $\neg x_i$ for each $i$, and hence correspond to a satisfying assignment of truth values to the $n$ variables.


There is no way to choose the parameters A, B, C, D properly;
as it is the case for most heuristics, the parameters are chosen ''by experience''.
Worse, there is no guarantee that the solution (the array of the outputs)
of this heuristic is indeed a feasible TSP tour!

In this context, perhaps interesting to read: Wilson and Pawley,
On the stability of the Travelling Salesman Problem
algorithm of Hopfield and Tank,
Biological Cybernetics 58 (1988) 63-70.

To your first comment: I don't think that this TSP energy function is useful for practical purposes.
If you want to solve TSP in practice, maybe here
is the right starting point.


Create a bipartite graph:

For every element $x\in\bigcup_{i=1}^nS_i$, introduce a corresponding vertex $u(x)$.
For every set $S_i$, introduce a corresponding vertex $v(S_i)$.
Connect vertex $u(x)$ to vertex $v(S_i)$ by an edge, if and only if $x\in S_i$.

Then your problem essentially asks, whether there exists a subset $F$ of the edges, so that

every vertex $u(x)$ is incident to at most one edge in $F$, and
every vertex $v(S_i)$ is incident to at least $b_i$ edges in $F$.

This is an instance of the so-called $f$-factor problem, and hence solvable in polynomial time.
See for instance the book "Matching Theory" by László Lovász and Michael D. Plummer.


Least fixed point logic is efficiently $\operatorname{P}$-bounded for $\operatorname{P} \Leftrightarrow L_\leq$ is a logic for $\operatorname{P}$

People informally use the phrase "a logic for P" for the notion of a logic that captures P, which corresponds to Chen and Flum's definition of a "P-bounded logic for P". Essentially, this means that the logic defines exactly the polynomial-time properties of relational structures and formulae can be evaluated in polynomial time.1 Specifically, it's no use if your logic defines exactly the polytime properties but it takes exponential time to figure out whether a formula's true.

I think the confusion has arisen because Chen and Flum use the phrase "a logic for P" to mean just any logic that defines exactly the polytime properties of structures, without the requirement that formulae can be evaluated in polytime.  The logic $L_\leq$ is a logic for P in this specific sense.  Every polytime property is definable by a formula $\phi\in L_\leq$ but the semantics of the logic requires testing whether $\phi$ is $|A|$-invariant and there is no known way to do that in polynomial time.

$L_\leq$ defines all polytime properties because, by the result of Immerman and Vardi cited by Chen and Flum, LFP captures P on the class of ordered structures. More specifically, any ordering of the structure's universe lets you use tuples in $A^k$ to represent $k$-digit numbers in base $|A|$, which you can use as both for timestamps and to say "the $i$th character on the tape is $c$. You can then use a fixed-point formula that says, "If the configuration at time $t$ is $C_t$, then the configuration at time $t+1$ is $C_{t+1}$. The resulting formula doesn't depend on which ordering is chosen, so it's order-invariant, as required. Choosing a different ordering is just permuting the meaning of the digits in your base $|A|$ numbers.

Note that order-invariance in general is not decidable, which is why Chen and Flum restrict to order-invariance only on structures up to the size of the one we're evaluating the formula on. That's decidable but not known to be in P.  (But the formulas constructed above are, in fact, order-invariant across all structures.)

1 More formally, for every formula $\phi$, there is a deterministic algorithm and a constant $k$ such that the algorithm decides whether $\cal{A}\vDash\phi$ in time at most $|A|^k$.


How to generate a permutation uniformly by repeating using an one-bit uniform random generator?

Your solution does not work (or I don't understand it): the resulting permutation would not be uniformly random.

To Sasho Nikolov, this is a research topic and is actually the topic (among others) of a paper I have recently submitted, where I provide an optimal algorithm. I can give you an idea of the lower bound. Indeed, you would have to distinguish between n! different permutations, so theoretically you would need at least log2(n!) bits exactly. But Knuth and Yao show in their seminal paper ("The complexity of nonuniform random number"), that because of "rounding errors" (to simplify), the actually random-bit complexity is between log2(n!) and log2(n!) + 2, that those are the best bounds, and in addition they provide an exact expression in terms of entropy of the distribution (in this case the uniform distribution).

It can (and has) been shown that the exact complexity involves fluctuations periodic in log2(n), much like the average complexity of divide-and-conquer algorithms such as QuickSort. (Such details are routinely hidden by the traditional sledge-hammer approach known as the "Master theorem" :-).

Now, supposing you have your random number X, the bijection between the number and the corresponding permutation is a subproblem of what is more largely referred to as "unranking". Martinez and Molinero have devised a nice general framework based on a popular random generation framework introduced by Wilf and Nijenhuis and formalized by Flajolet et al.. But for permutations it is a much simpler problem: you consider the factorial-base expansion of X to get the random integers needed for the Fisher-Yates algorithm. See the following for more info:

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

http://en.wikipedia.org/wiki/Fisher%E2%80%93Yates_shuffle

EDIT: added the image which shows the optimal number of expected random bits needed to distinguish between N choices.


What's the intuition behind Rademacher complexity?

The standard "intuition" is that the Rademacher complexity quantifies the ability of the function class $F$ to fit symmetric random noise: a low value (close to 0) means that this ability is limited (and hence the "capacity" of this class is bounded), while a high value (close to 1 for $\{-1,1\}$-valued classes) means that essentially any sequence of random signed bits has a perfect fit (and hence the capacity is unbounded).
To delve a bit deeper, it's always helpful to consider the extreme cases. Let $F$ be a collection of $\{-1,1\}$-valued functions on some large set $\Omega$, $|\Omega|=N\gg1$. What happens when $F$ consists of a single function $f$? What happens when $F=2^\Omega$ consists of all possible functions? You can also consider the cases where $|F|=2,3$ and look up "Massart's finite class lemma", which gives a bound for $|F|<\infty$ and is actually at the heart of more sophisticated (covering-number based) bounds.


Combining subset sum and subset product problems

It is still NP-complete. Here is a very sketchy reduction from subset sum. The goal of the whole reduction will be to make $T$ unimportant.
If the inputs for subset sum are $a_i$, then add $a_i$ and $2^Na_i$ to our inputs, where $N$ is large, but still $poly(n)$.
Set $S$ to be $2^N$ times the original subset sum plus $2^N-1$.
Set $T$ to be the product of the $a_i$'s multiplied by a sufficiently big power of $2$, to be determined later.
The idea is that if the number with index $i$ was not picked, then we can pick $a_i$, while if it was picked, we can pick $2^Na_i$.
Finally, add a lot of each small power of $2$ to our input to be able to make the desired sum and product.
Notice that this gives us enough liberty to get $S$ and $T$.


What are the practical issues with intersection and union types?

Here are a few things to keep in mind:

Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types are.  So, it's worth pinning this down before you embark on an implementation.
One element which I think is awfully important for understanding intersections and unions is the concept of type refinement, essentially the idea that a program has a certain intrinsic "archetype" (e.g., "foo is a function from integers to integers"), which can then be refined to express more precise properties (e.g., "foo takes even integers to even integers and odd integers to odd integers"). With the concept of refinement in hand, the key property which distinguishes intersections and unions from products and sums is that the intersection/union of two types can be formed only if they refine the same archetype.  In other words, the type formation rules for intersections and unions may be expressed like so (read "$S \sqsubset A$" as "$S$ refines $A$")
$$\frac{S\sqsubset A \quad T \sqsubset A}{S\cap T\sqsubset A}\qquad
\frac{S\sqsubset A \quad T \sqsubset A}{S\cup T\sqsubset A}$$
whereas the formation rules for ordinary products and sums are
$$\frac{S\sqsubset A \quad T \sqsubset B}{S* T\sqsubset A*B}\qquad
\frac{S\sqsubset A \quad T \sqsubset B}{S+T\sqsubset A+B}$$
Since intersections and unions can be used to make more precise assertions about the run-time behavior of a program, it is natural that typing becomes sensitive to evaluation order. For example, papers (2) and (4) below explained why  the "obvious" (and fairly standard) typing and subtyping rules for intersections and unions are actually unsound for ML-like languages (due to the presence of side effects and non-termination). You have been warned!
For similar reasons, global type inference generally becomes impractical or undecidable. Indeed, the whole concept of "principal type" is arguably a red-herring, since a function may satisfy many different properties which are irrelevant to its intended use (e.g., "foo takes prime integers to integers greater than 7"). Instead, practical approaches to intersections and unions (see (3), (4)) are generally based on a combination of inference and checking.

I suppose some of the above points might sound negative, though I wouldn't call them "cons" but merely "realities" of intersection and union types. On the other hand, from a language design perspective, one reason for making the effort of supporting intersections and unions (and for getting them right!) is that they allow more precise properties of programs to be expressed in a fairly incremental way, requiring a much less drastic transformation than, say, dependent type theory.

A brief reading list:

Design of the Programming Language Forsythe by John C. Reynolds
Intersection Types and Computational Effects by Rowan Davies and Frank Pfenning
Practical Refinement-Type Checking by Rowan Davies (dissertation)
Tridirectional Typechecking by Joshua Dunfield and Frank Pfenning


Algorithm to find a polyhedral embedding

Doesn't this give you what you want?  Because you only care about the combinatorics, your problem is to embed a graph in a surface, I gather a surface of genus zero.

  Bojan Mohar, "Embedding graphs in an arbitrary surface in linear time," STOC 1996 (ACM link).


Integer relation detection for Subset Sum or NPP?

Let m be the logarithm of the largest number.
If $m=O(\log n)$ then it is solvable in polynomial time using dynamic programming.
In general, every known algorithm take at least $\Omega(2^{m})$ time. There is no known polynomial time algorithm when $m=\omega(\log n)$ and $m=o(n)$

However, Flaxman and Przydatek provide an algorithm that solves Medium-Density Subset Sum Problems in Expected Polynomial Time.

Check this reference:

Flaxman and Przydatek, Solving Medium-Density Subset Sum Problems in Expected Polynomial Time


No. Given any linear ordering of the $n$-bit strings, find a sequence of at most $n+1$ strings going from the first string in the ordering to the last string in the ordering by single-bit changes per step. Some two adjacent strings $x$ and $y$ in this sequence must be at least $2^n/n$ steps apart from each other in the ordering. But then, unless your definition of "far" only allows linearly many strings to be far apart from each other, there must be some $z$ that is far from $x$ and $y$ but between them in the ordering. So changing one bit from $x$ to $y$ reverses the ordering with $z$.


Is compiler for dependent type much harder than an intepreter?

This is an interesting question! As Anthony's answer suggests, one can use the usual approaches to compiling a non-dependent functional language, provided you already have an interpreter to evaluate terms for type-checking.

This is the approach taken by Edwin Brady. Now this is conceptually simpler, but it does lose the speed advantages of compilation when performing type checking. This has been addressed in several manners.

First, one can implement a virtual machine which compiles terms to byte-code on the fly to perform the conversion check. This is the idea behind vm_compute implemented in Coq by Benjamin Gregoire. Apparently there is also this thesis by Dirk Kleeblatt on this exact subject, but down actual machine code rather than a virtual machine.

Second, one may generate code in a more conventional language which, upon execution, checks all the conversions necessary to type-check a dependently typed program. This means we can use Haskell, say, to type-check an Agda module. The code can be compiled and run, and if it accepts, then the code in the dependently-type language can be assumed to be well-typed (barring implementation and compiler errors). I've first heard this approach suggested by Mathieu Boesflug.

Finally, one may require that the terms appearing in types and the terms intended to be run be part of two distinct languages. If the terms appearing at the type level do not themselves have dependent types, then one may compile in two stages: first, compile the "type-level" code and then you can execute this when checking the types of the "term-level" code. I'm not aware of any system that proceeds in this manner, but it is potentially possible for many systems, like Microsoft's F$^*$ language which has distinct type-level and program-level terms.


Papers to credit for spectral partitioning of graphs

It seems that the first paper introducing this set of ideas (using the algebraic invariant $\lambda_2$, the second smallest eigenvalue of the graph Laplacian, to bound various properties of the graph) to graph theory was Fiedler's "Algebraic Connectivity of Graphs" in Czechoslovak Mathematical Journal. It appeared in 1973,  roughly at the same time as the Cheeger's paper (1970), which dealt with manifolds. I am not sure who was the first to observe the parallel between graphs and manifolds in that respect. $\lambda_2$ is sometimes called the Fiedler number.

Interestingly, there is a remark at the end of the Fiedler's paper, pointing out an independent technical report by Anderson and Morley titled Eigenvalues of the Laplacian on a Graph from 1971, which apparently had similar ideas. However, it the paper by Anderson and Morley with the same title appeared in Linear and Multilinear Algebra only in 1985.


There are already some rather good related answers regarding LTL versus CTL. In a nutshell, LTL is first and foremost a logic of traces, and an LTL formula is true for a transition system $S$ if and only if it is true for each trace of $S$. CTL, on the other hand, is a branching-time logic, which can in a sense talk about multiple paths at the same time.

One standard example here (not the one you give, about which more below) is a labelled transition system $S=(Q,T,q_0,L)$ with set of locations $Q=\{q_0,q_1,q_2\}$, set of transitions $T=\{(q_0,q_0),(q_0,q_1),(q_1,q_2),(q_2,q_2)\}$, and labelling given by $L(q_0)=L(q_2)=\{p\}$, $L(q_1)=\emptyset$. This system satisfies $FGp$, but not $AFAGp$, which can be seen as follows.

$FGp$ means that for every path $\pi=s_1,s_2,\dots$ in a given system, there is some point after which $p$ is always satisfied, i.e. there is some $i$ such that for all $j\geq i$, $p\in L(s_i)$. This is satisfied by $S$ since every path in $S$ either remains in $q_0$ forever (such that $p$ is always satisfied) or eventually gets to $p_2$ (after which $p$ is always satisfied).

On the other hand, $AFAGp$ means that every path $\pi=s_1,s_2,\dots$ eventually reaches a state satisfying $AGp$, i.e. a state such that on every path $\pi'$ starting there, $p$ is always satisfied. Formally, this means that there is an $i$ such that for all $\pi'=s_1',s_2',\dots$ with $s_1'=s_i$ and all $j$, we have $p\in L(s_j')$. But in $S$, for the path which always remains in $q_0$, the transition to $q_1$, where $p$ is not satisfied, is always available, so that at no point of that path $AGp$ holds; therefore $AFAGp$ is not satisfied by $S$.

As for your example, this is actually a case where two formulas are equivalent. This does happen. The proof is a little involved, but I can add it if you are interested.


The Maxwell's Demon and Computer Science

A good place to start looking at these ideas is this paper, though it talks about the (related) idea of information and thermodynamics. It relates fundamental computational tasks (eg. editing a bit) to fundamental thermodynamic tasks (eg. energy extraction). Following the links within the paper should give reasonable access to literature on the subject. Also, see this paper.

EDIT - There is also discussion regarding this on Scott Aaronson's blog https://www.scottaaronson.com/blog/?p=3327. See the comments section too.

References -

1. The Hot Bit 1 : The Szilard-Landauer Correspondence,
M Gopalkrishnan - arXiv preprint arXiv:1311.3533, 2013

2. The Thermodynamics of Computation — a Review, C. Bennet -
International Journal of Theoretical Physics 21.12 (1982): 905-940.


Algorithm for identifying unprovable statements

I don't know much about complexity theory, but I can answer your first questions.

If the set of axioms is strong enough to encode Peano arithmetic, then you can construct unprovable statements by Gödel's first incompleteness theorem. You can easily construct infinitely many such statements, or equivalently, "detect" statements that are constructed like this. However…
Some statements are unprovable, but you cannot prove that they are unprovable. Using the same basic diagonalization as in the proof of Gödel's incompleteness theorems, you can e.g. consider a statement P that says "P is unprovable or false". P can't be proven true (otherwise it is false), nor proven false (otherwise it is true), nor proven unprovable (otherwise it is proven true). So, it is unprovable, but you can't prove it.
You can enumerate all provable statements, but not all unprovable ones — otherwise, you could just run both enumerators in parallel for long enough and that would give you a way to test whether a statement is true or provable, for any statement. I don't think there's a way to do strictly better than this "naive" enumeration.
Your last question is a bit vague — you're asking whether you could show that a proof of a statement exists in some non-constructive way; but what is "show" here? If you prove that the proof of a statement exists in the language of whatever axiomatic system you're using, then it "counts" as a valid proof within this system, so you actually constructed a proof…

I don't think you will spontaneously find statements like the ones described in this answer in complexity theory. This other question seems to indicate that this would require "radically new ideas". You might be able to fit weird provability theory statements into the language of complexity theory somehow, but it would probably be more of an artificial curiosity rather than a natural way of doing things.


How to become referee for TCS papers and conferences

Generally, you are invited to be a referee because the editor knows you or your work or he/she finds you because the paper under review cites your work or is in the same field as your work (perhaps via a google search).

Of course, if you are on the PC of a conference, you get to review loads of papers. You get on the PC by being invited, generally because you are either an old hand in the field or an up and coming star (or a friend/(ex-)colleague of the PC chair).

If you are a student or post-doc, then you should get to do some reviewing if your supervisor/boss/colleague/etc is on the PC of a conference.

In short, you need to be known or linked with someone who is known. Or alternatively you could ask a colleague whether you could review some papers for him/her next time he/she is on a PC.


One way of doing this is to, at each step, draw a random card from all the remaining decks that satisfy the constraints. I would suggest doing this by shuffling all the decks, and then taking the top card from one of the legal decks, picking a deck with probability proportional to the number of cards left in it.

This has the advantages that (a) in the case of no restriction, it is essentially Fisher-Yates-Knuth shuffling, and so gives a completely uniform permutation, and (b) since it favors decks with more cards, it leaves you with a reasonable chance of not ending with a bunch of cards in just one deck.

I suspect this is a reasonably good algorithm to use in practice, depending on what you want it for. However, it is not equivalent to the process of picking a uniform shuffle that satisfies the constraints, as I argue below.

Suppose you just have two decks, and you have $n/2$ cards in each deck for some large $n$. This question is equivalent to choosing a random way of tiling a length $n$ strip with alternating black or white tiles of length either $1$ or $2$, with the constraint that you have an equal area of black and white. We'll forget both the factor of two that comes from the fact that you can start with either a black or a white tile, and the restriction of equal areas of black and white, since for large $n$ these will contribute lower-order terms. The number of ways of tiling this strip is the $n$th Fibonacci number $F_n$, and the ratio of tiles of length $1$ to those of length $2$ is the golden ratio $\phi=\frac{\sqrt{5}+1}{2}$. You can see this because the last tile is either of length $1$ or length $2$, and for a length $1$ tile, there are $F_{n-1}$ ways of tiling the remaining strip, while for a length $2$ tile, there are $F_{n-2}$ ways. The ratio of the two lengths for the tile ending at position $n$ is thus $F_{n-1}/F_{n-2}$, which converges to $\phi$.

The process I sketched above, of choosing a random card from a legal deck, gives $1$ for this ratio of the number of runs of length $1$ do those of length $2$—a white card will be followed with equal probability by a white one (making a run of length $2$) or a black one (making a run of length $1$). Thus, it doesn't yield a uniform distribution among shuffles.

ADDED :

Here's an idea that will probably come pretty close to a uniform distribution over all allowed shuffles, although I can't analyze it. Suppose you just have two decks. Start by shuffling each deck. Choose a deck, say A, randomly to start the procedure. Take one card from deck A with probability $1/\phi$ and two cards from deck A with probability $1/\phi^2$. Then do the same for deck B. Keep this up, but adjust the probabilities so that the probability of one card from a deck is $1/\phi \pm \epsilon$, where $\epsilon$ is chosen so that you expect to exhaust the two decks at the same time. For more than two decks, or a restriction to no more than $k$ cards from each deck, you can use the same strategy, but you will have to figure out what the appropriate probabilities for choosing each allowed number of cards in the uniform distribution over allowed shuffles.


Is there a simple algorithm for proof search on CoC?

Is there a simple algorithm? yes. Simply enumerate all possibilities.  Of course this is pretty intractable in practice.

A proper sub-problem of term generation in CoC is "higher-order unification".  It handles the simply typed lambda calculus.  It is undecidable.  But there is a classic practical solution by Huet.  There are a lot of resources here: https://stackoverflow.com/questions/1936432/higher-order-unification.

Now the only good reference I know for CoC term generation is "A Complete Proof Synthesis Method for the Cube of Type Systems" by Dowek.  I believe this summarizes his thesis work (in french) and there is a draft pdf floating around (it has some errors).  His r-splitting construction is a little awkward for implementations, but he does a good job of highlighting the difficulties, and suggesting practical in-complete solutions.


What is known about computing distinct count range queries?

A sketch data structure is an approximation of a set of elements. Sketches vary in what they store -- some store just hashes, some store elements from the set (a sample), and some store floating-point numbers.

This solution uses the sketch data structure from "A Minimal Variance Estimator for the Cardinality of Big Data Set Intersection", by Cohen et al. It stores $k$ hash values.

Let $I = 2nk/m$. Let $F[t] = \{A[1], A[2], \dots , A[tI]\}$ and $B[t] = \{A[n], A[n-1], \dots, A[n-tI]\}$.  Store the sketches for $F[1],  F[2], \dots, F[m/2k]$ and $B[1],  B[2], \dots, B[m/2k]$. That is a total of $m/k$ sketches, each of size $k$, using a total of $m$ words of space.

Let $r(x)$ denote the value of $x$ rounded to the nearest integer. To estimate the carnality of $\{A[i], \dots, A[j]\}$, estimate the cardinality of $F[r(j/I)] \bigcap B[r((n-i)/I)]$. The Cohen et al. paper describes how to do this in $\text{poly}(k)$ time. The variance of the estimate is a long formula in Corollary 2, combined with the error induced by only using $m/k$ samples, which is at most $4nk/m$.


Let's consider $n$-bit strings $x$. Definitions:

$f(x,i)$ = bit string $x$ with last $i$ bits complemented.
$b(x)$ = "imbalance" of $x$: number of 1s in $x$ $-$ number of 0s in $x$.

Now fix a string $x$. Consider the function $g(i) = b(f(x,i))$. Observations:

$g(0) = b(x)$.
$g(n) = -g(0)$.
$|g(i) - g(i+1)| = 2$ for all $i$. We either remove one 0 and add one 1 or vice versa.

Now it follows that there exists an $i$ such that $-1 \le g(i) \le +1$.

Hence we can construct an $(n+O(\log n))$-bit string $y$ as follows: concatenate $f(x,i)$ and the binary encoding of the index $i$. The absolute value of the imbalance of $y$ is $O(\log n)$. Moreover, we can recover $x$ given $y$; the mapping is bijection.

Finally, you can add $O(\log n)$ dummy bits that reduce the imbalance of $y$ from $O(\log n)$ to $0$.


Can one reverse a hash with partial plaintext knowledge?

For an ideal hash function, the fastest way to compute a first or second preimage is through a brute-force attack. That is, if there's no structural weaknesses in the design of the hash function, your best bet is to mount a brute-force attack.

The knowledge of the message size (n bits) and some parts of it (m bits) will certainly reduce the complexity of finding a preimage under the brute force attack: The worst-case complexity will reduce from 2n to 2n-m.

A space-time trade-off over the brute-force attack is by exploiting rainbow tables. I believe  the partial knowledge of the preimage may prove useful in mounting this attack too.


Complexity of Smoothed $\ell_0$ algorithm

There appear to be two user-introduced parameters $K,L$ in the algorithm you point to. Apart from that, the main task appears to be the computation of a pseudoinverse, and matrix multiplication. Without any further knowledge of the structure of the $n\times n$ matrix $A$, it would appear that the running time is $O(KL g(n))$, where $g(n)$ is your best estimate for computing the inverse and doing the multiplication.

Crudely, both of these can be bounded by $cn^3$, but there might be better answers based on your actual setting (if A is sparse, or if you use Strassen's matrix multiplication, and so on)


Are endmarkers necessary for Deterministic Pushdown Automata?

Short answer: it depends on how you set the acceptance condition of the DPDA model: final state or empty stack.

The endmarkers are not necessary for DPDAs in which the accept condition is final state (which is also used to define the deterministic context-free languages - DCFLs): for all $L \dashv$ ("endmarked" language) recognized by a DPDA there is a DPDA that recognizes $L$.

See:

Theorem 2.43. $A$ is a DCFL if and only if $A \dashv$ is DCFL

in Michael Sipser's Introduction to the Theory of Computation.

But endmarkers play a role when proving equivalence between DPDAs and DCFGs (deterministic context free grammars):

Theorem: An endmarked language is generated by a deterministic CFG iff it can be recognized by a DPDA

Very informally a DCFG for $L$ exists if and only if there is a DPDA that accepts $L$ with empty stack acceptance condition (the stack is empty at the end of the input); which is not the "standard" definition of a DPDA. With non-determinism the two conditions are equivalent because the PDA can guess the end of the input and clear the stack with $\epsilon$ moves; without non-determinism they are not equivalent.

Without the endmarker DCFGs can only generate a proper subset of the languages recognized by DPDAs: DCFGs can only generate the prefix-free languages recognized by DPDAs (no string is a prefix of another string).

As a simple example consider this language: $L = \{ a^n b^m \mid m < n \}$. There is no DPDA with empty stack acceptance condition for it.

Note on the Kozen's book

In Lecture 23 he defines PDA as: $M = ( Q, \Sigma, \Gamma, \delta, s, \bot, F)$ where "... $F\subseteq Q$ is the final or accepts states".
Then he describes the two different acceptance conditions and proves their equivalence for (N)PDAs.

In Supplementary Lecture F he defines DPDA as: "$M = ( Q, \Sigma, \Gamma, \delta, s, \dashv, \bot, F)$ where everything is the same as with NPDAs except  (i) $\vdash$ is a special symbol not in $\Sigma$, called the right-endmarker ..." (then he adds the other conditions to forbid non-determinism and to prevent the pop of the $\bot$ symbol).

He then says: "We consider only acceptance by final state. One can define acceptance by empty stack and prove that such machines are equivalent. The assumption (iii) would have to be modified accordingly" (which is correct because the model described uses the extra endmarker $\dashv$).


Special Properties Of DAWGs with Unique Elements

I could be missing something, but if you took an arbitrary DAG, assigned unique IDs to each vertex, and constructed all words formed by traversing monotone chains from top to bottom, then wouldn't the DAWG of that set be the original DAG ? If so, then a DAWG has no special structure.

Update: Peter Taylor's comment is the key difference. only one node with indegree 0 unlike a regular DAG.


If PIT over a finite field $F$ is in P, then there is a family of multilinear polynomials whose graph is decidable in $\mathsf{NE}$ but which does not have poly-size $F$-algebraic circuits (Carmosino-Impagliazzo-Kabanets-Kolokolova APPROX-RANDOM '15). (And a similar result holds over $\mathbb{Z}$.) This is an algebraic circuit lower bound on $\mathsf{NE} \subseteq \mathsf{NEXP}$.

To get $\mathsf{P} = \mathsf{BPP}$ out of, e.g., Nisan-Wigderson (& Impagliazzo-Wigderson), one needs a Boolean (sub)exponential circuit lower bound on functions in (deterministic) $\mathsf{EXP}$.

So, on the one hand, an algebraic circuit lower bound on $\mathsf{NEXP}$ is a lot closer to $\mathsf{P} = \mathsf{BPP}$ than we are today, but still seems pretty far in some absolute sense: algebraic -> Boolean*, super-poly lower bound -> exponential, and $\mathsf{NEXP}$ -> $\mathsf{EXP}$.

(Of course, as discussed by Emil Jerabek in the comments, if one uses Impagliazzo-Kabanets to get PIT in $\mathsf{quasiP}$ by giving an exponential algebraic circuit lower bound, then the "super-poly -> exponential" gap goes away. But I took the question to mean "Suppose $PIT \in \mathsf{P}$ by any arbitrary method...")

*Over a fixed finite field this is probably the easiest one to overcome.


Timothy Gowers has a set of videos on Computational Complexity and Quantum Computation online.


Element distinctness can be solved deterministically in the RAM model in time within $O(n\log\log n)\subset o(n\log n)$ time:

Sort in time within $O(n\log\log n)$ your $n$ numbers of $w$ bits using the sorting algorithm described by Han in STOC 2002 ("Deterministic sorting in $O(n\log\log n)$ time and linear space"), then scan in linear time for collisions.

As far as I know, that is the best result known to this day.


Here's a straightforward application in communication complexity (which I see now is also described in a comment by Andy Drucker on his blog) outside the context of derandomization:

Suppose Alice and Bob are given strings $x$ and $y$ respectively, and they want to find out if the Hamming distance between $x$ and $y$ is at most $\epsilon n$ (where $\epsilon$ is some fixed constant).  We want to prove a communication complexity lower bound for this problem.  The observation is that any deterministic protocol for this problem yields a deterministic protocol with the same number of rounds for checking equality of two strings $a$ and $b$ of length $cn$ where $c<1$ is some constant depending on $\epsilon$.  Why?  To check equality of $a$ and $b$, Alice and Bob can run the protocol for the first problem on $C(a)$ and $C(b)$ where $C$ is an error correcting code with distance at least $\epsilon$.  Since there is an easy linear lower bound for the equality problem, this also yields a deterministic linear lower bound for the first problem.


Tool for specifying operational semantics for given formally specified programming language

We have been working on one for the last few years: Lem, a higher-order, typed language with backends for OCaml, Coq, Isabelle/HOL, HOL4, LaTeX and HTML.  Lem has been used internally in the group to formalise various machine models (PowerPC, ARM, and so on), memory models (the C memory model, etc.), programming language semantics (OCaml Light), and so on.


There is a data structure called an "invertible Bloom filter" due to Goodrich and myself that can be used for storage: you can add and remove keys and, whenever the current number of keys is below the capacity of the structure, determine what they are with high probability (regardless of whether it was ever above capacity in the past). Goodrich and Mitzenmacher have generalized this to allow values to be associated with the keys as well.

However, one drawback to these structures is that they use quite a bit more space than a normal Bloom filter: basically, a logarithmic number of bits per key rather than a constant number of bits per key.

See

Space-efficient straggler identification in round-trip data streams via Newton's identitities and invertible Bloom filters.
D. Eppstein, and M. T. Goodrich.
arXiv:0704.3313.
IEEE Trans. Knowledge and Data Engineering 23(2): 297-306, 2011.

and

Invertible Bloom Lookup Tables
Michael T. Goodrich, Michael Mitzenmacher
arXiv:1101.2245


Is the unbounded fan-in model realistic?

Don't forget that even though the fan-in is unbounded, the number of gates is polynomially bounded in the number of variables $n$ (in the definition of $\mathsf{AC}$ for instance) .


Why do functional programming languages require garbage collection?

All of the following comments are premised on the choice of a standard implementation strategy using closures to represent function values and a call-by-value evaluation order:

For the pure lambda calculus, garbage collection is not necessary. This is because it is not possible to form cycles in the heap: every newly-allocated value can only contain references to previously-allocated values, and so the memory graph forms a DAG -- so reference counting suffices to manage memory.
Most implementations do not use reference counting for two reasons.

They support a form of pointer type (eg, the ref type constructor in ML), and so true cycles in the heap can be formed.
Reference counting is much less efficient than garbage collection, since

it requires a lot of additional space to keep the reference counts, and
updating the counts is usually wasted work, and
the updates to the counts create a bunch of write contention which kills parallel performance.

Linearly-typed languages can eliminate the reference count (essentially because counts are 0-1: either the value has a single reference to it or it is dead and can be freed).
However, stack allocation still does not suffice. This is because it is possible to form function values which refer to free variables (i.e., we need to implement function closures), if you allocate things on the stack, then live values can be interleaved with dead values, and this will cause incorrect asymptotic space usage.
You can get the right asymptotics by replacing a stack with a "spaghetti stack" (ie, implement the stack as a linked list in the heap, so that you can cut out dead frames as needed).
If you want a real stack discipline, you can use type systems based on "ordered logic" (essentially linear types minus exchange).


It's the $\alpha^{\mathrm{th}}$ moment of the Tribus surprisal.
This generalizes the statement that entropy = expected surprisal.
Or in Ross's textbook, "expected surprise".


Your problem is solved in the paper Spheres of Permutations under the
Infinity Norm — Permutations with limited displacement by Torleiv Kløve.

See also A002524 and other sequences linked there. I found Kløve's paper by calculating the first few values of A002524 and finding it on the OEIS.


Major unsolved problems in distributed systems?

See, for instance, Eight open problems in distributed computing.


Type systems preventing laziness-related memory leaks?

Levy's call by push value calculus makes a distinction between values and their thunks.  For a value v of type ty the computation thunk v has type U ty.  Lindley and McBride's Frank language, inspired by CBPV, also makes this distinction between computations and values explicit, though unlike Haskell, Frank is strict.


I give a trivial construction which satisfies the requirement. I provide it to merely answer the existence of "reflexive" hash function.

Let $G$ be any hash function producing high entropy in the output. Assume that $G$ hashes arbitrary-length binary strings to $k$-bit binary strings, where $k$ is any positive integer. Let $+$ denote the concatenation operator, and let $|x|$ denote the length of the binary string $x$.

Define the hash function $H$ on input $x$ as follows:

If $|x| \le k$, then $H(x) \overset{\text{def}}{=} G(x)$.
If $|x| > k$, let $L$ and $R$ be the $(|x|-k)$-bit prefix and $k$-bit suffix of $x$, respectively. That is, $x = L + R$ and $|R|=k$. If $R = H(L)$ (where $H(L)$ is computed recursively), then $H(x) \overset{\text{def}}{=} R$; otherwise, $H(x) \overset{\text{def}}{=} G(x)$.

As I said, this is a trivial construction. It can be applied to any hash function, practical (such as MD5, SHA-1, ...) or theoretical.


How can you build a coinductive memoization table for recursive functions over binary trees?

It's easy enough to get the recursion pattern to work with sized types.
Hopefully the sharing is preserved through compilation![1]

module _ where

open import Size
open import Data.Nat

data BT (i : Size) : Set where
  Leaf : BT i
  Branch : ∀ {j : Size< i} → BT j → BT j → BT i

record Memo (A : Set) (i : Size) : Set where
  coinductive
  field
    leaf : A
    branch : ∀ {j : Size< i} → Memo (Memo A j) j

open Memo

trie : ∀ {i} {A} → (BT i → A) → Memo A i
trie f .leaf = f Leaf
trie f .branch = trie (\ l → trie \ r → f (Branch l r))

untrie : ∀ {i A} → Memo A i → BT i → A
untrie m Leaf         = m .leaf
untrie m (Branch l r) = untrie (untrie (m .branch) l) r

memo : ∀ {i A} → (BT i → A) → BT i → A
memo f = untrie (trie f)

memoFix : ∀ {A : Set} → A → (A → A → A) → ∀ {i} → BT i → A
memoFix {A} lf br = go
 where
  go h : ∀ {i} → BT i → A
  go = memo h
  h Leaf = lf
  h (Branch l r) = br (go l) (go r)

[1] https://github.com/agda/agda/issues/2918


Change the binary search procedure to pick a weighted midpoint at each time step:

1.  Input: Search key K, sorted array A, probability distribution P.
2.  Initialize m=0, M=n=len(A)=len(P).
3.  Repeat:
4.     Pick i with m <= i < M such that
5.       sum(P[j] for m<=j<i) <= sum(P[j] for m<=j<M)/2
6.     and
7.       sum(P[j] for i<j<M) <= sum(P[j] for m<=j<M)/2.
8.     Compare K with A[i].
9.     If K==A[i], return i.
10.    If K<A[i], set M=i.
11.    If K>A[i], set m=i+1.
12.    If m==M, return -1. (Fail.)

Suppose the search key is in the array - i.e., K==A[i] for some i. The algorithm halves the value sum(P[j] for m<=j<M) after each iteration. Moreover, this sum starts at 1 and must always be at least P[i]. Thus the number of comparisons is at most 1+log_2(1/P[i]).

If you want to retain the $O(\log n)$ worst case performance, you can mix a bit of the uniform distribution into your distribution. That is, run the algorithm with P'=(P+U)/2, where U is the uniform distribution. Then the number of iterations is at most 1 + log_2(1/P'[i]) <= 2 + min{ log_2(1/P[i]), log_2(n) }.


With equirecursive types are there downsides to making all types potentially recursive?

My advice would be to make sure that your translation function is  compositional and straightforward, i.e., for a typical construct $A * B$ the translation function $t$ should have the form $t(A * B) = s(t(A), t(B))$, where $s$ is the translation of $*$. Thus the translation should follow the syntax of the input language. If you want to perform any "optimizations", those should come as convinient tactics that get used after the translation phase. This will make it easier to pove that your translation works correctly.

Concretely, if your input language has a construct for defining recursive types, such as data in Haskell, then you should translate those to $\mu \cdots$ even if they are not actually using the recursion, because that is what they are. You can always have a simple lemma afterwards which shows that $\mu$ can be omitted in certain cases. If you set up your tactics the right way, the theorem prover will simplify things by itself (and do much more if needed). But you should not put $\mu$ in front of a definition that cannot be recursive, such as newtype. In other languages, for example in Ocaml, the only way to introduce a new type is with type, which may be recursive, so there you'd put $\mu$ in front of everything.


Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?

The compactness theorem for classical first-order logic is a direct consequence of the completeness theorem, and, actually, one can prove directly Compactness by the Henkin-style argument used for Completeness without ever mentioning derivation.

The Completeness theorem for classical FOL with respect to standard Tarski models has been formalized in Mizar. See the series of articles under http://fm.mizar.org/2005-13/fm13-1.html

The same completeness theorem, but with a constructive proof, has been almost formalized in the Coq proof assistant by myself, see the zip file under https://sites.google.com/site/dankoilik/publications/phd-thesis

I say "almost" because there is one technical point, proving a correctness of a sorting algorithm, that I have not yet had time to finish, however the main ingredient (constructive ultra-filter theorem for countable languages) is formalized.

One can also consider Completeness, and hence Compactness, for a non-standard notion of validity, and get a complete and formalized constructive proof.


What would it mean to disprove Church-Turing thesis?

There's a subtle point that I rarely see mentioned in these kinds of discussions and that I think deserves more attention.

Suppose, as Andrej suggests, someone builds a device which reliably computes a function $f$ that cannot be computed by any Turing machine.  How would we know that the machine is in fact computing $f$?

Obviously, no finite number of input/output values would suffice to demonstrate that the machine is computing $f$ as opposed to some other Turing-computable function that agrees with $f$ on that finite set.  Therefore, our belief that the machine is computing $f$ would have to be based on our physical theories of how the machine is operating.  If you look at some of the concrete proposals for hypercomputers, you will find that, sure enough, what they do is to take some fancy cutting-edge physical theory and extrapolate that theory to infinity.  O.K., fine, but now suppose we build the hypercomputer and ask it whether a Turing machine that searches for a contradiction in ZFC will ever halt.  Suppose further that the hypercomputer replies, "No."  What do we conclude?  Do we conclude that the hypercomputer has "computed" the consistency of ZFC?  How can we rule out the possibility that ZFC is actually inconsistent and we have just performed an experiment that has falsified our physical theory?

A crucial feature of Turing's definition is that its philosophical assumptions are very weak.  It assumes, as of course it must, certain simple features of our everyday experience, such as the basic stability of the physical world, and the ability to perform finite operations in a reliable, repeatable, and verifiable manner.  These things everyone accepts (outside of a philosophy classroom, that is!).  Acceptance of a hypercomputer, however, seems to require us to accept an infinite extrapolation of a physical theory, and all our experience with physics has taught us not to be dogmatic about the validity of a theory in a regime that is far beyond what we can experimentally verify.  For this reason, it seems highly unlikely to me that any kind of overwhelming consensus will ever develop that any specific hypercomputer is simply computing as opposed to hypercomputing, i.e., doing something that can be called "computing" only if you accept some controversial philosophical or physical assumptions about infinite extrapolations.

Another way to put it is that disproving the Church-Turing thesis would require not only building the device that Andrej describes, but also proving to everybody's satisfaction that the device is performing as advertised.  While not inconceivable, this is a tall order.  For today's computers, the finitary nature of computation means that if I don't believe the result of a particular computer's "computation," I can in principle carry out a finite sequence of steps in some totally different manner to check the result.  This kind of "fallback" to common sense and finite verification is not available if we have doubts about a hypercomputer.


Popular average-case complexity assumptions

The assumptions often used in crypto are a form of average-case complexity assumptions, such as hardness of factoring or discrete log in various groups.

Many lattice problems used for strong hardness guarantees for lattice based cryptography are qualitatively somewhat different than the factoring/discrete log based cryptographic assumptions.

The development of indistinguishability obfuscation has also introduced a number of novel average case hardness assumptions.

Often times average case complexity is used in the study of data structures for upper bounds (eg., of hash tables), but there are also some useful lower bounds. For example, the worst case $\Omega(n \log n)$ lower bound on sorting can be generalized to the average case, and to randomized algorithms as well (eg., see these lecture notes)


Stackelberg solution to $n$-player Hotelling's game on a segment

This game has been studied in

  Hee-Kap Ahn, Siu-Wing Cheng, Otfried Cheong, Mordecai Golin, René van Oostrum:
  "Competitive facility location: the Voronoi game"
  Theoretical Computer Science 310, 2004, pp 457-467

There also are lots of follow-up works, as for instance

  Sayan Bandyapadhyay, Aritra Banik, Sandip Das, Hirak Sarkar:
  "Voronoi game on graphs"
  Theoretical Computer Science 562, 2015, pp 270-282


This is the notation for Harper's "abstract binding structures": x.t represents the binding site of a variable x and the term t the variable scopes over.
Apparently you are in the parts that define variable bindings. $\mathcal{B}[\mathcal{X}]_s$ appears to be the set of terms, or binding structures at sort $s$ whose free variables are among $\mathcal{X}$. So I would expect (but I don't have the book) that there is in fact an explanation for this notation close by.


Computing Functions with Dynamical Systems

Brockett [1] studied a closely related idea, and showed how to construct dynamical systems that solve any linear programming problem in (I believe) the same manner you suggest, as well as dynamical systems to sort a list of numbers and to diagonalize a matrix. You may be able to use this to directly get the dynamics you need to compute the squaring function.

(At some point I saw a cool video of the trajectory of a dynamical system for sorting, but I can't seem to find it...)

I won't venture a guess as to whether such dynamical systems formulations could be used to prove something interesting in computability/complexity, but can offer some further references that may be relevant.

In quantum computing, Nielsen, Dowling, Gu, and Doherty show that QC can be realized as (if I understand correctly) geodesic flow on a certain manifold - a particular example of the kind of dynamical system you're talking about. See [2] and references therein for a discussion of some complexity issues related to this.

Finally, although I don't think it's exactly what you're talking about, it would probably also be worth checking out Bernard Chazelle's work on "influence systems" which are a type of dynamical system that is at least as powerful as Markov chains and Turing machines, but can exhibit all kinds of dynamic behavior (including chaos, etc). See [3] and references therein.

[1] Roger W. Brockett, Dynamical Systems that Sort Lists, Diagonalize Matrices and Solve Linear Programming Problems, Proc. 27th IEEE Conf. Dec. and Control, Austin, TX, pp. 799-803, Dec. 1988.

[2] Mark R. Dowling, Michael A. Nielsen. The geometry of quantum computation, arXiv:quant-ph/0701004, 2007.

[3] B. Chazelle, Natural Algorithms and Influence Systems, Comm. ACM 55 (2012), 101-110.


How hard is a variant of graph automorphism problem?

If I understood well the question, this is an attempt to prove that your problem is $GI$-complete.

Given two graphs $G_1, G_2$ connect all the nodes of $G_1$ to a new node $x$ and all the nodes of $G_2$ to a new node $y$. Then connect $x$ and $y$ with a path of new nodes: $ x_1, x_2, ... x_k,\; z\;, y_k, ...,y_2, y_1$ (there is an odd number of nodes between $x$ and $y$, and $z$ is the central node).

Now you can pick some pairs of nodes at the two endpoints: $(x,y),(x_1,y_1),(x_2,y_2),...$. In this way you end up with an instance of your problem that has a solution if and only if the two original graphs are isomorphic.


That question was about a translation from an arbitrary instance of SAT to a HORN-SAT instance with the exact same satisfying assignments. The translation property needed for P$\neq$NP is just equisatisfiability, not equality of assignments. That is, it simply requires them both to be satisfiable, or unsatisfiable. If satisfiable, they may be satisfied by different assignments.

For example:
$a \wedge \neg b$ and $\neg a \wedge b$ are equisatisfiable (they are both satisfiable), but they have different satisfying assignments.

The answer was that there can not be a satisfying assignment preserving translation, but this doesn't tell us whether there is a polynomial time satisfiability preserving translation.


The most applicable areas in Theoretical Computer Science

Anything to do with Machine Learning has a lot of career prospects because you could be employed by either finance or technology companies in general.


What methods exist for returning all points within an arbitrary closed shape?

There are no options.

For any set of $n$ points, if you want to answer range queries for arbitrary ranges, all $2^n$ subsets are possible answers.  (In fact, for any set of $n$ points in convex position, every subset is the intersection with some convex range.)  It follows immediately that any query algorithm (describable as a decision tree) requires $\Omega(n)$ time, no matter how much time and space you spend preprocessing the points.

Equivalently: The range space (points in the plane, convex regions in the plane) has unbounded VC-dimension, so there's no hope for an efficient range searching algorithm.


All pair shortest path problem for large number of nodes

Search papers on : "Shortest Path Queries Using Highway Hierarchies". There is a paper by Sanders and Schultes. If you follow their citations, there are lot of other papers. These methods are very useful for real road networks.


How many minimal $k$-cycles can you put in a graph?

If $k$ is divisible by 2 we can take a clique on $n/2$ vertices and subdivide each edge once.
This graph will have ${n/2 \choose k/2} \cdot (k/2-1)!/2$ cycles of length $k$.

Hence the total number of cycles is $\frac{1}{2} \sum_{i=k/2}^{i=n/2} {n/2 \choose i} \cdot (i-1)!$


What is contextual equivalence ignoring non-termination called?

(This is an extended comment).

I may be misreading your definitions, but it seems to me that the relation you introduce, let us call it $\simeq$, is not an equivalence relation because it is not transitive.

If $V_1,V_2$ are two distinct closed normal forms (values), then obviously $V_1\not\simeq V_2$.

On the other hand, the genericity lemma (Proposition 14.3.24 in Barendregt's $\lambda$-calculus book) says that given an unsolvable term, say $\Omega$, for any context $C$, either $C[\Omega]\!\Uparrow$ or $C[M]$ has the same normal form (a value, if we assume to work with closed terms) for every term $M$ (including $\Omega$). This shows in particular that $\Omega\simeq V_1$ and $\Omega\simeq V_2$, hence the failure of transitivity.


Explicit mu-recursive expression for Ackerman function

Breaking the Ackermann function all the way down to the elementary operators would really be quite lengthy, but here is a sketch:

Note that when computing $A(m,x)$ recursively, at any point of the computation you are dealing with an expression of the form $A(m_1,A(m_2,\dots,A(m_k,z)\dots)$. Given a bijective pairing function $p$ with inverse $(\pi_1,\pi_2)$, we can encode this state as $p(z,p(k,p(m_k,\dots,p(m_2,m_1)\dots)$ (just $p(z,0)$ in case $k=0$). We then can define the one-step evaluation function, given a state:

$e(p(z,0)) = p(z,0)$;

$e(p(z,p(k,p(0,c)))) = p(z+1,p(k-1,c))$;

$e(p(0,p(k,p(m+1,c)))) = p(1,p(k,p(m,c)))$;

$e(p(z+1,p(k,p(m+1,c)))) = p(z,p(k+1,p(m+1,p(m,c))))$.

You then get the n-step evaluation function using primitive recursion:

$E(0,m,x) = p(x,p(1,m))$ and $E(n+1,m,x) = e(E(n,m,x))$.

Finally, wrap $\mu$-recursion around $E$ to find the point where we get to a state of the form $p(z,0)$  - $z$ will be $A(m,x)$.


The Complexity Theory Companion by Hemaspaandra and Ogihara.  It's not exhaustive in terms of techniques (I imagine no such book is), but I think it qualifies as an answer to your question.  Here are the titles of the chapters:

The Self-Reducibility Technique.
The One-Way Function Technique.
The Tournament Divide and Conquer Technique.
The Isolation Technique.
The Witness Reduction Technique.
The Polynomial Interpolation Technique.
The Nonsolvable Group Technique.
The Random Restriction Technique.
The Polynomial Technique.


An identical homomorphism characterization of DCFL does not seem to be possible. The following is extracted from Greibach's original paper.

  We show that every context-free language can be expressed as $h^{-1}(L_0)$ or $h^{-1}(L_0-\{e\})$ for a homomorphism $h$. The algebraic statement is: the family of context-free languages is a principal AFDL; ... By way of contrast, the family of deterministic context-free languages is not a principal AFDL [7].

The paper 7 is the conference version of the paper. In the conference version, Theorem 4.2 states that "The family of deterministic context-free languages is not a principal AFDL".

However some analogue characterization may still be possible. Okhotin provided homomorphic characterizations of conjunctive and Boolean grammars. For DCFL's the problem seems to be open. The following is the conclusion of Okhotin's paper (from 2013).

  Every family of languages closed under inverse homomorphisms can potentially
  have an analogue of Greibach’s inverse homomorphic characterization.
  The question is, which families have it? Could it exist for linear, deterministic
  or unambiguous variants of ordinary (context-free) grammars? Could
  there be such a characterization for linear conjunctive grammars, unambiguous
  conjunctive grammars, etc.?


What is the state of the art in online voting?

This question is probably too broad to be answerable here, because the answer depends on what kinds of security requirements you have, what the threat model is, and what assumptions we're willing to make -- there are many different versions of those.  In other words, the "secure voting" problem is not one problem, but a broad class of problems.  I suggest doing a literature search, reading some of the classic papers, then see if you have a more specific question.  You could start with papers published at EVT and WOTE use them to seed your literature search.

If you're specifically interested in coercion, I suggest looking at Juels, Catalano, and Jakobson (WPES 2005) and Civitas (IEEE S&P 2008).  Those are two important early papers.  Also, by doing a search on papers that cite them, you'll be able to turn up a lot of more recent work on coercion.

All of these schemes have something in common; they do require some kind of trusted channel to the voter or some situation where the voter does register in person in a supervised environment.  They might not require supervision during the time of voting; that can be pushed to a setup phase.

Also, the solutions may depend on whether you are willing to assume that voters have a personal device (e.g., smartphone) and whether voters are willing to trust it.  Obviously the problem gets easier if you answer that in the affirmative.


Complexity of unbalanced bipartite isomorphism

If you are willing to relax the 2 to some other constant, then yes: this can be solved in $O(c^a)$ time for some absolute constant $c$. You can view this problem as isomorphism of hypergraphs, where the vertices in $A_i$ are the vertices of your hypergraph, and the vertices in $B_i$ are hyperedges. Luks (STOC '99) showed how to solve hypergraph isomorphism for hypregraphs on $a$ vertices in $O(c^a)$ time for some absolute constant $c$.


Graphs in which all shortest paths are unique

According to Information System on Graph Classes and their Inclusions, these graphs are studied under the name “geodetic graphs.”


Since Steven Stadnicki's answer doesn't appear to have been accepted by the asker, I figured it may still be helpful to provide an update: I have a reduction from 3SAT to MULTI-GAME. I haven't looked at Steven's answer carefully or followed through the link he provided, but based on the following reduction I won't be surprised if MULTI-GAME is indeed PSPACE-complete. I might not bother extending this result beyond NP-hardness, however.

A 3SAT instance consists of clauses $C_1, \dots, C_m$, each clause being of the form $C_i = L_{i1} \vee L_{i2} \vee L_{i3}$ where each $L_{ik}$ is either one of the variables $x_1, \dots, x_n$ or the negation of one of the variables.

Given such a 3SAT instance, the reduction creates a MULTI-GAME instance consisting of $n + 1$ games -- one for each variable and another game used as an excess capital sink. First we'll define the structure of the graphs for each game, then look at an example and discuss the core idea, and then we'll figure out what exact costs to assign to the edges to make the reduction hold firm.

First, the variable game graph $G_j$ for each variable $x_j$:

Create vertex labeled $x_j$ marked with an A (i.e. a winning vertex for Alice). The chip for $G_j$ starts on vertex $x_j$.
Create a vertex labeled $T$ and a vertex labeled $F$, each marked with a B (i.e. both are winning positions for Bob). Create directed edges from $x_j$ to both $T$ and $F$, both with costs of $1$.
For each literal $L_{ik}$ of clause $C_i$, if $L_{ik} = x_j$ or $L_{ik} = \neg x_j$, create vertices labeled $C_iTA$ and $C_iFA$ marked with A and vertices labeled $C_iTB$ and $C_iFB$ marked with B. Add edges $(T, C_iTA)$ and $(F, C_iFA)$ with costs both set to $l_{ik}$. (We'll define $l_{ik}$ later.)

Add edges $(C_iTA, C_iTB)$ and $(C_iTA, C_iTB)$. If $L_{ik} = x_j$, then set $(C_iTA, C_iTB)$'s cost to $l_{ik} - 1$ and $(C_iTA, C_iTB)$'s cost to $l_{ik}$. Otherwise set $(C_iTA, C_iTB)$'s cost to $l_{ik}$ and $(C_iTA, C_iTB)$'s cost to $l_{ik} - 1$.

The capital sink game:

Create a vertex labeled $C$, marked with B.
For each clause $C_i$, create a vertex labeled $C_iA$ marked with A, and a vertex labeled $C_iB$ marked with B. Create an edge $(C, C_iA)$ with edge cost $c_i$ (again to be determined below), and an edge $(C_iA, C_iB)$ also with edge cost $c_i$.

This is a lot to take in, so hopefully an example makes this a little more digestible. Our 3SAT instance is as follows:

$C_1 = x_1 \vee x_2 \vee \neg x_3$

$C_2 = x_2 \vee x_3 \vee \neg x_4$

$C_3 = \neg x_1 \vee \neg x_3 \vee x_4$

The reduction turns this instance into 4 variable game graphs and 1 capital sink graph. In the diagrams below, the red vertices are marked with A (i.e. are winning positions for Alice), and the cyan vertices are marked with B (are winning positions for Bob).

Graph for $x_1$:

Graph for $x_2$:

Graph for $x_3$:

Graph for $x_4$:

Graph for capital sink:

The idea is as follows:

Bob is forced to make the first $n$ moves in order to get out of losing positions in the $n$ variable games. Each such move encodes an assignment of true or false to the corresponding variable.

Alice will then have enough capital to make exactly 4 moves, each of which Bob will need to have enough capital to match in order for Bob to win. The $c_i$ values and the $l_{ik}$ values are to be chosen so that Alice's only possible winning strategy is as follows, for some clause $C_i$:

  Alice's clause $C_i$ strategy: let $C_i = L_{i1} \vee L_{i2} \vee L_{i3}$. For each $k \in \{1, 2, 3\}$, if $L_{ik} = x_j$ or $\neg x_j$, move to $C_i?A$ in the variable game for $x_j$. Also move to $C_iA$ in the capital sink game.

($C_i?A$ denotes either $C_iTA$ or $C_iFA$, only one of which is reachable in a given variable game after Bob's opening moves.)

If Bob's opening corresponds to a truth assignment that leaves some clause $C_i$ unsatisfied, then Alice choosing $C_i$ and implementing the strategy above costs Alice $l_{i1} + l_{i2} + l_{i3} + c_i$ capital to implement, and Bob the same to beat; if on the other hand $C_i$ is satisfied, then Bob's counterplay gets a discount of at least $1$. Our goal in setting the $c_i$ and $l_{ik}$ values and Alice and Bob's starting capitals is to ensure that said discount is the deciding factor in whether Alice or Bob wins.

To that end, set $b = m + 1$, and set

$l_{ik} = 2b^{10} + ib^{2k}$ for each $k \in \{1, 2, 3\}$,

$c_i = 3b^{10} + b^8 - \sum_{k=1}^3 ib^{2k}$,

Alice's starting capital to $9b^{10} + b^8$,

and Bob's starting capital to $9b^{10} + b^8 + n - 1.$

Note that all of these values are polynomial in $m$, so the MULTI-GAME instance outputted by the reduction has size polynomial in the size of the 3SAT instance even if these costs are encoded in unary.

Note also that for each clause $C_i$, $l_{i1} + l_{i2} + l_{i3} + c_i = 9b^{10} + b^8$ is Alice's starting capital. (Which is also $1$ greater than Bob's capital after making the first $n$ moves.)

First of all, it is immediately clear that if Bob's opening defines a truth assignment that leaves a clause $C_i$ unsatisfied, then Alice wins using her clause $C_i$ strategy given above.

If Bob's opening satisies all clauses, we can argue constraints on Alice's options which rule out any other possibility of Alice winning. Note that the order in which Alice makes her moves is irrelevant, as Bob's responses are forced and the total capital Bob will require to respond to Alice's moves is unchanged by the order of Alice's moves.

Alice can't make more than 4 moves: if Alice makes 5 or more moves, then her moves have a total cost of $\ge 5b^{10}$, which exceeds her budget.
Alice must make 4 moves: if Alice selects 3 moves from the capital sink game then her total cost is $\ge 9b^{10} + 3b^8 - 3b^7 > 9b^{10} + 2b^8$ which is over budget. If she selects even one move of 3 from a variable game, then her total cost is $\le 8b^{10} + 2b^8 + b^7$ which is is substantially less than Bob's post-opening capital, so Bob can easily afford the counterplay.
Alice must select a move from the capital sink game: if she doesn't, then she selects 4 moves from variable games, with total cost $\le 8b^{10} + 4b^7$, and again Bob can easily afford the counterplay. (Note that if there were a separate capital sink game per clause, we could even show that Alice must play in exactly one such game.)

From this stage we can disregard the $b^{10}$ and $b^8$ terms in the move costs chosen, as they will always sum to $9b^{10} + b^8$.
Since Alice must choose exactly one move in the capital sink game, assume that move is to $C_iA$. Then Alice has (ignoring $b^{10}$ and $b^8$ terms) $\sum_{k=1}^3 ib^{2k}$ capital remaining, and Bob has $1$ less than this amount remaining.

Alice must select at least one move costing $l_{j3}$ for some clause $C_j$: if she doesn't, then her moves cost (again lower-order terms) $\le 3b^5$, and Bob has more than enough capital for counterplay.
Said move costing $l_{j3}$ must be the move costing $l_{i3}$: it can't be a move costing $l_{j3}$ for $j > i$, otherwise this move alone costs $\ge (i+1)b^6$ which is greater than Alice's remaining budget. If it's $l_{j3}$ for $j < i$, then the $l_{(i - j)3}$ cost move must also be chosen by Alice to exhaust the $b^6$-order term in Bob's remaining budget. But then Either the $b^2$-order term in Bob's remaining budget or the $b^2$-order term doesn't get exhausted, so Bob wins handily.

Similar arguments should establish that Alice must select the moves costing $l_{i2}$ and $l_{i1}$. If Bob's truth assignment satisfies $C_i$, then even this strategy doesn't work, as the discount Bob gets on one of the $l_{ik}$-based costs makes up for the $1$ less capital he has after his opening.

A remark on my previous answer: it's obvious in hindsight that, for the TABLE-GAME variant of MULTI-GAME I defined in the comments of that answer, a knapsack-style DP suffices to determine which player has a winning strategy. You can argue that Bob's best strategy is to always respond to a losing state in a given game table with the minimal investment possible (this can't cut off a subsequent move for Bob that he would have otherwise), and from there that the order of Alice's moves doesn't matter. It then becomes a matter of choosing a split of Alice's capital among the games such that the sum of Bob's minimal winning responses over those games exceeds his budget, which can be reframed as a knapsack-style problem, which has a polynomial-time DP due to the unary representation of costs. (My recurrence actually would've worked for TABLE-GAME if I framed it in terms of Alice.)

It turns out that even a simple tree structure for each game, with constant depth and really only one meaningful fork per game (namely those at the start which force Bob to choose a truth assignment) is sufficient to get NP-hardness. I had some ideas for getting rid of that initial fork, which stalled out at somehow forcing Bob to invest a relatively large fixed amount of capital in $n$ games without Alice having to precommit to those games in advance, but obviously since TABLE-GAME is in P this is not possible without the fork.

I haven't thought much about your special case from UPD3. I suspect it's also NP-hard, for the reason that my variable gadgets seem at a glance like they may be adaptable to those constraints, but I probably won't look into it further.


Problem in deterministic time $n^p$ and not lower

For many years researchers have studied pebbling problems and emptiness/reachability problems.  Some of these problems have known unconditional resource lower bounds.

Such a problem $X$ is typically shown to have unconditional time complexity lower bounds by reducing the simulation of an $n^k$-time bounded Turing machine on a given input to an instance of $X$.  The time hierarchy theorem can then be applied to obtain the lower bound.

Here are two examples:

Pebbling games: A. Adachi, S. Iwata, T. Kasai. Some Combinatorial Game Problems Require Omega(n^k) Time. 1984
Intersecting one context-free language with k regular languages OR Intersecting k tree languages:  J. Swernofsky  and  M.  Wehar. On  the  complexity  of  intersecting  regular,  context-free, and tree languages. 2015

It's worth noting that there is a parameterized complexity class called $XP$ which contains parameterized problems that are solvable in $n^{f(k)}$ time.  A parameterized problem $X$ is $XP$-complete if every $XP$ problem is $fpt$-reducible to $X$.  There are a few known $XP$-complete problems.  Each $XP$-complete problem $X$ satisfies the property that there exist unbounded functions $f$ and $g$ such that for every $k$, $k$-$X \in DTIME(n^{f(k)})$ and $k$-$X \notin DTIME(n^{g(k)})$.

There are some parameterized problems $Y$ with finer reductions where we know that there exist $c_1 > 0$ and $c_2 > 0$ such that for all $k$, $k$-$Y \in DTIME(n^{c_1 k})$ and $k$-$Y \notin DTIME(n^{c_2 k})$.

Here is a post about the search for $XP$-complete problems: A list of XP-hard problems

I suspect that we could find a pebbling or reachability problem where it is solvable in cubic time, but not quadratic time (maybe intersecting three tree languages could work?).  However, this would require quite a bit of care and careful investigation of the existing Turing machine simulations.

This is a topic that I am very interested in.  Please always feel welcome to reach out if you would like to discuss this in more detail.  Thank you!


Reference request: pi-calculus with simultaneous events

Milner defines the SCCS calculus in [1]. This is a generalization of CCS where the actions form an abelian group, and where the communication rule is defined as in my question.
[1] Milner, R. Calculi for synchrony and asynchrony. 1983. https://www.sciencedirect.com/science/article/pii/0304397583901147


NEXPTIME-completeness with more time for reductions

The trouble with exponential-time reductions is that they may exponentially expand the input, and this leads to all sorts of weirdness.
So, to begin with, neither EXP nor NEXP is closed under exp-time reductions in the first place. The languages exp-time reducible to EXP-languages comprise EEXP (doubly exponential time, also written as 2-EXP) by an obvious padding argument, and likewise, the languages exp-time reducible to NEXP comprise NEEXP.
A related fact is that exp-time reductions are not closed under composition, hence the corresponding relation $\le_{\exp}$ between languages is not transitive: for example, if $L_0$, $L_1$, and $L_2$ are languages complete for P, EXP, and EEXP (respectively) under poly-time reductions, then $L_2\le_{\exp} L_1\le_{\exp}L_0$, but $L_2\nleq_{\exp}L_0$.
(The transitive closure of exp-time reductions consists of all Kalmár-elementary reductions, and likewise, the smallest class containing EXP or NEXP that is closed under exp-time reductions is ELEMENTARY.)
To answer the question, the classs of problems NEXP-complete under exp-time reductions is unconditionally different from either NEXP or from the class of usual NEXP-complete problems:
On the one hand, SAT is NEXP-complete under exp-time reductions, but since it belongs to $\mathrm{NP}\subsetneq\mathrm{NEXP}$ by the nondeterministic time-hierarchy theorem, it is not NEXP-complete under poly-time reductions.
(More generally, the class of languages NEXP-time complete under exp-time reductions includes all languages in NEXP that are NP-hard in the usual sense.)
On the other hand, the trivial languages $\varnothing$ and $\Sigma^*$ are not NEXP-complete under any kind of many-one reductions. If you want a nontrivial example, you have to assume $\mathrm{EXP\ne NEXP}$ (as any language in EXP exp-time reduces to any nontrivial language), but that is clearly also sufficient: if you take any nontrivial language $L\in\mathrm{P\subseteq NEXP}$, then $L$ is not NEXP-complete under exp-time reductions unless $\mathrm{EXP=NEXP}$.
If we restrict the exp-time reductions to time $2^{O(n)}$ (rather than $2^{n^{O(1)}}$) and refer to NE instead of NEXP, there is a simple characterization. The following are equivalent:

$L$ is NE-complete under exp-time (i.e., time-$2^{O(n)}$) reductions.

$L\in\mathrm{NE}$, and $L$ is hard for unary NP languages under poly-time reductions.

For 1→2, if $L_1\in\mathrm{NP}$ is a unary language, let $L_2=\{w\in\{0,1\}^*:1^w\in L_1\}$ be its binary encoding; then $L_2\in\mathrm{NE}$, thus there is a time-$2^{cn}$ reduction $f$ of $L_2$ to $L$. Then $x\mapsto f(|x|)$ is a reduction of $L_1$ to $L$ working in polynomial time $2^{c(\log n)}=n^c$.
For 2→1, if $L_2\in\mathrm{NE}$, its unary encoding $L_1=\{1^w:w\in L_2\}$ is in NP, thus $L_1$ reduces to $L$ via a poly-time reduction $f$. Then $w\mapsto f(1^w)$ is a $2^{O(n)}$-time reduction of $L_2$ to $L$.
For NEXP and time-$2^{n^{O(1)}}$ reductions, a similar characterization should work using hardness for unary nondeterministic quasipolynomial-time languages under quasipolynomial-time reductions.


What can the Haskell package category-extras be used for?

This library is not especially useful for category-theoretic proofs, since Haskell's typechecking is not sufficient to verify that the constructions satisfy the required properties. Surprisingly enough ;), it's actually intended to be used for writing Haskell programs. You are best off asking on the Haskell-cafe mailing list for examples.


A random walk that moves to less-visited nodes

The assumption here is that the input graph is not a disconnected graph. If it is then it will run forever since some of the nodes will never be reached from set of nodes.

Since the graph is undirected, at any point in time, the decision is made solely based on at what node you are and from that node a neighbor with least visited is going to be picked. So, it is possible that the node that is used to reach the current node may very well be next node to be visited (returning). As you visit the node, it increases the node's visited count and forces alternate node at next choice. Each node would have a visited count any where from 1 to N and no more than N without all nodes being visited.

The constraint that the next node to be visited be a least visited tracks whether node is visited or not and forcing to visit all nodes. Let us say that a global variable tracks the number of visited nodes. Whenever a node's visited counts goes from 0 to 1, increment this counter by 1 for the newly visited node. Until this count reaches the number of nodes in the input graph, we know that there exists some nodes that are not yet visited.

At every node, the unvisited node(s) gets priority over already visited nodes since the unvisited node's visited count is 0. So, initially it tracks like DFS and avoids cycle unless there is no other way. As you visit the node that is already visited, it increments the node's visited count there by making it least preferred till every node in the connected component's node weight to be increased as well. If there is another way to reach other unvisited nodes, then those nodes would be preferred and thereby making to find alternate path. If there is no other way, then we would end up back to articulation point which would have at least one node that is least visited. This least visited component would be now explored until all nodes in that component are visited.

The visited count of each articulation point would be number of nodes in the largest component it is connected to plus number of components it is connected to. Eventually, the largest count possible for a node in the graph is one plus the count of articulation point that has maximum of sum of largest component it is connected to plus the number of components it is connected to.

Therefore, the largest hitting time will be O(n^2).


What is mathematical difference between "random" and "unique"?

When you say random numbers you want to have a series of numbers such that given any sequence of $i-1$ numbers, the probability of the $i$th number having a certain value is independent from all its predecessors (I (over)simplify here), i.e.

$\begin{equation*}Pr[n_i = k \mid n_0, \dots, n_{i-1}] = Pr[n_i = k]\end{equation*}$

Unique numbers can be generated without having to guarantee that (e.g. just counting upwards yields unique numbers). These kinds of unique numbers can be guessed, which make them bad random numbers.

In fact, most things that are called random-number generators in practice are pseudo-random-number generators. That means that they have a perfectly deterministic and predictable algorithm of constructing the next number but they start with a secret seed that changes from application to application. Without knowing that seed the generated series have many properties of true random sequences. That can be checked by certain statistical methods.

In most practical, every-day scenarios you want to have unguessable sequences, e.g. for password creation. Pseudo-random-number generators are fine for that provided you choose a proper seed; many people use the system timestamp when the request comes in, assuming this is pretty hard to predict up to the millisecond. If you really need the statistical properties of random sequences, for example for Monte Carlo simulations, you should be more wary.

Edit: To clarify: Random sequences (R) and unique sequences (U) are not opposing concepts; you can have all combinations of both:

R, !U: roll die (or observe other allegedly random event, see random.org)
R, U: roll a die with lots of sides and reject duplicates ( or roll many dice)
!R, U: use any bijective enumeration scheme, e.g. $f(n) = n$
!R, !U: $1,1,1,\dots$ (also: PRNG)


Reference for the fact that (0=1) implies false requires a universe in MLTT

I know of:

Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.


Can decoying provide security against traffic analysis?

How can Bobs prove that their transmissions are junk? Given that the transmissions can be encrypted using information theoretically secure one-time pads (OTPs), it is not possible to prove that they are not significant messages. Even if the messages from Bobs would be assumed to be encrypted with a single cipher of a good grade (AES?) it would be very hard to show that there is no key that decodes a given message into meaningful content, because, assuming such a method would exist, it would simultaneously show that the cipher (AES?) is broken. A statistical method showing that a message from a Bob cannot be an AES-encrypted message would correspond to a distinguisher for AES and that would also signal that it is a weak cipher.


Regarding question A, it is possible to adapt the PRNG to yield uniformly distributed numbers using this. However, the range of this new uniform generator has size smaller than $K$, unless the PRNG is itself uniform. The number of possible outcomes of this new generator will depend on the min-entropy of the original generator.

To get some intuition on why this is so, try to view the problem from an adversarial point of view where the goal is to guess the outcome of the PRNG. If $P_{guess}>1/K$ is the probability of the most probable outcome of the PRNG, then there is no deterministic way to lower the adversary's guessing probability without adding randomness. Therefore if you are to transform the outcome to a uniform distribution then all the equaly likely outcomes must happen with probability at least $P_{guess}$, so there can be at most $1/P_{guess}$ outcomes. Of couse, I'm assuming that the adversary knows the deterministic procedure that is applied, as is usually the case in cryptography.

So the answer to question B is that this nesting trick does not increase randomness, it can only decrease it. There is no deterministic procedure that can increase randomness.

Hope this helps