[facebook digest] Status transferred

1. DNF Poster accepted to APLAS.    [2011-10-12 17:10:10 +0100]  [ 4 人說讚！]
2. Dijkstra simply hated pictorial aids.. How did he do Euclidean geometry, then? ↦ E.W. Dijkstra Archive: Written in anger (EWD 696)    [2011-10-12 21:17:19 +0100]
   • Josh Ko ⇒ "[T]he role of the auxiliary variables in proofs of program correctness is very similar to the role of auxiliary lines or points in geometrical proofs, and their invention requires each time a similar form of creativity. This is one of the reasons why I as a computing scientist can only regret that the attention paid to Euclidean geometry in our secondary school curricula has been so drastically reduced during the last decades."
     So he liked Euclidean geometry..
     http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD641.html    [2011-10-12 21:22:01 +0100]
   • Josh Ko ⇒ I can now almost imagine how rude he was..    [2011-10-12 21:27:46 +0100]
   • J************* ⇒ He did it axiomatically, of course. But even EWD admits to the need for creative invention, which (surely) can benefit from pictures?    [2011-10-13 05:43:04 +0100]
3. And he didn't think that functional programs can be reasoned about using algebraic laws is an advantage! So supposedly he would have attacked me fiercely had he read the first paragraph of my transfer dissertation.    [2011-10-12 22:59:42 +0100]
   • Josh Ko ⇒ "And then comes his fundamental complaint "In any case, proofs about programs use the language of logic, not the language of programs. Proofs talk about programs but cannot involve them directly [? EWD] since the axioms of von Neumann languages are so unusable." and he presents as an advantage --without questioning-- that in his system "Algebraic transformations and proofs use the language of the programs themselves, rather than the language of logic, which talks about programs." I am not quite sure what is meant by talking proofs and talking logic. But whereas machines must be able to execute programs (without understanding them), people must be able to understand them (without executing them). These two activities are so utterly disconnected --the one can take place without the other-- that I fail to see the claimed advantage of being so "monolingual". (It may appear perhaps as an advantage to someone who has not grasped yet the postulational method for defining programming language semantics and still tries to understand programs in terms of an underlying computational model. Backus's section "Classification of Models" could be a further indication that he still belongs to that category. If that indication is correct, his objection is less against von Neumann programs than against his own clumsy way of trying to understand them.)"
     
     http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD692.html    [2011-10-12 23:00:51 +0100]
   • Josh Ko ⇒ If I say that axiom postulation has to be based on the way we (mentally) execute programs, he probably would dismiss me by calling me an "integralist".
     
     http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD611.html    [2011-10-12 23:09:30 +0100]
   • Josh Ko ⇒ Eventually I would have to fight against formalism, I think..    [2011-10-12 23:10:04 +0100]
   • J************* ⇒ Nevertheless, the beauty of functional languages is that you can conduct your reasoning in the language, rather than having to step out of it into predicate calculus. If EWD had understood FP, I'm sure he would have seen this as a benefit; we agree that "the axioms of von Neumann languages are unusable".    [2011-10-13 05:47:15 +0100]
   • Josh Ko ⇒ Yes, that's what Backus said, but Dijkstra did not think that this advantage is obvious. Instead, he thought that using two different languages reflects that machine execution and human understanding are "utterly disconnected" activities, and then attacked Backus (rudely) for not knowing the correct (axiomatic) way to understand programs.
     
     I don't think Dijkstra caught the point, but I cannot come up with a counterattack yet..
     
     (I messed up the quote of EWD 692 by adding quotation marks at the beginning and end.. Everything except the first and the last quotation mark is Dijkstra's writing and his quote of Backus's words, so "the axioms of von Neumann languages are unusable" is Backus's comment, which presumably Dijkstra objected.)    [2011-10-13 08:43:21 +0100]
4. I am confused by change-of-base and reindexing.. Are they related? (Or perhaps I should ask: How are they related?)    [2011-10-13 09:25:54 +0100]
5. Changed the bulb of my desk lamp to an LED one. Now it's brightly white (instead of yellow).    [2011-10-13 19:21:36 +0100]
   • W************ ⇒ Do you like white light more than yellow light ?    [2011-10-14 03:35:01 +0100]
   • J******** ⇒ The street lights beside CGU have change to LED. If someone stand under it, the color of their clothes is kind of strange!
     But for reading, LED might be find~~    [2011-10-14 05:28:15 +0100]
6. 如果我可以忍受再一個半月不剪頭髮，我就能回台灣再剪了！    [2011-10-13 19:25:43 +0100]  [ 4 人說讚！]
   • 柯** ⇒ 回台灣我幫你剪~免費唷！    [2011-10-14 08:20:50 +0100]
   • T************** ⇒ 你要帶幾磅來臺灣    [2011-10-15 10:35:31 +0100]
7. There are only 7 posters in APLAS...    [2011-10-14 08:28:49 +0100]
8. A spider in my shoe.. Fortunately it didn't bite me. (I've sent it out of the window.)    [2011-10-14 19:26:34 +0100]  [ 1 人說讚！]
9. Again a particular cold day for matriculation.    [2011-10-15 09:23:12 +0100]
   • L********** ⇒ It is quite warm in Marston.    [2011-10-15 11:15:12 +0100]
