00:00:16 <oerjan> shachaf: oh so it's from tswett's network
00:00:40 <hppavilion[1]> shachaf: I did think of rho expressions, which are like lambda expressions but based on the rho calculus
00:02:35 <hppavilion[1]> `le/rn last-class function/A last-class function is a function that cannot be passed as an argument, accept a function as an argument, be returned by a function, return a function, set to a variable other than its initial name, or be called
00:02:38 <HackEgo> Learned «last-class function»
00:02:44 <HackEgo> A last-class function is a function that cannot be passed as an argument, accept a function as an argument, be returned by a function, return a function, set to a variable other than its initial name, or be called
00:03:05 <tswett> 08:07:49 <b_jonas> `learn integer/An integer is a number that does not contain a wildcard that matches any character other than a line feed.
00:03:05 <tswett> 08:07:50 <HackEgo> /hackenv/bin/learn: line 3: wisdom/integer/an: No such file or directory \ Learned 'integer/an': integer/An integer is a number that does not contain a wildcard that matches any character other than a line feed.
00:03:14 <tswett> My network is getting really good at remembering long phrases.
00:04:05 <oerjan> tswett: clearly today's xkcd is relevant.
00:04:13 -!- spiette has quit (Quit: :qa!).
00:05:28 <oerjan> `` sed -i 's/$/. It can, however, be pointed at, derisively./' wisdom/'last-class function'
00:05:37 <oerjan> `? last-class function
00:05:38 <HackEgo> A last-class function is a function that cannot be passed as an argument, accept a function as an argument, be returned by a function, return a function, set to a variable other than its initial name, or be called. It can, however, be pointed at, derisively.
00:06:27 <oerjan> hppavilion[1]: you now, like the higher classes point at the lower
00:08:08 -!- lynn has quit (Ping timeout: 244 seconds).
00:28:49 -!- fungot has quit (Ping timeout: 250 seconds).
00:29:28 <HackEgo> Alas, poor fungot, I knew him well!
01:01:38 -!- tromp_ has joined.
01:04:33 -!- adu has quit (Quit: adu).
01:11:50 -!- mihow has quit (Quit: mihow).
01:41:59 -!- lambda-11235 has joined.
02:14:50 -!- oerjan has quit (Quit: Latezzz).
02:28:47 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
02:29:33 <pikhq> shachaf: I haven't.
02:37:27 -!- nisstyre has quit (Ping timeout: 244 seconds).
02:43:23 -!- andrew has joined.
02:43:47 -!- adu has joined.
02:44:17 <adu> hppavilion[1]: NOOOOOOOO
02:44:33 <adu> wait, I mean YEEEEEEEEEEES
03:05:55 -!- nisstyre has joined.
03:16:49 -!- andrew has quit (Remote host closed the connection).
03:30:59 -!- aloril has quit (Ping timeout: 240 seconds).
03:39:02 -!- aloril has joined.
03:56:26 -!- andrew has joined.
04:06:11 -!- tromp_ has quit (Remote host closed the connection).
04:07:09 -!- mad has joined.
04:08:52 -!- bb010g has joined.
04:11:30 -!- perrier_ has quit (Read error: Connection reset by peer).
04:11:33 -!- Guest37376 has quit (Read error: Connection reset by peer).
04:11:36 -!- Guest58776 has quit (Remote host closed the connection).
04:11:42 -!- Guest20424 has quit (Remote host closed the connection).
04:12:29 <HackEgo> echo "Alas, poor $@, I knew him well!"
04:12:38 <zgrep> Oh. That's boring. :(
04:15:40 <HackEgo> cat: bin/bin: No such file or directory
04:15:54 <HackEgo> cat: bin/bin/bin: No such file or directory
04:16:00 <HackEgo> cat: /secret: No such file or directory
04:16:08 <HackEgo> cat: bin/secret: No such file or directory
04:16:17 <MDude> `cat bin/supersecret
04:16:18 <HackEgo> cat: bin/supersecret: No such file or directory
04:16:22 <MDude> Well I'm ut of dieas.
04:18:34 <zgrep> `` find / -name '*secret*'
04:19:05 <HackEgo> /proc/sys/net/ipv4/ipfrag_secret_interval \ /proc/sys/net/ipv6/ip6frag_secret_interval \ find: `/proc/tty/driver': Permission denied \ find: `/proc/1/task/1/fd': Permission denied \ find: `/proc/1/task/1/fdinfo': Permission denied \ find: `/proc/1/task/1/ns': Permission denied \ find: `/proc/1/fd': Permission denied \ find: `/proc/1/fdinfo': Per
04:20:35 -!- andrew has quit (Remote host closed the connection).
04:23:01 -!- adu has quit (Quit: adu).
04:25:11 -!- adu has joined.
04:25:22 -!- adu has quit (Client Quit).
04:31:03 -!- earendel has quit (Ping timeout: 250 seconds).
04:54:32 -!- XorSwap has joined.
04:58:09 <coppro> Taneb: have you played mage knight?
04:58:12 -!- adu has joined.
04:59:22 <zgrep> `` find / -name '*secret*' > secret.txt
05:00:00 <HackEgo> find: `/proc/tty/driver': Permission denied \ find: `/proc/1/task/1/fd': Permission denied \ find: `/proc/1/task/1/fdinfo': Permission denied \ find: `/proc/1/task/1/ns': Permission denied \ find: `/proc/1/fd': Permission denied \ find: `/proc/1/fdinfo': Permission denied \ find: `/proc/1/ns': Permission denied \ find: `/proc/2/task/2/fd': Permissi
05:00:02 <HackEgo> File system. HackEgo/HackBot's is http://codu.org/projects/hackbot/fshg/index.cgi
05:01:05 <zgrep> http://codu.org/projects/hackbot/fshg/index.cgi/file/8a87b4c82f52/secret.txt
05:04:00 <HackEgo> http://codu.org/projects/hackbot/fshg/index.cgi/file/tip/secret.txt
05:04:25 <zgrep> Although there probably should be a thing for the permanent version of the latest URL...
05:06:43 -!- tromp_ has joined.
05:11:27 -!- tromp_ has quit (Ping timeout: 276 seconds).
05:19:39 -!- earendel has joined.
05:21:32 -!- earendel has quit (Client Quit).
05:22:59 -!- earendel has joined.
05:23:34 <Elronnd> ...Where does HackEgo get his wordlist?
05:23:43 <zgrep> http://codu.org/projects/hackbot/fshg/index.cgi/file/a4e2b9749d1d/bin/word
05:29:59 -!- APic has quit (Ping timeout: 240 seconds).
05:36:14 -!- APic has joined.
05:51:54 -!- Xe has quit (Ping timeout: 260 seconds).
05:53:50 -!- Xe has joined.
06:31:03 -!- lambda-11235 has quit (Quit: Bye).
06:48:12 -!- XorSwap has quit (Quit: Leaving).
06:51:37 -!- adu has quit (Quit: adu).
07:02:48 -!- tromp_ has joined.
07:07:02 -!- tromp_ has quit (Ping timeout: 250 seconds).
07:10:56 -!- earendel has left.
07:10:59 -!- earendel has joined.
07:23:11 <earendel> these numbers @word.. is this some kind of probability of occurence for that syllables?
07:25:17 <earendel> also how have is this association there "happened"?
07:37:01 <deltab> yes, they're weights; a random number is chosen from their sum
07:40:41 -!- MDude has changed nick to MDream.
07:41:19 <deltab> they're presumably generated from lots of input text, counting up how often 'th' is followed by 'w' etc.
07:55:41 <deltab> https://en.wikipedia.org/wiki/Markov_chain#Markov_text_generators
08:05:20 -!- AnotherTest has joined.
08:07:59 -!- tromp_ has joined.
08:12:29 -!- tromp_ has quit (Ping timeout: 240 seconds).
08:41:20 -!- jaboja has joined.
08:52:33 -!- hppavilion[1] has quit (Ping timeout: 244 seconds).
08:57:59 <HackEgo> Useless use of a constant (warn 4.5+6.3) in void context at -e line 1.
09:34:04 -!- impomatic_ has quit (Ping timeout: 240 seconds).
09:54:11 -!- AnotherTest has quit (Ping timeout: 248 seconds).
09:55:34 -!- J_Arcane has quit (Ping timeout: 240 seconds).
10:06:55 -!- AnotherTest has joined.
10:23:25 -!- lynn_ has joined.
10:43:59 -!- jaboja has quit (Ping timeout: 240 seconds).
10:44:38 <fizzie> They're generated from word lists, actually.
10:45:45 <fizzie> Which is probably subtly different from generating them from lots of input text, since it presumably has a higher weight for more uncommon trigrams (or 4-grams or whatever they were).
10:46:29 <fizzie> It's the same procedure fungot uses, except fungot does words, and it uses a variable-length model generated by https://github.com/vsiivola/variKN
10:46:47 <fizzie> Oh, right, the internet gave up at night.
10:47:14 -!- fungot has joined.
10:47:22 <fizzie> fungot: Feeling all right there?
10:47:23 <fungot> fizzie: they don't ever define " fnord" is invalid? the line does ( which is useful
10:47:41 <fizzie> All subsystems nominal, I guess.
10:49:00 -!- ais523 has joined.
10:49:22 <ais523> hmm, new sort of spam I've never seen before
10:49:54 <ais523> it's piggybacking on other spam in an unusual way: it suggests that if we download a particular mobile app, it'll cause one category of spam to stop arriving
10:50:41 <ais523> basically trying to position itself as an opt-out, in a way that's fairly suspicious to people who are aware of computers, but it seems likely to fool some people
11:26:33 -!- boily has joined.
11:29:01 <b_jonas> ais523: yes, many spam does that in a much more straightforward way: they include a link to "unsubscribe" from that very spam.
11:29:21 <b_jonas> but I think I've heared of spam that talks about other spam
11:30:57 <b_jonas> ais523: here's one example http://bendwavy.org/wp/?p=3416
11:31:36 <b_jonas> then there's http://www.xkcd.com/810/
11:32:19 -!- ais523 has quit (Ping timeout: 248 seconds).
11:44:33 -!- zemhill has joined.
11:47:14 -!- lynn has joined.
11:47:43 -!- benderpc_ has joined.
11:49:46 -!- lynn_ has quit (Ping timeout: 244 seconds).
11:53:46 -!- zemhill has quit (Remote host closed the connection).
11:53:58 -!- zemhill has joined.
11:56:56 -!- zemhill has quit (*.net *.split).
11:58:08 -!- zemhill has joined.
12:02:13 -!- zemhill has quit (Remote host closed the connection).
12:02:25 -!- zemhill has joined.
12:03:12 * boily should nuke that /boot partition
12:03:35 <boily> is it possible to merge partitions together?
12:09:23 -!- zemhill has quit (Remote host closed the connection).
12:09:33 <boily> I'm using ubuntu's default partition scheme, and /boot is way too small, always getting clogged by old kernels.
12:09:35 -!- zemhill has joined.
12:10:07 <boily> either there's a way to automatically remove old versions, or just take everything in /boot and put it in /.
12:10:36 <boily> (and make /boot disappear in a puff of Logic.)
12:14:36 -!- zemhill has quit (Remote host closed the connection).
12:14:48 -!- zemhill has joined.
12:18:48 -!- zemhill has quit (Remote host closed the connection).
12:19:00 -!- zemhill has joined.
12:19:05 -!- benderpc_ has changed nick to bender|.
12:19:15 -!- bender| has quit (Changing host).
12:19:16 -!- bender| has joined.
12:23:16 -!- zemhill has quit (Remote host closed the connection).
12:23:28 -!- zemhill has joined.
12:24:52 -!- boily has quit (Quit: GLASS CHICKEN).
12:28:52 -!- zemhill has quit (Remote host closed the connection).
12:29:04 -!- zemhill has joined.
12:33:04 -!- zemhill has quit (Remote host closed the connection).
12:33:16 -!- zemhill has joined.
12:37:16 -!- zemhill has quit (Remote host closed the connection).
12:37:30 -!- zemhill has joined.
12:41:30 -!- zemhill has quit (Remote host closed the connection).
12:41:42 -!- zemhill has joined.
12:43:37 -!- carado has quit (Quit: Leaving).
12:44:23 -!- carado has joined.
12:48:23 -!- zemhill has quit (Remote host closed the connection).
12:48:36 -!- zemhill has joined.
12:51:32 -!- AnotherTest has quit (Ping timeout: 250 seconds).
12:55:33 -!- zemhill has quit (Remote host closed the connection).
12:55:45 -!- zemhill has joined.
12:59:45 -!- zemhill has quit (Remote host closed the connection).
12:59:57 -!- zemhill has joined.
13:03:57 -!- zemhill has quit (Remote host closed the connection).
13:04:10 -!- zemhill has joined.
13:07:27 <HackEgo> [wiki] [[Addleq]] https://esolangs.org/w/index.php?diff=46458&oldid=20442 * 85.194.216.168 * (+18) Added OISC category
13:10:14 -!- AnotherTest has joined.
13:14:14 -!- zemhill has quit (Remote host closed the connection).
13:14:26 -!- zemhill has joined.
13:17:07 -!- lynn_ has joined.
13:19:40 -!- lynn has quit (Ping timeout: 244 seconds).
13:23:40 -!- zemhill has quit (Remote host closed the connection).
13:23:51 -!- zemhill has joined.
13:27:51 -!- zemhill has quit (Remote host closed the connection).
13:28:03 -!- zemhill has joined.
13:32:03 -!- zemhill has quit (Remote host closed the connection).
13:32:15 -!- zemhill has joined.
13:32:32 -!- tromp_ has joined.
13:33:37 -!- jaboja has joined.
13:37:37 -!- zemhill has quit (Remote host closed the connection).
13:37:49 -!- zemhill has joined.
13:41:49 -!- zemhill has quit (Remote host closed the connection).
13:42:01 -!- zemhill has joined.
13:46:01 -!- zemhill has quit (Remote host closed the connection).
13:46:13 -!- zemhill has joined.
13:46:36 -!- tromp_ has quit (Remote host closed the connection).
13:50:36 -!- zemhill has quit (Remote host closed the connection).
13:50:49 -!- zemhill has joined.
13:51:43 -!- vodkode has quit (Quit: Leaving).
13:55:43 -!- zemhill has quit (Remote host closed the connection).
13:55:55 -!- zemhill has joined.
13:59:55 -!- zemhill has quit (Remote host closed the connection).
14:00:07 -!- zemhill has joined.
14:04:07 -!- zemhill has quit (Remote host closed the connection).
14:04:19 -!- zemhill has joined.
14:08:19 -!- zemhill has quit (Remote host closed the connection).
14:08:31 -!- zemhill has joined.
14:09:05 -!- J_Arcane has joined.
14:12:35 -!- jaboja has quit (Ping timeout: 250 seconds).
14:16:35 -!- zemhill has quit (Remote host closed the connection).
14:16:49 -!- zemhill has joined.
14:19:36 -!- lynn_ has quit (Ping timeout: 244 seconds).
14:23:36 -!- zemhill has quit (Remote host closed the connection).
14:23:43 -!- spiette has joined.
14:23:48 -!- zemhill has joined.
14:27:48 -!- zemhill has quit (Remote host closed the connection).
14:28:00 -!- zemhill has joined.
14:30:39 <Taneb> brainfuck competition is tomorrow
14:34:20 -!- jaboja has joined.
14:38:20 -!- zemhill has quit (Remote host closed the connection).
14:38:31 -!- zemhill has joined.
14:42:31 -!- zemhill has quit (Remote host closed the connection).
14:42:43 -!- zemhill has joined.
14:46:43 -!- zemhill has quit (Remote host closed the connection).
14:46:56 -!- zemhill has joined.
14:47:11 -!- tromp_ has joined.
14:48:00 -!- lambda-11235 has joined.
14:51:47 -!- tromp_ has quit (Ping timeout: 248 seconds).
14:55:47 -!- zemhill has quit (Remote host closed the connection).
14:56:00 -!- zemhill has joined.
15:00:00 -!- zemhill has quit (Remote host closed the connection).
15:00:15 -!- zemhill has joined.
15:04:06 -!- `^_^v has joined.
15:06:47 -!- earendel2 has joined.
15:07:07 -!- earendel2 has left.
15:07:07 -!- earendel has quit (Disconnected by services).
15:07:09 -!- earendel has joined.
15:11:09 -!- zemhill has quit (Remote host closed the connection).
15:11:22 -!- zemhill has joined.
15:11:34 -!- ais523 has joined.
15:15:34 -!- zemhill has quit (Remote host closed the connection).
15:15:46 -!- zemhill has joined.
15:19:34 -!- AnotherTest has quit (Ping timeout: 240 seconds).
15:23:34 -!- zemhill has quit (Remote host closed the connection).
15:23:45 -!- zemhill has joined.
15:27:45 -!- zemhill has quit (Remote host closed the connection).
15:27:57 -!- zemhill has joined.
15:31:57 -!- zemhill has quit (Remote host closed the connection).
15:32:09 -!- zemhill has joined.
15:36:06 -!- AnotherTest has joined.
15:40:06 -!- zemhill has quit (Remote host closed the connection).
15:40:19 -!- zemhill has joined.
15:40:19 -!- AnotherTest has quit (Ping timeout: 248 seconds).
15:41:48 -!- J_Arcane has quit (Ping timeout: 244 seconds).
15:42:57 -!- bender| has quit (Quit: Leaving).
15:46:57 -!- zemhill has quit (Remote host closed the connection).
15:46:57 -!- AnotherTest has joined.
15:47:08 -!- zemhill has joined.
15:50:04 -!- jaboja has quit (Ping timeout: 240 seconds).
15:51:57 -!- vanila has joined.
15:52:02 <vanila> is this the occult room
15:52:45 <vanila> thanks so much oerjan!!!!!!!!!!
15:52:56 <HackEgo> vanila: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: <http://esolangs.org/>. (For the other kind of esoterica, try #esoteric on EFnet or DALnet.)
15:52:57 <ais523> I know you're a regular but this seems like a suitably passive-aggressive response
15:53:04 <vanila> ais523, I wonder why we aren't celebrating?
15:53:12 <vanila> there was a new brainfuck hello world WORLD RECORD
15:53:24 <ais523> I was happy about the last one
15:53:27 <vanila> it sould be all over the wiki
15:53:27 <ais523> I didn't know about this one though
15:53:33 <vanila> it was a few weeks ago
15:53:35 <ais523> what sort of hello world is it printing and what principle does it use?
15:53:47 <vanila> let me get the link you may have sen it already
15:53:51 <ais523> oh, I might have celebrated it already then
15:54:24 <b_jonas> a bf golf to print hello world should have a principle?
15:54:24 <vanila> b_jonas, it did some clever trick about preparing the differences between chars across half the string
15:54:34 <vanila> it wasn't just brute forced
15:54:39 <vanila> although there was some bruting
15:54:44 <vanila> invorlved in its creation
15:55:28 <ais523> vanila: in that case I've seen it ages ago and we've discussed it already
15:55:49 <ais523> I was hoping someone had found a cleverer trick than transforming the left half of the hello world into the right half
15:56:09 <vanila> i didnt mean to get hopes up
15:56:34 -!- lambda-11235 has quit (Quit: Bye).
15:57:23 <b_jonas> is it http://codegolf.stackexchange.com/a/68494/6691 ?
15:58:29 -!- AnotherTest has quit (Ping timeout: 240 seconds).
15:58:41 <vanila> this might be up peoples street here
15:58:47 <vanila> are you familiar with minikanren?
15:58:52 <b_jonas> let's mention it form http://esolangs.org/wiki/Brainfuck#Hello.2C_World.21
15:59:23 <vanila> its this prolog like thing that can generate quines
15:59:45 <vanila> from querying an interpreter like this: (eval q q)
16:00:11 <vanila> and the question is why can't you do this in prolog (with occurs check and fair search)
16:00:26 <vanila> https://www.reddit.com/r/prolog/comments/473hig/generating_scheme_quines_with_prolog/
16:00:33 <vanila> there's a link to all the code and stuff
16:00:54 <vanila> if anyone could figure out what the secret is.. someone here could (but I coudln't...)
16:02:12 <HackEgo> [wiki] [[Brainfuck]] https://esolangs.org/w/index.php?diff=46459&oldid=46402 * B jonas * (+180) /* Hello, World! */ golf
16:02:16 <vanila> is that even interesting to nayone i hope
16:02:36 <b_jonas> Rosetta seems to have only comma-less variants. What herecy!
16:05:48 -!- AnotherTest has joined.
16:05:53 <lambdabot> KSFO 231556Z 18003KT 10SM BKN200 11/10 A3008 RMK AO2 SLP185 T01060100 $
16:06:07 <vanila> was anyone at all interested in that :S
16:06:22 <vanila> its not exactly eso but its really cool imo
16:06:57 <int-e> vanila: since you asked, yes, I was interested, I just have nothing to add...
16:07:45 <vanila> if we found out the secret ingredient it could be aded to clue
16:07:55 <vanila> myabe it already has it though
16:11:55 -!- zemhill has quit (Remote host closed the connection).
16:12:07 -!- zemhill has joined.
16:12:29 -!- AnotherTest has quit (Ping timeout: 240 seconds).
16:16:29 -!- zemhill has quit (Remote host closed the connection).
16:16:43 -!- zemhill has joined.
16:17:20 -!- lynn has joined.
16:21:20 -!- zemhill has quit (Remote host closed the connection).
16:21:32 -!- zemhill has joined.
16:25:32 -!- zemhill has quit (Remote host closed the connection).
16:25:44 -!- zemhill has joined.
16:29:44 -!- zemhill has quit (Remote host closed the connection).
16:29:56 -!- zemhill has joined.
16:33:26 -!- digitalcold has quit (Ping timeout: 268 seconds).
16:34:00 -!- digitalcold has joined.
16:38:00 -!- zemhill has quit (Remote host closed the connection).
16:38:12 -!- zemhill has joined.
16:42:12 -!- zemhill has quit (Remote host closed the connection).
16:42:24 -!- zemhill has joined.
16:46:24 -!- zemhill has quit (Remote host closed the connection).
16:46:36 -!- zemhill has joined.
16:47:08 -!- p34k has joined.
16:47:18 -!- tromp_ has joined.
16:51:18 -!- zemhill has quit (Remote host closed the connection).
16:51:30 -!- zemhill has joined.
16:51:47 -!- tromp_ has quit (Ping timeout: 248 seconds).
16:55:47 -!- zemhill has quit (Remote host closed the connection).
16:55:59 -!- zemhill has joined.
16:56:05 -!- jaboja has joined.
17:00:05 -!- zemhill has quit (Remote host closed the connection).
17:00:18 -!- zemhill has joined.
17:03:42 <ais523> fizzie: zemhill seems to be in some sort of trouble
17:04:01 <ais523> I don't mind the effect on the channel (it's going pretty slowly), but you might want to check to see if the server's doing OK
17:07:53 <fizzie> I remember it getting into this sort of state before.
17:08:22 <fizzie> I see these messages in the console, but it's also trying to send "JOIN #esoteric" all the time.
17:08:39 <fizzie> I'm guessing it's some sort of a bug in the IRC library I used. Last time I just restarted it to fix it.
17:08:42 -!- zemhill has quit (Remote host closed the connection).
17:08:47 <fizzie> Will do the same again.
17:08:57 -!- zemhill has joined.
17:09:03 <fizzie> Should've known better than to write it in Ruby, I guess.
17:53:08 -!- MoALTz has quit (Quit: Leaving).
18:02:34 -!- AnotherTest has joined.
18:07:58 -!- callforjudgement has joined.
18:08:03 -!- ais523 has quit (Disconnected by services).
18:08:06 -!- callforjudgement has changed nick to ais523.
18:10:18 -!- MoALTz has joined.
18:16:56 -!- ais523 has quit (Read error: Connection reset by peer).
18:18:06 -!- ais523 has joined.
18:25:03 -!- lambda-11235 has joined.
18:28:04 -!- `^_^v has quit (Ping timeout: 240 seconds).
18:31:47 -!- `^_^v has joined.
18:36:26 <prooftechnique> vanila: Nearly every problem I ever had with Prolog was solved by generously sprinkling cuts around the place
18:43:03 -!- Phantom_Hoover has joined.
18:52:24 -!- jaboja has quit (Ping timeout: 276 seconds).
18:58:47 -!- bb010g has quit (Quit: Connection closed for inactivity).
19:03:17 -!- jaboja has joined.
19:21:29 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds).
19:22:51 -!- Phantom_Hoover has joined.
19:23:49 -!- zyla has joined.
19:31:05 -!- hppavilion[1] has joined.
19:33:47 -!- earendel has quit (Changing host).
19:33:47 -!- earendel has joined.
19:41:08 <b_jonas> so those strange things Wrecan says in #1025 are a reference to something actually
19:42:52 -!- ais523 has quit (Ping timeout: 255 seconds).
19:48:02 -!- ais523 has joined.
19:55:44 -!- zyla has left ("WeeChat 1.1.1").
19:55:53 <hppavilion[1]> I'm reading the "gentlest introduction to the ρ-calculus"
19:57:17 <vanila> is that pattern matching
19:59:16 <hppavilion[1]> vanila: I'm trying to figure out rho-expressions (analogous to lambda-expressions) for a LISP
19:59:39 <vanila> might be fun to learn abuot
20:00:13 <hppavilion[1]> vanila: This is the only introduction I could find: http://rho.loria.fr/data/rta2001.pdf
20:02:57 -!- nycs has joined.
20:04:59 -!- `^_^v has quit (Ping timeout: 240 seconds).
20:13:22 -!- earendel has quit (Ping timeout: 252 seconds).
20:16:09 -!- lambda-11235 has quit (Quit: Bye).
20:20:35 -!- MDream has changed nick to MDude.
20:25:40 <hppavilion[1]> prooftechnique: That site without the path should take you there, but it doesn't seem to have much
20:28:46 <prooftechnique> hppavilion[1]: Though I am now also reading that rho paper :D
20:31:08 <prooftechnique> It sort of looks like a weird extension of normal state machine productions, but I'm only on the second page. Embedding LC sounds promising, anyway
20:31:59 <hppavilion[1]> prooftechnique: What would be the rho analogue to a lambda expression in a LISP?
20:34:16 <vanila> rho rho rho of rank always equals one
20:36:24 -!- `^_^v has joined.
20:36:35 -!- nycs has quit (Read error: No route to host).
20:41:01 <prooftechnique> \lam X . b seems to be just a rewrite rule X -> b. Maybe something like (defun rho (lhs rhs) (lambda lhs rhs))? So then conditionals look like (defun cond-rho (lhs rhs cond) ((rho lhs (rho 't rhs)) cond)
20:41:43 <prooftechnique> Where we assume cond has already been normalized by strat
20:44:56 <prooftechnique> Ew, but then I get to the examples, and of course it's not that simple
20:48:01 -!- hppavilion[1] has quit (Ping timeout: 252 seconds).
20:48:07 -!- lambda-11235 has joined.
20:50:26 <prooftechnique> @tell hppavilion[1] http://link.springer.com/chapter/10.1007%2F3-540-45315-6_11
20:58:15 -!- lambda-11235 has quit (Quit: Bye).
21:08:04 -!- hppavilion[1] has joined.
21:08:43 <hppavilion[1]> I'm wondering what branch of mathematics to base a proof assistant on- what prooftechnique(s) to use
21:08:53 <hppavilion[1]> prooftechnique: You seem like a good person to ask
21:09:09 <vanila> base it on typed lambda calculus
21:09:20 <hppavilion[1]> vanila: Perhaps. Maybe I should make more than one?
21:09:32 <vanila> the little prover book
21:09:40 <vanila> its a different sort of prover
21:13:03 <hppavilion[1]> vanila: Perhaps I should make a proof assistant with strings as a primitive type?
21:13:19 <hppavilion[1]> vanila: Perhaps even using (bit)strings for numbers, making them a derived type?
21:13:50 <vanila> do you have any theorems in mind you want ot prove with it
21:14:02 <hppavilion[1]> vanila: No; just want to make one for the experience
21:14:15 <lambdabot> prooftechnique said 23m 46s ago: http://link.springer.com/chapter/10.1007%2F3-540-45315-6_11
21:14:34 <vanila> pick some slighlty nontrivial theorem you like
21:14:35 <hppavilion[1]> vanila: Perhaps I should. What's a good theorem to start with with a known proof?
21:14:38 <vanila> and make a prover that can prove it
21:16:07 <hppavilion[1]> vanila: If I do the Pythagorean Theorem, I have lots of options for proofs
21:16:21 <hppavilion[1]> vanila: I'm thinking of making more than one, each in a different niche
21:17:41 <vanila> a proof should be a polytime checkable object
21:17:57 <vanila> i haddnt even finished
21:18:41 <hppavilion[1]> vanila: In fact, if it's NP, it hardly counts as a proof IMO
21:18:55 <vanila> P = Proof, NP = Not a Proof
21:19:37 <vanila> what's the name of this..
21:22:26 <hppavilion[1]> vanila: I'm thinking of including multityping- a single value can be a member of more than one type
21:25:56 -!- ais523 has quit.
21:25:58 <hppavilion[1]> e.g. 5 is NATURAL, WHOLE, INTEGER, REAL, COMPLEX, SPLIT, DUAL, GAUSS, SPLIT_GAUSS, DUAL_GAUSS
21:26:07 <hppavilion[1]> And maybe PRIME if I include it, but I probably won't
21:30:08 <fizzie> Scheme has a numerical tower vaguely like that.
21:31:47 <fizzie> Goes number ⊇ complex ⊇ real ⊇ rational ⊇ integer, approximately.
21:32:17 -!- jaboja has quit (Remote host closed the connection).
21:32:29 <fizzie> "For example, 3 is an integer. Therefore 3 is also a rational, a real, and a complex." (R5RS 6.2.1)
21:33:31 <fizzie> (They're strict subtypes of the higher-level ones, though.)
21:34:46 -!- hppavilion[1] has quit (Ping timeout: 252 seconds).
21:40:51 -!- MDude has quit (Ping timeout: 248 seconds).
21:46:04 -!- lynn_ has joined.
21:46:19 -!- lynn has quit (Ping timeout: 252 seconds).
21:46:27 -!- earendel has joined.
21:51:25 -!- mihow has joined.
22:15:35 -!- hppavilion[1] has joined.
22:20:35 -!- XorSwap has joined.
22:22:19 -!- `^_^v has quit (Quit: This computer has gone to sleep).
22:28:40 -!- AnotherTest has quit (Ping timeout: 252 seconds).
22:45:43 -!- XorSwap has quit (Ping timeout: 252 seconds).
22:58:08 -!- zemhill has quit (*.net *.split).
22:58:09 -!- relrod has quit (*.net *.split).
22:58:09 -!- hppavilion[1] has quit (*.net *.split).
22:58:09 -!- Xe has quit (*.net *.split).
22:58:10 -!- sebbu has quit (*.net *.split).
22:58:10 -!- deltab has quit (*.net *.split).
22:58:10 -!- erdic has quit (*.net *.split).
22:58:10 -!- Froox has quit (*.net *.split).
22:58:10 -!- newsham has quit (*.net *.split).
22:58:11 -!- nisstyre has quit (*.net *.split).
22:58:11 -!- Deewiant has quit (*.net *.split).
22:58:12 -!- mad has quit (*.net *.split).
22:58:12 -!- ^v has quit (*.net *.split).
22:58:12 -!- int-e has quit (*.net *.split).
22:58:12 -!- tswett has quit (*.net *.split).
22:58:12 -!- copumpkin has quit (*.net *.split).
22:58:12 -!- coppro has quit (*.net *.split).
22:58:13 -!- vifino has quit (*.net *.split).
22:58:13 -!- Phantom_Hoover has quit (*.net *.split).
22:58:13 -!- p34k has quit (*.net *.split).
22:58:13 -!- fungot has quit (*.net *.split).
22:58:14 -!- Treio has quit (*.net *.split).
22:58:15 -!- yorick__ has quit (*.net *.split).
22:58:15 -!- pikhq has quit (*.net *.split).
22:58:15 -!- lleu has quit (*.net *.split).
22:58:16 -!- prooftechnique has quit (*.net *.split).
22:58:16 -!- augur has quit (*.net *.split).
22:58:16 -!- jameseb has quit (*.net *.split).
22:58:16 -!- mihow has quit (*.net *.split).
22:58:17 -!- vanila has quit (*.net *.split).
22:58:17 -!- carado has quit (*.net *.split).
22:58:17 -!- kline has quit (*.net *.split).
22:58:18 -!- zgrep has quit (*.net *.split).
22:58:18 -!- staffehn has quit (*.net *.split).
22:58:18 -!- FreeFull has quit (*.net *.split).
22:58:19 -!- Lord_of_Life has quit (*.net *.split).
22:58:19 -!- jix_ has quit (*.net *.split).
22:58:19 -!- lynn_ has quit (*.net *.split).
22:58:20 -!- MoALTz has quit (*.net *.split).
22:58:21 -!- quintopia has quit (*.net *.split).
22:58:21 -!- EgoBot has quit (*.net *.split).
22:58:21 -!- Gregor has quit (*.net *.split).
22:58:21 -!- mtve has quit (*.net *.split).
22:58:21 -!- nitrix has quit (*.net *.split).
22:58:22 -!- idris-bot has quit (*.net *.split).
22:58:22 -!- rodgort has quit (*.net *.split).
22:58:22 -!- kragniz has quit (*.net *.split).
22:58:23 -!- spiette has quit (*.net *.split).
22:58:23 -!- gniourf has quit (*.net *.split).
22:58:23 -!- Sgeo has quit (*.net *.split).
22:58:23 -!- FireFly has quit (*.net *.split).
22:58:24 -!- heroux has quit (*.net *.split).
22:58:24 -!- clog has quit (*.net *.split).
22:58:24 -!- Vorpal has quit (*.net *.split).
22:58:24 -!- cnr has quit (*.net *.split).
22:58:24 -!- diginet has quit (*.net *.split).
22:58:25 -!- earendel has quit (*.net *.split).
22:58:25 -!- aloril has quit (*.net *.split).
22:58:25 -!- puckipedia has quit (*.net *.split).
22:58:26 -!- tromp has quit (*.net *.split).
22:58:26 -!- Alcest has quit (*.net *.split).
22:58:26 -!- izabera has quit (*.net *.split).
22:58:26 -!- fractal has quit (*.net *.split).
22:58:26 -!- pdxleif has quit (*.net *.split).
22:58:26 -!- paul2520 has quit (*.net *.split).
22:58:27 -!- incomprehensibly has quit (*.net *.split).
22:58:27 -!- Riviera has quit (*.net *.split).
22:58:27 -!- ocharles_ has quit (*.net *.split).
22:58:27 -!- Hoolootwo has quit (*.net *.split).
22:58:28 -!- Nithogg has quit (*.net *.split).
22:58:28 -!- hydraz has quit (*.net *.split).
22:58:28 -!- myname has quit (*.net *.split).
22:58:28 -!- mbrcknl has quit (*.net *.split).
22:58:29 -!- fizzie has quit (*.net *.split).
22:58:30 -!- Veltas has quit (*.net *.split).
22:58:30 -!- \oren\ has quit (*.net *.split).
22:58:30 -!- digitalcold has quit (*.net *.split).
22:58:30 -!- APic has quit (*.net *.split).
22:58:31 -!- Sprocklem has quit (*.net *.split).
22:58:31 -!- atehwa has quit (*.net *.split).
22:58:31 -!- catern has quit (*.net *.split).
22:58:31 -!- Melvar has quit (*.net *.split).
22:58:32 -!- Taneb has quit (*.net *.split).
22:58:32 -!- j-bot has quit (*.net *.split).
22:58:32 -!- nortti has quit (*.net *.split).
22:58:32 -!- shachaf has quit (*.net *.split).
22:58:32 -!- b_jonas has quit (*.net *.split).
22:58:32 -!- ski has quit (*.net *.split).
23:00:27 -!- vifino has joined.
23:00:27 -!- coppro has joined.
23:00:27 -!- copumpkin has joined.
23:00:27 -!- tswett has joined.
23:00:27 -!- int-e has joined.
23:00:27 -!- ^v has joined.
23:00:27 -!- Deewiant has joined.
23:00:27 -!- mad has joined.
23:00:27 -!- jameseb has joined.
23:00:27 -!- augur has joined.
23:00:27 -!- prooftechnique has joined.
23:00:27 -!- lleu has joined.
23:00:27 -!- pikhq has joined.
23:00:27 -!- yorick__ has joined.
23:00:27 -!- Treio has joined.
23:00:27 -!- fungot has joined.
23:00:27 -!- p34k has joined.
23:00:27 -!- Phantom_Hoover has joined.
23:00:27 -!- mbrcknl has joined.
23:00:27 -!- myname has joined.
23:00:27 -!- hydraz has joined.
23:00:27 -!- Nithogg has joined.
23:00:27 -!- Hoolootwo has joined.
23:00:27 -!- ocharles_ has joined.
23:00:27 -!- Riviera has joined.
23:00:27 -!- incomprehensibly has joined.
23:00:31 -!- augur has quit (Remote host closed the connection).
23:00:56 -!- mihow has joined.
23:00:56 -!- vanila has joined.
23:00:56 -!- carado has joined.
23:00:56 -!- zgrep has joined.
23:00:56 -!- staffehn has joined.
23:00:56 -!- FreeFull has joined.
23:00:56 -!- Lord_of_Life has joined.
23:00:56 -!- jix_ has joined.
23:00:59 -!- zemhill has joined.
23:01:01 -!- relrod has joined.
23:01:05 -!- lynn_ has joined.
23:01:05 -!- MoALTz has joined.
23:01:05 -!- spiette has joined.
23:01:05 -!- gniourf has joined.
23:01:05 -!- Sgeo has joined.
23:01:05 -!- FireFly has joined.
23:01:05 -!- heroux has joined.
23:01:05 -!- clog has joined.
23:01:05 -!- EgoBot has joined.
23:01:05 -!- quintopia has joined.
23:01:05 -!- Vorpal has joined.
23:01:05 -!- cnr has joined.
23:01:05 -!- Gregor has joined.
23:01:05 -!- mtve has joined.
23:01:05 -!- nitrix has joined.
23:01:05 -!- diginet has joined.
23:01:05 -!- idris-bot has joined.
23:01:05 -!- rodgort has joined.
23:01:05 -!- kragniz has joined.
23:01:43 -!- Xe has joined.
23:02:05 -!- hppavilion[1] has joined.
23:02:05 -!- sebbu has joined.
23:02:05 -!- erdic has joined.
23:02:05 -!- deltab has joined.
23:02:05 -!- Froox has joined.
23:02:05 -!- newsham has joined.
23:02:05 -!- kline has joined.
23:03:00 -!- digitalcold has joined.
23:03:00 -!- APic has joined.
23:03:00 -!- Sprocklem has joined.
23:03:00 -!- atehwa has joined.
23:03:00 -!- catern has joined.
23:03:00 -!- Melvar has joined.
23:03:00 -!- Taneb has joined.
23:03:00 -!- j-bot has joined.
23:03:00 -!- nortti has joined.
23:03:00 -!- shachaf has joined.
23:03:00 -!- b_jonas has joined.
23:03:00 -!- ski has joined.
23:03:04 -!- Veltas has joined.
23:03:04 -!- \oren\ has joined.
23:03:17 -!- nisstyre has joined.
23:03:17 -!- fizzie has joined.
23:03:43 -!- nisstyre has quit (Max SendQ exceeded).
23:03:46 -!- augur has joined.
23:03:49 -!- augur has quit (Remote host closed the connection).
23:04:00 -!- zgrep has quit (Ping timeout: 240 seconds).
23:04:25 -!- hppavilion[1] has quit (Ping timeout: 252 seconds).
23:04:34 -!- aloril_ has joined.
23:04:41 -!- catern has quit (Excess Flood).
23:05:11 -!- catern has joined.
23:05:53 -!- Xe has quit (Changing host).
23:05:53 -!- Xe has joined.
23:05:56 -!- nisstyre_ has joined.
23:06:26 -!- aloril has joined.
23:06:26 -!- puckipedia has joined.
23:06:26 -!- tromp has joined.
23:06:26 -!- Alcest has joined.
23:06:26 -!- izabera has joined.
23:06:26 -!- fractal has joined.
23:06:26 -!- pdxleif has joined.
23:06:26 -!- paul2520 has joined.
23:06:39 -!- kline has quit (Changing host).
23:06:40 -!- kline has joined.
23:06:51 -!- earendel has joined.
23:07:01 -!- Alcest has quit (Max SendQ exceeded).
23:07:01 -!- aloril has quit (Max SendQ exceeded).
23:08:41 -!- mihow has quit (Quit: mihow).
23:10:31 -!- augur has joined.
23:11:48 -!- gde33 has joined.
23:12:17 -!- lynn_ has quit (Ping timeout: 244 seconds).
23:12:31 -!- lynn has joined.
23:14:42 -!- mihow has joined.
23:18:41 -!- spiette has quit (Quit: :qa!).
23:25:34 <FireFly> what is a number that a complex isn't?
23:28:45 -!- boily has joined.
23:31:07 -!- zgrep has joined.
23:34:13 -!- ais523 has joined.
23:35:15 -!- ais523 has quit (Client Quit).
23:35:24 -!- ais523 has joined.
23:42:09 <HackEgo> category theory/In category theory, category theory is a theory in the category of theories.
23:42:46 <shachaf> `` sed -i 's/category theory/the theory of categories/' wisdom/category\ theory
23:43:04 <HackEgo> In the theory of categories, category theory is a theory in the category of theories.
23:44:48 -!- hppavilion[1] has joined.
23:48:59 <HackEgo> A category is an enriched category where the enriching category is the category of classes.
23:49:40 <boily> HackEgo has no class.
23:53:11 <ais523> how many of the category theory wisdoms are actually mathematically accurate?
23:53:14 <HackEgo> Monads are just monoids in the category of endofunctors.
23:53:20 <HackEgo> Comonads are just monads in the dual category.
23:53:32 <ais523> that one is I think? not 100% sure
23:53:39 <ais523> it may be missing details
23:53:48 <fizzie> FireFly: As far as I know, nothing in standard R5RS, but it does have both number? and complex? predicates.
23:54:09 <fizzie> "In many implementations the rational? procedure will be the same as real?, and the complex? procedure will be the same as number?, but unusual implementations may be able to represent some irrational numbers exactly or may extend the number system to support some kind of non-complex numbers."
23:54:29 <boily> his523. comonads are right.
23:58:19 -!- J_Arcane has joined.
23:58:20 <hppavilion[1]> `le/rn theory/To be theory is to be like a theorem, but inferior
23:58:45 <hppavilion[1]> It's a proof assistant based on string rewriting. It's utterly useless.
23:59:13 <hppavilion[1]> And I can't test it because I don't know of any good theorems/axiom schemas to test it on
23:59:29 <HackEgo> forty means "in a fort-like manner"