Say that a universe $U$ is impredicative if the product $\prod_{x : A} B(x)$ is in $U$ whenever $B(x)$ is in $U$ for all $x$, and $A$ is arbitrary, i.e., not necessarily in $U$.

Are there any impredicative universes? Let us think about what an impredicative universe would be for sets: a set $U$ such that for every family of sets $B : A \to U$, no matter how large $A$ is, $\prod_{x : A} B(x)$ is in $U$. That's only possible in two cases: when $U$ contains the singleton (or many copies of it) and when it contains the empty set and the singleton (or many copies of it). This is so because a product of sets which are all singletons or empty is again such a set. If $U$ contains a set $S$ with at least two elements then $S^U$ (which is a special case of a product) will fail to be contained in $U$ for cardinality reasons.

Of course, we recognize that the case $U = \{\emptyset, \{\emptyset\}\}$ is just the case when $U$ is the set of truth values, i.e., $\mathsf{Prop}$. This is one reason why $\mathsf{Prop}$ is treated differently: it is impredicative – not only in classical set theory but also more generally, because truth values are closed under $\forall$. Note that $\forall$ and $\prod$ coincide on families of sets that all contain at most one element.

In system $F$ we have impredicativity because types there are closed under $\forall$ ranging over the whole universe of types, and $\forall$ behaves like $\prod$.

One could hope that there are other models, where for instance $\mathsf{Type}_i$ is impredicative. Indeed, there are realizability models of (extensional) type theory that contain an impredicative universe of sets (as opposed to truth values). However, one cannot have two impredicative universes such that one is a member of the other, because one can then cook up a Burali-Forti paradox.


Proofs obtained only through spectral graph theory


Consequences of $\oplus \mathbf{P} \subseteq \mathbf{NP}$

There are two oracle sets defined in T88 such that ${\bf NP^A \not \subseteq \oplus P ^A}$ and ${\bf \oplus P^B \not \subseteq NP^B}$.


Data structures in programming language with linear types

Linearity is not a sufficient constraint to pin down a unique stateful representation, and so the answer to your question depends on how you interpret linear logic in terms of state. This will typically be reflected in how you must interpret the $!A$ modality.

If your intended semantics of references says that all pointers are unique values (i.e., there is at most a single reference to an object) then dags and graph structures are not expressible, for the sort of tautological reason that a dag may contain multiple references to the same object. In this case, $!A$ must be a computation which creates a new value of type $A$, since you want maps $\delta_A : !A \multimap !A \otimes !A$ and $\epsilon_A : !A \multimap A$.

However, suppose that you want $!A$ to represent sharing. Then, objects can be garbage-collected with reference counting, with the maps  $\delta_A : !A \multimap !A \otimes !A$ and $\epsilon_A : !A \multimap A$ can be realized as operations which just bump reference counts. In this case, you can't use linearity to assume that it's always safe to mutate values, since there's sharing. But you can ensure that all memory allocation is explicit in your program, and that there are no cycles in the heap.

Most practical implementations of linear types use neither of these two interpretations. Instead, references are viewed as freely duplicable entities, and what we track linearly are in fact capabilities. Capabilities are not runtime values; they are purely conceptual entities which are intended to represent the permission to access a reference. The idea is that you program in a permission-passing style, and so even if there are many references to the same object, a read or modification of a piece of state can only occur if you also have the capability to access it. And since the capability is linear, you know that only you can change it.

$$
\array{
\mathsf{new} & : & \forall \alpha. \;\alpha \multimap \exists c : \iota. \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\
\mathsf{get} & : & \forall \alpha, c:\iota. \;\mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \multimap \alpha \otimes \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\
\mathsf{set} & : & \forall \alpha, c:\iota. \;\mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \otimes \alpha \multimap \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\
\mathsf{copy} & : & \forall \alpha, c:\iota.\; \mathsf{ref}(\alpha,c) \multimap \mathsf{ref}(\alpha,c) \otimes \mathsf{ref}(\alpha,c)
}
$$

In the API sketched above, $c$ ranges over $\iota$, some domain of compile-time indices, and $\alpha$ ranges over types. We have a type $\mathsf{cap}(c)$ which is a capability indexed by $c$, and a type $\mathsf{ref}(\alpha, c)$, which is a type of references to $\alpha$ accessed by a capability $c$. Calling $\mathsf{get}$ and $\mathsf{set}$ on a reference requires the capability $c$, and calling $\mathsf{new}$ creates a new reference and a new capability sharing a common index. However, $\mathsf{copy}$-ing a reference does not require access to any capability, so anyone can copy a reference as long as they don't look inside it.


Is it possible to prove that a game(ex. chess or othello...) will eventually halt at some point.

You can make games that will halt and those that won't.  Othello will always halt because it cannot continue for more than 60 moves based on the rules.  Chess ends only because there are rules to prevent infinite-move games (repetition rule, 50-move rule, etc).  You can certainly construct games that never end... a silly example is "whoever names the highest integer wins".

Then there are games that lead to a paradox when you try and ask if they will end or not.  A famous example is the game called CHOICE.  The first move of CHOICE is to choose a game that does eventually end.  The 2nd move of CHOICE is to play the first move of the chosen game, etc.

Now we ask, "does CHOICE end or not?"  If you say it does, then the first move of CHOICE could be to choose CHOICE, and continuing this way leads to a never-ending game.  So suppose we say CHOICE does not end, thereby disqualifying it as a possibility for the first move.  Then clearly it DOES end.


Implications of Riemann Hypothesis variants in TCS

First, I’m not aware of any CS application of Riemann’s hypothesis as such. There are various applications of generalizations of RH.

Second, a terminological note: contrary to popular belief, there is no such thing as “the generalized Riemann hypothesis” or “the extended Riemann hypothesis”. Both of these terms are used more-or-less interchangeably in the literature as a loose denotation of any kind of generalizations of the RH to some class of $L$-functions. They have no fixed specific meaning, or at least none consistent across papers of different authors (or even different papers of the same author).

The result mentioned in the OP is based on a result of Koiran that the existential theory of $\mathbb C$ (which commonly goes under the confusing name “Hilbert’s Nullstellensatz”) is in AM, and therefore in the polynomial hierarchy. It assumes the RH for Dedekind $\zeta$-functions; specifically, it relies on an effective version of the Chebotarev density theorem.

Another class of CS applications exploit the fact that every nontrivial quadratic Dirichlet character modulo $m$ assumes $\chi(x)=-1$ for some $x=O((\log m)^2)$, originally due to Ankeny, often stated with a reference to Bach who improved the constant in the $O$-notation. It relies on the RH for $L$-functions of quadratic Dirichlet characters, which is weaker than the one for Dedekind $\zeta$-functions. (The result actually holds more generally for finite-order Hecke characters, and in full generality it needs the RH for $L$-functions of said Hecke characters, which is in fact equivalent to the RH for Dedekind $\zeta$-functions. However, the CS applications I’m aware of do not need this.) The consequences are that one can derandomize several algorithms, such as the Miller–Rabin primality testing algorithm, or the Shanks–Tonelli algorithm for computing square roots modulo primes.

As far as I know, RH is not useful to deterministically find primes in a given interval, as alluded to in a comment above. This would follow from Cramér’s conjecture or a similar bound on prime gaps, but the RH is too weak to prove such bounds (the error term in the prime number theorem is at least of order roughly $\sqrt x$ no matter what).


hardness of approximation result for a Min-CSP, by reduction from PCPs

One reason we see Max-CSPs more is that they often capture convex optimization problems for which minimization is easy (e.g., Max-CUT vs Min-CUT).

A Min-CSP is equivalent to a Max-CSP when you negate all the constraints. So minimization and maximization are equivalent if you're asking for the optimum solution. But this reduction is not approximation preserving in the sense that, say, a constant factor approximation of the negated CSP does not necessarily imply a constant factor approximation of the original CSP. Approximation of Max-CSPs and Min-CSPs can however be studied under the unified framework of "generalized CSPs", when constraints have weights and can be fractionally satisfied. Prasad Raghavendra's thesis is a good resource about this.

The specific problem of Vertex-Cover is not really a CSP in the standard sense. However the approximation of the problem is captured by the so-called "free-bit complexity" of PCPs. See "Free bits, PCPs and non-approximability -- towards tight results" by Bellare, Goldreich, and Sudan.


Are social networks typically good expanders?

Social networks typically have many vertices with just one or two connections to the rest of the graph. Such vertices will typically lead to a bad spectral gap.

What you could hope for is good vertex/edge expansion for sufficiently large sets. However, if you have tightly-knit communities within the network, then again you would expect low expansion.

I'm not sure if it quite answers your question, but the following empirical paper looks at exactly expansion-like properties in social networks. The answer seems to vary from network to network.
http://fragkiskos.me/papers/expansion_SNSMW11.pdf

I'm sure there is other work out there along these lines, possibly disguised using alternate terminology ("community structure", cut sizes, etc).


What is an unambiguous language in the sense of Schützenberger?

Jean Berstel maintains a website with Schützenberger's collected papers. You can access the original paper (in French) here.
A definition of the unambiguous product you are referring to in English is given by Pin in Syntactic Semigroups, p.30:
"The product $L = L_0a_1L_1 \cdots a_nL_n$ is unambiguous if every word $u$ of
$L$ admits a unique factorization of the form $u_0a_1u_1 \cdots a_nu_n$ with $u_0 \in L_0, \cdots, u_n \in L_n$."
I recommend reading the following survey by Diekert, Gastin and Kufleitner for more background information. They refer to the concept of unambiguous product as "unambiguous monomial".

References:

J.-E. Pin, Syntactic semigroups, Chap. 10 in Handbook of language theory, Vol. I, G. Rozenberg and A. Salomaa (éd.), Springer Verlag, (1997), 679-746.
Volker Diekert, Paul Gastin, and Manfred Kufleitner. A survey on small fragments of first-order logic over finite words. International Journal of Foundations of Computer Science, 19(3):513-548, June 2008. Special issue DLT 2007.


Is there any work on purely functional approximation algorithms?

I'm consolidating my comments into an answer.

First, it is hard to make being "awkward to implement" precise, so an empirical study of program length or development time for a number of approximation algorithms is in order to answer that question.

From a more theoretical viewpoint, every algorithm that can be implemented on a RAM with runtime $f(n)$ can be implemented in a purely functional language with runtime at most $O(\log n * f(n))$. This is because functional languages are turing complete and the simulation of mutable, random access memory via search trees causes logarithmic slowdown. Chris Okasaki's Purely Functional Data Structures shows how to implement search trees in a functional language.

Nowadays many approximation algorithms are designed for huge datasets and are written in the language of MapReduce or Pregel. This type of algorithm is very easy to translate to functional languages, as these distributed computing paradigms generally avoid stateful computations.

As a comment below notes, this question on Stack Overflow is closely related. In particular Edward Kmett gives references that show that under strict evaluation (i.e. not like the lazy evaluation you see in Haskell) there are examples where the logarithmic slowdown is necessary. It seems to be open whether this is also true in lazy settings.


Can this formulation be trivially extended for each constructor by simply adding a Ci for an additional inductive case?

Yes. I can't provide a general nor a technical answer, but a while ago I was trying to solve a similar problem and someone helped me by providing a visualization of the general procedure. This helped me a lot, so I'll reproduce it here in the case it helps you too.

