12:00 AM
Meh, I just missed the rep cap by 5 rep today

I'll not be very active this weekend. But maybe I have an idea for a new question outside of my domain.

@AlextenBrink By the way, I believe I can prove that heap automata do accept a subset of CSL.
@AlextenBrink Where do you see that?

Do you have any specific subset in mind?

@AlextenBrink No, only a general simulation proof.

I have gained 195 rep today, and it says 'yesterday' now, so I've just missed it - you can find it on the reputation page on your user page.

12:02 AM
@Gilles: by the way I spent a few hours on your λ-calculus question (I should know this stuff) but couldn't find anything interesting...

@Raphael What I mean is, proving it accepts { a } already proves it accepts a subset of CSL, which is not a very interesting subset

@AlextenBrink Hm, 200 yesterday and 217 the day before; I guess 200 is not the cap?

Accepted answers and rep through edits do not count towards the cap

@AlextenBrink Misunderstanding: I mean HAL \subseteq CSL

@StéphaneGimenez !
I should know this stuff too, but I haven't practiced for a few years

12:04 AM
$Raphael As I proved that HAL \subseteq L and CSL = NLINSPACE, HAL \subseteq CSL is immediate I mean, HAL \subseteq NL Unless you are not convinced by my proof (which may very well be wrong) Well yea, but I did not buy this proof 100%. Even if, I like to do the CSG simulation. On the topic of active users, I see a few users on the list that have 100 rep but are quite active on CSTheory I think the crucial bit is that part about union elimination needing to happen in the context. That's a dissymmetry with intersection, which can use a subtyping presentation with the usual rule$\dfrac{x : T \quad T \le T'}{x : T'}$Guys, got to go to bed now. Nice talking to you in real time! See you later today. That question popped into my head suddenly, when I thought intersection types are a classic object of study and union types rarely come up, and why would that be when they should be dual in some way 12:08 AM @Raphael Good night Thanks, you too. I still want to read the original papers by Pierce before I let the matter rest Yes λ-calculus corresponds to intutionistic logic, there is no complete duality That's why I suggested to introduce call/cc which would make it closer to classical logic. But I still don't really understand how unions could be useful to type more terms. Ok time to go to bed for me too. Good night. Well this room picked up in my absence. And died off as soon as I got here, of course. @Raphael 200 is the cap from votes, things like accepts and bounties don't count towards it. 12:56 AM 0 I want to know if the following problem is decidable and how to find out. Every problem I see I can say "yes" or "no" to it, so are most problems and algorithms decidable except a few (which is provided here)? Input: A directed and finite graph G, with v and u as vertices Question: Does a p... 1:51 AM 0 There are many ways to define the Kolmogorov-Complexity, and usually, all these definitions they are equivalent up to an additive constant. That is if$K_1$and$K_2$are kolmogorov complexity functions (defined via different languages or models), then there exists a constant$c$such that for ev... 2:05 AM 1 The live refresh feature doesn't take MathJax into account. Here's a screenshot of the Mathematics after clicking on “$n$questions with new activity”: I saw the same effect on the CS private beta. I'm running Chrome 17.0.963.65 (stable) on Linux. I posted on MSO and not CS.Meta because it happens on other sites @ComputerScience suggested edit (meaningful title) 2:48 AM 0 We are now in the third day of private beta with a couple of questions. That is great. However, most of questions here so far are about CS theory, which already have a full-grown site. The overlap is not a problem per se and is expected. However, if we continue this way, I fear that we could not... 3:46 AM 0 I hereby propose to ban soft-question, as well as should it arise big-picture and any other similar meta-tag. First, let me reiterate the main generic arguments in the blog post. These tags do not indicate the topic of the question, they indicate its breadth or depth. They cannot work as the sol... 2 Consider the following protocol: The Client's "time" is skewed with an unknown constant$u$. Assume message travels from the Client to Server within$C_1$time, and from Server to Client within$C_2$time (and these constants don't change with time). Initially, the Server sends an empty mess... Oh hey, this site is up now? Can someone put either Ran or me out of our misery? I get the impression that Ran's method can't work 1 hour later… 5:00 AM @Gilles I tend to agree. BTW, should the erroneous answer be deleted? 5:37 AM 0 I am starting a personal bibliographic research on type-checking algorithms and want some tips. What are the most commonly used type-checking algorithms and strategies? Given some strongly static typed languages with complex typing systems like C++, Java 5+ or Scala, what are the type-checking al... 0 In computer networking and high-performance cluster computer design, network topology refers to the design of the way in which nodes are connected by links to form a communication network. Common network topologies include the mesh, torus, ring, star, tree, etc. These topologies can be studied an... 2 hours later… 7:33 AM @Kevin thanks for clarifying. @Mana Jup, welcome! 7:53 AM 1 In database normalization, 1NF (no multivalued attributes), 2NF (all non-PK attributes depending only on PK attributes) and 3NF (all non-PK attributes depending on all of the PK attributes) are widely known. The 4NF (no part of the PK depending on other part of the PK) is less known, but still re... 1 hour later… 8:59 AM @RanG only if you think it's wrong. Maybe my proof that it can't be done this way is wrong and it's preventing me from understanding how it can be done. The patent Raphael cites would be subject to the same objection, I think; I haven't yet had time to read it to understand how it claims to do the job. 4 hours later… 1:04 PM 0 Someone I know is planning on implementing a text editor in the near future, which prompted me to think about what kind of data structures are fast for a text editor. The most used structures are apparently ropes or gap buffers. Van Emde Boas trees are just about the fastest priority queues arou... 1 Consider decision problems stated in some “reasonable” formal language. Let's say formulae in higher-order Peano arithmetic with one free variable as a frame of reference, but I'm equally interested in other models of computation: Diophantine equations, word problems from rewriting rules using Tu... 1:31 PM 0 Which of the following statements is correct? sufficient and necessary conditions about regularity of a language exist but not discovered yet. There's no sufficient and necessary condition about regularity of a language. Pumping lemma is a necessary condition for non-regularit... 2 hours later… 3:51 PM 0 We know from this paper that the minimum number of clues to solve a valid sudoku puzzle is 17. Can all valid sudoku puzzles be specified in 17 clues? If not, what is the minimum number of clues that can completely specify every valid puzzle? 1 hour later… 5:15 PM 1 Given a language$L$, define the length set of$L$as the set of lengths of words in$L$: $$\mathrm{LS}(L) = \{|u| \mid u \in L \}$$ Which sets of integers can be the length set of a regular language? 1 Specifying any arbitrary 9x9 grid requires giving the position and value of each square. A naïve encoding for this might give 81 (x, y, value) triplets, requiring 4 bits for each x, y, and value (1-9 = 9 values = 4 bits) for a total of 81x4x3 = 972 bits. By numbering each square, one can reduce t... 6:09 PM 1 Consider unlabeled, rooted binary trees. We can compress such trees: whenever there are pointers to subtrees$T$and$T'$with$T = T'$(interpreting$=$as structural equality), we store (w.l.o.g.)$T$and replace all pointers to$T'$with pointers to$T$. Give an algorithm that tak... 1 hour later… 7:15 PM @Raphael @RanG Have you tried reading that patent about clock synchronization? I get to the point where they've done a round trip in each direction, and then there seems to be a sign error: the text claims$\theta_A = \theta_B$, but if you perform the round trip in different directions, that should be$\theta_A = - \theta_B$, and the equations crumble away. Or am I being dense? 7:34 PM @ComputerScience Should I answer this question? I have a good idea of what I expected an answer to say, but it feels a bit cheesy 1 hour later… 8:51 PM This is the moment you wish sudokus used digits 0-F. Storing 1-9 into 4 bits can be irritating :-) By the way, grouping by 5 digits is quite decent :-) @jmad or by 9, you can store 9! in 19 bits and the decoding isn't too bad how do you group by 5 digits anyway? @Gilles sure, I just looked at the bits needed to store n digits, with n=17,18,.. and 5 was not bad I guess it is because log(9^5)/log(2)≈15.85 is close to 16. Sure, you can do it with grouping by 9 digits but it's not fun. (at maybe not a great idea for 17..22 clues) @jmad you aren't taking advantage of the non-repeat conditions though But anyway, it's always more space-efficient to encode into a single integer. what do you mean by non-repeat conditions? @jmad in a Sudoku puzzle, the digits don't repeat inside a line, column or 3x3 square If you take advantage of one of them, you can encode the digits using 9!^9 possibilities rather than 9^81 9:04 PM Oh that, right. I was talking about the "81+4n bits" solution which can be transformed into "81+log(9^n)/log(2) bits" but that is not very interesting 9:48 PM$81+log(9^n)/log(2) \$
Huh, very neat. It works.

