When we are using Random Oracle Model There are protocols which make use of invoking an oracle or submitting queries to an oracle and getting response from that. There are many examples in which oracles are used to define security, like IND-CCA security and there are many examples of using the term oracle to just a procedure accepting input and providing some output, independent of the input, like non-information oracles of Canetti (you can refer to my previous question to read more about non-information oracles). My question is about the Random Oracle, that is an oracle with random output.

  When can we determine that we are using the random oracle model? For example, when we use the random output of a hash function, definitely we are in the random oracle model, but if we use one way property of hash function we are not using random oracle model. Can you provide more examples on this?

Let me clarify my ambiguity through an example. In this article the authors use a new oracle which is relatively unknown called linear oracle bilinear Diffie-Hellman (or in short LO-BDH) and security of their approach lies in the hardness of this assumption. How can I determine that using this assumption, we are not using the random oracle model (the authors claim that they are not in the random oracle). Here is another source of ambiguity:

  They are using commitments over UC framework which are impossible in the plain model thus they are at least using common reference string (CRS) model. How can I make sure that if I use such an oracle (LO-BDH) in the security proof of another protocol, I am still in the plain model or using it does not cause undesired shifting of models?

Edit: I found interesting material on RO methodology in the book Introduction to modern cryptography by Katz and Lindell. the rest is from the mentioned book.

  When defining pseudorandom functions, the authors have considered algorithms having oracle access to a random function. But usage of a random function there is very different from the usage of a random function in the RO methodology. In the pseudorandom functions, a random function is used as a way of defining what it means for a concrete keyed function to be pseudorandom. In the random oracle model, the random function is used as part of the construction of the primitive, so must somehow be instantiated in the real world if we want a concrete realization of the primitive.

BTW, the authors have noted that a random oracle is not a one way function because random oracle is not a fixed function, but in order to implement it in a real world, it must first be instantiated and description of it must be fixed. So a hash function is fixed before executing the protocol.

Let us first step back and say more precisely (mathematically) what "the Random Oracle Model (ROM)" is, because it is fundamentally different from an "assumption" as they are thought of in cryptography.

One way to formalize the ROM is to see it as alternative model of computation.  In particular, algorithms in this model of computation have a extra distinguished state (or subroutine, or circuit gate, whatever), that computes some function $H:\{0,1\}^\ast\to\{0,1\}^n$, where n is the security parameter.  An algorithm A is executed in this model by picking $H$ at random from all possible functions, and then running $A$ with its $H$ subroutine set to compute that function.

When we "analyze a protocol in the ROM", we mean first define the protocol via algorithms that have access to $H$, and then we prove a theorem about the protocol when it is attacked by adversaries that also have access to $H$.  The theorem will say that something happens with high probability, where the probability is over the choice of $H$, amongst other things.

This model of computation is not realistic, however, because we do not all have access to a truly random function.  So instead we take our algorithms (which were defined in the ROM) and set $H$ to something efficiently computable, like SHA-256.  Of course, the theorem does not actually cover such usage, but this approach is remarkably effective for avoiding wide classes of attacks against protocols.  We just hope ("assume") that things will work out for the protocols under consideration, but in general this assumption is false[1].

A cryptographic assumption, on the other hand, say something about the limitations of the "standard model of computation", i.e. Turing machines, circuit families, etc.  A distinguishing feature here is that assumptions might true, but the ROM will never "true".  This holds even for interactive assumptions that involve weird oracles - even a random oracle.

Things brings us to the point of confusion:  When you're sitting down to design a protocol (algorithm) and prove it secure in the standard model under an assumption, you can't assume that your algorithm has access to any oracles, because it needs to be an algorithm in the usual sense.  Even if your assumption has a random oracles represented somewhere in it, you still need to give a well-defined algorithm or protocol.

[1] See "The random oracle methodology, revisited" by Ran Canetti, Oded Goldreich and Shai Halevi.


What is known about the hardness of the chromatic index for restricted graph classes? There is a nice paper from 1991 that contains three diagrams about different graphclass-families showing what is known about the hardness of determining the chromatic index for them.
Are there any news since then on these?

I'm most interested in what is known about graphs with a bounded chromatic number.
My curiosity has been raised by https://mathoverflow.net/questions/238448/hypergraph-edge-colouring.

Here's one very relevant looking result:

Koreas, Diamantis P. (1997), "The NP-completeness of chromatic index in triangle free graphs with maximum vertex of degree 3", Appl. Math. Comput. 83 (1): 13–17.

The title is self-explanatory.


Problems still "hard" in the SMP/Referee model with shared randomness? In the referee (SMP: Simultaneous Message Passing) model introduced by Yao (see e.g. [1]), Alice and Bob have respectively inputs $x\in X$ and $y\in Y$, and wish to communicate with a third-party, the Referee, to compute $f(x,y)$ where $f\colon X\times Y\to\{0,1\}$ is a function known to the three parties.

The restriction, however, is that the communication is one-way: Alice and Bob can only send a message to the referee, who then must output the answer ($A\leadsto R$ and $B\leadsto R$). (This differs from the one-way CC setting as the referee does not hold any input.)

While the deterministic communication complexity in this model seems well-understood, and lower bounds (tight for $\sf EQ_n$) for the private-coin setting are known [1], I could not find examples of cases (preferably for promise problems, i.e. with a gap between $\sf yes$ and $\sf no$-instances) for which there was a strong separation between one-way public-coin communication complexity and SMP public-coin communication complexity.

  What are problems $\Pi$ for which there is a gap between $\operatorname{ow-CC}_{\rm pub}(\Pi)$ and $\operatorname{smp-CC}_{\rm pub}(\Pi)$?

For instance, ${\sf EQ}_n$ is $\Theta(\sqrt{n})$ for SMP private-coin, and $O(\log {n})$ for one-way private-coin; but in the public-coin setting, it is $O(1)$ for both. On the other end of the spectrum, ${\sf DISJ}_n$ is $\Theta({n})$ for both models, and so is ${\sf GAPHAMMING}_n$.

(As a side note, one can derive a separation between one-way "imperfectly-shared"-coin communication complexity and SMP "imperfectly-shared"-coin communication from the work of Bavarian et al. [2] on communication with correlated random bits, from their ${\sf GAPIP}_n$ problem, but this separation does not hold for perfectly shared randomness (public coins)).

[1] Randomized simultaneous messages: solution of a problem of Yao in communication complexity, L. Babai. 1997.
http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=612319&tag=1

[2] On the Role of Shared Randomness in Simultaneous Communication, M. Bavarian, D. Gavinsky, T. Ito, 2014.
http://arxiv.org/abs/1508.06395

If A has a pointer (of length $\log n$) to a bit of B (whose input has length $n$), that requires, $\Theta(\log n)$ one-way communication, even with a public-coin. On the other hand, the referee needs $\Theta(n)$ bits to solve the problem, even with a public-coin. Or did I misunderstand something?


How to be more "theory-minded"? Apologies in advance for this a soft question which has no closed, correct answer. This is probably the best forum to ask my question.

I am a third year graduate student in theory group of a top-15 school in US. So far, I've been doing decently well. I have a first author theory paper and a first author practical paper so far. My advisor has been superb in helping me honing my skills but I feel stuck (and helpless).

So far, my advisor has been a helping hand and a guiding force to always point me right directions and pose the right questions (not too abstract, not too concrete) which have been instrumental in me finding the answers to research problem. As I try to be more "independent", i.e, ask the right questions and prove results, I feel I have failed miserably and quickly feel overwhelmed. I feel that I don't have the maturity of a theory PhD student yet where I can ask myself the right questions and come with answers. In other words, given the right definitions and some hand holding, I am able to do things but otherwise, it becomes very hard. My sloppiness when it comes to writing proofs doesn't help either.

I am looking for advice on how can I sharpen my skills and be more "theory-minded" where I can grasp things quicker and require less hand holding. While one answer is simply to keep working and hope that experience makes me wiser, I am not sure how this will work out. The only solution I have is to actually go through come recent papers in my area and write down proofs by hand in as much detail as possible to help me nail proof writing skills and build intuition.

Any advice would be extremely helpful. Please let me know if question is unclear or needs more detail.

One way I have often found theory problems to work on is by reading about an area and trying to figure out exactly what the state of the art is on a problem.  Invariably, some basic questions end up being left unanswered, and that’s where I will start my research. Such questions are sometimes left unanswered not because they are too difficult, but because nobody formalized things properly, and this is something that can come naturally to a theorist who is just trying to understand what’s known and what’s not. And the ability to formalize problems is a key aspect of doing successful theory.

Another natural way to do successful theory is by trying to solve known open problems, for example those found in the discussion sections of recent papers.  There, the key is having a good enough understanding of your own strengths and interests that you choose problems where you might make progress.  This takes some experience and also some self-awareness, which you can actively think about and cultivate as you go through your PhD.

And as you do your PhD, you’ll develop these skills and more, including the ability to grasp proofs in papers quicker, and if things go well, you’ll be coming up with your own directions naturally by the end.


Implementing "Internal" Languages One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured category.

For instance, Synthetic Differential Geometry has models in topoi that contain and embedding of the category of smooth manifolds, so you can use higher-order logic to construct smooth functions and solve differential equations.

As another example, in this paper, they notice that "step-indexing" is really just working with presheaves over the naturals (another topos), so you can use the syntax of higher order logic to define step-indexed logical relations without the tedious manipulation of steps.

Finally, Andrej Bauer shows in this MO question that you can do a lot with the "internal language" of the topos of graphs.

My question is, has anyone realized this vision literally in a theorem prover?
For instance, if I show that a category I care about is Cartesian Closed, I could then move to "internal mode" where I write lambda-calculus syntax (with some model-specific axioms) and then can move back to "external mode" and manipulate them as objects in my model?

In the extreme I would even want topos theory and higher-order logic, so I could write my step-indexed logical relations without steps, or teach classical mechanics with a theorem prover using SDG. This seems to me to be a very powerful idea as someone could implement extensional dependent type theory once and provide nice tooling and then use it with wildly different applications as described above.

In Extending Type Theory with Forcing by  Guilhem Jaber, Nicolas Tabareau and Matthieu Sozeau, 2012, intuitionistic forcing is presented as an internalization of the presheaf construction, implemented as a type-preserving translation in the style of Bernardy and Lasson's parametricity translation.

This means that you can define terms in your usual type theory, and then "translate them" into a "forcing layer" where they are interpreted as translations at a different translation type. For example, the translation induced by indexing over decreasing natural numbers lets you use your usual terms in a post-translation theory where a later modality is definable. This sounds rather close to your idea of working internally in the topos of trees.