Generating the elimination principle

Given an inductive type of the form (using Agda syntax):

data Foo : (index_0 : I_0) -> ... (index_N : I_N) -> Set where
  ctor_0 : (field_0 : F_0) -> ... (field_N : F_N) -> ret_0
  ...
  ctor_N : (field_0 : F_0) -> ... (field_N : F_N) -> ret_N

Its elimination is, generally, in that form:

let Foo_match =

    -- Index arguments
    (index_0 : I_0) -> ...
    (index_N : I_N) ->

    -- Scrutinee
    (X : Foo index_0 ... index_n) ->

    -- Motive
    (P :
      (index_0 : I_0) -> ...
      (index_n : I_N) ->
      (witness : Foo I_0 ... I_N) ->
      Set) ->

    -- Constructor arguments
    (ctor_0 :
        (field_0 : F_0) -> ...
        (field_N : F_N) ->
        ret_0[Foo/P] (ctor_0 field_0 ... field_N)) ->
    (ctor_N :
        (field_0 : F_0) -> ...
        (field_N : F_N) ->
        ret_N[Foo/P] (ctor_N field_0 ... field_N)) ->

    -- Result type
    P index_0 ... index_N X

Where [Foo/P] means we replace the constructor type by the variable P in ret_N.

Example

If our type is:

data Vect : (A : Set) -> (n : Nat) -> Set where
  cons : (A : Set) -> (n : Nat) -> (x : A) -> (xs : Vect A n) -> Vect A (succ n)
  nil  : (A : Set)                                            -> Vect A zero

Then we get:

let Vect_match =

    -- Index arguments
    (A : Set) -> ...
    (n : Nat) ->

    -- Scrutinee
    (X : Vect A n) ->

    -- Motive
    (P : (A : Set) -> (n : Nat) -> Vect A n -> Set) ->

    -- Constructor arguments
    (cons :
        (A  : Set) ->
        (n  : Nat) ->
        (x  : A) ->
        (xs : Vect A n) ->
        P A (succ n) (cons A n x xs)) ->
    (nil :
        P A zero nil) ->

    -- Result type
    P A n X

Note: I've not included parameters, but they're trivial. They work like indices, except they're not included on the constructors. I've also not included the inductive argument, so this is not actually the elimination principle, just total pattern-matching. You can get induction by applying Foo_match recursively to sub terms. Problem is I don't remember out of my head its shape, but someone is welcome to edit in.


Class of languages recognizable by single-tape 3-state TMs

The beast is extremely powerful, for example we can build a TM $M$ that  accepts every string of the form

$L_Y = \{ r\; 0^n \; 1^m\;A \mid m \leq n \}$

and rejects every string of the form

$L_N = \{ r\; 0^n \; 1^m\;A \mid m > n \}$

The idea is to transform the first $r$ into $R$ and then let the head reach the middle of the string then do a "stateless"  zig-zag; if it reaches $A$ before $R$ then it accepts.

Informal description:

on $r$ write $R$ and move right (prepare for rejecting)
on $0$ write $c$ and move right (moving toward the center)
on $1$ write $>$ and move left (mark a $1$, prepare for next left-to-right crossing, and go left)
on $c$ write $<$ and move right (mark a $0$, prepare for the next right-to-left crossing, and go right)
on $<$ write $>$ and go left (left-to-right crossing, prepare for next  right-to-left)
on $>$ write $<$ and go right (right-to-left crossing, prepare for next  left-to-right)
on $A$ accept, on $R$ reject
on blank $b$ reject

Example:

  :r 0 0 0 1 1 A
   R:0 0 0 1 1 A
   R c:0 0 1 1 A
   R c c:0 1 1 A
   R c c c:1 1 A
   R c c:c > 1 A
   R c c <:> 1 A
   R c c < <:1 A
   R c c <:< > A
   R c c:< > > A
   R c:c > > > A
   R c <:> > > A
   ...
   R c < < < <:A ACCEPT

This zig-zag technique is used in the smallest 2-states Universal Turing machine (it has 18 symbols) constructed by Rogozhin (Rogozhin 1996. TCS, 168(2):215–240)).

Some attention should be paid in order to prove that $M$ halts on all inputs (just note that it rejects on blank input and all non-halting symbols "converge" to  $<$ or $>$ which cannot lead to an infinite loop).

As commented by DavidG, the language $L(M)$ recognized by $M$ is a superset of $L_Y$ (i.e. $L_Y \subset L(M)$) but it doesn't contain any string from $L_N$ (i.e. $L(M) \cap L_N = \emptyset$) and - as commented by MikhailRudoy - this is enough to prove that $L(M)$ is not regular.

Indeed if $L(M)$ is regular then also $L(M) \cap \{ r0^*1^*A \} = L_Y = \{ r0^n 1^mA \mid m \leq n \}$ would be regular (which is not by a simple application of the pumping lemma); leading to a contradiction.

So $L(M)$ is not regular.

... But like all superheroes $C_3$ has an Achille's heel: it cannot even recognize the regular:

$L = \{ 1^{2n} \}$

Informally it can use only the leftmost $b 1 ...$ ($b$ is the blank symbol) or the rightmist $1b...$ as a hook and "expand" in the other direction; but the final Accept or Reject cannot be on the blank symbol of the opposite side, so it can be done only on the inner part of the $1$s and starting from a long enough input it can be "faked" stretching it by one.

Finally - after reading the paper - I can confirm that the one-state TM described in it matches your $C_3$ class ... (so nothing new here :-) ...and the langauge used by the author to prove that it contains non-regular languages is very similar to mine.


A definition of computable numbers that requires to "wait an infinite amount of time" to get the correct result; how to make this precise

This is not a research-level question, but since the general level of interest seems high, here is an answer. I cannot guess from your question whether you're shooting for something that will result in the usual computable numbers, or you're trying to surpass that.

First we have Turing's definition of computable real number, and it is the one others have been commenting on: a real number $x \in \mathbb{R}$ is said to be computable if any one of the following holds:

(Calculation fo approximations) There is a Turing machine $M$ which on input $n$ terminates outputs a pair of integers $(a, b)$ such that $|x - a/b| < 2^{-n}$.
(Calculation of digits) There exists a Turing machine $M$ which runs forever and writes out the digits of $x$ on an infinite write-once tape. That is, once it writes a digit, it cannot change it.
(Calculation of neighborhoods) There exists a Turing machine $M$ which on input $(p,q)$, where $p$ and $q$ are rational numbers, terminates if, and only if, $p < x < q$.

There are many other equivalent definitions.

We can also ask about various other kinds of computability, and we shall discover a hierachy of classes of reals, see for instance X. Zheng's Classification of the Computable Approximations by Divergence Boundings. One can also study subclasses of computable reals, see again X. Zheng's work.
For instance, we can try these:

(Mind-change computability) A real $x$ is computable with $k$ mind changes if there exists a Turing machine $M$ which runs forever and writes its digits on an output tape. While so doing, it may change its mind about any particular digits at most $k$ times, for some fixed $0 \leq k < \infty$. A variant allows computations where every digit eventually stabilizes, i.e, the number $k$ is not fixed to be the same for all digits.
(Oracle computation) A real $x$ is computable with oracle $A$ if there is an oracle Turing machine $M$ such that $M^A$ computes $x$ (in any of the senses above).
(Infinite-time Turing machine computation) A real $x$ is infinite-time Turing computable if there exists an infinite-time Turing machine $M$ which computes $x$ (in any of the senses above).
(Definable real number) A real $x$ is definable, say in the language of set theory, if there exists a formula $\phi$ such that $\phi(x)$ holds and, if $\phi(y)$ holds for any $y \in \mathbb{R}$ then $y = x$.

I am guessing you had in mind some sort of mind-change computability. It is stronger than the usual computability.


The issue may be whether or not Schwartz and Sharir show that motion plan existence is many-one polynomial time reducible to $\exists\mathbb R$.

If they need several queries to $\exists\mathbb R$ for a given motion plan existence instance, then that's not a many-one reduction.


Fast Computation of First k Eigenvectors of Graph Laplacian

Answer to Q1:

In [1], it is argued at the end of section 1 that the first k eigenvectors can be approximated in time roughly $O(mk)$ (up to log-factors), with $m$ the number of edges. They are not very precise in their statement however, but I'm not aware of a better reference explictly stating this.

Answer to Q2:

No, this will not hold in general. You are describing a $k$-dimensional embedding of the nodes $[n] \to \mathbb{R}^k; i \mapsto U_{i,1:k}$, as is used in for instance spectral clustering. For nodes $i, j$ which lie in the same cluster (e.g., in the same clique of a dumbbell graph), the quantity $\|U_{i,1:k} - U_{j,1:k}\|_2$ will be small for sufficiently small $k$. On the other hand, if $i \neq j$ then $U_{i,:}$ is orthogonal to $U_{j,:}$ and hence $\|U_{i,:}-U_{j,:}\| = \sqrt{2}$.

[1] Koutis et al. "Faster spectral sparsification and numerical algorithms for sdd matrices." (2015)


Approximation algorithms for multicut for special classes of graphs

Check the following survey:

Marie-Christine Costa, Lucas Létocart, and Frédéric Roupin, "Multicut and integral multiflow: a survey", 2005

You can also check my dissertation on the directed case.


what is known about efficient set intersections

When you want to know about a specific problem, it is always good to start with reading a recent paper.  I recommend you to read this paper and the references therein.

Bolin Ding, Arnd Christian König: Fast Set Intersection in Memory. PVLDB 4(4): 255-266 (2011)


Relation between Code Length and Symbol Weight in a Huffman Code

Yes. A Huffman code is optimal. If a less frequent symbol had a shorter code length than a more frequent symbol, then you could get a code with better performance by exchanging them.


Does this notation have a special meaning?

No special meaning here. The angle brackets simply denote a tuple or pair. The author chose the angle brackets to look prettier than the usual round parentheses. Thus a graph $G$ is a set of vertices $A \cup L$ and a set of edges $E$.


Is there a fine grained relation between LH and AC0?

Here are the definitions that make it work. Fix $d\ge1$:

Let $\Sigma_d\text-\mathrm{TIME}(f(n))$ denote the set of languages recognizable in time $O(f(n))$ by an alternating Turing machine that starts in an existential state, and makes at most $d-1$ alternations. Since we are interested in logarithmic time, we work in a model where we do not have an input tape, but we can access the input by writing on a query tape the index of an input position in binary, and its assumed value, and asking the input oracle if our assumption is correct. Additionally, we require that the ATM makes only one such query, at the very end of the computation, and returns the answer of the oracle as the result of the computation. (In order to make this feasible, we need to stipulate that the machine starts with the input length $n$ written in binary on one of its tapes. A log-time TM can compute the length of its input, but it needs $\Omega(\log n)$ input queries to do that.)
A Boolean formula or circuit is $\Sigma_d$ if it consists of $d$ alternating layers of (unbounded fan-in) conjunctions and disjunctions, the top layer being a disjunction, and a layer of literals (variables and negated variables) at the bottom. A language is in non-uniform $\Sigma_d\text-\mathrm{AC}^0$ if it is computable by a family of polynomial-size $\Sigma_d$ circuits $\{C_n:n\in\mathbb N\}$. A language is in DLOGTIME-uniform $\Sigma_d\text-\mathrm{AC}^0$ if, additionally, we can enumerate the nodes of $C_n$ by numbers of $O(\log n)$ bits in such a way that we can compute the following in (deterministic) time $O(\log n)$:

