2011/04/09

[facebook digest] 返台六週

  1. Just a title and another line "Don Knuth (Stanford)". Is it real?! ↦ Oxford University Computing Laboratory: Long and skinny knight's tours    [2011-02-14 11:03:49 +0000]
    • Josh Ko ⇒ So close! But he is so intimidating... XD    [2011-02-14 13:02:19 +0000]
    • J************* ⇒ He's really quite friendly...    [2011-02-14 19:21:22 +0000]
  2. Perhaps Lansoprazole works better for me. Even if it is not the case, I still feel much better today anyway.    [2011-02-14 13:57:38 +0000]
  3. Knuth REALLY knows how to have fun!    [2011-02-15 18:09:46 +0000]
    • Josh Ko ⇒ His grasp of concrete mathematics is so clear and natural - certainly a real artist.    [2011-02-15 18:39:13 +0000]
    • Josh Ko ⇒ Concretely, he went through Chapter 42 of one of his latest books, Selected Papers on Fun and Games.
      http://www-cs-faculty.stanford.edu/~uno/fg.html    [2011-02-15 19:40:32 +0000]
    • L********** ⇒ You seemed to have great fun from his talk too!    [2011-02-15 20:30:54 +0000]
    • Josh Ko ⇒ I did, for sure!    [2011-02-15 21:07:25 +0000]
    • L********** ⇒ I can tell that your understanding of concrete maths is very concrete, dont you think?    [2011-02-16 00:22:00 +0000]
    • W************ ⇒ Although I can get the mean of concrete mathematics, i think it's very interesting for the grasp.    [2011-02-16 01:02:40 +0000]
    • Josh Ko ⇒ My understanding? No, I am not skilled in concrete math (specifically, all those techniques recorded in the book with the name). But I appreciate the concrete flavour in Knuth's work, and I am awed by how concrete he can get to.    [2011-02-16 08:17:54 +0000]
    • L********** ⇒ I see, Don is indeed quite passionated in concrete maths.    [2011-02-16 10:54:22 +0000]
  4. I need to make a major change to the direction of my essay... Otherwise it's bound to get too long and less focused.    [2011-02-17 11:38:19 +0000]
    • Josh Ko ⇒ I estimate the original plan can lead to a 50-page essay...    [2011-02-17 11:54:37 +0000]
    • C************ ⇒ Relax~There're three more years !haha    [2011-02-17 14:55:59 +0000]
    • Josh Ko ⇒ This essay, however, is due at the end of this term, merely 23 days away...    [2011-02-17 15:39:05 +0000]
    • S************ ⇒ Is that your transferring dissertation?    [2011-02-18 00:28:08 +0000]
    • Josh Ko ⇒ No, it's not, but it may form a part of the dissertation.    [2011-02-18 07:45:47 +0000]
  5. 舉頭忽見，柔墨輕潑月暈渲，今夜又共嬋娟。    [2011-02-17 21:00:54 +0000]
  6. 看起來很容易操作的食譜，可以當新購（二手）電鍋的處女作。 ↦ 【反媽簡易食譜】香噴噴的 魯肉飯..省錢方便又簡單的電鍋料理來囉.. @ 反嗑為主 反推有理 :: 痞客邦 PIXNET ::    [2011-02-18 20:15:11 +0000]
    • J******** ⇒ 我也常做類似的
      簡單的豬肉醃一下放入電鍋
      飯好肉也好了，之後再炒個菜快速方便    [2011-02-19 00:30:44 +0000]
  7. 又以出清價向 Mark 收購一個完整版的大同電鍋，順帶拿了不少保鮮盒和幾件餐具，可料想日後的菜色應該會愈來愈多。需要保鮮盒的可以找我拿幾個，我一個人用不了那麼多⋯    [2011-02-21 18:03:55 +0000]
    • 翁** ⇒ 原來牛津是餐飲大學XDDD    [2011-02-22 00:46:00 +0000]
    • W************ ⇒ 民以食為天啊XD 自己動手比較便宜咩~    [2011-02-22 09:15:30 +0000]
  8. 魯肉做成蒸肉，單吃還不錯，配麵就不夠鹹了。肉應該要先醃一下顏色才會比較深？ ↦ http://www.facebook.com/photo.php?fbid=168359006549978&set=a.126799950705884.40277.100001276392360    [2011-02-22 13:09:47 +0000]
    • W************ ⇒ 應該不用吧，是要不要再煮久一點 ?    [2011-02-23 03:17:53 +0000]
    • J******** ⇒ 麵是指湯麵嗎？通常湯麵配抄過的料會比較香歐！
      配飯瓜子肉是個不錯的選擇(英國有華人超市吧！？)    [2011-02-23 05:04:50 +0000]
    • E******** ⇒ 醬油多一點，小火悶久一點，應該不用醃吧    [2011-02-23 12:27:41 +0000]
  9. I need a good example for with-matching...    [2011-02-23 16:01:11 +0000]
    • S************ ⇒ Are you teaching someone Agda?    [2011-02-23 17:00:44 +0000]
    • L************** ⇒ (mod n) ?    [2011-02-23 17:03:22 +0000]
    • Josh Ko ⇒ @scm: Not exactly. I am describing dependent pattern matching in my essay.
      @LT: That's a view, right? I was seeking something more exciting but now I think I will use a view...    [2011-02-23 19:02:24 +0000]
    • Josh Ko ⇒ Small examples are boring, while interesting examples are too big...    [2011-02-23 19:33:41 +0000]
  10. Perhaps I have never been really aware that I have given up playing the piano seriously, in the sense that it is almost for sure that I will never succeed in playing the Polonaise-Fantaisie, or Ballades No 1 & 4, because I will never be able to reach the demanded technical level nor allocate much time for them. (There is a mutual implication between the two reasons.) The best hope is that the accumulated time I spend on them in my whole life will lead to an acceptable approximation. That's going to be one of the justifications for my exclusive interest in Chopin's works. ↦ http://www.facebook.com/photo.php?fbid=168714059847806&set=a.126799950705884.40277.100001276392360    [2011-02-23 23:03:03 +0000]
  11. I have felt the ulcer again since last night. So far it has been relatively mild, but I have no idea whether it will become worse or go away quickly. (This time I had 4 days of peace, from Sunday to Wednesday.)    [2011-02-24 10:32:12 +0000]
  12. Prepared quite some steamed rice with vegetables with my electric cooker. It tastes ok but I don't have appetite...    [2011-02-24 18:10:32 +0000]
  13. 肚子痛房間就一團亂⋯    [2011-02-24 20:19:39 +0000]
  14. feel worse today...    [2011-02-25 18:31:25 +0000]
    • W************ ⇒ It sounds not good …    [2011-02-26 09:01:58 +0000]
  15. 這兩天決定要不要回台灣吞胃鏡⋯    [2011-02-25 22:36:19 +0000]
    • F********* ⇒ Josh 千萬要保重!!! 有需要任何幫忙的話, 隨時打電話給我! Any time!!!    [2011-02-25 22:54:39 +0000]
    • T************** ⇒ 你要來台大醫院嗎    [2011-02-26 00:26:47 +0000]
    • T************** ⇒ 我比較好奇你喝urea的時候有停用PPI嗎？    [2011-02-26 00:31:13 +0000]
    • 陳** ⇒ 學長保重呀@@    [2011-02-26 00:46:43 +0000]
    • Y************* ⇒ 回來呀! 這樣就可以去找你了    [2011-02-26 04:27:22 +0000]
    • Josh Ko ⇒ @Frank: Thanks a lot! 希望能快點再和你們一塊晨走呀⋯
      @TS: 大概不會去台大，現在待台北不太方便。（你有特別推薦的理由？）做呼氣測試前醫生確實沒叫我停藥，我後來看到有一種標榜不用特別停藥的但我也不是吃那種，所以開始對他不太有信心⋯我現在比較擔心療程長短，不知道如果回台灣的話得待多久？
      @小朋友：謝啦！考試結果還 OK?
      @YT: 唉，聽說你六月才回去？我現在是希望頂多一個半月可以回英國啦，所以應該待不到六月。（如果待到六月就是休學了⋯）    [2011-02-26 06:23:46 +0000]
    • W************ ⇒ 嗯 ... 不知道要說什麼，反正，身體優先。    [2011-02-26 09:01:32 +0000]
    • L************** ⇒ 請保重！養病養好了再繼續會比較好 ...    [2011-02-26 12:18:42 +0000]
    • 王** ⇒ take good care    [2011-02-26 13:52:21 +0000]
    • T************** ⇒ 胃鏡頂多只要半小時，你可以看完就回彰化，又不是要開刀...
      台大有幾個醫生我覺得不錯，不然施銘gay應該可以有好的人選建議，
      應該是兩個星期左右吧 然後停藥 然後再測 失敗再換別的藥 再測

      while JoshKo.getUlcer == 1
      {
      JoshKo.takeExam()
      JoshKo.takeMed()
      JoshKo.stopMed()}
      }    [2011-02-26 14:56:22 +0000]
    • Josh Ko ⇒ 我媽剛才已經在彰基找比較熟的醫生約好星期四做胃鏡，明天打電話給旅行社，希望星期二回去。    [2011-02-26 14:59:29 +0000]
    • T************** ⇒ 好禿 我下下星期會回彰化 再去看你    [2011-02-26 15:01:38 +0000]
    • S************ ⇒ 希望早日康復！如果需要來台北的話可以住我這邊。    [2011-02-27 01:12:50 +0000]
    • Y************* ⇒ So you are in Taiwan now? Oh ~ no    [2011-02-27 05:27:04 +0000]
    • Josh Ko ⇒ @scm: Thanks! 治療順利的話，還可以去聽一下你的課耶！
      @YT: 還沒但快嘍。如果我之後進度趕得回來的話，說不定九月可以有理由再回去勒！    [2011-02-27 18:15:06 +0000]
  16. even worse today, unbelievable...    [2011-02-26 19:55:51 +0000]
    • T************** ⇒ 可以好的，看我現在這樣子就知道了XD
      不過你應該可以體會到我那時候的絕望了XD    [2011-02-27 03:00:55 +0000]
    • T************** ⇒ 你媽說要買軟便劑，我建議可以買MgO (magnesium oxide)，他也是鹼性的，附帶中和胃酸。我不確定會不會和PPI有交互作用，你可以問問看施銘gay    [2011-02-27 03:27:13 +0000]
    • T************** ⇒ 你可以變成餅乾怪獸，肚子比較不會痛    [2011-02-27 03:36:19 +0000]
  17. 倉皇準備逃回台灣，雖然狼狽不堪但也是段經歷。 ↦ Pollini plays Chopin Nocturne op.32 no.2    [2011-02-27 11:18:51 +0000]
    • P************* ⇒ 祝福你    [2011-02-27 14:44:14 +0000]
    • J******************* ⇒ 身體是革命的本錢! PHD慢慢讀就可以了!    [2011-02-27 14:45:18 +0000]
  18. Flights confirmed (and X70 bus tickets booked):
    21:00, 1 Mar, LHR T4 - CI070 - 18:35, 2 Mar, TPE T1
    09:25, 12 Apr, TPE T1 - CI069 - 17:05, 12 Apr, LHR T4    [2011-02-27 14:52:14 +0000]
  19. GSS report done; don't forget the Census.    [2011-02-27 15:23:48 +0000]
  20. It cannot be related to what I am thinking?! My idea about "generic lookup with ornaments" has begun to take shape, but a moment ago when I tried to compare my (still rough) idea with the diamond modality and its associated find operation, I started to feel something in my stomach.    [2011-02-28 20:21:28 +0000]
    • S************ ⇒ At least there is now a clue worth following..    [2011-03-01 07:21:36 +0000]
  21. Ever since I played in Chopin Nocturne Night I have never touched the piano again, except for the digital piano which is now owned by Liang-Ting. My original plan (formulated before Christmas) was to play daily! It is obvious how seriously the plan was disrupted.    [2011-02-28 21:04:39 +0000]
  22. Position this term.
    (http://gaogaigar.wikia.com/wiki/Protect_Shade) ↦ http://www.facebook.com/photo.php?fbid=169907736395105&set=a.126799950705884.40277.100001276392360    [2011-02-28 21:14:10 +0000]
  23. 撤電腦、拔插頭、出發！    [2011-03-01 14:32:43 +0000]
    • J******************* ⇒ welcome back to Taiwan    [2011-03-01 14:55:07 +0000]
  24. Checked in. Depart in three and a half hours.    [2011-03-01 17:29:35 +0000]
  25. No free wifi at Heathrow. Sigh, even Taoyuan airport provides that!    [2011-03-01 18:49:22 +0000]
  26. Now on board the aircraft. Turning off the mobile.    [2011-03-01 20:27:35 +0000]
  27. Finally arrived at home.    [2011-03-02 14:10:21 +0000]
    • Josh Ko ⇒ Tony Hoare's lecture(s) regretfully missed.    [2011-03-02 14:14:23 +0000]
    • J********** ⇒ I'm going there tonight @ Wolfson and tomorrow @ comlab!    [2011-03-03 15:28:59 +0000]
    • Josh Ko ⇒ Please give me a summary of what he says afterwards!    [2011-03-03 20:05:02 +0000]
  28. It seems the generic lookup problem has been satisfactorily solved by generic modality. I need to find another story to tell.    [2011-03-03 13:27:14 +0000]
  29. Just came up with a more ambitious idea than generic lookup, which looks promising in terms of potential, but I'm not sure how hard it will be to develop the idea yet. And safe indexing for lists can be a motivating example for it if it works.    [2011-03-03 20:28:22 +0000]
  30. Ornamental-algebraic ornaments turn out to be very worth investigating!    [2011-03-04 00:53:56 +0000]
    • Josh Ko ⇒ Wished I were at Oxford...    [2011-03-04 00:56:02 +0000]
    • 翁** ⇒ 可以寫中文嘛，應該入境隨俗喔XDD    [2011-03-04 01:03:37 +0000]
    • Josh Ko ⇒ 「結果裝飾代數式的裝飾很值得研究一番！」
      不要翻譯比較好啊⋯ XD    [2011-03-04 01:52:38 +0000]
    • 翁** ⇒ 恩，太學術的東西還是英文好!醫生看的如何?    [2011-03-04 01:55:22 +0000]
    • Josh Ko ⇒ 胃鏡照起來還滿正常的，現在感覺也正常，但之前那些痛就得不到完善的解釋。再觀察幾天看看。    [2011-03-04 01:57:28 +0000]
    • 翁** ⇒ 恩，看來沒問題，那可以吃頂唐鋒了XD    [2011-03-04 02:00:33 +0000]
    • Josh Ko ⇒ 欸，吃那個好飽好痛苦喔，不能吃個皇上皇就好嗎？XD    [2011-03-04 02:01:22 +0000]
    • 翁** ⇒ XD可是我覺得吃燒臘飯很普通耶    [2011-03-04 02:02:10 +0000]
    • Josh Ko ⇒ 一點也不⋯ 我好想念他的燒肉飯 XD。    [2011-03-04 02:02:53 +0000]
    • W************ ⇒ 愛家啦    [2011-03-04 14:21:33 +0000]
  31. Time to consider composition of ornaments, starting from the special (but already useful) case where one of the two ornaments is algebraic.    [2011-03-04 02:21:45 +0000]
  32. Why, ornamental-algebraic ornaments correspond perfectly to realisability! Why does "Vec A n" say that the natural number n realises List A? Because to expand n to a list of A's, we need to supply n elements of A, which is a vector of length n!    [2011-03-04 02:28:38 +0000]
    • Josh Ko ⇒ And this explanation works for all the examples I have in hand: Nat to Fin, Nat to List, List to Vec, and List to SortedList.    [2011-03-04 02:31:51 +0000]
    • Josh Ko ⇒ And we can prove that a realiser of some type A and a corresponding realisability proof can be integrated into a proof of A, echoing our intuition about realisability.    [2011-03-04 02:34:20 +0000]
    • Josh Ko ⇒ Conversely, we can of course separate a proof of A into a realiser and a realisability proof. Since the realiser is of a simpler type and the realisability predicate is one on the realisers, which are of the simpler type, we essentially factored a complex type into simpler ingredients. The potential for compositionality then shows up.    [2011-03-04 02:38:57 +0000]
  33. I think I now have a cute story to tell!    [2011-03-04 14:41:39 +0000]
    • Josh Ko ⇒ Bad timing. I really should have been in Oxford now.    [2011-03-04 14:56:36 +0000]
    • J************* ⇒ Feel free to tell me by email...    [2011-03-04 18:42:16 +0000]
    • Josh Ko ⇒ Just did that!    [2011-03-04 23:39:56 +0000]
  34. Everything just fits together and works!    [2011-03-04 20:39:46 +0000]
  35. My idea is more accurately described as "fusing an algebra into an ornament" instead of "fusing two ornaments where one of them is algebraic". The new description subsumes the original notion of algebraic ornaments, which is fusing an algebra into the identity ornament.    [2011-03-05 12:39:08 +0000]
    • Josh Ko ⇒ The algebras then form some kind of structure (with weak properties, I guess) which acts on the ornaments.    [2011-03-05 12:42:54 +0000]
    • Josh Ko ⇒ Not sure whether we should get rid of the original notion of algebraic ornaments.    [2011-03-05 12:47:25 +0000]
    • Josh Ko ⇒ The subsumption cannot be proved in Agda due to lack of extensionality.    [2011-03-05 13:31:17 +0000]
  36. A possible title might be "Ornamental algebraic ornaments, algebraic ornament ornaments". XD    [2011-03-05 15:55:16 +0000]
  37. Need to do the proofs on paper first. It is hopeless to try to work out the proofs directly in Agda...    [2011-03-05 23:32:03 +0000]
  38. Note on ornamental algebraic ornaments and algebraic ornament ornaments. (The names can be changed!) ↦ http://sites.google.com/site/joshkos/OAOAOO_note.pdf    [2011-03-06 13:19:53 +0000]
  39. Implementation is nontrivial.    [2011-03-06 23:12:45 +0000]
    • Josh Ko ⇒ Because doing datatype-generic induction is painful...    [2011-03-06 23:37:46 +0000]
  40. As suspected, the remember function and the recomputation lemma for algebraic ornaments are subsumed by the general facilities of the realisability framework.    [2011-03-06 23:29:30 +0000]
  41. 6 goals, 6 inductions. Pretty scary...    [2011-03-07 00:37:05 +0000]
  42. 有史以來做過最難的 induction，幾無頭緒，都快哭出來啦！    [2011-03-07 03:40:52 +0000]
    • Josh Ko ⇒ 算是卡住了。也是該卡住，不然刷刷刷一下寫完不就沒什麼價值！    [2011-03-07 03:42:47 +0000]
    • W************ ⇒ ... 加油 !!    [2011-03-07 04:14:26 +0000]
  43. There does not seem to be particular reason not to directly consider fusion of arbitrary ornaments.    [2011-03-07 13:11:22 +0000]
    • Josh Ko ⇒ Not very straightforward after a quick experiment. Let's stick to algebraic ornament ornaments for now.    [2011-03-07 13:29:16 +0000]
  44. Oops, fusion of arbitrary ornaments is successfully defined, which is more complex than algebraic ornament ornaments, of course. If the former really works then there's no point dealing with the latter anymore.    [2011-03-07 17:40:08 +0000]
    • Josh Ko ⇒ The good thing is that we can get rid of the awkward name "algebraic ornament ornaments". XD    [2011-03-07 17:43:17 +0000]
    • Josh Ko ⇒ Hmm... I like the word "composition" more than "fusion".    [2011-03-07 17:45:52 +0000]
    • Josh Ko ⇒ I anticipate there will be significant difficulties with substitution of equal indices...    [2011-03-07 17:58:46 +0000]
    • Josh Ko ⇒ My gosh, I just noticed that the new index set is actually a pullback!    [2011-03-07 18:03:47 +0000]
  45. Soon heading for Taipei and will try to sell the story to Shin in the afternoon.    [2011-03-07 22:50:12 +0000]
  46. Finally succeeded in my first datatype-generic induction! (More to come...)    [2011-03-09 02:55:17 +0000]
    • L********** ⇒ Any interesting result?    [2011-03-09 20:06:20 +0000]
    • Josh Ko ⇒ I think so, if I can succeed in implementing the ideas (which look plausible)!    [2011-03-09 22:56:05 +0000]
    • L********** ⇒ En...We all can not avoid coding at some point...    [2011-03-10 23:18:15 +0000]
  47. It is really absolutely necessary to record my own playing so defects can be identified and corrected afterwards. Keep in mind to sing and breath elegantly when playing Chopin!    [2011-03-10 09:08:03 +0000]
  48. Once again the goal type is too long to be pasted on fb as a status update. The length is actually not surprising; the problem is I don't know how to abstract variables to make induction go through.    [2011-03-11 08:34:55 +0000]
  49. If I just give up and postulate extensionality...?    [2011-03-11 11:27:15 +0000]
    • Josh Ko ⇒ Then we won't have practically working examples. That's bad.    [2011-03-11 11:28:50 +0000]
  50. Goal:
    erase O
    (mapFold ⌊ O ⌋ ⌊ O ⌋ (ornAlg O)
    (erase (algOrn ⌊ O ⌋ (φ ∘ erase O))
    (mapFold ⌊ algOrn ⌊ O ⌋ (φ ∘ erase O) ⌋
    ⌊ algOrn ⌊ O ⌋ (φ ∘ erase O) ⌋
    (ornAlg (algOrn ⌊ O ⌋ (φ ∘ erase O)))
    (isoF₂ O φ
    (mapFold ⌊ algOrn' O φ ⌋ ⌊ algOrn' O φ ⌋
    (<_> ∘ isoF₂ O φ) ds)))))
    ≡
    erase (algOrn' O φ)
    (mapFold ⌊ algOrn' O φ ⌋ ⌊ algOrn' O φ ⌋ (ornAlg (algOrn' O φ)) ds)    [2011-03-12 10:30:42 +0000]
    • Josh Ko ⇒ Still finding a way to suitably generalise this type.    [2011-03-12 10:31:28 +0000]
    • Y************* ⇒ what's the hell?    [2011-03-13 04:52:35 +0000]
    • Josh Ko ⇒ You're right, it's hell! Therefore I am trying to bypass this mess.    [2011-03-13 04:59:47 +0000]
    • Y************* ⇒ Ha! I know that's the devil you are facing now. My point is what's that? Is it a kind of mathematical issue?    [2011-03-13 05:09:51 +0000]
    • Josh Ko ⇒ It's some proposition I am trying to prove. You can see that there is a three-line equality sign in the middle, so what I'm trying to prove is that two things are equal, which have long and scary descriptions.    [2011-03-13 05:12:35 +0000]
    • T************** ⇒ ⌊ O ⌋ 感覺很強壯
      Orn' 小狗    [2011-03-14 10:15:02 +0000]
  51. Perhaps try to perform fold fusion?!    [2011-03-12 12:00:24 +0000]
  52. Even just stating the fusion theorem is problematic...    [2011-03-12 22:46:36 +0000]
  53. Fusion theorem stated and proved (with an explicit application of subst)!    [2011-03-13 03:58:01 +0000]
  54. So now the hard work falls on proving the fusion conditions, which is still far from trivial.    [2011-03-13 06:01:06 +0000]
  55. Two ways to go: keeping staring at the fusion condition and trying to disentangle the parameters, or postulating extensionality and finishing the coding quickly, at the expense of losing a working implementation.    [2011-03-14 00:25:03 +0000]
  56. Un oh, the need to disentangle the parameters is not eliminated by postulating extensionality...    [2011-03-14 01:03:47 +0000]
  57. Good luck to Japan... (Just before the first ICFP ever held in Asia... sigh.)    [2011-03-15 10:42:55 +0000]
    • Josh Ko ⇒ Pollini plays Etude Op 25 No 12 (Ocean): http://www.youtube.com/watch?v=5M2PO4f5Y7k    [2011-03-15 10:45:55 +0000]
  58. Bought this from iTunes Store UK. A good recording to own. ↦ Fryderyk Chopin - The Complete Works of Fryderyk Chopin on historical instruments - NIFCCD 007. 24 E    [2011-03-15 11:55:05 +0000]
  59. After (finally) recognising the recursion pattern as accumulating parameters, now it seems I am on a right track to a suitable generalisation.    [2011-03-16 00:39:15 +0000]
    • Josh Ko ⇒ That also means I need to invent a nice and useful loop invariant...    [2011-03-16 00:48:33 +0000]
  60. Stomachache reappeared yesterday but has been relieving, indicating the real cause may have been identified. Meanwhile I am still having trouble proving the datatype-generic fusion condition. Perhaps I should start writing the easy part first.    [2011-03-18 08:48:54 +0000]
  61. I didn't know Robert Harper's writing is so "spicy"! ↦ Existential Type    [2011-03-19 00:32:03 +0000]
    • L*********** ⇒ Waiting for more posts, hahaha..    [2011-03-19 15:55:07 +0000]
  62. 默哀⋯ "We have now had the official clearance from Council that the department can change its name to The Department of Computer Science as of the 1st June 2011."    [2011-03-24 00:09:04 +0000]
  63. Unbelievable! Suddenly I managed to come up with a nice and working loop invariant and the proof of the fusion condition just went through effortlessly! (Three more to go...)    [2011-03-24 01:07:59 +0000]
    • L************** ⇒ That's really mathematical!    [2011-03-24 01:09:25 +0000]
    • Josh Ko ⇒ And then I realised I proved the wrong thing. That's also a common phenomenon, I think? XD    [2011-03-24 01:14:55 +0000]
    • L************** ⇒ Sometimes you find the right proof from a wrong one. :-)    [2011-03-24 01:21:02 +0000]
  64. Impressive! ↦ GaoGaiGar - Television Tropes & Idioms    [2011-03-24 05:49:47 +0000]
  65. Reduced the fusion condition to some kind of parametricity. Hope it will be easier to see how to melt and expand the structures involved.    [2011-03-26 14:21:53 +0000]
    • Josh Ko ⇒ Turns out to be the right direction. Now I can do induction without worrying about "parameter entanglement".    [2011-03-26 15:40:20 +0000]
    • Josh Ko ⇒ I believe I am close to my first projection.    [2011-03-26 16:04:39 +0000]
  66. First projection typechecked! It took me quite a few days to realise I needed to break things into pieces finer than I had anticipated. I think it was due to lack of experience. But well, now I have gained the experience. XD    [2011-03-27 02:52:41 +0000]
    • Josh Ko ⇒ Second projection should be similar. What's more interesting (meaning requiring some more work) is integration, which should be able to be tackled in time because we're looking at a special case (namely algebraic ornament-ornaments).    [2011-03-27 02:59:27 +0000]
    • Josh Ko ⇒ The code will require substantial tidy-up afterwards...    [2011-03-27 03:09:09 +0000]
  67. Second projection produced in minutes by copy-n-paste.    [2011-03-27 05:41:30 +0000]
  68. Integration (with six successive rewrites) also typechecked! Only the examples are left, which are easy.    [2011-03-27 12:52:55 +0000]
    • Josh Ko ⇒ And the paper, of course.    [2011-03-27 13:10:33 +0000]
  69. The solution looks quite straightforward - after it is found...    [2011-03-27 13:48:45 +0000]
    • L********** ⇒ This happens from time to time    [2011-03-29 04:35:44 +0000]
  70. I am not writing a pearl after all, so let's stick to the standard form, beginning with a standard introduction...    [2011-03-29 15:45:56 +0000]
  71. Suddenly not very sure how to sell my discovery...    [2011-03-30 08:47:20 +0000]
    • J******************* ⇒ 包裝也是一門技術阿XD    [2011-03-30 08:48:38 +0000]
    • 王** ⇒ 我發現寫科學文章腦中最長閃過的念頭就是如何自圓其說    [2011-03-30 10:06:04 +0000]
    • L********** ⇒ Does it wok well in practice?    [2011-03-30 23:10:45 +0000]
    • Josh Ko ⇒ It is a solution to a practical problem and works well, I think, but what is the exact problem that it solves I am still not very sure (but not far away from it).    [2011-03-31 07:16:55 +0000]
    • S************ ⇒ Reminds me of the old 42 joke -- it's an answer taking millions of years to compute. However, the question was lost.    [2011-04-01 01:37:06 +0000]
    • S************ ⇒ Answer to the Ultimate Question of Life, the Universe, and Everything (42)    [2011-04-01 01:37:08 +0000]
  72. 寫得又慢又爛，真討厭⋯ 不過還是只能先寫個大概再修了。    [2011-03-31 05:58:16 +0000]
    • 翁** ⇒ 果然是太久沒寫作文了XDD    [2011-03-31 06:04:36 +0000]
    • Josh Ko ⇒ 應該叫學弟每個月交中英文論說文各一篇！XD    [2011-03-31 06:05:58 +0000]
    • 翁** ⇒ ......中文就要寫不出來了，還寫英文哩，我看辦公室也沒人會改XD    [2011-03-31 06:06:47 +0000]
    • Josh Ko ⇒ 編預算請老師來改好了 XD。    [2011-03-31 06:07:49 +0000]
    • W************ ⇒ 我看用英文寫這條件一出來可能就沒人要進來了XDD    [2011-03-31 08:53:49 +0000]
  73. "Incidentally, had we proved AOE and AOE^{-1} from scratch, implementation of remember and recomputation can be made perfectly symmetric under the realisability view." I like this part because the symmetry comes out somehow surprisingly and looks beautiful. And it is much more justified to publish a paper which contains something beautiful.    [2011-04-01 06:20:20 +0000]
    • L************** ⇒ What does AOE mean?    [2011-04-01 12:16:04 +0000]
    • Josh Ko ⇒ Age of Empires... XD
      (Seriously, the initials of "algebraic ornament" and "equality".)    [2011-04-01 12:31:48 +0000]
    • Josh Ko ⇒ (The realisability predicate for an algebraic ornament can be reduced to an equality.)    [2011-04-01 12:32:30 +0000]
    • L************** ⇒ Cool! Are you giving a talk after you arrive? BCTCS?    [2011-04-01 12:33:28 +0000]
    • Josh Ko ⇒ You mean to you, right? I still did not sign up for MGS in the end. BCTCS, hmm... not sure whether it is worthwhile to stay for three days...    [2011-04-01 12:39:51 +0000]
    • L************** ⇒ Surely you can leave earlier! Don't worry about the registration fee. If you'd like, you can stay at my place to get £100 off. But, I think it will be paid from the project funding?    [2011-04-01 12:41:50 +0000]
    • Josh Ko ⇒ Whoo, I didn't notice the registration fee. Can I just sneak in for the talks and skip the lunches, banquet and stuff, and also skip the payment? XD    [2011-04-01 12:47:36 +0000]
    • L************** ⇒ Yes, I think so. But if you'd like to give a talk, of course you have to pay it!    [2011-04-01 12:48:22 +0000]
    • Josh Ko ⇒ Oh, I was thinking of giving a talk to you at your place. For now I am less interested in talking in BCTCS - it's safer to publicise it after I have some discussions with Jeremy, I think. XD    [2011-04-01 12:56:00 +0000]
    • L************** ⇒ I'd be quite happy to enjoy your talk!    [2011-04-01 13:03:08 +0000]
  74. Diagram for the first projection. ↦ http://www.facebook.com/photo.php?fbid=177814358937776&set=a.126799950705884.40277.100001276392360    [2011-04-01 18:37:03 +0000]
    • Josh Ko ⇒ TikZ.    [2011-04-02 10:47:21 +0000]
    • L********** ⇒ Thx    [2011-04-04 22:01:06 +0000]
  75. Produced an insertion sort which emits a sorted vector carrying proof that it has a certain length and is sorted, but it can only sort at most **TWO** elements. Give it a three-element list and Agda just hangs.    [2011-04-06 07:42:11 +0000]
    • Josh Ko ⇒ This is the sorted vector [0, 1]:
      <
      true ,
      < false , refl > ,
      < false , refl > ,
      < false , < false , refl > , refl > ,
      < true , < false , refl > , refl > ,
      <
      true ,
      < true , < false , refl > , refl > ,
      < false , refl > ,
      < false , < true , < false , refl > , refl > , refl > ,
      < false , refl > ,
      < false , < true , < false , refl > , refl > , refl > , refl
      >
      , refl
      >    [2011-04-06 07:51:31 +0000]
    • Josh Ko ⇒ Hmm, it just takes a very long time to produce [0, 1, 2] (from [1, 2, 0]):
      <
      true ,
      < false , refl > ,
      < false , refl > ,
      < false , < false , refl > , refl > ,
      < true , < true , < false , refl > , refl > , refl > ,
      <
      true ,
      < true , < false , refl > , refl > ,
      < false , refl > ,
      < false , < true , < false , refl > , refl > , refl > ,
      < true , < false , refl > , refl > ,
      <
      true ,
      < true , < true , < false , refl > , refl > , refl > ,
      < true , < false , refl > , refl > ,
      <
      true ,
      < true , < false , refl > , refl > ,
      < false , refl > ,
      < false , < true , < false , refl > , refl > , refl > , refl
      >
      ,
      < false , refl > ,
      <
      false , < true , < true , < false , refl > , refl > , refl > , refl
      >
      , refl
      >
      , refl
      >
      , refl
      >    [2011-04-06 08:00:47 +0000]
    • L********** ⇒ Why does it take so long?    [2011-04-07 04:39:44 +0000]
    • Josh Ko ⇒ I think Agda implementors do not put emphasis on optimisation for speed (it is not necessary anyway, given that the language is an experimental one). Also I used a lot of rewrites which get translated to a large amount of code.    [2011-04-07 07:39:40 +0000]
  76. Acceptable, I think.    [2011-04-06 15:14:55 +0000]
    • Josh Ko ⇒ Barely acceptable, to be precise...    [2011-04-06 15:18:40 +0000]
  77. 巡迴結束於今日的中興大聚餐，明天收一收後天回去嘍。（照片和 blog 後補⋯）    [2011-04-08 11:38:10 +0000]
    • Josh Ko ⇒ 琦皓你的相機時間慢了一年！XD    [2011-04-08 11:44:46 +0000]
    • 翁** ⇒ 抱歉，當初是相機店老闆設定的，我也沒特別注意XD    [2011-04-08 12:04:35 +0000]
    • Josh Ko ⇒ iPhoto 可以批次調整日期，所以按幾個鍵就搞定了 XD。    [2011-04-08 12:06:06 +0000]
    • 翁** ⇒ 我把相機更新了XD    [2011-04-08 18:07:34 +0000]
  78. APLAS '11 (and CPP '11) to be held in KENTING! (So that was what they were secretly discussing last year.) Should consider submitting a... poster? XD ↦ start [The Ninth Asian Symposium on Programming Languages and Systems, APLAS 2011]    [2011-04-09 00:24:01 +0000]
    • S************ ⇒ Should I post the CFP on facebook?    [2011-04-09 00:54:53 +0000]
    • Josh Ko ⇒ Sounds like a good idea! More publicity does no harm. (Dunno whether this has been done before. Perhaps you'll be the first one to do so? XD)    [2011-04-09 00:59:17 +0000]

Labels:

posted by Josh Ko @ 2:13 pm   0 項意見