It seems that they have a new, simpler Coq plugin implementing these ideas at CoqHott/coq-forcing, and in particular SI.v builds this forcing translation for step-indexing. Unfortunately, while it does the work of building the model, there is no example of using it for step-indexed definitions in practice (the only thing translated instead of defined in the forcing layer is Forcing Translate eq, which isn't terribly informative). You could try to experiment to see how (in)convenient this is to use.


Arithmetic coding, the termination symbol, and the empty string Suppose the source alphabet is $a, b, c$ with $a$ as the termination symbol and so the unit interval is correspondingly divided as
$[0, P(a), P(a)+P(b), 1]$.

Strings consisting of a bunch of $b$'s and $c$'s ending with an $a$ (the termination symbol) are valid for encoding. Strings with an $a$ in middle are considered invalid for encoding.

So its easy to construct strings with encodings lying in the interval $[P(a), 1)$. But does arithmetic coding assign any string an encoding in the interval $[0, P(a))$? Would the empty string qualify as being encoded to a bitstring lying in $[0, P(a))$? Since the empty string can be thought of as the string "$a$" or as just the termination symbol.

Since devoting space to encoding the empty string would seem pointless why not have the first division of the unit interval be
$[0, (P(b)-P(a))/(1-P(a)), 1]$ which corresponds to mapping $[P(a), P(a)+P(b), 1]$ to fill up the unit interval. Then subsequent refining divisions would use $[0, P(a), P(a)+P(b), 1]$ as usual.

Why shouldn't you be able to send the empty string? Shouldn't it be considered a valid message?

But if you don't allow the empty string as a message, then your modified protocol will work fine, and will save you on average a small fraction of a bit per message.

Is this tweak worth putting into your implementation so as to improve the performance? Let's work out how much it saves you. Suppose you're using a binary alphabet, and your average message is around 100 bits in length. You then want the termination symbol to have probability 1/100. By not allowing the possibility of the termination symbol being the first bit, you save on the order of 1/100 bits* per message. If you assume a compression ratio of 2, the total improvement in performance is 0.02%. Since 100 bits is a smaller average message length than I expect you would see anywhere, the actual performance improvement would probably be even smaller. I thus suspect that this variant would not actually be used in practice.

* 1/100 nats, or 0.014 bits, to be more precise.


How to find a specific research topic to concentrate on? I recently started my masters course. Last semester I took courses from different disciplines like networks, software engineering, architecture, etc. Recently, after taking an advanced course in algorithms and data structures I think I found a course which interests me most (including other similar topics likes programming languages, etc).

How do I find a research topic - specific data structure or algorithm I can work on for my thesis, and possibly follow up into a PhD? I am currently looking at some of the research done at my university in the same disciplines.

edit

I think some people confused the Question due to ambiguous framing from my side.
I want to find a topic for my masters thesis, I am still somewhat far awaw from starting a PhD(If I do)

Let me offer a slight variant of @Shir's answer.  For your first problem, it really doesn't matter what you work on.  Just pick a random problem out of the air and start working on it.  Do not worry about "finding a thesis".  Do not worry about "finding an advisor".  However, you may find more problems floating in the air near active researchers—both faculty and students—than, say, in your apartment or at the library.  And you may find that people are more willing to help you solve your problem (and polish the solution for publication) if it's a problem they care about.  Talk to everyone.  Listen to everyone.  Read everything.  Then pick your own problem.

Once you've solved your first problem, start over.  Pick a different problem, and talk to different people.  Meanwhile, write up your first solution, and give talks about it, if only to a faculty member or another student or your cat.  Listen to their feedback.  (Meow.)  Practice, practice, practice.  (Don't forget to ace your classes and your qualifying exams.  If necessary, find a faculty member to sign your paperwork.)

Once you have experience solving individual problems, then you can start developing a larger research program (aka a thesis direction).  [This is probably about the point where you finish your MS thesis and start as a PhD student.]  With a two-point sample of problem space, you have a better view of your own talents and interests.  With a multiple-point sample of potential-collaborator-space, you have some idea of what kind of researchers (in particular, what kind of advisor) you work well with.  Having feedback from multiple audiences, you'll have some clue about what problems other people and/or cats care about, and what kind of intuition you're best at conveying.  All that information will help you make more informed decisions about what to work on in the future.

But for your first problem, it really doesn't matter.  Just pick something you're interested in and start working.


Does distance-2 coloring fit in Telle and Proskurowski 's algorithm for partial-k trees? This question is on "Vertex Partitioning Problems" framework of Telle and Proskurowski.
For solving problems in parital $k$-trees (i.e., graphs of bounded treewidth), the "Vertex Partitioning Problems" framework of Telle and Proskurowski looks promising. This framework gives practical algorithms for some problems (as opposed to MSO). Given a graph $G$ and a $q\times q$ matrix $D$ each entry of which is a subset of $\{0,1,2,\dots\}$, the question "Does there exist a partition $V_1, V_2, \dots ,V_q$ of $V(G)$ such that $\forall x \in V_i,\; |N(x) \cap V_j| \in D(i,j)$" is a vertex partitioning problem.
Their paper (Algorithms for vertex partitioning problems on partial k-trees) claim that every vertex partitioning problem is solvable in time polynomial for partial $k$-trees (time complexity is like $\mathcal{O}(nq^{2(k+1)})$
My doubt is regarding the "cofinite" condition they use. Is this important? Doesn't that mean this method doesn't work (out of box) for distance-2 coloring, since for distance-2 coloring the matrix $D$ must consist of entries $\{0\}$ along (main) diagonal and entries $\{0,1\}$ for off-diagonal.
Note: They explicitly state that the method works for coloring. For coloring also, diagonal entries are same; May be main diagonal is a special case?
Thank you.

distance-2 coloring is coloring in the square (d(x,y) <= 2 implies xy an edge in the square). If a graph has tw k, its square has bounded clique-width (see Gurski-Wanke and Suchan-Todinca). See Oum et al. for algorithms as in Proskurowski-Telle for graphs of bounded clique-width.


Complexity for single-linkage clustering with max norm Let $S\in\mathbb Z^d$ be a set of points, with some notion of distance $d(x,y)$ between two points $x,y\in S$. I am specifically interested in the max distance, that is $d(x,y)=\max_{1\le i\le d} |x_i-y_i|$ where $x=(x_1,\dotsc,x_d)$ and $y=(y_1,\dotsc,y_d)$.

Single-linkage clustering consists in computing a tree $T$ on the set $S$ of minimal distances, that can be defined by the following algorithm that computes the set $E$ of edges of $T$ as follows:

Set $E=\emptyset$ [each point is a cluster]
While $|E|<|S|-1$, add to $E$ a pair $(x,y)$ such that

$x$ and $y$ are in distinct connected components of $T$;
$d(x,y) = min_{u,v} d(u,v)$ where the minimum is taken over all pairs of points $u$, $v$  that are in distinct connected components of $T$.

If one first computes all the distances between pairs of points in $S$ and sort them, the above algorithms allows to compute the tree $T$ in time $\tilde O(n^2)$ if one assumes that the distance can be computed in time $O(1)$. Here the notation $\tilde O(\cdot)$ hides poly-logarithmic factors.

  What is the complexity of computing this tree, when the distance is the max distance?

  If $d=2$, is there a quasi-linear algorithm (that is in time $\tilde O(n)$)?
  More generally, if $d$ is fixed, is there a quasi-linear algorithm?
  Or is there a quadratic lower bound (in some reasonable model)?

Note: I asked a similar question some days ago on cs.sx. I had no answer, so I re-post it here with a new (and I guess better) formulation.

Single-linkage clustering gives the same connections in the same order that you would find using Kruskal's algorithm for the minimum spanning tree, and the clustering can be found by finding a minimum spanning tree and then running Kruskal's algorithm on the resulting $(n-1)$-edge graph. Therefore, the time is bounded by the MST construction + the time to sort the edges of the MST.

The two-dimensional $L^\infty$ MST can be constructed in $O(n\log n)$ time using rectilinear Voronoi diagrams, and an $O(n\log n)$ algorithm for the three-dimensional version is given by

Krznaric, Drago; Levcopoulos, Christos; Nilsson, Bengt J. (1999),
Minimum spanning trees in $d$ dimensions,
Nordic J. Comput. 6 (4): 446–461.

more generally an algorithm that is within a polylog factor of linear for any fixed dimension is given by

Gabow, Harold N.; Bentley, Jon Louis; Tarjan, Robert E. (1984), Scaling and related techniques for geometry problems, Proc. 16th ACM STOC, pp. 135–143, doi:10.1145/800057.808675


Shouldn't relativisation contain consistency proof ? My question may be stupid, but let's take the Baker-Gill-Soloway theorem as an example :

There exists an oracle A such as $P^A = NP^A$ and an oracle B such as $P^B \neq NP^B$.

If we take both oracles A and B, I suppose we have $P^{A,B} = NP^{A,B}$ and $P^{A,B} \neq NP^{A,B}$, and then, theory wouldn't be consistent.

What says us that the theory with only oracle A is consistent ? If such theory isn't consistent, then there could be non-relativizing proofs of $P \neq NP$.

Whether or not $P^{A,B}$ equals $NP^{A,B}$ is going on the particular oracle languages A and B that you are using.  Iirc, in the BGS paper the language A is TQBF (or any other PSPACE-complete language).  The language B, somewhat ironically, is actually defined via a diagonalization construction.  Now, if you use the construction from the paper and apply it to TMs with an A oracle, then the resulting language B will be such that $P^{A,B} \ne NP^{A,B}$.  On the other hand, if you stick with the original language B from the paper, it will depend on the details of B's construction.  If B is in PSPACE (I don't know offhand if it is or not), then a TM with an A oracle could simulate any queries to B, and you should have $P^{A,B} = NP^{A,B}$.

The bottom line, though, is that this has nothing to do with consistency--it is just a technical question about the specific oracle languages A and B (and you could get different answers depending on the particular choices of A and B that you use).


Algorithm to compute distance between powers Given coprime $a, b$, can you quickly compute $$ \min_{x, y > 0} |a^x - b^y| $$

Here $x, y$ are integers. Obviously taking $x = y = 0$ gives an uninteresting answer; in general how close can these powers get? Also, how do we quickly compute the minimizing $x, y$?

First I thought it would be best to use the continued fraction of $\log(a)/\log(b)$ and test at its convergents, because at that convergents there are points $(x,y)$ of in some sense optimal approximation. After that it becomes clear, that one needs to use at least the generalized continued fractions to make sure to have monotonic decreasing distances.
After that and the complicated algorithm with this the following brute-force algo was even faster in Pari/GP

\\ print X,Y,d conditional X>lowboundX, Y > lowboundY, d<upperboundD
{pri1(lbX,lbY,ubd,a,b,X,Y,d)=if(X<lbX || Y<lbY || abs(d)>ubd,return(0));
                  print(a,"^",X,"-",b,"^",Y,"=",d)); }

{mylist(maxa=19,maxb=99,lbX=3,lbY=2,ubd=100)=print(" ");
for(a=2,maxa,for(b=a+1,maxb,
     if(gcd(a,b)>1,next()); \\ ignore trivial multiples
     X=1;Y=1;Xa=a;Yb=b;
     d=Xa-Yb;  pri1(lbX,lbY,ubd,a,b,X,Y,d);
     for(k=1,20,
        while(d<0,Xa*=a;d=Xa-Yb;X++;pri1(lbX,lbY,ubd,a,b,X,Y,d););
        while(d>0,Nb*=b;d=Xa-Yb;Y++;pri1(lbX,lbY,ubd,a,b,X,Y,d););
        if(X>30 || Y>20, break());  \\ stop at max X=30 or Y=20
       );
   )); }

