Computer Science

8:06 AM

@babou You mean in the sense that it could fit the reference question? If so, sure, just post an answer there? Or did you want feedback whether I agree?

@DavidRicherby Parameterized complecity resp. kernelization methods kind of go into that direction, don't they? (cc @babou)

For the funs:

34

Q: I want to expose my 5-year-old daughter to boys and girls toys equally, but she just turned her nose up at Star Wars. What do I do?

My aspiration is to give my daughter experiences of boys and girls toys. My background is that I work as a software engineer and had experiences of LEGO, Meccano, programming and sci-fi movies. I don't want to hold that stuff back from my daughter. She has decided at an early age (2) that she i...

gender

Some of the comments are golden. :D

babou

9:59 AM

@Raphael Yes, I was asking whether you consider it worth it as reference answer. Actually, I am still working on this question, to get some more general techniques out of it. So I will do more. But I thought it could fit a new reference question: How do I build a CF grammar for xxx? ... The same could exist also for constructing a PDA. Would it be OK to have a new reference question?

BTW, it is also an interesting example of Curry-Howard isomorphism (to be checked for details with logic experts). The point is that, except in a very small number of cases (I know only two, about FA) the results we use in proving that a language is CF are all constructive. Hence, from (nearly) any proof that a language is CF or regular, we can mechanically extract the grammar or the automaton that will recognize the language.

I wonder whether there is an implemented system that does that. It would be a good educational tool, both for understanding that there is little magic in formal languages and automata, for making general properties (closure) more interesting than direct construction with matchsticks, and also for getting hands-on experience with Curry-Howard. And also to show how pervasive CS concepts can be, and that both a grammar or an automaton may be considered programs.

Possibly an undergraduate project, but it has to be done well.

Nevertheless, Curry-Howard will work well, but may give unpalatable results. There may be simplification techniques, but direct development such as proposed in the answer I submitted to you are still interesting as they may give nicer results. These are all the thoughts that came to me while seeing the same questions repeated over and over (some of them of very limited educational interest imho). This might be more useful than writing yet another textbook.

Raphael

@babou I don't think one specific example qualifies as reference.

@babou I agree. I have more than half a mind to write a (free) book collecting all mechanic and semi-mechanic constructions/proofs you meet in undergrad TCS. It's the time I lack.

@babou I'll leave that tab open for later reading.

Essentially, you want to match closure properties to automata/grammar constructions?

babou

10:28 AM

@Raphael Well, that is true, but my guess is that it is not the only question about constructing a CF grammar. So there may be more to collect from. And asking it as a reference question may attract more interesting answers. Maybe I (or someone else) could just ask it as a question, providing also one or two answers. The only problem is that such a question, intended as a reference, is by nature very open, too open, so that it is usually quickly closed by the site police.

Raphael

@babou What is wrong with the current question?

I think answers discussing how to come up with CF grammars fit there perfectly.

(And then point to the L=L(G) question, if creative steps were involved.)

I would appreciate such. I recall that Rick Decker had a similar answer with some "gadgets". I'd rather close all these "help me build a grammar" questions (without own attempts) as duplicate of a comprehensive reference question.

babou

@Raphael If you have that feeling. That is fine with me. We can always do that. And possibly split in two questions later, if there are many answers that are more centered on actually exhibiting the grammar (without mechanical assistance).

Raphael

@babou Let's do that, then. I think "How to show L is CF?" in one place, and "How to come up with a CFG for L?" in another would be redundant, but maybe I'm wrong.

I was thinking of this one:

1

Q: Converting to CFG from a CFL?

I am trying to learn CFG. Now to make a CFG from a CFL it is really difficult for me. Is there any simple rule or steps so that I can easily find a CFG for a CFL. I am trying to solve one problem for generating a CFG. The Problem statement is to find a CFG that generates the following CFL: $$\{...

formal-languages context-free formal-grammars

So if you start writing something up, you may want to incorporate the stuff from there. (Don't hesitate to use Rick's material as well, he as had plenty of time to do so himself.)

babou

10:46 AM

@Raphael Thanks for the reminder. I wanted to do it, but could not recall where it was.

Raphael

@babou I've read your answer now. It's nice, for the given question, but I think it's too specific to be useful as reference. Well, the numbered list is general enough, but maybe a bit too "fuzzy". The general technique you are proposing is, in essence: since all (?) the proofs of closure properties are constructive, work along closure properties!

babou

@Raphael Well. My feeling is that we should not write books, but symbolic computation systems decorated with educational material. Or possibly have crosslinks between the symbolic system, and an hypertext document explaining the corresponding math. It may actually be a hard task, as one may want smart algorithmics hidden in the system (or both smart and trivial, since students learn the trivial stuff first). But my idea is also how to understand the logic of these proofs.

In that sense, the Curry-Howard aspect should be important.

Raphael

10:59 AM

As such, it should certainly be an answer on the reference question (currently we have "use nesting structure" (similar to what you plan, but not near as comprehensive) and Chomsky-Schützenberger, which can be seen as "ultimate" but harder to use version of your concept.)

@babou I don't know what you mean by "Curry-Howard aspect", sorry. Was that in your discussion with David Richerby above?

@babou My goal would be a book going down to pseudocode for the algorithms, in a building-blocks fashion. Companion implementations might be nice, but also every (at least average) student should be able to implement the algorithm themselves as an exercise.

I don't think, as far as undergrad education goes, much is earned by giving students a full system.

Once you have mastered the material, you want something like that, of course: "here's my language representation derived with smarts; now give me a grammar/automaton/parser". And we have tools like that (mostly from grammars to parsers).

But students should go the long road, because usually their representation will be wrong. And only in doing the mechanical stuff themselves can they see/feel where they went wrong, and iterate.

babou

11:36 AM

@Raphael No relation to my discussion with David Richerby.

The idea is that a system should be organized around a proof assistant for doing proofs about formal automata and languages. Of course, this entails some kind of formalization of a logic for such proof - most likely an incomplete one (according to Gödel). I never used Coq, but I suspect it should be usable for the purpose.

The proof would then be interpreted as steps for constructing the grammar or the automaton for whatever language has been proved to belong to some family. Trios and AFLs would become very natural concepts to use, and closure properties in general. Extracting mechanically the CF grammar or PDA from a proof of CF-ness of the language is just a fairly simple instance of the Curry-Howard isomorphism paradigm. One that is easy to understand intuitively.

This probably extends to many much more sophisticated aspects of computability and complexity. There is a possibility that such a system already exists. How this is then embedded in a proper educational framework is another issue. But I think it is what things should look like in the end.

Raphael

@babou There are multiple concerns. 1) You'll only ever be able to automate the "boring" parts (fully). We want to teach exactly the other parts. Maybe such a system can help teaching the intersting parts, if it's usable enough.

