00:01:48 -!- poe_T has joined. 00:04:52 -!- spiette has quit (Ping timeout: 256 seconds). 00:10:34 -!- poe_T has left ("Leaving"). 00:26:50 Ugh 00:27:09 I've got a λ-calculus parser up and running, but I'm not sure how to evaluate, or what evaluation would even look like 00:27:41 -!- p34k has quit. 00:35:34 Find a place where you've got a lambda-function applied to something. 00:35:45 Perform alpha-conversion if necessary, then perform beta-reduction. 00:35:50 Repeat. 00:35:59 If you can't find such a place, you're done evaluating. 00:36:07 'Course, there are several different evaluation orders you can use... 00:36:58 You should use normal order, because all the others are abnormal. 00:43:50 Here's an idea 00:44:00 A language designed to be archaeologically analyzed 00:45:28 It would be designed to have a vast, complex syntax and subtle semantics 00:53:49 And absolutely no documentation. 00:53:52 Or example code. 00:54:30 we call that MUMPS 00:55:11 -!- spiette has joined. 00:55:57 lifthrasiir: The /point/ is that it's just released onto the web one day 00:56:15 Just a (safe, somehow) executable, no source 00:56:16 yeah, I know, but I couldn't resist :) 00:57:38 lifthrasiir: And the people of the world are expected to decrypt the meaning of the language 00:58:44 -!- adu has quit (Quit: adu). 00:58:45 You could find a lot of unintentional examples of that if you s/language/bytecode/ 00:59:27 That is, you could find examples of undocumented bytecode formats being reverse-engineered. I'm thinking of scripting engines in games mainly 01:00:52 FireFly: Sure 01:01:14 (which, by the way, is pretty fun...) 01:01:14 FireFly: What do you think of the idea though? A diggable language? 01:01:37 I dunno, it sounds a bit weird to intentionally design it for that, but I guess it could work 01:01:40 Only problem with me doing this is I'm not good at languages I can compile xD 01:02:01 And it kind of defeats the purpose if you can look at the source 01:02:46 (though it would make things go faster, as you can check for evilness if it's PD) 01:06:55 -!- adu has joined. 01:07:12 -!- adu has quit (Client Quit). 01:20:51 FreeFull: The people on ##programming like the idea :) 01:46:33 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 02:00:40 -!- bender| has joined. 02:04:31 -!- adu has joined. 02:08:08 -!- bb010g has joined. 02:12:26 -!- hppavilion[1] has quit (Ping timeout: 240 seconds). 02:20:11 -!- hppavilion[1] has joined. 02:59:58 [wiki] [[Special:Log/newusers]] create * YoshikuniJujo * New user account 03:10:25 -!- bender| has quit (Ping timeout: 260 seconds). 03:10:57 We're having a sudden growth in new user join rate 03:11:01 I wonder what that's about 03:14:10 [wiki] [[Zot]] https://esolangs.org/w/index.php?diff=46289&oldid=31882 * YoshikuniJujo * (+71) 03:18:38 -!- adu has quit (Quit: adu). 03:19:12 -!- adu has joined. 03:24:11 -!- adu has quit (Ping timeout: 264 seconds). 03:34:58 -!- Treio has quit (Ping timeout: 250 seconds). 03:44:33 hppavilion[1]: topic? 03:44:48 well, imagine a hoard of users that search "trump" from /list 03:45:07 * lifthrasiir realizes it is a nightmare of sort 03:45:49 -!- spiette has quit (Ping timeout: 265 seconds). 03:46:55 lifthrasiir: No, new users on the Wiki 03:52:09 -!- MDude has changed nick to MDream. 03:52:32 -!- hppavilion[1] has quit (Ping timeout: 276 seconds). 04:00:26 -!- hppavilion[1] has joined. 04:28:55 -!- adu has joined. 05:06:21 -!- bender| has joined. 05:25:38 hppavilion[1], similar to Smalltalk? 05:25:50 Oh, no source 05:26:11 Sgeo_: Yeah. No source. 05:26:25 Sgeo_: Until somebody solves some complex problem (perhaps producing full, accurate docs?) 05:26:46 Then they are granted the source, with which they can do as they wish 05:27:17 Sgeo_: It's not a non-FOSS thing, it's a preventing cheating thing 05:27:27 Oh, censorship, not inherent 05:28:04 I need to not have a fever 05:29:05 Sgeo_: Huh? 05:29:09 The first message 05:29:18 night 05:29:23 It wouldn't be fun if you could see the source- oh, night 05:29:53 Was thinking source doesn' 05:29:59 doesn't even exist 05:30:12 Oh xD 05:30:35 Sgeo_: No, the source just isn't provided because otherwise you could look at it and it wouldn't be fun 05:31:55 I'd like to provide the source, but there's no game if I do 05:47:56 -!- hppavilion[1] has quit (Ping timeout: 240 seconds). 06:04:31 -!- hppavilion[1] has joined. 06:09:54 hppavilion[1]! 06:10:08 Hadu! 06:10:19 that's almost my nick 06:11:10 adu: It's also almost "Hi" 06:11:18 (assuming ! is not included as "that") 06:11:20 :) 06:12:25 adu: So I had an idea for a cool project 06:12:36 An Archaeological Programming Language 06:12:40 so if an algorithm is defined in terms of bits, but it's implemented in terms of int64's, is it a bit algorithm, or a word algorithm? 06:12:43 between ] and ! there are a series of tag characters for "IMPLIED GREETING TAG" 06:13:31 ! not in "that" 06:13:38 adu: It's a qucomplex (like complex, but qubits instead of bits) algorithm 06:15:00 File "", line 1 06:15:00 ! not in "that" 06:15:00 ^ 06:15:00 SyntaxError: invalid syntax 06:15:05 here's what I don't get, qubits are 3-states, up, down, and 90 degrees from the pole, but the there are an infinite number of possible states, but only 3 are recognized... 06:15:07 adu^ 06:15:20 adu: I don't understand it either 06:16:08 I think we should start with 7 states 3 above, 3 below, and 1 for the 90 degree state, and then gradually improve with technology 06:16:32 then we could have 127-qubit processors, then 1024-qubit processors, etc... 06:16:51 adu: Wait, it's neither 06:17:00 neither? 06:17:03 I think 06:17:13 adu: It's 1, 0, or some probabilistic superposition of both 06:17:30 So it could be e.g. pi%1, (100-pi)% 0 06:17:41 oh, right, and it's the superposition that can be prime oracle 06:18:17 There was one guy who spent 10 years building a quantum computer that can factor "15" 06:18:29 adu: On 3 atoms though 06:19:23 yeah, pretty impressive, but still not hack-the-world level 06:20:15 adu: I think I just found what is probably the only Wikipedia article with this combination of categories: 06:20:21 "Quantum mechanics" 06:20:24 "Banknotes" 06:20:58 adu: Oh, and the probabilities are apparently complex numbers 06:21:03 Because logic 06:21:21 complex numbers are very simple, actually 06:21:30 it's quaternions that are complex 06:21:44 adu: Yes, I know that 06:21:51 adu: I understand complex numbers 06:22:45 do you know my favorite complex number? 06:23:04 adu: pi? 06:23:12 4 + 3*I 06:23:40 the absolute value is 5 06:23:41 4+3i... |4+3i| = 25 06:23:48 Yes, you beat me xD 06:23:59 Wait, forgot to sqrt 06:24:32 also, because it's more real than imaginary :) 06:24:32 well, it's just a pythagorean triple 06:25:57 my favorite real number would have to be 1.6353244967152763993453446183... 06:26:07 and my favorite integer is 65536 06:26:19 https://youtu.be/GO6TsdwxcwM 06:27:06 also https://youtu.be/ZoT82NDpcvQ 06:28:12 pythagoras is /everywhere/ 06:28:48 as you can see in both videos: there are at least 4 interesting states 06:28:49 1.635... is the supremum of the interval of convergence of y = x^^y 06:28:58 1, 0, left, right 06:29:17 so qubits are 5-state? 06:29:40 well, infinitely many, but how do you come to 5? 06:29:56 myname: I'm just trying to understand quantum mechanics 06:30:05 currently, I don't 06:30:12 take a look at the two videos 06:30:55 also, there was a neat talk at 32c3 06:30:58 * adu is currently running several computations while watching Continuum, when the episode is over, I'll look at the videos 06:31:46 the talk from 32c3 is german, though 06:37:20 adu: How do qubits correspond to norbits? 06:37:54 hppavilion[1]: the movie? 06:38:05 adu: norbits are just bits 06:38:13 nor(mal) bits 06:38:27 http://www.imdb.com/title/tt0477051/ 06:39:18 adu: But what's the correspondence between bits and qubits? Do you know? 06:39:49 no 06:52:03 define correspondence 06:53:12 qubits collapse to bits 06:53:39 <\oren\> my favorite real number is only hypothetical 06:54:06 <\oren\> it's the unthinkable number closest to 1 06:55:25 so it's a hyperreal 06:55:52 <\oren\> no. 06:56:18 <\oren\> unthinkable numbers are those for which no formula could be written, even in theory 06:56:42 well, it exists in hyperreals 06:58:22 <\oren\> not because the number is infinite or anything, but because the sequence of digits is truly random, and therefore to identify the number requires an infinite amount of information 06:58:37 -!- llue has joined. 06:58:50 -!- lleu has quit (Read error: Connection reset by peer). 06:58:57 no, you just gave all the information: the smallest positive number 06:59:44 <\oren\> the smallest number such that it is unthinkable 07:00:00 <\oren\> er, no, closest to 1 07:00:24 <\oren\> among numbers for which no formula can be written, the one closest to 1 07:01:40 you don't have to write a formula for a number to exist 07:02:12 <\oren\> exactly my point 07:03:15 but on the other hand, "the smallest number without a formula" can most likely be expressed as a formula 07:03:48 <\oren\> now you're getting it 07:04:06 okay 07:05:47 my math teacher used to teach us that math is a language 07:06:25 <\oren\> so with for example godel numbering, you can enumerate all formulae for real numbers. 07:06:59 well, yeah, that's what gödel did, isn't it? 07:07:22 <\oren\> then you find that, although the real numbers are uncountable, the real numbers that can actually be thought of or used are countable! 07:08:34 \oren\: so it's a real number that is in a neighborhood of 1 07:08:55 "A The complement of A" 07:09:05 this book is going to be fun 07:09:39 <\oren\> is there supposed to be a accent on that A? 07:10:00 i can't see any. may be due to bad scanning 07:10:18 <\oren\> urgh 07:11:33 I see "A The ..." 07:11:43 exactly 07:11:54 and I have unicode fonts 07:12:01 it is ascii 07:12:12 so if there was something to see, I would see it 07:12:24 i just _typed_ it 07:12:41 "gödel" comes thru 07:13:00 what's wrong with gödel 07:13:17 myname: Which book? 07:13:52 <\oren\> adu: he's saying the book doesn't have the accents, because of some sort of error 07:13:56 that computational linguistics thingie that was "recommended" here yesterday 07:16:32 myname: I mustn't've been online 07:17:12 statistical natural language processing 07:24:14 ᵃᵇ?ᵈᵉ?ᵍʰⁱʲᵏˡᵐⁿᵒᵖ?ʳˢᵗᵘᵛʷˣʸᶻ 07:42:59 -!- adu has quit (Quit: adu). 08:08:38 -!- hppavilion[1] has quit (Ping timeout: 276 seconds). 08:10:06 -!- mauris has joined. 08:13:35 -!- mauris_ has quit (Ping timeout: 265 seconds). 08:15:44 -!- mroman has joined. 08:33:04 -!- hppavilion[1] has joined. 08:40:27 Does untyped Quantum λ-calculus make any sense? Something with the nice λs so I feel safe reading it? xD 08:41:16 if all you have is a hammer :p 08:41:45 yeah 08:41:51 but you may not use this hammer for commercial purposes 08:42:07 also you may only use it to hammer in nails produced by $company 08:42:10 everything else is illegal 08:42:16 @massages-load 08:42:17 oerjan said 17h 11m 36s ago: blub. blib blub blub! 08:42:24 @tell oerjan what? 08:42:25 Consider it noted. 08:42:40 that would be the case if the hammer were software 08:42:43 or hardware 08:43:02 such licenses should be illegal. 08:43:17 If I get a product I should be allowed to use it like I want to 08:43:32 (unless I'm using it against other laws such as not killing people) 08:43:43 but otherwise I should be allowed to do whatever the fuck I want with it. 08:44:23 if a hammer were software people could demand that they get a revenue share of everything you build with that hammer. 08:44:47 "Ow see, you built this house with our hammer and that means we now own part of that house because you used our tool to construct it." 08:48:28 Nintendo is doing something like that with YouTube revenue :) 08:49:02 you gotta share your revenues with Nintendo as soon as you have at least one video in your channel featuring nintendo content. 08:49:23 they are going to collect money from people now that advertise your product for free on the internet 08:49:34 that's like ... the most capitalist thing ever ... 08:50:52 "See, you bought our hammer and teach courses on how to hammer with it to people for money. Since it's our hammer we're entitled that you share your total income with us." 08:51:38 where can I lobby against these kind of companies :( 08:57:05 -!- J_Arcane has quit (Ping timeout: 265 seconds). 09:10:28 -!- Froo has joined. 09:12:44 -!- andrew has joined. 09:13:28 -!- Froox has quit (Ping timeout: 250 seconds). 09:31:16 mroman: You asked whether the microphone in a smartphone works underwater. 09:31:20 Re: blub. 09:59:47 -!- hppavilion[1] has quit (Ping timeout: 276 seconds). 10:14:19 well 10:14:22 sound travels underwater 10:14:23 so.... 10:14:35 not very good but it travels 10:15:17 MInsky :( 10:45:41 `quote 147 10:45:43 147) syntax is the least important part of a programming language other than Python 10:48:43 -!- mauris_ has joined. 10:49:48 -!- AnotherTest has joined. 10:51:50 -!- mauris has quit (Ping timeout: 260 seconds). 10:57:48 -!- AnotherTest has quit (Quit: ZNC - http://znc.in). 11:12:54 j-bot: help 11:12:54 Taneb: |value error: help 11:13:04 j-bot: 4 * 2^.5 11:13:05 Taneb: 9.28771 11:14:03 What's the character for j-bot? 11:14:11 ( 4 11:14:11 4 : Integer 11:14:23 Thanks, idris-bot 11:14:31 fungot: what's the character for j-bot? 11:14:32 Taneb: the latter, usually only way for it to compile! 11:14:49 Thanks, fungot, but that's not quite what I meant 11:14:49 Taneb: a good first choice, but i don't use any linux at all. it is _much_ harder than trying to find 11:15:54 ( log 2 11:15:54 0.6931471805599453 : Double 11:16:08 ( 4 * log 5 / log 2 11:16:09 9.287712379549449 : Double 11:26:14 -!- andrew has quit (Remote host closed the connection). 11:27:00 -!- andrew has joined. 11:30:07 -!- boily has joined. 11:45:25 Taneb: [. 11:48:26 fizziello. ]? 11:51:37 -!- oerjan has joined. 11:55:08 hellørjan. floating brackets. 11:56:25 helloily. li(ke thi)s? 11:56:55 @messages- 11:56:56 mroman said 3h 14m 31s ago: what? 11:57:09 . o O ( somebody set us up the bomb! ) 11:57:38 like { 11:57:39 https://github.com/ryna4c2e/sed-brainfuck https://github.com/svbatalov/bf.sed 11:57:41 this } 11:57:46 @tell mroman mroman said 3h 14m 31s ago: what? <-- blub. you no speak fish? 11:57:46 Consider it noted. 11:58:18 izabellora. are you svbatalov? 11:58:24 @tell mroman i've forgotten why i spoke fish, except that there was a good reason. try the logs. 11:58:24 Consider it noted. 11:58:29 nope 11:58:36 impressive work tho 11:58:40 both of them 12:01:05 -!- backendbeemo has joined. 12:01:07 -!- backendbeemo has left. 12:03:51 and now there's a sed process that's eating 100% of my cpu trying to sing 100 bottles of beer on the wall 12:05:12 100% of cpus on the wall ♪ 12:05:57 :) 12:10:42 it actually worked, took 7m12.5s but it worked 12:10:58 * izabera is impressed 12:13:29 -!- boily has quit (Quit: SUBCOMPACT CHICKEN). 12:13:45 -!- oerjan has set topic: Go tromp et al.! | The international hub for magic gathering and deployment. | Eﬃ's ﬁneﬆ ﬂuﬀy waﬄes | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/?C=M;O=D | https://esolangs.org/ | 100% of cpus on the wall ♪. 12:14:36 `? boily 12:14:47 boily is monetizing a broterhood scheme with the Guardian of Lachine, apparently involving cookie dealing. He's also a NaniDispenser, a Trigotillectomic Man Eating Chicken and a METARologist. He is seriously lacking in the f-word department. 12:14:59 laggy 12:15:13 crappy vm 12:17:29 -!- backendbeemo has joined. 12:17:30 -!- backendbeemo has left. 12:20:48 my left arrow key is lagging too :( 12:22:02 or seemingly missing occasional presses 12:23:46 oerjan: The reason was a discussion on whether smartphone microphones work underwater hth 12:23:56 For fish, not for lagging keys. 12:24:21 (I told this to mroman as well.) 12:24:42 right 12:30:53 -!- andrew has quit (Remote host closed the connection). 12:39:57 > iterate (1.63**) 1 12:40:00 [1.0,1.63,2.21751106303051,2.95480183600564,4.23615968785223,7.9224695022536... 12:45:04 this doesn't work and i have no idea what adu meant 12:49:23 @tell adu the weirdness of qubits is such that the answer to how many states they have is either (a) 2, like ordinary bits; or (b) that's meaningless, you cannot think of the global quantum state as separated into the individual qubits. 12:49:24 Consider it noted. 12:53:24 fungot: You're running on a Linux system, I don't think you can say you don't use any Linux at all. 12:53:24 fizzie: yes tell me how to not care. i just wish someone could translate the ca 10 haskell lines to scheme for you. i spent too much time 12:53:35 fungot: Don't you get uppity with me. 12:53:35 fizzie: a fnord c-like language for making bot ai's for a game 12:54:07 fungot: You *are* a bot AI for the game called IRC. 12:54:07 fizzie: didn't work too insanely well as you can get some food 12:56:10 @tell adu or put differently, there are only two _well_-defined states for a qubit to be in, all other states only make sense as states of the whole system of qubits. 12:56:11 Consider it noted. 13:02:42 @tell \oren\ <\oren\> it's the unthinkable number closest to 1 <-- there is no such number. the impossible part isn't the "unthinkable", but the "closest to 1" hth 13:02:43 Consider it noted. 13:03:56 * oerjan thinks the logs are disturbingly full of shoddy math today 13:05:30 would you waste time to optimize +++, to , ? 13:05:36 in a brainfuck optimizer 13:05:53 @tell \oren\ proof: clearly 1 is not unthinkable. if x is unthinkable, then (1+x)/2 is also unthinkable, but closer to 1. thus no closest exists QED. 13:05:53 Consider it noted. 13:06:05 if EOF is 0 or -1 13:06:54 pro: obviously better con: only improves stupid programs 13:07:41 izabera: note that "stupid" includes "auto-generated" 13:09:43 -!- izabera1 has joined. 13:09:54 wtf my amazon server is offline 13:10:27 * oerjan has a feeling the universe doesn't want him to spread his wisdom today. 13:10:56 blub! 13:11:00 @massages-load 13:11:00 oerjan said 1h 13m 13s ago: mroman said 3h 14m 31s ago: what? <-- blub. you no speak fish? 13:11:00 oerjan said 1h 12m 36s ago: i've forgotten why i spoke fish, except that there was a good reason. try the logs. 13:11:21 -!- p34k has joined. 13:11:31 -.- online 13:11:46 > group $ iterate (1.63**) 1 13:11:48 [[1.0],[1.63],[2.21751106303051],[2.95480183600564],[4.23615968785223],[7.92... 13:12:13 > filter (\c -> (length c) >= 2) $ group $ iterate (1.63**) 1 13:12:17 -!- izabera1 has quit (Client Quit). 13:12:18 mueval-core: Time limit exceeded 13:12:21 hm 13:12:33 mroman: i seriously doubt that converges, which is why i wondered wtf adu meant 13:12:43 yeah but double has finite precision 13:12:49 so I thought at some point it wouldn't change anymore 13:13:01 (because of precision limitation) 13:13:04 well it would reach +INF 13:13:19 > filter (\c -> (length c) < 2) $ group $ iterate (0.63**) 1 13:13:22 [[1.0],[0.63],[0.7474541304505948],[0.7079722983415685],[0.7210056493825268]... 13:13:30 > filter (\c -> (length c) >= 2) $ group $ iterate (0.63**) 1 13:13:34 mueval-core: Time limit exceeded 13:13:37 > drop 10 $ iterate (1.63**) 1 13:13:39 [Infinity,Infinity,Infinity,Infinity,Infinity,Infinity,Infinity,Infinity,Inf... 13:13:54 > group $ drop 10 $ iterate (1.63**) 1 13:13:56 [[Infinity,Infinity,Infinity,Infinity,Infinity,Infinity,Infinity,Infinity,In... 13:13:59 the point is, it's not actually _converging_, it's growing faster 13:14:14 oh 13:14:15 ok 13:14:22 it can't calc the length of that group of infinities 13:14:29 how large is a group of infinities? 13:14:35 infinite hth 13:14:40 but... 13:14:49 it contains infinity infinitely many times 13:14:49 PRETTY SURE 13:14:54 so it's SUPER INFINITE 13:15:01 > group $ replicate 3 (1/0) 13:15:05 [[Infinity,Infinity,Infinity]] 13:15:16 oh you already checked that 13:16:03 hm... 13:16:50 also it's lazy enough to give the infinities, but it would hang if you ever try to find the next group. 13:17:23 but grouping that contains a list of infinite infinity 13:17:27 so length hangs 13:17:56 mroman: you know that m*m = m when m infinite cardinality is a theorem equivalent to the axiom of choice, right? 13:18:26 that doesn't matter 13:18:37 well it means you cannot super infinite that way 13:18:40 if the list is [1,2,3,Infinity,Infinity,Infinity,Infinity....] 13:18:45 and you group it 13:18:48 (power sets work, of course) 13:18:54 you have 3 elements of length 1 13:18:57 and one element of length infinity 13:19:04 so map (length) on that grouped list would hang 13:19:15 yep. as would length itself 13:19:20 exactly 13:19:25 that's why the length >= 2 doesn't work 13:19:33 it should work with atLeastTwo 13:20:11 well then you get the problem that it hangs if you try to get the "next" group 13:20:20 > let atLeastTwo (x:y:_) = True; atLeastTwo _ = False in filter atLeastTwo $ group $ iterate (0.63**) 1 13:20:24 mueval-core: Time limit exceeded 13:20:26 hm 13:20:32 at least in my head this would've worked 13:20:44 > let atLeastTwo (x:y:_) = True; atLeastTwo _ = False in head $ filter atLeastTwo $ group $ iterate (0.63**) 1 13:20:48 mueval-core: Time limit exceeded 13:21:01 it doesn't work because it doesn't know that there is no more groups after the infinite one 13:21:10 oh hm 13:21:17 _that_ should have worked. 13:21:27 * oerjan confused now. 13:21:30 > let atLeastTwo (x:y:_) = True; atLeastTwo _ = False in head . head $ filter atLeastTwo $ group $ iterate (0.63**) 1 13:21:33 this' should give Infinity 13:21:34 mueval-core: Time limit exceeded 13:21:46 @type let atLeastTwo (x:y:_) = True; atLeastTwo _ = False in head . head $ filter atLeastTwo $ group $ iterate (0.63**) 1 13:21:48 (Eq c, Floating c) => c 13:22:04 y u not working like u should man 13:22:15 hm 13:22:16 atLeastTwo shouldn't hang 13:22:30 indeed 13:22:39 and it should never look at more than the first 13:22:43 oh 13:23:14 you're using 0.63 instead of 1.63 13:23:41 > drop 10 $ group $ iterate (0.63**) 1 13:23:44 [[0.7177586391896805],[0.7177528833823562],[0.7177547921676407],[0.717754159... 13:23:53 > drop 50 $ group $ iterate (0.63**) 1 13:23:56 [[0.7177543168046071],[0.717754316804607],[0.7177543168046071],[0.7177543168... 13:24:23 thought so. that theoretically converges, but in double it gives a periodic loop. 13:25:40 wait, did adu just write 1 instead of 0 13:26:17 > drop 50 $ group $ iterate (0.64**) 1 13:26:21 [[0.7239190318772367],[0.7239190318772366],[0.7239190318772367],[0.723919031... 13:26:41 still looks pretty converging 13:27:44 mroman: ok your problem was that with 0.63 it converges, but _not_ in Double. 13:34:28 Floating points strike again. 13:39:43 du du duuun 13:42:01 [wiki] [[Special:Log/newusers]] create * Sbneelu * New user account 13:43:58 -!- impomatic_ has joined. 14:08:59 -!- ais523 has joined. 14:09:16 I suspect in the real numbers it would converge too, although I have no proof 14:09:33 There probably is some way to prove it 14:09:40 -!- impomatic_ has left. 14:10:40 there probably is some way to prove that there's some way to prove it 14:11:52 very few things will converge in Double 14:11:59 (besides constant sequences, of course) 14:12:17 > let f (x:y:_) | x == y = x; f (_:y) = f y in f $ iterate (0.66**) 1 14:12:20 0.7363978892794596 14:12:26 the nature of denormals means that you can't get most numbers closer than denormals are to 0 14:13:59 what magic is happening with that guard 14:14:29 ah 14:14:32 nevermind 14:16:42 yeah, took me a moment too 14:18:38 oerjan: what? 14:18:54 @type let atLeastTwo (x:y:_) = True; atLeastTwo _ = False in head . head $ filter atLeastTwo $ group $ iterate (1.63**) 1 14:18:55 (Eq c, Floating c) => c 14:18:57 > let atLeastTwo (x:y:_) = True; atLeastTwo _ = False in head . head $ filter atLeastTwo $ group $ iterate (1.63**) 1 14:19:00 Infinity 14:19:11 oh I see :D 14:19:20 mroman: iterate (0.63**) ends up fluctuating between two close Doubles. 14:19:20 > let f (x:y:_) | x == y = repeat "conv"; f (x:y:z:_) | x == z = repeat "p2"; f (_:y) = f y in ((!! 100) . f . (\x -> iterate (x**) 1)) <$> [0.60, 0.61, 0.62, 0.63, 0.64, 0.65, 0.66, 0.67, 0.68, 0.69, 0.70] 14:19:23 ["conv","p2","conv","p2","p2","conv","conv","conv","p2","conv","conv"] 14:20:02 Wolfram Alpha says that for z = k^z the solution is z = Wn(-log(k))/log(k) 14:20:38 hm... 14:20:46 Where Wn is some weird function 14:21:16 > log 0.63 * 0.63**0.717754316804607 14:21:18 -0.33162794564223064 14:22:10 FreeFull: see how the derivative is smaller than 1 in absolute value. that means it will shrink the interval around the fixpoint (now just prove there is a fixpoint) 14:22:57 oerjan: Can you show it diverges for k > 1? 14:23:07 (actually, prove there's some interval mapped into itself, where the derivative is || < 1) 14:23:15 -!- spiette has joined. 14:40:05 -!- Treio has joined. 14:48:51 are independence theorems necessarily provable 14:49:07 if S is a sentence, I is "S is independent", and I' is "I is independent" 14:49:20 coppro: if they're theorems, they are provable hth 14:49:24 then if I' is true, S cannot be provably true, and cannot be provably false, so I is true, contradiction 14:49:29 oerjan: w 14:49:40 therefore I' is false 14:53:11 coppro: "I is true" does not imply "I is not independent" hth 14:53:57 hm wait 14:56:41 yep 14:57:19 if S is not provably true, not provably false, then I is true, but not necessarily provable, so I' can still be true. 14:57:31 *nor 14:59:31 what does "independent" mean here? that neither assuming it nor assuming its negation leads to a contradiction? 15:00:13 presumably. 15:01:41 coppro: there are various different formalizations of provability, in some of them but not all you have a result of the form "if 'X is provable' is provable, then X is provable", and in some of them but not all you have the converse 15:03:01 also, in some of them you can prove those statements inside the logic, and in others they're true but you can't prove them inside the logic 15:21:36 oerjan: hmm right 15:21:45 it would take a *proof* of I' to lead to a contradiction 15:21:46 -!- oerjan has set topic: R.I.P. Marvin Minsky | The international hub for magic gathering and deployment. | Eﬃ's ﬁneﬆ ﬂuﬀy waﬄes | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/?C=M;O=D | https://esolangs.org/ | 100% of cpus on the wall ♪. 15:40:29 coppro: this was my reasoning about P=NP 15:40:36 was wondering if it might actually be undecidable 15:40:42 I concluded that if it were undecidable, there would be no way to prove that 15:44:44 i think there are subtleties there 15:53:08 Undecidably undecidable? 15:53:27 -!- MDream has changed nick to MDude. 15:53:48 MDream: it could well be decidably decidable 15:53:56 I see how it couldn't be provably undecidable. 15:54:24 Since if it proven undecidable, you'd know you'd never get prove that would make it decidable. 15:54:46 And any algorithm that allows P to equal NP would be decisive. 15:55:12 It could even be undecidably decidable 15:55:29