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