hello Gigili
hey, I thought of a follow-up “puzzle” to your question on decidability of a finite graph problem
Do you think that every problem on finite graphs is decidable? After all, if the graph is finite…

I think that covers part of the problem I had
'Ello BTW.
By what they said there, when it's finite it's decidable
But let me try to find a counterexample
The graph is finite, so it's possible to write an algorithm for every problem and you can say yes or no to it
/methinks

there's a subtlety here. Don't feel bad if you don't get it at once.
If the solution space is finite, then the problem is trivially decidable
But you can have an infinite solution space even if the problem is about a finite object
That's why in my answer I first dealt with cycles: there is an infinite number of paths in a graph that has a cycle
but for that specific problem the cycles turned out to be irrelevant, because if there's a solution there's a cycle-free solution
so “is there a path from u to v” is equivalent to “is there a cycle-free path from u to v”
and the latter has a finite solution space so it's decidable
Now consider the decision problem “does this program terminate?”
A program is a finite construct, but there is no finite solution space to explore, and the problem is well-known to be undecidable

Like what?

10:03 PM
@Gigili sorry, what like what?

An undecidable problem, there's none about finite graphs, right?

@Gigili no, there are, but they tend not to be obviously about graphs
Consider the following problem: write the size of the graph in base 256, and interpret this as a Haskell program; does the Haskell program terminate?
This is technically a decision problem about a graph, and it's undecidable
Obviously it's not a natural way to phrase this problem

Yes and it's more about programming languages than graphs
Thank you, it's clearer now.
And I really got offended by your comment, "Are you sure this is the question you meant to ask?".
But seems you use the word "obviously" so often

@Gigili I'm sorry if you got offended, that was absolutely not intended
At first I thought you might have made a mistake in the problem statement
Then I reevaluated my interpretation of your question
Over the Internet it's difficult to know where the other guy is coming from, what his unstated assumptions are

Yes, I wanted to ask if there's a problem and the given information is not enough to solve it, is it undecidable?
@Gilles Very true.

10:13 PM
@Gigili I don't understand what that can mean. Normally you have complete information, the problem is to extract what you want from that pile of information
I'm sure people have studied partial-information settings in a way that resembles decidability theory, but that would have other notions beyond decidable/undecidable

Right, I meant if a piece of information is missing, for instance "finite" in my question

@Gigili if you remove the assumption that the graphs are finite, you need to explain what graphs you're considering
otherwise the question is simply ill-formed
There are surely classes of infinite graphs where connectivity is decidable
For example, the class of graphs that are strongly connected along finite paths ;)

Aha, so you cannot call it "undecidable" in that case?