Given $n$ and $u$, check if $u$ is the output node of $C_n$.
Given $n$ and $u$, find the type ($\land$, $\lor$, variable, negated variable) of node $u$ in $C_n$.
Given $n$, $u$, and $v$, determine if there is a wire from node $v$ to $u$ in $C_n$, or if $u$ denotes variable number $v$ or its negation.

  Proposition: For any $d\ge1$, $\Sigma_d\text-\mathrm{TIME}(\log n)$ equals DLOGTIME-uniform $\Sigma_d\text-\mathrm{AC}^0$.

Note that the definition of DLOGTIME uniformity above refers to more-or-less the standard direct connection language of the circuit. It is not sensitive to minor changes in the definition.

On the other hand, the restriction to input queries only at the end in the definition of $\Sigma_d\text-\mathrm{TIME}(\log n)$ does appear to be significant. I cannot exactly characterize the class without this restriction, but it is somewhere between DLOGTIME-uniform $\Sigma_d\text-\mathrm{AC}^0$ and $\Sigma_{d+\frac12}\text-\mathrm{AC}^0$, where a $\Sigma_{d+\frac12}$-circuit is a $\Sigma_{d+1}$-circuit whose bottom layer only allows connectives of fan-in $O(\log n)$.

The proof of the proposition is fairly straightforward.

On the one hand, a language described by a DLOGTIME-uniform family of $\Sigma_d$ circuits can be evaluated by an ATM in a top-down fashion: in the initial existential state, we guess (and check) the top node of the circuit, which is a disjunction, and nondeterministically choose one of its input conjunction nodes. We switch to a universal state, and co-non-deterministically choose the next node. We proceed this way down the circuit. At the bottom layer of connectives, we (existentially or universally, as appropriate) choose not only the next node, which is a literal, but also its type ($x_v$ or $\neg x_v$). Then we make an input query to find the value of the literal, and return it.

On the other hand,  consider a language computable by a $\Sigma_d\text-\mathrm{TIME}(\log n)$ machine. We may assume that as the machine computes, it records a log of the states it has been in (which in particular tells us if it is in an existential or universal state, how many alternations it went through, and which nondeterministic choices it has taken). Let $C_n$ be the circuit whose nodes are certain configurations of the ATM on inputs of $n$ bits, namely: the initial configuration; the final query configurations; and configurations just after an alternation between existential and universal states. The type of a non-final node is $\lor$ or $\land$ according to if the corresponding configuration is existential or universal. There is a wire from $v$ to $u$ if there is an alternation-free computation path from $u$ to $v$; note that this computation path is uniquely determined by $v$’s log, hence it can be checked in DLOGTIME.


A small C-like language that turing machines can simulate

If your students have done any functional programming, the nicest approach I know is to start with the untyped lambda calculus, and then use the bracket abstraction theorem to translate it into SKI combinators. Then, you can use the $smn$ and $utm$ theorems to show that Turing machines form a partial combinatory algebra, and so can interpret the SKI combinators.

I doubt this is the simplest possible approach, but I like how it rests  on some of the most fundamental theorems in computability (which you may well wish to cover for other reasons).

It appears that Andrej Bauer answered a similar question on Mathoverflow a few months back.
If you are set on a C-like language, your path will be a lot rougher, since they have a rather complicated semantics -- you'll need to

Show that Turing machines can simulate a stack and a heap at the same time, and
Show how variables can be implemented with a stack, and
Show that procedure calls can be implemented with a stack.

This is much of the contents of a compilers class, honestly.


Allender suggests the answer is no:

  There seems to be no pair of natural NP-complete problems A and B known, where a reduction from A to B is known to require more than linear time (even under the assumption that P $\ne$ NP)

Reference:

E. Allender and M. Koucký, Amplifying lower bounds by means of self-reducibility. Journal of the ACM 57, 3, Article 14 (March 2010).


Intractability of NP-complete problems as a principle of physics?

I don't think that the fact that $P\neq NP$ is an asymptotic statement is an automatic "dealbreaker". One can make concrete conjectures that are consistent with our knowledge but stronger than P vs NP such as "It takes at least $2^{n/10}$ steps to find a satisfying assignment for a random n variable 10SAT formula" (with "random" being e.g., the planted model of Achlioptas Coja-Oghlan, this is just an example - I don't know what are reasonable concrete numbers offhand).

Such conjecture can result in a refutable prediction that any natural system that will try to solve this will fail (e.g., get stuck in a local minima), something you can verify with experiments. Indeed, I'm not an expert on this but to my knowledge, as Joe Fitzsimons mentioned, such predictions had been confirmed with Adiabatic computing. (Scott Aaronson also had some entertaining experiments with soap bubbles.)

Of course you can also see some "empirical evidence" for $P \neq NP$  in the fact that people have been trying to solve optimization problems, cryptoanalyze encryptions, etc.. and haven't been successful so far...


Is counting simple cycles in $P$ for graphs of bounded tree width?

A simple cycle is a connected set where every vertex has degree 2. Then you have a formula SC(X) stating X (a set of edges) is a simple cycle. You can see many versions of Courcelle's theorem for listing and counting. You can refer to this book or this paper


Palindrome language and Finite Automata Machines

Regarding probabilistic (and quantum) automata, you may start by digging this survey: https://arxiv.org/abs/1507.01988

For very recent results on quantum automata, you may check two recent works by Zachary Remscrim: https://eccc.weizmann.ac.il/author/659/

Palindrome is an (exclusive) stochastic language, but a probabilistic machine requires log-space to recognize it with bounded error. Two-way quantum automata recognizes palindrome language with bounded-error in super-polynomial time.


Complexity of computing the average distance of a graph

Computing ad(G) in $O(n^{2-\delta})$ time for constant $\delta>0$ even in graphs with $\tilde{O}(n)$ edges and $n$ vertices would imply that the Strong Exponential Time Hypothesis (SETH) is false. (SETH was defined by Impagliazzo, Paturi and Zane'01 and implies that CNF-SAT on $n$ variables does not have $O(2^{(1-\varepsilon)n})$ time algorithms.)

To prove this, note that we recently proved in (Fast approximation algorithms for the diameter and radius of sparse graphs, Liam Roditty, V. Vassilevska Williams. STOC'13.) that if one can distinguish between graphs of diameter 2 and 3 in subquadratic time, then SETH is false.
The proof goes via a reduction from CNF-SAT.
The same reduction can be used to show that computing ad(G) in subquadratic time shows that SETH is false, as the average distance in the graphs in the reduction would be $2-M/{N\choose 2}$ (where $N$ and $M$ are the number of nodes and edges in the reduction instance) if the CNF-SAT instance is not satisfiable, and more than that if there is a satisfying assignment.


How can the actor model be applied to allow pure functional languages to have side-effects?

Erlang is an example. I actually don't know Erlang, so I'm going to use some pseudocode:

Suppose you have two threads, Alice and Bob. They talk by calling each other's Send member route, which blocks until the other end replies. Alice can keep some "mutable state" for a single integer as follows:

Alice:
  function main_loop(state):
     message = Receive()
     if message == "get":
        Reply(state)
     else
        Reply("Okay")
        main_loop(message)
  main_loop(0)

Bob:
  Alice.Send(100) // Store 100 into the mutable state
  Alice.Send("get") // obtain the 100
  Alice.Send(200) // Store 200
  Alice.Send("get") // get the 200


Proof nets are interesting essentially for three reasons:

1) IDENTITY OF PROOFS. They provide an answer to the problem "when are two proofs the same"? In sequent calculus you may have many different proofs of the same proposition which differ only because sequent calculus forces an order among deduction rules even when this is not necessary. Of course, one can add an equivalence relation on sequent calculus proofs, but then one has to show that cut-elimination behaves properly on equivalence classes, and also it is necessary to turn to rewriting modulo, which is quite more technical than plain rewriting. Proof nets solve the problem of dealing with equivalence classes by providing a syntax where every equivalence class is collapsed on a single object. This situation is anyway a bit idealistic, as for many reasons proof nets are often extended with some form of equivalence.

2) NO COMMUTATIVE CUT-ELIMINATION STEPS. Cut-elimination on proof nets takes a quite different flavor than on sequent calculi because commutative cut-elimination steps disappear. The reason is that in proof nets the deduction rules are connected only by their causal relation. Commutative cases are generated by the fact that one rule can be hidden by another causally unrelated rule. This cannot happen in proof nets, where causally unrelated rules are far apart. Since most cases of cut-elimination are commutative one gets a striking simplification of cut-elimination. This has been particularly useful for studying lambda calculi with explicit substitutions (because exponentials = explicit substitutions). Again, this situation is idealized since some presentations of proof nets require commutative steps. However, their number is much smaller than in sequent calculus

3) CORRECTNESS CRITERIA. Proof nets can be defined by translation of sequent calculus proofs, but usually a system of proof nets is not accepted as such unless it is provided with a correctness criterion, i.e. a set of graph-theoretical principles characterizing the set of graphs obtained by translating a sequent calculus proof. The reason for requiring a correctness criterion is that the free graphical language generated by the set of proof net constructors (called links) contains "too many graphs", in the sense that some graphs do not correspond to any proof. The relevance of the correctness criteria approach is usually completely misunderstood. It is important because it gives non-inductive definitions of what is a proof, providing shockingly different perspectives on the nature of deductions. The fact that the characterization is non-inductive is usually criticized, while it is exactly what is interesting. Of course, it is not easily amenable to formalization, but, again, this is its strength: proof nets provide insights that are not available through the usual inductive perspective on proofs and terms. A fundamental theorem for proof nets is the sequentialization theorem, which says that any graph satisfying the correctness criterion can be inductively decomposed as a sequent calculus proof (translating back to the correct graph).

Let me conclude that it is not precise to say that proof nets are a classical and linear version of natural deduction. The point is that they solve (or attempt to solve) the problem of the identity of proofs and that natural deduction succesfully solve the same problem for minimal intuitionistic logic. But proof nets can be done also for intuitionistic systems and for non-linear systems. Actually, they work better for intuitionistic systems than for classical systems.


A reduction proof of SK-security for the Needham-Schroeder-Lowe protocol

I am not an expert on this subject, but it looks to me like the question makes some assumptions that may or may not be valid.  The question claims that the Needham-Schroeder-Lowe protocol is SK-secure.  However, I don't know whether there is any known proof that Needham-Schroeder-Lowe is SK-secure.  The paper that was cited in the question does not appear to claim that it is SK-secure.  You might want to start by first checking whether there's a known proof of its SK-security.

It's possible you might find the following paper of some relevance:

A Computational Analysis of the Needham-Schroeder-(Lowe) Protocol.  Bogdan Warinschi.  Computer Security Foundations Workshop 2003.

It gives a computational, reduction-oriented proof of security for the Needham-Schroeder-Lowe protocol, assuming that the encryption algorithm is CCA-secure.  However, I don't know what notion of security for key exchange algorithms this paper uses; I don't know if it proves SK-security, or something else.