after that call mylist(100,1000,3,3,100) to find all small difference with $|d| \lt 100$ where both exponents are at least $3$ for all bases $a=2..100$ and $b=(a+1) .. 1000$ . Check only up to $\max (X)=30$ and $\max(y)=20$.

This was much faster than the continued-fraction approach (which also had more unkind issues (for instance with completeness of the solutions) which are difficult to handle) although it is a somehow naive algo ...

A protocol (manually ordered) :

gettime();mylist(200,10 000,3,3,100);gettime() /1000.0 \\ ~ a*b/6000 sec
  (400 sec)

 2^8- 3^5= 13

 6^7-23^4= 95
 2^7- 3^4= 47

 2^7- 5^3=  3
 2^5- 3^3=  5
 3^4- 4^3= 17

---------------
 2^6- 3^4=-17

 3^5- 4^4=-13
 2^5- 3^4=-49

 2^8- 7^3=-87
(4^4- 7^3=-87)

 3^7-13^3=-10
 2^6- 5^3=-61
(4^3- 5^3=-61)
 2^5- 5^3=-93

 2^4- 3^3=-11
 3^4- 5^3=-44
 6^4-11^3=-35
15^4-37^3=-28

 3^3- 4^3=-37
 3^3- 5^3=-98
 5^3- 6^3=-91


Is there a relativized form of Rice Theorem? Suppose $P_1$ and $P_2$ are nontrivial semantic properties of Turing Machines, and suppose that $P_1\wedge P_2$ is nontrivial given $P_1$.  Can one claim that $P_1\wedge P_2$ is undecidable given an oracle for $P_1$?

A specific example: Let $P_2$ be a nontrivial property of total functions.  Is it undecidable when inputs are restricted to machines which are known to compute total functions?

The usual proof of Rice Theorem, via reduction from the Halting Problem, does not seem to work in this case.

You can prove your idea via the usual recursion theorem proof of Rice's theorem.

proof:

Suppose that $M_{yes}$ is a machine with both property $P_1$ and $P_2$ and that $M_{no}$ is a machine with property $P_1$ but without property $P_2$. Such machines must exist by the nontrivial assumption.

Then suppose there exists a decider $D$ which accepts any input $<X>$ such that machine $X$ satisfies both property $P_1$ and $P_2$, rejects any input $<X>$ such that machine $X$ satisfies property $P_1$ but not $P_2$, and has any behavior on all other inputs.

Consider the following machine:

$M =$ on input $w$:

Obtain the description $<M>$ via the recursion theorem.
Run $D$ on $<M>$
If $D$ accepts $<M>$, simulate $M_{no}$ on $w$ and output the same answer
If $D$ rejects $<M>$, simulate $M_{yes}$ on $w$ and output the same answer

This language $L(M)$ of this machine is either $L(M_{yes})$ or $L(M_{no})$ depending on whether $D$ rejects or accepts $<M>$. Notice that since $P_1$ is a semantic property shared by both $M_{yes}$ and $M_{no}$, we know that in either case, $M$ has property $P_1$. Then by definition of $D$, $D$ accepts $<M>$ if and only if $M$ has property $P_2$. Thus, we have that $L(M) = L(M_{no})$ if $M$ has property $P_2$ (i.e., $D$ accepts $<M>$) and $L(M) = L(M_{yes})$ if $M$ does not have property $P_2$ (i.e., $D$ rejects $<M>$). This, however, contradicts the fact that $M_{yes}$ has property $P_2$, $M_{no}$ does not have property $P_2$, and $P_2$ is semantic.

By contradiction, we can conclude that decider $D$ as described cannot exist. In other words, $P_2$ given $P_1$ is undecidable.


Constraint satisfaction problem (CSP) vs. satisfiability modulo theory (SMT); with a coda on constraint programming Does someone dare to attempt to clarify what's the relation of these fields of study or perhaps even give a more concrete answer at the level of problems? Like which includes which assuming some widely accepted formulations. If I got this correctly, when you go from SAT to SMT you're basically entering the field of CSP; vice-versa, if you limit CSP to booleans you're basically talking of SAT and maybe a few related problems like #SAT. I think this much is clear (e.g. cf Kolaitis and Vardi's chapter "A Logical Approach to Constraint Satisfaction" in Finite Model Theory and Its Applications by Grädel et al.), but what's less clear to me is when are the constraints "modulo a theory" and when aren't they? Does SMT always imply the theory uses only equality and inequality constraints are always in the broader field of CSP? As far as I can tell, you can often introduce slack variables, so the distinction [if it exists] is less than obvious.

The relatively recent "Satisfiability handbook" (IOP Press 2009) gathers both SMT and CSP problems under its broad "satisfiability" umbrella, but given the way it is structured (chapters written by various authors) doesn't really help me with figuring out this.

I would hope the terminology gets less confusing when you talk of constraint programming, which (by analogy with the term ''mathematical programming'') I hope involves minimizing/maximizing some objective function. The Wikipedia article on constraint programming is alas so vague that I can't really say if this framing happens though. What I can gather from Essentials of Constraint Programming by
Frühwirth and Abdennadher (p. 56)  is that a "constraint solver" usually provides more than just a satisfiability checker, with simplification etc. being important in practice.

Although this is hardly an actual CS-theory research question, I don't expect good answers to this one on the undergraduate CS.SE site given what I saw at https://cs.stackexchange.com/questions/14946/distinguish-decision-procedure-vs-smt-solver-vs-theorem-prover-vs-constraint-sol (which contains a lot of words but not what I would consider a real answer, alas).

SAT, CP, SMT, (much of) ASP all deal with the same set of combinatorial optimisation problems.
However, they come at these problems from different angles and with different toolboxes.
These differences are largely in how each approach structures information about the exploration of the search space.
My working analogy is that SAT is machine code, while the others are higher level languages.

Based on my thesis work on the structural theory of CSPs, I have come to believe that the notion of "clause structure" is essential in unifying all these paradigms and in understanding how they differ.
Each clause of a SAT instance represents a forbidden partial assignment; a clause like $x_1 \lor \overline{x_2} \lor x_3$ forbids the partial assignment $\{(x_1,0),(x_2,1),(x_3,0)\}$ that simultaneously sets $x_1$ and $x_3$ to false and $x_2$ to true.
The clause structure of a combinatorial optimisation problem is its representation as a SAT instance, using some suitable encoding.
However, the clause structure includes all the forbidden partial assignments, not just the ones given at the start.
The clause structure is therefore usually too large to manipulate directly: typically it has at least exponential size in the number of variables, and may be infinite.
Hence, the clause structure has to be approximated with a limited amount of space.
SAT/CP/SMT/ASP maintain and update a more-or-less implicit representation of an underlying clause structure.
This is possible because if one partial assignment is known to be in the clause structure, then this implies that many other clauses are also present.
For instance, the SAT clause above also forbids any partial assignment that contains it as a subset, so clauses like $x_1 \lor \overline{x_2} \lor x_3 \lor x_4$ and $x_1 \lor \overline{x_2} \lor x_3 \lor \overline{x_4} \lor x_5$ are all in the clause structure of that instance.

An approximation of the clause structure is kept to narrow down the set of solutions, and to help determine whether this set is empty.
During search some partial assignments may turn out not to be contained in any solution (even if they individually satisfy each of the constraints in the instance).
These are known as nogoods, a term introduced by  ("Mr GNU") Stallman and Sussman.
A nogood clause is therefore in the clause structure and can be included in an approximation of the clause structure, as a compact representation of many clauses that can be pruned from the search for solutions.
Adding nogoods to the approximate clause structure retains all the solutions, but better approximates those solutions.
So the approximate clause structure usually changes as search progresses.
Further, the way the problem is modelled in one of the combinatorial optimisation approaches affects the clause structure, often quite significantly.
For instance, propositional variables can represent intervals such as $x \le 5$ or points such as $x = 5$.
Hence there isn't a single general clause structure but one associated with each choice of representation, depending on what the singletons (literals) of the clause structure represent.

Constraint programming (CP) was traditionally an AI discipline, with a focus on scheduling, timetabling, and combinatorial problems, and therefore has a central role for variables that can take more than just two values (but usually only finitely many).
CP has emphasised efficient search and, motivated by the traditional applications, has given a central role to the all-different (injectivity) constraint, but has also developed efficient propagators for many other kinds of constraints.
The formal definitions of CP have been around since at least Montanari's 1974 paper Networks of constraints, with precursors going back even earlier.
This weight of history may have contributed to CP lagging behind other approaches in raw performance over the last decade.
CP classically maintains an approximation of the complement of the clause structure, via a set of active domains for the variables.
The aim is to eliminate values from the active domains, exploring the clause structure by trying to assign candidate values to variables and backtracking when necessary.

Satisfiability modulo theories (SMT) came out of the verification community.
Each theory in an SMT solver forms an implicit representation of potentially infinitely many SAT clauses.
The theories used with SMT and the constraints used in CP reflect their different historical applications.
Most of the theories SMT considers have to do with integer-indexed arrays, real closed fields, linear orders, and suchlike; these arise from static analysis of programs (in computer aided verification) or when formalising mathematical proofs (in automated reasoning).
In contrast, in timetabling and scheduling the injectivity constraint is central, and although the standard SMTLIB language has had an injectivity constraint since its inception in 2003 (via the distinct symbol), until 2010 SMT solvers only implemented distinct via a naive algorithm.
At that stage the matching technique from the standard CP propagator for all-different was ported across, to great effect when applied to large lists of variables; see An Alldifferent constraint solver in SMT by Banković and Marić, SMT 2010.
Moreover, most CP propagators are designed for problems with finite domains, whereas standard SMT theories deal with infinite domains (integers, and more recently reals) out of the box.
SMT uses a SAT instance as the approximation of the clause structure, extracting nogood clauses from the theories as appropriate.
A nice overview is Satisfiability Modulo Theories: Introduction and Applications
by De Moura and Bjørner,
doi:10.1145/1995376.1995394.

Answer set programming (ASP) came out of logic programming.
Due to its focus on solving the more general problem of finding a stable model, and also because it allows universal as well as existential quantification, ASP was for many years not competitive with CP or SMT.

Formally, SAT is CSP on Boolean domains, but the focus in SAT on clause learning, good heuristics for conflict detection, and fast ways to backtrack are quite different to the traditional CSP focus on propagators, establishing consistency, and heuristics for variable ordering.
SAT is usually extremely efficient, but for many problems huge effort is required to first express the problem as a SAT instance.
Using a higher level paradigm like CP can allow a more natural expression of the problem, and then either the CP instance can be translated into SAT by hand, or a tool can take care of the translation.
A nice overview of the nuts and bolts of SAT is On Modern Clause-Learning Satisfiability Solvers by Pipatsrisawat and Darwiche, doi:10.1007/s10817-009-9156-3.

