00:05:55 -!- arseniiv has quit (Quit: gone completely :o).
00:31:33 -!- sprocklem has joined.
01:30:40 -!- xkapastel has quit (Quit: Connection closed for inactivity).
01:46:42 -!- FreeFull has quit.
01:52:25 -!- oerjan has joined.
03:16:25 -!- Frater_EST has quit (Remote host closed the connection).
03:22:06 -!- imode has joined.
06:16:37 -!- kritixilithos has joined.
06:17:51 <oerjan> surprisingly, it looks like int-e may be wrong about the foglios. although probably just temporarily.
06:20:13 <oerjan> also i find that diagram strangely parallel to schlock mercenary a few days ago
06:21:50 <oerjan> well if it's a diagram. it could be just background decoration suspiciously looking like that.
06:21:55 <oerjan> maybe it's a shout-out
06:24:20 <oerjan> hm i don't think it's decoration because it's absent in the neighboring panels
06:25:45 <oerjan> (https://www.schlockmercenary.com/2020-02-22)
06:26:08 <oerjan> * <https://www.schlockmercenary.com/2020-02-22>
06:36:17 -!- sftp has quit (Excess Flood).
06:39:17 -!- sftp has joined.
06:39:43 -!- kritixilithos has quit (Ping timeout: 240 seconds).
06:50:54 -!- kritixilithos has joined.
07:39:25 -!- Lord_of_Life has quit (Ping timeout: 255 seconds).
07:40:25 -!- Lord_of_Life has joined.
07:41:14 -!- imode has quit (Ping timeout: 240 seconds).
08:10:21 -!- rain1 has joined.
08:26:50 -!- erdic has quit (Ping timeout: 240 seconds).
08:27:16 -!- rain1 has quit (Quit: Lost terminal).
08:28:14 -!- erdic has joined.
08:39:51 -!- kritixil1 has joined.
08:41:43 -!- kritixilithos has quit (Ping timeout: 240 seconds).
08:47:23 -!- xelxebar has quit (Ping timeout: 240 seconds).
08:55:58 -!- b_jonas has quit (Quit: leaving).
09:17:20 -!- cpressey has joined.
09:48:22 <cpressey> Good morning. My researches into ABTs have revealed a bewildering array of attempts to "solve the alpha-equivalence problem" in a nice way".
09:49:21 <cpressey> Especially when I got more into the Coq related literature, which makes sense, since a lot of people using Coq are using it to prove things about languages. So they want it to be able to reason about named things more easily.
09:49:29 <oerjan> what about attempts to prove it unsolvable wth
09:50:33 <oerjan> hm unfortunate acronym
09:50:44 <HackEso> dth is the dth ordinal. dth?
09:51:06 <cpressey> Yeah well, it's probably a bit hard to publish a result that consists of "Argh, I give up", isn't it?
09:51:56 <oerjan> no, what you do is "Argh, I've proved _no one_ can do it" hth
09:53:35 <oerjan> although that reminds me a bit of those P vs. NP obstacles scott aaronson has sometimes written about
10:02:44 <cpressey> https://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/
10:11:09 -!- oerjan has quit (Quit: Nite).
10:14:53 <cpressey> http://blog.discus-lang.org/2011/08/how-i-learned-to-stop-worrying-and-love.html
10:24:04 -!- imode has joined.
10:27:17 * cpressey starts just randomly welding random pieces of metal together randomly
11:02:02 -!- imode has quit (Ping timeout: 240 seconds).
11:08:23 -!- kritixil1 has quit (Ping timeout: 240 seconds).
11:23:26 <int-e> cpressey: make sure to keep an escape route for yourself
11:24:46 -!- arseniiv has joined.
11:38:52 -!- erdic has quit (Ping timeout: 258 seconds).
11:39:14 -!- erdic has joined.
11:40:13 -!- wib_jonas has joined.
12:14:27 <int-e> @tell oerjan I may have been wrong about the Foglios but I was definitely right about Clippy.
12:16:05 <int-e> arseniiv: 15 digits now (I left the program running over night, but it's stopped now so this will be the last update) ;-)
12:19:34 <arseniiv> int-e: I hoped you’d get to 20! (not a factorial)
12:19:38 <int-e> . o O ( I wonder how much could be accomplished in 200,000 years of computation though.)
12:20:25 <int-e> arseniiv: I won't say impossible, but I have no clue how to get there.
12:20:36 <int-e> Other than extreme luck, perhaps.
12:21:55 -!- kritixil1 has joined.
12:23:05 <kritixil1> arseniiv: did you find a proof of the segment length problem?
12:24:00 <esowiki> [[Int**]] N https://esolangs.org/w/index.php?oldid=70064 * Hakerh400 * (+7868) +[[int**]]
12:24:03 <int-e> (200,000 years because the last few dates on the current list of solvers are all in February 202020)
12:24:15 <esowiki> [[User:Hakerh400]] https://esolangs.org/w/index.php?diff=70065&oldid=70036 * Hakerh400 * (+12) +[[int**]]
12:24:58 <esowiki> [[Language list]] https://esolangs.org/w/index.php?diff=70066&oldid=70037 * Hakerh400 * (+12) +[[int**]]
12:27:19 <int-e> Hmm, cute. But the "uncountable ordinals" reference feels off.
12:27:35 <int-e> (Looking at the int** thing.)
12:29:10 <int-e> Actually I'm sure this is ill-defined; one should be able to encode Russell's paradox in this.
12:29:34 <int-e> Unless it forbids recursion, hmm.
12:34:56 <arseniiv> if they wouldn’t mention pointer types as an analogy, which isn’t a good one anyway. they wouldn’t need to say several times that changing an int* value doesn’t change anything other
12:36:12 <int-e> Well, a lot of paradoxes anyway, maybe not Russell's in particular.
12:37:04 <cpressey> From one of the examples it looks like int* is the same as int(int) so what is this actually
12:40:08 <cpressey> C already has mappings from ints to ints, they're called functions
12:40:36 <arseniiv> yeah in Haskell terms it allows Bool and data NatF (n :: Nat) where { NatZ :: Nat -> NatF 0; NatS :: (NatF n -> NatF n) -> NatF (n + 1) }, only all the values are strict
12:41:55 <arseniiv> I’d also think that modern C++ frowns upon indexing pointers but IDK
12:42:46 <esowiki> [[Talk:Int**]] N https://esolangs.org/w/index.php?oldid=70067 * Int-e * (+257) question about consistency
12:47:32 <cpressey> I expect they don't consider the inconsistency an actual problem, they probably categorize it under "the interpreter may never halt if it is unable to prove that two values are equivalent."
12:48:44 <int-e> arseniiv: Well what int** adds is an oracle... I suspect for the whole arithmetic hierarchy, but I have not thought it through completely, just handwaved that each level of contravariance should give you an alternation in quantifiers.
12:49:19 <int-e> And, of course, inconsistency.
13:08:47 <cpressey> int-e: So Coq also has an "auto" tactic. I did my first proof in Coq, I got halfway, I wasn't sure how to finish it, so I tried "auto" and it worked. I'm still not sure what it did.
13:10:16 <int-e> I think it mostly uses existing introduction rules to solve goals recursively?
13:11:36 <int-e> There's some setup for this, where lemmas can be registered for use with auto... I forgot what it is. There is a #coq (or ##coq? should be the former...) btw.
13:12:12 <cpressey> The proof I was doing was a very simple one so I'm not surprised it worked, it's more of a comment on the opacity of working with tactics.
13:12:45 <int-e> oh yeah, but soon you'll be happy it worked and move on ;)
13:13:43 <int-e> But that said, at the beginning it may actually be worthwhile to attempt a more detailed proof without automatic tactics.
13:14:39 <int-e> Often the real problem is to find the applicable lemmas. And you'll need to do that yourself when the automatic methods fail (and they often do...).
13:16:57 <int-e> I forgot, but I have some notes here... http://paste.debian.net/1132703/
13:17:15 <int-e> (basic ideas for exploration)
13:30:49 <fungot> int-e: i always use. " you'll need this to tell your boss and coworkers and all your goddamn family which is made of!
13:37:24 <int-e> fungot: stop being coherent
13:37:24 <fungot> int-e: fnord of data? or only boolean?, and i don't
13:48:24 <esowiki> [[Talk:Int**]] https://esolangs.org/w/index.php?diff=70068&oldid=70067 * Hakerh400 * (+791) /* Consistency */
13:55:33 <cpressey> It's not a paradox, it's simply an infinite loop, see?
13:56:21 <int-e> I'm more irritated by the absence of global variables in conjunction with the example at https://esolangs.org/wiki/Int**#Functions
13:57:00 <int-e> But if there's nontermination then equality becomes more interesting.
13:57:27 <wib_jonas> so the whole "uncountable ordinal" thing is a red herring because they're all countable ordinals?
13:58:12 <int-e> Nah, there are no ordinals at all.
13:58:41 <cpressey> I'm guessing sure they meant "levels of the arithmetic hierarchy" where they said "ordinals"
13:58:53 <cpressey> That's right, I'm guessing sure.
13:59:05 <cpressey> Not going to attempt to correct that.
14:00:32 <int-e> They could simply mean cardinals.
14:02:00 <cpressey> "cardinal" would also make more sense than "ordinal"
14:02:04 <int-e> which makes a bit of sense; testing equality of two (int -> int) -> int -> int functions naively means testing all uncountably many (int -> int) functions.
14:04:01 <int-e> ("naively" -- I would expect that there is a countable test set that always works)
14:04:48 <int-e> On a meta level, at least. In fact... start with a countable model of ZFC ;)
14:09:34 -!- sprocklem has quit (Ping timeout: 255 seconds).
14:09:40 <wib_jonas> int-e: you can't find one of those models without being able to decide the truth of any unparametrized first order logic statement about natural numbers though
14:11:44 <wib_jonas> it's no surprise, there's no easy cheat to collapse the arithmetical hierarchy
14:19:07 <esowiki> [[Talk:Int**]] https://esolangs.org/w/index.php?diff=70069&oldid=70068 * Int-e * (+603) /* Consistency */ more questions
14:25:29 <esowiki> [[Talk:Int**]] https://esolangs.org/w/index.php?diff=70070&oldid=70069 * Int-e * (+411) /* Consistency */
14:26:18 <int-e> wib_jonas: Oh sure, I didn't mean to suggest that any of this can actually be done in "practice".
14:26:37 -!- wib_jonas80 has joined.
14:27:11 <int-e> . o O ( what happened to 0 to 79? )
14:27:33 <kritixil1> fungot: which one's the real wib_jonas
14:27:33 <fungot> kritixil1: it might be
14:28:10 <wib_jonas80> I disconnected my laptop from the company network to diagnose a network problem
14:28:30 <wib_jonas80> then reconnected, but didn't bother to disconnect from irc first, so the other nick is still connected
14:28:48 -!- wib_jonas has quit (Disconnected by services).
14:28:57 -!- wib_jonas80 has changed nick to wib_jonas.
14:29:46 <wib_jonas> kritixil1: are you the real kritixilithos?
14:30:23 <int-e> . o O ( dear pixel cloud on my screen, define "real" )
14:30:35 <wib_jonas> int-e: I don't know how the wob client chooses fallback nicknames, but I think this is more sensible than the underscore escalation method
14:31:22 <kritixil1> fungot: what do you think, am i the real one?
14:31:22 <fungot> kritixil1: no one comments on my perl style welcome :)), so i can crash due to my fnord alist or is something not going to waste any more of those undeclared identifiers now:
14:31:45 -!- kritixil1 has changed nick to kritixilithos.
14:49:25 -!- rain1 has joined.
15:01:54 -!- sprocklem has joined.
15:19:23 -!- kritixilithos has quit (Ping timeout: 240 seconds).
15:47:18 <esowiki> [[Int**]] https://esolangs.org/w/index.php?diff=70071&oldid=70064 * Hakerh400 * (+93)
15:50:24 <esowiki> [[Talk:Int**]] https://esolangs.org/w/index.php?diff=70072&oldid=70070 * Hakerh400 * (+85)
15:53:55 -!- sprocklem has quit (Ping timeout: 260 seconds).
15:56:37 -!- rain1 has quit (Quit: leaving).
15:56:53 <wib_jonas> for some reason, listening to a performance of a classical musical opera where the libretto is originally in italian language but is sang in german sounds weird and wrong to me, much more so than when such an opera is sang in Hungarian
15:58:16 <wib_jonas> I mean, there's a reason why some operas are in italian, others are in german (and a few are in french), so when it's sang in german, that seems like it's sang in the wrong language, whereas if it's in hungarian, it's obviously just a translation, because the original can't be in hungarian
16:05:18 -!- sprocklem has joined.
16:13:36 -!- kritixilithos has joined.
16:23:46 -!- wib_jonas has quit (Remote host closed the connection).
16:47:55 <esowiki> [[I like frog]] https://esolangs.org/w/index.php?diff=70073&oldid=70051 * Apollyon094 * (+0)
16:49:01 <esowiki> [[I like frog]] https://esolangs.org/w/index.php?diff=70074&oldid=70073 * Apollyon094 * (+1)
16:50:13 -!- sprocklem has quit (Ping timeout: 255 seconds).
17:01:03 -!- cpressey has quit (Quit: A la prochaine.).
17:01:55 -!- LKoen has joined.
17:13:00 <esowiki> [[Talk:Int**]] https://esolangs.org/w/index.php?diff=70075&oldid=70072 * Hakerh400 * (+92)
17:19:17 -!- LKoen has quit (Remote host closed the connection).
17:25:59 -!- LKoen has joined.
17:40:22 -!- joast has quit (Quit: Leaving.).
18:49:47 <int-e> "Let's say that behavior in any disputable situation is implementation-dependent."
18:49:59 <int-e> Okay, that means we have a moving target for all interesting questions... moving on.
18:53:37 -!- joast has joined.
19:01:47 -!- FreeFull has joined.
19:24:59 -!- b_jonas has joined.
19:30:49 <b_jonas> int-e: are you reading old C code that doesn't know about <inttypes.h> or <stdint.h> and breaks if long isn't exactly 32 bit wide?
19:31:13 <b_jonas> or the opposite, breaks if long isn't the size of a pointer
19:32:13 <b_jonas> sometimes you can find fixed versions of the source code that replace long with hopefully the correct type
19:34:17 <b_jonas> now we have <inttypes.h> and <stdint.h> that partly solves this problem, as in, we now have a way to refer to an integer type that should be exactly 32 bit wide (int32_t, uint32_t), or the size of a pointer, etc,
19:35:18 <b_jonas> but there are still some problems, eg. there's an lrint/lfloor/lceil which return long, and an llrint/llfloor/llceil function which returns long long, but now how do I convert a floating point number to a 32-bit integer?
19:37:35 -!- Lord_of_Life_ has joined.
19:40:13 <int-e> b_jonas: No, I was engaging on the esowiki talk page for int**
19:40:43 -!- Lord_of_Life has quit (Ping timeout: 260 seconds).
19:40:46 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
19:41:10 <int-e> And Hakerh400's latest answer made me lose all my interest.
19:50:09 -!- kritixilithos has quit (Quit: quit).
20:13:38 -!- fredkerdraon has joined.
20:24:31 -!- fredkerdraon has quit (Remote host closed the connection).
20:27:32 -!- sprocklem has joined.
22:02:39 <zzo38> I read somewhere apparently they said that German language is too brutal for opera, and Italian is better. I don't know so much about opera, but, nevertheless I think they can try and then they can see if it is better or not. Different people might have a different opinion, too, I think.
22:18:30 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
22:34:59 <spruit11> zzo38: Weird? There's a _lot_ of German opera.
22:35:46 <spruit11> https://en.wikipedia.org/wiki/The_Magic_Flute <- Mozart, pretty well known.
22:37:58 <spruit11> You probably ran into a rivalry because Italian and German operas are the most well known. Then French, then English, both far behind.
22:43:12 <b_jonas> spruit11: yes, and that's why it sounds weird when an Italian opera is sang in German.
22:45:58 -!- imode has joined.
22:47:26 <zzo38> Well, I just mention what I read. Maybe that is what they meant; I don't know. What I know is that I don't know so much about opera, so I do not have any of my own opinions about it which is any good.
22:56:05 -!- imode has quit (Ping timeout: 240 seconds).