2010/11/06

[facebook digest] Adjunctions

  1. There was a fire drill just a few minutes ago, at 6am! (So the alarm just went off and everyone had to move outside the building.) After I knew it was nothing more than a fire drill, I thought it was cool to have one early in the morning and just couldn't help smiling.
    現在早上六點多，就在剛才竟然來個消防演習！（警鈴大作然後全部人都得移出戶外。）知道只是消防演習後我覺得在這種時間辦演習實在很炫（也很冷），一直很想笑 XD。    [2010-10-26 05:40:53 +0000]
  2. Luo's book is considerably more delicate than Nordström et al.    [2010-10-26 18:41:49 +0000]
  3. 畫這樣最好是有人看得懂啦。
    I'd be surprised if anyone (except perhaps Liang-Ting XD) can recognise this. ↦ http://www.facebook.com/photo.php?fbid=137589116293634&set=a.126799950705884.40277.100001276392360    [2010-10-26 19:57:34 +0000]  [ 1 人說讚！]
    • 賴** ⇒ 向上你改天可以研究一下 labview 的程式　寫不好的話　就跟一樣。    [2010-10-27 06:16:54 +0000]
    • L********** ⇒ Category theory!    [2010-10-27 19:54:52 +0000]
  4. "It has often said that mathematics is taught by intimidation, and learned by imitation." (N. G. de Bruijn) This was certainly true for today's categories lecture, where natural transformations and the (light version of) Yoneda lemma was thrown out with lots of symbols and arrows.    [2010-10-26 20:56:57 +0000]  [ 1 人說讚！]
    • Josh Ko ⇒ s/It has often said/It has often been said/    [2010-10-26 21:09:20 +0000]
    • F********* ⇒ Hi Josh:




      Keep going! I'm pretty sure that you are going to have your first paper in Science or Nature very soon.    [2010-10-26 21:09:28 +0000]
    • Josh Ko ⇒ Ha! Sadly (fortunately?) we do not normally submit papers to Nature or Science but to journals like Journal of Functional Programming or Science of Computer Programming, which are much less famous outside our field. I do hope I can finish my background reading soon and get my hands on some unsolved problems though.    [2010-10-26 21:19:10 +0000]
  5. 這週交的 categories 作業寫到後來大概昏了，問 Pos 裡的 products/coproducts 是什麼我竟然寫 initial/terminal objects。
    I seemed to get rather dizzy when working on the categories exercises submitted this week, in which I reasoned what and why initial/terminal objects in Pos are such and such while it was actually products/coproducts that was required.    [2010-10-26 21:26:48 +0000]
  6. I can finally recognise the forms of intensional and extensional equality, now being able to distinguish judgemental and propositional equality. I still do not understand the consequences of adopting an intensional or extensional equality, though.    [2010-10-27 07:05:32 +0000]  [ 1 人說讚！]
  7. Lambda Calculus 第三次作業的難度又上跳一級⋯
    The difficulty of the third homework of Lambda Calculus jumps again to a new level...    [2010-10-27 18:36:24 +0000]
  8. Perhaps it is possible to write up a (draft) section on Type Theory during the holidays between Michaelmas and Hilary Term.    [2010-10-27 22:18:39 +0000]
    • Josh Ko ⇒ BTW, it's really interesting to compare Luo's Extended Calculus of Constructions with Martin-Löf's Type Theory.    [2010-10-27 22:22:41 +0000]
    • L********** ⇒ about what aspect of type theory?    [2010-10-28 21:51:55 +0000]
    • Josh Ko ⇒ How they deviate on the interpretation and implementation of the propositions-as-types principle.    [2010-10-28 22:00:09 +0000]
  9. suddenly realised it has been exactly a month since he arrived at Oxford!突然發現今天是抵牛津一個月紀念日！    [2010-10-28 16:15:40 +0000]  [ 11 人說讚！]
  10. Pacman to the rescue!    [2010-10-28 16:58:46 +0000]
    • Josh Ko ⇒ Pacman := YK, courtesy of Prof Jean-Jacques Lévy.    [2010-10-28 17:00:33 +0000]
  11. 作業狀態：Lambda Calculus 好不容易 KO 了（過去），Program Analysis 正難產（現在），Categories 題目還不出現（未來）。    [2010-10-28 20:33:51 +0000]
  12. Great mystery: by default there is \bigsqcup but no \bigsqcap.    [2010-10-29 10:27:47 +0000]  [ 1 人說讚！]
  13. 這題 pullback lemma 根本不適合用 commutative diagram 證嘛⋯    [2010-10-29 21:27:17 +0000]
    • S************ ⇒ 可以用.. algebraic style 嗎？    [2010-10-29 23:32:31 +0000]
    • Josh Ko ⇒ 可以呀，上次的 exchange law (f \times g) . (h \times k) = (f . h) \times (g . k) 我就嫌 commutative diagram 太麻煩用 AoP 的方法證掉了。不過搞 categories 的人總是說畫圖比較正統，所以想試試看嘍。    [2010-10-30 07:22:13 +0000]
    • S************ ⇒ Ralf Hinze 和.. Daniel James (?) 最近的一篇 paper, 叫做什麼 isomophism 之類的，就都用等式證一般會用 diagram 去證的性質..    [2010-10-30 07:29:35 +0000]
    • Josh Ko ⇒ Reason Isomorphically!    [2010-10-30 07:35:55 +0000]
  14. Galois connections (and adjunctions) start to make a little bit of sense.    [2010-10-30 11:42:38 +0000]
    • L*********** ⇒ Isn't it making sense at first glimpse? XD Though I've already forgotten the detail.    [2010-10-30 11:50:38 +0000]
    • Josh Ko ⇒ Enlighten me!    [2010-10-30 11:55:14 +0000]
  15. is going to Oxford Town Hall in a few minutes with Liang-Ting for the "From the New World" concert.    [2010-10-30 18:30:17 +0000]  [ 2 人說讚！]
  16. 時間在凌晨悄悄改回 +0 了，今天賺一小時！XD    [2010-10-31 07:08:53 +0000]
  17. 好吧，這次的 Program Analysis 作業應該是爆掉了 XD。    [2010-10-31 17:00:18 +0000]  [ 1 人說讚！]
    • Josh Ko ⇒ 沒關係，明天就有習題課了 XD。    [2010-10-31 18:35:00 +0000]
  18. I guess the symmetry in Galois connections (adjunctions) is key to a deeper understanding of the notion. Let's try to find it out this evening.    [2010-10-31 19:08:52 +0000]
  19. Suddenly I can only connect to the Internet via https/SSL/VPN but not http. What happened? (Now connecting via VPN.)    [2010-10-31 21:49:28 +0000]
  20. Meditations on Galois connections. (It's just a beginning.) Only after I finished these notes did I realise I was doing the same thing as Descartes. Well, perhaps not exactly, because Descartes' Meditations were polished works while mine are truly raw, fresh notes that were scribbled down on the fly. ↦ http://sites.google.com/site/joshkos/Meditations_Galois_1.pdf    [2010-10-31 21:56:01 +0000]
  21. 「近年來，從事基礎計算科學研究的台灣學者們已在各校各自成立了數個研究團隊，並在一些題目上相互合作。和任何領域一樣，對基礎計算科學有興趣的學生必須透過一系列課程學習基本知識。然而，國內從事此類研究的學者分散在各校，難以僅靠一己之力開設整套課程。因此，我們希望有相同興趣的學者，一同開課，訓練下一代的研究人才。」這學期到現在還沒翻過去，毫無疑問是 FLOLAC 的功勞呀。不過陷我於此處境的也是 FLOLAC 就是了 XD。 ↦ start [2007 Formosan Summer School on Logic, Language, and Computation (FLOLAC '07)]    [2010-11-01 20:47:11 +0000]
    • Josh Ko ⇒ 現在的狀況就是很多基本常識都有在 FLOLAC 先聽到。scm 老師的願景實現得很成功。    [2010-11-01 20:53:03 +0000]
    • J******* ⇒ 我快翻了就是因為沒去 FLOLAC 嗎 (淚).. 真是錯誤決定啊orz    [2010-11-01 22:20:33 +0000]
  22. Interestingly, my "distorted proofs" got an A+ and my "exploded work" got an A.
    結果我的「歪七扭八證明」拿了 A+，「爆掉的作業」拿了 A。    [2010-11-01 21:01:37 +0000]  [ 8 人說讚！]
    • 施** ⇒ 炫耀文(指)    [2010-11-02 14:01:56 +0000]
  23. Today: Meditations on the entanglement of universal arrows and adjunctions!    [2010-11-02 19:21:40 +0000]
    • Josh Ko ⇒ "Tonight" is more accurate. XD    [2010-11-02 19:42:40 +0000]
  24. Not really meant for people other than me to read, though... ↦ http://sites.google.com/site/joshkos/Meditations_Universal_Arrows_and_Adjunctions_1.pdf    [2010-11-02 21:55:30 +0000]
    • C*********** ⇒ Looks like this : http://en.wikipedia.org/wiki/File:Sumerian_26th_c_Adab.jpg    [2010-11-03 05:11:33 +0000]
  25. Somehow I feel the abstraction process in category theory (e.g., from products to pullbacks then to limits) can be compared with internalisation of concepts in logic (e.g., A ∧ B true if A true AND B true). We encode more concepts into the language, so we can talk and reason about those concepts within the language.    [2010-11-02 22:09:02 +0000]
  26. And universality and adjunctions are really clever formulations that truly show the power of category theory. They really deserve more ruminations. (Being able to say that means I finally feel something about them... Yay!)    [2010-11-02 22:14:42 +0000]
  27. I find the "meditation form" useful at this stage of learning category theory.    [2010-11-02 22:23:57 +0000]
    • Josh Ko ⇒ If the idea is immature or vague, then it's not suitable to be written down as there are still a lot of fast searches going on. If the idea is mature and complete, then it shouldn't be treated in such an informal form like meditations. But if the idea has just formed up fresh, then the meditation form is free enough to let you quickly record the idea and has the advantage of being clearer than scribbled notes.    [2010-11-02 22:24:03 +0000]
  28. The categories class demonstrator told me my homework is one of the best, and suggested that I write my homework by hand instead of typesetting it because it's time-consuming. Well, in fact I find typesetting my homework more convenient because I keep revising my proofs. Shifting clauses and changing wording are not so easy with handwriting.    [2010-11-03 08:47:48 +0000]  [ 2 人說讚！]
    • Josh Ko ⇒ And since I spent quite some time thinking about how to do the proof (nicely), the time for typesetting is not very significant relatively. And I'm comfortable with ordinary math typesetting anyway, having done that for, in particular, the weekly assignments of the one-year undergraduate algebra course.    [2010-11-03 08:47:53 +0000]
    • 陳** ⇒ Well, I need hand writing for a draft. XD    [2010-11-03 13:09:39 +0000]
  29. Entering an extremely dry part of ECC...    [2010-11-03 14:12:32 +0000]
  30. Basically I skipped over the basic meta-theoretic properties of ECC (Chapter 3)... It's indigestible.    [2010-11-03 15:04:06 +0000]
    • 王** ⇒ ecc? error-correcting codes? XD    [2010-11-03 16:15:58 +0000]
    • Josh Ko ⇒ Extended Calculus of Constructions. XD    [2010-11-03 16:32:01 +0000]
    • E******** ⇒ 是營養學分的意思嗎？？XDDD    [2010-11-04 13:31:56 +0000]
    • Josh Ko ⇒ 沒耶，是太硬咬不下去 XD。    [2010-11-04 16:57:36 +0000]
  31. Chapter 4 is the strong normalisation theorem for ECC. It looks like I am going to watch a magic show (strong normalisation proved in front of my eyes but not knowing what really happens).    [2010-11-03 15:14:14 +0000]
  32. Things like Gödel numbering are really mind-boggling...    [2010-11-04 11:12:46 +0000]
    • Josh Ko ⇒ I'd like to reserve the prestigious adjective "mind-boggling" specifically for them!    [2010-11-04 11:15:13 +0000]
  33. Is there anyone who also thinks C(A, f) and C(g, B) should just be written as (f .) and (. g)?
    沒有人覺得 C(A, f) 和 C(g, B) 應該寫成 (f .) 和 (. g) 就好了嗎？    [2010-11-04 22:57:13 +0000]
    • Josh Ko ⇒ The only problem I can think of is that it's slightly easier to lose track of the types.    [2010-11-04 22:59:02 +0000]
    • L************** ⇒ It's not consistent with C(A, B)?    [2010-11-04 23:22:29 +0000]
    • Josh Ko ⇒ There are more inconsistencies and we choose to live with them, e.g., the direction of function composition and the related types (this is truly annoying sometimes), and a limit (colimit) is a couniversal (universal) element... And since C(A, -) is such a special kind of functor, I think it's okay to have a special notation for it.    [2010-11-05 08:20:14 +0000]
  34. "I, Hsiang-Shang Ko, from Changhua Senior High School and National Taiwan University, born 28th February 1987, son of Jung-Feng Ko and Hsiu-Ching Tsai, of Changhua City, Taiwan, herewith enter my name into the College Register. [signature]"
    在三百年歷史的學院名冊中留下一筆記錄。    [2010-11-05 09:56:05 +0000]  [ 12 人說讚！]
    • F********* ⇒ I hope that I can also set a record in your college next year!    [2010-11-05 23:12:49 +0000]
  35. I definitely have not been this comfortable with adjunctions before.    [2010-11-05 21:32:07 +0000]
  36. 原來今天就是煙火節啊⋯    [2010-11-05 21:40:41 +0000]
  37. 這次的 categories 作業畫了好多流通圖，看起來真是賞心悅目 XD。
    I drew quite a few commutative diagrams for this week's categories exercises, which look pleasantly beautiful.    [2010-11-05 23:10:15 +0000]
  38. 現在看 Mac Lane 的 Theorem IV.2（adjunctions 的等價條件定理）只差 unit 和 counit 互為 inverse 那一條還沒摸過，其他看起來都挺符合直覺了。Marvellous!    [2010-11-05 23:31:44 +0000]

Labels:

posted by Josh Ko @ 8:51 am   0 項意見