Which packages are ones which employed or employ licences which "require derived works to carry a different name"?
Severall tex/latex file have such a licence, for example/usr/share/texmf/metafont/base/plain.mf has the following licence:
Unlimited copying and redistribution of this file are permitted as long as this file is not modified. Modifications are permitted, but only if the resulting file is not named plain.mf.
Note that this is less troublesome for tex/latex than for many other thing because you can put into a file an information saying that when tex want to read the file "foo" it should use the file "bar" instead.
Did Debian rename them?
Well, as we have the same right than anybody over those file, we don't have the same problem than with firefox. So no we don't (or maybe if we have modified them, I don't know).
Perhaps if there's some historical cases of this happening I can relate to the problem might be clearer?
I've heard that there exist someone who have tried to make a software shipped by debian by giving a licence making the software free as long as it is part of debian, and non-free otherwise. But for what I know, it may be only an urban legend, I've no link nor name.
The fact is that mozilla have given an autorization to Debian to ship a modified firefox under the firefox name. Should we use this authorization, and so use a right that our user doesn't have, or should we ship it under a different name ? See DFSG #8:
License Must Not Be Specific to Debian
The rights attached to the program must not depend on the program's being part of a Debian system. If the program is extracted from Debian and used or distributed without Debian but otherwise within the terms of the program's license, all parties to whom the program is redistributed should have the same rights as those that are granted in conjunction with the Debian system.
Coming up with a proof, on the other hand, is a very hard task (being NP-complete, unless defined in a certain way) and thus usually requires a human (or sometimes, a lot of humans) to work on the problem.
If generating a proof could be NP-complete, it would be a good news. But it is only "half computable", that is there is a program that will find you a proof if there exist one, but won't halt of there is none, and there is no program that will alway stop, telling you if there is, or not a proof. (I've already say it in one of my comment, put simply take the theorem "this turing machine will halt").
Then even if you know that there is a proof, your theorem may use some non NP function, and so to proof your theorem you may need more than an expotancial time.
NP-complete problem are not the most complex problem there is. A NP-complete problem is in NP, and some problem are not in NP.
Then you'd better check your facts... there must be dozens (if not hundreds---erhhh, speaking about checking ones facts:-) ) of systems in which mathematical theorems are routinely proved (HOL, PVS, Coq, Mizar to name just a few)!
Then you'd better check your facts. At least coq, and probably the other too, are proof assistant, and that mean that the help you to wrote your proof, and check that it is correct. But most proof are still mainly done by human.
The only completly automatic prover I know of is prolog, and prolog is not able to soundly use the "not".
To find a proof of a given formula is generaly undicedable, and when you are sure that one exist, you generaly need an exponantial search to find it. Human are still needed to find the good direction in the search.
Well, to find if it exist, or not, a proof to some logical formula is in the same category as the halting problem: You can (if the logic you use is powerfull engought), for each Turing machine, wrote a formula that is provable if and only if the turing machine will halt. But to verify a proof is much easier: is more or less as easy as to verify that a description of a (finite) run of a turing machine is actually the run of the say turing machine, and not something else.
Well, the Coq proof assistant is a program that make semi-automatic proof (semi automatic in the sense that some time it found the proof alone, and often you have to help him to find it). When you have finshid your proof, coq passe it to its proof verifier, and this proof verifier is a (relatively) small function that have been proved by hand (as for some problem linked to the Godel theorem, you cannot proof a theorem prover using it...)
So its mainly the same idea: the proof assistant, and the proof verifier are disconnected (well, the proof assistant may use the proof verifier from time to time, but not the other way arround).
How is Google able to access the paid portions of AFP's site without paying?
AFP is selling content to other site. Those sites put the content they have paid for on the free part of their site. Then Google take those information, and put them for free in google news...
AFP is selling content that you can put on your site to attract a public. But to legaly display this content you have to pay AFP, even if other site are putting this content for free on the web.
Looking at the ocaml code and in particular at the functions that handle the memoizing, I'm wondering how big those memo tables are getting.
Well, this is not the problem : at the end of the execution, his table are empty. The problem is that the memoization is not done. Well after using Hashtable in place of assoc list, and after having realy memoize all function (only one had the problem) I've a good speedup...
I've not read all the ocaml code, but I've seen at the very begining this:
let rec printCells cs =
match cs with
| [] -> ""
| (c::rest) -> (printCell c) ^ (printCells rest);;
And I know that this program will be slow. The ocaml string concatenation operator copy both string each time it is called, and this concatenation work will take O(n^2) step.
You should use the Buffer module, or String.concat:
let rec printCells cs =
String.concat "" (list.map printCell cs)
If there is a lot of those mistake, no wonder it is so slow...
Second, while ignoring users may be a lot more pleasant than listening to their concerns and addressing them
I don't see how "A feature will be implemented if and only if there is a developer who wants to implement it" mean that the developer will ignore users. As you said
Finally, considering user requests can move development in an unexpected direction. Sometimes it's the wrong direction, and I think it's OK to answer a request with "that's a bad idea, and here's why". But sometimes after going in that direction, adding some features, maybe refactoring a bit, you look back and say "why didn't I think of that?" Any community of developers develops blind spots and biases, and sometimes these can be substantial enough for outside input to benefit everyone.
I'm sure lot of developer agreed with this, (I do, even if I'm not a very active developer), but still I will do something only if I want to do it. And this don't alway mean that I want the feature, I may only want to please some of my (few ?) user, or I may belive that my software will be better with this. But won't make me do something I don't want to do if you don't me paid for it.
I remind have read something about grape :
the skin of the grape contain something that
is good for the life, and the preparation of wine
is done in such way that this thing goes into the
wine.
So you can have part of the "wine effect" by
eating every day some grape (with their skin).
If other countrie are going to allow these patents to be violated, there's virtually no incentive for drug companies to develop any new drugs to fight AIDS. So yeah, Brazil and other countries who adopt this tactic may get some short term gains, but long term, it's going to kill AIDS patients.
do you realy believe that rich conutry will do this ? i dont't. I've recently read that 10% of the world population have 85% of the consomation power. Most of this people are in rich country. So until USA and Europe don't do this, most of the incentive for research will still be there.
If the Brazilian government were really interested in the health of their people, why aren't they willing to fund their own R&D and develop their own drugs ?
a little help to know why, just look the GDP per inhabitant
Brazil: 6 480 $ US (1997)
USA: 27 821 $
another question ?
It's what really bug me in this discussion : all this people, living in rich country without seeming to know it. Hey, wake up, the inhabitant of rich country have something like more than 4 time the money of an inhabitant of the Brazil. And can i recall you that their exist country much poorer than that ?
Brazil have a chance : they are sufficiently rich to product their own drug to sell them at a fair price, they would have been stupid to not do it.
You want money to make research for drug ? ask to the rich. I mean us, the inhabitant of rich country
So you should try ocaml + camlp4 :
ocaml is a functional language (like lisp) with a very powerful Modules system and object system, a very strong, and powerful type system. It also have a quick compiler that make very quick program. And camlp4 add to all this a very powerful macro language, very near to the lisp one.
Nope, just the Western governments are coming closer to what Eastern European governments were doing for 50 years - meddling in economic affairs, which should be left to the market,
you really believed so ? as far as i know, most of the governement of every country have "meddling" in economic affairs. What was the new Deal ? What about the way The Japanese have launch their re-industrialisation after the war ? How come on, i believed that the communism was a mistake, but i also believed that the liberalism is a mistake
In france, they are rebuiliding streetcar :
They near completly desappeare in 1966 (only 3 town had still one) but reapeared since 1986 in 8 twon at least (Nantes, Grenoble, PAris, Rouen, Lille, Strasbourg, Saint-Etienne and recently Lyon). They have discover that : there cheaper to build than subway, and better for the environement than bus and car.
Good point, and I agree. Public roads should be funded with tolls or other user fees. People who use choose mass
transit shouldn't be forced to subsidize drivers, and vice versa.
I don't aggred here : as mass transit is better for the whole polpulation (less polution), driver should be forced to subsidize drivers but not vice versa. (And as i use my car and not mass transit, it is not the better choice for my own interest)
Re:I'm a Maths Graduate but ...
on
Does P = NP?
·
· Score: 1
Just to say that the Halting Problem is not solvable at all. There is (or might be i don't remember) problem that are solvable, but not in polynomial time, even on a non-deterministic computer.
When i read this, one thing make me realy react : no, template aren't the only way to do genericity, the ML way of doing it, or better the OCaml way are fare better : they are type safe, whith no duplication of code.
More precisly, it's easier when programing object in ocaml to make generic function than to make non generic one, and all this whith out any lost of efficacity in size or speed.
You've got a good point here, but what can I say...? People research what they like. If you like type systems, it's pretty likely that you'll like functional programming too, since they're so similar. I do believe there is something fundamentally more natural about typing a functional language than an imperative one, though.
the fact is that the type is a kind of proof that the program is valid (for a certain meaning of valid), and it is well known that it is easier to prove automatically something on a functional language than to prove something on a imperative one, so it's more easy to find (or to verify) automatically the type of a program in a functional language
Slashdot Mirror
Severall tex/latex file have such a licence, for example
has the following licence:
Note that this is less troublesome for tex/latex than for many other thing because you can put into a file an information saying that when tex want to read the file "foo" it should use the file "bar" instead.
Well, as we have the same right than anybody over those file, we don't have the same problem than with firefox. So no we don't (or maybe if we have modified them, I don't know).
I've heard that there exist someone who have tried to make a software shipped by debian by giving a licence making the software free as long as it is part of debian, and non-free otherwise. But for what I know, it may be only an urban legend, I've no link nor name.
See DFSG #8:
The realease note make aptitude the prefered wayto upgrade. So do a "aptitude dist-upgrade" preferably to a 'apt-get dist-upgrade".
If generating a proof could be NP-complete, it would be a good news. But it is only "half computable", that is there is a program that will find you a proof if there exist one, but won't halt of there is none, and there is no program that will alway stop, telling you if there is, or not a proof. (I've already say it in one of my comment, put simply take the theorem "this turing machine will halt").
Then even if you know that there is a proof, your theorem may use some non NP function, and so to proof your theorem you may need more than an expotancial time.
NP-complete problem are not the most complex problem there is. A NP-complete problem is in NP, and some problem are not in NP.
Then you'd better check your facts. At least coq, and probably the other too, are proof assistant, and that mean that the help you to wrote your proof, and check that it is correct. But most proof are still mainly done by human.
The only completly automatic prover I know of is prolog, and prolog is not able to soundly use the "not".
To find a proof of a given formula is generaly undicedable, and when you are sure that one exist, you generaly need an exponantial search to find it. Human are still needed to find the good direction in the search.
Well, to find if it exist, or not, a proof to some logical formula is in the same category as the halting problem: You can (if the logic you use is powerfull engought), for each Turing machine, wrote a formula that is provable if and only if the turing machine will halt. But to verify a proof is much easier: is more or less as easy as to verify that a description of a (finite) run of a turing machine is actually the run of the say turing machine, and not something else.
Well, the Coq proof assistant is a program that make semi-automatic proof (semi automatic in the sense that some time it found the proof alone, and often you have to help him to find it). When you have finshid your proof, coq passe it to its proof verifier, and this proof verifier is a (relatively) small function that have been proved by hand (as for some problem linked to the Godel theorem, you cannot proof a theorem prover using it...)
So its mainly the same idea: the proof assistant, and the proof verifier are disconnected (well, the proof assistant may use the proof verifier from time to time, but not the other way arround).
AFP is selling content to other site. Those sites put the content they have paid for on the free part of their site. Then Google take those information, and put them for free in google news...
AFP is selling content that you can put on your site to attract a public. But to legaly display this content you have to pay AFP, even if other site are putting this content for free on the web.
Well, this is not the problem : at the end of the execution, his table are empty. The problem is that the memoization is not done. Well after using Hashtable in place of assoc list, and after having realy memoize all function (only one had the problem) I've a good speedup...
You should use the Buffer module, or String.concat:If there is a lot of those mistake, no wonder it is so slow...
I don't see how "A feature will be implemented if and only if there is a developer who wants to implement it" mean that the developer will ignore users. As you said
I'm sure lot of developer agreed with this, (I do, even if I'm not a very active developer), but still I will do something only if I want to do it. And this don't alway mean that I want the feature, I may only want to please some of my (few ?) user, or I may belive that my software will be better with this. But won't make me do something I don't want to do if you don't me paid for it.
I remind have read something about grape :
the skin of the grape contain something that
is good for the life, and the preparation of wine
is done in such way that this thing goes into the
wine.
So you can have part of the "wine effect" by
eating every day some grape (with their skin).
If other countrie are going to allow these patents to be violated, there's virtually no incentive for drug companies to develop any new drugs to fight AIDS. So yeah, Brazil and other countries who adopt this tactic may get some short term gains, but long term, it's going to kill AIDS patients.
do you realy believe that rich conutry will do this ? i dont't. I've recently read that 10% of the world population have 85% of the consomation power. Most of this people are in rich country. So until USA and Europe don't do this, most of the incentive for research will still be there.
If the Brazilian government were really interested in the health of their people, why aren't they willing to fund their own R&D and develop their own drugs ?
a little help to know why, just look the GDP per inhabitant
Brazil: 6 480 $ US (1997)
USA: 27 821 $
another question ?
It's what really bug me in this discussion : all this people, living in rich country without seeming to know it. Hey, wake up, the inhabitant of rich country have something like more than 4 time the money of an inhabitant of the Brazil. And can i recall you that their exist country much poorer than that ?
Brazil have a chance : they are sufficiently rich to product their own drug to sell them at a fair price, they would have been stupid to not do it.
You want money to make research for drug ? ask to the rich. I mean us, the inhabitant of rich country
May be you are talking about SML, but in Ocaml, it's very easy :
let file = open_out "file" in
fprintf "int : %i; string : %s" 12 "eza"
it doesn't seem that difficult...
(i believe that it is very similar in SML)
So you should try ocaml + camlp4 : ocaml is a functional language (like lisp) with a very powerful Modules system and object system, a very strong, and powerful type system. It also have a quick compiler that make very quick program. And camlp4 add to all this a very powerful macro language, very near to the lisp one.
In france, they are rebuiliding streetcar : They near completly desappeare in 1966 (only 3 town had still one) but reapeared since 1986 in 8 twon at least (Nantes, Grenoble, PAris, Rouen, Lille, Strasbourg, Saint-Etienne and recently Lyon). They have discover that : there cheaper to build than subway, and better for the environement than bus and car.
Just to say that the Halting Problem is not solvable at all. There is (or might be i don't remember) problem that are solvable, but not in polynomial time, even on a non-deterministic computer.
When i read this, one thing make me realy react : no, template aren't the only way to do genericity, the ML way of doing it, or better the OCaml way are fare better : they are type safe, whith no duplication of code. More precisly, it's easier when programing object in ocaml to make generic function than to make non generic one, and all this whith out any lost of efficacity in size or speed.