Now let's move on from generalities to present day specifics.

Over the last decade some people in CP have started to focus on lazy clause generation (LCG).
This is essentially a way to bolt CP propagators together using more flexible SMT-like techniques rather than the rather rigid active domains abstraction.
This is useful because there is a long history of published CP propagators to efficiently represent and solve many kinds of problems.
(Of course, a similar effect would be achieved by concerted effort to implement new theories for SMT solvers.)
LCG has performance that is often competitive with SMT, and for some problems it may be superior.
A quick overview is Stuckey's CPAIOR 2010 paper Lazy Clause Generation: Combining the power of SAT and CP (and MIP?) solving, doi:10.1007/978-3-642-13520-0_3.
It is also worth reading the position paper of Garcia de la Banda, Stuckey, Van Hentenryck and Wallace, which paints a CP-centric vision of The Future of Optimization Technology, doi:10.1007/s10601-013-9149-z.

As far as I can tell, much of the focus of recent SMT research seems to have shifted to applications in formal methods and formalised mathematics.  An example is reconstructing proofs found by SMT solvers inside proof systems such as Isabelle/HOL, by building Isabelle/HOL tactics to reflect inference rules in SMT proof traces; see Fast LCF-Style Proof Reconstruction for Z3 by Böhmer and Weber at ITP 2010.

The top ASP solvers have over the last few years been developed to become competitive with CP, SMT and SAT-only solvers.
I'm only vaguely familiar with the implementation details that have allowed solvers such as clasp to be competitive so cannot really compare these with SMT and CP, but clasp explicitly advertises its focus on learning nogoods.

Cutting across the traditional boundaries between these formalisms is translation from more abstract problem representations into lower level efficiently implementable formalisms.
Several of the top ASP and CP solvers now explicitly translate their input into a SAT instance, which is then solved using an off-the-shelf SAT solver.
In CP, the Savile Row constraint modelling assistant uses compiler design techniques to translate problems expressed in the medium level language Essence' into a lower level formalism, suitable for input to CP solvers such as Minion or MiniZinc.
Savile Row originally worked with a CP representation as the low-level formalism but introduced SAT as a target in version 1.6.2.
Moreover, the even higher-level language Essence can now be automatically translated into Essence' by the Conjure tool.
At the same time, low level SAT-only solvers like Lingeling continue to be refined each year, most recently by alternating clause learning and in-processing phases; see the brief overview What's Hot in the SAT and ASP Competitions by Heule and Schaub in AAAI 2015.

The analogy with the history of programming languages therefore seems appropriate.
SAT is becoming a kind of "machine code", targeting a low-level model of exploration of the clauses in the clause structure.
The abstract paradigms are becoming more like higher level computer languages, with their own distinct methodologies and applications they are good at addressing.
Finally, the increasingly dense collection of links between these different layers is starting to resemble the compiler optimisation ecosystem.


Are DPDAs without a $\epsilon$ moves as powerful as DPDAs with them? In the formal description of Deterministic Pushdown Automata, they allow $\epsilon$ moves, where the machine can pop or push symbols onto the stack without reading a symbol from the input. If these $\epsilon$ moves aren't allowed, and the stack can only be modified once after each symbol read, are the resulting automata equal to power to DPDAs?

There may be something trivial I am missing with regards to using the powerset of $\Gamma$ as your new $\Gamma$, allowing you to "compress" $\epsilon$ moves into the equivalent automaton without them, similar to how you can compress $\epsilon$ moves in a DFA. Just it seems that such a conversion is not as trivial as for DFAs, and I'm not sure it's even possible.

So are the two equivalent in power? I'm just asking because everyone seems to assume that DPDAs have $\epsilon$ moves and I'm wondering why that assumption exists, since it seems like a more complex model.

Perhaps I found some relevant information in:

Jean-Michel Autebert, Jean Berstel, Luc Boasson; Context-Free Languages and Pushdown Automata; Handbook of Formal Languages; 1997, pp 111-174

DPDAs without $\epsilon$-transitions are known as realtime deterministic pushdown automata.

They are less powerful than DPDAs, for example

$L = \{ a^n b^p c  a^n \mid p,n > 0\} \cup \{ a^nb^pdb^p\mid p,n > 0 \}$

is deterministic and can be recognized by a DPDA, but cannot be recognized by any realtime DPDA.

What you can do is eliminate increasing $\epsilon$-transitions:

Proposition 5.4: For any DPDA it is possible to construct a DPDA recognizing the same language such that any $\epsilon$-rule is decreasing.


Relation between $AC^0$ and regular languages Let $\mathsf{REG}$ be the class of all regular languages.

It is known $\mathsf{AC}^0 \not\subset \mathsf{REG}$ and $\mathsf{REG} \not\subset \mathsf{AC}^0$. But is there any characterization for languages in $\mathsf{AC}^0 \cap \mathsf{REG}$?

The following paper seems to contain an answer:

Mix Barrington, D. A., Compton, K., Straubing, H., Therien, D.: Regular languages in $\mathsf{NC}^1$. Journal of Computer and System Sciences 44(3), 478-499 (1992) (link)

One of the characterizations obtained there is as follows. The class $\mathsf{REG} \cap \mathsf{AC}^0 \subset \{0, 1\}^*$ contains exactly those languages that can be obtained from $\{0\}$, $\{1\}$ and $\mathsf{LENGTH}(q)$ for $q > 1$ with a finite number of Boolean operations and concatenations. Here every language $\mathsf{LENGTH}(q)$ contains all strings whose length is divisible by $q$. (There is also a logical characterization and two algebraic ones.)


Is the feedback vertex set problem on planar bounded degree graphs hard? Is it known whether the feedback vertex set problem on undirected planar graphs of bounded degree is $\mathsf{NP}$-hard?

According to Garey and Johnson's book Vertex Cover is NP-complete on planar graphs of maximum degree four. Using a simple reduction from Vertex Cover to Feedback Vertex Set should give maximum degree eight and preserve planarity.

VC to FVS: Replace each edge by a triangle (or a double edge).

One note:
Garey and Johnson also state that directed FVS is NP-complete on planar digraphs with no in- or out-degree exceeding two. They do not specifically mention undirected FVS under such restrictions.


Bounded distance decoding beyond Babai Consider a full-rank lattice in $\mathbb{R}^n$. Let $\lambda_1$ be the length of the shortest nonzero vector. Given a vector in $\mathbb{R}^n$ we wish to find the nearest lattice vector, as measured by Euclidean distance. In general this is NP-hard. However, we can add the promise that distance to the nearest lattice vector is at most $d$. I'll refer to this as the bounded distance decoding problem. My understanding is that Babai's nearest plane algorithm provably solves this for $d \leq 2^{-c n} \lambda_1$ for some specific value of $c$ (which I don't know but which I believe to be known, and which I think maybe originates from an LLL preprocessing step). My question is whether there is a known way to efficiently go beyond this by a polynomial factor. For example, is there a known polynomial-time algorithm to solve bounded distance decoding at $d = n 2^{-cn} \lambda_1$? The closest to this that I have managed to find in the literature is an algorithm by Klein and subsequent extension by Liu, Ling, and Stehle, which appears to extend beyond the radius of Babai's algorithm by a factor of $k$ at a complexity cost of $n^{k^2}$.

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

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

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

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

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

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

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

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

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

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


Lambda: The Ultimate Imperative - who is Jensen? One of the notes in the classical paper LAMBDA: The Ultimate Imperative says:

  {Jensensdevice}

  The technique of repeatedly modifying a variable passed call-by-name in order to produce side effects on another call-by-name parameter is commonly known as Jensen's device, particularly in the case where call-by-name parameters are j and a[j]. We cannot find any reference to Jensen or who he was, and offer a reward for any information leading to the identification, arrest, and conviction of said Jensen.

Today, after almost 40 years since the memo was published, do we know the identity of Jensen? I'm not hoping for the reward, just curious.

Jensen's device was developed by Jørn Jensen, who worked on one of the earliest ALGOL 60 compilers (this answer is based on comment by Kristoffer Arnsfelt Hansen).


Typo in the calculus of constructions paper? In the classic the calculus of constructions paper there is a rule that states

(page 7 of the pdf, page 101 of the original document)

This rule would mean that any context is reducible to a member of that context.  This seems like it shouldn't be correct, as it would entail

1 ≅ Nat
3 ≅ Nat
1 ≅ 3

if Nat is a context.

I think the best interpretation is that the lower delta was meant to be an M.  Especially considering the rules given on the next page.

So is this simply a typo, or some subtle logical rule that I don't understand?

You are correct, there is an error in that paper, and the rule should indeed read:
$$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$

the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see here for example). It's often replaced with an untyped operational definition in modern treatments, where there is no jugement of the form $\Gamma\vdash N\cong M$, and conversion is defined on raw terms.

Somewhat counter-intuitively, proving that the system with typed conversion is equivalent to the one without types is very difficult, and was settled in 2010 by Siles and Herbelin.


Where is the quote "Informal proofs are algorithms, formal proofs are code" from? Does anyone know the origin of the quote,

  Informal proofs are algorithms; formal proofs are code.

Its made in Benjamin C. Pierce et al.'s Software Foundations.

He doesn't cite any references for it and
Google doesn't return any results so
I don't think he is really quoting from anywhere.

The idea that a proof is a "construction"
(a term in intuitionistic/constructive mathematics
with a very close meaning to what we call algorithm nowadays)
goes back to at least Luitzen Egbertus Jan Brouwer.
Note that Brouwer was talking about informal proofs
as typically stated by mathematicians,
not formalized proofs which are a very recent phenomenon.

The idea that a formal proof is a like a program in a programming language
can be traced back to at least to
the BHK interpretation of intuitionistic logic by Arend Heyting.
The formal correspondence is Curry-Howard isomorphism.


parallel algorithms for the determinant of the Hessenberg matrix I am interested in highly parallel algorithms for computing the determinant of matrices of a special form (over finite fields).

It is known that computing determinant of general matrices over finite fields is in NC2.
I've been wondering whether something better is known (hopefully NC1) for the (say, lower) Hessenberg matrix.

If it helps, it is further restricted so that its subdiagonal is all 1's, and all I care about is whether the determinant is 0 or not.

Sorry, this is clearly unlikely.
Otherwise, it would be possible to use the algorithm to solve any NL\poly
problem in NC1 via a reduction to evaluating the determinant of a Hessenberg matrix over a sufficiently large field.
The reduction appears as Lemma 3 (and related discussion) in
"Perfect constant-round secure computation via perfect randomizing polynomials".


On the notion of positive rank of a matrix The positive rank of a square matrix is defined in Theorem $3$ of "Expressing Combinatorial Optimization Problems by Linear Programs" by Mihalis Yannakakis as follows: given a $n\times n$ matrix $A$, the positive rank $rank_{\Bbb R}^+(A)$ is the smallest $m$ such that $A=LR$ for a non-negative $n\times m$ matrix $L$, and non-negative $m\times n$ matrix $R$.

