IRC log started Sat May 1 00:00:00 1999 [msg(TUNES)] permlog 1999.0501 -:- SignOff Tril: #TUNES (Ping timeout for Tril[sloth.wcug.wwu.edu]) -:- Tril [dem@sloth.wcug.wwu.edu] has joined #TUNES -:- mode/#Tunes [+o Tril] by ChanServ !mccaffrey.openprojects.net!! Remote CONNECT drexelhill.pa.us.opirc.nu 8005 from lilo -:- teka [jorge@195.77.175.235] has joined #Tunes hola 05:40am -:- teka [jorge@195.77.175.235] has left #Tunes [] -:- smkl [sami@MCCCIII.rdyn.saunalahti.fi] has joined #tunes -:- Iepos [root@d12.t1-7.tecinfo.com] has joined #TUNES -:- AlonzoTG [Alonzo@client-151-200-125-145.bellatlantic.net] has joined #tunes -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) -:- tcn [tcn@cci-209150250104.clarityconnect.net] has joined #tunes hey Anyone really here? >>> tcn [tcn@cci-209150250104.clarityconnect.net] requested PING 925569530 494071 from #tunes 07:40am hello hello. 07:50am >>> tcn [tcn@cci-209150250104.clarityconnect.net] requested PING 925570969 604947 from #tunes oops, forgot I was still on here :) time? it has been said that time is 08:05:29 1999 08:10am -:- SignOff tcn: #TUNES (tcn has no reason) -:- AlonzoTG [Alonzo@client-151-200-120-227.bellatlantic.net] has joined #tunes -:- SignOff Fare: #TUNES (Ping timeout for Fare[quatramaran.ens.fr]) -:- Winchip [IDT@ppp03-245.algx.iadfw.net] has joined #Tunes -:- SignOff Winchip: #TUNES (Read error to Winchip[ppp03-245.algx.iadfw.net]: EOF from client) >>> Tril [dem@sloth.wcug.wwu.edu] requested PING 925582616 784685 from #TUNES hi Tril y0 -:- tcn [tcn@cci-209150250106.clarityconnect.net] has joined #tunes greetings howdy.. what's going on? * AlonzoTG/#tunes greets "Salutations tcn!" :-) topick? 11:20am alonzo, weren't you trying to learn lambda-calculus a while back? yepers... I have been reedin up on Lishp reciently... insteresting lingo... :) i wrote an introduction to it... you can get it at www.tunes.org/~iepos/lambda.html if you want. kool.. I mite take a gander in a few daze... it also covers combinatory logic a little. awesome! :) anyway... oops i forgot just a second it's not there yet :-) -:- HUGO [kikebass@hmo1-60.telmex.net.mx] has joined #Tunes hi Hugo buenas dias hi tril que ondas gotta finish reading the Arrow paper.. I'm on page 5 no hablo espanol bien :) its slo reedin... don't understand much of it... AlonzoTG: me either Okay... I like retro... -:- pasko [pasko@195.235.116.164] has joined #Tunes but I don't really understand it yet... I think kernel protection is a high priority for me... you mean, protection from user programs? I was thinking of instead of using interprited drivers... I mean so drivers don't crash the system... hi, pasko 11:30am -:- pasko [pasko@195.235.116.164] has left #Tunes [] bye :( In my system drivers will be implemented as protocol scripts in a "Device Interface Language" umm, I just posted a message saying I *don't* want kernel modules protected from each other... too slow Or use a trusted compiler to run them... That's a goal of Tunes proof-checking -:- SignOff HUGO: #TUNES (Ping timeout for HUGO[hmo1-60.telmex.net.mx]) like say DEFINE "ReadFloppyDrive" : output x; wait untill Y; Input Z... atg: so your "kernel" will have a compiler/interpreter in it? Then the OS will have a usable interface to the floppy drive that can't cause any problems because everything is safe... It will have an internal interpriter to run device scripts. Externally the compiler will probably be a module inside the persistant storage module... I think you'll find it's a bad idea to have a bunch of special languages not really sure... Hmmz... maybe... look at Unix heeh Anyway... that's what my prototype will find out... In Unix, you have to use shell scripts and crap a lot.. in Tunes you could use a real language like LISP or ML as your "script" language hmmz... -:- Tremebundo [kikebass@hmo1-60.telmex.net.mx] has joined #Tunes hi, Tremebundo -:- SignOff Tremebundo: #TUNES (Leaving) AlonzoTG: http://tunes.org/~tcn/retro/doc/faq.txt that'll clear things up a bit k look at the bottom 11:40am k -:- _QZ [brand@p0wer.qzx.com] has joined #tunes qz! I heard you were gonna release brix today <_QZ> yup 11:50am <_QZ> a kernel binary, linux source to the utilities to make an ofs image and add objects to it, and the api to write your own methods does it wokr with hard disks yet? is there an interactive interpreter or debugger? <_QZ> Tril: why would i want it to have ide support yet because floppies suck <_QZ> Tril: when it has ide/scsi support i will personally tell u. so u can stop asking me that everyday <_QZ> tcn: i kinda havent been working on brix for the last 2 weeks so i kinda didnt get all that finished are device drivers written with that api? <_QZ> yes so theoretically someone could add ide support :) we might get some synergy between brix/retro/clementine <_QZ> drivers are methods too and they too must use the same api that all other methods use hey, can anyone tell me how to get pine or elm working on my machine? what OS? iepos what distro slackware linux did you install one of them i've tried... but i can't seem to convince it to get the mail from my server, mail.tecinfo.com <_QZ> all u need to do is write a few methods for the ide device and then tell the startup method to add those to the kernel instead of the floppy methods yeah, actually i installed both. does that server have imap? what's an imap? pop3? ummm.... i don't know. just use fetchmail to download your mail to your home system. okay, i've never used that before... let me see... hmmm...... check if you have it installed, then make a .fetchmailrc to tell it how to download mail from your account all right, i'm looking at the man page now. 12:00pm <_QZ> is there an instruction that converts a linear address into a physical address I HATE RC files!!!!!! hmm... i keep getting a "STMP transaction error" lods*? i mean smtp iepos: what mail transport agent (MTA) are you using? sendmail? qz: I don't think so i'm using fetchmail. is that what you're asking? no. fetchmail will get the mail to you. that's for reading your mail. If you get an SMTP error, that is because you are trying to SEND mail. You need a different program to do that.. can you read mail? no. here, this is what i get... iepos:~# fetchmail -u magister mail.tecinfo.com Enter password for magister@mail.tecinfo.com: 19 messages for magister at mail.tecinfo.com (73267 octets). skipping message 1 not flushed reading message 2 of 19 (599 header octets) fetchmail: SMTP connect to localhost failed: Connection refused fetchmail: SMTP transaction error while fetching from mail.tecinfo.com fetchmail: Query status=10 iepos:~# hmm... why is it trying to connect to localhost? qz: nope.. there's no instruction iepos: it's trying to deliver the mail oh i need sendmail or something running? with that setup, yes qz: you can manually walk the page tables (looking at sendmail manpage)... 12:10pm hmm ... it looks like sendmail is only for sending mail. don't i need some sort of daemon running to receive the mail? qz: sendmail does that too err, iepos qz: AND and MOV execute fast, usually 1 cycle.. uh oh. sendmail is complaining about missing configuration file. iepos: sendmail listens on port 25 for incoming SMTP connections, to receive mail meant for your local system. If you're on a PPP connection, no one will probably be able to send mail this way. Fetchmail gets mail from a remote mail server and delivers it to sendmail through the port 25, so it thinks it's coming from a remote system okay... now i just need to get sendmail working. iepos: darn you set a root password <_QZ> i am trying to find a fast solution to this, so "walkingthe page tables" is out or i could have fixed it qz: don't YOU decide what linear address goes to what phyiscal address, since you're the OS designer? And you PUT those in the page tables? <_QZ> i no longer use a direct mapping qz: seen the linux mm ? qz: you just have to use a few ANDs and MOVs.. that's fast. they use some nifty tree for fast lookup ah ha! sendmail -bd uh oh # sendmail No local mailer defined <_QZ> and what i need this for is to copy stack parameters from the current stack to the stack of a new thread, which is not mapped into the current page directory <_QZ> tcn: how so hmm, odd. Slackware usually defines the local mailer as "deliver", and that's included with the sendmail package. iepos: do you even have a /etc/sendmail.cf installed? no :-) iepos: go get one out of /usr/doc/sendmail and copy it there i need debian. it probably sets this all up for me! <_QZ> oops, i asked my question wrong, i meant physical to linear iepos: did you run netconfig? qz: oh, u can't hmmm... i don't think so. maybe that would work <_QZ> er, wait now im confused iepos: it asks you your hostname, and which sendmail cf you want <_QZ> i dont know what i need :) qz: well it would be slow qz what are you trying to do? yes... i've used it before... forgot to run it again last time i reinstalled 12:20pm it should run automatically in the configure stage if you installed sendmail THIS is why I don't use LiNuKs :P atg: which distro did you try? Tril: he tried the crappy one :) (the one that makes linux look bad) <_QZ> heh slackware's not crappy, it is meant to teach you how to configure linux :) the hard way <_QZ> haha redhat is meant for newbies who don't care how to configure linux. and if you try you're screwed he told me he tried redhat 554 No local mailer defined <_QZ> doesnt matter what u say about redhat, its still #1 I tried redhat once too, then I went right back to slackware, and finally debian this year <_QZ> and redhat is still the ONLY distro that has investments by the corporate world if the corporate world gave money to debian it would be a donation not an investment hmm, any idea how to "define the local mailer"? what's eggdrop? eggdrop is uncomprehensible iepos: there is a line in sendmail.cf starting with "Mlocal" uh oh... netconfig didn't do anything to sendmail.cf abi, eggdrop is also an irc bot okay, Tril. so, no. iepos, there's another config for sendmail.. really, what is it? /var/adm/setup/setup.sendmail joy, it works ! i have all these messages popping up it all my terminals and annoying beeping sounds! thank you so much, tril put "biff n" in your login script or delete biff Iepos: now learn to stop using root all the time kill comsat well, if i stop being root all the time, then i'll always have to su 12:30pm just leave a terminal logged in as root X is a pain though.. if you su root in an xterm, it won't let you run X programs unless you do a bunch of complicated crap :) i agree it would be nice to have another user for when I telnet in remotely (which i almost never do). (say, anyone know how to do it?) tcn probably need to add root to the user's xauth hey, that reminds me, i've never gotten remote X programs to work. i always get "connection refused". I guess my local x server doesn't trust the incoming connection Tril: See, that's the problem w/ X, it's too damn hard to manage :) hmm, i guess xauth is probably the solution ... on the box you want the window to popup, type xhost +host.name ahhhhh! on the host.name box, in bash type "export DISPLAY=host2.name:0.0" yes, i'd gotten the DISPLAY set okay, but it should work now with xhost hmmm, by the way, do you know of any good xservers that run on top of windoze? cygnus X-Win32 is installed at my uni.. works fine hmmm ... i'm going to have to check that out i gotta go later thanx, Tril. -:- SignOff Iepos: #TUNES (Leaving) 4 pages left... gasp... wow Well I gotta get something done today see ya ok phew lunch * Tril/#TUNES is away: (afk) [BX-MsgLog Off] 12:40pm -:- SignOff tcn: #TUNES (tcn has no reason) -:- SignOff AlonzoTG: #TUNES (Ping timeout for AlonzoTG[client-151-200-120-227.bellatlantic.net]) -:- AlonzoTG [Alonzo@client-151-200-125-105.bellatlantic.net] has joined #tunes :/ my 'puter shorted out. :(((( <_QZ> HAHAHA 01:10pm sekund time zat happened.. ;((( hey, when your computer is 4 years old; we'll see who's lauhging!!!! 01:20pm -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) -:- NetSplit: clarke.openprojects.net split from sterling.openprojects.net [01:40pm] -:- BitchX+Deb1an: Press Ctrl-F to see who left Ctrl-E to change to [clarke.openprojects.net] -:- Netjoined: clarke.openprojects.net sterling.openprojects.net -:- Tril [dem@sloth.wcug.wwu.edu] has joined #TUNES -:- mode/#Tunes [+o Tril] by ChanServ -:- abi [nef@bespin.cx] has joined #Tunes -:- Tril has changed the topic on channel #Tunes to: http://tunes.org -:- ChanServ has changed the topic on channel #Tunes to: http://www.tunes.org - Free Reflective Computing System >>> Tril [dem@sloth.wcug.wwu.edu] requested PING 925599310 605821 from #TUNES -:- SignOff smkl: #TUNES (sleeping ...) -:- Iepos [root@d2.t1-4.tecinfo.com] has joined #TUNES yo yo hey, i still can't send mail receiving seems to work pretty much okay, though. I get an error "cannot find /usr/bin/uux: no such file or directory" you probably set up sendmail to use the UUCP config. Use SMTP instead. hmmm... 04:20pm maybe some option in sendmail.cf ... then again, maybe i need to run setup.sendmail again. it was from the setup.sendmail. don't choose the uucp option. oops -:- tcn [tcn@cci-209150250122.clarityconnect.net] has joined #tunes -:- SignOff Iepos: #TUNES (Leaving) tcn 04:30pm hey hello, tcn -:- Iepos [root@d6.t1-4.tecinfo.com] has joined #TUNES Tril, still there? ya tril, I don't see the problem with your object ID's in your typesystem.. there's one small problem. I don't always have the same hostname... because i dialup to my ISP. does that mean i do need UUCP after all? no, I have dynamic IP too hmm, well every time i send a message, i get an error: "sender domain must exist" it actually changes /etc/HOSTNAME? in pine set the sender-domain to some valid domain. but the user you run pine as, must be the username at the domain you give. oh, it doesn't what domain? so if you want to send mail to appear from iepos@tunes.org, make an account iepos on your box and set his .pinerc to say the user-domain is tunes.org. Then all mail will say From: iepos@tunes.org. Make sure you test it out real good. Make sure a message sent to "root@localhost" or just "root" goes to your machine, not your ISP i never had that happen with slackare hmm, but i do need reply messages to go to my ISP... I did when I switch mailhandler's :) then I got debian iepos: I don't understand what you just said what's a reply message? me neither :-) well i don't want people to reply to iepos@tunes.org because i don't have an email account there. i want them to reply to my ISP. i was just gonna say.. i created iepos@tunes.org, I guess because I forgot to earlier. what is your username at the ISP? "magister" @tecinfo.com you're on the member list at tunes so you get an email there oh... actually i'll probably just start using iepos@tunes.org make an account "magister" and set the user-domain in pine to tecinfo.com then. all right i get the idea, let me try... that's kind of annoying. that means i can't be root all the time! hmm , is there some way to trick pine? no, it's GOOD, you shouldn't be root all the time. heh heh all right okay let me make a new account and fix all my file permissions yeah, if you make a mistake as root, you can screw your whole hard drive 04:40pm or if you ran a trojan horse or virus (which are rare in Unix, but definately possible...) how do I make programs dump core go figure still, trojan horses can still do big-time damage. they can still wipe out all your user files, although maybe not your whole system if you're not root. I used to use trojans to trick administrators into giving me their pw :) but that's only an issue on servers * Tril/#TUNES cds to tcn's directory and types login or su or telnet :) If you take '.' out of your path, you won't run any trojans i guess I dont have . in my path debian leaves it out by default anyone know how to use gpg nope gpg: Warning: using insecure memory! uh oh, now it wants "metamail" what is metamail? stuff for file attachments mime aack... so why is sendmail looking for it? 04:50pm because it should be installed hmm... but it's not... let me see if i can find it Hey, there was a CERT advisory for metamail: A sender of a MIME encoded mail message can cause the receiver to execute an arbitrary command. If the attacker has an account on the ... fixed I hope :) the latest sendmail doesnt have that okay i have metamail, but now it says "relaying denied". good. what is relaying? spammers use it okay does that mean i'm a spammer ? :-) relaying means sendmail will process mail destined for a non-local domain and will send it yeah.. spammers use it to try to be anonymous umm, but i do need to be able to send mail to non-local domains. it should let local domains send to non-local domains just a minute i got mail from you really? why is your hostname iepos.tecinfo.com? is that right? maybe if you update the IP in /etc/hosts every time you connect, it will fix sendmail hmmm this is really confusing me :-) i guess my hostname should be iepos.tunes.org if i am getting mail from tunes.org ? no it doesn't matter whta your hostname is no one on the internet will see it unless they look at all the mail headers 05:00pm man, I've been making all kinds of stupid mistakes.. stosb instead of movsb! oops iepos:what's in /etc/hosts? let me see 127.0.0.1 localhost 127.0.0.1 iepos iepos.tunes.org hmmm, i can send mail to tunes.org but nowhere else. now you must have set the domain of your machine to tunes.org. don't do that. make up a domain name that doesn't exist for your machine okay hmm wait this is getting me confused. never mind do you care if you have to be online in order to send mail? not really well, why not just tell pine to use your isp's smtp server for sending then your local one doesn't have to work umm ... i guess i'll try that hey, what's the command to send all queued mail immediately? send a SIGHUP to the daemon joy, i think it works. it will restart and process the queue killall -HUP sendmail I should put that in my ppp-on i set my sendmail to queue all mail, and i dont run the daemon except when i'm connected. and when it's online it uses a queue time of like 1 min i think everything works now. but i still have use "fetchmail" to get my mail. is there a way to make pine do this? iepos try this, in pine hit G, then type {mail.tecinfo.com}iepos and hit enter 05:10pm what's that? if it works it will ask for a username and password, if it doesn't, it will wait a while and have a connection error it umm sort of works thats the syntax for pine to use remote IMAP folders it asks for username and password but then says "can't find folder ..." try "{mail.tecinfo.com}INBOX" or inbox lowercase both should work yes that works, but it asks for my username and password twice wait but that doesn't download the messages to my machine. correct. you can set that to be your inbox, then you won't even have to download them to your machine. i mean your default inbox when you run pine hmmmmm i use fetchmail with procmail for a delivery agent because I sort my mail into folders plus reading mail remotely is slower okay, it works for {tunes.org}inbox too. you can obviously use the Save command to move messages between mailboxes i prefer using .forward to do that though hey, anybody can unsubscribe anybody. if they use the web form, yeah heh heh Not like it matters didn't it send you a note that said you got unsubscribed? then you can just resubscribe yourself It's better than giving you a password for every mailing-list 05:20pm yes it did give a note. i guess it's not a real problem. if someone unsubscribes you, you could just resubscribe again. you can always check the archives for anything you missed ah the manpage for gpg says the insecure memory warning is because I didnt setuid the file yet. debian has this paranoid system for tracking all setuid programs. if you don't register a program with it, it seeks out and unsetuids anything it doesnt recognize tril, is there someone to tell pine to automatically enter my username and password? i have no idea okay, i'll just type it in every time... fetchmail does it automatically and it can do both tunes.org and your ISP go find pine.doc on www.cac.washington.edu/pine actually ... i think i'm getting kinda tired of playing with my email account :-) 05:30pm tril, you familiar with 386 multitasking (at a low level)? ... i read the 386 programmer's reference several times i'm pretty familiar ok, I'll ask you if I need another brain :) (I bought that book beacuse it was the only book I could find with complete opcodes. ASM books without opcodes are useless, how are you supposed to write your own assembler?) EVERY ONE of the books on C=64 asm had all the opcodes in it.. Intel's 386 manual seems better than 3rd-party manuals much more direct What cpu did the c64 use? 6510, of the 6502 family did the c128 use something newer? the 8-bit NES and apple ][ also used 6502s not sure the 64 was pretty cool, for its time had nice sound & graphics /who #tunes 05:40pm allright, how to do the initial task switch.. -:- SignOff tcn: #TUNES (tcn has no reason) oh wow. PINE starts for "Program for Internet News and Email" i always thought it stood for "PINE Is Not ELM" they changed it really, why? hey did that beep work? what beep? darn how useless. /beep just makes a local beep. i guess... ctrl-g often beeps on both ends  sending me a msg will beep my end, too really, what irc client are you using? bitchx oh i'm just using "irc". is there some way to make it beep, do you know? 05:50pm i usually just check back from time to time to see if anyone's said anything. nope try this: /ON MSG * BEEP but it puts "*"s before and after your name then msg yourself You may not type ON commands when you have the NOVICE variable set no ON . :-) ha ha some ON commands may cause a security breach on your machine ... well stop being root, then unset the NOVICE variable :) okay oops i'm still root just a sec -:- SignOff Iepos: #TUNES (Iepos) -:- iepos [iepos@d6.t1-4.tecinfo.com] has joined #TUNES all right, now i'm "safe" you will want to put common commands in your .ircrc okay i think the beep thing will work now. try it. yes it worked. hmmm, also how is it that people send messages like "Iepos laughs out loud" where it doesn't say who it's from? i dunno hmmm * Tril/#TUNES generates entropy yes, like that. oh the /me command :) * iepos/#TUNES tries using the /me command okay, so the first word has to be your name. you can also do a fake "return" so it looks like you are writing the beginning of someone else's line. floo foo i forget how. hmmm hmm, so how do you send a message so it comes up with "*"s around your name? /msg nick something to say here okay, so it's private message i guess. yes btw, have you looked at my proposal for implementing TUNES yet? let me look at it again. yeah, i changed it just a little... 06:00pm the second to last paragraph sort of rambles... i need to fix it... reading <_QZ> iepos: where? www.tunes.org/~iepos/proposal.html hmm i dunno is it confusing? it seems to me that having a logic system capable of representing a specification of TUNES, would have to be tunes itself i worry about that also but i was hoping (as mentioned in the last 2 paragraphs) that the problem could be easily transformed into a combinatory logic reduction problem. however, perhaps the reduction problem can only be solved by a tunes itself. i'm not sure 06:10pm i still want to talk to you about the types, though.. you say types can be emulated using predicates yes can you still type the predicates, then? analagous to the way multiple-parameter functions can be emulated using currying using other predicates can you type the predicates? well, you could make types that contain predicates, yes. ok, so if there are no types, what are objects? for instance, the type of all false predicates would be "x.!x" (where . is a lambda abstraction) objects... i.e. the things that you mentioned, which are not functions, but can be passed as arguments to functions ahh... you can use symbols to represent any concepts... i don't think that answers your question. i don't know what you mean by symbols in functions, I use objects instead of symbols. i.e. abstract, unnamed entities i mean simply sequences of characters. actually symbols could be other things as well in my implementation, symbols will be sequences of characters probably yes, i make no limitations on what a symbol can stand for they don't have to represent functions hmm, does this answer your question? in an intensional system, symbols are optional. instead, use direct links between wherever the symbol was and the thing the symbol stands for you can still name things by having a link to a sequence of characters , but you don't need it i think i understand what you're saying, but in order to _express_ a concept you're going to need symbols. express it where? but not every concept needs to have a unique symbol. Some concepts could be represented using function application trees ... well, in order for me to express a concept to my computer, i'm going to need some sort of symbols. a "direct link" isn't an option. the computer could then reason about the concept using whatever symbolism it wanted... you don't need a symbol, if everything in the system is built out of direct links you only need a symbol if you want to separate out part of the system and move it to another system that you can't access through direct links 06:20pm yes... any sort of communication will require symbols. They may be low-level symbols though, what you call "direct links". I have no idea what we're talking about. me neither :-) let me look back at your original question... so what you are saying is that arguments, and return values, are symbols? all i'm saying is that reasoning will be done in my system about abstract concepts, represented using symbols. arguments, return values, everything will be represented using simple symbols (strings of characters), or possibly a function-application tree with symbols at the nodes let me think of an example to clear things up ... suppose i want to reason about my grades at school... I want to state that i'm making good grades... I also will state that if i'm making good grades, then I will succeed. This could be done using my system by choosing a symbol to represent my "making good grades", say M. Then choosing another symbol for succeeding, say S. then the first statement (i'm making good grades) can be represented is my system using symbol M. the other statement (if i make good grades i'll succeed) could be represent using 'M -> S' M and S are symbols. "M -> S" isn't really a symbol in the sense i've been using it; it's a function application tree. hmm did that help? well, the point of a symbol is to be different from any other symbol, right? yes well, actually having symbol X and Y doesn't imply that X and Y aren't the same... they could be, but they aren't necessarily symbols are just used to represent concepts well, I use symbols, but they are handled entirely by the system, they don't have character strings associated with them (they dont NEED strings associated with them) i'm not planning on a full TUNES system being restricted to just strings for symbols sounds, pictures, anything could be used for symbols but for my initial bootstrapping logic system, i'm going to stick to character strings for symbols. why use symbols at all? how else can you communicate? how will i be able to describe the TUNES system without symbols? 06:30pm communicate with the computer by directly manipulating the internal data structure of the system. i'm talking about the "user"-interface though. that isn't an option. I need to give a description of the TUNES system to my logic system. why can't it be an interactive user interface, that lets you edit the internals of the system? it could (that would make it more complicated; remember i'm only talking about a bootstrapping system), but the concepts would still have to be represented using some sort of symbols. in my previous example, how am i going to tell the system M and M->S without using symbols? they are represented using UNIQUE IDs which, as in my specs, I explain are completely hidden. they have the same functionality as a symbol but there's no arbitrary name required for them well, there is an arbitrary name, that's the unique id. But I want it hidden, so i don't see it. still, remember i am talking about a way for bootstrapping TUNES (not TUNES itself)... are you really recommending these unique IDs for my bootstrapping system. ? remember i do not need to worry about distributed computations or anything. no, i'm not talking about bootstrapping yes, that's our problem. We're talking about 2 different things :-) i'm talking about what the system will be like when it's running. and I asked you what gets passed into functions and you said symbols. Is this true after you are done bootstrapping? I agree that concepts should not have a fixed arbitrary name. I haven't actually really done much thinking at all about a finished system. then how are you going to bootstrap it, if you don't know what it is? heh heh good question. actually i have done some thinking. I will probably still use a similar system for expression facts in a finished system too. similar to what, my system or yours mine :-) although actually a lot of what you're saying sounds good but your specification seems to be too low-level to be true specs, but too high-level to really show how to implement it. so true specs don't show how to implement them? if they were true specs, then you would not be talking about these unique IDs, because as you have said yourself, if they exist, _they are totally hidden_ (and hence have no place in a spec). okay, now we're arguing over the meaning of a word... :-) 06:40pm uhh by spec (as i use the word), I exclude implementation details. the spec said it didn't care how the unique ids are implemented, just that they have the given behavior. that seems correct for a spec to me. or even implementation strategies. hmmm, but why do you need to assert that they exist at all, if they are entirely hidden? because it's an important distinction. I dont know of any other systems that hide Ids. i think what you are really saying is that there is no forced non-hidden ID system. which i agree has place in a spec. no, I said the ids MUST be hidden. :) if they are not, the system is not secure. hmmm you have to have unique IDs, how else would you implement unique objects? Still, if there's another way to implement it, it can be done, because the implementation is hidden. in my system (as i've had a few thoughts about), there would not necessarily be a need for a unique ID for every concept. Many concepts would be stored using a grammar. you _can_ represent unique objects without unique ids. for instance, i refer to "my dog named Spot" without using a unique ID. "the sun" is a unique concept, but there is no need for a unique ID in the english language (or even in a logic system to reason about it) to represent it. hmmm, does this clear things up? ok, so how do you store which functions will work on "my dog named Spot" and "the sun" and which ones won't? i'm not sure what you mean by "work on". what happens if I try to add one to "my dog named Spot"? That should be illegal, right? the expression "1+my dog named spot" would be meaningless. The system would not be able to prove anything about it, but it wouldn't be "illegal". It could cause an error on a finished system maybe, if it was designed to warn users when they used those kinds of meaningless concepts. how do you prevent the + operation from actually being INVOKED on the arguments "1" and "my dog named spot"?? if it is invoked, it might lock up. or corrupt other data. i think this illustrates a key point ... functions as i use them _are not procedures_ (they aren't invoked). + is not an operation. 06:50pm it does not really make sense to think of "1+2" as being an operation... it is an expression representing a number now, the system may go through a procedure to prove that '1+2' is the same as 3. but + and '1+2' themselves are not procedures it's the same in some contexts, but not the same in others. Some cases you want to reason about 1+2 as an expression, without fully evaluating it. At what time is the expression 1+2 represented as a tree, with the + being the root and the operands being nodes? which are you talking about ?the expression "1+2" or the number '1+2'? i see a clear distinction between expressions and their meanings. exactly how do you distinguish in the system how do i distinguish in the system... hmmm ... well anything that is written is an expression. it is up to the system to deduce its meaning. how don't think this answers your question though. After the system "deduces meaning" it has an internal representation of the meaning, right? what do you mean? yes maybe well that meaning is an abstract syntax tree its representation could just be something like 'meaningof "1+2"' where meaningof is a system function that interprets user input... it shows the relationship between the parts of the expression wait, the expression (not that meaning) is an abstract syntax tree. this might even be at a level where the arguments are not distinguished from one another, such that the fact that they can be exchanged is implicit. i don't understand what you just said. No, from what you said, everything is an expression, meaning a sequence of characters Remember, we're talking about a finished system now. I'm not limiting expressions _necessarily_ to sequences of characters... i have no idea why i underlined "necessarily". i'm confusing myself :-) yes, you are confused :) nevertheless, sequences of characters does seem like a pretty good place to start for expressions. postfix, infix, or prefix notation? well, in a finished system, the user could pick his favorite syntax dynamic scoping or static? i'm not sure what you mean by scoping. 8-bit clean or unicode ummm... users won't be required to treat characters as bytes or words. they'll be "abstract" :-) 07:00pm what do you think of the arrow paper? it's confusing :-) but i've gotten a little from it. there are a few things i don't understand though let me help if arrows can only point to other arrows, and arrows always represent facts ("atoms of information"), how can relationships between concepts other than facts be stated? like what an arrow as i understand always represents a fact of relationship between its head and tail how could you say '2 > 0' ? you need to express a relationship between 2 and 0 (which are facts, but numbers), but the system seems only to be able of expressing relationships between arrows (relationships themselves). an arrow between 2 and 0 no, an arrow can't point to 2, as i understand. because 2 is not an arrow 2 and 0 are arrows if they are, then they are statements of relationship that is bogus maybe i've misunderstood his definition of the meaning of an arrow maybe they can represent things other than facts... don't ask me what the head and tail of 2 and 0 are, though.. heh heh :-) that is exactly my question.... maybe they're graphs i'm scared to ask him though. he'll probably bite my head off like last time. :-) and tell me to READ THE DRAFT again 0 can be the emtpy graph, 2 can be a graph with 2 arrows on it graphs are N-arrows, I think. that would be arbitrary though (but arbitrary is not necessarily bad)... so the 2 > 0 would be an arrow between two N-arrows representing graphs of 2 and 0 i'm guessing. hmmmm if it is, then i'd be really confused. the meaning of the expression 2 > 0 depends on what graphs reference its arrow. i really need to find information on combinatory logic reduction so i can start working on my bootstrapping system... heard of a library? :) heh heh. we don't have a good library down here i live in the south, in a little city where? greenville, mississippi well well ? there should be lots of that stuff online i hope... yeah maybe i'll start searching... didn't you try Coq? not really i haven't i tried it a little... couldn't really figure it out too well. i might be able to now though... i've learned a little more about logic... i got some books. so Tril, where do you live? 07:10pm Bellingham, Washington oh brb. brb ? what does brb mean? be right back okay i am back there's a university in town, and it has a very large library. oh that'd be nice... i'm looking for stuff using altavista now... i don't think conbinatory logic is too useful, it's hard to understand a statement by looking at it. it surely is it is terrible way to communicate for people even for computers. but... it may be useful for my bootstrapping. as it is an extremely simple (and quite well-studied i think) model of computation model of computation being the key not a good model of ideas in general which is hwat i am interested in very true i am also interested in that... but i need a nice model of computation to compute a TUNES system okay, iepos. ummm abi, iepos? iepos is having a problem or interested in that... but i need a nice model of computation to compute a TUNES system abi, iepos? i guess iepos is having a problem or interested in that... but i need a nice model of computation to compute a TUNES system heh heh tunes is generally uncomputable. it's also generally infinite, and can only be approximated on a finite computer. well maybe i will compute a near-TUNES system... actually by TUNES i mean a quite useful system, not necessarily a perfect system... so hopefully my bootstrapping system can find a real TUNES a perfect TUNES system would compute everything instantly and remember everything you told it 07:20pm i don't think my system is going to do that :-) -:- AlonzoTG [Alonzo@client-151-200-126-12.bellatlantic.net] has joined #tunes greetings alonzo y0 I saw that you are still holding by that logic system proposal... yeah i guess I officially have no comment on it. If it works great heh heh have you read my lambda-calculus introduction? But I see no reason why it should work... I skimmed it. oh, did you understand it? A little oh... hmm...... I am reading several books that directly or indirectly look at it... whatever ... i am hoping it will work. I will return to your paper if I get stuck... Logic is an analytical tool. but right now i need some info on how to efficiently reduce combinatory logic expressions... I don't see how it could *synthesize* anything... synthesize? well, logic could help computers gather information it could then act on the information absolutly gathering is what logic is for I only know boolean algebra right now... a good TUNES system is going to need to be able to do logic on statements and act on the results just learned it 2 weeks ago... what generates the statements? people, probably... that will work! :) yeah, now we just need to find a TUNES system that does that... But looking at a blinking cursor in the upper left corner, how do I know what statements will create the system I want? tril, I found a bunch of abstracts on weird papers i can't get :-) I hate those heh heh :((((( :~( iepos where? well, iepos is having a problem or interested in that... but i need a nice model of computation to compute a TUNES system oh... what papers i did an altavista search for +"combinatory logic" +reduction oh i can't even remember i skipped past them now oh, like papers that aren't online, but just abstracts of them? abi, i am looking for an efficient way to reduce combinatory logic expressions ...but iepos is having a problem or interested in that... but i need a nice model of computation to compute a TUNES system... I really don't understand that symbology, I just enter things like "Big" and "red" when I do a search... abi, iepos? you are probably having a problem or interested in that... but i need a nice model of computation to compute a TUNES system bot? abi, no!!! yes abi, iepos? it has been said that iepos is having a problem or interested in that... but i need a nice model of computation to compute a TUNES system abi, bot? alonzotg: bugger all, i dunno abi, no, iepos is confused okay, Tril. no, i am looking for an efficient way to reduce combinatory logic expressions. :) i mean "abi, no" :-) nice bot! abi, iepos? rumour has it iepos is confused heh heh that's good enough no not really abi, iepos? well, iepos is confused use /msg to abi, you're cluttering the channel that is a smart bot! 07:30pm abi, iepos? somebody said iepos was looking for an efficient way to reduce combinatory logic expressions. heh heh abi, AlonzoTG thinks you are a nice bot! abi, AlonzoTG is thinking that you area a nice bot. ...but alonzotg is their agent... lol no, abi, alonzoTG is not their agent. okay, iepos. hehe abi, alonzoTG? i think alonzoTG is not their agent. 07:40pm well i found the Journal of Automated Reasoning but i can't get any of the journals if it's an academic journal that's beacuse they charge $100+ for subscriptions. 07:50pm yes i noticed. this one was $174 per year well, do you have any recommendations as to where i can find this info? maybe there's some stuff on the tunes review page. use www.google.com, the best search engine. just type in what you want. it's smart yeah hopefully it will exclude these annoying academic journals hmm this is interesting... ANL's ATP software... automatic reasoning software.. hmm, Otter automated deduction system... 08:00pm looks interesting (free source code)... i think it might be just a theorum prover though. what i need to find TUNES is a prover that searches not for just one specific conclusion but for any conclusion that has a certain property (is contained in a certain set)... huh? prolog searches for multiple conclusions..you can accept one, or keep going to find more.. 08:10pm hmm ... i've never really used prolog it's quite limited from what i understand well, try it. maybe it can do what you need. maybe ... i actually tried it once ... but never really caught onto it. i'm going to try this otter thing it looks quite interesting 08:20pm -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) -:- SignOff iepos: #TUNES (Leaving) -:- tcn [tcn@cci-209150250126.clarityconnect.net] has joined #tunes hey hoy, tcn -:- SignOff tcn: #TUNES (tcn has no reason) 09:40pm * Tril/#TUNES is away: (afk) [BX-MsgLog Off] -:- cezar [czapien25@tntmor1-1-72.telmex.net.mx] has joined #Tunes -:- cezar [czapien25@tntmor1-1-72.telmex.net.mx] has left #Tunes [] -:- teka [jorge@195.77.175.168] has joined #Tunes holaa adios -:- teka [jorge@195.77.175.168] has left #Tunes [] [msg(TUNES)] newlog 1999.0502 IRC log ended Sun May 2 00:00:01 1999