<cedricshock>
We used it to take Rice's theorem to an ML program to take the ML program to a turing machine.
<Smerdyakov>
So? What connects "trivial" TM's to "trivial" theorems?
<cedricshock>
I also have the solution to P(!?)=NP, given two seemingly obvious, but so far unproven by me, lemmas.
<Smerdyakov>
See above.
<cedricshock>
Now it is a turing machine that looks at other turing machines and determines about them "You do not say anything non-trivial about other turing machine programs."
<Smerdyakov>
So? There are pretty widely understood definitions of "trivial" for the cases of TM's and proofs.
<cedricshock>
Oh darn. Argument fell through again.
<Smerdyakov>
They are very different definitions, though.
<cedricshock>
I agree.
<Smerdyakov>
You seem to be claiming a connection between the definitions through the C-H I.
<Smerdyakov>
I don't see that connection at all.
<cedricshock>
I'm not claiming a connection in the definitions of trivial. I'm claiming, given Rice's definition of trivial, his theorem is trivial.
<Smerdyakov>
No. You're claiming that the corresponding TM is trivial.
<Smerdyakov>
"Trivial" is overloaded here.
<cedricshock>
I do not claim that I think little of his theorem - I see all kinds of theorems and his stuck in my head enough for me to think of this.
<cedricshock>
This has turned into a #haskell type discussion.
<Smerdyakov>
That's irrelevant. You have not said anything to show that his theorem is trivial.
<Smerdyakov>
You have explained how a _compilation_ of it to another domain is trivial.
<Smerdyakov>
That is not the same thing.
<cedricshock>
Here we go:
<cedricshock>
TMs are a supperset of ML
<Smerdyakov>
No.
<Smerdyakov>
There is a compilation of ML to TM's.
<Smerdyakov>
Different concept.
<cedricshock>
Anything an ml program can do a tm can do.
<Smerdyakov>
OK.
<cedricshock>
Now it is a turing machine that looks at ML programs and determines about them "You do not say anything non-trivial about turing machines."
<cedricshock>
So we have a turing machine that is allowed to make this statement.
<cedricshock>
And Rice's theorem is an ml program.
<cedricshock>
It is an ml program that determines things about turing machines. So what it determines must be "trivial"
<Smerdyakov>
Ah. Now I see your misunderstanding.
<Smerdyakov>
No, it is not an ML program that determines things about TM's.
<Smerdyakov>
It is an ML program that builds proofs.
<Smerdyakov>
Which is stricly more work.
<Smerdyakov>
The type of the program is:
<cedricshock>
So it is an ML program that builds proofs that then say things about turing machines. So it is an ML program that is going to make a statement about turing machines.
<Smerdyakov>
forall M : TuringMachine. DoesntDecideAnythingInteresting(M)
<Smerdyakov>
The type is _not_:
<Smerdyakov>
forall M : TuringMachine. bool
<Smerdyakov>
_That_ corresponds to a trivial theorem.
<cedricshock>
So either the program can't halt, the program contradicts itself, or its "trivial.
<Smerdyakov>
No, Rice doesn't say anything about building proofs. His theorem doesn't apply here.
<cedricshock>
Ok, we can rework this whole problem for you.
<Smerdyakov>
It's not so much building proofs, really. It _is_ a proof, with no runtime existence to be examined.
<cedricshock>
Rice's theorem does say somethign about building proofs.
<Smerdyakov>
See above. I removed references to "building."
<cedricshock>
It says something about turing machines that look at other turing machines that are building proofs and determine things about them.
<Smerdyakov>
That's OK. No proof-building is involved here.
<cedricshock>
You're the one that introduced proof-building.
<Smerdyakov>
Yup, and I retracted it.
<cedricshock>
Fine - now you give me a shortcut:
<cedricshock>
It says somethinf about turing machines that are proofs and determines something about the,
<cedricshock>
I already know how you'll counter this.
<cedricshock>
It's still about turing machines.
<Smerdyakov>
Well, it wasn't a readable line, so I don't have anything to say about it.
<cedricshock>
That f is an m and the comma also is
mrsolo_ has quit [Read error: 110 (Connection timed out)]
<Smerdyakov>
No, Rice doesn't say anything about proof interpretations of TM's.
<cedricshock>
Any famous theorem with this property: Existence of polynomial time problem of order n implies existence of plynomial problem of order n+1 that can't be done in an amount of time on an order less than n+1?
kinners has joined #ocaml
<Smerdyakov>
Yes.
<cedricshock>
I need to do typing lessons again. I'm getting sloppy.
<cedricshock>
What's it called?
<Smerdyakov>
A polynomial hierarchy theorem
<cedricshock>
What is the simplest expression of the time complexity of an NP problem?
<cedricshock>
Can we safely say that they can be done on the order of e^x?
<Smerdyakov>
I don't think I follow you. Are you asking for a definition of the class NP? (And is this related to the still unresolved question we were just discussing?)
<cedricshock>
This is not related to the unresolved problem we were discussing.
<Smerdyakov>
Well, I want to finish the previous problem first.
<Smerdyakov>
How does can you argue using the TM that corresponds to the ML program of a proof of Rice to show that Rice is trivial?
<cedricshock>
I believe my ability to express myself in your jargon is insufficient to convey to you that the definition of triviality used in Rice's theorem (can be completed in a finite number of steps, or on a finite tape) can be aplied to a theorem, specifically Rice's to show that it is trivial. However this definition of trivial is not the usual definition of trivial for proofs, and would apply to all proved proofs.
<Smerdyakov>
The thing is that the TM corresponding to this ML program is not valid.
<Smerdyakov>
It doesn't return any result.
<Smerdyakov>
(And the language is really ML with dependent types, not any ML in wide use today)
<Smerdyakov>
To be concrete, say we mean CiC instead of ML everywhere above.
mrsolo_ has joined #ocaml
<Smerdyakov>
There is no sensible compilation strategy from Coq terms to Turing Machines that decide languages.
<cedricshock>
Why are we interested in turing machines to begin with?
<Smerdyakov>
That's what Rice was proved about.
<cedricshock>
I know. Why bother proving things about turing machines?
<Smerdyakov>
Where do I bother doing that?
<cedricshock>
You don't. Rice does.
<Smerdyakov>
OK....
<Smerdyakov>
Every CIC program terminates. Did you know that?
<Smerdyakov>
So Rice about CIC programs wouldn't hold.
<cedricshock>
No. I did not know that.
<cedricshock>
That is very interesting.
<Smerdyakov>
A full C-H I is between proofs and terms of a _strongly_normalizing_ (always terminating) language.
<cedricshock>
So the analog of Rice's theorem to _strongly_normalizing_ languages would be trivial by the regular way we talk about trivial proofs.
<cedricshock>
Whereas Rice's theorem about turing machines is non-trivial
<cedricshock>
but can be compiled into a trivial turing machine.
<Smerdyakov>
OK. So I hope now we agree that the C-H I can't be used in any interesting way with Rice's Theorem as you originally proposed?
<cedricshock>
A depressed, trivial turing machine that says about itself, "No :("
<cedricshock>
Ok, so the statement "There is a one-to-one, onto correspondence between proofs and programs" is quite a little misleading, in particular when dealing with non-terminating programs.
mrsolo_ has quit [Read error: 60 (Operation timed out)]
<Smerdyakov>
Right. I should have said "CIC programs" or similar.
<cedricshock>
If we were to prove such a nice and general result, then Rice's theorem would show itself to be "trivial". As it is C-H I is not enough.
<Smerdyakov>
And, since we know Rice's Theorem isn't trivial, we know there is no such result. :-)
<cedricshock>
So can NP problems be done on the order of e^x?
<cedricshock>
Un-unh: If you want to claim that you've got to show me that Rice's theorem isn't trivial.
<Smerdyakov>
I'm guessing not. There's probably a hierarchy theorem one can use to find a counterexample.
<cedricshock>
I'm not looking for a counterexample. I'm looking for an example.
<Smerdyakov>
Is x the input size in the above?
<cedricshock>
Yes.
<Smerdyakov>
What would "an example" of this be?
<cedricshock>
What I'm looking for is the time complexity in which we know a NP problem can be solved.
<Smerdyakov>
EXPTIME
<cedricshock>
s/a/an and by an I just mean any one of them
<cedricshock>
EXPTIME being the times like e^x, orthe times like f^x where f is something else?
<Smerdyakov>
Yup.
<Smerdyakov>
Of course, if P = NP, then e^x is certainly enough. :-)
<cedricshock>
Why is that?
<Smerdyakov>
Then every NP problem is solvable in polynomial time, and every polynomial is dominated by e^x.
<cedricshock>
Ok.
<cedricshock>
Good.
<cedricshock>
I have a proof that P >= NP. It's about half a page long. Where should I send it?
<Smerdyakov>
What is ">=" here?
<cedricshock>
Greater than or equal to. That is there exist polynomial time problems, that connot be done on any smaller order of polynomial time that will strictly take at least as long to execute as the simplest NP problem.
<Smerdyakov>
The simplest NP problem is the empty language.
<Smerdyakov>
Any algorithm takes at least as long as the best solution.
<cedricshock>
"simplest NP problem" is a misnomer
<cedricshock>
take at least as long to execute as (an NP problem that takes the shortest known execution time)
<Smerdyakov>
And that problem is the empty language, in every case.....
<cedricshock>
Ok. Fine. As long as it takes at least (1+epsilon)^x time, where epsilon > 0 and x is whatever we call the growing thing.
<Smerdyakov>
No. It takes, say, 1 time.
<Smerdyakov>
It immediately outputs "NO."
<cedricshock>
That is not NP. That is a case of an NP problem. That's like the problem of weather or not I can fit 0 files with sizes [] onto 1 disk of size 2.
<Smerdyakov>
The empty problem is in NP.
<cedricshock>
Yes. It is also in P.
<Smerdyakov>
Yup. So what is your point?
<cedricshock>
I'm saying given some class of problems in NP characterized by some number x, such that the complexity of being able to complete one is bounded above by f^x, f > 1, then I can produce a polynomial time problem which is also characterized by x so that its complexity is like g(x) and g(x) > f^x for all x >= 0.
salo has quit []
salo has joined #ocaml
<cedricshock>
I can prove P >= EXPTIME. That's what I'm saying. Now I've said too much.
<Smerdyakov>
What does it mean: "class of problems in NP characterized by some number x"
<Smerdyakov>
A "problem" is a language, not a particular input.
<cedricshock>
Ok Fine. I get it now.
<Smerdyakov>
OK.... so are you still claiming to have some interesting result?
<cedricshock>
No Id don't
<cedricshock>
Yes. I have a very interesting result.
<Smerdyakov>
OK. What is your result, using the correct definition of "problem"?
<Smerdyakov>
And use 'n' instead of 'x', and you get to assume it's input size, with standard conventions. :P
<cedricshock>
I can prove there are only problems solvable in time polynomial to n that take longer to solve than an NP-complete problem for all n.
<cedricshock>
Remove the word only
<Smerdyakov>
What do you mean "longer to solve than an NP-complete problem"?
<Smerdyakov>
You mean that, for every problem in P, you can find some less complex problem in NP?
<cedricshock>
No, that means for some proplem in P I can find a less complex problem in NP.
<Smerdyakov>
That's easy.
<Smerdyakov>
The P problem is "does the input begin with 1."
<Smerdyakov>
The NP problem is the empty language.
<cedricshock>
No no no.
<cedricshock>
Sorry.
<cedricshock>
I can prove for all np in NP there exists p in P such that P is at least as hard as NP. (Adopting your view of sets of solutions instead of my view of functions of n).
<Smerdyakov>
Do you mean "... such that p is at least as hard as np"?
<cedricshock>
yeah. sorry. should have used diferent symbols.
<Smerdyakov>
In other words, where Tp(n) is the running time function of p and Tnp(n) the running time function of np, Tnp(n) = O(Tp(n)) ?
<Smerdyakov>
Or just Tnp(n) <= Tp(n) for every n?
<cedricshock>
No Tp(n) >= Tnp(n) for all n.
<Smerdyakov>
Oh, and we are talking about the most time efficient algorithm for each problem here, right?
<cedricshock>
No. The most time-efficient algorithm for the Tp.
<Smerdyakov>
That doesn't make sense.
<Smerdyakov>
Tp is a function that computes running time. Why would we want an algorithm to compute it?
<cedricshock>
I don't care about the Tnp as long as it doesn't have the order of time of its execution changed.
<Smerdyakov>
You can't talk about "the running time of problems."
<Smerdyakov>
You can only talk about the running time of algorithms.
<cedricshock>
So I'll just say yes. The most efficient time.
<Smerdyakov>
OK. We take the most asymptotically efficient algorithm for each problem.
<cedricshock>
yes. But for np we don't need to show its the best, just don't give me one artificially inflated from where they arecurrently at.
<Smerdyakov>
And the most efficient p algorithm always takes at least as long as the most efficient np algorithm. Correct?
<cedricshock>
Yes
<Smerdyakov>
OK. Now why is this interesting?
<cedricshock>
Why wouldn't it be?
<Smerdyakov>
Well, let's see. If Tp dominates Tnp, then Tnp(n) = O(Tp(n)).
<Smerdyakov>
Since p \in P, p has a polynomial time solution.
<Smerdyakov>
So Tp(n) is O() of some polynomial.
<cedricshock>
Yes
<Smerdyakov>
Transitively, Tnp(n) runs in PTIME.
<cedricshock>
Yes
<Smerdyakov>
So NP \in P.
<cedricshock>
You are skipping obvious steps. Yes.
<Smerdyakov>
OK. So clearly your proof is wrong. :)
<cedricshock>
That's why I was asking why wouldn't it be?
<Smerdyakov>
Most people believe that NP is a strict superset of P, because no one has proven otherwise yet.
<cedricshock>
That's why I said my proof showed "P>=NP". I already know that "P<=NP".
<Nutssh>
NP subsumes P, so any P time algorithm is always in class NP.
<Smerdyakov>
I believe cedricshock is claiming to have proven P = NP.
<Smerdyakov>
By way of NP \subseteq P.
mrsolo_ has joined #ocaml
<cedricshock>
My proof, with a correct interpretation would show two things:
<cedricshock>
First that P includes NP, and secondly that no NP-complete problem will ever be solved in "polynomial" time.
<Nutssh>
Whats the proof that NP \subseteq P?
<cedricshock>
Actually it doesn't prove the second thing
<Smerdyakov>
P includes NP is what I said you meant: "NP \subseteq P"
<Smerdyakov>
And I am quite confident that you haven't proven that.
<cedricshock>
I know that's what you said. I was repeating it for clarity. Sorry.
<cedricshock>
It actually shows that a class of problems like what we attribute to NP-complete problems will exist, and will be in P, but will not run in "polynomial" time.
<Smerdyakov>
Every problem in P runs in polynomial time, by definition.
<Smerdyakov>
So, at best, you've found an inconsistency in your logical system, which is sounding more and more likely. :P
<cedricshock>
It's a proof that P = NP and at the same time a proof that something like NP-complete problems exist, with very similar properties.
<Smerdyakov>
At any rate, you haven't proved P = NP, and if you'd like our help finding where your proof goes wrong, then here we are!
<cedricshock>
Ok. Remove my last shred of doubt and I'll write it this weekend and submit it somewhere so the world can defame me as a cook.
<Smerdyakov>
LOL. I guess you just can't get that shrimp casserole right, eh?
<Smerdyakov>
(To be defamed as a cook)
kinners has quit [Read error: 110 (Connection timed out)]
<Smerdyakov>
Anyway, in case you don't know, here's the URL on how to claim $1 million for proving P = NP:
<cedricshock>
Is there a polynomial heirarchy theory that will give me polynomial time problems that can't be done faster than, for one fa(n) = n^a (polynomial) and for the next fa+1(n) = n^(a+1) + fa(n)?
<cedricshock>
No one will give me $1 million for this.
<Smerdyakov>
Someone will give $1mil to anyone proving P = NP or P <> NP.
<cedricshock>
I know that.
<Smerdyakov>
I don't understand your question.
<salo>
does anyone see my message on caml-list regarding building ocaml on mips/irix ? is there commonly a greater than 8 hour lag between posting and distribution on the list?
<Nutssh>
cedricshock: I don't know of any.. Minimum-time proofs are *notoriously* hard to do.
<Smerdyakov>
Nutssh, on the contrary, there are lots of polynomial time separation theorems.
<Smerdyakov>
Nutssh, O(n^i) and O(n^(i+1)) are provably distinct for any i, for example.
<Nutssh>
Yes.
<cedricshock>
Sorry. Can we show that there is a family of polynomial time problems, each taking time an the order of fa(n) = n^a where fa+1 = something_on_order_of(n^(a+1)) + fa(n)?
<Nutssh>
What I meant was proving that a non-trivial problem cannot be done faster than O(n^i)? Eg, factoring, graph coloring, etc.
<cedricshock>
Nutssh: Yes. That is hard to do.
<Smerdyakov>
Nutssh, these hierarchy theorems show the existence of such problems. They aren't natural problems, though.
* Nutssh
will buy that Smerdyakov.
<Smerdyakov>
cedricshock, what do you mean by "a family of problems"?
<cedricshock>
Nutssh: But we can construct artificial problems with the purpose of making them difficult.
<Smerdyakov>
cedricshock, do you mean a family of problems indexed by the 'a' parameter you used?
<Smerdyakov>
cedricshock, so we have Problem 1 running in O(f1(n)), Problem 2 running in O(f2(n)), etc.?
<Nutssh>
Smerdyakov: How are those heirchies built? (Got the name of one of the heirarchy theorems for me to look up?)
<cedricshock>
Any famous theorem with this property: Existence of polynomial time problem of order n implies existence of plynomial problem of order n+1 that can't be done in an amount of time on an order less than n+1 + the amount of time it would have taken to solve the earlier simpler problem, which was on the order of (whatever to the n)?
<Smerdyakov>
cedricshock, yes. You don't even need the hypothesis about existence of a problem. You can skip right to the conclusion.
<cedricshock>
So can I say that there is a polynomial time problem that is at least this hard, for any given m:
<Nutssh>
Smerdyakov: I don't see that as relevant. It describes P and NP, but no proof of distinctness... It also mentions undecidable/unrecognizable languages.
<Smerdyakov>
Nutssh, see top of page 6.
<cedricshock>
c1 n^m + c2 n^(m-1) + c3 n^(m-2) + c3 n^(m-3) .. + c3 n^1 where cs are all positive
<Smerdyakov>
cedricshock, you can assert the existence of a problem that requires Omega() of that, yes.
<Nutssh>
Ah, I see.
<Smerdyakov>
Or, rather, I'm not sure I've seen that exact result. You can assert that there is a problem doable in O() of that and not O() of a polynomial of any lower degree.
<cedricshock>
Can I assert the existance of a problem that takes at least that much time for all n? T
<cedricshock>
Yeah.
<Smerdyakov>
It's not "at least that much time." It's only on the granularity of integer polynomial degrees.
<cedricshock>
But can I say that there is a problem that is harder?
<Smerdyakov>
What does that mean?
<cedricshock>
That takes more time.
<Smerdyakov>
Like I said: for any natural number k >= 4, there exists a problem doable in O(n^k) but not O(n^(k-1)).
<cedricshock>
The coeffecients matter. I think. They shouldn't, but If i don't deal with them someone will start attacking my proof there.
ez4 has joined #ocaml
<Smerdyakov>
No, they don't matter.
<cedricshock>
Since it is based on the actual >= comparison.
<Smerdyakov>
Only the highest degree coefficient matters asymptotically.
<cedricshock>
It will if I want to say >= and there is no higher degree.
<Nutssh>
For now, don't worry about the coefficients.
<cedricshock>
Here's a question that someone else might have thought about:
<Smerdyakov>
>= isn't something that matters to complexity theorists. They only care about asymptotics.
<Nutssh>
Smerdyakov: THanks for the link.
<cedricshock>
does there exist a polynomial heirarchy theorem like above, in which solving one of the problems (that of order n^a) of the heirarchy for a specific input does not lend to any reduction in the complexity of solving a problem of the heigherarchy of the order n^(a-1) for the same input?
<Smerdyakov>
cedricshock, whaaat?
<cedricshock>
In otherword, is the a polynomial heirarchy theorem which produces problems in which solving one of them (of some order a) does not help you solve other problems of different orders?
<Smerdyakov>
I don't see how that's necessarily a well-defined notion.
<Nutssh>
I think the heirarchy of ones given in the link Smerdyakov have that property.
<cedricshock>
Or does there exist an infinite number of un-related polynomial heirarchies?
<Smerdyakov>
If you're talking about one-to-one reductions, if the O(n^a) problem has a known false instance, then it's easy to reduce the empty problem to it.
<Smerdyakov>
cedricshock, you're not making sense.
<Smerdyakov>
Nutssh, no. See above.
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
<cedricshock>
I would be making sense if I wern't trying to dance around the edges of an idea.
<Smerdyakov>
cedricshock, you don't seem to have any idea what you're talking about. I recommend reading a textbook for an undergraduate course on theory of computation, if you're interested in this subject.
<Nutssh>
Ah, I missed the 'for the same input', requirement.
<cedricshock>
I don't have any idea what I'm talking about.
<cedricshock>
I've never had a theoretical cs class.
<cedricshock>
I know how asymptotic complexity works.
<Smerdyakov>
Great. Then it seems to be time for you to stop talking nonsense. :)
<cedricshock>
However it is absolutely vital to my proof that there exist problems that take time like cn^a + dn^a-1 that cannot be simplified any further.
<salo>
my turn to talk nonsense: how do i do what i want with this:
<cedricshock>
Showing that there is a problem like n^(a+1) would usually work, but it will be impossible.
<Smerdyakov>
Then your proof is no doubt bogus. (Though that was pretty obvious already)]
<salo>
type ('genotype, 'fitness) individual = {genotype: 'genotype; fitness: 'fitness};;
<salo>
type population individual list;;
<salo>
or rather: type population = individual list;;
<Smerdyakov>
salo, individual takes two parameters. You must specify them.
GreyLensman has joined #ocaml
Nutssh has left #ocaml []
Nutssh has joined #ocaml
<Nutssh>
With 'type ('a,'b) population = ('a,'b) individual list'
* salo
tries it
<salo>
thanks. slowly ocaml is coming into focus
<salo>
anyone have experience with one of the BLAS modules?
<cedricshock>
Well, I can't prove P=NP as described by clay because of an unnecessary and entirely artificial distinction between P and NP
<cedricshock>
Oh yay. They introduce the problem on page 1 and remove it on page 2.
<salo>
if that is your only obstacle, then start preparing for fame and fortune
<Nutssh>
cedricshock, just as long as you're not James Harris, I wish you luck in your exploration.
<cedricshock>
Who's James Harris?
<cedricshock>
What does c.e. stand for in C.S. papers?
<cedricshock>
No, I'm Cedric Shock.
<Nutssh>
Google for his name with 'mathematics' and/or 'sci.math' on the web and usenet.
<cedricshock>
Ok. That's kind of funny.
<cedricshock>
That's like the old multiply both sides by 0 ...
<Nutssh>
Don't fall into the same trap. :)
* Smerdyakov
tries to write the rule of contradiction in ML using call/cc.
budjet has joined #ocaml
<Nutssh>
?
cjohnson has quit [Connection timed out]
<Smerdyakov>
Do you know the Curry-Howard Isomorphism?
cjohnson has joined #ocaml
<cedricshock>
Smerdyakov: Where would I find a practical complexity model for an np-complete problem? Like "this problem can be solved in n*2^n time"?
<Smerdyakov>
cedricshock, every NP problem can be solved in exponential time by brute force search.
<Smerdyakov>
cedricshock, it follows easily from the definition of NP.
<Nutssh>
Yeah. I don't see how you'll get around contradiction being a non-constructive proof technique. Does C-H work in that case?
<Smerdyakov>
Nutssh, I believe that call/cc allows one to create a term of the right type. I'm trying to reconstruct the details.
<Nutssh>
If you pull it off, NEAT. I'd like to see.
<salo>
exception ('genotype, 'fitness) Success of ('genotype, 'fitness) individual;;
<salo>
repairable?
<Smerdyakov>
salo, exceptions can't be parametrized.
<salo>
alas. thanks
<Nutssh>
salo, Perhaps you're being overabstract. Just use a concrete type defined in some base module, and later turn it into a functor if you want to reuse? (Thats what I did for some genetic stuff I did a couple of years ago)
<salo>
well i definitely am trying to be as abstract as possible, but i do not understand your suggestion. i am a scheme refugee, day 2 with ocaml
<Nutssh>
Don't be abstract by using paramaterized types to that extent. Just do a 'type genotype = BLAH' and 'type fitness = bleah' somewhere and use them as concrete types.
<Nutssh>
What you're doing is akin to the C++ coding and templatizing every class you write.
<salo>
right. but i am attempting to write a generic GP framework, not a specific problem instance.
GreyLensman has left #ocaml []
<Nutssh>
Thats still doable. For now, write it concretely, but plan for it to be functored later. You don't knwo about functors yet, do you?
<salo>
functions defined on functions? i have some understanding, but not in an ocaml context
<Nutssh>
No. Modules defined as functions over other modules.
<salo>
sounds intriguing. so you say that my current approach won't work? or that functors are a superior approach?
<Nutssh>
Eg, a GA library module thats parameterized over a module implementing genes or mutation.
<Nutssh>
What I'm saying is to start with a simpler example, learn the tools.
<salo>
ok, fair enuf, but if my current approach will never work, i'd like to know sooner rather than later ...
<Nutssh>
In this case, I'd write a library totally concretely, but I'd seperate out the modules with reasonable boundaries. If I needed to reuse code, I'd be able to functorize it fairly easily.
<Nutssh>
It'll work, but probably be overcomplicated. Ever seen some of those hyperlayered OO designs with like 10 layers of processing?
<salo>
sadly, yes ... but am i really going that far wrong?
<salo>
type ('genotype, 'fitness) individual = {genotype: 'genotype; fitness: 'fitness};;
<salo>
type ('genotype, 'fitness) population = ('genotype, 'fitness) individual list;;
<salo>
that's not sensible?
grom358 has joined #ocaml
<Nutssh>
IMHO, Thats not as important as the ability to recognize if you are going wrong.
<Smerdyakov>
Nutssh, fun contra f = callcc (fn k => falsee (f (throw k)))
<Nutssh>
I'd just do 'type population = individual list'.
<Smerdyakov>
Nutssh, contra : (('a -> FALSE) -> FALSE) -> 'a
<grom358>
Can anyone point me to database binding for ocaml (ala ODBC or JDBC)?
<Nutssh>
Smerdyakov: times like this I wish I had more of the 'scheme way'. I don't quite get that, particularily the 'throw k' part.
<grom358>
thanks... now the only other thing I need to find is binding to cross-platform GUI such as wxWidgets
<salo>
Nutssh: but my design calls for an individual to be a pair consisting of a genotype and a fitness ...
<Smerdyakov>
Nutssh, just stare at it for a while. :-) In the mean time, I've implemented a complete proof system for classical propositional logic in SML/NJ. :)
<Smerdyakov>
(Where proofs are checked by the SML type-checker)
m3ga has joined #ocaml
<Nutssh>
salo: So, just define it as 'type individual = {genotype:BaseTypes.gene; fitness:float} Where BaseTypes.gene = unit for now, but someoen can edit in what they want later.
<Nutssh>
Smerdyakov: That is bizarre, but I'm impressed! Whats the type of falsee?
<Nutssh>
No, I mean, applying the typing rules, I think I get that, now what you inferred.
<Smerdyakov>
OK, but then it also has the type I gave, with 'b = FALSE.
<cedricshock>
Smeryakov: The paper you pointed to doesn't seem to have polynomial complexity problems of arbitrarily high orders.
<Nutssh>
cedricshock: It proves they exist.
<Smerdyakov>
cedricshock, the approach generalizes.
<Nutssh>
Smerdyakov: Ok.. 'a = 'c. I see that now. But why is 'b = FALSE?
<Smerdyakov>
Nutssh, it _can_ be. That's all that matters.
<Nutssh>
Is that enough?
_fab has quit [Read error: 238 (Connection timed out)]
<cedricshock>
Smeryakov: It seems to be all about order 3, Is it in lemma 5, or am I supposed to substitute something for 3 and belive the argument still holds?
<cedricshock>
I know I typed the d that time.
<Nutssh>
cedricshock: The choice of 3 was arbitrary, so yes. If you're not sure, look at that until you can totally convince yourself before moving on.
_fab has joined #ocaml
<cedricshock>
polnomial heirarchy / polynomial heirarchy theory keep leading me to quite abstract sources.
<cedricshock>
I probably need to be looking at papers 30-40 years old to find ones that say, "Look we can build problems as hard as we want!" to cite.
cjohnson has quit [Read error: 104 (Connection reset by peer)]
<salo>
how do you create multiple internal definitions inside a function?
<salo>
let f x =
<salo>
let foo = 5
<salo>
and bar = 2*foo
<salo>
in
<salo>
foo * bar;;
<salo>
is wrong ...
<Nutssh>
The binding for 'let foo = ... in ...' isn't available until after the 'in'. Try 'let foo = ... in let bar = ... in ...'
<Nutssh>
cedricshock: Then do it. :)
<salo>
is there something equivalent to scheme's let*? let rec doesn't appear to work
<Nutssh>
It should, but in this case, let in let in would work.
<salo>
let f x =
<salo>
let rec foo = 5
<salo>
and bar = 2*foo
<salo>
in
<salo>
foo * bar;;
<salo>
is that close to working?
<Nutssh>
should.
<salo>
and bar = 2*foo
<salo>
^^^^^
<salo>
This kind of expression is not allowed as right-hand side of `let rec'
<Nutssh>
hmms. Maybe an overly conservative detection of circular definitions. Just use let in let in.
<cedricshock>
Thanks for your help. I'm going to a party.
<salo>
Nutssh: fair enough, but that form is ugly
cedricshock has quit ["Leaving"]
<Nutssh>
Its different. Space it right and its no uglier than sequential else if else if in C++/java/C
<salo>
better than those, but not as nice as let/and/and/.../in, which is analagous to internal definitions in scheme
grom358 has quit []
jinterest has joined #ocaml
jinterest has quit ["Leaving"]
salo has quit []
ez4 has quit [Remote closed the connection]
mrsolo_ has quit [Read error: 54 (Connection reset by peer)]
mrsolo_ has joined #ocaml
haakonn has quit [Read error: 110 (Connection timed out)]
ne1 has quit ["To understand recursion, you must first understand recursion."]
Herrchen has joined #ocaml
vezenchio has joined #ocaml
jason__ has joined #ocaml
<jason__>
Hm.. Is there any way to catch "Broken Pipe"?
<jason__>
...
<mflux>
handle sigpipe?
<mflux>
or ignore it and handle return values from write
<jason__>
Hm.
<jason__>
So, I have to handle system signals or something?
<jason__>
Can't try with?
<mflux>
hmm, lemme see, infact I just recently wrote code that manages broken pipe ok but it doesn't use the word pipe, investigating ;)
<mflux>
infact no, I might just never have bumped into the problem in that program, so it might very well just die
<mflux>
I wonder where SIGPIPE is defined
<mflux>
the documentation refers to it but I can't find the definition
<mflux>
anyway, I would expect code like but yes. I would imagine Unix.sigprocmask Unix.SIG_BLOCK [Unix.SIGPIPE] somewhere in the initialization to take care of the problem
<mflux>
whops, apparently I had text already written ;)
haakonn has joined #ocaml
<mflux>
s/.*like //
<mflux>
but as I said, I can't find the SIGPIPE definition, so..
<mflux>
ah, and now I notice there a little text referring to Sys.signal ;)
grom358 has joined #ocaml
<grom358>
is there already a ocaml binding for wxWidgets?
<mflux>
so you could just use Sys.set_signal Sys.sigpipe Sys.Signal_ignore
<mflux>
grom358, did you check out the hump?
<grom358>
yes
<mflux>
well, I don't have other ideas ;)
<grom358>
okay... I'll still looking into ocaml, but maybe can use SWIG (wxPython uses it) to generate oCaml bindings
<grom358>
mmm.. I found some code
jason__ has quit [Remote closed the connection]
<grom358>
has anyone here used SWIG to generate ocaml bindings?
Tristram has quit ["Leaving"]
mrsolo_ has quit [Read error: 54 (Connection reset by peer)]
<grom358>
does ocaml support unicode?
Nutssh has left #ocaml []
grom358 has quit [Read error: 232 (Connection reset by peer)]
haakonn has quit [Read error: 104 (Connection reset by peer)]
bk_ has joined #ocaml
haakonn has joined #ocaml
haakonn_ has joined #ocaml
haakonn has quit [Read error: 54 (Connection reset by peer)]
haakonn has joined #ocaml
haakonn_ has quit [Read error: 60 (Operation timed out)]
<vincenz>
can modules be nested?
cmeme has quit ["Client terminated by server"]
cmeme has joined #ocaml
<nysin>
THere's wxHaskell, so some people have tried (I don't know with what success) to essentially port that.
haakonn has quit [Read error: 104 (Connection reset by peer)]
haakonn has joined #ocaml
salo has joined #ocaml
<salo>
is anyone here on the caml-list ?
salo has quit [Client Quit]
haakonn_ has joined #ocaml
CosmicRay has joined #ocaml
haakonn has quit [Read error: 110 (Connection timed out)]
cedricshock has joined #ocaml
mrsolo_ has joined #ocaml
pango has quit [Nick collision from services.]
pango_ has joined #ocaml
cjohnson has joined #ocaml
lmbdwar has quit [Read error: 104 (Connection reset by peer)]
monochrom has joined #ocaml
Herrchen has quit ["bye"]
cjohnson has quit [Read error: 110 (Connection timed out)]
cjohnson has joined #ocaml
async has joined #ocaml
<async>
hello, what's the best way to do unsigned division with Int32?
<Smerdyakov>
You probably can't.
<async>
btw, is there a reason that int is only 31 bits?
<Smerdyakov>
Yes.
<Smerdyakov>
It's not necessary, but it follows from runtime system design choices.
<Smerdyakov>
Use MLton instead.
salo has joined #ocaml
async has quit [zelazny.freenode.net irc.freenode.net]
mrsolo_ has quit [zelazny.freenode.net irc.freenode.net]
cmeme has quit [zelazny.freenode.net irc.freenode.net]
jrosdahl has quit [zelazny.freenode.net irc.freenode.net]
nysin has quit [zelazny.freenode.net irc.freenode.net]
mellum has quit [zelazny.freenode.net irc.freenode.net]
Niccolo has quit [zelazny.freenode.net irc.freenode.net]
Hadaka has quit [zelazny.freenode.net irc.freenode.net]
slashvar[lri] has quit [zelazny.freenode.net irc.freenode.net]
CosmicRay has quit [zelazny.freenode.net irc.freenode.net]
det has quit [zelazny.freenode.net irc.freenode.net]
haakonn_ has quit [zelazny.freenode.net irc.freenode.net]
skylan has quit [zelazny.freenode.net irc.freenode.net]
buggs has quit [zelazny.freenode.net irc.freenode.net]
haelix has quit [zelazny.freenode.net irc.freenode.net]
srv_ has quit [zelazny.freenode.net irc.freenode.net]
vincenz has quit [zelazny.freenode.net irc.freenode.net]
TheDracle has quit [zelazny.freenode.net irc.freenode.net]
Excedrin has quit [zelazny.freenode.net irc.freenode.net]
mflux has quit [zelazny.freenode.net irc.freenode.net]
bacam has quit [zelazny.freenode.net irc.freenode.net]
monochrom has quit [zelazny.freenode.net irc.freenode.net]
bk_ has quit [zelazny.freenode.net irc.freenode.net]
vezenchio has quit [zelazny.freenode.net irc.freenode.net]
avn has quit [zelazny.freenode.net irc.freenode.net]
async has joined #ocaml
monochrom has joined #ocaml
mrsolo_ has joined #ocaml
CosmicRay has joined #ocaml
haakonn_ has joined #ocaml
cmeme has joined #ocaml
bk_ has joined #ocaml
vezenchio has joined #ocaml
Niccolo has joined #ocaml
jrosdahl has joined #ocaml
srv_ has joined #ocaml
vincenz has joined #ocaml
nysin has joined #ocaml
skylan has joined #ocaml
TheDracle has joined #ocaml
mellum has joined #ocaml
Hadaka has joined #ocaml
buggs has joined #ocaml
haelix has joined #ocaml
Excedrin has joined #ocaml
slashvar[lri] has joined #ocaml
avn has joined #ocaml
det has joined #ocaml
mflux has joined #ocaml
bacam has joined #ocaml
haakonn_ is now known as haakonn
<salo>
anyone have an opinion of the various BLAS modules ?
<Smerdyakov>
I have a hunch that very few ML users care about linear algebra.
<CosmicRay>
Smerdyakov: very few people do :-)
<salo>
curious statement
CosmicRay has left #ocaml []
<Smerdyakov>
salo, why?
<salo>
my interest in ocaml stems from its uniformly high performance on seminumerical benchmarks, particularily linear algebra.
cjohnson has quit [Connection timed out]
<Smerdyakov>
Sure, but that's unusual. Most ML users are more interested in symbolic computation.
cjohnson has joined #ocaml
<async>
im tring to write a c funciton which is the type Int32->realint (realint is a custom type).. how do i access the contents of the int32, and whats the best way to return a custom type (should i use alloc?)
<async>
Int32_val(v)
<async>
ok, thats #1
<salo>
smerdyakov: i guess it is a happy accident that ocaml performs so very well numerically?
<async>
salo: i'd use the BLAS/LAPACK module by marcus mottl
<async>
the stuff he writes is usually top-notch
<salo>
async: thanks, i'll look there first
<salo>
async: i cannot find a BLAS module by mottl in the humps directory ...
vezenchio has quit ["None of you understand. I'm not locked up in here with you. YOU are locked up in here with ME!"]
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
bk_ has quit ["Leaving IRC - dircproxy 1.1.0"]
<salo>
intererestings, thanks for the links
cjohnson has quit [Connection timed out]
cjohnson has joined #ocaml
cedricshock has quit ["Leaving"]
cjohnson has quit [Success]
cjohnson has joined #ocaml
monochrom has quit ["Don't talk to those who talk to themselves."]
mayhem has joined #ocaml
<mayhem>
yop
<Demitar>
In what domains are metaprogramming a good choice?
<Demitar>
Is it the right tool to generate codecs or is that purely the domain of preprocessors? And even more interestingly can it be used to automate the process of generating internally consistent datamodels?
<gl>
in the meta-life, not the real life
<Demitar>
Hmm... I guess some of my confusion arises from no proper distinction between metaprogramming and multi-stage programming.
<mayhem>
If I'm not mistaking, metaprogramming = resolving parts of problems at compile time
<mayhem>
thats more like a consequence of it, metaprogramming beeing writing a program that generates other programs, like writing a factorial template which automatically computes the prerequired immediate previous factorial automatically at compile time
<mayhem>
multistage programming -> I guess you refer to program transformation ?
<mayhem>
which is a technique of metaprogramming I guess
<mayhem>
maybe someone will contradict me and I'll learn something today ,;?
<Demitar>
So in practice it's mostly useful for optimization?
<mayhem>
all techniques that I know, yes thats the primary use of it, but an analysis software can make use of it as well, in a general context
<mayhem>
most peoples writing metaprograms will argue it for performance reasons
<mayhem>
but its much more powerful than just a performance trick imho
<Demitar>
I guess the way I'd like to use it is in many ways as a powerful and type-aware preprocessor.
<mayhem>
?
<Demitar>
Take the codec example.
<mayhem>
verification of the integrity of it, you mean ?
<Demitar>
I want to encode and decode a structure such as: type foo = A of int | B of string
<Demitar>
And I don't particularly like writing all those specific cases by hand.
<Demitar>
Hmm... I think my problem stems from the fact that there is no way (metaprogramming or no metaprogramming) to treat types as first-class values.
<Demitar>
(Thus I should probably go look at camlp4 again.)
<Demitar>
The same probably goes for my datamodel (which is a hierarchy of classes and objects interacting in various ways).
<Demitar>
Problem is that trying to do all of these things using a preprocessor easily becomes more complex than the problem itself.
<Demitar>
It's definitely metaprogramming but doesn't really fit the mold of multi-stage programming.
cjohnson has quit [Read error: 110 (Connection timed out)]