This concept is valuable in communication complexity, since it was shown that if $rank_{\Bbb R}^+(A)$ and $rank_{\Bbb R}(A)$ could be subexponentially related for a $0/1$ matrix $A$, then the log-rank conjecture holds.

Is there an exponential separation between $rank_{\Bbb R}^+(A)$ and $rank_{\Bbb R}(A)$ for a general non-negative real matrix $A$ (as opposed to just $0/1$) or is this problem also open?

I checked the references in Jukna's book, but I am still unable to clarify the above question.

There are examples of $n\times n$ real matrices of rank at most $3$ and non-negative rank at least $\sqrt{2n}$. So the non-negative rank cannot be bounded by any function of the rank in general. The construction I am aware of goes through extension complexity. An explanation follows.

The extension complexity $xc(K)$ of a convex set $K$ in $\mathbb{R}^d$ is the smallest possible number of facets of a (higher-dimensional) polytope that projects to $K$. (Equivalently the smallest possible number of constraints in a linear program for $K$). A famous theorem of Yannakakis shows that if there exist $A$, $b$ and $v_1, \ldots, v_n$ such that $K = \{x: Ax \leq b\} = \mathrm{conv}(v_1, \ldots, v_n)$, then
$$
xc(K) = \mathrm{rank}^+(S),
$$
where $S$ is the slack matrix, defined by $S = b1^T - A^TV$ for $V = (v_1, \ldots, v_n)$, i.e. the matrix whose columns are the $v_i$.

A result by Fiorini, Rothvoss, and Tiwari shows that there exist two-dimensional $n$-gons with extension complexity at least $\sqrt{2n}$. Since any $n$-gon $P$ in $\mathbb{R}^2$ can be written as $P = \{x: Ax \leq b\} = \mathrm{conv}(v_1, \ldots, v_n)$ for $A$ an $n\times 2$ matrix, $b$ an $n\times 1$ vector and $V = (v_1, \ldots, v_n)$ a $2\times n$ matrix, the slack  matrix $S = b1^T - A^TV$ of $P$ is the sum of a rank $1$ and a rank $2$ matrix, and therefore is of rank at most $3$. On the other hand by Yannakakis's and Fiorini et al.'s results $\mathrm{rank}^+(S) = xc(P) \geq \sqrt{2n}$.


the type system does not tell the whole story due to "exception" I am wondering whether it is a bad style to use "exception". For example, in Ocaml, the exception does not appear as the .mli file. So it appears to me that "exception" is something that cannot be tracked by a type system.

So my question in general is, is using exception a bad style because it hides information against the type system?

Concretely, I am trying to implement a type checker for an imperative language, say, Pascal. The essential judgment should have been of this signature,

well-typed_1: environment -> statement -> unit

But this seems to be insufficient because the environment would be modified due to a local variable declaration, thus a more reasonable interface for typechecker would be

well-typed_2: environment -> statement -> environment

An alternative would be use the former one, well-typed_1, dealing with local variables declaration through an exception Var_declaration (e : environment) which returns the updated environment to the type checker for its other recursion.

So, my question for this concrete example is , should I use the well-typed_1 + exception for variable declaration, or well-typed_2?

The disadvantage of well-typed_2 seems to be that, for most statement there are no side effect with regard to environment of types, thus that signature of well-typed_2 seems to be a bit redundant. The disadvantage of well_typed_2 + exception seems to reveal a general issue: the the signature of well-typed_1 in does not tell the whole story. (it does not tell the potential exception)

There have been numerous type systems dealing with exceptions and other kinds of computational effect, so the reason it doesn't appear in O'Caml is not that it cannot be done. I think there are two reasons why exceptions do not appear in types:

The types that programmers have to write become larger.
Exception typing interacts poorly with subtyping and higher-order features, such function types. Ultimately, this is because exception declarations will be an over-approximation of the exceptions that will be thrown, so reusable code needs to have very general exception declarations. For example, the exception declarations for a higher-order function need to be general enough to describe all possible functions passed to the higher-order function. Similarly, the exception declarations on a superclass need to anticipate all possible exceptions that can occur in the subclasses.  (Subtyping among exception types alleviates this problem somewhat.)

Java is a good example programming language that has exception typing and these two problems.

Here is some of the research done in the area:

Type-based analysis of Uncaught Exceptions by Xavier Leroy and Francois Pessaux
Monadic effects by Andrzej Filinski
A type system for call-by-name exceptions by Sylvain Lebresne
A theory of substructural types and control by Jesse A. Tov and Riccardo Pucella

Looking at these papers and chasing the references within will give you more details of what has been done in the field.


H-representation of convex hull Consider a set of polytopes $P_j\;\;j=1,2,\dots,r$ with the same structure as follows:

$P_j=\Big\{(x_{j1},\dots, x_{jt})\Big| \sum_{i=1}^t x_{ji}=1, x_{ji}\in [a_{ji},b_{ji}]\subseteq [0,1]\Big\}$ for $j=1\dots,r$.

Is it possible to derive the H-representation of the convex hull of the union of $P_j$s, i.e., ConvexHull$(\bigcup_j P_j)$, efficiently?

If you're okay with additional variables, then the answer is yes. This follows from Balas's extended formulation for the disjunction of polyhedra. It shows that $\operatorname{convex}.\operatorname{hull} ( \cup_j P_j)$ admits an extended formulation of size at most $\sum_{j}(\operatorname{xc}(P_j)+1)$, where $\operatorname{xc}(\cdot)$ denotes extension complexity. (The extension complexity of $P_j$ is at most the number of inequalities defining $P_j$.)

I have not thought about whether this can be done in the original space of variables.


Closure Properties of Locally Testable Language Are locally testable languages closed under complementation? I guess yes, because when I can decide membership by sliding a window of size $k$ over the word and looking if the $k$-length words appearing under the window are in a specified set, then deciding the complement is simply looking if some string under the window is not in the set.

The Wikipedia article states that these languages are not closed under complementation. Contrarily, in the paper Local languages and the Berry-Sethi algorithm by J. Berstel & Jean Eric Pin the authors prove that these languages are closed under union, concatenation and Kleene-Star, as opposed to the Wikipedia article. so the Wikipedia information does not seem very trustworthy. Following the proofs in the paper, if I have a local automaton, then the automaton in which the final- and ordinary states are exchanged is still local I think and accepts the complement of the original language. So I think these languages should be closed under complement. Am I right?

A language is $k$-locally testable if it is a Boolean combination of languages of the form $\{u\}$, $vA^*$, $A^*v$ or $A^*wA^*$, with $|u| < k - 1$, $|v| = k - 1$ and $|w| = k$. Thus, yes, $k$-locally testable languages are closed under complementation.

But the link you gave to Wikipedia gives the definition of local languages, which is not the same thing as locally testable languages.
And indeed, local languages are not closed under complementation.

Finally, a local automaton recognizing a language $L$ might be incomplete. Therefore, you first need to complete it to compute the complement of $L$ by exchanging final and non final states. But this completed automaton is no longer local...


Almost uniform sampling implies approximate counting I began studying papers about approximate counting and I keep seeing the above being quoted,  without further explanation. I suppose the procedure that yields the result is very well known and that is why. Can anyone give me roughly the idea if possible and secondly some references about it?

Given a set $A \subseteq B$, if you can sample uniformly from $B$, then you can estimate by repeated sampling the probability of the event that the sample is in $A$. That is, you can approximate the probability $|A| / |B|$, which is indeed close to enumerating the elements of $A$, and thus computing its size.


What is the proof of this nonstandard version of Azuma's inequality? In Appendix B of Boosting and Differential Privacy by Dwork et al., the authors state the following result without proof and refer to it as Azuma's inequality:

  Let $C_1, \dots, C_k$ be real-valued random variables such that for every $i \in [k]$,

  $\Pr[|C_i| \leq \alpha] = 1$, and
  for every $(c_1, \dots, c_{i - 1}) \in \text{Supp}(C_1, \dots, C_{i - 1})$, we have $\text{E}[C_i \mid C_1 = c_1, \dots, C_{i - 1} = c_{i - 1}] \leq \beta$.

  Then for every $z > 0$, we have $\Pr[\sum_{i = 1}^k C_i > k\beta + z \sqrt{k} \cdot \alpha] \leq e^{-z^2/2}$.

I'm having trouble proving this. The standard version of Azuma's inequality says:

  Suppose $\{X_0, X_1, \dots, X_k\}$ is a martingale, and $|X_i - X_{i - 1}| \leq \gamma_i$ almost surely. Then for all $t > 0$, we have $\Pr[X_k \geq t] \leq \exp(-t^2/(2 \sum_{i = 1}^k \gamma_i^2))$.

To prove the version of Azuma's inequality stated by Dwork et al., I figured we should take $X_0 = 0$ and $X_i = X_{i - 1} + C_i - \text{E}[C_i \mid C_1, C_2, \dots, C_{i - 1}]$. That way, I think $\{X_0, \dots, X_k\}$ is a martingale. But all we can say is that $|X_i - X_{i - 1}| \leq 2\alpha$ almost surely, right? That factor of two causes trouble, because it means that after substituting, we merely find that $\Pr[\sum_{i = 1}^k C_i > k\beta + z\sqrt{k} \cdot 2\alpha] \leq e^{-z^2/2}$, which is weaker than the conclusion stated by Dwork et al.

Is there a simple trick I'm missing? Is the statement by Dwork et al. missing a factor of two?

I can't find a reference, so I'll just sketch the proof here.

Theorem. Let $X_1, \cdots, X_n$ be real random variables. Let $a_1, \cdots, a_n, b_1, \cdots, b_n$ be constants. Suppose that, for all $i \in \{1,\cdots,n\}$ and all $(x_1,\cdots,x_{i-1})$ in the support of $(X_1, \cdots, X_{i-1})$, we have

$\mathbb{E}[X_i | X_1=x_1, \cdots, X_{i-1}=x_{i-1}] \leq 0$ and
$\mathbb{P}[X_i \in [a_i,b_i]]=1$.

Then, for all $t\geq0$, $$\mathbb{P}\left[\sum_{i=1}^n X_i \geq t\right] \leq \exp\left(\frac{-2t^2}{\sum_{i=1}^n (b_i-a_i)^2}\right).$$