10. Jackie 最後的午餐。 ↦ Wall Photos    [2011-10-17 14:16:30 +0100]  [ 3 人說讚！]
    • Y********** ⇒ 是"十月"的最後午餐啦XD    [2011-10-17 14:22:02 +0100]
    • J********** ⇒ :)    [2011-10-17 16:30:15 +0100]
11. "But the point is that fibrations have a great organisational strength. They provide appropriate ways of layering mathematical structures, by making explicit what depends on what." (Jacobs, p70)    [2011-10-17 20:27:53 +0100]
12. Just updated Agda to the latest (development) version and there are now unsolved meta-variables when typechecking OAOAOO.agda..    [2011-10-17 22:20:54 +0100]
13. From: Ralf Hinze
    Subject: Transfer viva: date
    Date: 18 October 2011 07:50:55 GMT+01:00
    To: Josh Ko
    
    Hi Josh,
    
    Tom and I can make it in week 5. Would
    12:00, Tue, 8th Nov, 2011
    suit you?
    
    Cheers, Ralf    [2011-10-18 08:19:15 +0100]  [ 1 人說讚！]
    • Y*********** ⇒ Finally......    [2011-10-18 09:30:57 +0100]
14. Getting lost in the category of fibrations.. (The category Fib of fibrations can be seen as fibred over the category Cat of categories, so the functor Fib -> Cat sending a fibration to its base category is a fibration itself. There should be some size problems we should avoid, but it's not urgent..)    [2011-10-18 09:03:07 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ And Fib has a 2-categorical structure.. That's too much for me now!    [2011-10-18 09:05:52 +0100]
    • Josh Ko ⇒ Skipping to Chapter 2.    [2011-10-18 09:19:33 +0100]
15. The NSC-RS joint grant application was unsuccessful... How I wished that Jeremy could visit Taiwan!    [2011-10-19 07:31:52 +0100]
16. A1 is already small enough for a poster.. A2 would certainly be much too small!    [2011-10-20 11:55:30 +0100]
    • L********* ⇒ 看到A1我還以為是要說Audi A1咧 XDDD    [2011-10-20 12:02:18 +0100]
17. prefixes [] = [ [] ]
    prefixes (x ∷ xs) = [] ∷ map (_∷_ x) (prefixes xs)
    
    The three conses really should have different meanings!    [2011-10-20 15:20:08 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ The meaning of the second one is particularly hard to pin down.    [2011-10-20 15:25:15 +0100]
    • Josh Ko ⇒ (Of course, there is also an implicit one in the first clause.)    [2011-10-20 15:26:22 +0100]
18. Received the payment for doing practicals demonstration for the UNIQ summer school.    [2011-10-21 10:24:37 +0100]
19. Now I think that the structure of my poster is indeed rather too "modernist". Will rework the structure completely.    [2011-10-25 22:35:08 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ But then I'm not so sure if I can do it in a classical way..    [2011-10-25 22:47:58 +0100]
    • Josh Ko ⇒ The current modernist version is no doubt very space-efficient.    [2011-10-25 23:29:48 +0100]
    • Josh Ko ⇒ I'll finish this version anyway, and then see if I can manage to produce a classical version..    [2011-10-25 23:41:43 +0100]
20. Bought Steve Jobs' biography.    [2011-10-26 13:56:28 +0100]  [ 4 人說讚！]
    • L********* ⇒ eBook version?    [2011-10-26 13:58:16 +0100]
    • Josh Ko ⇒ Hardcover.    [2011-10-26 14:01:43 +0100]
21. The "modernist" version. Even though I may not use this one for the conferences, I'd still like to have an A1 sized copy of it. ↦ Wall Photos    [2011-10-26 19:12:20 +0100]  [ 4 人說讚！]
    • H************ ⇒ very creative!!    [2011-10-26 21:48:31 +0100]
    • W********* ⇒ 真是太漂亮惹 請寄給我一份XD    [2011-10-27 00:05:58 +0100]
22. In fact, as I somewhat anticipated, I now feel that the modernist version is fine and hesitate to do a classical version. XD    [2011-10-27 08:47:07 +0100]
23. Found a small error in the code on the poster, which however means that the same error is present in my transfer dissertation..    [2011-10-27 10:39:41 +0100]
    • Josh Ko ⇒ Oh, it's just a typo in an auxiliary definition, so no harm to validity.    [2011-10-27 15:24:36 +0100]
24. Look at the two functions 'forget' and 'initialise' used in my solution to the Dutch National Flag problem: The former is a left inverse to the latter, but not vice versa; the latter is some kind of canonical injection, however, and we do have 'initialise . forget . initialise = initialise'. So there is likely to be an adjunction!    [2011-10-27 22:31:17 +0100]
    • S************ ⇒ A Galois connection?    [2011-10-28 00:45:58 +0100]
    • Josh Ko ⇒ Yes, indeed. (But some day I hope I can find a nontrivial adjunction! (No concrete ideas yet..))    [2011-10-28 08:15:14 +0100]
25. If we recall that types are specifications, then it becomes clear that practically it's not possible (thanks to typechecking) to write wrong (or buggy) programs but only imprecise or wrong specifications.    [2011-10-27 23:14:57 +0100]
26. Brouwer's proof of ¬¬¬p ↔ ¬p.    [2011-10-28 14:03:41 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ Theorem. Absurdity of absurdity of absurdity is equivalent to absurdity.
      
      Proof. When property y follows from property x, then from the absurdity of y follows the absurdity of x. Therefore necessarily, since truth implies absurdity of absurdity, absurdity of absurdity of absurdity implies absurdity.
      
      Conversely, because the correctness of an arbitrary property implies the absurdity of the absurdity of that property, so must absurdity of truth, that is absurdity, imply absurdity of absurdity of absurdity.    [2011-10-28 14:06:31 +0100]
    • Josh Ko ⇒ I simply cannot successfully pronounce three consecutive 'absurdity's..    [2011-10-28 14:07:00 +0100]
27. Really, I'd have liked to say simply "page 2 needs to be rewritten".    [2011-10-28 16:06:43 +0100]
    • 陳** ⇒ 學長加油Q.Q    [2011-10-28 17:09:57 +0100]
28. The abstract I reviewed probably took the author(s) only, say, 30 minutes to finish by copy-and-paste — the writing quality is definitely not good. Anyway, it's just an abstract for a student conference.. The work described looks sound so there is no reason to reject it!    [2011-10-28 21:22:48 +0100]
    • Josh Ko ⇒ Or can I give it a lower grade because I don't think it's well-written?    [2011-10-28 21:26:56 +0100]
    • L************** ⇒ Definitely you can.    [2011-10-28 21:43:42 +0100]
    • Josh Ko ⇒ I finally decided to still give it an accept but mentioned in the "remarks for the programme committee" section that I'd have given it a weak accept had writing quality been taken into consideration seriously.    [2011-10-28 21:50:48 +0100]
    • Y************* ⇒ So right now, you are a reviewer and have the authority to reject a paper. Oh my god, it sounds so cool, my friend.    [2011-10-29 00:12:20 +0100]
    • Josh Ko ⇒ It's just a student conference held in our department, so there's no substantial influence.    [2011-10-29 00:31:32 +0100]
    • Y************* ⇒ All right but it still cool.    [2011-10-30 01:56:50 +0100]
29. The Barcarolle simply has an amazingly golden colour..    [2011-10-29 13:02:23 +0100]  [ 2 人說讚！]
30. It seems that Dijkstra had a bad influence on me: I now tend to make ruder arguments. Fortunately I don't need to read his work intensively now as I have had a reasonable understanding of his philosophy.    [2011-10-30 19:09:41 +0100]  [ 1 人說讚！]
31. "Nobody cares."    [2011-10-30 21:52:13 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ http://sneezy.cs.nott.ac.uk/darcs/DTP08/slides/Lennart.pdf    [2011-10-30 21:52:56 +0100]
32. 不經意與此文重逢。 ↦ http://www.hgjh.hlc.edu.tw/~chenli/chopin.htm    [2011-10-30 22:41:00 +0100]
33. There's no way to do implicit existential quantification in Agda now, I believe? (I wish to use a (Σ ℕ (Vec A)) as if it's just a (Vec A n) for some n.)    [2011-10-31 10:27:08 +0100]
    • Josh Ko ⇒ (without having to write trivial constructors and projections.)    [2011-10-31 10:31:43 +0100]
34. Argh, Tarjan's Strachey lecture will be in December..    [2011-11-01 09:10:17 +0100]
    • L********** ⇒ Will be away in a conference that day...    [2011-11-01 11:26:41 +0100]
    • J********** ⇒ Great! I will be arriving in the morning of the 8th... Thx for the info:-)    [2011-11-01 13:54:10 +0100]
35. I have not been able to receive emails from Mail2000 smoothly ever since I upgraded to Lion. (I have to dismiss "password rejected" dialog boxes every time Mail tries to login.) After observing the discussions about this problem on the Apple forum for a long time, I decided that it might well be a server-side problem and wrote to Mail2000, attaching two particular messages from the forum that might be helpful.    [2011-11-02 12:26:11 +0100]
    • Josh Ko ⇒ Their reply was a long list of forum entries and suggested that I switch to, e.g., Thunderbird while waiting for Apple to solve the problem.    [2011-11-02 12:26:20 +0100]
    • Josh Ko ⇒ I was a bit annoyed. Today I used telnet to connect to the IMAP server and discovered that the same authentication process had to be repeated twice to login, which just didn't make sense. So I wrote to them again, attaching the telnet log and this time asking explicitly how Apple violates RFC in this case.    [2011-11-02 12:29:07 +0100]
    • Josh Ko ⇒ Really, if they cannot give me a satisfactory answer this time, there doesn't seem to be any point paying for their service anymore.    [2011-11-02 12:31:50 +0100]
36. > I am confused by change-of-base and reindexing.. Are they related? (Or perhaps I should ask: How are they related?)
    
    Right, change-of-base is reindexing in the category of fibrations.    [2011-11-03 09:59:52 +0100]  [ 1 人說讚！]
37. Now Mail2000 seems to be interested in solving the problem, but not quite at the right level yet. (They recommended that I change the settings in Mail.) I pointed out that this is no longer a problem with Mail but with how the server responds to the AUTHENTICATE command since the experiment results were produced by telnet/openssl, and asked them to look at the case again.    [2011-11-03 11:35:04 +0100]
    • Josh Ko ⇒ I thought the telnet session I sent them should be a quite obvious hint to them (who are supposed to be experts) about what goes wrong.    [2011-11-03 11:37:22 +0100]
38. "A category C has a terminal object if and only if the unique functor C -> 1 from C to the terminal category 1 has a right adjoint." Never thought of this..    [2011-11-04 10:36:55 +0100]
    • L************** ⇒ Now, you can think of universal and existential quantifiers in this way...    [2011-11-04 10:46:02 +0100]
    • Josh Ko ⇒ As right/left adjoints of a weakening functor?    [2011-11-04 10:49:25 +0100]
    • L************** ⇒ I overlooked your message. It seems different to what I thought. This is stated in the second section of adjunction in MacLane's book...    [2011-11-04 11:03:28 +0100]
    • Josh Ko ⇒ As a special case of limits/colimits expressed as right/left adjoints of the diagonal functor.    [2011-11-04 11:16:28 +0100]
39. Simplified version of the DNF poster. The text size is more readable, but now it would be very difficult (if possible at all) for the reader to understand the poster by him/herself since the explanations (among other things) are left out. ↦ Wall Photos    [2011-11-05 01:13:45 +0100]  [ 4 人說讚！]
    • L********** ⇒ I would probably prefer the "unsimplified" version    [2011-11-05 03:31:25 +0100]
    • Josh Ko ⇒ I like that one too, but it can't be denied that the texts are too small - it works ok for one or two people but less effectively for more than three, I guess.    [2011-11-05 10:05:55 +0100]
    • Josh Ko ⇒ I might print both of them out, however. XD    [2011-11-05 10:07:33 +0100]
40. While Dijkstra complained that Hilbert's formalism (and Leibniz's dream) was ignored by the maths community, I wonder how he could possibly ignore Gödel's incompleteness theorems?
    
    (I would say that he had his own "reality distortion field".) ↦ E.W.Dijkstra Archive: Under the spell of Leibniz's Dream (EWD 1298)    [2011-11-07 23:08:24 +0100]  [ 1 人說讚！]
    • J******************* ⇒ But the Reality Distortion Field usually works on others lol    [2011-11-07 23:59:09 +0100]
41. Hm, transfer viva is apparently very daunting. The assessors' questions sounded not to be in English even to a (presumably) native speaker!
    http://clamorousvoice.wordpress.com/2011/06/01/prs-dphil-oxford-english-transfer-viva/ ↦ PRS to DPhil: the transfer viva    [2011-11-08 11:24:11 +0100]
    • Josh Ko ⇒ And if you google for "transfer viva", the first entry is this: http://www.postgraduateforum.com/threadViewer.aspx?TID=9368    [2011-11-08 11:25:04 +0100]
    • Josh Ko ⇒ Jeremy was right about the result. XD    [2011-11-08 13:54:50 +0100]
42. Alright, I think I will shortly be a proper DPhil student!    [2011-11-08 14:03:18 +0100]  [ 4 人說讚！]
    • Josh Ko ⇒ (Just passed my transfer viva.)    [2011-11-08 14:04:04 +0100]
    • A*********** ⇒ congrats@    [2011-11-08 14:05:16 +0100]
    • G*************** ⇒ congratulations    [2011-11-08 14:44:29 +0100]
    • D******** ⇒ 恭喜啦！！    [2011-11-08 14:55:26 +0100]
    • M************ ⇒ cool!!!!!!!!    [2011-11-08 15:32:50 +0100]
43. I presented the internalist position, although Ralf and Tom were not convinced. I believe that their job at this stage is only to check that I have something to say, so they didn't push it further, but I will certainly need to offer a complete argument in the thesis.    [2011-11-08 14:41:03 +0100]
    • Josh Ko ⇒ That is, I really cannot take internalism for granted - its validity will have to be justified in the thesis.    [2011-11-08 14:43:30 +0100]
44. My verbal arguments tend to be rather unstructured. This weakness will have to be taken care of..    [2011-11-08 21:48:50 +0100]

--
It is really about time to write a review of the previous academic year now that I've transferred status..