2) Such systems tend to be highly specialised and hard to use. I, too, have never used Coq but I have used Isabelle/HOL. Learning how to use this for proving something non-trivial (and still elementary) took upwards of three months. That's way too much for a tool in teaching.

3) If not useful for teaching (of maybe even if), such a tool will only be built if a) it's an interesting research project in itself (doubtful here, but maybe I lack vision) or b) it promises applications for people with money (don't see that either).

babou

11:56 AM

@Raphael I am aware of your objections. I still think it might be worth spending some time investigating it. Possibly just trying to develop a bit the (possibly elementary) logic for conducting many of the proofs we see here ... just to see how much is required. In a way, that is what is done in the reference questions, but only very informally.

I feel that the paradigm should be usable more simply, if we manage the ergonomic aspects, for simpler contexts than what is aimed at in Coq or Isabelle. Much of the complexity of a system comes from the complexity of the problem space it addresses. Maybe that would only deal with the boring parts ... but the boring parts are precisely what is initially taught, and comes to us as questions.

Raphael

12:57 PM

@babou Hmm, not quite. The boring steps -- transform A to B, simulate set operation x by construction y, ... -- are given in lecture or textbooks. The interesting part is what makes questions end up on Computer Science, namely finding the right sequence of operations. (In particular, this is not computable in general.)

If you can not only implement the "boring" parts in an easy-to-use (and -combine) fashion but also assist in finding this sequence, then you may get somewhere. (Note that that's also what Coq et al. do; they can find simple proofs on their own by enumeration and heuristics.)

That said, a presentation along the lines of "use the toolbox, all you need is such a sequence!" is probably missing from many books/lectures; we can fill a gap there. (I tried to do the same with that algorithm analysis question.)

babou

1:43 PM

@Raphael Finding the right sequence is doint the proof (whether it is CF or Regular). My point is precisely that providing the grammar or the automaton is often not very interesting. But is is often the question being asked. I had only prrof checking in mind, but assisting the proof is another game.

I am always reminded of one thing that impressed me from someone you seem to like, Philippe Flajolet, and his group. He has this small language, such that if you could state your algorithm within the language (obviously not Turing complete), then he would give you the average complexity for free. It is a different context, but always with this idea of compiling sone description into a related piece of information.

Raphael

@babou Yea, Flajolet was all about transfer theorems. Definitely nice, but usually limited.

@babou You mistake me. Finding the grammar is interesting, because it contains non-trivial, creative steps. In the question you linked at the beginning of this conversation, the tool you use is finding a suitable representation so that the grammar follows by construction. So the sequence is not only the proof, it's also essential for getting the grammar. (There are probably easier proofs, too, if you compare with the "unfolded" version of the sequence.)

babou

2:23 PM

@Raphael Actually, in this example, proving it is context-free is a bit simpler than getting to the grammar. However, the grammar I can produce is probably nicer that what I would get by brute force extraction from a simpler CF-ness proof (I think). Not all proofs give the same result.

And one could also consider computing attributes on proof trees that might say something about the appropriateness for extracting a (nice) grammar. I once made a nice example of something similar about bootstrapping compilers, but the details escape me now. The idea was to extract the bootstrap process from a (mechanically produced) proof that it was possible.

Raphael

@babou True. I for one appreciate the conceptual neatness of "construction" proofs; I regularly advocate them. (Mostly for regular languages where you can transform in all directions more freely.)

@babou I think that's a tautology; you can always get a solution/certificate from a constructive proof. (Can't you?) Quantifying "niceness" sounds nice (be-dum-dum-tzz) but daunting.

Bounty!

5:26 PM

4

Q: Algorithm to generate two diffuse, deranged permutations of a multiset at random

Background $\newcommand\ms[1]{\mathsf #1}\def\msD{\ms D}\def\msS{\ms S}\def\mfS{\mathfrak S}\newcommand\mfm[1]{#1}\def\po{\color{#f63}{\mfm{1}}}\def\pc{\color{#6c0}{\mfm{c}}}\def\pt{\color{#08d}{\mfm{2}}}\def\pth{\color{#6c0}{\mfm{3}}}\def\pf{4}\def\pv{\color{#999}5}\def\gr{\color{#ccc}}\let\ss\...

algorithms combinatorics probability-theory scheduling permutations

Raphael

5:38 PM

Oh, a pretty one! Colors!

Raphael

5:57 PM

And a great question, too!

vzn

+1 (herd/ peer pressure) but feel it is "all over the place" (as the expr goes in english) & not too cleanly stated/ presented....

Transcript for