Proof. Define $Y_i = \sum_{j=1}^i X_j$. We claim that $$\forall i \in \{1,\cdots,n\}~\forall \lambda \geq 0 ~~~~~ \mathbb{E}\left[e^{\lambda Y_i}\right] \leq e^{\frac18 \lambda^2 \sum_{j=1}^i (b_j-a_j)^2}.\tag*{(*)}$$ For all $i$ and $\lambda$, we have $$\mathbb{E}\left[e^{\lambda Y_i}\right] = \mathbb{E}\left[e^{\lambda Y_{i-1}}\cdot e^{\lambda X_i}\right] = \mathbb{E}\left[e^{\lambda Y_{i-1}}\cdot \mathbb{E}\left[e^{\lambda X_i}\middle|Y_{i-1}\right]\right].$$
By assumption, $\mu(y_{i-1}):=\mathbb{E}[X_i|Y_{i-1}=y_{i-1}]\leq 0$ and $\mathbb{P}[X_i \in [a_i,b_i]] =1$ for all $y_{i-1}$ in the support of $Y_{i-1}$. (Note that $Y_{i-1}=X_1+\cdots+X_{i-1}$.) Thus, by Hoeffding's lemma, $$\mathbb{E}\left[e^{\lambda X_i}\middle|Y_{i-1}=y_{i-1}\right] \leq e^{\lambda\mu(y_{i-1})+\frac18 \lambda^2(b_i-a_i)^2}$$ for all $y_{i-1}$ in the support of $Y_{i-1}$ and all $\lambda \in \mathbb{R}$. Since $\mu(y_{i-1})\leq 0$, we have, for all $\lambda \geq 0$, $$\mathbb{E}\left[e^{\lambda Y_i}\right] \leq \mathbb{E}\left[e^{\lambda Y_{i-1}}\cdot e^{0+\frac18 \lambda^2(b_i-a_i)^2}\right].$$
Now induction yields the claim (*) above.
Now we apply Markov's inequality to $e^{\lambda Y_n}$ and use our claim (*). For all $t, \lambda > 0$, $$\mathbb{P}\left[\sum_{i=1}^n X_i \geq t\right]=\mathbb{P}[Y_n \geq t] = \mathbb{P}\left[e^{\lambda Y_n} \geq e^{\lambda t}\right] \leq \frac{\mathbb{E}\left[e^{\lambda Y_n}\right]}{e^{\lambda t}} \leq \frac{e^{\frac18 \lambda^2 \sum_{i=1}^n (b_i-a_i)^2}}{e^{\lambda t}}.$$
Finally, set $\lambda=\frac{4t}{\sum_{i=1}^n (b_i-a_i)^2}$ to minimize the right hand expression and obtain the result. $\tag*{$\blacksquare$}$
As I mentioned in my comment, the key difference between this and the "usual" statement of Azuma's inequality is requiring $X_i \in [a_i,b_i]$, rather than $X_i \in [-a,a]$. The former allows more flexibility and this saves a factor of 2 in some cases.
Note that the $Y_i$ random variables in the proof are a supermartingale. You can obtain the usual version of Azuma's inequality by taking a Martingale $Y_1, \cdots, Y_n$, setting $X_i=Y_i-Y_{i-1}$ and $[a_i,b_i]=[-c_i,c_i]$ (where $\mathbb{P}[|Y_i-Y_{i-1}|\leq c_i]=1$), and then applying the above result.


Embedding a graph in the euclidean space Given a graph $G=(V,E)$, find a mapping $f\colon V \rightarrow \mathbb R^d$ such that for every edge $(u,v) \in E$ we have that $||f(u)-f(v)|| \leq r$; and for every $(u,v) \not \in E$, we have the opposite $||f(u)-f(v)|| > r$ for some given $r$.
One could also view this problem as embedding a unit disc graph back into the euclidean space.

Now I have been told that - while the problem is NP-complete - the usual way to do it is as follows. This is where the hearsay starts, so excuse me if I am a little vague.

The proposed approach places an arbitrary node at $0$. Then, run a linear (or quadratic?) program that maximizes $\sum_{v \in V} g(f(v))$ under the side condition stated above, i.e. for all edges $(u,v) \in E$, $(f(u) - f(v))^2 \leq r^2$. $g$ is probably some norm, maybe $L_1$ or $L_2$.

This is how I more or less understood it. The general gist was to fix the position of an initial node and then "spread" the graph apart using the linear program.

I tried to find some sources on that, maybe a paper that introduced this approach, but so far my efforts failed - there are just too many ways to embed a graph in the $\mathbb R^d$. In particular, I am interested in how this approach deals with noisy data. For example, consider a grid graph of size $n \times n$ which should be perfectly embeddable in the euclidean plane. Now, add an edge from $(0,0)$ to $(n,n)$. Intuitively, in an embedding I would like to ignore the edge since the rest of the graph is a perfect grid. The approach above, however, would most likely produce a weird embedding.

Can anyone give me some pointers to work describing this approach?

I finally managed to ask the person that originally told me about this approach. It appears to be closely related to maximum variance unfolding (MVU), see also https://en.wikipedia.org/wiki/Semidefinite_embedding. The paper introducing this approach is "Learning a kernel matrix for nonlinear dimensionality reduction" by Weinberger, Sha, and Saul if I am not mistaken.


Bounds on the size of the solution of a quadratic program I am interested in a quadratic program of the form

$$ \min x^T Q x $$
$$s.t.$$
$$ Ax \leq b $$
where $x$ is a vector with $n$ entries, the size of the maximal entry in $Q, A$, and $b$ is $\varphi$, $A$ has $2^n$ rows, and  $Q$ has $poly(n)$ rows.

Is it true that if there is a minimal solution to the program, then there is one of size that is polynomial in $n$ and $\phi$?

Thanks!

In Quadratic Programming is in NP, it is shown that a slight variant of this problem (QPL) is in NP. The question can be formulated as follows: does there exist a point $x \in \mathbb{R}^n$ such that $ Ax \leq b $ and $x^T Q x \leq K$, where $K$ is a rational number. In the section 2 of this paper, they prove that, when the minimum exists, then there is a minimum $x^*$ with a polynomial number of digits. Their proof is independent from $K$, so it directly applies to your formulation.

The claim that $x^*$ has a polynomial number of digits is not enough, since you want the solution to be polynomial in $\varphi$ and $n$.

In their proof, they define $x^*$ as a particular global minimum with the maximum number of active inequalities, and then, they construct a nonsingular system of linear equations and show that $x^*$ (or a projection of $x^*$) is its unique solution. Thanks to a theorem by Edmonds they conclude that $x^*$ has a polynomial number of digits.

Since the system has a unique solution, $x^*$ is also the solution to a subsystem consisting of $n$ of the equations. At first sight, the projection of $x^*$ does not seem to be a problem, and all the coefficients of these equations can be kept integer and polynomial in $\varphi$.

So that should reduce your question to the following one:

For systems of linear equations $Cx=d$ (where $C$ is a $n\times n$ integer matrix, and the maximal entry in $C$ and $d$ is $\varphi$) with a unique solution $x^*$, is it true that $x^*$ is polynomial in $n$ and $\varphi$?

EDIT. As pointed out by Kristoffer Arnsfelt Hansen, it is of course useless to consider more than $n$ linear equations.


Complexity one-alternation SMT I'm looking for the complexity of satisfiability of a formula $\forall y_1, \dots,y_n, \exists x_1,\dots,x_m, \phi$ or of a formula $ \exists x_1,\dots,x_m \forall y_1, \dots,y_n,\phi$ where $\phi$ is formula of the form :
$$\phi:= \phi \wedge\phi ~| ~\neg \phi ~| ~ \phi\to \phi~| ~\psi$$
$$\psi := t>t~| ~t=t$$
$$ t:= t+t~| ~x_i~|~y_i ~| ~c$$
Where $c$ are the constant in $\mathbb{N}$, and the domain of variables $x_i,y_i$ is also $\mathbb{N}$.

In fact the $y_i$ are either $0$ or $1$. Does that simplify the complexity?

All answer with references would be gladly accepted.

Thanks

The question of truth in Presburger Arithmetic with bounded quantifier alternation has been answered with quite some precision by Reddy and Loveland:

C.R. Reddy & D.W. Loveland: Presburger Arithmetic with Bounded Quantifier Alternation.

The paper may be found here (sorry for the ugly link). Their main result is stated as follows:

  The membership in $\mathrm{PA}(m)$ (where $m$ is the number of quantifier alternations) of length $n$ can be decided within space
  $$ 2^{dn^{m+4}}$$
  and in (deterministic) time
  $$ 2^{2^{en^{m+4}}}$$
  Where $d$ and $e$ are constants.

Taking $m=2$, this seems to give at least an upper bound on what you want, and I suspect it's not far from tight, as you have almost full Presburger atomic formulas "at the root".


Trying understand a move in Cohen's proof of the independence of the continuum hypothesis I've read a few different presentations of Cohen's proof. All of them (that I've seen) eventually make a move where a Cartesian product (call it CP) between the (M-form of) $\aleph_2$ and $\aleph_0$ into {1, 0} is imagined. From what I gather, whether $CP \in M$ is what determines whether $\neg$CH holds in M or not such that if $CP \in M$ then $\neg$CH.

Anyway, my question is: Why does this product, CP, play this role? How does it show us that $\aleph_2 \in M$ (the 'relativized' form of $\aleph_2$, not the $\aleph_2 \in V$)? Could not some other set-theoretical object play the same role?

Our goal is to prove that $\aleph_1 < 2^{\aleph_0}$ in the model $M[G]$, and therefore the Continuum Hypothesis is not true in $M[G]$. This is equivalent to saying that $\aleph_2 \leq 2^{\aleph_0}$. So we need to construct a model $M[G]$ such that there is an injective map $f$ from $\aleph_2$ to $2^{\aleph_0}$ in $M[G]$. Note that each element of  $2^{\aleph_0}$ is a function from $\aleph_0$ to $\{0,1\}$ (by definition). Thus $f(x)$ (the value of $f$ at point $x$) is actually a function that maps a natural number to $\{0,1\}$. In the proof, we treat $f$ as a function of two parameters
$$h(x,y) = f(x)(y)$$
where $x\in \aleph_2$ and $y\in \aleph_0$. This is the reason why we want to prove that there exist a function $h$ from $\aleph_2 \times \aleph_0$ to $\{0,1\}$ satisfying certain properties.

The choice of $\aleph_2$ here is not arbitrary. Say, if we wanted to prove that $2^{\aleph_0} > \aleph_{19}$, we would consider functions from $\aleph_{20} \times \aleph_0$ to $\{0,1\}$.

BTW, $\aleph_2^M$ is always an element of $M$ and $M[G]$ (for any generic set $G$); on the other hand $\aleph_2$ is usually neither an element of $M$ nor $M[G]$, since $M$ is a countable transitive model of ZFC (or more precisely is a countable model of a large finite fragment of ZFC). So I'm not sure what you mean in the last paragraph.


