IRC log started Sun Aug 22 00:00:00 1999 [msg(TUNES)] permlog 1999.0822 -:- SignOff Mr_Wrong: #TUNES (Ping timeout for Mr_Wrong[adsl-63-192-213-146.dsl.snfc21.pacbell.net]) -:- Mr_Wrong [seanl@adsl-63-192-213-146.dsl.snfc21.pacbell.net] has joined #tunes -:- water [water@ppp-tnt-170.tscnet.net] has left #tunes [] -:- SignOff ruiner: #TUNES (Leaving) -:- SignOff liar: #TUNES (BRiX [http://www.qzx.com/brix] :: sleep) -:- SignOff KorGrey: #TUNES (Ping timeout for KorGrey[pm-ppp26.triton.net]) -:- water [water@ppp-tnt-170.tscnet.net] has joined #tunes -:- SignOff water: #TUNES (Ping timeout for water[ppp-tnt-170.tscnet.net]) -:- SignOff eihrul: #TUNES (Leaving) gakuk! 05:50am -:- AlonzoTG [Alonzo@209-122-205-175.s175.tnt4.lnh.md.dialup.rcn.com] has joined #tunes -:- hcf [nef@me-portland-us916.javanet.com] has joined #tunes -:- binEng [Anders@j141.ryd.student.liu.se] has joined #tunes * AlonzoTG/#tunes left clicks on binEng ouch 07:50am =\ 08:00am -:- SignOff hcf: #TUNES (Leaving) -:- pyro [tcn@cci-209150250116.clarityconnect.net] has joined #tunes hey.. anyone home? 08:50am -:- SignOff binEng: #TUNES ( ) * Fare/#Tunes is back home -:- smkl [sami@CMLXXVI.rdyn.saunalahti.fi] has joined #tunes -:- water [water@ppp-tnt-35.tscnet.net] has joined #tunes water! fare! what's up? 09:20am does anybody have some thoughts about using reflection to optimize search mechanisms of a theorem prover? kinda smkl: search for a survey about reflection by John Harrison if you had more than one kind of logic to choose from, you could reflect on the nature of the problem and then transform it into the context of a logic that deals with it with much les complexity (in precisely this topic) smkl: fermivista.math.jussieu.fr is your friend Immagine a string of data, several million units long that specifies unambiguously a number of operations that can be peroformed on itself... =P smkl: Coq has been growing on the reflection side, lately; NuPRL has always been strong on reflection, too not good enough water: ? those don't actually reduce problem complexity: they leave you with the noise of standard first-order logic water: what are you talking about, precisely? the fact that first-order logic can encode undecidable problems makes it more difficult to prove theorems with in any problem encoded in it ? n/m 09:30am later folks -:- SignOff pyro: #TUNES (pyro has no reason) rats... missed him... i'm just saying that a fol theorem-prover can't specialize its search strategy without a hack because it can't disinguish a priori undecidable problems from decidable or feasible ones ? jesus christ! if what you mean is "it can't decide the undecidable", then "sure"! no but that's hardly a limitation of it i'm saying that fol contains undecidable problems, and they "spoil the whole soup" if you mean "if you didn't build reflection in your system, then you won't otherwise magically have it", then "indeed", too. why do they spoil anything? forget it water: I forgot it you can't decidably separate these problems from decidable problems! so that's hardly a limitation of fol. no, but you can try no, you can't it's like trying to force people to act morally and i'm not talking about sitcking with fol as you are it only leads to oppression i'm talking about re-casting the problem in other simpler logics which you have obiously never considered if "simpler" means "less expressive", then *this* is a limitation yes (just like Coq -- chose to not be able to directly express non-terminating objects) sort of except that its own logical calculus is implicit: you can't change it to learn more about the problem you can't reflect on it :) ? 09:40am jfc! jfc? jesus fuckng christ you know, i've recently come to the conclusion that you listen ten times as well when a person has the letters PhD suffixed to their name as a title you pandered to that one professor on the mailing list very well. ? familiar with the term "brown-nosing"? ? i suppose not. let's say that you treat tunes members as second-class citizens ? just as you do to me right now you like feeling insulted, don't you? You see insult everywhere. I guess whatever I say, you'll feel insulted. no, just in _you_ well, to see the way that you complimented that john shapiro fellow at every other sentence your accusations sound like nonsense to me. of course I'm sure he feels insulted, too why don't you just admit that you want to sleep with him I don't think I complimented him at all, and I'm sure he knows it. since you worship him so much me, worship him???? 09:50am I don't know EROS much, and am not particularly impressed by what I saw (although there might be a lot more to it than I grasped) it certainly appears so, from the emails. you were tiptoeing through a glass shop just to try not to offend him with your close-minded reasoning I sure tried not to offend him. which you never do with anyone else unless their title includes "PhD" I'm sure interested in getting feedback from people inserted in academic situations. water: you're very well misled. and you're ignorant of your own situation I don't care if they're PhD or not. I care if they might invest in Tunes or not. you mislead yourself i don't disagree there but you still have "degree envy" no, I have "financial means of achieving Tunes" envy. lol I have "reaching my ends" envy much like anyone with any ambition. so, how's your reflective framework design going? i'm sure you have many great ideas, and of course you're just around the corner from completion, so that you'll be writing code shortly ;) (intentional sarcasm) that's the very definition of ambition, btw no, that's extensional sarcasm intended the other meaning extended whatever (btw, you evaded the point very well. that's insulting.) what's insulting? talk to me, don't correct me for your own egotistical pleasure y o u e v a d e d t h e p o i n t ! if you make it clear where your questions/propositions are, as opposed to mere whining/insulting, that'd be easier for me to discuss with you! when you irc, it's never clear. but i can't because everything i try to explain to you that i've learned gets the response of "?" of course you can. Just insist on what you feel is important that I didn't get. i pretty much spelled it out for you in three different ways earlier, and you acted like i was speaking another language the point about fol being too expressive? yes I see no evidence for that. and that one solution for "less expressiveness" is not/never enough bs! too expressive as compared to what? ok, I give you a logic where the only statement is the null statement, which is true modal logics, restricted relational algebras, arrow logic propositional dynamic logic or if you want, I also allow a bottom statement, which is false. are you satisfied with this logic? why not? 10:00am the logic should express the problem in a very small formula water: null and bottom are small formula but they don't express the target formula i.e. not expressive enough water: uh uh. So you want *more* expressiveness, don't you? * water/#tunes holds Fare by the hand a nd walks him through the oh so dangerous territory of conceiving the use of alternative logics. water: Godel ensures you will have "paradoxes" in any logic able to express numbers. Alternate or not. less than full fol, but more than your "nul calculus" just calling something "new fangled" and "modal" or "dynamic" won't remove the paradoxes. hello? there are logics which are quite expressive, but can't encode the numbers if you can express numbers, you can express paradoxes. not necessarily water: if the logic is reflective, it has paradoxes. again, not necessarily Godel showed that numbers allowed for reflection, but the core of the argument is in reflection, not in numbers. you read to much into his theorems s/to/too you can vary the logic in more ways, such as refining the quantifiers water: sure, just like Coq does, for instance, with a very elaborate type system... yes, but that's only one extension, which again is not enough another way is to restrict definitions, as in Boyer-Moore you should be able to shift paradigms based on the problem set, not some programmer's idea of the "best logic" water: in as much as your arrow logic can encode fol, it is more expressive and has all the usual paradoxes which _Coq does not do_! standard arrow logics cannot encode fol water: shifting paradigm is what reflection is about. Reflection was never a primary part of Coq's design (although they're adding it by the user end) my family of logics has expressivity which is varied by generating new arrow frames specified by axioms/ schema/ etc the range of expressivity achieved is great enough to encompass your "nul calculus" and fol and much more expressive logics so are fol, hol, lu, cl, and other logic frameworks it can also express programming paradigms no NO yes YES they are lame. they don't actually reify the new environment, they just implement it of course they can reify the new environment. that's what modal logics are about (lu is such, for instance) which for computational systems dealing with the possibility of paradoxes, is no help at all what are lu and cl ? Logic of Unity (with linear objects); Combinatory Logic 10:10am -:- _water [water@ppp-tnt-35.tscnet.net] has joined #tunes linear logic is a modal framework. -:- SignOff water: #TUNES (Read error to water[ppp-tnt-35.tscnet.net]: Connection reset by peer) <_water> so? it's still just one framework -:- _water is now known as water so? arrow logic is just one framework, too standard arrow logic is every single framework is just one framework! mine is not how is it not? I think you're mistaking yourself a lot on that. reflective in arbitrary ways. im not sure if everything in the system is reflective not yet what does that mean? can you formalize it? how can't other logical frameworks do it? not yet. i'm working on it. i need a way to express the fact that if you formulate a frame within an arrow logic, that you can reify it THESE are the key questions. yes, if all i want is a PhD :) yes, if you want to be understood at all yes, if you want to be able to convince anyone at all why not "code like crazy" and let the results speak for themselves? leave the formalization to the academics? convince people that you are right, not just convince people that you have some intuitions. i don't care if i'm right water: you'll have to find an academic to do that for you i'm not like you: i don't have to be "right" and this academic will have to at least have a hint on what you mean... i've already found a few, but they're waiting on code if you don't care, why should I? why should anyone care? about being right? being right is an illusion "Fare is right" = "Fare sucks professors well." "Reality is that which, when you stop believing in it, doesn't go away". -- P. K. Dick which is nothing /ignore water as usual water: you don't exist anymore. * water/#tunes wishes Fare would /ignore academia /ignore universe but then, Fare would cease to exist whatever. you're just finding more ways to think of me as someone who hasn't considered you're issues already so what? I wouldn't complain, if I didn't exist. are you coming here just to whine? that's not the point. it seems that your existence a priori assumes interest in academia i came here to discuss to suggest ideas which obviously are not appreciated how can an existence assume anything? it can't 10:20am ideas like "fol is too expressive"? so how can I do when I want to solve a problem easily expressed in fol? you're misguided about your notion of "easily expressed" you don't understand it must I learn to not care about such questions? reminds me of C++ "don't try to think to questions that cannot be solved with it" you think that your fol formulas are enough, but they are too complex if you're going to sell me a new kind of C++, I won't buy it. the existential operator itself is complex so what? good, because i'm not selling life is complex duh, but the problem often isn't complex enough to warrant it you mustn't fear complexity; but tame it. that's the approach of the academic that's the approach of life. as far as knowledge goes, that's the approach of science. because the academic wants to look like a "hero" when he's done with this overly complex expression of a problem another way is to pray until you have enlightment. or maybe to meditate. i.e. it makes papers look more respectible when they obfuscate the simple solution no, the academic looks like a hero when he spliced the complex problem into simpler parts. hahahahahah ob om only he's really only solving one simple problem in a way that others think is sooo difficult. he's a hero when he shows that what looked complex is actually simple. that's the illusion what was *a priori* complex is shown *a posteriori* simple. he dispells the illusion. the truth is that formalisms inherently make such issues mu the formalisms are unconsciously chosen for this property so you propose a non-formalism? can your non-formalism be communicated? consider the reluctance a few centuries ago to consider a geometrical solution to the polynomial solution no? maybe that's why you have a communication problem. polynomial problem formalising is about communicating formalisin is about impressing people when communicating not about the act itself it's about the meta-act of course, since formalism is the standard millenia old, informal ideas are dismissed for decades which brings about research anomalies like Galois theory "Actually a person does not _really_ understand something until teaching it to a _computer_, i.e. expressing it as an algorithm." D.E. Knuth. Galoiks theory is very formal shut up don't try to intimidate me with old men spouting nonsense water: you haven't seen the light. 10:30am they think that they've learned something, but they've just put themselves inside a box Try to read math books of pre-Descartes era, before formalism was used! * water/#tunes is not a machine i don't grow by teaching machines formalism IS about communicating, precisely and concisely. i'm not getting through to you at all. you're addicted to your point of view om something written in ten lines of formalism would take ten pages to express without formalism, at which point it would be completely ununderstandable. formalism makes complex things simple. water: do you know Galois theory? Fare: go snort your "formalism" cocaine Fare: go inject yourself with you "academic" heroin yep it should have been discovered many centuries sooner :P water: it could hardly have been discovered sooner. it wasn't an advance in research. the fact that it arrived so late signals that the academics ignored the possibility of such an idea before that time it was a *great* advance in research!!! yes, it could have been discovered by anyone ??? any idiot could have figured it out ??? their paradigms restricted them form imagining such things water: did you? yes age: 14. within geometry class mathematics is all about saying tautologies. But things that are known *a posteriori* to be tautologies. no, it isn't. it used to be about tautologies water: and you discovered the notion of polynomial, of number field, of subfield, of quotient field, etc, at age 14? well, congratulations. i didn't express them like that at all but my teacher understood what i was saying and pointed me to a few books oh, yeah, so I discovered the whole of maths at age 1, but i didn't quite express like other people did at all. * AlonzoTG/#tunes wishes he had yer teacher =\ and at age 3, I invented rocket science and the internet (a bit before Al Gore) hehehe thanks for respecting my opinions, fare. it's a wonder i have ever felt insulted you're just a bigot, and your goal with tunes is to prove that you aren't by surrounding yourself with people who can't argue with you what I meant is that *of course*, when you live in a world built upon a lot of common knowledge, it's very easy to "rediscover" the assumptions upon which so much was developed; inventing things from scratch is much harder. i know i'm an idiot, because i see others every day, and can't help them expand their minds well ah but these are epistemic ideas they might get clues from the world, but i'd bet galois got the same clues from his world 10:40am galois didn't live in the stone age my father being a math teacher, I never had any problem (re)discovering a lot of mathematical theory without being taught it -- because it seemed obvious from my surrounding environment. neither did pythagoras, for that matter the environment provides your formalism but when I reached the point of being in advanced math courses, my intuition faltered -- because I reached the limits of that environment. your formalism works like your environment it's too complex ;) galois lived in the (polished) stone age of mathematics. but he grew up without much help and he "discovered" his ideas very quickly, not like older researchers do so what? this was a novel field of study. this stone age you refer to is just what you consider to be the absense of formalism in mathematics no, it wasn't not novel at all just not respected he approached it with a fresh mind, from an original angle. exactly, and what you have is a stale mind you know, you're the one insulting other people all along. which means you only contribute regurgitations of old ideas yes, i am insulting you you deserve it, you bigot well, I don't resent it, but it is quite annoying. At most, I pity you. yes, to be reminded of one's place in the larger scheme of things is very annoying good. i wouldn't want you to step down from your pedestal :) I don't claim that much originality, either. ah! what, "ah"? so your ideas are just re-fried lambda-calculus, then? you only see pedestals because you crawl geez i don't see them at all i'm on the other end of the world (say, in australia) there's more to CS than being lambda-calculus or not lambda-calculus. you think that i'm standing upside-down and far beneath you lambda-calculus is the beginning, not the end. duh if you don't go through the beginning, you'll never reach the end, tho but you focus on it YOU are focused on it, not me. YOU spend your whole time hating it. that's because i don't implicitly assume it and you do btw, i only have this sort of argument with you. most others are very receptive :P GIGO GOGI you send them garbage input, they give you back garbage nodding. the causality loop here is very small and non-orientable then they forget about you. if you give me garbage, then all i can return is garbage i.e. the loop is non-orientable it works both ways 10:50am then forget me. what does that mean? there are so many ways to interpret that /ignore me, and do your stuff. Why waste your time insulting me? because you could help me out, and i could help you we both ignore each others' research interests besides, you lead a lot of people who otherwise might help me out then don't insult me. insults won't lead you anywhere. you represent their cs knowledge, because they don't know enough to argue ? then send your gripes to the list i'm saying that they can't give you feedback, and in that sense depend on you I still don't get that you won't ever learn from anyone in the tunes group, because they can't meaningfully argue with you you even attract people of that sort =\ lol sorry, atg i hate to say it, but i doubt if Fare's ever learned anything theoretical from a Tunes member. all I care about is getting my OS!!! learned = groked exactly, atg and Fare would drive away anyone who could teach him something theoretical from being a member water: I don't usually learn things theoretical from people, but rather from articles, sources, and experimentation. Tunes people have led me to a lot of such things. and I can only thank them. have led you to aka hcf? that's not what i'm talking about not just him. See the lots of URLs posted on the lists since 1994 i'm saying that tunesers won't ever be able to teach you anything themselves -:- liar [brand@p0wer.qzx.com] has joined #tunes ever hi liar hi that's what I'm talking about. Theoretical things are not the kind of things that are easily understood thru ircing or thru e-mail messages (although with long messages, you can) 11:00am lol. i bet you made the project an internet project for that purpose they are things you must read slowly and think about, and articles and books are the fit way to do it why don't you take this project off line? -:- sr [depag@phila-dialup008.nni.com] has joined #tunes hey (sometimes, a few long yet focused articles on a mailing-list or a usenet group does it) hey sr Fare: this project must waste a lot of your time, then also, deep things take some time to grok. So a message or article may be part or trigger of the process, but learning is mostl"Actually a person does not _really_ understand something until teaching it to a _computer_, i.e. expressing it as an algorithm." (oops, bad paste) I am really confused about I/O port addressing. is mostly an internal process oh great Intel manuals state that the I/O port address space is made of 64k 8-bit ports. It says that 16-bit and 32-bit ports only exist as composites of 8-bit ports. So if this is true, a 32-bit port would _have_ to be something like 03ah, 03bh, 03ch, and 03dh. However, i read some IDE manuals, and found the "data" port to be 1f0h. I thought it logical, but when i read further i found the "error" port to be 1f1h. It also was written that the "data" port was 16/32-bits! How could this be if all the ports had to be 8-bit, as intel stated?