00:03:24 -!- tromp has quit (Ping timeout: 252 seconds).
00:09:46 -!- Sgeo__ has joined.
00:13:04 -!- Sgeo_ has quit (Ping timeout: 258 seconds).
00:18:53 <tswett[m]> You know, it's very rare that I receive an email from another human being sent specifically to me. :D
00:18:53 <tswett[m]> Most of my email comes from "the Algorithm".
00:20:05 <zzo38> Then what is it for if not specifically for you? Mailing lists? Wide notifications?
00:20:43 <tswett[m]> Yeah, mailing lists and automated emails.
00:22:47 * kmc obeys and worships The Algorithm
00:23:13 <zzo38> I do not have any mailing lists or automated notifications (although I have occasionally received automated replies); all of the messages I receive are someone writing to me specifically. I have sometimes received spam messages, but when that happens I edit my /etc/aliases file so that they can't send it anymore.
00:24:34 <zzo38> (I have several email addresses, so if the spam is prevented in this way, it will not usually prevent legitimate messages.)
00:47:24 -!- tromp has joined.
00:51:49 -!- tromp has quit (Ping timeout: 252 seconds).
00:53:42 -!- tromp has joined.
00:54:58 -!- tromp_ has joined.
00:58:03 -!- tromp has quit (Ping timeout: 252 seconds).
00:59:31 -!- tromp_ has quit (Ping timeout: 252 seconds).
01:09:13 -!- atslash has quit (Quit: This computer has gone to sleep).
01:15:31 -!- tromp has joined.
01:17:51 -!- tromp_ has joined.
01:20:46 -!- tromp has quit (Ping timeout: 276 seconds).
01:22:43 -!- tromp_ has quit (Ping timeout: 276 seconds).
01:47:40 -!- Lord_of_Life has quit (Ping timeout: 246 seconds).
01:47:54 -!- xkapastel has quit (Quit: Connection closed for inactivity).
01:56:13 -!- Lord_of_Life has joined.
02:00:28 -!- FreeFull has quit.
06:04:26 -!- mapleBloodRed has joined.
06:11:38 -!- mapleBloodRed has quit (Read error: Connection reset by peer).
06:15:36 -!- Frater_EST has joined.
06:28:42 -!- akozar has joined.
06:57:14 <HackEso> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch [<output-file>] <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
06:57:18 -!- tromp has joined.
07:09:22 <int-e> akozar: I came up with https://int-e.eu/~bf3/tmp/primes.sme.txt just after you left earlier
07:10:06 <int-e> akozar: (which is borderline cheating because all the sieving is already done during initialization)
07:11:40 <akozar> WOW! That's incredible!
07:13:29 <akozar> Nice work! I'm assuming that it requires more lines to search higher?
07:18:09 <akozar> I think that you can remove the steps An+A where A is not prime, but of course then you have to know some of the primes in advance. ;-)
07:23:32 <akozar> int-e: I was figuring out how your unary counter program worked earlier. Thanks for these examples!
07:28:00 <akozar> And just before you messaged, I was checking out the info about tiling rectangles on your web site. Neat stuff. I enjoy combinatorial problems. ^_^
07:33:19 <int-e> Hmm I might still revisit that one at some point.
07:36:35 -!- b_jonas has quit (Quit: leaving).
07:42:25 -!- tromp has quit (Remote host closed the connection).
08:02:32 -!- tromp has joined.
08:09:52 -!- akozar has quit (Quit: akozar).
08:17:53 <int-e> tswett[m]: I have an unbounded binary counter :) https://int-e.eu/~bf3/tmp/binary.sme.txt
08:27:41 <esowiki> [[Klaus/Dense]] N https://esolangs.org/w/index.php?oldid=64228 * A * (+644) Thank you @Areallycoolusername
08:28:54 <esowiki> [[Klaus/Dense]] https://esolangs.org/w/index.php?diff=64229&oldid=64228 * A * (+3932) Fix typos and more info; Ctrl+C Ctrl+V first
08:39:03 <esowiki> [[Klaus/Dense]] M https://esolangs.org/w/index.php?diff=64230&oldid=64229 * A * (+120) Do partial work
08:52:49 <int-e> But this should not distract from the fact that this is a really annoying language to work in.
08:53:19 <esowiki> [[Klaus/Dense]] M https://esolangs.org/w/index.php?diff=64231&oldid=64230 * A * (+29) Hello World not yet translated.
08:54:40 -!- atslash has joined.
08:56:40 -!- arseniiv has joined.
08:59:13 -!- atslash has quit (Ping timeout: 245 seconds).
08:59:50 -!- atslash has joined.
09:03:22 <esowiki> [[Klaus/Dense]] M https://esolangs.org/w/index.php?diff=64232&oldid=64231 * A * (+124)
09:11:24 <esowiki> [[Klaus/Dense]] M https://esolangs.org/w/index.php?diff=64233&oldid=64232 * A * (-33) Simpler syntax to compile to Klaus
09:15:05 <esowiki> [[Klaus/Dense]] M https://esolangs.org/w/index.php?diff=64234&oldid=64233 * A * (+2)
09:23:47 <esowiki> [[Klaus/Dense]] M https://esolangs.org/w/index.php?diff=64235&oldid=64234 * A * (-100)
09:27:21 <esowiki> [[Klaus/Dense]] M https://esolangs.org/w/index.php?diff=64236&oldid=64235 * A * (+5)
09:35:06 -!- atslash has quit (Quit: Leaving).
09:35:42 <esowiki> [[Klaus/Dense]] M https://esolangs.org/w/index.php?diff=64237&oldid=64236 * A * (+12)
09:45:13 -!- atslash has joined.
10:28:31 -!- AnotherTest has joined.
10:46:40 <esowiki> [[Playlist]] N https://esolangs.org/w/index.php?oldid=64238 * A * (+1108) Created page with "[[Playlist]] is an esoteric programming language based on playlists. ==Rules of operation== Playlist operates over a playlist. There are a few commands in Playlist; they are..."
10:47:30 <esowiki> [[Playlist]] M https://esolangs.org/w/index.php?diff=64239&oldid=64238 * A * (+91)
10:48:59 <esowiki> [[Playlist]] M https://esolangs.org/w/index.php?diff=64240&oldid=64239 * A * (+127)
10:50:54 <esowiki> [[Playlist]] M https://esolangs.org/w/index.php?diff=64241&oldid=64240 * A * (+65) /* Example programs */
10:59:51 -!- nfd9001 has joined.
11:00:40 -!- nfd has quit (Ping timeout: 246 seconds).
11:25:33 -!- xkapastel has joined.
11:46:25 -!- Frater_EST has left.
11:56:34 <lambdabot> Local time for shachaf is Fri Jul 12 04:56:31 2019
11:57:06 <shachaf> ski: This probably doesn't make much sense because it's a thought I had lying in bed at 5 in the morning, but I feel like linear logic par is actually obvious and straightforward.
11:58:25 <shachaf> It just means "or" in one aspect of the classical logic sense: A # B means that "at least one" of A,B is true.
11:59:18 <shachaf> Which means you can turn a refutation of A into a proof of B, and a refutation of B into a proof of A. Which is just the standard thing that document said.
11:59:47 <shachaf> Say, for any natural n, I can tell you that either n is odd or Sn is odd. That means that if you show me that n is even, then I can prove that Sn is odd, and vice versa.
12:00:09 <shachaf> That all seems very simple so can someone remind me what's confusing about par?
12:04:44 <ski> well, consider the proof that for any prime integer `p', if `p' divides `a*b', then `p' divides `a', or `p' divides `b'
12:05:31 <ski> the standard proof of this has the basic shape "suppose `p' does not divide `a'. ... thus `p' divides `b'"
12:06:10 <ski> which seems to me to be exactly the kind of thing that a proof of a multiplicative disjunction would be
12:07:25 <ski> instead of "eagerly" pointing out which alternative we're to prove, we "lazily" wait for our opponent to disprove one disjunct, and only then do we prove the other one (possibly using information that we get from the disproof)
12:08:14 <esowiki> [[Klaus]] M https://esolangs.org/w/index.php?diff=64242&oldid=64225 * A * (+108) No, it is TC
12:08:23 <ski> however, when using this proof, what if we instead of disproving the first disjunct, instead disprove the second one ?
12:08:51 <ski> then we'd have to be able to from that derive a proof of "`p' divides `a'" -- how does that work ?
12:08:58 <esowiki> [[Klaus]] M https://esolangs.org/w/index.php?diff=64243&oldid=64242 * A * (+30) +CAT
12:09:09 <ski> well, in this case, we're in a symmetric situation. but in general, that won't be the case
12:09:55 <ski> so, it seems that one option would be to store both a function from disproof of left disjunct to proof of right disjunct, and a function from disproof of right disjunct to proof of left disjunct
12:10:57 <ski> and here my creeping suspicion is coming in that perhaps, if we take any such pair of functions, then won't necessarily "correspond to each other" (whatever that means)
12:11:10 <shachaf> Here's one odd thing -- I think people end up with expressions like "A # A" in linear logic. I'm not quite sure what that would mean.
12:11:47 <shachaf> Probably because I'm now thinking of these things as truth values, which doesn't work.
12:12:08 <ski> anyway, another option might be to analyze the construction from disproof of left disjunct to proof of right disjunct, in such a way that we can also interpret it as function from disproof of right disjunct to proof of left disjunct, effectively "reversing" it
12:12:34 <shachaf> I kind of like the fact that par is obviously symmetric, unlike functions.
12:13:02 <shachaf> (But the connection to modus tollens that someone mentioned the other day is what made me think of this.)
12:13:22 <ski> so, the one direction (considered as an intuitionistic function, via some forgetful, perhaps) would begat the other direction (which we can also consider in such a way), and then these two (the forgetful versions) would "correspond" in the desired way to each other
12:14:01 <shachaf> I'm not sure quite what you would want from such a correspondence.
12:14:46 <shachaf> Whatever it is it makes sense to want it to arise naturally from the way you write your proofs-or-whatever.
12:14:48 <ski> yeah, by "in this case, we're in a symmetric situation. but in general, that won't be the case", i meant that it's not obvious how to reach from `A^- -> B^+' to `B^- -> A^+', where `A' and `B' may look quite different (as opposed to the above example)
12:15:40 <shachaf> All your logic rules should presumably package up the forward and backward directions together.
12:15:52 <ski> "it makes sense to want it to arise naturally from the way you write your proofs-or-whatever" -- yes
12:16:39 <ski> but from a model-theoretic viewpoint, where we don't consider proofs ?
12:17:05 <shachaf> I don't know what you would want.
12:17:15 * ski neither ..
12:17:28 <shachaf> Informally, I think of "!a" as meaning something like "T & a & a*a & a*a*a & ..." -- a tensor of some number of copies of a, where you get to choose the number.
12:18:01 <shachaf> The De Morgan dual of that would be (0 + a + a#a + a#a#a + ...)
12:19:29 <shachaf> As an implication, you can say that a#a#a = (~a*~a*~a -o _|_)
12:19:57 <shachaf> So it's a thing that takes some number of copies of ~a
12:20:35 <shachaf> Wait, instead of T I should have said 1, and instead of 0 I should have said _|_
12:20:43 <ski> anyway, you can perhaps consider a rule something like from `Gamma , n : neg A |- e : B' derive `Gamma |- {@n |-> e} : A # B' .. hmm
12:21:19 <ski> the point being that we decide to "wait for" a refutaion of `A', and express the proof of `B' in terms of that
12:22:14 <ski> re `!', in that case i'm also pondering if we want some kind of condition on that, to express that "all the `a's are copies of each other"
12:22:36 <ski> (all the `a's in a single "term", i.e.)
12:23:17 <ski> the `T & a & a*a & a*a*a & ...' means that we'll pick how many `a's we like, at least
12:23:51 <ski> and so `0 + a + a#a + a#a#a + ...' means that the context (the opponent) will pick "how many `a's" we'll get fed by it
12:23:53 <shachaf> (It's 1 & a & ..., not T & a & ... -- T is the unit of & and 1 is the unit of *, which was the one I meant.)
12:24:26 <ski> (yea, but i write the additive truth as `1' anyway, so .. :)
12:24:44 <ski> (because it's terminal object)
12:24:58 <shachaf> That's actually a pretty good reason.
12:25:24 <ski> maybe. i'm not sure ;)
12:25:30 <shachaf> Thinking of "a" as a thing that's true or false, a#a makes no sense
12:25:54 <shachaf> So that's not the thing to think in linear logic. Which I already knew of course.
12:26:36 <ski> some systems have a "mix" rule that allows you to derive `A * B |- A # B', iirc
12:27:01 <ski> pretending that the computations corresponding to `A' and `B' communicate, while they actually don't
12:27:24 <ski> and then you can prove `|- 1 # 1' (`1' being mult. truth)
12:27:46 <shachaf> I don't think I have a good feel for the meaning of the four units.
12:28:40 <ski> `*' is "aggregation", and so `1' is "an empty space"
12:28:41 <HackEso> /srv/hackeso-code/multibot_cmds/lib/limits: line 5: exec: *': not found
12:30:20 <ski> (er, i should have used `T' of course in `T # T', if i was intending to be consistent with myself. `T' being mult. truth)
12:30:35 <ski> anyway, say you want to prove `T -o A' and `A -o _|_' (`_|_' being mult. false)
12:30:43 <shachaf> Do you have a + b |- a # b in any case?
12:30:45 <ski> prove them together, i mean
12:34:00 <ski> (i was trying to remember a point which i thought i had made in this situation. but now i'm not sure it's there. perhaps because i misremembered some details about the situation ?)
12:35:43 <lambdabot> Local time for shachaf is Fri Jul 12 05:35:40 2019
12:36:19 <shachaf> Thanks for the help. I'll think about it more when I wake up.
12:58:51 -!- nfd has joined.
12:58:54 -!- arseniiv_ has joined.
12:59:41 -!- stux- has joined.
13:00:14 <Taneb> Something I've just thought about
13:00:14 <Taneb> Consider the category "2" which has two objects and a morphism between them
13:00:14 <Taneb> I think there is an adjunction Set |- 2 (if I've got that notation right, I'm not very good at adjunctions)
13:00:14 -!- arseniiv has quit (Read error: Connection reset by peer).
13:00:15 <Taneb> Which maps the empty set to the codomain of the single non-identity arrow in 2, and all other sets to its domain
13:00:15 -!- sftp has quit (Excess Flood).
13:00:31 <Taneb> The reverse of this maps the codomain to the empty set and the domain to any non-empty set, e.g. {{}}
13:00:36 -!- sftp has joined.
13:01:43 -!- nfd9001 has quit (Ping timeout: 245 seconds).
13:02:09 -!- stux|away has quit (Ping timeout: 245 seconds).
13:19:07 <tswett[m]> Usually I just think of a # b as meaning ~a -o b, or equivalently ~b -o a, or equivalently ~(~a * ~b).
13:23:00 <tswett[m]> Let me try to remember here. There's a "protocol semantics" for linear logic. Any formula in linear logic represents a protocol.
13:24:18 <tswett[m]> Generally, you can submit a request to a protocol. After you do, you must wait for a response from that protocol. A protocol can "finish" after responding; if it does, then you have successfully consumed that protocol. However, a protocol can also finish *without* responding, in which case you have not successfully consumed the protocol.
13:25:03 <tswett[m]> You know what, I don't think I'm making any sense. So I'm going to start over.
13:25:19 <tswett[m]> There's a "ball game" semantics for linear logic. Any formula in linear logic represents a person who desires to participate in the game.
13:25:43 -!- stux- has quit (Quit: Aloha!).
13:25:57 -!- stux|away has joined.
13:26:51 <tswett[m]> Initially, you have the ball. In order to win the game (that is, in order to successfully consume the formula you are given), you must get everyone to leave the game, and you must possess the ball.
13:27:10 <tswett[m]> The semantics of the various connectives are...
13:27:19 <tswett[m]> 1 - A player who goes home immediately.
13:27:54 <tswett[m]> Bot - A player who waits to be thrown the ball, and then takes the ball and goes home with it.
13:28:16 <tswett[m]> Top - A player who refuses to go home under any circumstances.
13:29:18 <tswett[m]> 0 - A player who allows you to win the game immediately, by sending all the other players home (even Top), taking any excess balls, and giving you a ball if you need one.
13:29:40 <tswett[m]> a + b - A player who chooses either a or b to substitute for herself.
13:30:03 <tswett[m]> a & b - A player who allows you to pick either a or b, and has the player you chose substitute for herself.
13:31:02 <tswett[m]> a * b - A player who has both a and b standing behind her; when you throw her the ball, she will pass it on to either a or b (your choice), and also pass along any messages. When she receives the ball back from a or b, she throws it back to you.
13:37:58 <tswett[m]> a # b - A player who has both a and b standing behind her, and also has a ball in her pocket. When you throw her the ball, she then throws one ball each to a and b. Whenever she gets a ball back from either one, she throws it back to you; her team then sits and waits to receive the ball again, at which point she will throw it to whichever of her two subordinates she most recently got the ball from.
13:39:52 <tswett[m]> She will not go home until both of her subordinates have gone home and she has thrown you as many balls as you have thrown her.
13:42:00 <tswett[m]> ~a - A player who waits to be thrown the ball, then behaves like *you* are a player of type "a". This player will not go home until she has won (that is, she's done what is necessary to make a player of type "a" go home, and she has the ball).
13:43:06 <tswett[m]> So, all this explains why 1 # Bot can be successfully consumed, but 1 # 1 and Bot # Bot cannot be.
13:43:54 <tswett[m]> In the case of 1 # Bot, 1 goes home immediately; # throws a ball to Bot, who goes home with it; and # throws the other ball to you and goes home.
13:44:05 <tswett[m]> In the case of 1 # 1, both 1s go home immediately, so # has nobody to throw the extra ball to.
13:44:19 <tswett[m]> And in the case of Bot # Bot, # throws a ball to each Bot, they both go home, and # will never get the ball back like she wants.
13:46:12 -!- Lord_of_Life_ has joined.
13:49:34 -!- Lord_of_Life has quit (Ping timeout: 258 seconds).
13:49:36 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
14:45:11 -!- xkapastel has quit (Quit: Connection closed for inactivity).
14:57:59 <tswett[m]> I know I didn't get it *quite* right, but I think I was pretty close.
14:58:32 <tswett[m]> Way back when, I wanted to create a "linear Haskell" programming language.
14:58:47 <tswett[m]> I remember I really liked whatever name I came up for it, but I don't remember what that name was.
15:03:38 <tswett[m]> I think the name was mostly arbitrary. It was chosen for how it has a lot of the sounds from "Haskell" and "linear".
15:03:58 -!- user24 has joined.
15:04:18 <tswett[m]> It comes from the word "Hydralisk" from StarCraft, with the middle syllable dropped.
15:06:51 <tswett[m]> I had the idea to give it a rather fun "disjointed lambda" syntax, where you could write definitions such as this one:
15:06:56 <int-e> mmm straight line haskell
15:07:53 <int-e> . o O ( I even hava a slogan for it: "Don't declare. Just do!" )
15:08:18 <tswett[m]> dual :: ((a -> Bottom) -> Bottom) -> a
15:08:46 <tswett[m]> So in context, f :: (a -> Bottom) -> Bottom; \x :: a -> Bottom; and x :: a.
15:09:20 <tswett[m]> The -> operator sees an expression of type Bottom on the left, and a on the right, and forms an expression of type a.
15:15:06 <tswett[m]> It expresses the following rule: given "X, (a -o Bot) |- Bot" and "Y, a |- b", form "X, Y |- b".
16:17:08 -!- shotover has joined.
16:21:48 -!- shotover has quit (Client Quit).
16:22:24 -!- shotover has joined.
16:25:20 -!- moei has joined.
17:18:00 -!- user24 has quit (Quit: Leaving).
17:19:08 -!- budonyc has quit (Ping timeout: 272 seconds).
17:29:15 * kmc waves to tswett[m]
17:30:45 <kmc> how's life?
17:43:46 -!- Phantom_Hoover has joined.
18:29:14 <HackEso> 537) <Phantom_Hoover> OMG <Phantom_Hoover> What if <Phantom_Hoover> we shoot Hitler with neutrinos \ 1080) <fungot> boily: so i guess a really savvy glass programmer could make some money, maybe start a home based business of a profiler to spot outright dead code. macro-generated code often has big swaths of it. i'd hate learning cobol and fortran just for getting wiki work.
18:29:57 <fungot> Available: agora* alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp ukparl youtube
18:30:04 <fungot> Selected style: irc (IRC logs of freenode/#esoteric, freenode/#scheme and ircnet/#douglasadams)
18:30:14 <fungot> int-e: just copy-pasted from http://en.wikipedia.org/ wiki/ irp
18:47:17 <lambdabot> LOWI 121820Z VRB04KT 9999 -RA FEW015 BKN050 OVC090 15/13 Q1015 TEMPO SHRA
18:48:00 <lambdabot> LOWW 121820Z 28008KT 9999 FEW030CB SCT060 BKN300 21/12 Q1011 NOSIG
18:48:41 <lambdabot> EDDT 121820Z VRB02KT 9999 FEW025CB 20/14 Q1009 NOSIG
19:15:25 -!- FreeFull has joined.
19:32:59 <Phantom_Hoover> i like 537 because it's now an obscure reference to a very brief period in popular science
19:35:42 <esowiki> [[Esolang:General disclaimer]] https://esolangs.org/w/index.php?diff=64244&oldid=59371 * Areallycoolusername * (+122) Import Compensation Notice
19:36:15 <esowiki> [[Esolang:General disclaimer]] https://esolangs.org/w/index.php?diff=64245&oldid=64244 * Areallycoolusername * (+1)
19:52:13 <shachaf> Taneb: I don't understand your adjunction. Where do the functors map the arrows?
19:52:41 <shachaf> For example don't you need a function from {{}} to {}?
20:40:51 -!- atslash has quit (Quit: This computer has gone to sleep).
21:01:06 <arseniiv_> <tswett[m]> There's a "ball game" semantics for linear logic => the following was interesting!
21:06:30 -!- arseniiv_ has changed nick to arseniiv.
21:26:44 -!- AnotherTest has quit (Ping timeout: 252 seconds).
21:38:10 <zzo38> Finally, now I implemented the ability to post articles with bystand.
21:50:53 <zzo38> (It still isn't complete, though. Many additional stuff might be added/changed.)
21:56:55 -!- arseniiv has quit (Ping timeout: 246 seconds).
22:25:02 -!- budonyc has joined.
23:03:59 -!- lambdabot has quit (Quit: When will I be back? Only time will tell!).
23:05:45 -!- tromp_ has joined.
23:08:34 -!- tromp has quit (Ping timeout: 276 seconds).
23:19:09 -!- lambdabot has joined.
23:43:46 <esowiki> [[Category:Works-in-Progress]] M https://esolangs.org/w/index.php?diff=64246&oldid=63964 * Salpynx * (-31) Undo revision 63964 by [[Special:Contributions/A|A]] ([[User talk:A|talk]]) redundant category theory joke
23:51:01 -!- Phantom_Hoover has quit (Ping timeout: 246 seconds).
23:53:05 -!- zzo38 has quit (Ping timeout: 248 seconds).
23:53:51 <int-e> shachaf: Well there's a Theseus problem... it's all newly compiled code now!
23:54:10 -!- zzo38 has joined.
23:56:44 <int-e> I don't know how to answer that. (But I do see the pun.)