Why is the reduction from 3-SAT to 3-dimensional Matching Parsimonious? In this talk at the Simons Institute, Holger Dell notes that there is a parsimonious reduction from 3-SAT to the 3-dimensional Matching (3-DM) problem. In other words, there is a reduction between these two problems that also works as a reduction from counting satisfying assignnments to counting 3-dimensional matchings.
My question then, is what is an example of a parsimonious reduction from 3-SAT to 3-DM?
Additional Context:
The only reduction from 3-SAT to 3-DM I know of is the one presented in Garey & Johnson's Computers and Intractability (page 50, theorem 3.2). That reduction involves composing certain variable gadgets, clause gadgets, and garbage collection gadgets. Roughly speaking, a satisfying assignment is mapped to a partial matching of vertices in the variable and clause gadgets, and then this partial matching is extended to a full matching using the garbage collection gadgets.
It seems like that reduction ought not to be parsimonious because each satisfying assignment is mapped to a partial matching, and there are many different ways of using the garbage collection to extend this to a full matching. In addition, if a satisfying assignment is chosen that does not set a unique literal to True in each clause, the clause gadgets also seem to have multiple ways to extend the matching.
Is there a way to fix this reduction to be parsimonious? Or is the parsimonious reduction completely different? Or maybe the observations I made in this question are false?

You're right that the standard reduction from 3-SAT to 3D-matching (3DM) is not parsimonious.
For the record, here's a sketch of a reduction that is parsimonious.
It is obtained by composing parsimonious reductions from 3-SAT to 1-in-3-SAT, from 1-in-3-SAT to a problem we call 1+3DM, and from 1+3DM to 3DM.  We sketch each of these next.
Lemma 1. There is a parsimonious poly-time reduction from 3-SAT to 1-in-3-SAT.
Note: This reduction comes originally from [1].  [2] points out that it is parsimonious.
[1] Schaefer, Thomas J. The complexity of satisfiability problems, 1978, Proceedings of the tenth annual ACM symposium on Theory of computing.
[2] V. Bura. A Kernel Method for Positive 1-in-3-SAT.  draft on arXiv.org.
Proof sketch.  Given any 3-SAT instance $\Phi$, obtain $\Phi'$ from $\Phi$ by replacing each clause $x \vee y \vee z$ by the clauses $(\lnot x \vee u_1 \vee u_2) \wedge (y \vee u_2 \vee u_3) \wedge (\lnot z \vee u_3 \vee u_4)$, where $u_1, u_2, u_3, u_4$ are new variables specific to this clause.  The satisfying assignments for $\Phi$ then correspond bijectively to assignments for the modified formula $\Phi'$ such that exactly one literal in each clause is true. $~~~\Box$
For example, in an assignment for $\Phi$ that makes $x$ and $y$ true and $z$ false, the corresponding assignment for $\Phi'$ would extend that assignment by taking $u_1$ to be true, and $u_2, u_3, u_4$ to be false.
Next define 1+3DM to be the following variant of 3DM.  The input $(X,Y,Z,T,S)$ consists of three pairwise-disjoint sets $X, Y, Z$ each containing $n$ elements, a collection of triples $T \subseteq X\times Y \times Z$, and a collection of singletons $S\subseteq X \cup Y \cup Z$. The problem is to choose some of the triples and singletons so that each element is in exactly one of the chosen triples or singletons.  For technical reasons, we restrict to instances where, for every valid matching (solution), the set of chosen singletons distinctly determines the solution.
Lemma 2. There is a parsimonious reduction from 1-in-3-SAT to 1+3DM.
Proof sketch.  Given a 1-in-3-SAT formula $\Phi$, the reduction produces the following instance of 1+3DM.
For every variable $a$ in $\Phi$, let $k$ be the number of occurrences of $a$ in $\Phi$.  Build a variable gadget of "size" $k$ as follows.  First, create $4k$ new elements $a_1, a_2, \ldots, a_k$, and $\overline a_1, \overline a_2, \ldots, \overline a_k$, and $y_1, y_2, \ldots, y_k$ and $z_1, z_2, \ldots, z_k$.  For each $i\in\{1,2,\ldots, k\}$ add triples $(a_i, y_i, z_i)$ and $(\overline a_i, y_i, z_{i-1})$, interpreting $z_0$ as $z_k$.  Here's an illustration for $k=3$:
$~~~$
Note that in any solution either the $k$ triples of the form $(a_i, y_i, z_i)$ must be chosen, or the $k$ triples of the form $(\overline a_i, y_i, z_{i-1})$ must be chosen.  Hence, either all $k$ $a_i$'s are left uncovered, or all $k$ $\overline a_i$'s are left uncovered.
For every clause create a "clause gadget" as follows.  We'll illustrate the construction by example.  For the clause $a\vee \overline b \vee c$ in $\Phi$, select elements $a_h$, $\overline b_i$, $c_j$ (one for each literal in the clause), from the previously created variable gadgets, where the indices are chosen so that the clause contains the $h$th, $i$th, and $j$th occurrences of the variables $a$, $b$, and $c$, respectively, in $\Phi$.
Create two new nodes $y,z$.
Add three triples $(a_h, y, z)$, $(\overline b_i, y, z)$, and $(c_j, y, z)$:
$~~~$
Finally add three elements $\overline a_h$, $b_i$, and $\overline c_j$ (for the complements of the literals in the clause) to the set of singletons $S$.  These "singleton" elements do not occur in any triple in any clause gadget, although they do occur in triples in their respective variable gadgets.
Note that, for each variable $a$, among each pair of elements $a_i$ and $\overline a_i$ in the variable gadget, one of $a_i$ or $\overline a_i$ occurs in a triple in any clause gadget, while the other does not and is an allowed singleton.
Note that any solution must choose one of the triples in each clause gadget, thereby covering one of the three elements for the literals in the clause.
This completes the reduction.
To verify that it is correct, consider any 1-in-3 satisfying assignment $A$ for $\Phi$.  The corresponding matching uses the following triples.  For each variable $a$ that is true, use the triples of the form $(\overline a_i, y_i, z_{i-1})$ to cover all elements in the variable gadget except the $a_i$'s; also, for each element $a_i$ that is not used in any clause gadget, choose $a_i$ as a singleton.
For each variable $a$ that is false, use the triples of the form $(a_i, y_i, z_i)$ to cover all the elements of the variable gadget except the $\overline a_i$'s; also, for each element $\overline a_i$ that is not used in any clause gadget, choose $\overline a_i$ as a singleton.
For each clause, e.g., $a\vee \overline b \vee c$, select the true literal, and use the triple from the clause gadget that contains that literal.  E.g. if $a$ is true, use the triple $(a_i, y, z)$ from the clause gadget.
The above correspondence is a bijection between 1-in-3 assignments to $A$ and valid matchings, so the reduction is correct.
The instance meets the technical requirement that, for every valid matching, the set of chosen singletons is distinct.  This is because, for each variable, for each occurrence of that variable, the singleton is used iff the corresponding assignment sets the variable so that the literal does not satisfy the clause, so the presence or absence of the singleton determines the value assigned to the variable.  So the set of chosen singletons determines the corresponding assignment, which in turn determines the entire matching. $~~~\Box$
Lemma 3. There is a parsimonious reduction from 1+3DM to 3DM.
Proof idea. Given any instance $(X, Y, Z, T, S)$ of 1+3DM, the reduction outputs the instance $(X', Y', T')$ of 3DM obtained as follows.
Create three copies of each of $(X, Y, Z, T)$, with all copied elements distinct.
Label them $(X_1, Y_1, Z_1, T_1)$, $(X_2, Y_2, Z_2, T_2)$, and $(X_3, Y_3, Z_3, T_3)$.
Let $X'=X_1 \cup Y_2 \cup Z_3$, and $Y'= X_2 \cup Y_3 \cup Z_1$, and $Z'=X_3\cup Y_1 \cup Z_2$.
Let $T' = T_1 \cup T_2 \cup T_3 \cup S'$ where
$$S' = \big\{\{s_1, s_2, s_3\} : s \in S\big\},$$
where $s_1$, $s_2$, and $s_3$ are the three copies of element $s$
(that is, $s_i$ is the copy of $s$ that occurs in $X_i \cup Y_i \cup Z_i$).
Given any (1+3D) matching $M$ for $(X, Y, Z, T, S)$, the corresponding matching for $(X', Y', Z', T')$ is obtained by choosing, for every triple $(x, y, z)$ in $M$, the three corresponding triples in $T'$,
namely $(x_1, y_1, z_1)$, $(y_2, x_2, z_2)$,  and $(z_3, y_3, x_3)$,
along with a triple $(s_1, s_2, s_3)$ for each singleton $s$ in $M$.
This correspondence is bijective because of the technical assumption that the chosen singletons determine the matching $M$. $~~~~\Box$


Quantum algorithms based on transforms other than Fourier transforms In Quantum Computation and Quantum Information by Nielsen and Chuang they say that many of the algorithms based on quantum Fourier transforms rely on the Coset Invariance property of Fourier transforms and suggests that invariance properties of other transforms might yield new algorithms.

Has there been any fruitful research on other transforms?

I would like to add some more references to Scott's comment:

Indeed, Clebsch-Gordan transforms (that you can think of as multi-register quantum Fourier transforms) are a useful tool in the design of quantum algorithms for non-Abelian hidden subgroup problems (HSPs).

Clebsch-Gordan transforms were used by Greg Kuperberg and Oded Regev to solve the dihedral HSP in subexponential (yet superpolynomial) time. These quantum algorithms are not efficient, but they have better query complexity than classical algorithms.
Dave Bacon also used Clebsch-Gordan transforms to solve the hidden subgroup problem (HSP) over the Heisenberg group  $\mathbb{Z}_p^2\rtimes \mathbb{Z}_p$ in polynomial time. I can recommend that paper because it is quite clear.

I am also writing to add that we should not forget that both quantum Fourier transforms and Clebsch-Gordan transforms are not always indispensable, even if they can be very useful.

In Shor's algorithm (or even in quantum phase estimation) the Fourier transforms can be replaced with Hadamard tests, therefore only using Hadamard gates instead of Fourier transforms: this trick is due to Kitaev and you can read about it here.
There is yet another efficient algorithm for the HSP over $\mathbb{Z}_p^2\rtimes \mathbb{Z}_p$, by Bacon, Childs, Van Dam, that does not use Clebsch-Gordan transforms. Instead, the algorithm uses a certain type of powerful POVM known as the Pretty Good Measurement.

Of course, this list is probably  incomplete. I hope someone will point out other results that have not yet been mentioned.


Long-lasting errors in computer science This is my first question on the cstheory stack, so don't be too rude if I'm violating etiquette somehow )

As we know, in mathematics even famous mathematicians, superstars and geniuses are doing serious mistakes time to time. For example, both 4-color theorem and Fermat theorem provide us dramatic cases of how even brightest minds can be deluded. It even can take years to prove the incorrectness of some falsy proofs.

My question is - can you provide some outstanding examples of such mistakes in computer science? I don't know, something like "Dr. X has proved in 1972 that it is impossible to do Y in less than O(log n) time, but in  1995 it turned out that he actually was wrong".

An infamous example in computational geometry is the incorrect proof of the Zone Theorem for hyperplane arrangements published by Edelsbrunner, O'Rourke, and Seidel [FOCS 1983, SICOMP 1986].  The proof also appears in Edelsbrunner's 1987 computational geometry textbook.

  Zone Theorem: In any arrangement of $n$ hyperplanes in $\mathbb{R}^d$, the total complexity of all cells intersecting any hyperplane is $O(n^{d-1})$.

