01:06:29 Outlander joined #tunes
01:06:54 Outlander left #tunes
01:15:43 KingNato joined #tunes
03:25:24 smoke joined #tunes
03:32:31 [QUIT] gREMLiNs quit: SHU
03:41:54 Kyle_L joined #tunes
03:54:08 [QUIT] air quit: http://www.qzx.com/ :: 
05:35:27 [QUIT] smoke quit: Ping timeout for smoke[4dyn242.delft.casema.net]
05:38:48 smoke joined #tunes
06:11:13 eihrul joined #tunes
06:38:59 thomas joined #tunes
06:39:43 <thomas> is it nerd? is it a lamer? nooo - it's super T!
06:43:18 <thomas> hello you guys! It's me, super Thomas!
06:43:22 <thomas> hello?
06:43:41 thomas sees nothing amusing about this
06:59:24 <eihrul> problem?
08:46:37 smklsmkl joined #tunes
08:54:33 ult joined #tunes
08:59:26 [QUIT] I440r quit: Ping timeout for I440r[purplecoder.com]
09:29:11 Alex[] joined #tunes
10:51:05 [QUIT] Alex[] quit: Mangez un castor, sauvez un arbre.
10:58:49 junt joined #tunes
13:00:09 [NICK] rares changed nick to: dirtyNaziinfo
13:37:32 I440r joined #tunes
13:40:01 [NICK] rares changed nick to: runswithtreadmillunplugged
17:05:15 water joined #tunes
17:05:38 <water> re all
17:07:31 lmaxson joined #tunes
17:09:59 [QUIT] rares quit: Ping timeout for rares[wtrb-sh8-port169.snet.net]
17:10:36 lmaxson left #tunes
17:10:50 <water> )
17:13:56 eihrul joined #tunes
17:14:07 <water> re eih
18:04:50 <Kyle_L> hi water
18:05:15 <water> hey
18:06:10 <Kyle_L> workin on slate?
18:06:22 <water> yeah
18:08:23 <water> got thoughts?
18:11:18 <Kyle_L> I was wondering about "reflective logic" and what it means.   
18:11:29 <water> blah
18:11:51 <water> it doesn't mean much unless you mean it in a specific sense
18:12:05 <water> there are many interpretations of that kind of term
18:12:09 <water> which do you mean?
18:12:31 <Kyle_L> Representing a predicate logic in a machine, and what how existential qulification is represented.
18:12:55 <water> that's not reflection unless you're doing it in the same logic!
18:13:16 <Kyle_L> Yes, then reflecting on those structures.
18:13:28 <water> existential quantification is something i am currently looking at
18:13:38 <water> ok... let me address that
18:13:59 <water> "reflecting on those structures." does not mean you're using reflective logic at all....
18:14:19 <water> it means you are working at the meta-level of that logic
18:14:45 <water> which could be human language, completely informal and utterly useless to a computing language
18:15:29 <water> now...
18:15:47 <water> there ARE ways to do this that are computationally-friendly (in theory)
18:16:22 <water> for example, maude is a logic of equational rewrite systems, and is reflective in the way that lisp and other languages are
18:16:37 <water> and it's not comparable to prolog, either :P
18:17:15 <water> but existential quantification, for instance....
18:17:37 <water> is similar to what Fare has called a choice or epsilon function
18:17:47 <water> for choice function see the HLL specs
18:18:06 <water> for the epsilon construct, grep for "epsilon" in the tunes mlist archives
18:18:38 <Kyle_L> familiar with chioce functions.
18:18:39 <water> anyway
18:18:53 <water> this is not the same thing
18:19:16 <water> this is optimistically generating a new blank binding that has a given type
18:20:45 <water> and incrementally specifying that type with expressions entered afterwords
18:20:50 <water> er...
18:20:55 <water> s/type/object/
18:21:59 <water> since this thing is optimistic, it's solution set is the maximal one specified by constraints on it
18:22:12 <water> which is sort of co-inductive
18:23:01 <water> and is definitely in line with the idea of partial-evaluation
18:23:06 <Kyle_L> I fail to see how this relates to existential qualification.
18:23:12 <water> what?
18:23:15 <water> ok, example
18:23:19 <Kyle_L> Thanks.
18:23:52 <water> Ex is a choice function in a context that produces a new environment with 'x' "unbound"
18:24:08 <water> the syntax is poor, but historical
18:24:40 <water> anyways, if you consider it a complete statement (or program) all by itself
18:25:06 <water> ... then you see that 'x' could be anything that the current environment allows
18:25:37 <water> but if we subsequently add to this program...
18:26:10 <water> Ex ; (= 0 (- x 4))
18:26:24 <water> yes, i just ripped off lisp syntax ;)
18:26:55 <water> then you see that we've added a constraint to x
18:27:04 <water> this is very rough, keep in mind
18:27:28 <Kyle_L> MMmmm...
18:27:32 <water> there are many other ways to do this that have already been tried, but i'm trying to distill the Tunes concepts out of them
18:28:22 <water> hm
18:29:24 <Kyle_L> Functional languages are not intuitive to me.  The choice function seems odd.    
18:29:43 <water> it just means "give me a symbol"
18:29:44 [QUIT] ink quit: *erk* *choke* *splat* :)
18:30:04 <Kyle_L> I guess the choice function's existence is what says 'x' exists?
18:30:27 <water> the existence notion here is flimsy, though
18:30:47 <water> it doesn't ask that you make the spec consistent or anything
18:30:56 <Kyle_L> )
18:31:15 <water> you could make an x and then say that it has to equal two disjoint values simultaneously
18:31:51 <Kyle_L> I was hoping to tie existence with mebership of some super 'It Exists' set.
18:32:13 <water> oh that would be bad
18:32:39 <water> trying to make a set of all sets is just asking for trouble :)
18:33:06 <Kyle_L> I have one of those!
18:33:18 <water> oh great
18:33:29 <water> have you ever read anything on set theory and formal logic?
18:33:34 <Kyle_L> yes.
18:34:14 <water> uh so why'd you try to go for a broken concept like that?
18:34:42 <water> oh wait i haven't gotten to the best part about quantifiers
18:35:08 <water> suppose you have AyEx ...
18:35:31 <water> this has some interesting problems
18:35:47 <water> in terms of what "it's supposed to mean"
18:35:51 <water> hm brb
18:36:35 <water> basically you have two distinct meanings
18:37:02 <water> (1) is where the choice of Y is supposed to determine what X has to be
18:39:11 _water joined #tunes
18:39:27 <_water> but because of the historical syntax of it, you can't express the choice of X and Y *in parallel*
18:39:48 [QUIT] water quit: Killed (NickServ (GHOST command used by _water))
18:39:57 [NICK] _water changed nick to: water
18:41:01 <water> there's a book that i'm reading that's solely based on this idea
18:41:28 <Kyle_L> I would imagine that you can only choose then in parallel when the choice of x does not depend on y.
18:41:45 <Kyle_L> But then you could rephrase to capture the parrelelness.
18:41:56 <water> it turns out that you can't
18:42:12 <water> not with ordinary first-order logic
18:42:52 <water> you either modify the syntax or rely on specifying X as the result of a chosen function that depends on certain other quantified variables
18:43:33 <Kyle_L> yes, the latter is what I mean.
18:43:45 <water> oh well that's 2nd-order :)
18:44:03 <water> because you have to suppose that a function exists
18:44:35 [QUIT] eihrul quit: [x]chat
18:45:32 <Kyle_L> I see what you are saying now.  What I was doing naturally, was never in the realm of first-order logic to begin.
18:47:18 <water> well anyway, the book is interesting because it goes a lot into choice functions and game theory
18:48:21 <Kyle_L> May you point out why a set of all sets is a broken concept? 
18:48:30 <water> of course :)
18:48:51 <water> if you'll notice, then set of all sets is (rather obviously) also a set :)
18:48:56 <water> s/then/the/
18:49:04 <Kyle_L> yes, and a member of itself.
18:50:09 <water> which violates an important axiom
18:50:16 <water> well-foundedness
18:50:25 <Kyle_L> Yes, you are right.
18:50:31 <water> you can't recursively specify meaning in such a system
18:51:23 <Kyle_L> But do the axoims of set theory encompass all valid logical constructs? 
18:51:42 <water> huh?
18:51:48 <Kyle_L> I will admit I am outside formal set theory, but I am still inside consistency.
18:52:09 <water> go read the book "vicious circles"
18:52:36 <Kyle_L> But do the axoims of set theory encompass all valid consistent defintions?  (I am at a loss to describe this). 
18:52:44 <water> yes you are
18:53:01 <water> that's not a very meaningful question
18:53:18 <water> but to be short: NO
18:53:42 <water> to be long, No, but you don't want to drop axioms willy-nilly just because it seems cool
18:54:15 <Kyle_L> I beleive formal set theory could benefit from many new axioms.   
18:54:28 <water> that's a nice belief
18:54:30 <Kyle_L> But I do agree that they should not be added because they are cool.
18:54:44 <water> now go read "vicious circles" if you really mean that :)
18:55:10 <water> yes the book is cheap
18:55:27 <Kyle_L> Maybe we should just make these sets of sets, see what can be done, and in a hundred years the pattern will be apparent enough to add a new axiom or two. :) 
18:55:36 <Kyle_L> </sillyness>
18:55:52 <water> just read the damned book
18:55:59 <Kyle_L> ok.
18:56:09 <Kyle_L> thanks.
18:56:17 <water> because it covers that in ridiculous detail by a couple of authors who really know the subject
18:56:27 <water> np
18:57:31 <Kyle_L> who is the author (be sure I got the right book)
18:57:41 <water> barwise and moss
18:57:45 <water> '95
18:57:51 <Kyle_L> thanks
18:57:59 <Kyle_L> nice chattin.  bye
18:58:01 [QUIT] Kyle_L quit: Leaving
18:58:02 <water> ok
18:58:07 ult joined #tunes
18:58:11 <water> hey ult
18:58:16 <ult> 'lo
19:18:54 eihrul joined #tunes
19:34:42 [QUIT] ult quit: Read error to ult[user-38lcdsk.dialup.mindspring.com]: EOF from client
19:36:37 ult joined #tunes
19:52:27 [QUIT] water quit: The Tao went that-a-way!
19:56:25 water joined #tunes
20:13:56 [QUIT] water quit: Read error to water[tnt-10-24.tscnet.net]: Connection reset by peer
20:15:13 water joined #tunes
21:24:31 eihrul joined #tunes
22:25:21 XeF4 joined #tunes
22:32:31 ftt joined #tunes
22:34:35 <ftt> how goes
22:59:57 [QUIT] rares quit: [x]chat
23:27:35 I440r joined #tunes
23:38:21 billh joined #tunes
23:40:18 [QUIT] lar1 quit: [x]chat
23:51:27 [QUIT] KingNato quit: Ping timeout for KingNato[212.28.215.84]
23:52:29 KingNato joined #tunes
23:59:02 [QUIT] KingNato quit: Ping timeout for KingNato[212.28.215.84]
23:59:47 water joined #tunes
00:07:43 KingNato joined #tunes