IRC log started Tue Apr 13 00:00:00 1999
[msg(TUNES)] permlog 1999.0413
-:- ChanServ has changed the topic on channel #tunes to: Millenia Year Application Software System -- www.qzx.com/myass.txt
-lilo(lilo@varley.openprojects.net)- [GlobalNotice] Sorry all.  Had to reup services in order to resolve a timestamp problem.  Thanks for your patience.
!lilo:*! looks like the problem is resolved....I'll have to recompile to get rid of the test info but I think I'll wait till tomorrow my time 8)
-:- tantan [mismo@infb2.pntic.mec.es] has joined #Tunes
<tantan> que hable alguien por favor
-:- tantan [mismo@infb2.pntic.mec.es] has left #Tunes []
02:50am
-:- Downix [down@d-nh-concord-12.ici.net] has joined #Tunes
-:- SignOff Downix: #TUNES (Leaving)
-:- NuFAN [nufan@pppm24.rendsburg.netsurf.de] has joined #Tunes
-:- SignOff NuFAN: #TUNES (Leaving)
-:- Fare has changed the topic on channel #tunes to: Reflective Computing System <http://www.tunes.org/> QZ: Millenia Year Application Software System -- www.qzx.com/myass.txt
<Fare> (godwin strikes again)
07:10am
-:- AlonzoTG [Alonzo@client-151-200-120-65.bellatlantic.net] has joined #tunes
-:- hcf [nef@me-portland-us644.javanet.com] has joined #tunes
-:- ChanServ has changed the topic on channel #tunes to: Millenia Year Application Software System -- www.qzx.com/myass.txt
-lilo(lilo@varley.openprojects.net)- [GlobalNotice] Hi all.  That was, I hope, one last change to services.  Thanks for your patience!
-:- Downix [down@24.128.89.92] has joined #Tunes
<Downix> hey
09:10am
<Fare> loy
<Downix> what's up?
<Fare> hum. My stupidity is up
<Downix> ok
09:40am
<AlonzoTG> yer a genius!
<AlonzoTG> u understand lambda calc!
<AlonzoTG> :P
<hcf> AlonzoTG: everyone is a genius compared to u
* AlonzoTG/#tunes ignites a flamethrower and eyes hcf
09:50am
-:- Chikano [Tiqui@195.235.112.167] has joined #Tunes
<Chikano> Hijos dwe puta
-:- Chikano [Tiqui@195.235.112.167] has left #Tunes []
10:00am
-:- SignOff hcf: #TUNES (Leaving)
-:- SignOff Downix: #TUNES (Ping timeout for Downix[24.128.89.92])
!saberhagen.openprojects.net!! Remote CONNECT becquer.openprojects.net 8005 from lilo
!wang.openprojects.net!! Remote CONNECT becquer.openprojects.net 8005 from lilo
!koontz.openprojects.net!! Remote CONNECT becquer.openprojects.net 8005 from lilo
!koontz.openprojects.net!! Remote CONNECT becquer.openprojects.net 8005 from lilo
!sterling.openprojects.net!! Remote CONNECT becquer.openprojects.net 8005 from lilo
!hogan.openprojects.net!! Remote CONNECT becquer.openprojects.net 8005 from lilo
!netgod:*! anyone else starting to think becquer is unreachable?
!Is:*! traceroute stops at 194.179.28.21
!Is:*! (from saberhagen)
!lilo:*! netgod, why does a gline tell you you are 'terminated with extreme prejudice'?  that's not horribly friendly ;)
!lilo:*! another message that needs fixing 8)
-:- SignOff Fare: #TUNES (Read error to Fare[quatramaran.ens.fr]: Connection reset by peer)
-:- _QZ [brand@p0wer.qzx.com] has joined #tunes
<AlonzoTG> om
03:00pm
<_QZ> hello mo
<AlonzoTG> om!
03:10pm
-:- Fare [rideau@quatramaran.ens.fr] has joined #Tunes
<Fare> Gakuk!
<_QZ> gakuk
<Fare> QZ: why do you clobber my topic, instead of appending to it?
<Fare> will you show myass to me?
<Fare> have you screenshots of myass?
<Fare> is myass open, or is it proprietary?
<_QZ> i didnt clobber yer topic, chanserv did
<Fare> but you told it to, didn't you?
<_QZ> they added enhancements to chanserv yesterday and its screwed up
<_QZ> that is why tril is op'd
<Fare> I think that myass is fake, and that you're full of crap!
<_QZ> whatever
04:00pm
<Fare> shyte. I dunno the passwd
04:10pm
-:- Iepos [root@d11.t1-3.tecinfo.com] has joined #TUNES
<Iepos> anyone here?
<Fare> nope
<Iepos> oh
<Fare> I bet myass
<Iepos> i read the first part of your master's thesis ...
<Fare> oh. I reread it once, an was not proud of it.
<Iepos> i've never done any real study on type systems ...
<Fare> although not everything is to be thrown away
<Iepos> what makes them so interesting?
<Fare> there are *excellent* tutorials by B. Werner on the topic.
<Fare> type systems are more than interesting. They are a key concept.
<Iepos> yeah...
<Iepos> i wasn't planning on treating types specially in my system ...
<Iepos> but maybe it would be simpler if i did.
<Fare> For instance, people from category theory reconstructed type lambda calculus in an amazingly isomorphic way to what was known, from a completely different initial point of view!
<Fare> s/type/typed/
<Fare> well, my masters thesis doesn't treat types that specially.
<Iepos> hmm ... i tried to figure out category theory a while back ...
<Iepos> by the way, where does that "s/from/to" thing come from?
<Fare> in retrospect, it can be said to be lambda-calculus with a very bizarre syntax, but lots of interesting higher-order theorems, and an interesting way to draw diagrams.
<Fare> Iepos: it comes from ed.
<Iepos> yeah i'll agree with "bizarre syntax" and interesting diagrams
<Iepos> i couldn't understand anything i saw about it
04:20pm
<Iepos> it looked really funny... weird symbols everywhere
<Fare> but vi, sed, and perl have inherited s/// from ed
<Iepos> something about "morphisms" and objects but not sure what
<Iepos> oh ... vi ...
<Iepos> i usually use emacs
<Fare> so do I
<Iepos> is there someway around having to press ESC all the time in vi?
<Iepos> if there was, then i might use it
<Iepos> 'cause i hate waiting forever for emacs to load :-)
<Fare> but s/type/typed/ is easier to write than M-x replace-string t y p e RET t y p e d RET
<Iepos> haha...
<Fare> Iepos: why wait for emacs to load?
<Iepos> good question.
<Iepos> it is sometimes slow, sometimes fast, on my system.
<Fare> I launch xemacs once a week, and just spawn gnuclient's out of it.
<Iepos> kinda weird.
<Iepos> oh, i don't usually use X.
<Fare> a gnuclient window pops out instantly!
<Fare> even w/o X-window, you can keep an xemacs in a VC or in a screen(1)
<Iepos> oh
<Fare> and have gnuclient seize control of your terminal
<Iepos> a few minutes ago, i was trying to understand Curry's "U" ...
<Iepos> from his combinatory logic
<Fare> U ? Which combinator was it?
<Fare> a Universal combinator?
<Fare> or was it disjunction?
<Iepos> just a sec
<Fare> (like the Union symbol)
<Iepos> something like "\x.\y.forall z.!((x z) & (y z))"
<Iepos> all kinds of logic packed into one
<Iepos> strange...
<Iepos> i don't know why he chose it
<Fare> ! is not?
<Iepos> yes
<Fare> isn't it rather !(!(x z) & !(y z)) ???
<Iepos> i guess you can generate other fun combinators using it
<Iepos> like !, &, |, forall, etc.
<Iepos> well that would just be the same as (x z) | (y z)
<Fare> then it's type disjunction, indeed (well, assuming classical logic)
<Iepos> i think it's a nand... not both
<Fare> he's precisely defining disjunctino frmo conjunction and not
<Fare> only that's a bad move, for it presumes classical logic
<Iepos> what's the deal with "classical logic"?
<Iepos> is something wrong with it?
<Fare> and that leads him in big trouble (see my lambdaND paper about it)
<Fare> classical logic means you have !!A -> A
<Iepos> is something wrong with DeMorgan's theorum... is that it?
<Iepos> oh
<Fare> wrong: yes and no
<Iepos> ummm....
<Iepos> what is wrong with !!A -> A   ???
<Fare> classical logic is powerful, but it implies that it be possible to always decide that something be either true or false.
<Iepos> oh
<Iepos> so the liar's paradox gives trouble maybe?
<Fare> Which is clearly only possible to god, and leads to many paradoxes.
<Iepos> "this statement is false"
<Fare> yeah, it gives lots of gratuitous paradoxes, and forces to use a typesystem.
<Iepos> weird.
<Iepos> so what is the solution
<Iepos> how can you reason without !!A -> A ??
<Fare> and then, you cannot have a fully reflective logic, either.
<Iepos> haha
<Fare> Iepos: that's called intuitionnistic logic
<Fare> it's been fought for by Brouwer and others.
<Fare> it gave us things like Coq.
<Iepos> hmmm ... do you have any links to where i can learn about this?
<Fare> constructive logics.
<Fare> maybe Coq tutorials?
<Iepos> phew....... no not them !!
<Iepos> really confusing..
04:30pm
<Iepos> :-)
<Fare> if you're really in math theory, get the MacLane & Mordijk
<Iepos> seems to assume i already understand it.
<Iepos> so what are some basic axioms of intuitionist logic?
<Iepos> intuitionnistic
<Fare> if not, well, 
<Fare> s/.*//
<Iepos> ???
<Fare> same axioms, except for excluded middle
<Iepos> oh what is excluded middle?
<Fare> in simple propositional logic, you have axioms S, K, I, that correspond to well-known combinators.
<Fare> propositional logic == simply typed lambda-calculus
<Iepos> oh
<Fare> axiom I = \x->x : P->P
<Fare> axiom K = \x y.x : P->Q->P
<Iepos> it doesn't seem like you could do much reasoning with just SKI
<Fare> axiom S = \x y z.x z (y z) : (P->Q->R)->(P->Q)->P->R
<Iepos> how could you even say the proposition "A=B"?
<Iepos> no equality?
<Fare> and modus ponens: from f:P->Q and x:P deduce (f x):Q
<Fare> Iepos: propositional logic has grammar P ::= A | P->P
<Iepos> ???
<Iepos> what is "::=" ?
<Fare> you can add arbitrary atomic equality propositions.
<Fare> Iepos: BNF syntax
<Iepos> but then you'd have to add axioms as well, wouldn't you?
<Fare> it reads "a proposition is either an atom, or an implication of a proposition by another proposition"
<Fare> much shorter, everyone understands, and scales to much more complicated grammars.
<Iepos> oh ... i get it... P is for Proposition
<Fare> Iepos: oh, then you add axioms for your particular target domain
<Iepos> A is for atom
<Iepos> then you have to extend the system to make it work
<Fare> those three axioms only give you tautologies
<Iepos> so the original SKI system wasn't very useful after all?
<Fare> (definition of tautologies: things "always" valid, independently from particulars of the problem at hand)
<Fare> of course it is.
<Fare> Also note that this is only simply typed logic, and that there is more to lambda-calculus than this simple type system.
<Iepos> this is strange... 
<Fare> without atoms, you can still have your tautologies, and the calculus is sufficient to express quite a few things.
<Iepos> i don't even see how you could express "P -> Q" with just SKI...
<Fare> Actually, even with the simply typed calculus, it suffices to accept a one recursive type to be Turing-equivalent
<Fare> I: P->P
04:40pm
<Fare> K: P->Q->P
<Fare> S: (P->Q->R)->(Q->R)->P->R
<Iepos> sooo ... S, K, and I are propositions ?
<Fare> and if you want classical logic, add ((P->A)->A)->P
<Fare> S, K, I are *proof terms*
<Iepos> they are statements, aren't they?
<Fare> they are proof terms for basic axioms.
<Fare> the statement proved by I is P->P
<Iepos> rather than functions, i mean.
<Fare> the statement proved by K is P->Q->P
<Fare> etc.
<Iepos> i was thinking you were talking about combinatory logic, with functions.
<Fare> that's the curry-howard isomorphism.
<Iepos> i guess there is implicit universal quantification
<Iepos> I proves that, for all P, P->P
<Iepos> K proves for all P and Q, that P->Q->P
<Fare> btw, X:((P->A)->A)->P is kind of a call/cc, iirc
<Fare> oh, yeah, but this quantification is outside to the calculus
<Iepos> yeah, the definitions of S, K, and I are outside ...
<Iepos> that makes sense...
<Iepos> this is starting to make more sense
<Fare> there's a quantification over propositions at the meta-level, but not inside the calculus (which is why this is propositional logic and/or simply typed lambda-calculus)
<Fare> you *can* get quantification *inside* the calculus, and then things are more complicated,
<Fare> and you need more combinators, etc.
<Iepos> then it is the "predicate" calculus, right?
<Fare> there are *many* ways to look at things.
<Fare> yeah, when there are quantifications, you have predicates rather than mere propositions.
<Fare> although there is a distinction I don't understand between "predicative" and "impredicative" logics.
-:- Fare has changed the topic on channel #tunes to: lambda-calculus 101
<Iepos> hmmm...
<Iepos> these S, K, and I axioms are very similar to the S, K, and I functions i've seen before
<Fare> they are isomorphic!
<Fare> hence, the name!
<Iepos> I remember that I was unneccessary ...
<Fare> that's the Curry-DeBruijn-Howard isomorphism!
<Iepos> it could be expressed as (S K K)
<Iepos> is it the same here then?
<Fare> yeah
<Fare> except that 1) I is more elegant,
<Fare> and 2) you do need a P->P, not just (P->R)->(P->R)
<Fare> as you'd get with plain (S K K) under this system.
<Iepos> well you don't have functions in this system, do you?
<Iepos> so there is no (S K K) ... because no function application
<Iepos> or do you just use imp instead?
<Fare> functions do not appear among propositions, only as proof terms.
<Iepos> (S->K)->K ??
<Fare> again, that's the simplest type system possible
<Iepos> :-)
<Iepos> wait
<Iepos> though
04:50pm
<Iepos> S is not a term
<Iepos> only an axiom
<Fare> (well, simplest non-trivial type system)
<Fare> it's the *proof* of an axiom.
<Iepos> i don't see any types at all in this system.
<Iepos> where are the types?
<abi> the types are sets, you can do set union on two types
<Iepos> abi i wasn't talking to you!
<Iepos> :-)
<Fare> the axiom is (P->Q->R)->(Q->R)->P->R
<Fare> S is the proof of the axiom, the axiom is the (simple) type of S.
<Fare> C-dB-H isomorphism!
<Iepos> heh heh ... i've never heard of Curry-DeBruijn-Howard isomorphism.
<Iepos> you can tell i haven't gone to school for this
<Fare> well, read tutorial papers by B. Werner (around same ftp directory as Coq)
<Fare> these are things you mostly don't learn in school.
<Iepos> what ftp dir?
<Fare> see the ftp address for Coq
<Iepos> oh .... i don't remember
<Fare> something like ftp.inria.fr:/Projects/coq/
<Iepos> i just remember going to coq.inria.fr and following links...
<Iepos> oh
<Fare> or /local/Projects/coq
<Iepos> i'll have to read um on this
<Iepos> s/um/up
<Iepos> because i still don't have a clear idea of what this system is ...
<Iepos> ... and what it is for .
<Fare> well, experiment with Coq.
<Fare> It uses the C-dB-H isomorphism, but with a much richer type system than Church's simple type system.
<Fare> (should be Simple, as a personal name)
<Iepos> let's see... and this is "propositional logic"?
<Iepos> or is there a more specific name ?
<Iepos> for this some with the "->" trees and SKI.
<Fare> well, intuitionistic propositional logic with only the -> connector.
<Iepos> s/some/stuff
<Iepos> okay i got one of the files
<Fare> you can add more connectors if you wish, and possibly a classical axiom.
<Iepos> in the Benjamin.Warner dir
05:00pm
<Fare> dunno which are the best.
<Fare> Maybe you should publish a bibliography of good stuff for Review/ ?
<Iepos> maybe ...
<Iepos> i probably don't know enough about it now ...
<Iepos> ... to tell what is good.
<Fare> that's fine: publish things that pleased you
<Fare> things that made you understand.
* Fare/#Tunes wishes Tril was here.
<Iepos> okay
<Fare> Hum. This kind of summoning doesn't look like it works.
<Fare> gotta go, now.
<Iepos> okay
<Iepos> bye
<Fare> Bye!
-:- SignOff Iepos: #TUNES (Iepos)
* Fare/#Tunes is away (sleep)
05:10pm
-:- XeF4 [xef4@wbrady.wasilla.ptialaska.net] has joined #tunes
* XeF4/#tunes is away: (taxes) [BX-MsgLog On]
-:- NetSplit: carter.openprojects.net split from koontz.openprojects.net [07:08pm]
-:- BitchX+Deb1an: Press Ctrl-F to see who left Ctrl-E to change to [carter.openprojects.net]
* XeF4/#tunes is back from the dead. Gone 0 hrs 53 min 11 secs
-:- SignOff XeF4: #TUNES (Leaving)
-:- Netjoined: carter.openprojects.net koontz.openprojects.net
-:- _QZ [brand@p0wer.qzx.com] has joined #tunes
-:- hcf [nef@me-portland-us328.javanet.com] has joined #tunes
<AlonzoTG> om
07:40pm
-:- SignOff hcf: #TUNES (Leaving)
-:- hotrod231 [MyComputer@gnzl-as1-52.eatel.net] has joined #tunes
-:- hotrod231 [MyComputer@gnzl-as1-52.eatel.net] has left #tunes []
-:- SignOff Tril: #TUNES (Ping timeout for Tril[sloth.wcug.wwu.edu])
-:- SignOff Fare: #TUNES (Ping timeout for Fare[quatramaran.ens.fr])
-:- Tril [dem@sloth.wcug.wwu.edu] has joined #TUNES
-:- mode/#tunes [+o Tril] by ChanServ
<_QZ> Tril: u here?
09:40pm
<AlonzoTG> om
09:50pm
-:- SignOff _QZ: #TUNES (Ping timeout for _QZ[p0wer.qzx.com])
-:- _QZ [brand@p0wer.qzx.com] has joined #tunes
* AlonzoTG/#tunes slaps _QZ around a bit with a large trout
<AlonzoTG> 15:42 hours of uptime...
11:00pm
<_QZ>  12:02am  up 8 days,  3:36,  1 user,  load average: 0.00, 0.00, 0.00
<_QZ> ah horseshit
<_QZ> i wouldnt have shown that if i had remembered the reboot last week
<AlonzoTG> this makes no sense, my IRC client says I've been on this server longer than my dialer say's I've been connected... :((((((((((((((((((((
<AlonzoTG> my dialer reports 14:11 hours...
<AlonzoTG> oh well...
<AlonzoTG> to bed I go...
<AlonzoTG> see you in 4 hours...
<AlonzoTG> :P
-:- SignOff AlonzoTG: #TUNES (Have Nice Day :))
-:- SignOff _QZ: #TUNES (Ping timeout for _QZ[p0wer.qzx.com])
11:10pm
-:- _QZ [brand@p0wer.qzx.com] has joined #tunes
-:- SignOff _QZ: #TUNES (BRiX [http://www.qzx.com/brix] :: sleep)
[msg(TUNES)] newlog 1999.0414
IRC log ended Wed Apr 14 00:00:00 1999