Evidence that matrix multiplication is not in $O(n^2\log^kn)$ time

There's an algorithm for multiplying an $N \times N^{0.172}$ matrix with an $N^{0.172} \times N$ matrix in $N^2 \operatorname{polylog}\left(N\right)$ arithmetic operations. The main identity used for it comes from Coppersmith's paper "Rapid multiplication of rectangular matrices", but the explanation for why it leads to $N^2 \operatorname{polylog}\left(N\right)$ instead of $N^{2 + \epsilon}$ is in the appendix of Williams' paper, "New algorithms and lower bounds for circuits with linear threshold gates".

This only works because Coppersmith's identity has some additional structure you can take advantage of, and the more recent MM algorithms don't seem to have this structure. That said, I'm not sure why one can't hope to extend this approach to $N \times N \times N$ matrix multiplication.


Yes, it would still be zero knowledge. However, it wouldn't be a proof of anything, since whether the colors matched or not, you still know nothing about whether the graph is actually 3-colored or not. It's not a trick question -- just a bad one.


What is the simplest universal unidimensional interaction net system?

Turing machines and unidimensional cellural automata may both be regarded as "unidimensional" interaction net systems (see Lafont's Interaction Combinators paper).  So any simple UTM or Turing-complete cellula automaton induces a "simple" Turing-complete system.  I'm afraid no better answer is known.

Anyway, "simple" is relative: the interaction net system corresponding to even a very small UTM is big compared to the interaction combinators. Cellular automata probably give smaller systems (although still bigger than the interaction combinators) but the interest of these is nevertheless unclear as no special feature of interaction nets is used about them, they are just paraphrases of the original model.


The sum of all degrees $d(x)$ in a graph is at most $2e$. The sum of all $d(x)^{\alpha}$ is at most $(max degree)^{\alpha -1}$ times sum of all $d(x)$. Together these give the upper bound.


Generating $k$ random bits from a pdf with entropy $H(p) = k$

The relevance of Shannon entropy is to repeated sampling: Given $n$ independent samples from a source with binary Shannon Entropy $k$, you can extract $nk(1+o(1)$ i.i.d. uniform bits as $n$ tends to infinity with probability tending to 1. This follows e.g. from the Keane-Smorodinsky [1] finitary isomorphism theorem. See also [2]-[5] below.
[1] M. Keane and M. Smorodinsky (1979), Bernoulli schemes of the same
entropy are finitarily isomorphic. Annals of Math. 109, 397–406.
[2] P. Elias (1972), The efficient construction of an unbiased random sequence. Ann. Math. Statist. 43, 865–870.
[3] D. E. Knuth and A. C. Yao (1976), The complexity of nonuniform
random number generation. Algorithms and complexity (Proc. Sympos., Carnegie-Mellon Univ., Pittsburgh, Pa., 1976), 357–428. Academic Press, New York.
[4] Y. Peres (1992), Iterating von Neumann’s procedure for extracting random bits. Ann. Stat. 20, 590–597.
[5] Harvey, Nate, Alexander E. Holroyd, Yuval Peres, and Dan Romik. "Universal finitary codes with exponential tails." Proceedings of the London Mathematical Society 94, no. 2 (2007): 475-496.


Find shortest prefix to generate original string by overlapping

You are asking about "quasiperiodicity".   This is a well-studied topic and a google scholar search will turn up many papers about it.  For example, there is an $O(n (\log n)^2)$ algorithm
here and an $O(n \log n)$ algorithm here.


Where to learn more about what Theoretical Computer Science is?

First, "theoretical computer science" means different things to different people. I think for most users on this site, a historical caricature (which reflects some modern sociological tendencies) is that there is "Theory A" and "Theory B" (with no implied order relation between them): Theory A consists of the theory of algorithms, complexity theory, cryptography, and similar. Theory B consists of things like the theory of programming languages, theory of automata, etc. Depending on your tastes in mathematics, you may prefer one over the other (or like both equally). I am more familiar with "Theory A," so let me give some references there:

Start with Sipser's book. This will give you a good introduction to automata, Turing machines, computability, Kolmogorov complexity, P vs NP, and a few other complexity classes. It is very well-written (in my opinion, it is one of the best-written technical books ever)
For algorithms, I have a slighty preference for Kleinberg-Tardos, but there are many good introductory books out there. You might be especially interested in computational geometry, which has its own set of great books.
Given that you are a mathematics graduate student, a major branch of TCS that is missing from these books is algebraic complexity theory, which often is closely related to algebra (both commutative and non-commutative), representation theory, group theory, and algebraic geometry. There is a canonical text here, which is Burgisser-Clausen-Shokrollahi. It is somewhat encyclopedic, so may not be the best introduction, but I'm not sure there is a really introductory book in this area. You might also check out the surveys by Chen-Kayal-Wigderson and Shiplka-Yehudayoff.

After that, I'd suggest browsing through more advanced books on particular topics, depending on your mathematical taste:

Arora-Barak is more modern complexity theory (continues on where Sipser's book ends, so to speak), giving you a flavor of the techniques involved (mix of combinatorics and algebra, mostly)
Jukna's book on Boolean function complexity does similar, but more in-depth for Boolean circuit complexity in particular (very combinatorial in flavor)
Geometric complexity theory. See here or Landsberg's introduction for geometers.
O'Donnell's book Analysis of Boolean Functions has a more Fourier-analytic bent.
Cryptography. The more advanced mathematical aspects here are typically number theory and algebraic geometry. While these pure mathematical aspects represent only a small portion of cryptography, they are an important one that you might find interesting. Not being my area, I'm not sure of what a good starting book is here.
Coding theory. Here, the mathematical theory ranges from sphere-packing (see the book by Conway and Sloane) to algebraic geometry (e.g., the book by Stichtenoth). Again, not my area, so I'm not sure if these are the best starting points, but flipping through them you will quickly get the flavor and decide if you want to delve deeper.

And then there are many other mathematical topics that only appear in the research literature, like connections with foams, graph theory, C*-algebras (let me just point you to the Kadison-Singer conjecture), invariant theory, representation theory, quadratures, and on and on. See also these related questions

Resources for mathematicians hoping to learn more computer science
Are there any topics in theoretical CS that are more about pure math?
Applications of TCS to classical mathematics?
Solid applications of category theory in TCS?


Weighted Min-Cut in bounded-genus graphs

For graphs embedded on a surface of genus g with bounded weights $w:E \rightarrow \mathbb{Z}$, you can solve MAX-CUT in time $4^g poly(n)$ using an algorithm of Gallucio, Loebl and Vondrák. Applying it to your instance after taking the opposite weights and looking whether the result is positive seems to solve your problem.


Find the right/best track combination for a given distance, using a genetic algorithm or ?.

You could easily formulate this as a integer linear programming (ILP) problem. This is a linear programming problem where the solutions are constrained to be integers. The problem is NP-hard as indicated in other answers, but software does exist to address this sort of problem.

Let $L$ be the ultimate length you are aiming for, $a$ be the number of
Track A used, $b$ be the number of Track B used, and so forth. Finally,
let $A$, $B$, $C$, and $D$ be the amount of each kind of track you have.

($a,b,c,d$ are variables; the rest are constants.)

Then the integer linear programming problem is formulated as:

$L - 0.5 \le 3.0 a + 5.0 b + 6.5 c + 10.5 d \le L + 0.5$
$0 \le a \le A$
$0 \le b \le B$
$0 \le c \le C$
$0 \le d \le D$
$a,b,c,d$ are integers
minimise $a+b+c+d$

The condition $a+b+c+d$ can be changed to what you want to minimise/maximise to suit your needs so long as
it is linear in the variables $a,b,c,d$. The could be something capturing the costs of the various Tracks. All of the other ingredients can be changed in an obvious way, for different track lengths, different tolerance level, and so forth, so long as they are constants when you submit your question to an ILP system.

Plenty of software packages exist to solve such problems; many are listed on the page linked to above.


Is it possible to include an optimization algorithm's own running time in the cost?

Analyzing algorithms on real word machines is complicated but there has been some work done in this area in terms of how an algorithm behaves based on access to memory hierarchy. External Memory or memory hierarchy access based analysis are much more useful in understanding how an algorithm grows for large data-sets and in modern machines on most problems external memory access is the one which creates most latency AFAIK. You should check out work done on Cache Oblivious algorithms and algorithms for External Memory for understanding the run time cost of your problem.

I am not aware of work done on CPU cycles but someone who knows about this can pitch in.


Implications of $\mathsf{P}\neq\mathsf{NP}$ in $\mathsf{BSS}$ model

$\newcommand\Ptime{\mathsf P} \newcommand\NP{\mathsf{NP}} \newcommand\poly{\mathsf{poly}}$
It is known that $\Ptime/\poly \neq \NP/\poly \implies \Ptime_{\mathbb C}\neq \NP_\mathbb{C}$ [1] where the latter two represent the classes $\Ptime$ and $\NP$ in the BSS model over the complex numbers. (You can take the contrapositive to obtain a consequence of $\Ptime_\mathbb C = \NP_\mathbb C$.)
To the best of my knowledge, this is the only known result, though results of the same kind are known for other classes (in particular in Koiran's weak model).

For more on this, look at Chapter 1 (in particular Fig. 1.1) and Chapter 8 of Bürgisser's book [2].

[1] F. Cucker, M. Karpinski, P. Koiran, T. Lickteig, and K. Werther. On real
Turing machines that toss coins. In Proc. 27th ACM STOC, Las Vegas,
pages 335–342, 1995.
[2] Peter Bürgisser. Completeness and reductions in algebraic complexity theory, 1998.


No, no-regret dynamics do not converge to Nash equilibrium in general games, and its not hard to think of examples.

On the other hand, no regret dynamics do always converge to coarse correlated equilibrium in any game, and no-internal regret dynamics always converge to the set of correlated equilibria.

They are also known to converge to Nash equilibrium in several special cases of n-player games: for example, separable zero sum games, congestion games, and a few others.

In general, there are no efficient learning dynamics that converge to Nash equilibrium though. Not only is computing a Nash equilibrium PPAD hard, but even ignoring computation, for any "decoupled learning dynamics" (among which no regret dynamics are a special case) must exchange exponential communication before finding a Nash equilibrium in general games.


Upper bound on the pseudoentropy of any distribution

Take any distribution $D$ on $\{0,1\}^n$. Sample $k(n)$ points $x_1, \cdots, x_{k(n)}$ independently from $D$ and let $\tilde D$ be the uniform distribution that gives a random $x_i$. Then, if $k(n)$ is super-polynomially large e.g. $k=n^{\log n}$, you cannot distinguish $D$ and $\tilde D$ using only $\mathrm{poly}(n)$ samples. Hence $D$ is computationally indistinguishable from a distribution $\tilde D$ with entropy $\mathrm{poly}\log(n)$.


Although there aren't any problems known to be $\mathsf{BPP}$-complete (and Sipser gave an oracle relative to which $\mathsf{BPP}$ doesn't have complete problems), one topic to look at here is pseudorandom generators. The existence of a good enough pseudorandom generator implies $\mathsf{BPP} = \mathsf{P}$. This isn't $\mathsf{BPP}$-complete, but it does have the feature that a single algorithm could show $\mathsf{BPP}=\mathsf{P}$.

Also, although not $\mathsf{BPP}$-complete, Polynomial Identity Testing is a good single problem in $\mathsf{BPP}$ to focus on derandomizing. Many problems in $\mathsf{BPP}$ are actually in $\mathsf{RP}$ or $\mathsf{coRP}$, often due to the Schwarz-Zippel Lemma (in fact, there are apparently very few known candidates that are known to be in $\mathsf{BPP}$ but not in $\mathsf{RP} \cup \mathsf{coRP}$, see this related question), so derandomizing PIT would derandomize a whole bunch of problems. Furthermore, derandomizing PIT is known to imply strong lower bounds on $\mathsf{NEXP}$.


Does L have a definition in terms of circuits?

Well, $L = SC^1$, where $SC^1$ is the class of languages computed by polynomial size circuits of $O(\log n)$ width.

As for $NL$, it could be characterized as the class languages computed by polynomial size skew circuits (which in some sense is just another way of saying nondeterministic branching programs).


Characterisation of computability of partial functions from infinite words into finite words by functions with prefix-free domain

I guess I have an alternative solution. Let $f :\subseteq \Sigma^{\omega} \to \Sigma^{\omega}$ be computable. Define
$$
 h(u) = v \mbox{ iff }
  f(u\Sigma^{\omega}) = \{v\} \mbox{ with $u$ minimal}
$$
and let $h(u)$ diverge otherwise. Then $\mbox{dom}(h)$ is prefix-free for if $h(u) = v$ then $f(u\Sigma^{\omega}) = \{v\}$ as the machine behaves the same when reading the prefix $u$, producing $v$. Also $h$ is computable, for if $M$ is a machine for $f$ and $u \in \Sigma^{\ast}$, just simulate $M$ on $u0^{\omega}$ and if it produces some output and stops check if the prefix read by $M$ equals $u$; and if not just enter an infinite loop.

Furthermore we have $f = h_{\ast}$. For if $f(p) = u$ then there exists some minimal prefix $w \sqsubseteq p$ with $f(w\Sigma^{\omega}) = \{u\}$, hence $h_{\ast}(p) = h(w) = u$. For the other direction suppose $h_{\ast}(p) = u$, then $w \sqsubseteq p$ with $h(w) = u$, i.e. $f(w\Sigma^{\omega}) = \{u\}$, in particular $f(p) = u$.


How would I go about learning the underlying theory of the Coq proof assistant?

One place to start is  the Coq reference manual (pdf). Chapter 4 describes the underlying logic of Coq, and ultimately everything is based on this. It's called the calculus of (co)inductive constructions, and many  papers describe. Getting your hands on the Coq'Art book Interactive Theorem Proving and Program Development provides a more leisurely but not cheap introduction to Coq.

To learn about how tactics work, have a look at this earlier question: How do 'tactics' work in proof assistants?

To build up the required theory, you need to learn about Type Theory. Most closely related to the theory underlying a proof assistant is probably Per Martin-Löf's Intutionistic Type Theory notes (or book) or the book Programming in Martin-Löf Type Theory, which is really about writing and proving theorems in type theory. A programming language perspective on type theory can be obtained from Pierce's Types and Programming Languages. Girard et al's Proofs and Types, which also addresses the importance of the Curry-Howard Correspondence, is another excellent reference.
Then you are probably well and truly ready to read Coquand and Huet's The Calculus of Constructions. Finally chase up some of the references in the back of the Coq manual.

There are other proof assistants, HOL, NuPRL, Mizar, Twelf, etc., and they have their theory too, so you can learn a lot too by reading in that direction.

Finally, for an overview of the history and future of proof assistants, check out the recent article by Herman Geuvers.


What is the difference between propositions and judgments?

First, you should know that, in general, there is not consensus about these terms and their definitions depend on the system in which one is working.Since you asked about intuitionist type theory, I'll quote Pfenning:

  A judgment is something we may know, that is, an object of knowledge. A judgment is evident if we in fact know it.

Propositions on the other hand, according to Martin-Löf are sets of proofs. In this interpretation, if the set of proofs for a proposition is empty then it is false and otherwise true.

  A proposition is interpreted as a set whose elements represent the proofs of the proposition

says Nordström et al.  On the other hand, in classical logic and in general, propositions are objects expressed in a language which can be either "true" or "false".

To give you some extra intuition; from my point of view, judgments are metalogical and propositions logical.

I suggest "Constructive Logic" by Frank Pfenning, "Proofs and Types" by Jean-Yves Girard and "Programming in Martin-Löf's Type Theory" by Bengt Nordström et al. All three are freely available on the Internet. The last one is probably the closest to what you want as it is oriented to programming and goes into great detail, at length, about the meanings of these terms and many more.


$ACC^0$ implementation of a boolean function

Suppose $x \in \{0,\dots,2n\}$. Then we have $((2n)^2 - n) + x$ is square if and only if $x=n$. This is easily seen to imply that the square function is complete for $\mathrm{TC}^0$ under $\mathrm{AC}^0$ Turing reductions.


Computational consequences of Friedman's (unprovable) Upper Shift Fixed Point theorem?

I don't know of any consequences of this particular theorem, but normalization proofs of lambda calculi like the calculus of inductive constructions rely on large cardinal axioms -- even though the set of lambda-terms is as countable as you could want.

I think the best way to understand the computational significance of set-theoretic axioms asserting the existence of large cardinals is to think of set theory as a way of phrasing the theory of graphs. That is, a model of a set is a collection of elements equipped with a binary relation used to interpret membership. Then, the axioms of set theory tell you properties of the membership relation, including how you can form new sets from old. In particular, the axiom of foundation means that the membership relation is well-founded (ie, it has no infinite descending chains). This well-foundedness in turn means that if you can line up the execution states of a program with the transitive membership of the elements of a set, then you have a termination proof.

So an assertion that a "big" set exists has a computational payoff as a claim that a certain class of loops in a general recursive programming language terminate. This interpretation works uniformly, all the way from the plain old axiom of infinity (which justifies natural number iteration) all the way up to large cardinal axioms.

Are these axioms true? Well, if the axiom is false you can find a program in one of these classes which doesn't terminate. But if it's true, we will never be sure, thanks to the Halting theorem. Everything from natural number induction on is a matter of scientific induction, which may always be falsified by experiment -- Edward Nelson has famously hoped to prove exponentiation is a partial function!


I apologize beforehand for the blog-post format of my answer. I couldn't help myself making a small overview of the parallel computing world.

You can categorize parallel programming models in roughly two categories: control-flow and data-flow models.

The control-flow models try to make parallelism work within the context of a explicit-control program, basically every programmable computer today.  The fundamental problem being tackled is that such a 'Von Neumann architecture' was not designed for parallel execution, but efficient sequential computations.  Parallelism in such context is obtained by duplicating parts of the basic modules (memory, control, arithmetic).

Duplicating only arithmetic gives you SIMD instructions, all ALUs share the same Program Counter (PC) and thus always execute the same operation in parallel, albeit on different data.

Duplicating ALU and the PC but keeping the instruction sequencer inside the control unit gives you Out of Order (OoO) execution that yield some pipeline-parallelism. In this category you also have the Very Long Instruction Word (VLWI) and branche-prediction techniques. You rarely see this category at a software level though.

Going a bit further is duplicating the whole 'core' but keeping the memory shared, these are the current multicore processors that give you task (or thread) parallelism.  Sharing memory in this context gives you very, very hard and subtle concurrency issues.  Parallel computations on current multicore are thus completely revolving around synchronization/concurrency problems, the careful balance of performance (no sync) and desired semantics (totally synchronized, sequential execution semantics). Examples of this is the PRAM or more popular these days the Cilk ofshoots such as fork/join (IntelTBB, Java.Utils.Concurrency). CSP and Actor models are concurrency models, but as mentioned above concurrency and parallelism become blurred in a shared-memory environment. n.b. parallelism is for performance, concurrency to maintain correct semantics.

Duplicating memory too gives you either networked computers that get programmed with MPI and its ilk or just strange non-Von Neumann architectures such as the network-on-a-chip processors (cloud processor, the Transputer, Tilera). Memory models such as UMA or NUMA try to maintain the illusion of shared memory and can exist on either software or hardware level. MPI maintains the program-level parallelism and only communicates via message passing. Message passing is also used on a hardware level for communication and concurrency (Transputer).

The second category are data-flow models. These were designed at the dawn of the computer age as a way to write down and execute parallel computations, avoiding the Von Neumann design.  These have fallen out of vogue (for parallel computing) by the '80s after sequential performance rose exponentially. However, a lot of parallel programming systems such as Google MapReduce, Microsoft's Dryad or Intel's Concurrent Collections are in fact dataflow computational models.  At some point they represent computations as a graph and use that to guide execution.

By specifying parts of the models you get different categories and semantics for the dataflow model. What do you restrict the shape of the graph to: DAG (CnC, Dryad), tree (mapreduce), digraph?  Are there strict synchronization semantics (Lustre, reactive programming]? Do you disallow recursion to be able to have a static schedule (StreaMIT) or do you provide more expressive power by having a dynamic scheduler (Intel CnC)? Is there a limit on the number of incoming or outgoing edges? Do the firing semantics allow firing the node when a subset of the incoming data is available? Are edges streams of data (stream processing) or single data tokens (static/dynamic single assignment). For related work you could start by looking at the dataflow research work of people like Arvind, K. Kavi, j. Sharp, W. Ackerman, R. Jagannathan, etc.

Edit: For the sake of completeness. I should point out there are also parallel reduction-driven and pattern-driven models. For the reduction strategies you broadly have graph-reduction and string-reduction. Haskell basically uses graph-reduction, which is a very efficient strategy on a sequential shared-memory system. String-reduction duplicates work, but has a private-memory property that makes it better suited to being implicitly parallelized. The pattern-driven models are the parallel logic languages, such as concurrent prolog. The Actor model is also a pattern-driven model, but with private memory characteristics.

PS. I use the term 'model' broadly, covering abstract machines for both formal and programming purposes.


What are some standard books/papers on Information Theory?

This is a list of recommended books, videos and web sites copied from the Further Readings section of my book on information theory (given at the end of this post).

Applebaum D (2008). Probability and Information: An Integrated Approach. A thorough introduction to information theory, which strikes a good balance between intuitive and technical explanations.

Avery J (2012). Information Theory and Evolution. An engaging account of how information theory is relevant to a wide range of natural and man-made systems, including evolution, physics, culture and genetics. Includes interesting background stories on the development of ideas within these different disciplines.

Baeyer HV (2005). Information: The New Language of Science Erudite, wide-ranging, and insightful account of information theory. Contains no equations, which makes it very readable.

Cover T and Thomas J (1991). Elements of Information Theory. Comprehensive, and highly technical, with historical notes and an equation summary at the end of each chapter.

Ghahramani Z (2002). Information Theory. Encyclopedia of Cognitive Science. An excellent, brief overview of information.

Gleick J (2012). The Information. An informal introduction to the history of ideas and people associated with information theory.

Guizzo EM (2003). The Essential Message: Claude Shannon and the Making of Information Theory. Master’s Thesis, Massachusetts Institute of Technology. One of the few accounts of Shannon’s role in the development of information theory.
See http://dspace.mit.edu/ bitstream/handle/1721.1/39429/54526133.pdf.

Laughlin, SB (2006). The Hungry Eye: Energy, Information and Retinal Function, Excellent lecture on the energy cost of Shannon information in eyes. See http://www.crsltd.com/guest-talks/ crs-guest-lecturers/simon-laughlin.

MacKay DJC (2003). Information Theory, Inference, and Learning Algorithms. The modern classic on information theory. A very readable text that roams far and wide over many topics. The book’s web site (below) also has a link to an excellent series of video lectures by MacKay. Available free online at http://www.inference.phy. cam.ac.uk/mackay/itila/.

Pierce JR (1980). An Introduction to Information Theory: Symbols, Signals and Noise. Second Edition. Pierce writes with an informal, tutorial style of writing, but does not flinch from presenting the fundamental theorems of information theory. This book provides a good balance between words and equations.

Reza FM (1961). An Introduction to Information Theory. A more comprehensive and mathematically rigorous book than Pierce’s book, it should be read only after first reading Pierce’s more informal text.

Seife C (2007). Decoding the Universe: How the New Science of Information Is Explaining Everything in the Cosmos, From Our Brains to Black Holes. A lucid and engaging account of the relationship between information, thermodynamic entropy and quantum computing. Highly recommended.

Shannon CE and Weaver W (1949). The Mathematical Theory of Communication. University of Illinois Press. A surprisingly accessible book, written in an era when information theory was known only to a privileged few. This book can be downloaded from http://cm. bell-labs.com/cm/ms/what/shannonday/paper.html

For the complete novice, the videos at the online Kahn Academy provide an excellent introduction.

Additionally, the online Scholarpedia web page by Latham and Rudi provides a lucid technical account of mutual information: http://www.scholarpedia.org/article/Mutual_information.

Finally, some historical perspective is provided in a long interview with Shannon conducted in 1982: http://www.ieeeghn.org/wiki/ index.php/Oral-History:Claude_E._Shannon.

Finally, my book is called Information Theory: A Tutorial Introduction (2015). Chapter 1 can be downloaded from here:
http://jim-stone.staff.shef.ac.uk/BookInfoTheory/InfoTheoryBookMain.html


FPRAS on #P complete problems and self reducibility

This theorem from that paper of Sinclair and Jerrum is slightly stronger than the sentence quoted in the question, and gives the fpras mentioned by Dyer:

  THEOREM 4.6. Let $R\subseteq \Sigma^*\times\Sigma^*$ be self-reducible. If there exists a polynomially time-bounded randomised approximate counter for $R$ within
  ratio $1 + O(n^\alpha)$ for some $\alpha\in\mathbb R$, then there exists a fully polynomial randomised approximation scheme for $\#R$.

Note the quantification over $R$. Your first question asks if "counting self-reducible structures might have an FPRAS", but this theorem is looking at particular $R$'s and showing that if $R$ has a weak kind of approximation algorithm, then $R$ also has a stronger kind of approximation algorithm.

Jerrum and Sinclair explain it like this:

  The chief significance of Theorem 4.6 is that it establishes a notion of
  approximate counting which is robust with respect to polynomial time
  computation, at least for the large class of self-reducible relations [...] We suggest that this notion will be useful in the future classification
  of hard counting problems [...]


What's the simplest noncontroversial 2-state universal Turing machine?

This is not a real answer to your question (I don't know much about the (2,3) machine debate); but I suggest you the paper "Small Turing machines and generalized busy beaver competition". I quickly read it some time ago, and it has a nice graph with the borderlines between the 4 types of small TMs:

decidable
open Collatz-like problem
$3x + 1$ simulation
universal

(perhaps some results have been improved).

The notion of TM used in the paper is the standard definition of TM used in papers on small universal Turing machines :

... They have a unique one-dimensional tape infinite in both directions, and a unique twoway
read–write head. There is a blank symbol denoted by 0. Initially, a
finite word, the input, is written on the tape, other cells contain the blank
symbol, the head reads the leftmost symbol of the input, and the state is the
initial state. At each step, according to the current state of the machine and
the symbol read by the head, the symbol is modified, the head moves left or
right (and cannot stay reading the same cell), and the state is modified. The
computation stops when a special halting state is reached. ...


Complexity of counting weighted cycles in planar graphs?

If you allow repetition of vertices, but not edges, within a cycle, then the problem is $\text{#P}$-complete.  This paper shows that the problem of counting Eulerian tours is $\text{#P}$-complete for 4-regular planar graphs.  Therefore the problem I just described (call it $\text{#}A^\prime$) is $\text{#P}$-hard, because it is at least that difficult: in the special case where all edges have weight 1 and all nodes have weight 0, the Eulerian tours are just those cycles with total weight equal to the number of edges in the graph.  On the other hand, $\text{#}A^\prime\in\text{#P}$, because the corresponding decision problem $A^\prime \in \text{NP}$.


First note that #2 and #3 are saying the same thing. Next, notice that if u is an ancestor of v in T, then in a pre-order traversal, we see u before v, and therefore pre(u) < pre(v). On the other hand, since T is a depth-first search tree (as opposed to an arbitrary tree) of the connected undirected graph G, and $(u,v) \in G-T$, we can deduce that pre(u)<pre(v) results in u being an ancestor of v.

The following image, taken from Wikipedia, can help:

Preorder traversal sequence: F, B, A, D, C, E, G, I, H (root, left, right)

Postorder traversal sequence: A, C, E, D, B, H, I, G, F (left, right, root)


an axiomatic framework for clustering by jon kleinberg may have a problem?

I do not want to attempt a general definition of "unnatural", but I find your argument about the inherent incompatibility of the scale-invariance axiom and the richness axiom as defined in Section 2 of Kleinberg's NIPS paper.

The impossibility result in Section 3 of his paper is stronger, however, and can directly address your concern.

  Theorem 3.1 If a clustering function f satisfies Scale-Invariance and Consistency,
  then Range(f) is an antichain.

So you can consider weakening the richness axiom, e.g. by asking for all partitions with at least 2 parts, and as long as your set of partitions is rich enough to not be an anti-chain, the impossibility theorem goes through.

Hopcroft and Kannan have come up with a "natural" alternative to the richness axiom for which clustering is possible.  It is buried in their book Computer Science Theory for the Information Age, and described in a lovely teaser on the Gödel’s Lost Letter blog.


All literals implied by a set of horn clauses

It's called finding a minimal model of a Horn formula.

This model is unique because the intersection of two models of a Horn formula is itself a model. In fact, [Horn, On sentences which are true of direct unions of algebras, 1951] proved the following: A boolean function can be expressed as a conjunction of Horn clauses if and only if its set of models is closed under intersection.


Difference between self-information and entropy

The entropy refers to a set of symbols (a text in your case, or the set of words in a language). The self-information refers to a symbol in a set (a word in your case).

The information content of a text depends on how common the words in the text are wrt the global usage of those words.

E.g. "Next saturday morning" should have less self-information (as a named entity) than "Large Hadron Collider", each of the words should have less self information (except for large, maybe). However the entropy may be higher in the first case, there are not many Large Hadron "things".

Maybe Markov chains or some model that is better suited for probability in natural language would give you better (more significant and useful) results.


Is joint Kolmogorov Complexity order invariant?

You don't need symmetry of information. The invariance theorem does the trick. Let $p$ the smallest program such that $U(p) = \langle x, y\rangle$. One way of producing $(y, x)$ is to take make a program $q$ that runs whatever program it is given as input, interprets the output as a pair, and flips the two parts. This gives you a program $\overline{q}p$ to produce $\langle y, x\rangle$. Since $\overline{q}$ is only a constant number of bits long, the two $K$'s are equal up to a constant.

Now for higher numbers of arguments, the same idea works in principle. However, the constant does depend on the number of arguments: if I want to write a $q$ program to compute some $n$-tuple of numbers and re-arrange it into an arbitrary order, I need to encode the order in $\log(n!)$ bits (if the ordering is random). So if the number of arguments is not fixed to a constant, you need to take that into account.

Isn't there some other way, besides the $q$ program? No, if there were we could encode free information in the ordering of the tuple.

Assume for a contradiction that $K(x_1, \ldots, x_n)$ is invariant up to a constant to permutation of the arguments, with the constant independent of $n$. Let $X = \langle x_1, \ldots, x_n\rangle$ be the enumeration of the first $n$ binary strings, so that $K(X) \leq_+ K(n)$. Let $z$ be a random string with $|z| = \log(n!)$ Let $\langle x_1, \ldots, x_n \rangle$ be a random string. Index all permutations of $n$ elements by binary strings and pick the one corresponding to $z$. Call this permutation of our tuple $X_z$. Let $p$ and $p_z$ be the shortest programs for $X$ and $X_z$ respectively. Build a program $q$ that reads input $\overline{p}p_z$ and returns $z$. Putting all this together gives us
$$\log(n!) \leq_+ K(z) \leq_+ |\overline{q}\overline{p}p_z| \leq_+ 2K(X) \leq_+ 2K(n) \leq_+ 4\log(n).$$


Are there efficient general Bonferroni-style bounds known?

I think you'll find the answer in the paper "Approximate Inclusion-Exclusion" by Linial and Nisan:
http://www.cs.huji.ac.il/~nati/PAPERS/approx_incl_excl.pdf


There is a combinatorial algorithm by Mahajan and Vinay that works over commutative rings: http://cjtcs.cs.uchicago.edu/articles/1997/5/contents.html


Non-termination, strict positivity and free monads

Using Free, you can have a HOAS embedding of the untyped lambda calculus. And then write a structurally recursive function firing the top-level redex again and again. Good luck trying to normalise reduce omega.

{-# NO_POSITIVITY_CHECK #-}
data Free (f : Set → Set) (a : Set) : Set where
  Pure : a → Free f a
  Roll : f (Free f a) → Free f a

data LAMF (T : Set) : Set where
  App : T → T → LAMF T
  Lam : (T → T) → LAMF T

LAM : Set → Set
LAM = Free LAMF

pattern `lam b   = Roll (Lam b)
pattern `app f t = Roll (App f t)

data ⊥ : Set where

-- Type of closed term: LAM ⊥

delta : LAM ⊥
delta = `lam λ x → `app x x

omega : LAM ⊥
omega = `app delta delta

reduce : ∀ {A} → LAM A → LAM A
reduce (`app (`lam b) t) = reduce (b t)
reduce t = t


There is a list of open problems in computational geometry. It is edited and maintained by Demaine, Mitchell, and O'Rourke.


It is known that $\mathsf{UP= NP}$ implies $\mathsf{SpanP = \#P}$ since Kobler, Schoning, and Toran proved that $\mathsf{UP= NP}$ if and only if $\mathsf{SpanP = \#P}$. It is easy to see that $\mathsf {\#P}$ is contained in $\mathsf {SpanP}$.

A function $f : Σ^* →\mathbb N$ is in $\mathsf{SpanP}$ if there is an $\mathsf {NP}$ Turing machine transducer $M$ such that for all $x$, $f(x)$ is the number of distinct outputs of $M$ on input $x$.

J. Kobler, U. Schoning, and J. Toran. On counting and approximation, Acta Informatica,
26:363-379, 1989.


Note: I have had a similar question about the correctness proof of Paxos and Fast Paxos before and posted it here. Wish the excellent answer to it be helpful to you.

A few words about this paper:

Leslie Lamport has his own, very impressive writing style. He is not satisfied with the common pattern of stating a theorem, proving it, moving on to another theorem, and so on. He is good at demonstrating the way how to solve a problem. In his paper, you will see that proof does not follow a theorem; instead, it comes along with a theorem. The paper "Paxos Made Simple" is a typical example of this style.

About your questions:

  Your question (1): How can he add the additional assumption? Is it reasonable?

Leslie Lamport is using strong induction. The goal here is to prove

  $P2^{b}:$ If a proposal with value $v$ i chosen (say, with number $m$), then every higher-numbered proposal issued by any proposer has value $v$.

We apply strong induction to natural number $\mathbb{N}$. I summarize the proof as follows and explain it later.

The base case is "some proposal with number $m$ and value $v$ is chosen".
The strong induction hypothesis is "every proposal issued with a number in $m .. (n-1)$ has value $v$".
The induction step to prove $P2^{b}$: Combining the premise of "$m$ is chosen (with value $v$)" with the above induction hypothesis, we get (for reference, I call it $C$-condition):

  $C$-condition: Every acceptor in $C$ (defined in the paper) has accepted a proposal with number in $m .. (n-1)$, and every proposal with number in $m .. (n-1)$ accepted by any acceptor has value $v$.

Now, Lamport introduces $P2^{c}$, which, along with the above $C$-condition, is sufficient for $P2^{b}$.

You can think of this induction process step by step:

The base case $m$ is trivially valid.
Given that step 1 is valid, the argument in "The induction step" above (of course with $P2^{C}$) shows that the proposals numbered $m+1$ has value $v$.
Given both step 1 and step 2 are valid, the same argument shows that the proposals numbered $m + 2$ has value $v$.
And so on.

This also answers your second question.

  Your question (2): In reality, proposal numbered in $m..(n - 1)$ can have value other than v, isn't it?

No, it isn't. The Paxos algorithm guarantees that all the proposals with larger numbers than $m$ must have value $v$, given that $m$ is chosen with value $v$.


Maximum disjoint set: what is the actual approximation factor of the greedy algorithm?

What is the actual maximum minimum DIN in collections of unit-disks?

It is 3.


Order of quantifiers in the definition of NP-completeness: does the reduction allow arbitrary polynomials?

The latter. The former is impossible for NP-complete languages by the nondeterministic time hierarchy theorem: assume for contradiction that $B$ is a language computable in nondeterministic time $p(n)$ such that every NP language reduces to it in time $q(n)$. Then
$$\mathrm{NP}\subseteq\mathrm{NTIME}(q(n)+p(q(n)))
\subsetneq\mathrm{NTIME}((q(n)+p(q(n)))n)\subseteq\mathrm{NP},$$
a contradiction.

You asked more generally about NP-hard languages. Consider the language $B\in\mathrm{NEXP}$ defined as
$$B=\{M\#w:\text{$M$ is a clocked poly-time NTM and $M$ accepts $w$}\}.$$
It is clear that any NP-language $A$ reduces to $B$ in time $n+c_A$ for some constant $c_A$, namely $c_A=1+|M_A|$ where $M_A$ is a fixed NTM accepting $A$.

But in fact, every $A\in\mathrm{NP}$ reduces to $B$ in time $3n+c$ for some constant $c$ independent of $A$. The reduction function reads up to the first $c_A$ letters of the input, storing them in its state. If the input has length $\le c_A$, the reduction directly finds the result in a lookup table, and outputs one of two fixed inputs that make $B$ accept or reject as appropriate. Otherwise, it outputs the description of $M_A$, copies the first $c_A$ input letters from the internal state to the output, and proceeds to copy the rest of the input. The running time is thus bounded by
$$\begin{cases}n+c,&n\le c_A,\\c_A+2c_A+(n-c_A)\le3n,&n>c_A\end{cases}$$
for some absolute constant $c$ independent of $A$.


Han's $O(n \log\log n)$ time, linear space, integer sorting algorithm

I was just wondering the same thing.

Fortunately, I was able to find a journal-article published in 2011 which explains this very thing; whats more, you don't need a subscription to view it: Implementation and Performance Analysis of Exponential Tree Sorting

I recommend reading the entire article to learn how it can be implemented and to better understand its underlying theory. It also shows how Exponential Trees stack up against Quick-Sort and Binary Trees. Here's the relevant excerpt related to Han's $\bf O(n \log\log n)$ time, linear space, integer sorting algorithm:

  Yijie Han has given an idea which reduces the complexity to expected
  time in linear space.[6] The technique used by him is coordinated pass
  down of integers on the Andersson’s exponential search tree[8] and the
  linear time multi-dividing of the bits of integers. Instead of
  inserting integer one at a time into the exponential search tree, he
  passed down all integers one level of the exponential search tree at a
  time. Such coordinated passing down provides the chance of performing
  multi-dividing in linear time and therefore speeding up the algorithm.
  This idea may provide speed up, but in practical implementation it is
  very difficult to handle integers in batches.

[6]  Y.  Han,  Deterministic  sorting  in  O(n  log  log n)  time  and linear space, 34th STOC, 2002.

[8]  A.  Andersson,  Fast deterministic  sorting  and  searching  in linear  space,  IEEE  Symposium  on  Foundations  of Computer Science, 1996.


There is a recent paper from  Scott Aaronson which provides a new proof that the permanent is #P-hard. This proof is based on the model of linear-optical quantum computing and is more intuitive than that of Leslie Valiant.


Fun with Algorithms!  Although it is a conference not a journal that you might looking for, among other things several NP-hardness results about (combinatorial) games are published here, including this one.

However this is a triennial conference (except for 2014, where the last conference was in 2012), so if you want to publish it soon then there might be a better choice.


How much time to recognize palindromes in logarithmic space?

You can use the same argument used to prove the $\Omega(n^2)$ time bound on single tape.

Suppose that you have a TM with $S(n)$ space that recognize palindromes
$\{x\,0^{\frac{n}{3}} x^R \mid |x|=n/3 \}$ (where $x^R$ is the reverse of $x$) in time $T(n)$.
When the (input) head crosses the middle $0^{n/3}$ it can carry only $S(n)$ bits of information. So it needs to make $\Omega(n / S(n))$ crosses, and each cross requires $n/3$ time.

So $T(n)S(n)=\Omega(n^2)$.


No Fair Merge via Nondeterminstic Data Flow Streams

When in doubt, consult the original source: Clinger's Thesis. Clinger shows that fair merge cannot be written in a nondeterministic dataflow program. He does this by considering the semantic domains in which such a function would be defined, ultimately deriving a contradiction to the assumption that fair merge exists.

Firstly, as Daniel Apon points out, $merge(\bot,1^\omega)=\{1^\omega\}$. This is the only reasonable definition of merge for these arguments (see page 84 of Clinger's thesis).

Secondly, $merge(\bot,1^\omega)\subseteq merge(0,1^\omega)$, because  $\bot\le 0$, as stream $0$ is a possible extension of stream $\bot$ (bottom of page 73),  and by assumption $merge$ is monotone. In more detail, the ordering on the domain of strings states that any prefix of a string, is $\le$ the string, thus the empty string $\bot$ is the smallest element, and hence $\bot\le 0$, where $0$ is the string with just the element $0$. The function $merge$ has type $S\times S\to\mathcal{P}(S)$, where $S$ is string and $\mathcal{P}(-)$ is powerset.  The assumption that $merge$ is monotone means that if $a\le b$ then $merge(a,s)\subseteq merge(b,s)$. (Similarly for the second argument.)

Now $1^\omega\in merge(0,1^\omega)$ violates the assumption that $merge$ is fair – a fair merge of $0$ and $1^\omega$ should to contain the $0$. In more detail, $merge(S,T)$ is interleaving the "cards" from $S$ and $T$, without shuffling them. The significance of the stream $1^\omega$ is that it is infinite. $0$ is simply some character different from $1$. A fair merge of $0$ and $1^\omega$ should result in a string such as $1^*01^\omega$. Fairness means that within some finite time it selects elements from each string, thus the character $0$ is eventually chosen.

Hence $merge$ cannot be written as a nondeterministic dataflow program.


A language can be thought of as having both a static semantics, which determines the compile-time analysis that occurs; and a dynamic semantics, which determines the execution-time behavior of programs.

In Standard ML, for example, the static semantics concerns a language of Modules and a language of Types. The semantics show how types are assigned to terms in the core language and then checked for consistency. The module static semantics describe how signatures and structures are matched, how functors transform one structure to another, etc.

This is a fairly rich and complex language that is evaluated solely at compile-time; once this occurs, almost all of the semantic objects involved are no longer relevant to the execution semantics of the program and can be forgotten. The semantics works over the same syntax as the dynamic semantics, but the static semantics is very different in character from the dynamic semantics!

In a language such as Idris, which is dependently typed, the character of evaluation of the static semantics and the dynamic semantics ends up having far greater overlap. Instead of the static semantics working over types and the dynamic semantics working over values, both semantics now encompass both types and values. This doesn't mean that there aren't differences in the character of the static and dynamic semantics, just that there is significant overlap and they both concern some of the same semantic objects. In particular, the static semantics is often restricted to total functions, which ensures that evaluation will terminate (albeit sometimes after a lengthy delay).

Some parts of programs in dependently-typed languages exist only to provide evidence in the static semantics that other parts of the program are indeed well-typed. Idris doesn't make any syntactic distinctions here, but ATS (a systems programming language with dynamic semantics similar to C, but with a dependent type system) syntactically distinguishes terms that exist only to provide proof of assertions made in types. Idris does, on the other hand, allow annotation of programmer intent that some terms be "erased", which will produce an error in the static semantics if that desire can't be met.

Now, with that out of the way, let's look at C++ templates:

Instead of dealing with polymorphism and dependency of types on values directly in the static semantics, C++ adds an extra untyped language of template expansion into the static semantics. Rather than deal with complex static semantics, extra code is generated that should be checkable simply via the simple core language static semantics.

Although this lets you deal with some of the same practical problems that can be solved with polymorphic and more general dependent types (polymorphism is just a different sort of dependency, one of terms depending on types) it's not actually part of the type system; it's just an extra layer in the static semantics separate from the type system. Furthermore, the only way any extra "stuff" generated by template expansion could be erased would be by the general "dead code elimination" portion of the compiler, which isn't even a well-defined part of the static C++ semantics.

Sometimes in a dependently-typed language, type parameters can't be erased at run-time, because they are relevant to the determination of the run-time semantics. In C++, you would have to carry an extra parameter as well; this might be a "length" parameter that would be part of a Vector type in a dependently-typed language. C++ lacks the ability to make such parameters implicit and to define code that automatically calculates on them and make appropriate consistency checks with them.

Dependently-typed languages give you the choice of how much effort you will put into static proof of the runtime-irrelevance of such parameters; with little effort you can let them carry over into the dynamic semantics and be run-time checked, but with more effort you may be able to supply a proof that the property asserted by the type term is never violated and thus erase the run-time representation entirely.


Upperbound on the degree of a boolean function in terms of its sensitivity

This paper came up on the arXiv today and it improves on the upper bound on $bs(f)$ in terms of $s(f)$. They prove the following bound:

$$
bs(f) \leq 2^{s(f)-1}s(f).
$$

This along with the connection that Marcos mentioned in his comment should give better bounds than previously known.


in SAT resolution proofs, are all DAGs possible?

Let's assume that you do not allow Tautologies in the leafs, and consider a structure where exactly 3 leafs have edges to a node $A$. Denote the leaf clauses by $(a\vee L_1),(\neg a\vee b\vee L_2),(\neg b\vee L_3)$, where $L_1,L_2,L_3$ are discunctions of literals.
Since they all have edges to $A$, we have the following:
Leaves 1,2 resolve to $(b\vee L_1\vee L_2)$.
Leaves 2,3 resolve to $(\neg a\vee L_2\vee L_3)$

Since $A$ is a single node, then these expressions are equal.
Since there is no initial tautology, then $b\notin L_3$, but this implies that $b\in L_2$, which isn't the case (assume we have no duplicates).

So the only possibility is $b=\neg a$, but this means that $L_1=L_2\vee L_3$ and $L_3=L_2\vee L_3$, so the leaves aren't distinct.

If I am not mistaken, then this means that this structure is not possible, so not every DAG is possible (under the assumptions).


Are there variants of visibly pushdown automata that allow pushing of words onto the stack?

With epsilon pushes

For the version with pushes on epsilon-transitions, the undecidability proof of universality of pushdown-automata can be adapted to this new setting, so we lose at least the following properties: closure under complementation, determinizability, decidability of universality and inclusion.

Proof scheme:
Take a Turing Machine $M$, we want to build a VPA $A$ with epsilon-pushes such that it is universal if and only if M has no accepting run.

We design $A$ such that a word is not accepted if and only it is of the form:

$$\#C_0\&C_0\$(\overline{C_0})^R\#C_1\&C_1\$(\overline{C_1})^R\#C_2\&C_2\$(\overline{C_2})^R\dots\#C_n\&C_n\$(\overline{C_n})^R$$
where

Each $C_i$ encodes a valid configuration of $M$
$C_0$ is initial, $C_n$ is accepting
$u^R$ is the reverse of a word $u$
$\overline{u}$ is a copy of $u$ using pop letters
$\#,\&,\$$ are special separation symbols not in the alphabet of $M$
$C_i\to C_{i+1}$ is always a valid transition of $M$

The VPA $A$ is forced to do pop on factors of the form $C_i^R$. $A$ can non deterministically guess a violation of either property, and verify it. The key is that it can either push on $C_i$, or do nothing, which allows to verify all conditions (actually guess their violations). In particular, it can guess that the first (or second) occurence of $C_i$ does not match $(\overline{C_i})^R$, by ignoring the other component. It can also guess that $C_i\to C_{i+1}$ is not a valid transition, by pushing both occurences of $C_i$, then popping one, push no $C_{i+1}$, and compare $(\overline{C_{i+1}})^R$ to the stack content. For other $C_j$ that are not part of the guessing, one component is pushed and the $(\overline{C_j})^R$ is popped.

Pushing words

As for the variants where words are pushed, it seems that the determinizability proof in the original paper on VPAs can be adapted to this setting. It suffices to adapt the construction so that stack symbols are of the form $(S,R,u)$ where $u\in A^*$ is a prefix of a word that can be pushed according to the transition function. When popping a letter $a$, $(S,R,va)$ is turned to $(S',R',v)$, where $S'$ and $R'$ are updated normally to reflect the current powerset construction status.
However, this time we a priori get a deterministic pushdown automaton that is not visibly pushdown. At least this means that equivalence and universality are decidable.


Are $PSPACE$-complete problems inherently less tractable than $NP$-complete problems?

This is a very nice question that I have thought about a lot: Does the fact that a problem is $NP$-complete or $PSPACE$-complete actually affect the worst-case time complexity of the problem? More fuzzily, does such a distinction really affect the "typical case" complexity of the problem in practice?

Intuition says that the $PSPACE$-complete problem is harder than the $NP$-complete one, regardless of what complexity measure you use. But the situation is subtle. It could be, for example, that $QBF$ (Quantified Boolean Formulas, the canonical $PSPACE$-complete problem) is in subexponential time if and only if $SAT$ (Satisfiability, the canonical $NP$-complete problem) is in subexponential time. (One direction is obvious; the other direction would be a major result!) If this is true, then maybe from the "I just want to solve this problem" point of view, it's not a big deal whether the problem is $PSPACE$-complete or $NP$-complete: either way, a subexponential algorithm for one implies a subexponential algorithm for the other.

Let me be a devil's advocate, and give you an example where one problem happens to be "harder" than the other, but yet turns out to be "more tractable" than the other as well.

Let $F(x_1,\ldots,x_{n})$ be a Boolean formula on $n$ variables, where $n$ is even. Suppose you have a choice between two formulas you want to decide:

$\Phi_1 = (\exists x_1)(\exists x_2)\cdots (\exists x_{n-1})(\exists x_{n})F(x_1,\ldots,x_{n})$.

$\Phi_2 = (\exists x_1)(\forall x_2)\cdots (\exists x_{n-1}(\forall x_{n})F(x_1,\ldots,x_{n})$

(That is, in $\Phi_2$, the quantifiers alternate.)

Which one do you think is easier to solve? Formulas of type $\Phi_1$, or formulas of type $\Phi_2$?

One would think that the obvious choice is $\Phi_1$, as it is only $NP$-complete to decide it, whereas $\Phi_2$ is a $PSPACE$-complete problem. But in fact, according to our best known algorithms, $\Phi_2$ is an easier problem. We have no idea how to solve $\Phi_1$ for general $F$ in less than $2^n$ steps. (If we could do this, we'd have new formula size lower bounds!) But $\Phi_2$ can be easily solved for any $F$ in randomized $O(2^{.793 n})$ time, using randomized game tree search! For a reference, see Chapter 2, Section 2.1, in Motwani and Raghavan.

The intuition is that adding universal quantifiers actually constrains the problem, making it easier to solve, rather than harder. The game tree search algorithm relies heavily on having alternating quantifiers, and cannot handle arbitrary quantifications. Still, the point remains that problems can sometimes get "simpler" under one complexity measure, even though they may look "harder" under another measure.


Is this tree minimization problem NP-complete?

Your problem is ill-defined. Since the functions $f\colon \mathcal{T} \rightarrow \mathbb{Q}$ and $\mu\colon 2^N \rightarrow \mathbb{Q}$ (rather than real-valued) have a very long description, you can go over all possible trees $T \in \mathcal{T}$ in polynomial time.

To make the question more meaningful you might want the algorithm to have oracle access to $f$ and $\mu$, and then instead of NP-completeness you might want to prove a lower bound on the number of evaluations of $f$ and $\mu$.

Another possibility is that $f$ and $\mu$ have some structure and so can be specified succinctly. If this is the case, then you need to refine the problem reflecting that feature.

A similar problem occurs in submodular optimization. Suppose we want to maximize a monotone submodular function over a matroid constraint. There are several randomized polynomial time algorithms giving a $1-1/e$ approximation. There is a lower bound by Vondrák showing that in the (so-called) value oracle model, any better approximation requires evaluating the function at exponentially many places (this lower bound is information-theoretic rather than complexity-theoretic). Feige proved that a special case of the problem, maximum coverage, is NP-hard to approximate better than this ratio. Finally, Vondrák and Dobzinski show how to lift the value oracle result to a complexity result in the succinct representation model, assuming RP$\neq$NP (rather than P$\neq$NP as in Feige's result); the technique (whose main ingredient is list-decoding) also gives results that Feige's can't.


MA $\subseteq$ PSPACE $\subseteq$ EXP $\subseteq$ NEXP  and  P/poly has undecidable unary languages, so

NEXP $\subseteq$ P/poly  $\implies$  NEXP $\subset$ P/poly  $\implies$  NEXP $\subseteq$ EXP .

As something like a generalization of that  (showing that EXP-complete languages are

in CHECK is difficult) ,  for all languages L in CHECK with a checker whose queries all have

length at most  nd ,  for all non-decreasing functions  S : {0,1,2,3,4,...} $\to$ {0,1,2,3,4,...} :

If L's circuit-size in bits is at most S then

L  $\in$  DSPACE$\left(\hspace{-0.04 in}\left(\hspace{-0.02 in}n^d\hspace{-0.05 in}\cdot \hspace{-0.03 in}S\hspace{-0.05 in}\left(\hspace{-0.03 in}n^d\hspace{-0.02 in}\right)\hspace{-0.04 in}\right)\hspace{-0.04 in}+\hspace{-0.03 in}poly\hspace{.02 in}(n)\hspace{-0.03 in}\right)$  $\subseteq$  DTIME$\hspace{-0.02 in}\left(\hspace{-0.05 in}2^{\left(n^{\hspace{.02 in}d} \hspace{-0.02 in}\cdot S\left(\hspace{-0.02 in}n^{\hspace{.02 in}d}\hspace{-0.03 in}\right)\hspace{-0.03 in}\right)+\hspace{.02 in}poly\hspace{.02 in}(n)}\hspace{-0.04 in}\right)$   ,

so by contrapositive, if    L  $\not\in$  DTIME$\hspace{-0.02 in}\left(\hspace{-0.05 in}2^{\left(n^{\hspace{.02 in}d} \hspace{-0.02 in}\cdot S\left(\hspace{-0.02 in}n^{\hspace{.02 in}d}\hspace{-0.03 in}\right)\hspace{-0.03 in}\right)+\hspace{.02 in}poly\hspace{.02 in}(n)}\hspace{-0.04 in}\right)$

then L's circuit-size in bits exceeds S infinitely-often.

("in bits" as as opposed to "in gates".)

Similarly, for all functions T and $\ell$ and $S$ from {0,1,2,3,...} to {1,2,3,4,5,...},

for all search problems R in  FNTIME(T)  whose output-lengths are bounded above by $\ell$:

If R's circuit-size in bits is at most S then R is solvable by  FDTIME$\left(\hspace{-0.02 in}2^{S(n)} \hspace{-0.04 in}\cdot \hspace{-0.04 in}poly\hspace{.02 in}(S(n))\hspace{-0.04 in}\cdot \hspace{-0.04 in}T(n)\hspace{-0.03 in}\right)$ ,

so by contrapositive, if R is not solvable by  FDTIME$\left(\hspace{-0.02 in}2^{S(n)} \hspace{-0.03 in}\cdot \hspace{-0.03 in}\left(\left(\hspace{.05 in}poly\hspace{.02 in}(S(n)) \cdot \ell(n)\right)+ T(n)\right)\hspace{-0.03 in}\right)$

then R's circuit-size in bits exceeds S infinitely-often.


what advantage does heapsort has over smoothsort?

Having just done some reading up on the two algorithms, it would appear that heapsort has no implicit O advantage over smoothsort. This kind of makes sense when you think that smoothsort is just a special kind of heapsort, using a special kind of heap.

Where heapsort does have is an advantage is that it is easier to understand, and much better documented. There are very few publicly available implementations of smoothsort, and very little literature on them, however there is a lot of literature on heapsort.

Indeed, the only real accessible literature is this write-up by Keith Schwarz. It is also the basis of the wikipedia article.