IRC log started Fri Apr 16 00:00:01 1999 [msg(TUNES)] permlog 1999.0416 -:- Downix [down@d-nh-concord-22.ici.net] has joined #Tunes -:- mode/#Tunes [+v Downix] by Tril morning 02:30am -:- Horizon [thunda@di-017.downunder.net.au] has joined #tunes -:- mode/#Tunes [+v Horizon] by Tril -:- SignOff Horizon: #TUNES (A little older. A little wiser. But not much.) -:- lagggg [sdevil@usr06.primenet.com] has joined #tunes -:- mode/#Tunes [+v lagggg] by Tril -:- lagggg [sdevil@usr06.primenet.com] has left #tunes [] -:- AlonzoTG [Alonzo@client-151-200-125-29.bellatlantic.net] has joined #tunes -:- irc [abergel@chimene.enst.fr] has joined #tunes -:- mode/#Tunes [+v irc] by Tril -:- irc is now known as Zif [Zif(abergel@chimene.enst.fr)] hello -:- SignOff Zif: #TUNES (Leaving) -:- aPasc [anin_p@pA31.hbt.southcom.com.au] has joined #Tunes -:- mode/#Tunes [+v aPasc] by Tril -:- aPasc [anin_p@pA31.hbt.southcom.com.au] has left #Tunes [] -:- SignOff Downix: #TUNES (Leaving) -:- NetSplit: sterling.openprojects.net split from koontz.openprojects.net [06:26am] -:- BitchX+Deb1an: Press Ctrl-F to see who left Ctrl-E to change to [sterling.openprojects.net] -:- Netjoined: sterling.openprojects.net koontz.openprojects.net -:- Tril [dem@sloth.wcug.wwu.edu] has joined #Tunes -:- abi [abi@bespin.cx] has joined #Tunes -:- AlonzoTG [Alonzo@client-151-200-125-29.bellatlantic.net] has joined #Tunes -:- ServerMode/#Tunes [+o Tril] by varley.openprojects.net -:- Fare [rideau@quatramaran.ens.fr] has joined #Tunes -:- mode/#Tunes [+v Fare] by Tril -:- Fare has changed the topic on channel #Tunes to: Reflective Computing System -:- Zeus [Zeus@ie-191.arrakis.es] has joined #Tunes -:- mode/#Tunes [+v Zeus] by Tril hello -:- Zeus [Zeus@ie-191.arrakis.es] has left #Tunes [] 07:50am -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) -:- Closing Link: TUNES[bespin.cx] by vinge.openprojects.net (Ping timeout for TUNES[bespin.cx]) -:- Connection closed from irc.us.openprojects.net: Success -:- Connecting to port 6667 of server irc.us.openprojects.net [refnum 0] -:- BitchX+Deb1an: For more information about BitchX type /about -:- Welcome to the Internet Relay Network TUNES (from tolkien.openprojects.net) -:- Your host is tolkien.openprojects.net, running version u2.10.04.resolv9.nmt.egcs4.tok.pten.tlim4.admin.upper4.whisper3.gipl.modeless7 (from tolkien.openprojects.net) -:- This server was cobbled together Sun Jan 24 1999 at 15 50:17 EST(from tolkien.openprojects.net) -:- tolkien.openprojects.net u2.10.04.resolv9.nmt.egcs4.tok.pten.tlim4.admin.upper4.whisper3.gipl.modeless7 dioswkfcg biklmnopstv -:- [local users on irc(10)] 4% -:- [global users on irc(100)] 38% -:- [invisible users on irc(161)] 62% -:- [ircops on irc(12)] 5% -:- [total users on irc(261)] -:- [unknown connections(0)] -:- [total servers on irc(33)] (avg. 7 users per server) -:- [total channels created(72)] (avg. 3 users per channel) !tolkien.openprojects.net Highest connection count: 19 (17 clients) -:- Mode change [+f] for user TUNES -:- Mode change [+iws] for user TUNES -:- JOIN activated by "TUNES #tunes tunes@bespin.cx " -:- TUNES [tunes@bespin.cx] has joined #tunes -:- Topic for #TUNES: Reflective Computing System -:- topic set by Fare [Fri Apr 16 06:46:50 1999] -:- [Users(#Tunes:5)] [ TUNES ] [vFare ] [vtimestamp ] [@Tril ] [ abi ] -:- mode/#Tunes [+v TUNES] by Tril -:- Channel #Tunes was created at Sun Feb 28 08:48:06 1999 -:- BitchX+Deb1an: Join to #tunes was synced in 7.505 secs!! -:- Mode change [-s] for user TUNES -:- GMOL [gmol@24.66.11.51] has joined #tunes -:- mode/#Tunes [+v GMOL] by Tril CAn anyone explain the term "first class" when used in terms of languages? Haaaaarooooooo? 09:00am * GMOL/#tunes slaps GMOL around a bit with a large trout dgidfg GMOL: first class means it can be manipulated like any other entity in the system. in particular, it can be taken as a function parameter and returned by a function (or similarly used in a variable) 09:10am Oh ok tha makes sesne, another thing I was wondering is just how do theorm provers like we are /have been talking about have anything to do with a OS/reflective computing etc. I.e. what does proving things have anything to do with practical computing? 09:40am !asimov.openprojects.net!! Remote CONNECT xing.openprojects.net 8005 from lilo !asimov.openprojects.net!! Remote CONNECT lu.openprojects.net 8005 from lilo !jordan.openprojects.net!! Remote CONNECT xing.openprojects.net 8005 from lilo !jordan.openprojects.net!! Remote CONNECT lu.openprojects.net 8005 from lilo !lu.openprojects.net!! Remote CONNECT xing.openprojects.net 8005 from lilo !xing.openprojects.net!! Received :lu.openprojects.net SERVER jordan.openprojects.net from lu.openprojects.net !?! !jordan.openprojects.net!! Remote CONNECT xing.openprojects.net 8005 from lilo -:- smkl [sami@MCV.rdyn.saunalahti.fi] has joined #tunes -:- mode/#Tunes [+v smkl] by Tril -:- FAYRI [jo@gardeny.udl.es] has joined #Tunes -:- mode/#Tunes [+v FAYRI] by Tril -:- FAYRI [jo@gardeny.udl.es] has left #Tunes [] -:- andrea [jfontecham@195.235.168.242] has joined #Tunes -:- mode/#Tunes [+v andrea] by Tril hi! 11:40am -:- andrea [jfontecham@195.235.168.242] has left #Tunes [] lo! GMOL: if you can't make sense of programs, i.e. prove things about them, then you can only safely do trivial manipulations on them. So that useful metaprogramming implies a clean formal proof system inside the system. Since Reflection is but the fixpoint of metaprogramming, so does it. 11:50am -:- andrea [jfontecham@195.235.168.242] has joined #Tunes -:- mode/#Tunes [+v andrea] by Tril -:- andrea [jfontecham@195.235.168.242] has left #Tunes [] I see...a proof checker can be seen as something that accurately determines a programs function, so that it know what it does and can operate with (hook it to something else, put it in it's toolbox for carrying out a task etc.)..yes? 12:20pm /back /back /bac stupid 12:40pm -:- SignOff Tril: #TUNES (Disconnecting) -:- Tril [dem@sloth.wcug.wwu.edu] has joined #TUNES -:- mode/#Tunes [+o Tril] by ChanServ -:- binEng [bineng@dialup122-1-29.swipnet.se] has joined #tunes -:- mode/#Tunes [+v binEng] by Tril hi there niihau, binEng * binEng/#tunes looks at abi with an annoyed look 01:20pm -:- SignOff GMOL: #TUNES (Leaving) For a totally meaningless (but graphical and fun) account of how I and my sister made muffins earlier today, look at http://home7.swipnet.se/~w-71548/muffins/ -:- SignOff binEng: #TUNES (Leaving) -:- AlonzoTG [Alonzo@client-151-200-127-25.bellatlantic.net] has joined #tunes 02:30pm -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) -:- _QZ [brand@p0wer.qzx.com] has joined #tunes -:- mode/#Tunes [+v _QZ] by Tril hi _QZ 03:20pm * Fare/#Tunes is back hey Fare hum. bespin looks like it's down. is it, to you? <_QZ> bespin isnt down 03:50pm my route to it is down :( <_QZ> bummer -:- tcn [tcn@cci-209150250125.clarityconnect.net] has joined #tunes -:- mode/#Tunes [+v tcn] by Tril <_QZ> need something from it? my mail :) happily, fwprc is my friend :) <_QZ> fwprc? read the Firewall-Piercing mini-HOWTO :) <_QZ> i can give u an account on borg and u can telnet to bespin <_QZ> might be a little slow tho :) I already have an account on a machine that can see bespin. But I appreciate your offer. hey guys <_QZ> hey tcn I finally played halflife :) <_QZ> kewl game eh? we had a big killfest in the college lab <_QZ> > if killing is a sin and being gay is also a sin, is it a sin to kill a <_QZ> > fag? <_QZ> are you asking this in sarchasm or truth? I think I already know. <_QZ> You are an honorable person, although comical. <_QZ> u see those damn missionary ppl cant give a straight answer haha the answer is simple, killing is worse <_QZ> but a fag is not a person in the eyes of the church wow that's hypocrisy for ay 04:00pm well, I gotta leave the phone open <_QZ> where does the mormon church stand on this? is it ok to hunt animals, for food, if yer a mormon? gay people are animals to the church arent they? so if u eat a gay person after killing them is that ok? <_QZ> i just emailed him again :) haha stick a spit up their ass and roast 'em on a fire <_QZ> heh <_QZ> so u get anything done on retro? maybe they'll say it's ok as long as you don't eat the genitals retro? nope. I guess I'll get Forth so it can compile programs, then do multitasking. <_QZ> i think i will work on brix tonight <_QZ> hopefully finish the kernel I can't believe April 1st was 2 weeks ago Seems like yesterday hey, yesterday, I met a great guy. I asked him if he was married, but he said he had had a friend, but had parted from him. The guy was so great, I thought that if I were a homosexual, I'd try to hook him. <_QZ> heh whats that suppose to mean :) <_QZ> Fare: thats just sick April 1st is 350 days from now. 04:10pm another way to look at it is: if great guys like him are homosexual, this lowers competition to catch women, which is good for us remnant heterosexual guys. tcn: someone just mailed me about eForth 1.0c Fare: what did they say? <_QZ> Fare: did u make eforth? why would some1 email u about it? tcn: just asked me why it didn't work anymore. I replied: because of ELF. QZ: I "ported" it to linux, in the good old days. <_QZ> ahh six sick sikhs seek sea ski see ya's <_QZ> cya -:- SignOff tcn: #TUNES (tcn has no reason) -:- Iepos [root@d7.t1-7.tecinfo.com] has joined #TUNES -:- mode/#Tunes [+v Iepos] by Tril anyone here? <_QZ> ya greetings. how's brix coming? hey, what did you decide on the string size issue? Hey, it's not june! ??? <_QZ> string? size issue? April, in Paris! i thought earlier you were trying to decide how the size of strings would be terminated ... ? null-terminated or prefixed with a size ... <_QZ> oh that was tcn ooops retro soorrry i get mixed up sometimes :-) hey Fare, have you read my doc on the logic system? 04:20pm ~iepos/proposal.html? yes... that's the one... yeah, very good paper. I think I wrote something similar, somewhere on the tunes list. really ... (too lazy to dig the archives) what do you think of turning the computation into a reduction problem? and your use of illative combinatory logic is just the same as my masters thesis and lambdaND works. not sure what you mean "reduction problem" i once wrote a combinatory logic reducer, but it was not too efficient. -:- Closing Link: TUNES[bespin.cx] by tolkien.openprojects.net (Ping timeout for TUNES[bespin.cx]) -:- Connection closed from irc.us.openprojects.net: Success -:- Use /Server to connect to a server -:- Connecting to port 6667 of server clarke.openprojects.net [refnum 1] -:- BitchX+Deb1an: For more information about BitchX type /about -:- Welcome to the Internet Relay Network TUNES -:- Your host is clarke.openprojects.net[blueberry.inwa.net], running version u2.10.04.resolv9.nmt.egcs4.tok.pten.tlim4.admin.upper4.whisper3.gipl.modeless7 -:- This server was cobbled together Mon Jan 25 1999 at 07 12:10 EST -:- clarke.openprojects.net u2.10.04.resolv9.nmt.egcs4.tok.pten.tlim4.admin.upper4.whisper3.gipl.modeless7 dioswkfcg biklmnopstv -:- [local users on irc(14)] 5% -:- [global users on irc(101)] 38% -:- [invisible users on irc(166)] 62% -:- [ircops on irc(12)] 4% -:- [total users on irc(267)] -:- [unknown connections(0)] -:- [total servers on irc(33)] (avg. 8 users per server) -:- [total channels created(73)] (avg. 3 users per channel) !clarke.openprojects.net Highest connection count: 27 (26 clients) -:- Mode change [+f] for user TUNES -:- Mode change [+iws] for user TUNES -:- JOIN activated by "TUNES #tunes tunes@bespin.cx " -:- TUNES [tunes@bespin.cx] has joined #tunes -:- Topic for #TUNES: Reflective Computing System -:- topic set by Fare [Fri Apr 16 06:46:49 1999] -:- [Users(#tunes:8)] [ TUNES ] [vIepos ] [v_QZ ] [@Tril ] [vsmkl ] [vFare ] [vtimestamp ] [ abi ] -:- mode/#tunes [+v TUNES] by Tril -:- Channel #tunes was created at Sun Feb 28 08:48:06 1999 -:- BitchX+Deb1an: Join to #tunes was synced in 7.629 secs!! -:- Mode change [-s] for user TUNES hmm ... Fare, are you still here? <_QZ> http://www.qzx.com/clinton.txt that's mean ... :-) what's wrong, you don't like clinton? :-) at least he can't be elected again maybe next election everyone will vote Libertarian ... (yeah right) 04:30pm hmm ... i wonder where everyone has gone. -:- jason [jason0077@148.237.39.35] has joined #Tunes -:- mode/#tunes [+v jason] by Tril greetings -:- AlonzoTG [Alonzo@client-151-200-127-200.bellatlantic.net] has joined #tunes -:- jason [jason0077@148.237.39.35] has left #Tunes [] greetings alonzo <_QZ> i vote libertarian every election <_QZ> never won tho :( really ... heh heh . Iepos: if you read lambdaND, you'll know that sadly, you must have non-determinism to have illative combinatory logic. <_QZ> ya im libertarian Fare: why? or maybe i should just read it. iepos: and that there is no possible efficient implementation (no possible efficient *complete* implementation) well i don't really need _illative_ combinatory logic anyway all i want is S and K. then, get Haskell :) at least that is all I need to make the logic system probably... <_QZ> why just S and K, what about U and C or one of those "optimal reduction" lambda-calculus implementations QZ: what do you call U and C? <_QZ> they go between S and K :) of course, without U, you can't make logical statements ... i was just planing on using pure combinatory logic (no U) as a low-level implementation for the logic system (which could have logical statements) ... if you can make logical statements, it's an illative combinatory logic. yes, the logic system itself will be illative then, i guess. 04:40pm Iepos: you cannot implement illative CL w/o non-determinism what exactly do you mean by non-determinism? a choice operator U A B -> A ; U A B -> B A or B A \/ B yes A \cup B A \vee B write it as you wish. wait ... that would be your "U" is conjunction. if it implies A and B. ? -> here was reduction, not implication oh... (Curry's implication combinator is P) have you read Curry's book? nope :-) i should... what's it called? Combinatory Logic ? oh... aptly named. volume I and II. i still don't understand though ... i think i can see how the logic system could be implemented using only pure S/K reduction. Iepos: depends on what you mean by "implemented". Iepos: cannot be a faithful implementation w/o choice. -:- lar1 [larman@153.37.12.242] has joined #tunes -:- mode/#tunes [+v lar1] by Tril Iepos: which I prove in lambdaND hey i mean that a system for finding a desired conclusion, given a set of desired conclusions and a set of premises and inference rules could be found... that would be the "implementation" of my logic system if it could find a desired conclusion, and get it into a usable form with only S and K you can build a system for verifying, but not a system for finding. actually, you could emulate choice by explicit search. om (I read yer message) my algorithm was simply to try each possible application of an inference rule in a recursive search hi, Alonzo... what did you think? note that to fully search means a breadth-first traversal what do you mean by "breadth-first" I think that you aren't respecting the limits of logick... something awfully inefficient when the search space is as large as among all programs. logick just doesn't do that kind of stuff... I know it is... but it could be done ATG: uh? fare, I mean the search would complete eventually... given enough time using only S and K reduction it could find a desired conclusion (centuries) Iepos: you should read Kolmogorov complexity theory to understand just _how_ terribly inefficient that inefficient means! it would certainly be very very inefficient i know, but doesn't it still prove that non-determinism isn't necessary? 04:50pm or is this an "emulation" of non-determinism you were talking about? depends on "necessary". necessary to *what*? necessary to find the desired conclusion. wait, it doesn't take nearly this complex of an example... How about this, given "X -> Y" an "Y -> Z" in an illative combinatory logic, the conclusion "X -> Z" can be easily found by a human. have you understood the notion of high-level vs low-level ? is the human using non-determinism? understood the notion of high-level vs low-level? I guess... 05:00pm maybe that was not a good example actually... anyway ... where are you Fare? -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) anyway, I wasn't planning on actually doing the search ... only translating the process into pure combinatory logic, which can hopefully reduced with some optimizations that allow it not to search the whole space... 05:10pm fg ls aack 05:30pm i do not like unix . :-) where is everyone it has been said that everyone is gone again :~( :~( !varley.openprojects.net!! Received :sterling.openprojects.net SERVER lu.openprojects.net from sterling.openprojects.net !?! -:- SignOff Iepos: #TUNES (Iepos) 05:40pm -:- NetSplit: carter.openprojects.net split from koontz.openprojects.net [05:42pm] -:- BitchX+Deb1an: Press Ctrl-F to see who left Ctrl-E to change to [carter.openprojects.net] -:- Iepos [root@d15.t1-7.tecinfo.com] has joined #TUNES -:- mode/#tunes [+v Iepos] by Tril -:- SignOff Iepos: #TUNES (Iepos) -:- _QZ [brand@p0wer.qzx.com] has joined #tunes -:- mode/#tunes [+v _QZ] by Tril -:- SignOff smkl: #TUNES (smkl has no reason) -:- AlonzoTG [Alonzo@client-151-200-121-151.bellatlantic.net] has joined #tunes -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) !driz:*! pardon the unannounced hiccup.. had to do an emergency router reboot =) !lilo:*! run that one by me again? :) !lilo:*! oh, ic, nevermind :) -:- ^lilo [lilo@varley.openprojects.net] has joined #tunes -:- mode/#tunes [+v ^lilo] by Tril <^lilo> hi all <_QZ> hi <_QZ> is timestamp yours? -:- ^lilo has changed the topic on channel #tunes to: Reflective Computing System * ^lilo/#tunes nods <^lilo> it's for some server name changes we're going to do <_QZ> name changes? 11:00pm -:- SignOff _QZ: #TUNES (BRiX [http://www.qzx.com/brix] :: sleep) -:- hcf [nef@me-portland-us822.javanet.com] has joined #tunes -:- mode/#tunes [+v hcf] by Tril -:- hcf has changed the topic on channel #tunes to: Reflective Computing System , Beyond Ada: The First Paranoid Programming Language -:- SignOff hcf: #TUNES (Leaving) [msg(TUNES)] newlog 1999.0417 IRC log ended Sat Apr 17 00:00:01 1999