The Zone Theorem is a key step in the proof that the standard recursive incremental algorithm to build an arrangement of $n$ hyperplanes in $\mathbb{R}^d$ runs in $O(n^d)$ time.

In 1990, Raimund Seidel discovered that the published proof was incorrect, after being challenged on a subtle technical point by a student in his computational geometry class.  Meanwhile, a huge literature on hyperplane/halfspace/simplex/semialgebraic range searching had been developed, all of which relied on the $O(n^d)$ construction time for arrangements, which in turn relied on the Zone Theorem.  (None of those authors noticed the bug.  Raimund had taught the published "proof" in detail for several years before he was challenged.)

Fortunately, Edelsbrunner, Seidel, and Sharir almost immediately found a correct (and much simpler!) proof of the Zone Theorem [New Results and New Trends in CS 1991, SICOMP 1993].


Papers on relation between computational complexity and algebraic geometry/topology? I was wondering what papers I should read to understand this question

  A unexpected connection to other areas of mathematics such as algebraic geometry or higher cohomology. Perhaps even an area of mathematics not yet developed. Perhaps someone will develop a whole new direction for mathematics in order to handle the P versus NP question.
  -From Fortnow 2002

Another phrasing of the question would be "What papers should I read to create a connection from computational complexity to algebraic geometry / topology?"

I have looked at Geometric Complexity Theory already . Also papers in Topological Quantum Computation which I have read enough papers that I am already familiar with the field. Am I missing anything?

As background, you should definitely study Ben-Or's work on lower bounds, as well as Mulmuley's P vs NC paper.


Complexity of Portal 2 I am studying the complexity of Portal 2 and I would like to know if the problem has been studied before. In particular, I would be interested any reference discussing the complexity of Portal 2 and it being NP-hard/PSPACE-hard and approaches to prove such results.

(An earlier version of this question asked if anyone has shown Portal 2 to be NP-hard.)

Yes, someone has done this.  Portal 2 is at least NP-hard.

My friend created a proof-of-concept map showing that the ability to beat a Portal 2 level implies the ability to solve 3SAT instances:

http://steamcommunity.com/sharedfiles/filedetails/?id=73499175


Novel proof of pumping lemma for regular languages Let $\mathcal{L}$ be the family of all languages over $\Sigma$ satisfying the pumping property of regular languages. Namely: for each $L\in\mathcal{L}$, there is an $N\in\mathbb{N}$ s.t. every word $w\in L$, $|w|> N$ can be written in the form
$ w=xyz$ where:
1. $|y|>0$,
2. $|xy|\le N$,
3. $xy^i z\in L$ for all $i\ge 0$.

It is a simple exercise[1] to prove that $\mathcal{L}$ contains the singleton languages $L=\{\sigma\}$, $\sigma\in\Sigma$, and is closed under union, concatenation, and Kleene star. It is likewise well-known that the family of regular languages is the smallest one that contains the singletons and is closed under union, concatenation, and Kleene star. Conclusion: the regular languages satisfy the pumping property.

Question: has anyone seen this proof in the literature?
[1] Proposed by D. Berend.

Essentially the same argument is made by Andries P.J. van der Walt (1976, Lemma 2.3 and Example 2.9) for the variant of the pumping lemma where $N$ letters are marked and all three of $x$, $y$, $z$ must contain marked letters.  See also Autebert, Boasson, and Cousineau (1978) for more properties of abstract families of languages satisfying this variant of the pumping lemma.


Category-theoretic treatment of diffs, patches and merging? Is there a category of patches that looks roughly like this:

The objects are strings in some base alphabet
The morphisms are edit scripts ("diffs" or "patches") between the strings

I'm interested in these questions:

Is there a categorical notion of minimal edit script? Maybe the category of patches is enriched in PO-Sets?
Is merging of patches the categorical pushout?
How to generalise this from strings to trees (a file system, or an algebraic datatype)?

As pointed by Martin, there is some work on the categorical representation of patches. Mimram and Di Giusto's "A Categorical Theory of Patches" being the most extensive categorical approach to edit-scripts as used by the UNIX diff.

In their sense, you have what you want. The objects are finite sequences of words over an alphabet $L$, seen as a mapping $A : [n] \rightarrow L$, where $[n]$ denotes the set with $n$ elements. An arrow between $A : [n] \rightarrow L$ and $B : [m] \rightarrow L$ is an injective partial increasing mapping $f : [n] \rightarrow [m]$. Injectivity and increasing are there to indicate that copies never cross over each other. You can find all the details on the paper.

Yes, merging is seen as the pushout on the free cocompletion of the above category.
We need the cocompletion to make sure we add merge conflicts to our construction.
It is not the case that a merge always exists.

Onto your second question, there is no categorical notion of minimal edit script for two main reasons.

Edit-scripts come in all shapes and forms. Some authors consider insertions, deletions and copies, some authors like to add substitutions as an operation too.
When you generalize from strings to trees, then, a plethora of other operations become
feasible.
More importantly, though, minimal-cost edit-scripts are not unique.
Take the file $ab$, and write a patch that transforms it into $ba$. What is the
minimal edit script that does this? There are two! Once again, when generalizing into
trees one can find even more situations where a notion of "minimality" is doubtful.

There has been a lot of work on generalizing edit scripts to trees. This has been split in two main bodies of work:

Untyped Trees: Think of s-expressions only. The tree-edit-distance between two
trees is the string-edit-distance between the preorder traversal of said trees. You can check some bibliography by Demaine et al. or Pawlik and Augsten, for example.
Typed Trees: Patches over Abstract Syntax Trees that are guaranteed to preserve
the well-typedness of the object, ie, applying a patch will always yield a valid AST.
Under the typed umbrella, there are less edit operations one can consider. Substitution, for example, doesn't make sense. Nevertheless, there exists a diff over the preorder traversal of the trees by Lempsink et al., which was later extended by Vassena. I am currently focusing on approaches that distance themselves from edit scripts for the very problems I pointed earlier, such as our latest work or some earlier work which tries to take advantage of the structure of the type of the values being "patched".

In either of those cases I have not seen a careful categorical interpretation of tree-structured patches.


How small can a NFA be, compared to the minimal Unambiguous Finite Automaton (UFA) of the same regular language? Unambiguous Finite Automatons (UFA) are special type of non-deterministic finite automatons (NFA).

A NFA is called unambiguous if every word $w\in \Sigma^*$ has at most one accepting path.

This means $DFA\subset UFA\subset NFA$.

Known related automaton results:

  NFA minimization is PSPACE-Complete.
  NFA minimization over finite languages is DP-Hard.
  UFA minimization is NP-Complete.
  There exists NFAs which are exponentially smaller than minimal DFAs.
  (Also - there exists UFAs which are exponentially smaller than minimal DFAs - R B).

The question is: can we find a regular language $L$ such that the there exists a NFA accepting $L$ which is exponentially smaller (state-wise) than the minimal UFA for $L$?
Can this happen for a finite language?

I believe such (finite) $L$ exists, but my proof currently relies on the Exponential Time Hypothesis to hold, and was wondering if someone has a proof which doesn't rely on it.

Also, can someone characterize the set of languages for which such size difference exist?

EDIT: @Shaull gave a nice link to a paper dealing with infinite language. Does anyone know a similar result for a finite language?

There is even a stronger result than your request:

There are exponentially-ambiguous NFAs for which the minimal polynomially-ambiguous NFAs are exponentially larger, and in particular the minimal UFAs.

Check this paper by Hing Leung.


Is there a P/NP-complete dichotomy theorem for natural interesting properties of cubic graphs? It is well known result proved by Holyer that deciding 3-edge colorability of cubic graphs is $NP$-complete problem.

By Vizing's theorem, all cubic graphs are edge colorable using $\Delta +1$ colors. So, the property of 3-edge colorabilty partitions cubic graphs into two infinite sets. Therefore, the property of 3-edge colorability is an interesting natural property of cubic graphs. Another example is the the $NP$-complete problem of deciding whether a cubic graph $G(V, E)$ has a partitioning of $V$ as $T_1 ∪ T_2$ such that $T_1$ and $T_2$ induce trees of equal size (Deciding whether a cubic graph is Yutsis graph). The preceding two example problems demonstrates what I mean by natural interesting property of cubic graphs.

Another natural interesting property of cubic graphs is the problem of deciding the existence of 2-colorable perfect matching in cubic graphs which was proved to be $NP$-complete by Schaefer using his famous dichotomy theorem of CSP's. The problem is to decide the existence of 2-coloring of the vertices of cubic graph such that every vertex has exactly one neighbor of the same color as itself.

I'm interested in a dichotomy theorem that tells us which natural interesting problems on cubic graphs are polynomial-time decidable and which ones are $NP$-complete.

  Is there a P/NP-complete dichotomy theorem for natural interesting properties of cubic graphs?

As it is apparent from the examples, I'm only interested in decision problems where the validity of a solution can be expressed independent of the solution size. I require that the solution has a specific structural property. Bach's post may help in clarifying my motivation. My answer to Bach's post which involves the efficient dominating set problem ( 1-perfect code ) on cubic graphs is a perfect example for natural interesting property of cubic graphs.

Another famous natural interesting property of cubic graphs is being Hamiltonian. Also, it may not be obvious, I'm only interested in natural interesting properties of connected cubic graphs.

EDIT 1-30-2014:  To capture the essence of natural property of cubic graphs, I accept a natural $NP$ property $X$ of cubic graphs where there is natural efficient verifier that verifies a natural interesting relation $(x, c)$ where $x$ is an input instance (i.e. connected cubic graph) and $c$ is a short witness of membership of $x$ in $X$. All witnesses are indistinguishable to the verifier. The validity of witnesses must be decided by running the natural verifier. Such natural $NP$ property must partition the class of cubic graphs into two infinite sets.

Here are some examples of problems which I believe have a reasonable claim of being "natural" (at least, they can be stated concisely) which (when phrased as decision problems) do not appear to be known in P nor known NP-complete. So if you want a dichotomy theorem you either need to be more precise about what you mean by "natural" in a way that excludes examples like these, or you need to look for more precisely defined subclasses of the natural problems (e.g. MSO formulas with the second-order quantification restricted to be existential and outside everything else) for which there might be more hope of a dichotomy.

I've made this community wiki because I think it could be a large list.

Are there evenly many 3-edge-colorings? (Should be $\oplus P$-complete)
Who wins at strings-and-coins? (Might be PSPACE-complete)
What is its list coloring or list edge coloring number? (Might be $\Pi^p_2$-complete)
Is it a unit disk graph? A unit distance graph? (Might be $\exists \mathbb{R}$-complete)
Given two cubic Halin graphs with the same labeled outer face, how few steps does it take to convert one to the other by alternatingly contracting an interior edge and then uncontracting it the other way? (Equivalent to the open problem of computing rotation distance on binary search trees; might also be interesting for broader classes of cubic graphs)