00:10:51 -!- Xylochoron has quit (Ping timeout: 256 seconds).
00:31:21 -!- joast has quit (Quit: Leaving.).
00:52:55 -!- Sgeo__ has joined.
00:55:52 -!- Sgeo_ has quit (Ping timeout: 246 seconds).
00:59:45 -!- MatrixBridge has joined.
00:59:48 -!- MatrixBridge has left ("User left").
01:01:29 -!- Xylochoron has joined.
01:03:22 <HackEso> Xylochoron: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: <https://esolangs.org/>. (For the other kind of esoterica, try #esoteric on EFnet or DALnet.)
01:03:48 <fungot> shachaf: shortly after the war, the strength of the interests of your hearers, there to shine forever, while the world lasts, a warning to protect their own buildings ( which were without any fnord or fnord anything. will you let in a mussulman? will you hazard so desperate a step while there is any mistake about it," said clodius.
01:05:07 <Xylochoron> hey, i'm a regular on the esolangs Discord server. working on a thing to compile turing machines into cyclic tag these days....
01:05:13 <Xylochoron> i gather you guys are not big fans of discord.
01:06:20 * kmc definitely isn't
01:06:42 <Xylochoron> uhm, anyway, i know i'm just like, showing up in ur server all of a sudden, but, well, some of us discorders are like, not so happy about discord ourselves, and there's this open source thing like discord called Matrix,
01:06:49 <Xylochoron> so i'm 4 sure not asking you guys to join that or anything
01:07:13 <Xylochoron> i know someone asked about that for discord before and i heard u guys said no, but maybe matrix would be ok?
01:07:39 <shachaf> Don't people already use Matrix with IRC?
01:07:42 <Xylochoron> just though i'd ask, there's a lot of us who are curious to know what you guys are all talking about but are kinda stuck on some of the features of discord :-/ riot has pretty much the same features and is open source and stuff so,
01:07:54 <Xylochoron> ok sorry i'm actually just new to matrix today X-D
01:08:00 <shachaf> Looks like tswett[m] here is doing that.
01:08:05 <Xylochoron> so i might not be completely understanding how it works haha
01:08:31 <Xylochoron> i made my own esolang room there, but if there's a way to just connect with you guys more directly that'd be great to
01:08:35 <shachaf> Anyway I'm not the person to ask about these things but I usually don't like these bridges.
01:09:12 <tswett[m]> Xylochoron: There already is a bridge. I'm using it right now.
01:09:19 <Xylochoron> ok, i gotcha. let me actually just look into if there's a more direct way to
01:09:32 <shachaf> IRC has plenty of problems but at least it's relatively simple and a protocol you can make your own clients for.
01:10:25 <Xylochoron> simple isn't necesarily a huge benefit for me but like, i'm sure it is for others, to each their own i dunno?
01:10:36 <Xylochoron> how do i get on your side of the bridge tswett[m]
01:11:12 <tswett[m]> I think you just join #freenode_#esoteric:matrix.org.
01:11:21 <Xylochoron> would love to know what u guys have been talking about. have some good friends on discord too though i hope i can convince evryone to merge or something.......
01:11:39 -!- Xylochoron has quit (Quit: Page closed).
01:12:14 -!- Xylochoron has joined.
01:13:46 <shachaf> did you know that the Matrix standard specifies RESTful HTTP APIs for securely transmitting and replicating JSON data between Matrix-capable clients
01:14:05 <shachaf> are all things that describe themselves as RESTful bad
01:14:08 <tswett[m]> I also use Discord, by the way, so I'd be interested in knowing about the esolang Discord. :D
01:16:23 <Xylochoron> lol i guess i can tell you about the esolang discord, but really over there we've been talking about switching to matrix
01:16:39 <Xylochoron> so it'd be a little weird to have some people moving that way and others this way lol
01:17:32 <Xylochoron> sorry could you tell me that address to add on matrix again
01:18:54 <Xylochoron> sorry for being dumb but i'm actually having some trouble figuring out how to join from matrix
01:19:00 <Xylochoron> where do i plug in "#freenode_#esoteric:matrix.org" :-/
01:19:36 <Xylochoron> i'm trying to "create a new room" and typing that address into the search bar
01:19:53 <Xylochoron> nothing comes up, searching for esoteric doesn't come up with anything either
01:20:38 <Xylochoron> i'm using the desktop riot client thing,
01:20:42 <tswett[m]> Click on the join-a-room button, type in #freenode_#esoteric:matrix.org, and hit enter.
01:20:55 <tswett[m]> You won't see any search results, but that doesn't matter.
01:21:22 -!- xylochoron[m] has joined.
01:21:55 <xylochoron[m]> ok right wow, all i had to do was hit "join" and not worry about it being in the search results duh
01:22:58 <xylochoron[m]> this should be cool, i'm always worried that on discord we're talking about stuff you guys have already figured out the answer to over here haha
01:23:54 <tswett[m]> Like how to write a loop in ///. :D
01:24:18 <tswett[m]> Holy cow, I invented /// half my life ago.
01:26:26 <xylochoron[m]> i'm so sad i didn't get into programming when i was younger than i did, but i hope i'm making up for it in time. i'm 35 and only really started coding around 22 or so D-:
01:26:40 <xylochoron[m]> i guess i messed around with calculator basic in middle school a little bit lol
01:26:44 <kmc> yeah you don't have to start early to be great at it
01:26:54 <xylochoron[m]> but its pretty cool to hear about people making that kind of stuff at like 13
01:27:21 <xylochoron[m]> i'm like, the oldest person by far on the discord server haha
01:33:01 -!- Xylochoron has quit (Quit: Page closed).
01:36:53 -!- budonyc has joined.
01:43:24 -!- tswett[m] has quit (Changing host).
01:43:24 -!- tswett[m] has joined.
01:43:24 -!- tswett[m] has quit (Changing host).
01:43:24 -!- tswett[m] has joined.
01:47:30 -!- budonyc has quit (Quit: Leaving).
02:46:34 -!- joast has joined.
02:48:27 -!- adu has joined.
03:20:10 -!- FreeFull has quit.
03:52:52 -!- esowiki has joined.
03:54:33 -!- esowiki_ has joined.
03:55:43 -!- esowiki_ has left.
03:57:02 <esowiki> 03:27 User talk:Groowy (diff | hist) . . (+760) . . Ais523 (talk | contribs) (Creative Commons licenses make it legal to do certain things with the work, but there are restrictions; Esolang doesn't meet those restrictions, so you can't post Creative Commons work (other than the unrestricted CC0) here)
04:01:15 -!- esowiki has quit (Quit: Page closed).
04:02:13 -!- esowiki has joined.
04:24:36 -!- a_ has joined.
04:24:46 <HackEso> A is one of seven villages in Norway. The BBC invented them by not understanding things on top of letters.
04:25:25 <HackEso> A is one of seven villages in Norway. The BBC invented them by not understanding things on top of letters.
04:25:43 <HackEso> Do you know adu? Adu adu adu adu adu!
04:26:06 <adu> what's happening
04:26:23 -!- a_ has left.
04:26:32 -!- esowiki has quit (Quit: Page closed).
04:27:19 <shachaf> a_ is pretending to be the esowiki bot now.
04:28:15 <HackEso> Å _is_ a village in Norway, unless you're the BBC and don't understand things on top of letters.
04:28:29 <HackEso> a:A is one of seven villages in Norway. The BBC invented them by not understanding things on top of letters. \ å:Å _is_ a village in Norway, unless you're the BBC and don't understand things on top of letters. \ cocoa:A is a village in Norway. The BBC invented it by not understanding things on top of letters.
04:38:22 -!- a_ has joined.
04:38:53 <HackEso> b_jonas egy nagyon titokzatos személy. Hollétéről egyelőre nem ismertek.
04:39:17 <shachaf> a_: You are being obnoxious and repeatedly engaging in behaviors that people have asked you to stop.
04:39:40 -!- a_ has quit (Client Quit).
04:57:14 <adu> shachaf: thanks
05:04:02 -!- Zsdf has joined.
05:04:08 <HackEso> Queen Shachaf of the Dawn sprø som selleri and cosplays Nepeta Leijon on weekends. He hates bell peppers with a passion. He doesn't know when to stop asking questions. We don't like this.
05:04:18 -!- Zsdf has quit (Client Quit).
05:09:04 -!- Zsdf has joined.
05:09:07 <Zsdf> a_: You are being obnoxious and repeatedly engaging in behaviors that people have asked you to stop.
05:09:12 -!- Zsdf has left.
05:14:46 <shachaf> what is the deal with this person's random harassment
05:16:22 -!- Sgeo_ has joined.
05:19:27 -!- Sgeo__ has quit (Ping timeout: 244 seconds).
05:29:29 -!- Frater_EST has joined.
05:31:14 -!- Frater_EST has left.
06:02:00 <ski> shachaf,int-e : hm, i've pondered that median thing, before
06:04:43 <ski> orin : "`x' is at most `y'" is written `x =< y'
06:05:08 <ski> the `(a \/ b) /\ (a \/ c) /\ (b \/ c) = ... = (a /\ b) \/ (a /\ c) \/ (b /\ c)' one
06:10:47 <ski> i was pondering "matching" on bags
06:30:29 -!- AnotherTest has joined.
06:30:32 -!- adu has quit (Quit: adu).
07:06:08 -!- tromp has quit (Read error: Connection reset by peer).
07:06:20 -!- tromp has joined.
07:36:59 <b_jonas> tswett[m]: in that case look at the other string-rewriting esolanguages at http://esolangs.org/wiki/Category:String-rewriting_paradigm
07:37:39 <b_jonas> tswett[m]: 13 years ago, that was around 2006, right? http://esolangs.org/wiki/Fuun_DNA is from 2007
07:38:24 <b_jonas> xylochoron[m]: basic of what calculator specifically? it's hard to guess because I don't know when you were in middle school
07:39:40 <b_jonas> nah, if you were that old, you wouldn't have had a calculator with basic in middle school
08:03:00 <b_jonas> wow, thunderstorm warning for today, sunday and monday
08:05:53 -!- GeekDude has quit (Ping timeout: 245 seconds).
08:21:30 -!- b_jonas has quit (Quit: leaving).
08:41:57 -!- Sgeo_ has quit (Read error: Connection reset by peer).
08:42:21 -!- Sgeo_ has joined.
08:54:57 -!- Sgeo__ has joined.
08:57:58 -!- Sgeo_ has quit (Ping timeout: 245 seconds).
09:13:42 -!- wob_jonas has joined.
09:33:27 -!- GeekDude has joined.
10:00:17 -!- tromp has quit (Remote host closed the connection).
10:07:51 -!- tromp has joined.
10:10:54 -!- Sgeo_ has joined.
10:13:57 -!- Sgeo__ has quit (Ping timeout: 244 seconds).
10:17:03 -!- Lord_of_Life has quit (Ping timeout: 244 seconds).
10:18:12 -!- Lord_of_Life has joined.
10:58:16 -!- tromp has quit (Remote host closed the connection).
11:09:32 -!- tromp has joined.
11:19:47 -!- Camto[m] has joined.
11:40:18 -!- S_Gautam has joined.
11:52:05 -!- sebbu3 has joined.
11:53:02 <wob_jonas> oh nice, I hadn't seen this one before. website registration form, with javascript that checks whether the password you want to set satisfies their password complexity criterion. it lists each condition in a separate line, and checks immediately during typing the password, so when you type the first capital letter, it marks "At least 1 capitalized
11:53:55 <wob_jonas> and yeah, "Avoid using '," , & ,< , >,/ special character" because they apparently aren't sure they can write working javascript or sql placeholders or something
11:54:19 <wob_jonas> let me try to remove that javascript and register with a password that fails some of those criterions
11:55:21 -!- arseniiv has joined.
11:56:04 -!- sebbu has quit (Ping timeout: 258 seconds).
12:22:54 -!- dingwat_ has joined.
12:23:28 -!- j4cbo has quit (Ping timeout: 264 seconds).
12:23:51 -!- j4cbo has joined.
12:24:09 -!- trn has quit (Ping timeout: 244 seconds).
12:24:25 -!- rdococ has quit (Quit: CHEAPIE! What did you do to the bouncer?! :P (jk)).
12:24:27 -!- Lymia has quit (Ping timeout: 248 seconds).
12:25:00 -!- Lymia has joined.
12:25:46 -!- dingwat has quit (Ping timeout: 252 seconds).
12:25:48 -!- dingwat_ has changed nick to dingwat.
12:25:50 -!- tswett[m] has quit (Ping timeout: 252 seconds).
12:25:53 -!- wmww has quit (Ping timeout: 252 seconds).
12:26:56 -!- tswett[m] has joined.
12:28:12 -!- rdococ has joined.
12:28:56 -!- wmww has joined.
12:43:45 -!- trn has joined.
12:56:36 -!- sebbu3 has changed nick to sebbu.
13:11:16 <int-e> ski: fun fact: (a \/ b) /\ (a \/ c) /\ (b \/ c) = (a /\ b) \/ (a /\ c) \/ (b /\ c) implies distributivity (assuming a lattice). Fairly difficult...
13:26:24 <myname> that sounds interesting
13:27:00 <int-e> I don't know why. I've just proved it ;-)
13:27:54 <int-e> the shape vaguely resembles distributivity in that it swaps inner and outer \/ and /\.
13:28:34 <int-e> But beyond that I have little intuition.
13:29:31 <myname> how did you prove that
13:42:30 <arseniiv> int-e: neat! And you don’t need bounds or negation, only lattice axioms?
13:43:33 <int-e> It's funny because my paper proof is incorrect... but I convinced Isabelle ;-)
13:46:45 <wob_jonas> int-e: did you give any hints to Isabelle, or did it just derive the result automatically?
13:47:07 <arseniiv> let’s see… if c ↦ b, that median thing implies (a ∨ b) ∧ b = (a ∧ b) ∨ b. Hm, that’s in axioms already, wrong turn
13:47:13 <int-e> I proved an intermediate lemma.
13:48:34 <int-e> but then I used sledgehammer so there's a proof step I don't understand at all :)
13:53:09 <int-e> arseniiv: I think you used distributivity in that thought.
13:53:58 <int-e> (assuming that c |-> b means c = c \/ b)
13:55:42 <int-e> oh, wrong way, that should be b \/ c = b.
13:56:43 <ski> (do you mean, assuming that `c =< b' ?)
13:57:33 <int-e> I would rather not involve the order at all at this point.
13:58:23 <ski> (i don't see what "if c ↦ b" or "assuming that c |-> b" even means)
13:59:00 <int-e> read it as an implication, then rewrite it as \supset ;-)
14:01:27 <arseniiv> int-e: why, I simply substituted b for c and used some associativity and idempotency
14:02:16 <int-e> I read something else, so I gave away a bit of a hint :)
14:02:42 <int-e> but in retrospect reading it as a substitution would've made perfect sense.
14:04:42 <xylochoron[m]> I had a TI-89 graphing calculator with basic on it. They were introduced in 1998, when I was in 7th grade.
14:05:13 <xylochoron[m]> Cost about the same as it does today too, yay for monopoly?
14:07:41 <wob_jonas> ha, you were in middle school when the TI-89 was already available. I don't think you're the oldest
14:08:59 <ski> ⌜↦⌝ is not an implication arrow, to me
14:10:28 <int-e> ski: I read something that I wanted to see.
14:10:56 <xylochoron[m]> ? I’m the oldest amonth those who’ve admitted their ages on the Discord server, which is most. I think the second oldest is like 23. If there’s older people here yeah that’s great
14:10:59 <ski> xylochoron[m] : fwiw, it's not IRC custom to prefix people's nicknames with sigils like `@', when messaging or referring to them. simply mention their nickname, e.g. at the beginning of the message, followed e.g. by a comma or a colon, and the message
14:12:16 <ski> (many IRC clients hilight a message / alert a user, if their nickname is mentioned, first thing in a message. i think not as many do that, in case the nickname is mentioned somewhere else in a message. though i think most also highlight/alert, on private message ?)
14:12:38 <ski> (oh .. and `@' already means something else on IRC (namely that the person in question is an operator on the channel))
14:12:53 <ski> xylochoron[m] : just fyi :)
14:13:50 <xylochoron[m]> Ok thanks :-D I am a little embarrassingly new to this so just let me know thanks :-D
14:13:53 <ski> (perhaps the other old people are ashamed to admit how old they are, on Discord ?)
14:14:45 <ski> (that was partly in jest)
14:17:24 <xylochoron[m]> https://discordapp.com/invite/say2ERQ?utm_source=share&utm_medium=ios_app
14:18:01 <arseniiv> oh I can’t believe I’m within several years of 30. It feels so old :\
14:18:14 <xylochoron[m]> I was actually trying to convince some of those guys to switch to matrix with me but not sure how much success I’m having
14:18:24 <arseniiv> please tell me here are someone over 80
14:19:07 <ski> i've chatted with people on IRC who're at least 70, i think
14:19:23 <xylochoron[m]> Yeah can I please talk to an actual old person lol
14:19:25 <myname> at least some of them behave like it
14:19:26 <wob_jonas> I've chatted people in real life who're at least 70
14:19:59 <arseniiv> hm I’m chatted with my grandmother :o :o
14:20:16 <ski> perhaps you could chat to two people, whose combined age is at least seventy )
14:20:46 <wob_jonas> have my hon. and learned friend fungot chatted with people who're at least 70?
14:20:47 <fungot> wob_jonas: " had the reviewer's object, in whatever hands, whether high or low prices, whether he chooses to call one two, and eight grinders. its body is covered with an obscurity not to be begged. they must at length have a retreat from the malice of his adversary, by fnord cringing to the public peace. if our liberty has enfeebled the executive power, rendering government in all undertakings for the public necessities, and c
14:21:22 -!- rdococ has quit (Changing host).
14:21:22 -!- rdococ has joined.
14:21:31 <arseniiv> ski: hm, combined ages should indeed make things more bearable… I hope!
14:21:54 <xylochoron[m]> My grandparents once were talking about how when you’re 60, 50 is so young, when 70 60 is young, 80 70
14:22:19 <arseniiv> anyway did int-e say that there was a hint? should I presume b ≤ c and try to make something of that?..
14:22:37 <arseniiv> xylochoron[m]: makes sense, too, yeah
14:22:38 <ski> perhaps sum is not the appropriate arithmetical (geometrical ?) operation ?
14:24:03 <arseniiv> as we’ve seen, max is pretty boring, so maybe arithmetic-geometric mean or something
14:24:05 <ski> > logBase 2 (2 ** 30 + 2 ** 40)
14:24:34 <arseniiv> ski: hm I think base 2 is unnatural
14:24:35 <ski> too close to `max', i suppose
14:25:17 <ski> not that much difference
14:25:19 <ski> > logBase 1 (1 ** 30 + 1 ** 40)
14:26:37 <arseniiv> yesterday I learned P(Z) = Q ∪ {∞}, acted on with usual fractional-linear transformations
14:27:10 <ski> > [30 ** log 40,40 ** log 30] -- and this is greater than sum
14:27:13 <lambdabot> [281139.7457691163,281139.74576911645]
14:27:31 <ski> "fractional-linear" ?
14:27:52 <arseniiv> it should be that different because Z has so many non-unit elements
14:29:08 <arseniiv> ski: I mean, x ↦ (ax + b) / (cx + d) where a, b, c, d ∈ Z
14:30:57 <ski> hm, reminds be of Möbius transformations
14:31:23 <arseniiv> yeah, they are precisely these transformations of P(C)
14:31:35 <ski> i wonder whether that's related to "linear relations"
14:31:44 <ski> `P' being powerset ?
14:31:44 <HackEso> /srv/hackeso-code/multibot_cmds/lib/limits: line 5: exec: P': not found
14:32:07 <arseniiv> no, P just stands for projectivization
14:32:33 <arseniiv> though usually I’ve seen it come after something, like in RP^n
14:32:38 <ski> that was confusing me for a bit
14:34:04 * ski is reminded of musical intervals
14:37:43 <wob_jonas> wait, so the "[m]" is something that the bridge of this "matrix" chat appends?
14:38:14 <ski> presumably
14:38:19 <wob_jonas> that explains a lot, because earlier I've seen a different channel with a lot of users with that in the nick
14:38:32 <ski> though i think not all people connected via Matrix has that nickname suffix
14:41:12 <ski> btw `\(x,y) -> x ** logBase b y' is commutative
14:42:57 -!- arseniiv has changed nick to arseniiv[hm].
14:43:22 -!- arseniiv[hm] has changed nick to arseniiv.
14:43:34 <wob_jonas> ski: http://math.ucr.edu/home/baez/diary/february_2019.html#february_16
14:43:57 <ski> Baez has a diary now ?
14:44:04 <myname> my favourite funfact in that regard was how gdc(fib(x), fib(y)) is supposedly fib(gdc(x, y))
14:44:29 <myname> i never proofed it, though
14:45:14 <ski> fwiw, i was mostly thinking of it, in the context of modular arithmetic (so `logBase b' is the "index", the discrete logarithm, wrt the primitive root `b')
14:48:44 <wob_jonas> but there's a more general statement that you could conjecture but that's false: namely that for any second order linear recurrence of the form s_0 = 0; s_1 = 1; s_{k+1} = A*s_{k-2}+B*s_{k-1}; you'd get gcd(s_x,s_y)=s_{gcd(x,y)}
14:48:52 <wob_jonas> and it's interesting to find a counterexample to that
14:49:30 <wob_jonas> myname: prove at first that if k divides n then fib(k) divides fib(n), then the converse of that
14:49:45 <wob_jonas> use the recurrence relation directly
14:50:05 <wob_jonas> and look at the sequence modulo fib(k)
14:51:13 -!- unlimiter has joined.
14:51:54 <wob_jonas> this is typical for such second order linear recurrences,
14:56:12 <wob_jonas> including the important case of s_k = 2**k - 1, which is what you get for A=-2, B=3
14:56:36 <wob_jonas> you might already know that if k divides n, then (2**k - 1) divides (2**n - 1)
15:01:21 -!- unlimiter has quit (Ping timeout: 252 seconds).
15:01:55 <wob_jonas> or maybe it's not true in that case?
15:02:18 <wob_jonas> I think the direction that if k divides n then (2**k - 1) divides (2**n - 1) is true,
15:03:59 -!- unlimiter has joined.
15:05:54 <wob_jonas> I think both are true for that sequence
15:12:07 <arseniiv> wob_jonas: for my part, I consider number theory an obscure discipline of magic
15:19:06 <int-e> yay, https://en.wikipedia.org/wiki/Distributive_lattice#Characteristic_properties
15:19:36 <int-e> (Also my lemma is to show that the lattice is modular.)
15:37:21 -!- moei has joined.
15:40:25 -!- Sgeo__ has joined.
15:44:36 -!- Sgeo_ has quit (Ping timeout: 272 seconds).
15:48:56 <wob_jonas> arseniiv: for my part, I consider lattices an obscure discipline of magic. I'm fine with some special cases of course.
15:49:11 <wob_jonas> arseniiv: but the statement I made isn't too deep in number theory of course
15:49:16 <wob_jonas> some parts of number theory are magic, sure
15:49:36 <wob_jonas> well, that applies to more or less any branch of mathematics
15:49:57 -!- wob_jonas has quit (Remote host closed the connection).
15:50:27 <arseniiv> wob_jonas: mhm of course I’m not too deep in lattices, but I don’t consider them magic, it’s just something partially unknown to me, without strange feelings
15:52:08 <arseniiv> int-e: the second one there looks like it seems practical for some subtyping typechecking/inference algorithms
15:52:45 <int-e> In any case, I still don't have a complete paper proof for this. It's kind of annoying. :)
15:52:55 -!- Sgeo_ has joined.
15:55:59 -!- Sgeo__ has quit (Ping timeout: 252 seconds).
16:10:52 -!- unlimiter has quit (Quit: WeeChat 2.4).
16:22:20 <rain1> are these lattice formulas decidable?
16:24:38 <rain1> > The classical papers Ph. M. Whitman [1941] and [1942] solved the word problem
16:24:40 <rain1> for free lattices: Whitman gave an algorithm for determining if two lattice terms
16:24:41 <lambdabot> Data constructor not in scope: The :: t0 -> t1 -> t2 -> b0 -> cerror: Va...
16:24:42 <rain1> (polynomials) were equal in all lattices.
16:24:57 <rain1> this sounds like a Knuth-Bendix type thing, but for lattices?
16:26:26 -!- unlimiter has joined.
16:27:55 -!- Sgeo__ has joined.
16:28:25 <int-e> Impossible to say without having a closer look.
16:29:24 <int-e> (Knuth&Bendix' approach can fail even for equationaly theories with a decidable word problem)
16:30:10 <int-e> And Wikipedia is wrong on this... sigh.
16:31:07 -!- Sgeo_ has quit (Ping timeout: 244 seconds).
16:33:12 <int-e> (It claims that Knuth-Bendix completion is a semi-decision procedure, but that's only true for ordered completion, aka unfailing completion, which came quite a bit later... due to Bachmair and Dershowitz I guess?)
16:35:56 <int-e> rain1: it's also worth noting that the decidable word problem has little bearing on the question whether a given equation implies another in the theory of lattices; adding the first equation changes the equational theory, after all.
16:57:49 -!- tromp has quit (Remote host closed the connection).
16:58:12 -!- unlimiter has quit (Quit: WeeChat 2.4).
16:58:54 -!- tromp has joined.
17:05:02 -!- Phantom_Hoover has joined.
17:07:04 -!- b_jonas has joined.
17:13:54 -!- Sgeo_ has joined.
17:17:42 -!- Sgeo__ has quit (Ping timeout: 272 seconds).
17:25:59 -!- unlimiter has joined.
17:36:17 -!- unlimiter has quit (Quit: WeeChat 2.4).
17:38:45 -!- tromp has quit (Remote host closed the connection).
17:44:46 -!- tromp has joined.
17:48:55 -!- Sgeo__ has joined.
17:49:17 -!- tromp has quit (Ping timeout: 252 seconds).
17:51:51 -!- Sgeo_ has quit (Ping timeout: 252 seconds).
17:52:45 -!- budonyc has joined.
18:07:36 -!- tromp has joined.
18:13:26 -!- Sgeo_ has joined.
18:16:25 -!- Sgeo__ has quit (Ping timeout: 252 seconds).
18:18:12 -!- ais523 has joined.
18:18:13 -!- ivzem[m] has joined.
18:30:59 -!- budonyc has quit (Ping timeout: 244 seconds).
18:32:18 <b_jonas> xylochoron[m]: if you like the /// esolang, then among the other string-replacement languages https://esolangs.org/wiki/Category:String-rewriting_paradigm , you may want to check out https://esolangs.org/wiki/Fuun_DNA , which is another one where the only way to loop is to copy your source code
18:32:36 <b_jonas> only in that one, it's much easier to copy, because it can match more freely than just literals
18:35:50 -!- callforjudgement has joined.
18:35:55 -!- ais523 has quit (Ping timeout: 268 seconds).
18:37:52 -!- callforjudgement has changed nick to ais523.
18:45:38 -!- tromp has quit (Remote host closed the connection).
18:49:23 -!- Sgeo__ has joined.
18:52:49 -!- Sgeo_ has quit (Ping timeout: 246 seconds).
18:58:41 -!- tromp has joined.
19:01:06 <xylochoron[m]> one thing i like about slashes is that it's TC with only two symbols, but ofc there's esolangs i like that have more than two symbols also :-P
19:03:41 <shachaf> one symbol is all you need hth
19:08:07 <b_jonas> there's another set of such languages, though they also make copying easy:
19:08:58 <b_jonas> https://esolangs.org/wiki/McCulloch%27s_second_machine counts as string-rewriting, right?
19:26:58 -!- FreeFull has joined.
19:37:40 -!- Phantom_Hoover has quit (Ping timeout: 272 seconds).
19:37:43 -!- Phantom__Hoover has joined.
19:53:06 -!- zzo38 has joined.
19:53:14 -!- tromp has quit (Remote host closed the connection).
19:53:56 -!- tromp has joined.
19:55:54 -!- Sgeo_ has joined.
19:58:48 -!- Sgeo__ has quit (Ping timeout: 245 seconds).
20:08:38 -!- atslash has quit (Quit: This computer has gone to sleep).
20:10:40 -!- budonyc has joined.
20:31:27 -!- Soni has joined.
20:31:45 <Soni> has anyone built a brainfuck interpreter that can execute /dev/urandom?
20:34:23 -!- Sgeo__ has joined.
20:38:28 -!- Sgeo_ has quit (Ping timeout: 272 seconds).
20:46:35 <zzo38> Everything inside the outer brackets has to be saved until that loop is finished, and if you find ] before [ then it won't be valid (but you could use ] to separate the program from the input, perhaps)
20:46:42 <lambdabot> shachaf asked 1d 21h 51m 10s ago: Do you like GF2P8AFFINEQB?
20:46:49 <zzo38> shachaf: I don't know
21:00:22 -!- Sgeo_ has joined.
21:03:27 -!- Sgeo__ has quit (Ping timeout: 248 seconds).
21:04:26 -!- ais523 has quit (Quit: sorry for my connection).
21:04:43 -!- ais523 has joined.
21:05:01 <ais523> Soni: I'm not sure; you'd have to make the execution start running the program as it read it
21:05:34 <ais523> that's basically what Easy interpreters do, but they read input and program from the same stream so it isn't the same language as brainfuck (that's why it has a different name)
21:05:53 <ais523> it'd be easy enough to adapt an Easy interpreter to read input and program from different files…
21:07:05 <shachaf> Are there any interesting quines that don't look like the classic quine?
21:07:25 <b_jonas> shachaf: what counts as looking like the classic quine?
21:07:29 <shachaf> I mean that they don't have two copies of almost the same string, one quoted and one not, or something, but use some other mechanism.
21:08:00 <b_jonas> shachaf: in some languages you can have just one copy of most of your code and recover it
21:08:15 <b_jonas> you know, like e = '... code here ...'; eval(e)
21:08:36 <shachaf> Well, using the language's mechanism for it (or reading the input file) seems a bit uninteresting.
21:08:45 <b_jonas> and then there are quines where there are two copies, but the data one is encoded so much that it doesn't look anything like the code
21:08:52 <b_jonas> not just a few backspaces, but completely encrypted
21:09:11 <b_jonas> and of course the code and data can intermix
21:09:55 <shachaf> I suspect the answer to my question is no, this is more or less the only way quines can work.
21:10:17 <b_jonas> and there's all sorts of strange language-dependent stuff like error quines
21:10:49 <ais523> shachaf: there are two common classes of non-degenerate quines which don't have a large repeated section: eval quines and topological quines
21:11:33 -!- ais523 has quit (Quit: sorry for my connection).
21:11:46 -!- ais523 has joined.
21:11:59 <shachaf> What are topological quines?
21:12:23 <ais523> shachaf: they're quines in languages like Befunge which make use of parts of the language world which wrap around
21:12:33 <ais523> so that the "repeated section" only actually appears once in the program
21:13:05 <b_jonas> ais523: oh, so like the seek DATA,0,0 quines in perl?
21:13:13 <b_jonas> which read their own source code
21:13:19 <b_jonas> or do those count as eval quines?
21:13:32 <ais523> that's either a topological quine or just plain cheating, depending on your point of view
21:14:11 <ais523> toplogical quines in Befunge normally start with an unmatched "
21:14:22 <b_jonas> yeah, there are plain cheating ones, such as ones that access a copy of the source code that's outside the source code, such as downloading them from the internet, or reading it from a different file
21:14:32 <ais523> which puts the whole program inside the string (because the playfield wraps around, so the " matches itself), but it's /also/ outside the string so it runs after the entire thing has been placed into a string literal
21:16:03 <ais523> there may be other quine patterns too, but classic/topological/eval are the three main categories I'm aware of
21:16:34 <ais523> there's also double-literal quines but those probably count as cheating, they abuse a bug in codegolf.stackexchange's definition of a quine
21:16:52 <b_jonas> what does double-literal quines mean?
21:17:05 <ais523> they ban literal-only quines, but in languages where programs run right to left and literals just echo themselves, you can write the same literal twice
21:17:24 <ais523> then each of the literals prints the other, rather than each literal printing itself, so it doesn't count as literal-only
21:17:38 <ais523> btw, a literal-only quine is this sort of thing:
21:19:03 <b_jonas> so classic means the quine has some data and some code that prints the data twice, and one of the time it prints it it matches the data, right? and it counts even if the code and data are intermixed, or if the data is encoded in some unrecognizable way?
21:19:59 <b_jonas> what makes it classic is that the code and data parts are mostly disjoint?
21:20:03 <ais523> a classic quine is a program as code, + an encoding of that code as data
21:20:30 <ais523> the encoding might be weird or whatever but it's still just a separate part of the program
21:20:37 <ais523> then from that encoding, you generate both the code and the encoding itself
21:21:33 <ais523> incidentally, I tried to come up with a precise definition of a classic quine, but oerjan came up with a silly counterexample where you have /two/ identical data sections, each of which is used to generate the other (so that data is never used to regenerate itself)
21:22:21 <b_jonas> most of my quines are classic quines then, though I have some eval quines and even cheating quines
21:24:10 <b_jonas> `perl -e print unpack a35X35a34xaXXaaXaXXa,"print unpack a35X35a34xaXXaaXaXXa,\"\\"
21:24:11 <HackEso> print unpack a35X35a34xaXXaaXaXXa,"print unpack a35X35a34xaXXaaXaXXa,\"\\"
21:24:55 <b_jonas> `perl -eprint unpack a43X43a42xaXXaaXaXXa,"`perl -eprint unpack a43X43a42xaXXaaXaXXa,\"\\"
21:24:55 <HackEso> `perl -eprint unpack a43X43a42xaXXaaXaXXa,"`perl -eprint unpack a43X43a42xaXXaaXaXXa,\"\\"
21:26:28 <b_jonas> `perl -eprint+("`perl -eprint+(","\"",",","\\",")[g1012131121212133121414=~/./g]")[g1012131121212133121414=~/./g]
21:26:28 <HackEso> `perl -eprint+("`perl -eprint+(","\"",",","\\",")[g1012131121212133121414=~/./g]")[g1012131121212133121414=~/./g]
21:28:59 -!- AnotherTest has quit (Ping timeout: 248 seconds).
21:40:55 -!- Sgeo__ has joined.
21:43:48 -!- Sgeo_ has quit (Ping timeout: 245 seconds).
21:44:54 -!- Phantom__Hoover has quit (Read error: Connection timed out).
22:03:01 -!- ineiros has quit (Ping timeout: 276 seconds).
22:04:45 <shachaf> b_jonas: I just made up the term "classic quine", I don't know what it's called.
22:05:05 <shachaf> I mean a quine which is generated by Lawvere's theorem or something.
22:05:16 -!- atslash has joined.
22:05:21 <b_jonas> shachaf: well, ais523 also used "classic", so that sounds good
22:08:16 <shachaf> There isn't even a Wikipedia page for Lawvere's theorem.
22:14:00 <shachaf> The Y combinator is also arguably a quine.
22:14:14 <shachaf> At least it's a special case of diagonalization.
22:14:51 -!- b_jonas has quit (Quit: leaving).
22:15:51 -!- unlimiter has joined.
22:16:30 -!- unlimiter has quit (Client Quit).
22:16:36 <ais523> because it doesn't print its own source code, but its own /output/
22:16:47 -!- Phantom_Hoover has joined.
22:17:36 -!- Lord_of_Life has quit (Ping timeout: 248 seconds).
22:19:19 -!- Lord_of_Life has joined.
22:21:08 <shachaf> Lawvere's theorem is: In a CCC, if there's a surjective phi : A -> B^A, then every arrow f : B -> B has a fixed point
22:22:00 <ais523> shachaf: what's the quantifier on A, \exists or \forall?
22:23:47 -!- adu has joined.
22:24:12 <shachaf> I guess I shouldn't say surjective in a CCC.
22:25:13 <ais523> I find CCCs really unintuitive because there are two different vaguely function-like things (categorical arrows, and exponentials)
22:25:42 <ais523> and I find it hard to keep them apart in my head
22:25:43 <shachaf> But you have an evaluation map.
22:26:04 <shachaf> I think the idea is that they're similar enough that you don't need to.
22:27:33 <ais523> oh, there are functors as well, those are also vaguely function-like
22:27:57 <shachaf> And natural transformations!
22:28:13 <ais523> I'm one of the few people who always specifies everything involved in a natural transformation, rather than eliding
22:28:28 <ais523> because a) people get really sloppy when discussing them, and b) I find myself hopelessly confused without doing that
22:28:35 <shachaf> Do you like whiskering notation for natural transformations?
22:28:49 <shachaf> I used to think it was a bad shorthand but after a while I decided it was brilliant.
22:29:13 <ais523> page 49 of my thesis shows the notation that I use
22:29:18 <ais523> I don't know what the whiskering notation is
22:29:21 <shachaf> Whiskering is composing natural transformations and functors, as in Fε or εF
22:30:07 <shachaf> Which means respectively: (Fε)_x = F(ε_x) and (εF)_x = ε_{Fx}
22:30:28 <ais523> that makes sense for /natural/ transformations, doesn't it?
22:30:45 <ais523> it's much the same thing as omitting parens when you have a string of associative operatoins
22:31:25 <HackEso> smlist 501: shachaf monqy elliott mnoqy Cale
22:31:26 <shachaf> I agree that it makes sense.
22:31:39 <ais523> it seems like a disaster on unnatural transformations, but people don't study those much
22:31:46 <shachaf> I'm looking for your thesis now to find page 49.
22:31:57 <shachaf> What are the things people normally elide?
22:32:15 <ais523> the functors, normally
22:32:32 -!- arseniiv_ has joined.
22:32:36 <shachaf> Do you like the definition of a natural transformation as a functor : CxI -> D?
22:32:46 <ais523> also the source category, but I can forgive eliding that
22:32:49 <shachaf> Where I the the category with two objects and three arrows, one between the two objects.
22:33:06 <ais523> that definition seems horrible :-D
22:33:11 <ais523> that doens't necessarily mean I don't like it
22:33:24 <shachaf> Do you like the one-sorted definition of a category?
22:33:28 <Cale> It's nice from the perspective that it looks a whole lot like the traditional definition of a homotopy
22:33:44 <shachaf> That's where you only define the arrows, and leave the objects implicit.
22:33:54 <shachaf> You can also define one-sorted functors and one-sorted natural transformations.
22:34:05 <ais523> presumably an object is somehow identified with its identity arrow?
22:34:41 <Cale> I think the objects are good for the sake of understanding
22:34:46 <shachaf> In this definition, a natural transformation : F -> G : C -> D gives an arrow in D for every arrow in C.
22:34:52 <shachaf> Rather than merely for objects in C.
22:35:11 -!- arseniiv has quit (Ping timeout: 248 seconds).
22:35:18 <shachaf> The identity arrows correpond to the usual components of a natural transformation. The non-identity arrows correspond to diagonals of the naturality square.
22:37:02 <shachaf> Anyway, Lawvere's theorem says that the fixed point of f is, in pseudo-lambda calculus notation: (\x. f(phi(x)(x))) (\x. f(phi(x)(x)))
22:38:11 <shachaf> But you get Cantor's theorem and other diagonalization arguments from this as well.
22:39:04 <shachaf> phi is the isomorphism between B and B^B that you use to talk about the untyped lambda calculus as a CCC.
22:39:36 <shachaf> (You can also define it in Haskell, newtype Rec a = Rec (Rec a -> a), which lets you define Y.)
22:50:48 <shachaf> ais523: I see your notation now. It's very explicit.
22:52:38 -!- Phantom__Hoover has joined.
22:55:16 -!- Phantom_Hoover has quit (Ping timeout: 272 seconds).
23:07:22 -!- Soni has quit (Ping timeout: 252 seconds).
23:07:25 -!- S_Gautam has quit (Quit: Connection closed for inactivity).
23:09:30 -!- budonyc has quit (Quit: Leaving).
23:11:28 -!- ais523 has quit (Quit: sorry for my connection).
23:11:40 -!- ais523 has joined.
23:14:14 -!- arseniiv_ has changed nick to arseniiv.
23:19:58 -!- arseniiv has quit (Ping timeout: 272 seconds).
23:24:25 <zzo38> Do you like my variation of Along and Across? Now there is output (a single number), and you can use numbers as inputs of the along program rather than bits.
23:26:57 <ais523> zzo38: well, Along and Across was designed for a very specific purpose (to attempt to work out if a specific definition of Turing-completeness was reasonable), your version doesn't achieve the same goals I had but might achiieve different goals
23:27:03 -!- Soni has joined.
23:28:05 <ais523> that said, the difference in the along program inputs might not be relevant, although it isn't obvious
23:28:43 <zzo38> It depends what along language is in use
23:29:06 <zzo38> Also, I should think the output doesn't change the Turing-completeness.
23:31:37 <ais523> yes, the output is irrelevant for TCness
23:35:56 <Soni> can you make a program that just does whatever it wants
23:36:15 <ais523> https://esolangs.org/wiki/Baby_Language ?
23:37:54 -!- Sgeo_ has joined.
23:38:01 <shachaf> zzo38: Did you write https://www.realworldtech.com/forum/?threadid=150494&curpostid=169010 ?
23:40:55 -!- Sgeo__ has quit (Ping timeout: 252 seconds).
23:53:39 -!- Phantom___Hoover has joined.
23:55:25 <zzo38> shachaf: I think so.
23:57:20 -!- Phantom__Hoover has quit (Ping timeout: 272 seconds).
23:57:23 <Soni> ais523: not really. more like, glue random things together and see what happens
23:58:14 <Soni> if we ever figure out how life started, that'll probably help us figure out how to bring it to computers
23:58:35 <Soni> but we have no idea how life works
23:58:49 <Soni> we can simulate all the chemistry and physics involved and it's all very expensive
23:59:03 <Soni> but understanding how it actually works is something else entirely