00:00:16 -!- hppavilion[1] has joined. 00:00:23 Here's a problem of theoretical interest to me 00:00:58 Given a number by its prime factorization, calculate the prime factorization of its successor 00:01:10 The idea behind it is Esoteric Data Types 00:01:35 Specifically, the PFact number encoding 00:01:37 easy, drop everything you have and start from scratch 00:02:01 myname: Huh? 00:02:44 i don't think you can get the factorization any easier with the factors of the predecessor 00:02:54 at least not in the general case 00:03:01 myname: This isn't for code I'm working on, this is for a humorous data types 00:03:26 myname: How about for numbers that can be expressed as the product of 8 prime numbers, all of which must be in the smallest 256 prime numbers? 00:03:27 xD 00:03:51 (wait, no, smallest 255, where 0b00000000 is 1) 00:04:17 -!- Nithogg has quit (Ping timeout: 260 seconds). 00:04:32 myname: The idea behind the PFact type is that it's a data type that expresses numbers as the product of 8 primes 00:04:59 -!- Nithogg has joined. 00:05:00 Well, up to 8 00:05:22 myname: Assuming 64-bit registers, each number must fall in the 255 smallest primes, with 1 filling in gaps when n<8 00:11:34 -!- augur has joined. 00:14:40 hey 00:18:48 -!- tromp has joined. 00:20:55 Lemme find one of those hard-to-factor numbers. 00:21:21 Now, the question "given the factorization of n, what is the factorization of n+1?" definitely sounds pretty interesting. 00:21:36 And here's one thing that you do know: the two numbers cannot have any prime factors in common. 00:21:52 would be surprised if you can say anything enormously stronger than that 00:22:14 (Because if p is a prime factor of n and p is also a prime factor of n+1, then n/p and (n+1)/p are both integers, so 1/p is an integer. But that's impossible.) 00:22:40 afaik the link between the primeness of n and n+2 is still an open problem 00:23:22 Here's a number that's hard to factor: 00:23:24 1522605027922533360535618378132637429718068114961380688657908494580122963258952897654000350692006139 00:23:32 also, at most one of the numbers can _be_ prime hth 00:23:44 ...excepting 2 and 3. 00:23:51 Except that it's pretty easy to factor it using the Google method. 00:23:59 Anyway, let's see what the factorization of its predecessor is. 00:24:24 oerjan: 2 and 3 don't have any prime factors in common 00:24:41 Other than 2.5 00:24:46 coppro: and this contradicts what i said how? 00:24:57 oh 00:25:01 I missed the line above that 00:25:02 nvm 00:25:15 Okay, I found the factorization. It is: 00:25:41 2 * 3^2 * 210974974123 * 400944086233670527306310281636760087998315351567377660286363410284049027879820778576767 00:25:57 the 2 was easy 00:25:58 That's probably pretty dang unhelpful. 00:26:04 Yup. 00:26:28 Fun fact: for 100% of all prime numbers p, p-1 has 2 as a factor. 00:26:50 I wonder what the factorization of 400944086233670527306310281636760087998315351567377660286363410284049027879820778576766 is... 00:26:52 what about 2? 00:27:01 i vaguely recall there's some restriction on the prime factorization of pq-1 in order for pq to be a good RSA key 00:27:16 myname: nope, 2-1 doesn't have 2 as a factor. 00:27:28 that's not 100% then 00:27:33 Of course it is. 00:27:38 Surprisingly, 400944086233670527306310281636760087998315351567377660286363410284049027879820778576766 is taking several seconds to factor. 00:27:52 how is it? 00:28:03 myname: it's 100% by the most useful definition, aka density. 00:28:07 Well, what percentage do you think it is? 00:28:22 i see what you did there 00:32:33 Dang, it's taken over five minutes so far to factor that bad boy. 00:37:23 -!- impomatic_ has quit (Ping timeout: 248 seconds). 00:39:50 if I recall the idea of RSA is that, if you calculate 2^n modulo 13, the result will loop every steps 00:39:59 every 12 steps 00:40:33 since the result can't go through 0 but it has to go through all other numbers since 2 and 13 have no common factors 00:41:29 Do you know if it is OK to call Pa_Terminate and/or Pa_CloseStream in a signal handler? 00:41:41 if you calculate 2^n modulo 13*17, logically the modulo 13 part loops every 12 and the modulo 17 part loops every 16 00:44:11 ""For security purposes, the integers p and q should be chosen at random, and should be similar in magnitude but 'differ in length by a few digits"" 00:46:18 "Since any common factors of (p-1) and (q-1) are present in the factorisation of p*q-1,[14] it is recommended that (p-1) and (q-1) have only very small common factors, if any besides the necessary 2." 00:52:20 -!- XorSwap has joined. 00:58:47 Woo. It took half an hour and fifteen seconds, but I got that number factored. The factorization is: 00:59:25 2 * 3 * 409 * 1645447576107402059859920361500918359 * 99294502354941754852634597949140561238814554731 00:59:35 Now, of course, I wonder what the factorization of 99294502354941754852634597949140561238814554730 is. 01:00:27 go for it 01:00:51 if I recall the idea of RSA is that, if you calculate 2^n modulo 13, the result will loop every steps <-- i think you may be confusing RSA with discrete logarithm, or something. 01:01:18 It's 2 * 5 * 17 * 22369 * 243130343851969331 * 107396603915138092862971. And the factorization of 107396603915138092862970 is 2 * 3 * 5 * 13 * 17 * 281 * 991 * 2758397 * 21088237. 01:02:09 And the factorization of 21088236 is 2^2 * 3 * 13 * 135181, and the factorization of 135180 is 2^2 * 3^2 * 5 * 751. 01:02:12 Done. 01:02:29 oerjan : RSA and the discrete logarithm are related I think 01:02:30 weird anchor 01:02:47 `? weird anchor 01:02:55 weird anchor? ¯\(°_o)/¯ 01:03:13 since the result can't go through 0 but it has to go through all other numbers since 2 and 13 have no common factors <-- that's not enough, you actually need to check if 2 has that property. however, given that 13 is prime, _some_ number ("primitive root") will loop through all of them. 01:03:48 mad: a bit maybe. 01:04:18 > length $ nub [2^n `mod` 13 | n <- [0..11]] 01:04:19 12 01:04:51 oerjan: huh? 01:04:59 what did you expect? 01:05:12 > [(p,length $ nub [2^n `mod` p | n <- [0..p-1]]) | p <- [3,5,7,11,13,17,19,23,29,31]] 01:05:13 [(3,2),(5,4),(7,3),(11,10),(13,12),(17,8),(19,18),(23,11),(29,28),(31,5)] 01:05:30 myname: it could have been something else. of course 13 _wouldn't_ be an example. 01:06:10 ah, 1,2,4,1 01:06:12 i see 01:06:23 look at 7, 17, 23 and 31 up there. 01:07:02 in general, the order is some factor of p-1 01:07:19 but not all numbers will give exactly p-1. 01:07:42 hmm 01:09:40 if you calculate 2^n modulo 13*17, logically the modulo 13 part loops every 12 and the modulo 17 part loops every 16 <-- i vaguely recall our professor pointing out that RSA works even if the number you take power of _does_ have _one_ of the primes as a factor. which doesn't follow from that argument and needs a distinct proof. 01:10:00 hmmm 01:11:29 hm wait does that make sense. 01:12:19 hm i think so. 01:12:35 tswett: Oh, you're factoring numbers. Great 01:12:44 tswett: Of course, you're doing it the noob way 01:12:48 well 01:13:05 if you start with some number N, multiply by 2, modulo M 01:13:12 say M is 17 01:13:16 repeat 01:13:23 you have two possible loops 01:13:47 Done. <-- now use that to create a prime certificate for whatever it was you started with hth 01:13:56 Let's play: What's! That! Algorithm! 01:14:34 You all know the rules: Given an algorithm constraint or constraint set (complexity class, space complexity, etc), name an algorithm that operates in it 01:14:38 O((log N)2(log log N)(log log log N)) 01:15:08 1>2>4>8>16>15>13>9>1... and 3>6>12>7>14>11>5>10>3... 01:15:14 why is the 2 in the middle? 01:15:32 i guess you are missing stuff 01:15:47 i guess it is ^2 and there is a / et the end 01:15:49 myname: It's a suberscript 01:15:56 the loop time is guaranteed to be p-1 or p-1 divivded by n 01:16:23 myname: I copied it directly, there are no mistakes 01:17:27 mad: p-1 is just (p-1)/1, anyhow 01:19:05 hppavilion[1]: you're assuming copying a webpage formula gives you a reasonable copy tdnh 01:19:40 oerjan: It did in this case 01:19:54 oerjan: O((log N)2(log log N)(log log log N)) is short enough to verify correctness by reading 01:19:58 isn't the 2 a superscript at _least_? 01:20:24 you said as much. so it was not correctly copied. 01:21:17 n ^ (p-1) modulo p = 1 01:21:20 I _think 01:21:32 mad: yes, that's fermat's little theorem. 01:22:03 n ^ (p-1)(q-1) modulo pq = 1 01:22:25 mad: assuming p and q are not factors of n 01:22:57 well, assuming n < pq 01:23:20 and yes assuming that p and q are prime 01:23:40 n < pq is not enough, what if n = p 01:24:09 then it's looping though q only I think? 01:24:20 obviously. 01:24:29 which means that then n ^ (q-1) = 1 01:25:18 but still you have n ^ ((p-1)(q-1)+1) == n (mod pq), which is what my professor mentioned 01:25:48 or thereabouts. 01:25:55 n ^ k(p-1)(q-1) modulo pq = 1 for any k 01:26:21 well, obviously 01:26:36 1^k = 1 is no rocket science 01:26:55 except in linear logic hth 01:27:28 i don't know that stuff yet 01:27:39 oerjan: So what does it mean that LEM is multiplicative? 01:28:23 least evil multiple 01:28:47 law of excluded middle 01:29:22 shachaf: well, you know that proof of LEM (or something equivalent to it) using continuations, right? 01:30:08 Yes. 01:30:10 and using continuations for cheating by passing a counterexample back... which is iiuc also what # allows you to do 01:30:21 so it needs that feature of #. 01:30:21 Right, except it's more/less restricted. 01:30:44 # is a bit like threads. 01:30:50 And so is ⊗ 01:33:01 lemCC = callCC (return . Right . (<=< return . Left)); 01:33:41 callCC x = lemCC >>= either return x; 01:34:10 :t callCC (return . Right . (<=< return . Left)) 01:34:11 MonadCont m => m (Either a (a -> m b)) 01:34:43 Does a prime number not being in a number's prime factorization imply that that number does not evenly divide the latter number? 01:34:56 I would think it does under the Fundamental Theorem of Arithmetic 01:35:21 hppavilion[1]: yes. i think that's usually a lemma used to _prove_ the FTA 01:35:23 how should it? 01:35:27 Yes it does imply 01:35:40 that is, if p divides m*n, then p must divide either m or n. 01:36:46 Oh, I see where this bug is coming from 01:36:50 I think callCC is a better axiom than the law of excluded middle. 01:37:01 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 01:37:01 In fact, it's more of a lemma. 01:37:06 Well, either one would work 01:37:17 shachaf: callCC is pierce's law 01:37:22 I know. 01:37:25 Either one can be prove by the other one 01:37:26 I was just going for the pun. 01:37:58 oerjan: also it's peirce's law because why should anything be easy hth 01:38:17 Wait... 01:38:23 -!- JX7P has joined. 01:38:30 Intuitionistic logic forgoes the law of excluded middle, does it not? 01:38:32 shachaf: i considered checking and/or lampshading 01:38:37 hppavilion[1]: yes. 01:38:50 this must be the closest to a substitute for ##programming that i can find focusing particularly on PLT/language design 01:38:52 oerjan: And type systems are typically intuitionistic? 01:39:02 JX7P: PLT? 01:39:13 programming language theory 01:39:13 <\oren\> wat. kim kardashian's father was oj simsons lawyer? 01:39:15 JX7P: Yeah, we're the most active one at least 01:39:21 often, like gay rights, symbolised by the lambda 01:39:25 JX7P: There is ##proglangdesign, but it's not as active 01:39:32 JX7P: Yeah xD 01:39:38 it is also empty 01:39:42 Yes normally the type system are using intuitionistic logic, although you can use classical logic with continuations 01:39:47 JX7P: Might've typoed 01:40:03 JX7P: It was kind of a shock when I first saw the lambda associated with gay rights :P 01:40:19 wat 01:40:21 oerjan: What do you think about dual-intuitionistic logic? 01:40:33 JX7P: We do do design, but we typically don't focus on making it good so much as interesting and different, but we might still be able to help you. 01:41:04 shachaf: dual-intuitionistic logic thinks about me hth 01:41:19 oerjan: Are you a soviet? 01:41:26 oerjan: cmccann was excited about it a while ago and now that I'm reading about linear logic I'm a bit excited about it too. 01:41:30 hppavilion[1], as a community alone it will be interesting i think 01:41:45 JX7P: OK 01:41:53 ##programming did not appreciate my constant invocation of dialectical logic, which led to getting quieted 01:41:55 JX7P: Do you have any ideas in mind? 01:42:03 Dialectical? 01:42:19 <\oren\> what's dialectical logic? 01:42:20 i, on the other hand, think the perfect riposte to that is a programming language substituting dialectical logic for formal logic 01:42:38 -!- augur has quit (Remote host closed the connection). 01:42:45 whoa whoa whoa 01:42:58 it's the logic developed by plato, hegel, marx, and adorno 01:42:58 "Dialectical logic was the system of laws of thought, developed within the Hegelian and Marxist traditions, that sought to supplement or replace the laws of formal logic." 01:42:59 Is that like dialectica categories? 01:43:14 oerjan: Are you a soviet? <-- no, but dual logic clearly is hth 01:43:22 oerjan: Yeah 01:43:26 oerjan: Also, dialectical 01:44:11 maybe the most significant thing noted in dialectical logic is that ¬¬X is X, but X isn't ¬¬X 01:44:12 -!- lynn_ has quit (Ping timeout: 244 seconds). 01:44:28 oerjan: Dual-intuitionstic logic has DNE but not DNI 01:44:54 the negation of the negation is 'enriched', it is the original but of a higher order 01:45:03 ##programming did not appreciate my constant invocation of dialectical logic, which led to getting quieted <-- such is being the antithesis? 01:45:24 oerjan, the synthesis being my joining this channel 01:45:34 Like how in intuitionistic logic logic you can only have one thing on the right side of a sequent, in the dual you can only have one thing on the left side. 01:45:35 now I am back at the thesis, being in a channel about programming 01:46:01 but this time it has become refined, enriched, by finding a channel more specifically suited to my particular interests 01:46:20 shachaf: you know, that sounds strangely like what JX7P said above 01:46:25 JX7P: Checked out the wiki yet? 01:46:34 somehow. 01:46:37 hppavilion[1], i'm afraid i haven't 01:46:40 You can tell me if you intend to design any kind of programming language and whatever 01:46:45 `wiki 01:46:46 /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: wiki: not found 01:46:51 Damn, was hoping that'd work 01:46:53 oerjan: whoa whoa whoa, so it is 01:47:01 maybe dual-intuitionistic logic and dialectic logic is the same thing! 01:47:02 http://esolangs.org/ is wiki 01:47:40 dual intuitionistic logics have some similarity since they can handle contradictions 01:47:42 `` echo "echo \"http://esolangs.org/wiki/Main_Page\"" > bin/wiki 01:47:42 oerjan: maybe you and i are the same thing 01:47:45 No output. 01:47:48 `wiki 01:47:49 /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: /hackenv/bin/wiki: Permission denied \ /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: /hackenv/bin/wiki: cannot execute: Permission denied 01:47:52 ... 01:47:56 I'm not going to go there today 01:47:58 hppavilion[1]: should've used mkx 01:48:04 shachaf: Right, right 01:48:24 `rm bin/wiki 01:48:27 But also shouldn't've cluttered bin/ like that. That's why we have wisdom. 01:48:28 No output. 01:48:33 ...To be cluttered up? 01:48:42 shachaf: Yes, but this way we can just do `wiki 01:48:45 And look badass 01:48:51 (Relatively) 01:49:03 ^wiki 01:49:03 http://esolangs.org/wiki/ 01:49:04 anyway, thanks zzo38 01:49:04 JX7P: Know any LISP? 01:49:07 oerjan: Thank you 01:49:11 hppavilion[1]: why not add a factoid instead of a command? 01:49:20 hppavilion[1], i'm familiar with scheme at a basic level 01:49:21 `? wiki 01:49:23 The wiki is at http://esolangs.org/wiki 01:49:28 JX7P: Made your own LISP yet? 01:49:28 hppavilion[1]: I didn't even do that for `weather 01:49:31 `? weather 01:49:32 lambdabot: @@ @@ (@where weather) CYUL ENVA ESSB KOAK 01:49:34 CYUL 050100Z 15004KT 15SM SKC M07/M15 A3025 RMK SLP248 \ ENVA 050050Z 09007KT 5000 -SN VV007 01/M01 Q1002 RMK WIND 670FT 14013KT \ ESSB 050120Z AUTO 12005KT 9999 FEW025/// OVC031/// 01/M00 Q1008 \ KOAK 050053Z 15012KT 10SM -RA SCT019 BKN037 OVC075 17/17 A2993 RMK AO2 RAE18B34 SLP133 P0000 T01720167 01:49:37 also Coke (which is not quite Lisp but is close) 01:49:39 -!- augur has joined. 01:49:40 lambdabot: THAMBDABOT 01:49:46 `misle/rn wiki/The wiki is at http://esolangs.org/wiki 01:49:49 Was lied to about «wiki» 01:50:00 hppavilion[1], it formed a very useful avenue for research https://github.com/Valutron/Valutron 01:50:11 i really want to misle rn 01:50:15 hppavilion[1]: why? 01:50:28 it was a partnership effort. unfortunately my partner lost interest 01:50:36 Can we make `? wiki direct you to an ancient stone tablet or give you an ISBN? xD 01:50:46 Why? 01:50:53 I think the esolang wiki is not a book? 01:50:53 what for? 01:51:08 myname: shachaf: zzo38: To be more in line with wisdom 01:51:16 eh? 01:51:23 What are you suggesting? 01:51:27 That wisdom isn't useful? 01:51:30 `tomfoolery wisdom 01:51:33 wisdom is tomfoolery 01:51:51 shachaf: No 01:51:59 shachaf: It'd be the ISBN for a really good book 01:52:05 shachaf: Which would be useful 01:52:10 But that's not what people want. 01:52:14 that would not be the wiki 01:52:18 in the end, valutron's main yield was twofold: #1 lisps can be easily translated into a forth; #2 everything must, must be an object 01:53:35 \oren\: OO language alert 01:54:00 hppavilion[1]: any attempt to cleanse wisdom of everything true may lead to me merging tomfoolery back into it hth 01:55:07 hppavilion[1] : the world is OO 01:55:44 what i particularly like about SmallTalk is that Alan Kay describes the objects as monadic 01:55:50 (meaning it in the leibnizian sense) 01:56:00 <\oren\> hppavilion[1]: as i've said before my problem sin't with OO itself but with the way a lot of OO languages treat functions badly 01:56:02 this causes no end of confusion to functional people 01:56:08 https://www.quora.com/What-is-the-most-illegal-thing-you-could-possibly-do/answer/Phil-Albert 01:56:28 \oren\, perhaps you would respect the Combined Object-Lambda Abstraction and its implementation Coke 01:56:43 plot twist: removing true wisdoms is illegal? 01:57:15 or even SmallTalk-71/72, when it was still obviously lisp 01:57:30 \oren\ : how do OO languages treat functions badly? 01:59:59 <\oren\> for example, in java, you can't have a function that isn't inside a class 02:00:13 this is a design element 02:00:29 and? you can have a static function instead, that's functionally equivalent 02:00:35 the idea is that the only action is the communication of objects 02:00:39 <\oren\> and can't pass a function to another function (even though C can) 02:01:02 in SmallTalk-family languages, one can simply pass a selector or a block to functions 02:02:34 or even a whole message ready to be sent 02:02:46 there are no functions in the Kayian OO 02:02:55 \oren\ : java uses interfaces instead of pointers for callbacks yes 02:03:35 I want to make a hackable LISPlike2JS compiler 02:03:45 s/compiler/transpiler/ 02:04:04 Something that people can download and reengineer into a custom language for their own devious purposes 02:05:20 I guess you could say the same for C/C++, what you have is really more callbacks than function variables 02:05:37 <\oren\> overall, these OO languages tend to require a lot of boilerplate and repeating the same code 02:06:01 i think it's important not to conflate Java and C++ with authentic Kayian OO 02:06:04 \oren\: Which is exactly what OO and functions were invented to eliminate xD 02:06:17 <\oren\> there are good OO languages 02:06:30 <\oren\> python for instance 02:06:41 you have experimented with the SmallTalk? 02:06:46 (or even Objective-C?) 02:07:31 JavaScript supports real function-oriented programming, and so does Haskell 02:08:04 i like ruby more 02:08:37 myname: BOOOOOOOOO 02:08:40 everything is an object, but in a way that doesn't throw sticks at you if you ignore that 02:09:09 it is like 110% syntax sugar 02:09:17 i observed a large deal of smalltalk influence in the ruby 02:09:20 In JavaScript not everything is object, although everything other than undefined and null can be used as objects 02:09:53 <\oren\> ruby is good too, but it's slow 02:10:04 if ypu ever even need one gem in ruby, you are screwed, though 02:18:58 null is evil 02:19:43 quite 02:20:34 <\oren\> in VB it is called 'Nothing' 02:20:56 <\oren\> If x Is Nothing Then Return Nothing 02:30:55 On Error Resume Next 02:30:57 Yes I have program in VB as well, the null of JavaScript is like Nothing in VB, and I suppose undefined in JavaScript corresponds to Empty in VB, maybe, although it has been some time so I don't quite remember properly 02:39:28 -!- ^v has joined. 02:46:43 -!- hppavilion[1] has quit (Ping timeout: 252 seconds). 03:11:22 myname: What's wrong with gems? 03:34:37 -!- oerjan has quit (Quit: Nite). 03:37:10 I got an error message when using PortAudio, it is exactly the same as shown here: https://github.com/Katee/quietnet/issues/18#issuecomment-40658475 (look below "quietnet# python send.py") 03:38:10 (Sound output nevertheless seems to work) 03:39:54 I found something I can try 03:41:49 I got rid of the first three lines at least 03:48:07 Despite the error message, the sound works. 04:06:41 -!- bender|_ has joined. 04:07:31 <\oren\> I finally got around to intalling mingw and compiling my game for windows 04:09:58 Is 735 a too low frame count? 04:10:01 What game is that? 04:11:32 <\oren\> a shooting game where you look at it in 3d by crossing your eyes 04:12:11 -!- bender|_ has quit (Remote host closed the connection). 04:13:59 -!- bender|_ has joined. 04:14:21 -!- sid123__ has joined. 04:14:35 -!- sid123__ has quit (Read error: Connection reset by peer). 04:15:01 <\oren\> maybe I'll rewrite it in Javascript 04:15:33 <\oren\> or maybe just line-by line translate it from C into Javascript 04:15:46 <\oren\> yah that's a better idea 04:19:58 <\oren\> anyway, the game and the bmp font file it uses are here 04:20:08 <\oren\> http://www.orenwatson.be/autostereo.htm 04:20:16 <\oren\> http://www.orenwatson.be/littlefont2.bmp 04:21:05 <\oren\> containing an ancient version of neoletters 04:33:49 -!- lleu has joined. 04:34:55 <\oren\> `unidecode 渚 04:35:06 [U+FA46 CJK COMPATIBILITY IDEOGRAPH-FA46] 04:43:12 -!- treaki_ has joined. 04:43:17 <\oren\> `u8tbl 0x6e1a 0x6e1a 04:43:18 Segmentation fault 04:43:23 <\oren\> `` u8tbl 0x6e1a 0x6e1a 04:43:24 渚 04:47:03 -!- treaki has quit (Ping timeout: 268 seconds). 04:48:48 -!- XorSwap has quit (Quit: Leaving). 05:31:47 -!- augur has quit (Remote host closed the connection). 05:49:06 -!- augur has joined. 05:52:38 This certainly won't get confusing: http://slbkbs.org/coherent-notations.png 06:01:22 -!- hppavilion[1] has joined. 06:02:45 https://en.wikipedia.org/wiki/Category:Category-theoretic_categories is a fun wikipedia category 06:03:50 Something that'd be fun is a math wiki where the wiki categories are category-theoretic 06:09:45 <\oren\> shachaf: somehow I think that would be easier to read in the orginal LaTeX source code 06:16:29 <\oren\> > 8 * 670 06:16:31 5360 06:52:28 hppavilion[1]: What's the initial object of a wiki category? 06:52:45 prooftechnique: The main page for that category 06:53:10 prooftechnique: What is an "Initial Object"? 06:55:04 An object L such that for any object X there's a unique arrow from L to X. 06:55:27 shachaf: Ah 06:55:32 What objects are initial in the categories I talked about the other day? 06:55:42 shachaf: Let me check 06:56:25 shachaf: Well 0 in category A, off the top of my head 06:56:32 shachaf: (I don't have my notes open yet) 06:56:59 They should have better names. 06:57:08 A should be called N. 06:57:33 B should be called Lin 06:57:36 C should be called Fnord 06:57:56 shachaf: Blackboard Bold N? 06:58:10 Whatever you want. 06:58:23 Fraktur N is prettier 06:58:54 My internet is going REALLY slow :/ 06:59:06 I think I hit the data cap and it hasn't reset yet 07:00:17 shachaf: So composition in ℕ is just the transitive property of ≤, correct? 07:00:30 A naive assumption would be that the wiki category listing page is the initial object, as long as none of the pages are interlinked 07:00:55 Composition is a function. 07:01:00 prooftechnique: Can a category have more than one initial object? 07:01:07 shachaf: Ah 07:01:12 They're isomorphic 07:01:13 shachaf: See, I knew that, but I wasn't sure 07:01:30 The answer is either yes or no depending on what you mean. 07:01:35 I wasn't sure it HAD to be a function 07:01:36 On the other hand, the category listing page is almost certainly a terminal object 07:02:06 Well, it doesn't have to be function. 07:02:13 Some categories are too large for it to be a function. 07:02:16 prooftechnique: Is linking an arrow from the linker or from the linkee? 07:02:40 shachaf: What function is there that is suitable for composition in ℕ? 07:02:44 shachaf: I can't think of any 07:02:46 Depends if you can go the other way, I guess 07:02:55 hppavilion[1]: It composes arrows. 07:03:13 shachaf: OK... 07:03:20 So for example there's an arrow from 2 to 4 and an arrow from 4 to 8. You can compose them to get an arrow from 2 to 8. 07:03:33 It corresponds to transitivity, sure. 07:03:55 OK 07:04:02 shachaf: But is that right? xD 07:04:09 What? 07:04:37 shachaf: What is composition in ℕ? Is it just the transitive property, or is it something else? 07:04:49 I don't know. 07:04:56 shachaf: I'm unsure if that last message is a yes because of the word "corresponds" 07:05:02 I'd say that it's a function and not a property. 07:05:07 OK 07:05:09 But it's substantially the same thing. 07:05:42 shachaf: If it's properties, it works well because x ≤ x, which of course works with the identity morphisms nicely 07:06:44 There's a property: If there's an arrow : A -> B, and there's an arrow : B -> C, then there's an arrow : A -> C 07:07:09 But composition doesn't just tell you that there is an arrow, it's a function that takes those two arrows and gives you the third one. 07:07:10 shachaf: Yes, knew that 07:07:18 shachaf: OK 07:07:27 In this case that's pretty boring because there's only one arrow : A -> C 07:09:24 shachaf: I think my issue is that I have no clue what arrows are supposed to be in ℕ; in sets they're functions, but I can't tell what they are here 07:09:36 s/in/with the objects as/ 07:09:39 They aren't anything. 07:09:43 OK 07:09:50 That's what I've been assuming, but I had to check 07:09:58 They aren't anything in Set either. 07:10:09 shachaf: They /represent/ functions 07:10:27 OK. 07:10:36 Then these arrows represent the relationship <= 07:10:39 shachaf: At least that's what wikipedia told me 07:10:50 shachaf: Yes, that was a given 07:12:28 Anyway the question of what object is initial is easy 07:13:26 shachaf: My money's on 0 07:13:41 Why? 07:14:00 shachaf: Because all natural numbers are greater than or equal to 0 07:14:13 sgtm 07:14:19 What about a terminal object? 07:14:32 shachaf: None; there's always a bigger number 07:14:40