How can I optimize my brute-force solution to this problem?

Integer linear programming
Your problem can be formulated in the following way: we are given vectors $v_{i,j} \in (\mathbb{Z}/N\mathbb{Z})^d$, where the board has $d$ cells, and the goal is, given a vector $c \in (\mathbb{Z}/N\mathbb{Z})^d$, find a function $f$ so that $\sum_i v_{i,f(j)}=c$.  This problem could then be solved by integer linear programming.  This is related to a $d$-dimensional subset-sum problem, so you might also be able to find other algorithms for multi-dimensional subset-sum and try them out as well.
How do we formulate it in that way?  If the grid has $d$ cells, we can think of a shape as a $d$-vector of 0's and 1's, with 1's in the cells covered by the shape.  Each shape can be placed in a number of different positions, yielding different vectors.  $v_{i,j}$ corresponds to the $j$th place where shape $i$ can be placed.  $c$ corresponds to the the numbers originally in the grid (well, the negation of those numbers, modulo $N$).  All arithmetic is done modulo $N$.
Slightly smarter brute force
Alternatively, here is a way to improve brute force a little bit, by trading memory for time.  Suppose you have $k$ shapes.  Start by enumerating all ways to place the first $k/2$ shapes onto an empty board of all zeros, and store all resulting positions in a hashtable or sorted list.  Then, enumerate all ways to place the last $k/2$ shapes onto the starting position, and look up each of the resulting positions in the hashtable or sorted list.  If you find any match, then that yields a solution.  This will let you push brute force a bit further -- potentially to about twice as many shapes -- if you have an unlimited amount of memory.  There are a lot of details involved in optimizing this to the max, but it's an idea you could consider if you brute force gets you close but falls a little bit short.  It is still an exponential-time algorithm so it will still hit a limit.


Pi-type over a list in dependent type theory

You asked several questions.
You asked about a type indexed by a list, so you can do this.
data DataType (A : Type) (F : A -> Type) : List A -> Type where
  empty : DataType A F []
  _bla_ : forall {xs} {x} -> DataType A F xs -> F x -> DataType A F (x ∷ xs)

Where F is a type family that is indexed by the elements of the list.
Apart from that, you mentioned tuples. Probably you want a sized vector (Data.Vec in stdlib) for tuples. For instance, Vec Nat 3 is such a type that 1 ∷ 2 ∷ [] and 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] are both invalid instances, only 1 ∷ 2 ∷ 3 ∷ [] is.


What is the complexity of chordalization?

If the graph doesn't already have any K4, then Q2 is the same as asking for whether the graph has treewidth at most two. This is easy to check in linear time: it's true iff every biconnected component is series-parallel.


A graph parameter possibly related to treewidth

Though we've chatted about this in person before, I'll add this in the hope that this will allow someone else to provide a complete answer.
In your process of adding vertices, define a partial function $f:V(G) \rightharpoonup V(G)$ from each vertex $v$ which gets used, to the vertex which was added when $v$ got used. Then it turns out that $f$ is a (causal) flow function (p. 39), which is a restricted version of a path cover. Indeed, your description of these graphs of "complexity k" (given a set of vertices which are to be the initially unused vertices, and the final unused vertices) is precisely the star decomposition of a "geometry" with a causal flow (p. 46 of the above article).
Although these "causal flows" have been studied mainly in the context of (measurement-based) quantum computation — where they are motivated by certain structures of unitary circuits — there are graph-theoretic results about them which are totally divorced from quantum computation:

Uniqueness modulo endpoints: the graphs with " complexity $k$ " are precisely those for which there exist (possibly intersecting) sets $S,T \subseteq V(G)$, both of size $k$, such that $G$ has exactly one path cover of size $k$ whose paths start in $S$ and end in $T$.
Extremal graphs: A graph on $n$ vertices which has "complexity $k$" has at most $kn - \binom{k+1}{2}$ edges.

Using these results, and given a candidate pair of sets $S,T$, determining whether or not they "subtend" a unique path cover in this way can be determined in time $O(k^2 n)$; but finding whether or not such sets of endpoints exist that is the apparent difficulty, and the extremal result above (which is only a necessary condition) seems to represent the state of the art in efficient criteria to determine whether such sets exist.


What is the intuition behind linear logic?

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an  answer somebody might have given had the question  been posted on cs.stackexchange.

In order to understand linear logic's notion of duality $(\cdot)^{\bot}$,
which forces conjunction and disjunction apart much further than we are used to in conventional logic, I recommend
not
  to think of linear logic in terms of resources (although this is
  an important reading). Instead  think of linear logic formulae $A$
  as processes that communicate
  at a port / name / channel. This interpretation has been fleshed out first in (1) to the best of my knowledge, but it's already alluded to in Girard's original work. As a picture:

(I'm not sure how properly to center images here.)
Linear conjunction $A \otimes B$ is interpreted as running processes $A$
  and $B$ in parallel.  The process $A \otimes B$
  communicates pairs $(a, b)$ at its port, where $a$ comes from
  $A$ and $b$ is $B$'s communication.

Dualisation $(.)^{\bot}$ (which is linear logic's
  negation) switches input and output. Hence the dual of $A \otimes B$
  is

$$
  (A \otimes B)^{\bot} \quad = \quad A^{\bot} ⅋ B^{\bot}
  $$

In this reading $A^{\bot} ⅋
  B^{\bot}$ is the process that communicates with $A \otimes B$.

Linear logic's equivalent of disjunction can
  be given a similar process-theoretic reading. The formula

$$
  A\ \&\ B
  $$

should also be seen as  two processes $A$ and $B$ in parallel, but rather than actively sending messages, they wait for
  the environment to decide which to run. So $A \& B$ sits there,
  waiting on its channel for a bit of information which decides if $A
  \& B$ should run as $A$ or as $B$. This is a 'parallel' version of
  the $if/then/else$ in sequential programmaning languages. The dual
  $(A \& B)^{\bot}$ of $A \& B$ is

$$
  (A \& B)^{\bot} \quad = \quad A^{\bot} \oplus B^{\bot}
  $$

can be seen as a process sending 1 bit of information to $A \&
  B$, namely: "continue as $A$" or "continue as $B$". This is similar to in  $if\ true\ then\ P\ else\ Q$ evaluating to $P$ while
  $if\ false\ then\ P\ else\ Q$ evaluating to $Q$, except that
the choice between $A$ and $B$ is now made by the environment.

  The !-operator also has a process-theoretic interpretation: if $A$
  is read as a process, then $!A$ can be read as running infinitely
  many processes $A$ in parallel.

In this reading the axioms $A \vdash A$ of linear logic become simple 'wires' that forward messages from processes $A^{\bot}$ to processes $A$. This interpretation of axioms is already in Girard's proof nets (3).

This process-theoretic interpretation  has been influential and
  given rise to a lot of follow-up work like e.g. (2) for session types.
 Nevertheless, there are some
edge cases that make it a bit awkward, and to the best of my knowledge
  it hasn't been made to work perfectly for full linear logic even in 2017.

1. S. Abramsky, Computational Interpretations of Linear Logic.

2. P. Wadler, Propositions as sessions.

3. Wikipedia, Proof net.


To which complexity class does this language belong?

(as pointed out by Robin the problem is in DP...)

...and it is also DP-complete.

In fact, Jörg Rothe has shown that this even holds for fixed k=4: Jörg Rothe: Exact complexity of Exact-Four-Colorability. Inf. Process. Lett. (IPL) 87(1):7-12 (2003)


If I arrange the disks into a spiral pattern then the problem is NP-hard. It may be even harder in your general case. This would be a variation on the polygon covering problem.

See https://en.wikipedia.org/wiki/Polygon_covering


Arranging letters to make a word in a regular language

With an idea by Louis Jachiet, we managed to design a PTIME algorithm for this task. Long story short, it's a dynamic programming algorithm where you sort the $b$'s by decreasing "ending time" (i.e., by increasing $q_i$ above), consider the $b$'s by intervals of "starting time" (the $p_i$ above), and restrict the search to greedy schedulings that follow the idea for $(ab)^*$ given in the question. Somewhat surprisingly, the problem is in PTIME even if the target regular language is also given as part of the input (i.e., not fixed). Also, the algorithm would also work if, instead of copies of the letter $a$, we had a fixed word on some alphabet; however all the $b$'s should be the same symbol.

I'll rephrase the problem of my question to a problem where each $b$ comes with a pair $(s_i, e_i)$ saying that this $b$ must be inserted with at least $s_i$ $a$'s to the left, and strictly less than $e_i$ $a$'s to the left. This is equivalent to the original problem phrasing in the question (take $s_i := p_i$ and $e_i := m + 1 - q_i$  where $m$ is the number of $a$'s), but it is a bit easier to reason with: we can now see the constraints as defining an interval $[s_i, e_i[$ of positions where the insertion can take place. By a position $p$, I mean a position in the word of $a$, i.e., $0 \leq p \leq m$; when we insert multiple $b$'s then they do not change positions of other $b$'s in the word of $a$'s. Besides, since all $b$'s are the same symbol, it suffices to know the position where we insert them; we don't care about the relative positions of the $b$'s that are all inserted at the same position in the word of $a$'s.

I will need to talk about state pair sets of the automaton, which are just sets $S$ containing pairs $(q, q')$ of states. Given a word $w$ over $\{a, b\}$, I will write $\phi(w)$ for the state pair set that it achieves, i.e., all $(q, q')$ such that there is a path from $q$ to $q'$ labeled by $w$, which can clearly be computed in PTIME from $w$ and an automaton representation of the word. Given two state pair sets $S$ and $S'$, I define $S \odot S'$ to be the set of all state pairs $(q, q'')$ that can be obtained by combining a pair of $S$ and of $S'$, formally $S \odot S' = {(q, q'') \mid \exists q', (q, q') \in S \land (q', q'') \in S'}$. Notice that we have $\phi(w w') = (\phi(w)) \odot (\phi(w'))$ for any words $w$ and $w'$. What is more, the question of whether a word is accepted or not boils down to checking whether $\phi(w)$ contains a pair $(q_0, q_f)$ for a final state $q_f$. (What I'm redefining here is basically the transition monoid of the automaton, for those familiar with it.)

I will consider the $b$'s by decreasing ending time $e_i$, and break ties in some arbitrary but consistent way, so when I talk about the $i$-th $b$, with constraints $(s_i, e_i)$, then it is the $i$-th $b$ according to this order that I fixed.

Let me now claim that, if we can achieve a word $w$ by insertions of $b$'s into the $a$'s, then we can achieve the same word $w$ by doing insertions following a greedy strategy: when I insert the $i$-th $b$ at a position $p$ in the word of $a$'s, then all subsequent $b$'s that could also go at that position (i.e., $s_j \leq p < e_j$ for some $j$) are inserted to the left of that position, i.e., their position is $p'$ with $p' \leq p$. Let's see why we can always restrict to greedy strategies without loss of generality. Consider a stategy to do insertions to achieve $w$, and let's see that we can change it into a greedy strategy that achieves the same word. Consider a violation in the current strategy where we insert the $i$-th $b$ at position $p$ (so $p_i \leq p < e_i$) and the $j$-th $b$ (with $j > i$) could also go at that position (so $p_j \leq p < e_j$) but it was inserted to the right, i.e., $p' > p$. Let's see why the $i$-th $b$ can also be inserted at $p'$, which justifies that we can fix that violation by swapping the two insertions, and thus iteratively repair any strategy to a greedy strategy.  By definition of the order, we have $e_j \leq e_i$, so as $p' < e_j$ we have $p' < e_i$. Now, as $p_i \leq p$ and $p < p'$, we have $p_i \leq p'$. So indeed $p \in [p_i, e_i[$ and we can indeed fix the violation by inserting the $i$-th $b$ at $p'$ and the $j$-th $b$ at $p$.

Now I can explain the dynamic algorithm. We will compute, for all $0 \leq i \leq j \leq m$, for all $0 \leq s \leq s' \leq m$, for all $0 \leq k \leq n$ (with $n$ the number of intervals), the set $S(i, j, s, s', k)$ which is the union of the state pair sets over all words that can be obtained by taking the subword of $a$'s from the $i$-th $a$ (included) to the $j$-th $a$ (excluded), performing insertions of $b$'s using exactly the $b$'s with position $i \geq k$ in the order (numbering them from $0$ to $n-1$) and with starting time $s \leq s_i < s'$, and considering the word obtained in this fashion (containing $j - i$ $a$'s and some $b$'s inserted before, after, or between them).

The quantity that we wish to compute to solve our problem is $S(0, m, 0, m, 0)$, telling us what can be achieved by inserting all intervals in the whole word of $m$ $a$'s; we then simply check if there is a pair of the form $(q_0, q_f)$ in the result, with $q_0$ the initial state and $q_f$ a final state.

The base case is the $S(i, j, s, s', n)$, where we ask what can be achieved without any insertions: this is simply the effect of the $a$'s on their own, formally, it is $\phi(a^{j-i})$.

Now, for the inductive step, consider $S(i, j, s, s', k)$ with $k < n$. Consider the $k$-th copy of $b$ and its interval $[s_k, e_k[$. If we don't have $s \leq s_k < s'$, then we are not considering this $b$, so we simply have $S(i, j, s, s', k) = S(i, j, s, s', k+1)$. Otherwise, we are considering the $k$-th $b$, and we claim that:

$$S(i, j, s, s', k) = \hspace{-1cm} \bigcup_{\max(i, s_k) \leq p \leq \min(j, e_k-1)}\hspace{-1cm} S(i, p+1, s, p+1, k+1) \odot \phi(b) \odot S(p+1, j, p+1, s', k+1).$$

In particular, if the interval for the $k$-th $b$ does not overlap with $[i, j[$, then $S(i, j, s, s', k) = \emptyset$ (meaning that we cannot perform the insertions).

To see why this formula holds, observe that we must insert the $k$-th $b$ as we are considering it, and this insertion must be at a position $p$ such that $s_k \leq p < e_k$, so $s_k \leq p \leq e_k-1$, and also we are considering insertions in the subword from the $i$-th $a$ (included) and the $j$-th $a$ (excluded) so $i \leq p \leq j$ (we can insert immediately after the end of this subword of $a$). Now, all remaining $b$'s (strictly after $k$) with starting position in $[s, s'[$ are partitioned between those with starting position in $[s, p+1[$ and those with starting position in $[p+1, s'[$. Let's argue that these $b$'s must be inserted as we claim, i.e., the first ones in the subword of $a$ between $i$ included and $p+1$ excluded (so at or before $p$) and the second ones between $p+1$ included and $j$ excluded (so strictly after $p$). For the second ones, this is clear, as their starting position is $\geq p+1$ so they must be inserted at position $p+1$ or later. For the first $b$'s, either their ending time is $\leq p+1$, in which case they must necessarily be inserted strictly before position $p+1$; or their ending time is $> p+1$, but in this case, as their starting position is $< p+1$, this means that they could legally be inserted at position $p$ where we inserted the $k$-th copy of $b$; now by definition of a greedy strategy, since they come after this $k$-th $b$ in the order which we inserted at a position $p$, then they must be inserted at a position $\leq p$.

Formally, correctness can be shown by showing inductively that the $S(i, j, s, s', k)$ contains the right state pair set: one direction is because what we compute really corresponds to a way to perform the insertions; the other is because any way to perform the insertions is equivalent to a greedy strategy, and all greedy strategies are represented by the above reasoning.

This algorithm clearly establishes that the problem is in PTIME, with complexity like $O(n \times n^4 \times m \times \mathrm{Poly}(A))$ where $A$ is the automaton. We're not claiming that this is optimal. :)


Is the problem of finding the chromatic number of a modified interval graph NP-Complete

I believe these graphs can be colored in polynomial time. Moron has already provided a reference, but here's an explicit algorithm.

Suppose that $G-uv$ is an interval graph, for edge $uv$, and form an interval representation for it. We can assume without loss of generality that no two intervals have the same endpoint. We can also assume without loss of generality that $u$ and $v$ are the two extreme intervals; for, if some other interval were extreme, we could remove it, optimally color the resulting smaller graph (also of the form interval+one edge), and then optimally extend the coloring to the removed vertex (because its neighborhood is a clique).

So the remaining question is: does $G-uv$ have an optimal coloring in which $u$ and $v$ have different colors, or does edge $uv$ require us to use one more color? But this is easily solved by a dynamic program on the subintervals of the interval representation.

In more detail, for subinterval $i$ let $C[i]$ denote the set of intervals (vertices of G) that cover that subinterval, let $D[i]$ be a Boolean value, true if there exists a coloring of the subinterval (in an optimal coloring of $G-uv$) that does not use the same color as $u$, and let $E[i]$ be the set of vertices that can be colored with the same color as $u$ (again, in an optimal coloring). As a base case, $C[0]=E[0]=\{u\}$ and $D[0]$ is false. When going from subinterval $i$ to subinterval $i+1$, across the right endpoint of an interval $w$, we set $D$ to be the disjunction of its old value and the predicate $w\in E[i]$, and we then remove $w$ from $C[i]$ and $E[i]$. When going across the left endpoint of an interval $w$, we add $w$ to $C[i]$, we add it to $E[i]$ if $D$ is true, and we change $D$ from true to false if the new size of $C[i]$ equals the number of colors in an optimal coloring of $G-uv$.

Then, the optimal number of colors of $G$ is the same as for $G-uv$ iff either D is true for the final subinterval, or E[i] has more than one member in the final subinterval. Otherwise, the optimal number of colors for $G$ is one plus the optimal number of colors for $G-uv$.


Nomenclature aside (a line graph is something different than what you describe), you appear to be describing the problem of ''maintaining order in a list''. You have a list of items $v_i$ (your graph), you can remove an item from one point in the list and re-insert it elsewhere, and you want to check whether one item appears earlier than another in the list. This problem has a constant-time solution; see Dietz and Sleator, "Two algorithms for maintaining order in a list", STOC 1987, https://www.cs.cmu.edu/~sleator/papers/maintaining-order.html and https://en.wikipedia.org/wiki/Order-maintenance_problem


I think what's confusing you is that $A \times B$ is both a product and a coproduct:

It is the product of two factors, namely $A$ and $B$.
It is the coproduct of $A$-many copies of $B$.

Once you realize this, you will see that we can obtain $A \times B$ as both a $\sum$ and a $\prod$:

Take $P : \mathtt{bool} \to \mathsf{Type}$ where $P(\mathtt{false}) = A$ and $P(\mathtt{true}) = B$. Then
$$\sum_{b : \mathtt{bool}} P(b) \simeq A + B$$
and
$$\prod_{b : \mathtt{bool}} P(b) \simeq A \times B$$
Take $Q : A \to \mathsf{Type}$ where $P(x) = B$ for all $x : A$. Then
$$\sum_{x : A} Q(x) \simeq A \times B$$
and
$$\prod_{x : A} Q(x) \simeq (A \to B)$$

We should therefore not pay attention to $A \times B$ when deciding on a good naming scheme for these two constructs.

The dependent exponential is exactly a dependent product.


Separation of limited nondeterminism classes?

For attempts to separate the bounded nondeterminism hierarchy, I think monotone dualization of prime formulas is the most salient topic.

Consider the decision problem

  MONOTONE DUAL
  Input: two monotone CNF formulas, from which no literals can be removed
  Question: is the one formula the dual of the other?

MONOTONE DUAL can be decided with $O((\log\ n)^2/\log\ \log\ n)$ nondeterministic steps.  There is also a quasi-polynomial $n^{o(\log\ n)}$ time upper bound for this problem which has stood since 1996.

So MONOTONE DUAL is in co-$\beta_2$P and also doesn't seem to require the full power of this class.  On the other hand, MONOTONE DUAL may be a good candidate for a problem that is outside P = co-$\beta_1$P.

This is surveyed in:

Thomas Eiter, Kazuhisa Makino, and Georg Gottlob, Computational aspects of monotone dualization: A brief survey, DAM 156 2035– 2049, 2008.  doi: 10.1016/j.dam.2007.04.017 (preprint)

I am not sure there is more work along these lines.  As with many other areas with the potential to separate P from NP, after some promising early progress new ideas now appear to be necessary.


Theoretical guarantees for running times of belief propagation methods?

BP and most of its variants are proved to converge on graphs without cycles. When you have cycles they show very strange behavior sometimes. For these cases people have tried different approximations schemes, for example Sherali-Adams, Lovasz-Schrijver, and Lasserre Hierarchies.

See [1] for a comprehensive review of these approximations. Also (Wainwright and Jordan, 2008) includes other class of approximations.

[1] http://cs.nyu.edu/~dsontag/papers/sontag_phd_thesis.pdf


You may need to look at this report:
https://www.cs.princeton.edu/~fiebrink/423/AmortizedAnalysisExplained_Fiebrink.pdf

Each individual operation takes $O(\log n)$ but when you apply amortized analysis to a sequence of operations, you get something interesting.

Directly from this report:
"However, amortized analysis can be used to show that any sequence of $m$ insert and delete operations causes $O(m)$ structural modifications in the worst case (Cormen et al. p.428). It can similarly be shown that the total time for  $m$ consecutive insertions in a tree of $n$ nodes is $O(n + m)$ (Tarjan 1985)."


How many more colours do you need if you add to $G$ a maximum matching from $G^c$?

One always has $\chi(G+M)\leq 2\chi(G)$, and this bound does not seem improvable in general. To see the bound itself, note that the only edges of the matching $M$ that can possibly ruin an optimal coloring of $G$ are those between two vertices of the same color class; in particular, we can color $G+M$ by simply creating two new colors for every original color and placing the two nodes on any such violating edge with distinct colors.
To see that this is tight, for any $k$, consider a $k$-partite complete graph with an even number of nodes in each part. It is easy to see that the original graph is $k$-colorable and that adding any perfect matching (which only can have edges within each part) will increase the clique number to $2k$, and so the chromatic number is at least $2k$.


In the context of regular languages, must the alphabet be finite?

It makes sense in some contexts in mathematics to consider strings or languages over infinite alphabets. For instance, this concept is used in the strong version of Higman's lemma. But a finite automaton requires a finite alphabet, and only finitely many symbols can actually appear in a single regular expression. So, specifically for the context of regular languages, alphabets must be finite.

It's not important whether you achieve this by declaring that "alphabet" means a finite set (as HMU and Sipser do) or whether you allow infinite alphabets and instead put the requirement of finiteness elsewhere than the definition of that word (as AU do).


Complexity of the search version of 2-SAT assuming $\mathsf{L = NL}$

Given a satisfiable 2-CNF $\phi$, you can compute a particular satisfying assignment $e$ by an NL-function (that is, there is an NL-predicate $P(\phi,i)$ that tells you whether $e(x_i)$ is true). One way to do that is described below. I will freely use the fact that NL is closed under $\mathrm{AC}^0$-reductions, hence NL-functions are closed under composition; this is a consequence of NL = coNL.

Let $\phi(x_1,\dots,x_n)$ be a satisfiable 2-CNF. For any literal $a$, let $a^\to$ be the number of literals reachable from $a$ by a directed path in the implication graph of $\phi$, and $\let\ot\leftarrow a^\ot$ the number of literals from which $a$ is reachable. Both are computable in NL.

Observe that $\let\ob\overline \ob a^\to=a^\ot$, and $\ob a^\ot=a^\to$, due to skew-symmetry of the implication graph. Define an assignment $e$ so that

if $a^\ot>a^\to$, then $e(a)=1$;
if $a^\ot<a^\to$, then $e(a)=0$;
if $a^\ot=a^\to$, let $i$ be minimal such that $x_i$ or $\ob x_i$ appears in the strongly connected component of $a$ (it cannot be both, as $\phi$ is satisfiable). Put $e(a)=1$ if $x_i$ appears, and $e(a)=0$ otherwise.

The skew-symmetry of the graph implies that $e(\ob a)=\ob{e(a)}$, hence this is a well-defined assignment. Moreover, for any edge $a\to b$ in the implication graph:

If $a$ is not reachable from $b$, then $a^\ot<b^\ot$, and $a^\to>b^\to$. Thus, $e(a)=1$ implies $e(b)=1$.
Otherwise, $a$ and $b$ are in the same strongly connected component, and $a^\ot=b^\ot$, $a^\to=b^\to$. Thus, $e(a)=e(b)$.

It follows that $e(\phi)=1$.


Representing bound variables with a function from uses to binders

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments.

To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, but the earliest place where I saw it for lambda terms was in an old essay by Knuth:

Donald Knuth (1970). Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages, E. Engeler (ed.), Lecture Notes in Mathematics 188, Springer.

On page 234, he drew the following diagram (which he called an "information structure") representing the term $(\lambda y.\lambda z.yz)x$:

This kind of graphical representation of lambda terms was also studied independently (and more deeply) in two theses in the early 1970s, both by Christopher Wadsworth (1971, Semantics and Pragmatics of the Lambda-Calculus) and by Richard Statman (1974, Structural Complexity of Proofs). Nowadays, such diagrams are often referred to as "λ-graphs" (see for example this paper).

Observe that the term in Knuth's diagram is linear, in the sense that every free or bound variable occurs exactly once -- as others have mentioned, there are non-trivial issues and choices to be made in trying to extend this kind of representation to non-linear terms.

On the other hand, for linear terms I think it's great! Linearity precludes the need for copying, and so you get both $\alpha$-equivalence and substitution "for free". These are the same advantages as HOAS, and I actually agree with Rodolphe Lepigre that there is a connection (if not exactly an equivalence) between the two forms of representation: there is a sense in which these graphical structures may be naturally interpreted as string diagrams, representing endomorphisms of a reflexive object in a compact closed bicategory (I gave a brief explanation of that here).


See exercise 9 of section 6.4 of The Art of Computer Programming.

Any irrational $A$ would work, because $\{kA\}$ breaks up a largest gap of $\{A\}, \{2A\}, \ldots, \{(k-1)A\}$ (I use the notation $\{x\}$ for $x\mod 1$).

But if $A = \phi^{-1}$ or $A = \phi^{-2}$, it has a special property: these are the only values for which neither of the two newly created gaps is more than twice as long as the other.


Online/approximate weighted and capacitated bipartite matching

I think there is no paper solving that exact problem, but "Online Vertex-Weighted Matching" by Aggarwal, Goel, Karande, and Mehta (2011) is very close. If I understood correctly, they solve your problem only with all capacities equal to one.

My best guess is that you will have to do some work to extend their guarantees and algorithm to your setting. On the other hand, a greedy algorithm probably should guarantee 0.5 of optimal by a standard argument: Consider the opt matching; for every "slot" in OPT left unmatched by greedy, there was some other match made that was more valuable (since the slot was available, its partner must have gone elsewhere). I hope you will forgive this discussion of methods contrary to your request.

(edit: I want to mention that this argument wouldn't work if the weights are on the arriving vertices; it's good to think about why.)


Can a computer simulate itself as part of a simulated world?

No, a computer cannot perfectly simulate itself in addition to something else without violating basic information theory: there exist strings which are not compressible.

Here's the simplest possible proof: suppose the computer has a total of $N$ possible states, and suppose there is something outside of the computer in the universe, so the universe has at least $N+1$ possible distinct states.  With zero overhead, each state of the computer can correspond to a state of the universe, but since the universe has more states than the computer, some states of the universe will map to the same state of the computer, in which case the simulation will not be able to distinguish between them.


While my initial instinct was also that the problem should be NP-hard, it looks like it might be close to a problem in P, namely list coloring on graphs whose blocks, or 2-connected components, are cliques. I am not sure to what extent this is helpful, because when you solve the reduced instance all meetings will be filled to capacity, which is an additional constraint on your problem. But if the rest of the argument holds up this might have workarounds, so I will state the partial progress.

If sensible, this reduction does not need to know which day a meeting happens to fall on, so I am using more relaxed notation (dropping the info about which day the meeting was on).

Introduce cap$_m$ vertices $$\{v_m^{(1)}, v_m^{(2)}, \ldots, v_m^{(c_m)}\}$$ for every meeting $m$. Let $M_r$ denote the set of all meetings $m$ that are associated with the constraint $c_r$. the edge set involves a big clique on all vertices involved in representing $m \in M_r$, that is, $$E = \{ (v_p^{(i)},v_q^{(j)}) | p,q \in M_r \}$$
$$\color{red}{\cup \{(v_p^{(i)}, v_q^{(j)})| p, q \text{ are meetings at the same day})\}\text{  [see comment below]} }.$$

The color pallette has one color for every person, and the list asssociated with a meeting vertex is the set of all people for whom the meeting is on their preference list.

A valid list coloring in the graph will fill all meetings to full capacity, and will never assign the same person to similar meetings, and will always give a person a meeting that they wanted to be in.

Some things to note:

The meetings will be filled to capacity, so this is not a completely accurate reduction. The simplest fix is to ask for a partial coloring, but I am not sure about the complexity of this question.  One could make the same copies of every meeting an independent set, and add a complete partite structure across meetings with the same constraint. Now, the color corresponding to a person can be repeated within a meeting. However, I am not completely sure that the graph structure now allows for the Ptime algorithm! The other fix would be to introduce junk colors in the pallette, but then some people may not get assigned to meetings at all.
The reduction works with longer preference lists, too.
Conflicts within the same day can also be handled with this modelling.

And this paper mentions that list coloring can be resolved in polynomial time when the blocks of the graph are cliques.


What are the best known upper bounds and lower bounds for computing O(log n)-Clique?

The best known upper bound is essentially $n^{O(\log n)}$. You can improve a little on the constant factor in the big-O using fast matrix multiplication, but that's about it. There are a lot of algorithmic references on the $k$-clique problem which describe this reduction, it originates from papers of Itai and Rodeh and Nesetril and Poljak. (Apologies to Czech readers, I am ignorant of the proper diacritical marks.) See http://en.wikipedia.org/wiki/Clique_problem

If you could solve $\log n$-clique in $n^{\varepsilon \log n}$ for every $\varepsilon > 0$, then you could also solve 3SAT in subexponential time. This can be seen as a "lower bound" to further progress. One way to prove this is to first show that if $\log n$-clique in $n^{\varepsilon \log n}$ for every $\varepsilon > 0$, then MaxCut on $n$ nodes is in $2^{\varepsilon n}$ time for every $\varepsilon > 0$. This follows directly from a theorem in my ICALP'04 paper that relates the time complexity of MaxCut to the time complexity of $k$-clique. From there, one can appeal to standard reductions to reduce 3SAT to MaxCut, showing that subexponential MaxCut implies subexponential 3SAT.

In terms of unconditional lower bounds, nothing nontrivial is known, to my knowledge. We don't even know how to show that $O(\log n)$-clique isn't solvable with an algorithm that runs in linear time and uses only logarithmic workspace.


Type inference for imperative statements other than assignment

If you're looking for a neat, functional reference to type-inference, I'm a bit partial to Gundry, McBride, and McKinna's 2010 "Type Inference in Context", though this may not be a good guide to any actual existing implementations.

I think part of the answer is that, beyond the value restriction, there really isn't that much difficulty adapting Hindley-Milner type inference to imperative languages: if you define e1; e2 as syntactic sugar for (fn _ => e2) e1 and define while e1 do e2 as syntactic sugar for whiledo e1 (fn () => e2), where whiledo is a regular recursive function

fun whiledo g f = if g then (f (); whiledo g f) else ();

then everything will work fine, including type inference.

As for the value restriction being a special technique, I like the following story; I'm pretty sure I picked it up from Karl Crary. Consider the following code, which the value restriction will prevent you from writing in ML:

let
   val x: 'a option ref = ref NONE
in
   (x := SOME 5; x := SOME "Hello")
end

Compare it to the following code, which is totally unproblematic:

let
   val x: unit -> 'a option ref = fn () => ref NONE
in
   (x () := SOME 5; x () := SOME "Hello")
end

We know what the second example does: it creates two new ref cells containing NONE, then puts SOME 5 in the first one (an int option ref), then puts SOME "Hello" in the second one (a string option ref).

But think about the first example in terms of how we would represent x in System F (the polymorphic lambda-calculus). In such a setting, x would be a value of type "$\forall \alpha. \mbox{ref}(\mbox{option}(\alpha))$", so that means that, as a term, the value of x must be a (type) lambda: "$\Lambda \alpha. \mbox{ref}[\alpha](\mbox{NONE})$".

This would suggest that one "good" behavior of the first example is to behave exactly the same way the second example behaves - instantiate the type-level lambda two different times. The first time we instantiate x with int, which will cause x [int] to evaluate to a reference cell holding NONE and then SOME 5. The second time we instantiate x with string, which will case x [string] to evaluate to a (different!) reference cell holding NONE and then SOME "Hello". This behavior is "correct" (type-safe), but it's definitely not what a programmer would expect, and this is why we have the value restriction in ML, to avoid programmers dealing with this unexpected sort of behavior.


Ruzzo-Simon-Tompa oracle access mechanism

A definition of oracle access that works for small circuit complexity classes (the $AC^k$ and $NC^k$ hierarchies) as well as for logarithmic space classes, with the property that all known inclusions relativize, can be found in this paper:

Klaus Aehlig, Stephen Cook and Phuong Nguyen: Relativizing Small Complexity Classes and their Theories, CSL 2007, Springer LNCS 4646


Structural normalization algorithm for the simply typed lambda calculus

You can: define /hereditary substitution/ on already normalized STLC terms using structural induction (where the induction is (in part) on the type).
I couldn't find the reference I was thinking of right now, but a quick search for "agda hereditary subtitutions STLC" pointed to various relevant pages, such as https://github.com/ezyang/lr-agda/blob/master/STLC.agda


NP-hardness of a special case of Number Partitioning

(This is a little more detailed version of my comments on the question.)

As turkistany suggested in a comment on the question, this problem is NP-hard for every constant k≥3 by a reduction from the k-partition problem.  The reduction does not change instances at all: just note that the maximum of the product of the sums is at least (∑ai/k)m if and only if the numbers can be partitioned into m sets each with size k whose sums are all equal.

Note that the input to the k-partition problem is usually defined to be km numbers which may not be all distinct, and this is essential in the standard proof of its NP-completeness (such as the one in Garey and Johnson).  Therefore, the reduction above only proves the NP-hardness of a slight generalization of the current problem where the input is allowed to be a multiset instead of a set.  However, this gap can be filled because the k-partition problem remains NP-complete even if the numbers in the input are required to be all distinct; see [HWW08] for the case of k=3 (see also Serge Gaspers’s answer to another question), which can be modified easily for larger values of k.

In addition, everything stated here remains NP-complete/NP-hard even when the numbers in the input are given in unary.

[HWW08] Heather Hulett, Todd G. Will, Gerhard J. Woeginger.  Multigraph realizations of degree sequences: Maximization is easy, minimization is hard.  Operations Research Letters, 36(5):594–596, Sept. 2008.  http://dx.doi.org/10.1016/j.orl.2008.05.004


What are good references on understanding online learning?

Most online learning algorithms come from at least one out of these lineages:

the perceptron

State of the art perceptrons are the passive-aggressive algorithm, the structured perceptron, and their many varieties.
The winnow

The winnow has been reformulated as exponentiated gradient methods, and can be applied to structured problems as well. There are also varieties that deal directly with L1 regularization (to guarantee sparsity), such as SMIDAS.
Stochastic gradient descent

Stochastic gradient descent is when you apply online optimization to a possibly batch problem. State of the art algorithms are Leon Bottou's LaSVM, Pegasos, and many neural network algorithms can be easily trained in this setting. See the theano tutorial for many examples. Maybe online EM fits here.
particle filtering

This is also known as rao-blackwellized inference, and it allows you to update a graphical/probabilistic model as more data arrives. Some good examples are online topic models and the NIPS tutorial on SMC.

There are also some broader issues with online learning, like online-to-batch conversion, budget techniques for online learning with kernels (like this paper, this paper, and this paper), many different flavors of generalization bounds, sparsity concerns (and also the SMIDAS paper I cited above), hashing to save memory, and many other issues.


Below is a long-winded answer, but tl;dr in the general case there is no hope for such a formulation, but for many of the particular classes of sparse graphs that have regularity lemmas this formulation exists.

For background, there are two popular versions of the SRL.  They are: for any fixed $\varepsilon > 0$ and any $n$-node graph $G = (V, E)$, one can partition $V = V_0 \cup V_1 \cup \dots \cup V_p$ into $p = O_{\varepsilon}(1)$ parts so that ...

  (Combinatorial Phrasing) (1) $|V_0| \le \varepsilon n$ and the sizes of any $V_1, \dots, V_p$ differ by at most $1$ ($V_0$ is called the "exceptional set"), and (2) all but $\varepsilon p^2$ pairs of the remaining parts $(V_i, V_j)$ satisfy
  $$\left|d(S, T) - d(V_i, V_j)\right| < \varepsilon \text{ for all } S \subseteq V_i, T \subseteq V_j$$
  (here $d(\cdot, \cdot)$ gives the density between the parts, i.e. the fraction of edges that are present).
  (Analytic Phrasing) Letting
  $$\mathop{disc}(V_i, V_j) := \max \limits_{S \subseteq  V_i, T \subseteq V_j} |V_i||V_j|\left|d(V_i, V_j) - d(S, T)\right|,$$
  we have
  $$\sum \limits_{i, j =0}^p \mathop{disc}(V_i, V_j) < \varepsilon n^2.$$

The "combinatorial phrasing" (I just made these names up, they are not standard) is the original and probably more famous one, whereas the "analytic phrasing" is more modern and related to graph limits, etc (I think it was popularized here).  To my eye the analytic one is the right formalization of "graph approximated by union of bipartite expanders," since it gives a control on the total "error" of such an approximation, and there is not an exceptional set in which to hide mass.  But at this point this is just cosmetic, because it's an easy but important lemma that these two phrasings are equivalent.  To get from Combinatorial to Analytic, just union bound the contribution to discrepancy of the irregular parts and exceptional set.  To get from Analytic to Combinatorial, just move any part that contributes too much discrepancy to the exceptional set and apply Markov's Inequality to control its mass.

Now to sparse regularity.  The goal of sparse regularity is to replace the $\varepsilon$ in the respective inequalities with $\varepsilon d(G)$, where $d(G)$ is the fraction of all possible edges present in $G$.  Critically, with this change, the two phrasings are no longer equivalent.  Rather, the Analytic phrasing is stronger: it still implies Combinatorial exactly as before, but Combinatorial does not generally imply Analytic, because (as anticipated in the OP) one can potentially hide a lot of density in the exceptional set or between the non-regular pairs of parts.  Indeed, this separation is formal: the lower bound graphs for the dense SRL (say, this one) imply that the Analytic Phrasing doesn't extend in general to sparse graphs, but the paper by Scott linked in the OP shows that the Combinatorial Phrasing actually does extend to all sparse graphs with no conditions.

The survey linked in the OP mostly talks about an SRL for "upper-regular" sparse graphs, which roughly means that the graph has no cuts that are denser than average by more than a constant factor.  For these particular graphs, the Combinatorial and Analytic phrasings are equivalent, because there can't be too much extra mass hidden in the exceptional parts so their contribution to discrepancy can be union bounded like in the dense case.  So these graphs have an "approximated by union of bipartite expanders" interpretation.

Finally, I should mention that there are many other hypotheses in the literature that also imply equivalence between these phrasings.  For example, $L_p$ Upper Regularity (defined here) is more general than Upper Regularity and is still enough to imply equivalence.  However, for this graph class and others, I am only aware of associated weak regularity lemmas.


Is this variant of bitwise cyclic tag Turing-complete?

It is. There's a fairly simple construction compiling from CT to CT2.
First, consider that it's possible to double every command in a CT program without producing any behaviour (that is, A becomes AA, B becomes BB, C becomes CC). The queue of bits now has every bit doubled, but the cycle of commands only does anything with every second bit, so the modified behaviour has the same behaviour as the original.
Let $n$ be the number of A commands in a program. You can observe that pushing a string of $n$ false bits (indeed, any multiple of $n$) will have no effect on a CT program (as will not pushing a string of $n$ false bits), so you can safely write a string of $n$ Bs anywhere in a program without changing its behaviour.
Suppose we take a CT program with every command doubled, and insert a string of $2n$ Bs immediately before each AA pair (i.e. immediately before an A before it was doubled); here, $n$ is the number of A commands after the doubling (i.e. twice the number of A commands in the original program). This does not change the behaviour of the program. Additionally, those Bs that happen to be in even positions can be changed to Cs without changing the behaviour of the program (because the even-numbered bits in the queue are skipped by the second A command of a pair, their values are irrelevant). We can thus change somewhere from $0$ to $n$ of each run of $2n$ inserted Bs into Cs, and produce a CT program which has identical behaviour to the original, and for which additionally the number of Bs between each pair of As is a multiple of $n$.
Now consider what happens if we reinterpret this CT program as a CT2 program. It will have mostly the same behaviour as the CT program, except that sometimes an additional run of a multiple of $n$ false bits will be appended to the queue (due to B commands running when the head of the queue is false). The added bits will always be in runs whose length is a multiple of $n$.
When these runs reach the front of the queue, they will, in effect, end up pushing a number of false bits onto the queue equal to the number of B commands in the entire program (rather than doing nothing, like they would in CT); this happens regardless of where the false bits appear in the queue and regardless of what point of the program we have reached (they cycle through the program from some point in it back to that point again). But this is still going to be a multiple of $n$ (the number of B commands between any two A commands is a multiple of $n$, so the total number of B commands is produced by adding multiples of $n$ and is still a multiple of $n$).
In other words, there's a direct correspondence between CT programs constructed as above (which have the same computational power as CT programs in general), and their reinterpretations as CT2 programs. If you define CT2's halt state as "the queue consists entirely of false bits", this is sufficient to make CT2 Turing-complete. (I don't know whether it's possible for nontrivial CT2 programs to halt if you continue to define the halt condition as the queue being empty, though.)
(As a side note: is this question just a question-in-the-abstract asked out of curiosity, or do you need it as an intermediate result for something? I've been looking at similar but more complex constructions when trying to produce Turing-completeness results for various simple languages, and if you're aiming to do something similar yourself, I'd be interested to know what you're working on.)


The answer to your question is yes. It is a result of Erdős and Szemerédi from 1972. We know a little, but non-zero about pseudo-random properties of Ramsey graphs. For example, we know that many different kinds of induced subgraphs appear in such a graph. See, for example, a paper by Alon–Balogh–Kostochka–Samotij and references therein.


Fixed parameter tractable Integer Programming and $FPP$

You're confusing decision problems (in the classical sense) with parameterized decision problems. Classical decision problems are subsets of $\Sigma^*$, whereas parameterized decision problems are often considered as subsets of $\Sigma^* \times \mathbb{N}$ (see [1, Chapter 2]). Classical complexity classes (such as NC, P and NP) are sets of classical decision problems, and parameterized complexity classes (such as FPT) are sets of parameterized decision problems.
(If $Q \subseteq \Sigma^* \times \mathbb{N}$ is a parameterized decision problem, then the unparameterized version of $Q$ denotes the classical decision problem $Q' = \{ x\ |\ (x,k) \in Q \}$.)

Integer linear programming (ILP) is a classical decision problem (that is, the variant you're referring to: deciding whether there exists a feasible integer solution that achieves at least a certain value of the objective function). If you consider a parameterized variant of this problem (e.g., when taking as parameter the number of variables), it is a parameterized decision problem. So asking whether the problem of ILP parameterized by the number of variables is P-complete or in NC does not make sense. What you should be asking is whether it is complete for a parameterized analogue of P, or whether it is contained in a parameterized analogue of NC.

The parameterized complexity class FPT (consisting of all parameterized decision problems that are fixed-parameter tractable) is the parameterized analogue of P. One possible appropriate parameterized analogue of NC is the parameterized complexity class FPP (see [2]). FPP consists of all parameterized decision problems that are solvable in time $f(k) \cdot (\log n)^c$ by a parallel algorithm with at most $f(k) \cdot n^c$ processors, for some computable function $f$ and some constant $c$, where $n$ is the input size and $k$ is the parameter value.

To answer question (2): an example of a parameterized decision problem that is FPT-complete and whose unparameterized version is NP-complete, is the problem of satisfiability of propositional logic formulas in CNF, parameterized by the size of the smallest strong backdoor to Horn (see, e.g., [3]). Essentially, this problem is FPT-complete (under an appropriate parameterized variant of log-space reductions) because satisfiability for propositional Horn formulas is P-complete (under log-space reductions).

For any NP-complete decision problem, you can come up with a parameterized version that is in FPP: take as parameter the size of the input. Then the problem is (trivially) solvable in time $f(k)$ (for some exponential function $f$) on a single processor. Basically, such an algorithm can solve the problem in brute force in time $f(k)$. You're probably asking for natural parameterized variants of NP-complete problems that are in FPP.

References

[1] Downey, Rodney G., and Michael R. Fellows. Fundamentals of parameterized complexity. Springer, 2013.

[2] Cesati, Marco, and Miriam Di Ianni. Parameterized parallel complexity. European Conference on Parallel Processing. Springer, Berlin, Heidelberg, 1998.

[3] Gaspers, Serge, and Stefan Szeider. Backdoors to satisfaction. In: The Multivariate Algorithmic Revolution and Beyond. Pages 287-317. Springer, 2012.


Basic property of boolean functions with restrictions

This is Corollary 3.22 of Analysis of Boolean Functions, by Ryan O'Donnell (2014). You may want to consult the proof in the book, or look directly at the online version (which has a different numbering: this corresponds to Corollary 22 there).

Note that you can obtain a version of the book following this link.


W[1]-hard problems on bounded degree graphs

Ball and Trap I remains $W[1]$-hard when restricted to binary trees.

Theorem 5 states:

  Theorem 5. Ball and Trap I remains $W[1]$-hard restricted to binary trees,
  the maximum number of traps per vertex is one per color, and balls are placed
  on neither leaves nor parents of leaves.


In a 1967 pager, Al Rosenberg gave the example of a language which is deterministic linear time but not deterministic quasi-realtime that Book & Greibach probably refer to.
Rosenberg mentions that such examples were published previously by himself and Cole.


Do past time LTL and future time LTL have the same expressiveness?

The quick summary is that LTL with only past and no future modalities defines properties expressed over finite-words and these are the star-free subset of the regular languages. Standard LTL when extended with past-time modalities does not have more logical expressive power than LTL with only future modalities but properties can be defined in an exponentially succinct manner.

For a more detailed answer, there are at least three logics one can consider in answering your question and at least three different notions of expressiveness.

Standard Linear Temporal Logic (LTL), which has the standard modalities next and until and is interpreted over traces that have a finite history and an infinite future.
Past-time Linear Temporal Logic (ptLTL), which has the modalities "previously" instead of "next" and "since" instead of until and is interpreted over finite traces, or at some point in an infinite trace but refers to the history of the trace.
Temporal logic with past and future modalities (sometimes abbreviated to TL), which has the modalities of LTL and ptLTL and is interpreted either over infinite traces or over finite and infinite traces.

The three notions of expressiveness are to ask (i) what languages (of finite or infinite words) each logic can define, (ii) what first-order structures these logics define, and (iii) what the complexity of defining a given language (or first-order structure) in each logic is. A more refined vocabulary for comparing expressiveness is provided by the notion of hierarchies, which are briefly mentioned at the bottom.

First-Order Structures definable by temporal languages

Kamp in 1968 studied an until modality that is slightly different from the notion commonly used in computer science today. I will write it as $\mathit{Until}_+$ for because a formula $p ~Until_+~ q$ is true at time instant i if $q$ is true at some $j > i$ and if $p$ holds at all $i < j' < j$. Note that the orders are strict. The temporal-dual is the modality $Since_+$. Kamp compared temporal logics to the Monadic First-Order Logic of Order (MLO, sometimes MFLO or FMLO). MLO formulae contain unary predicate symbols and a relation $<$ and are interpreted over linear orders.

Kamp's theorem shows that a logic with only $Until_+$ and $Since_+$ modalities is expressively equivalent to MLO when both logics are interpreted over the naturals or over the non-negative reals. In fact, Kamp's theorem applies to a family of structures called Dedekind-complete chains (which notably does not include the non-negative rationals). Stavi's theorem shows that a temporal logic with standard since and until and a special since and until modality is expressively-equivalent to the first-order monadic logic of order over every linear order. The notion of expressiveness in these results is "definability of first-order structures".

Gabbay, Pnueli, Shelah and Stavi considered a family of MLO formulae called future formulae, which intuitively only refer to future points in time. They showed that on a family of models called discrete, complete orders, which includes the naturals, future MLO formulae have the same expressive power as temporal logic with the $Until_+$ modality, a next and previously modality. So these results relate certain temporal and first-order logics on certain structures.

Relating languages to first-order logic, McNaughton and Papert showed that first-order definable languages are star-free and regular, which in conjunction with Kamp's theorem shows that all the logics above only define subsets of regular languages. Adding the next and previous modalities does not change what you can define and a proof that the third logic above still defines only the star-free regular languages is due to Zuck and Pnueli, I believe.

Comparative expressive power of temporal languages

Kamp was also one of the first to study how the properties one can express changes with the modalities in a temporal logic.  He showed that the $Until_+$ modality cannot be expressed in a logic with the Eventually, Next and more modalities. This difference in expressive power led him to study the $Until_+$ and $Since_+$ modalities.

Gabbay, Pnueli, Shelah and Stavi proved what is called a separation theorem. They showed that a formula that involves $Until_+$ and $Since_+$ can be written as a Boolean combination of formulae that involve either only $Until_+$ or only $Since_+$. (The story goes that when Kamp heard of a form of this separation theorem from Gabbay, he went out and bought Gabbay a cake.) This paper and separation result is sometimes cited as the reason for not including past modalities in temporal logics. It follows from their results that for a formula with $Until_+$ and $Since_+$, there exists a formula involving only $Until_+$ such that at time instant $0$, either both are true or both or false. It follows from this result that a temporal logic with the standard $Next$, $Until$, $Since$ and $Prev$ modalities, when interpreted over time indexed by the natural numbers (the standard semantics in computer science) has the same expressive power as LTL with only $Next$ and $Until$.

Unfortunately the only algorithm known to compute the separation above non-elementary complexity. Moreover, not every temporal logic has the separation property. In particular, if you only have an eventually and previously modality, separation does not hold. Lichtenstein, Pnueli and Zuck did show that every formula in LTL with past modalities is equivalent to a formula with the form below.

  $\bigvee_1^n (GF~\varphi_i) \land (FG~\psi_i)$, where $\varphi_i$ and $\psi_i$ do not contain standard $Until$ or $X$.

Complexity

In terms of complexity, it is known that temporal logic with past-time modalities is exponentially more succinct than LTL with only future-time modalities. Nonetheless, a result of Sistla and Clarke (1985) shows that the model checking problem for both is in PSpace. The actual complexity issues are a bit more complicated because one can ask for lower-bounds for expressiveness in both logics involved in a comparison. I recommend consulting the references below for more on this.

Vince Bárány's temporal logic course has all the reading material in one place.
Temporal Logic with Past is Exponentially More Succinct, Laroussinie, Markey, and Schnoebelen has recent results on a logic with a now modality and a forgettable notion of past.
The Glory of the Past, by Lichtenstein, Pnueli and Zuck is the definite starting point for reading on complexity differences between LTL with and without past-time modalities.
Lenore Zuck's PhD thesis is a good place to read about background on past and future modalities, in particular Chapters 2 and 3. Chapter 5 has the main results on expressiveness of the logic with past and regular languages.
Propositional temporal logics: decidability and completeness, Lichtenstein and Pnueli, 2000. Studies decidability and completeness of LTL with past and future modalities and has surveys the history of these logics.
Separation - past, present and future, Hodkinson and Reynolds, is a survey of many different logics using the notions of until and since from Kamp, and which discusses these issues from the perspective of the separation theorem.
Expressive Power of Temporal Logics, Rabivonich, 2002 discusses several other notions for comparing expressiveness such as dot-depth, quantifier alternation and basis for a temporal logic.
Efficient Monitoring of Safety Properties, Havelund and Rosu studies an application of ptLTL, and is a place to find a definition of the logic.
The Rise and Fall of LTL by Vardi is a talk that covers most of this and much more from a high level.
Specification in CTL+Past for Verification in CTL, Laroussinie and Schnoebelen, 2000, will answer the questions you haven't yet asked about what happens if you have past-time modalities in a branching-time logic.


Find minimum number of transformations to transform from input to target string

EDIT

As noted by usul, my previous answer is too broad, so these are some additional notes with personal ideas (so it is now more like an extended comment, than an answer):

If the given grammar is context sensitive, the alphabet has size >= 2 and there are no limits in the number of transformations, then even the problem of deciding if the grammar generates the target string is undecidable. You can easily find a grammar that simulates a NTM; as pointed out by Jeffe Markov algorithms are Turing complete, so given a TM and a string w you can build a grammar and a source string that generate a target string iff TM halts on w. So finding the minimum is undecidable, too.

If you put a limit in the number of transformations (polynomial), then the problem of deciding if the grammar generates the target string is PSPACE complete, and the problem of finding the minimum number of transformations is surely harder.

If the number of transformations is fixed, I think that the the problem is NP complete (I've a fuzzy idea of a quick reduction from monotone NAE-3SAT)

I leave the previous answer below.

The problem of finding the smallest CFG grammar  that generates a given string (also known as Minimum Grammar Compression or MGC) is NP-complete (J. Storer, "NP-completeness results concerning data compression", 1977).

I think that the complexity of the problem when the alphabet is restricted to $\{0,1\}$ (2-MGC) is still unknown.

If you switch to context sensitive grammars (LBAs) then you can look at resource-bounded Kolmogorov complexity. Unlike the unbouded Kolmogorov complexity, finding the smallest program that computes a given string is decidable, but we are obviously nearby intractability. There is a lot of reasearch on the subject (and many open problems); for example consider a binary string of length $2^n$ that represents the truth table of a boolean function $f$ and an integer $s$; the complexity of deciding if there is a boolen circuit of size at most $s$ that computes $f$ is unknown (probably not in $P$ but also unlikely to be NP-complete). Here it is a simple introduction and a very nice paper on the power of random strings.


Finding islands of vertices in a network of roads containing one-way streets

As Robin says, you want strongly connected components.  They can be easily found using Tarjan's algorithm, Gabow's algorithm, or several others.


What's a good advanced textbook/resource for studying the complexity of counting and combinatorics?

If I understood correctly, you're looking for a book (chapter) on counting complexity. In this case, I'd recommend the book of Sanjeev Arora and Boaz Barak, which has a chapter on counting complexity. A draft of it can be found here.

Concerning Extremal Combinatorics, Wiki suggests reading Extremal and Probabilistic Combinatorics by Noga Alon and Michael Krivelevich which contains pointers to some resources (mainly graph-related).


The Average-case Complexity of Simplex Algorithm

The first thing that comes to mind is "Smoothed Analysis" of Spielman and Teng: arxiv.org/pdf/cs/0111050.pdf. Their main result is Theorem 5.0.1, which bounds the expected (over "typical instances") runtime of a version of the Simplex algorithm by a polynomial, though the degree of the polynomial is not stated there.


I highly recommend Paolo Codenotti's thesis for the group-theoretic aspects, and the book The Graph Isomorphism Problem: Its Structural Complexity by Johannes Köbler, Uwe Schöning, and Jacobo Torán for the complexity aspects.


Efficient algorithm for updating a parse tree

As per @Agos request, I turned the comment into an answer.

First, I must admit that I'm not really knowledgeable in this field. Yet I suggest you read the papers Building friendly parsers and Efficient and Flexible Incremental Parsing to have a view of what algorithms were used for incremental parsing before 2000.

For updated treatments, you may take a look at these papers:

Lazy functional incremental parsing (2009)
Practical, incremental, noncanonical parsing: Celentano's method and the Generalized Piecewise LR parsing algorithm (2006)
Incremental validation of XML documents (2004)
Incremental parsing in language-based editors: user needs and how to meet them (2001)
Incremental Parsing and the C Preprocessor (Couldn't find the PDF anywhere. It is from Google cache.)

More info: There are (at least) two approaches to parsing/compilation:

The batch approach, in which the whole block of code is parsed/compiled.
The incremental approach, in which the document is first parsed/compiled in the batch mode, and then changes are detected and the minimal re-parsing/re-compilation is applied. This approach not only increases the parse/compilation speed, but also helps in IDE nifty features such as background compilation, which is related to lazy compilation. (You can also search about commercial features such as the  IntelliSense).


Is contextual equivalence of a language with `quote`-`eval` trivial or not?

First, this entirely depends on what you take to be your set of contexts.  If (quote []) is a context, then contextual equivalence is syntactic equivalence.

Traditionally, contexts for contextual equivalence are taken to be contexts in which "expressions", in whatever meaning that has in the language, can appear. This rules out contexts like "[]", where the context places its argument inside a string literal. These kinds of contexts were also, IIRC, ruled out by Quine when he originally described referential transparency.

From this perspective, I think (quote []) is also not a context. Instead, the contexts are the places where expression evaluation could potentially happen, such as in the body of a function or in the argument of an application.

Potentially problematically, this means that in a Lisp program with macros (or a Racket or Scheme program) you don't know what the contexts are until you run the potentially-nonterminating macro expansion process, because you don't even know where the expressions are. Whether you think this is a problem or not is mostly a philosophical question rather than a technical one.


Karp-like reductions vs Cook-like reductions for Functional Complexity Classes.

I think this situation is too general to draw many conclusions, but here goes...

If $A$ is closed under Cook-like reductions, then (2) would imply $B \subseteq A$, contradicting (1), so it tells you that $A$ is not closed under Cook-like reductions.

One way to paraphrase the original statement is: to make the classes equal in power requires more than a single query.

One can then ask about other intermediate types of reductions to get a better sense of just how many queries are needed and in what way e.g. are the classes equivalent under truth-table (nonadaptive) reductions? What's the best bound we can put on the number of queries ($2$, $O(1)$, $O(\log n)$?) Since these are counting classes, one could also ask about parsimonious reductions.


Does XOR automata (NXA) for finite languages benefit from cycles?

I think that the answer is the affirmative.  Maybe there is a simpler proof, but here is a sketch of a proof which uses linear algebra.

Like domotorp, we will view a configuration of an n-state XOR automaton as a vector in V=GF(2)n.

Let L be a finite language over an alphabet Σ={1, …, k}, and consider an XOR automaton for L with the minimum number of states.  Let n be the number of states.  We assume that the states are labeled 1, …, n, and state 1 is the initial state.

First we set up the notation.  Let v0 = (1, 0, …, 0)T ∈ V be the elementary vector corresponding to the initial state, and let s be the row vector whose ith entry is 1 if and only if state i is an accepting state.  The subspace R = {v: sv=0} of V corresponds to the configuration vectors that are rejected.

For each a∈Σ, let Aa be the n×n matrix over GF(2) which represents the transition caused by letter a.  For example, the configuration vector after reading the input string ab is AbAav0.  For a string σ=a1…at, we denote the product Aat…Aa1 by M(σ).  Let S = {A1, …, Ak}.

A subspace W of V is said to be S-invariant when AW ⊆ W for every A∈S.  In our context, this means that once the configuration vector goes in W, there is no way out of W by reading more letters.

Because this XOR automaton has the minimum number of states, we have the following properties.

The only S-invariant subspace of V that contains v0 is V itself.  This is because if W is a proper S-invariant subspace containing v0, then we can use W in place of V, contradicting the minimality.
The only S-invariant subspace contained in R is {0}.  This is because if W is a nontrivial S-invariant subspace contained in R, then we can use the quotient vector space V/W in place of V, again contradicting the minimality.

Because L is finite, let m be an integer larger than the length of any string in L.

Lemma 1.  For any string σ of length at least m, we have that M(σ)=0.

Proof.  First we prove that for any string σ of length at least m, we have that M(σ)v0=0.  Let W be the subspace of V spanned by {M(σ)v0: σ is a string of length at least m}.  By definition, W is S-invariant.  Because the XOR automaton in question rejects these strings σ, W is contained in R.  Therefore W={0}, which means that M(σ)v0=0 for all such strings σ.

Now consider any vector v∈V.  Because the only S-invariant subspace of V that contains v0 is V itself, v can be written as a linear combination of vectors of the form M(τ)v0 for some strings τ.  Because M(σ)M(τ)v0 = M(τσ)v0 = 0 (the latter equality follows from the previous paragraph because the length of τσ is at least m), it holds that M(σ)v=0.  ■

We need one more fact from linear algebra.

Lemma 2.  Let A1, …, Ak be n×n matrices over a field, and define M(σ) as above.  If there is m≥0 such that M(σ)=0 for every string σ of length at least m, then the matrices A1, …, Ak are simultaneously similar to strictly lower triangular matrices (that is, there exists an n×n nonsingular matrix P such that the matrices P−1A1P, …, P−1AkP are strictly lower triangular).

The case of k=1 is a well-known characterization of nilpotent matrices, and Lemma 2 can be proved in the same way.

Now consider the n-state XOR automaton in which the transition matrix corresponding to symbol a∈Σ is given by P−1AaP, the initial configuration vector is given by P−1v0, and the characteristic (row) vector of the accepting states is given by sP.  By construction, this XOR automaton accepts the same language L.  Because the transition matrices are strictly lower triangular, every transition edge in this XOR automaton goes from a state with a smaller index to a state with a larger index, and therefore this XOR automaton is acyclic.  Although the initial configuration vector may have more than one 1s, it is easy to convert this XOR automaton to a usual XOR automaton with a single initial state for the same language without increasing the number of states or ruining the acyclicity.


Why is regularity a problem in cubical type theory?

The difficulty is in making such a reduction compatible with all the other reductions involving transport/coe. From one perspective it is a “confluence” problem. It is unfortunate that in the community, so much was said about "decidability of degeneracies" that we began to give the impression that this was the hard part of the algorithm (since as you say, in syntax you can decide degeneracy)...
The real problem is competing reductions. If you have both the type-based reductions and the regularity rule, then the term Transport(P, a) can reduce in potentially many different ways. It is necessary to ensure that the type-based reductions satisfy the regularity law, then. The problem in cubical type theory was that the type-based reductions do not satisfy the regularity law (actually, most of them do satisfy it, but ones involving the glue type do not). So the difficulty with regularity was to find new versions of these type-based reductions that preserve regularity, and I personally believe this cannot be done without extending the language of cofibrations beyond what appears in the CCHM or ABCFHL papers. (If you add further cofibrations, it is trivial to correct the reductions for CCHM & ABCFHL --- but my ideas in this direction do not seem possible to implement.)
The reason that Arend doesn't seem to have this problem is that Arend doesn't support the other reductions... So in principle it is possible to have a sound type theory that supports the regularity reduction for paths by simply deleting the other reductions that might conflict with it (but I do not want to make a claim about Arend's soundness).


Partitioning the edges of a complete graph into smaller complete graphs

After some search, I have found out that a solution was already published in 1948. De Bruijn and Erdos proved that it is not possible to partition the edges of $K_n$ into fewer than $n$ smaller cliques. I do not have a direct link to their paper, but it is referred to in the 1988 paper by Erdos, Faudree and Ordman, "Clique Partitions and Clique Coverings".


Are deterministic context-free languages closed under outfix (or other erasing operations)

A proof that uses closure properties:

DCF languages are not closed under union, so take,  $L_1, L_2 \in DCF$ s.t. $L = L_1 \cup L_2 \notin DCF$

Add three new symbols $\{\alpha, \beta, \#\}$ to the original alphabet $\Sigma$ and build the languages:

$L'_1 = \{ \alpha \# w \mid w \in L_1\}$
$L'_2 = \{ \beta \# w \mid w \in L_1\}$

We have $L'_1, L'_2$, but also $L' = L'_1 \cup L'_2 \in DCF$ (it is enough to add a starting state that leads to the recognition of $\#L_1$ after reading a leading symbol $\alpha$ or the recognition of $\#L_2$ after reading a leading symbol $\beta$).

Now suppose that $Outf(L') \in DCF$; we know that DCFs are closed under intersection with regular languages, so:

$$Outf(L') \cap \{ \#w \mid w\in \Sigma^*\} =  \{ \#w \mid w\in L_1 \lor w \in L_2 \} \in DCF$$

too.

But given a DPDA for $Outf(L') \cap \{ \#w \mid w\in \Sigma^*\}$ it is immediate to build a DPDA for $\{ w \mid w \in L_1 \lor w \in L_2\} = L$ (just skip the recognition of the first leading symbol $\#$), so $L \in DCF$ contradicting the hypothesis.


What is the largest gap between rank and approximate rank?

First I'll give some background and define approximate rank. A good reference is the recent survey by Lee and Schraibman Lower Bounds on Communication Complexity.

Definition: Let $A$ be a sign matrix. The approximate rank of $A$ with approximation factor $\alpha$, denoted $rank^\alpha(A)$, is
$rank^\alpha(A)=\min_{B:1\leq A[i,j]\cdot B[i,j] \leq \alpha} rank(B)$.
When $\alpha\to \infty$, define
$rank^\alpha(A)=\min_{B:1\leq A[i,j]\cdot B[i,j]} rank(B)$.

A result by Krause says that $R_\epsilon^{pri}(A)\geq \log rank^\alpha(A)$ where $\alpha=1/(1-2\epsilon)$ and $R_\epsilon^{pri}$ is the bounded-error private-coin communication complexity of $A$ with error upper-bounded by $\epsilon$.
The above was for background. Now to answer the question, Paturi and Simon showed that $rank^\infty(A)$ completely characterizes the unbounded-error communication complexity of $A$. They also showed that this agrees with the minimum dimension of an arrangement realizing the boolean function whose communication matrix is $A$. The unbounded-error communication complexity of the equality function is $O(1)$. Keep that in mind.
The communication matrix for equality is just the identity, i.e., a boolean matrix with $2^n$ rows and $2^n$ columns with all ones in the diagonal. Let's denote this by $I_{2^n}$. Alon showed that $rank^2(I_{2^n})=\Omega(n)$ which is tight up to a logarithmic factor (with the theorem by Krause we obtain $R_\epsilon^{pri}(EQ)=\Omega(\log n)$).
The identity matrix has full rank, i.e., $2^n$. Thus, we have exponentially large separations for $\alpha=2$ and $\alpha\to\infty$.


Construction of provably-secure block ciphers are considered in the following papers:

Pseudo-Random Permutation Generators and Cryptographic Composition by Luby & Rackoff. Full version of this paper can be found in How to Construct Pseudorandom Permutations from Pseudorandom Functions.
On the Construction of Pseudo-Random Permutations: Luby-Rackoff Revisited by Naor & Reingold. This is in fact a revised version of the above ideas by Luby & Rackoff. Full version can be found in here.

The construct by Pat Morin and many others are reviewed in Building Secure Block Ciphers on Generic Attacks Assumptions.


Sufficient conditions to guarantee unique fixpoint (not unique least/greatest fixpoint) for monotone functions on complete lattice

Constant functions have unique fixed points. Another criterion that may be applicable is to compare approximations, $\mu_i = \bigcup_{k<i}f^k(\bot)$ and $\nu_i = \bigcap_{k<i}f^k(\top)$, of the least and the greatest fixed points. Trivially, as soon as $\mu_i = \nu_i$ for some $i$, it has been settled that $f$ has a unique fixed point. The problem with this characterization is that, depending on the lattice and $f$, it is incomplete unless you are prepared to explore transfinite approximations.


programming language with type-level functions

Yes, and this is much, much more common than you may have thought. You can do meaningful (and actually Turing-complete!) type-level computation in C++ (see this post by Matt Might for example). Haskell allows type-level partial functions by way of type families, etc.

Of course, the system that fits your description best is probably dependent typing, which unify types and terms, i.e. there is no differentiation between type-level and value-level computation in a dependently-typed language. There are a myriad dependent type systems (Calculus of Constructions, Martin-Lof type theory, Zhaohui Luo's UTT, etc.), and also plenty of dependently-typed programming languages (Coq, Agda, Idris, you name it).

So, I doubt this question is anywhere near research-level. But the answer to your question is, yes, there are such languages, and a lot, and the theory of such languages is already fairly well-researched. For a reference on dependent types, you might want to consult Chapter 2 of Advanced Topics in Types and Programming Languages (ATTAPL), or Software Foundations by Benjamin Pierce et al., and Type-Driven Development with Idris by Edwin Brady if you're more inclined to work with code.


The Stalin compiler brutally optimizes, but how?

The key is probably the fact that it uses whole program analysis and whole program optimisation. The more you know about a how a program behaves, the more you can specialise and inline and make performant.

The MLton compiler for Standard ML does a similar thing (http://mlton.org/). There is one presentation (at least) about it: http://mlton.org/pages/References/attachments/060916-mlton.pdf.

Earlier work was done by Craig Chambers and his group at the University of Washington (for example: http://www.cs.washington.edu/research/projects/cecil/www/pubs/jdean-thesis.html). This was done in the context of Self and later Cecil/Vortex.

There's probably more work in the Scheme/Lisp community. You probably want to consider googling "whole program optimisation".


Is there a constructive parallel repetition theorem for nice MIP protocols?

In his simplified proof of the parallel repetition theorem, Holenstein gives the following explicit bound on the value of the $n$-fold parallel repetition of a game with value $v$:

$$
\left(1-\frac{(1-v)^3}{6000}\right)^{n/\log(|\Sigma_1|\cdot |\Sigma_2|)},
$$
where $\Sigma_1, \Sigma_2$ are the alphabets of the two players.

It's not clear to me that Raz's bound is not constructive in your sense; I am wondering what step in his proof you think is not computable. He does not make his bound fully explicit, but I thought this was done more for exposition.


As far as I understand it, the notion of polymorphic set denotes sets which are primitive, in other words which are first-order objects that can be manipulated, and such that set membership is a predicate, elements can be members of multiple sets. In monomorphic sets, sets are interpreted as predicates on types, and membership of a type is a jugement. In particular, a term can only be a member of a single set (up to equality of types).

While polymorphic sets are the more traditional view, there is an argument that the way mathematicians actually reason is mostly monomorphic e.g. $\mathbb{R}\in 2$ is not a proposition that should make sense. These notes by Martin Löf may clarify matters a bit.


Let $G$ be the host graph and $T$ the tree. Try "growing" $T$ in $G$. At each step, mark in $G$ the subtree $T'$ of $T$ that has been grown so far. Using the bounds on $\delta(G)$ and $\vert V(T)\vert$, argue that we can always expand the marked subgraph if it is not yet isomorphic to $T$.

Oh, but you wanted the Probabilistic Method. Here we go: Toss a coin $k$ times, throw out the results, and then do the above (old joke).


Entropy inequality of joint von Neumann entropy given some marginal inequalities

Why should this be true?

Let the dimensions of $A, B, C, D$ all be the same.

Let $\omega_{AB}$ and $\omega_{CD}$ both be pure states, with
$$S(\omega_A) = S(\omega_B) = S(\omega_C) = S(\omega_D).$$

Now, let $U$ perform a cyclic permutation on $A, B, C, D$.

We have $S(\tau_{AB}) = 2 S(\tau_B)$, and  $S(\omega_{AB}) = 0$, while
$S(\tau_B) = S(\omega_B)$.

Now all you have to do is show that you can perturb this construction slightly to get the desired inequalities in your hypothesis.


A naive approach is as follows. This approach can be used when no better solution is available:

Keep a ternary search tree: Each node (except leaves) has three children: a 0, a 1, and a .. The height of tree is L. Each leaf stores 1 bit: whether the pattern denoted by the path from the root to that leaf exists in your sequence.

A full ternary search tree takes a space of $3^L$. Since L is rather small (L=15), the space will be $3^{15} \approx 14 \ MB$. Since |data|=100,000, and since K << L, it is possible to prune the tree in such a way that it takes much less space.

Now, a backtracking algorithm can search this data structure: Given input x, it starts at the root of the tree, and checks the MSB of x. This bit is either 0 or 1. Assume wlog that the bit is 0. Then, the algorithm omits the 1 child, and takes the 0 and . children. This is continued until we find a match, a mismatch, or when the number of .'s along the path becomes greater than K (assuming the tree is not pruned already).

The above algorithm may take a long time, unless you have pruned the tree properly. That is, if a node does not have a child in the data, mark it as having no child.

Note that since $\binom{15}{7} = 6435$, in the extreme case, up to 6435 patterns in data might match x (which is 6% of |data|; so even the best algorithm has to search this fraction of the database in the worst case).


What advantages does having a null-able string type confer to a programming language?

At the risk of starting a religious war, I will express my opinion that there are no advantages to having nullable types. These should always be replaced by a sum type such as Ocaml option or Haskell Maybe (paired with sane deconcstructors for such types that force the programmer to always consider both possibilities).

The main reason for this is that null pointers, null objects, and the like are responsible for many, many bugs and countless headaches.


Prefix Probability in Stochastic Languages

According to their definition of PFA, to compute $Pr(w\Sigma^*)$ you simply need to compute the probability of having read $w$ after a random path of length $|w|$, which is easy.

Their model of PFA differs from the usual model: usually, for each state $q$ and letter $a$, we have $\sum_{q'} \delta(q,a,q')=1$, so you assume that in a run, the word is fixed beforehand and probabilities are played upon reading each letter.

Here, the setting is different: for each state $q$, we have $F(q)+\sum_{a,q'} \delta(q,a,q')=1$, meaning that a path is chosen at random (including the end), and induces a word. That is what makes the problem easier.


Generating a point in a rational polytope $P \subseteq R^k$ given a point in $P^\epsilon$

From any choice of a polytope $P$ in ${\mathbb R}^k$, $\epsilon$, and a point $q$ in ${\mathbb R}^k$ it is possible to find a polytope $\hat P$ in ${\mathbb R}^{k+1}$, together with an embedding of ${\mathbb R}^k$ into ${\mathbb R}^{k+1}$, such that $\hat P$ is within $\epsilon$ Hausdorff distance of (the embedded image of) $P$ and such that (the embedded image of) $q$ belongs to $\hat P^\epsilon$. To do this, simply make the facets of $\hat P$ be nearly parallel to the embedded image of ${\mathbb R}^k$, so that translating them by $\epsilon$ in ${\mathbb R}^{k+1}$ causes their intersection with ${\mathbb R}^k$ to move away from $\hat P$ by a much greater distance.

Because $q$ was arbitrary, the knowledge of $q$ is of no use in finding a point in or near $P$; everything you could do with it you could do without it. But, because $\hat P$ and $P$ are so close, finding a point near $P$ is equivalent to finding a point near $\hat P$. Therefore, the knowledge of $q$ (a point in $\hat P^\epsilon$) is of no use in finding a point near $\hat P$.


This is not an answer, but the description of a problem which I think the asker wants to ask.

To vaibhav: While I believe that this is at least close to what you want to ask, please edit the question so that it is clearly understandable.  Otherwise, we can only make a guess about what is being asked.

We are given Cx,i, Cy,i, Cz,i ∈ ℕ and Px,i, Py,i, Pz,i > 0 for i=1,2,3 such that Px,1 < Px,2 < Px,3, Py,1 < Py,2 < Py,3, and Pz,1 < Pz,2 < Pz,3.  We are also given K∈ℕ.

The values Cx,i and Px,i describe the content of a stack named x.  From top to bottom, the stack x contains Cx,1 items each of profit Px,1, Cx,2 items each of profit Px,2, and Cx,3 items each of profit Px,3.  The contents of stacks y and z are defined in the same way.

We are allowed to retrieve K items in total from the three stacks.  How can we find efficiently the way to maximize the total profit?


Can Elementary Affine Logic be used as the core type system of a practical programming language?

Something very similar, but using light affine logic (LAL) instead of EAL, was attempted a few years ago by Baillot, Gaboardi and Mogbil (you may find the paper here).  I think their work may be easily generalized to EAL, which is a more liberal system.

As for the features of such language, you have polymorphism natively (EAL is a restriction of second order linear logic). As far as I know, no-one has looked at dependent types, but I don't see why they shouldn't work.  In fact, untyped EAL works just as well as typed EAL, because its normalization properties do not depend on types.

One consequence is that in EAL you may use arbitrary fixpoint of types (see for instance this other paper by Baillot) and define data types in the natural recursive style (like $\mathtt{list\ A := nil\mathrel | A\ *\ list\ A}$), along with the less natural (from a programming perspective) system F definition.  However, by the above remark on untyped normalization, a programming language based on EAL will always be total, which means that you won't have a fixpoint combinator and the use of recursive types is not as natural as you would expect.  For instance, take Scott numerals: without recursive definitions (given by the fixpoint combinator) it is hard to express anything beyond constant-time operations with this representation of integers.  Therefore, you will still need to use Church numerals for iteration (i.e., $\mathtt{for}$ loops), by using which you will incur in the fundamental stratification restriction of light logics (which gives them their complexity properties): you cannot iterate a function $\mathsf{Nat}\rightarrow\mathsf{Nat}$ which has itself been defined by iteration ($\mathsf{Nat}$ here is the type of Church integers).

An example: with some "Church integer hacking", it is possible to define in EAL $\mathsf{dbl}:\mathsf{Nat}\rightarrow\mathsf{Nat}$ such that $\mathsf{dbl}\ \underline{n} = \underline{2n}$ without using iteration.  Then, you may iterate $\mathsf{dbl}$ to define the exponential function $\mathsf{exp}$ which, however, cannot itself be iterated.  So whatever programming language based on EAL will need to have some kind of mechanism forbidding certain definitons by iteration; it s hard to imagine how such restriction would not result in a language which feels awkward to the programmer.  Anyway, no-one forbids you to try and see what you can get!

In any case, if you are interested in the relationship between optimal evaluation, EAL and light logics in general, I suggest you take a look at Coppola's papers from the early to mid-2000s.


An intuitive/informal proof for LP Duality?

Per OP's wish, here's the math.SE answer I link to in my comment above.

Maybe it's worthwhile to talk through where the dual comes from on an example problem.  This will take a while, but hopefully the dual won't seem so mysterious when we're done.

Suppose with have a primal problem as follows.

$$
        Primal =\begin{Bmatrix}
        \max \ \ \ \  5x_1 - 6x_2  \\
        \ \ \  s.t. \ \ \ \ 2x_1 -x_2 = 1\\
        \ \ \ \ \ \ \ \ \ \ \ \ \ \ x_1 +3x_2 \leq9\\
        \ \ \ \ x_1 \geq 0\\
        \end{Bmatrix}
$$

Now, suppose we want to use the primal's constraints as a way to find an upper bound on the optimal value of the primal.  If we multiply the first constraint by $9$, the second constraint by $1$, and add them together, we get $9(2x_1 - x_2) + 1(x_1 +3 x_2)$ for the left-hand side and $9(1) + 1(9)$ for the right-hand side.  Since the first constraint is an equality and the second is an inequality, this implies $$19x_1 - 6x_2 \leq 18.$$
But since $x_1 \geq 0$, it's also true that $5x_1 \leq 19x_1$, and so $$5x_1 - 6x_2 \leq 19x_1 - 6x_2 \leq 18.$$
Therefore, $18$ is an upper-bound on the optimal value of the primal problem.

Surely we can do better than that, though.  Instead of just guessing $9$ and $1$ as the multipliers, let's let them be variables.  Thus we're looking for multipliers $y_1$ and $y_2$ to force $$5x_1 - 6x_2 \leq y_1(2x_1-x_2) + y_2(x_1 + 3x_2) \leq y_1(1) + y_2(9).$$

Now, in order for this pair of inequalities to hold, what has to be true about $y_1$ and $y_2$?  Let's take the two inequalities one at a time.

The first inequality: $5x_1 - 6x_2 \leq y_1(2x_1-x_2) + y_2(x_1 + 3x_2)$

We have to track the coefficients of the $x_1$ and $x_2$ variables separately.  First, we need the total $x_1$ coefficient on the right-hand side to be at least $5$.  Getting exactly $5$ would be great, but since $x_1 \geq 0$, anything larger than $5$ would also satisfy the inequality for $x_1$.  Mathematically speaking, this means that we need $2y_1 + y_2 \geq 5$.

On the other hand, to ensure the inequality for the $x_2$ variable we need the total $x_2$ coefficient on the right-hand side to be exactly $-6$.  Since $x_2$ could be positive, we can't go lower than $-6$, and since $x_2$ could be negative, we can't go higher than $-6$ (as the negative value for $x_2$ would flip the direction of the inequality).  So for the first inequality to work for the $x_2$ variable, we've got to have $-y_1 + 3y_2 = -6$.

The second inequality: $y_1(2x_1-x_2) + y_2(x_1 + 3x_2) \leq y_1(1) + y_2(9)$

Here we have to track the $y_1$ and $y_2$ variables separately.  The $y_1$ variables come from the first constraint, which is an equality constraint.  It doesn't matter if $y_1$ is positive or negative, the equality constraint still holds.  Thus $y_1$ is unrestricted in sign.  However, the $y_2$ variable comes from the second constraint, which is a less-than-or-equal to constraint.  If we were to multiply the second constraint by a negative number that would flip its direction and change it to a greater-than-or-equal constraint.  To keep with our goal of upper-bounding the primal objective, we can't let that happen.  So the $y_2$ variable can't be negative.  Thus we must have $y_2 \geq 0$.

Finally, we want to make the right-hand side of the second inequality as small as possible, as we want the tightest upper-bound possible on the primal objective.  So we want to minimize $y_1 + 9y_2$.

Putting all of these restrictions on $y_1$ and $y_2$ together we find that the problem of using the primal's constraints to find the best upper-bound on the optimal primal objective entails solving the following linear program:

$$\begin{align*}
\text{Minimize }\:\:\:\:\: y_1 + 9y_2& \\
\text{subject to }\:\:\:\:\: 2y_1 + y_2& \geq 5 \\
                   -y_1 + 3y_2& = -6\\
                   y_2 & \geq 0.
\end{align*}$$

And that's the dual.

It's probably worth summarizing the implications of this argument for all possible forms of the primal and dual.  The following table is taken from p. 214 of Introduction to Operations Research, 8th edition, by Hillier and Lieberman.  They refer to this as the SOB method, where SOB stands for Sensible, Odd, or Bizarre, depending on how likely one would find that particular constraint or variable restriction in a maximization or minimization problem.

             Primal Problem                           Dual Problem
             (or Dual Problem)                        (or Primal Problem)

             Maximization                             Minimization

Sensible     <= constraint            paired with     nonnegative variable
Odd          =  constraint            paired with     unconstrained variable
Bizarre      >= constraint            paired with     nonpositive variable

Sensible     nonnegative variable     paired with     >= constraint
Odd          unconstrained variable   paired with     = constraint
Bizarre      nonpositive variable     paired with     <= constraint


Here are a few more details for Suresh and Yoshio's answer. Following e.g. https://en.wikipedia.org/wiki/Semidefinite_programming, an SDP is of the form

$$\begin{array}{rl}
{\displaystyle\min_{X \in \mathbb{S}^n}}
& \langle C, X \rangle_{\mathbb{S}^n} \quad\text{subject to}\\
& \langle A^{(k)}, X \rangle_{\mathbb{S}^n} \leq b_k, \quad (\forall k \in \{1,\ldots,m\}) \\
& X \succeq 0
\end{array}$$
where $\mathbb{S}^n$ is the space of all $n\times n$ real symmetric matrices, $\langle C, X \rangle_{\mathbb{S}^n} = \sum_{ij} C_{ij} X_{ij}$, and $X \succeq 0$ constrains $X$ to be positive semi-definite.
The latter constraint is equivalent to (sometimes by definition)
$$y^T X y \ge 0~~~(\forall y\in \mathbb{R}^n).$$
(See e.g. here.)
Hence, the SDP is equivalent to
$$\begin{array}{rr@{}ll}
{\displaystyle\min_{X \in \mathbb{R}^{n\times n}}}
& \sum_{ij} C_{ij} X_{ij}  &\text{subject to}\\
& \sum_{ij} A^{(k)}_{ij} X_{ij} &\leq b_k,
& (\forall k \in \{1,\ldots,m\}) \\
& \sum_{ij} y_i y_j X_{ij} &\ge 0
& (\forall y\in \mathbb{R}^n)\\
& X_{ij} &= X_{ji} & (\forall i,j\in\{1,\ldots,n\}).
\end{array}$$

So, we can think of the SDP as minimizing (or maximizing) a linear function of the vector $X$ subject to (infinitely many) linear constraints on $X$.  Hence, it is an optimization problem with a convex feasible region and a linear objective.  So any local optimum is a global optimum.


A natural $\text{NEXP}^{\text{NP}}$-complete problem is deciding a sentence of Presburger arithmetic with an $\exists^*\forall^*\exists^*$-quantifier prefix (as shown here). Further complete problems related to database theory have been studied here.


Is it NP-hard to _play_ minesweeper perfectly?

Just an extended comment; in

Allan Scott, Ulrike Stege, Iris van Rooij, Minesweeper May Not Be NP-Complete but Is Hard Nonetheless

the authors face the problem I mentioned in my comment above.

From the abstract:

In volume 22 of The Mathematical Intelligencer, Richard
Kaye published an article entitled "Minesweeper is NP-Complete."
We point out an oversight in Kaye's analysis
of this well-known game. As a consequence, his
NP-completeness proof does not prove the game to be hard.
We present here an improved model of the game,
which we use to show that the game is indeed a hard problem;
in fact, we show that it is co-NP-complete.
....In this article, we investigate the complexity of the
deterministic part of playing Minesweeper. In our
analysis, we assume that the player is given a
consistent Minesweeper board configuration.
That is, when completely revealed,
the board presented has in each square either
a mine or a numeber corresponding to the correct number
of neighboring mines.
Further, we assume an ideal player who makes no
mistakes in reasoning. Note that these assumptions imply
that the player can only lose (try to open a square containing a mine) when forced
to guess. Therefore, our optimal player who follows
the strategy described previously will avoid guessing whenever possible.
However, to do so he must be able to decide
whether it is possible to make progress on the board
without guessing. This problem is what we call the
Minesweeper Inference problem.
...

There is also a recent paper on arXiv that seems relevant (I just found it now):

Michiel de Bondt, The computational complexity of Minesweeper

Abstract: We show that the Minesweeper game is PP-hard, when the object is to locate all mines with the highest probability. When the probability of locating all mines may be infinitesimal, the Minesweeper game is even PSPACE-complete. In our construction, the player can reveal a boolean circuit in polynomial time, after guessing an initial square with no surrounding mines, a guess that has 99 percent probability of success. Subsequently, the mines must be located with a maximum probability of success.
Furthermore, we show that determining the solvability of a partially uncovered Minesweeper board is NP-complete with hexagonal and triangular grids as well as a square grid, extending a similar result for square grids only by R. Kaye. Actually finding the mines with a maximum probability of success is again PP-hard or PSPACE-complete respectively.
Our constructions are in such a way that the number of mines can be computed in polynomial time and hence a possible mine counter does not provide additional information. The results are obtained by replacing the dyadic gates in [3] by two primitives which makes life more easy in this context.


A good old trick is that it's sufficient to give an algorithm that achieves this with $O(\log n)$ expected number of coin flips and $99\%$ probability, as if we are exceeding the expected running time a lot, we can just output anything, using Markov's inequality this won't ruin our error much. And this we can do as follows.

Always keep an active interval that is supposed to contain an approximately unbiased coin (but might not). Then repeat the following.

1, Halve the size of the active interval by flipping its middle coin a couple of times. Update the active interval (if the middle coin showed no bias, then arbitrarily).

2, Flip both ends of the active interval a couple of times to check that we made no errors. If an error is detected, then go back to the previous active interval.

This way, with a constant number of coin tosses we halve the size of our active interval with high probability and double it with small probability. Thus, in $O(\log n)$ expected time, we reach size $1$, which means one coin. We can check this coin with $\log n$ further coin tosses (though I'm not sure if this is necessary).