2010/10/24

[facebook digest] Type Theory

  1. 月亮跑好快⋯
    The moon has been moving so fast...    [2010-10-17 21:09:33 +0100]  [ 1 人說讚！]
  2. Equality is hard...    [2010-10-17 21:15:49 +0100]
    • Josh Ko ⇒ My guess: intensional equality involves only mechanical reductions and is hence decidable, while whether two objects are extensionally equal may in general require construction of proofs, which cannot be automated. But I still do not fully understand what Nordström et al says on p 61. In particular several meta-theorems are mentioned without any details or references. Marked.    [2010-10-17 21:30:54 +0100]
    • Josh Ko ⇒ And now eta-equality can be established at the judgmental level only if we have extensional equality, while we can prove eta-equality as a propositional, intensional equality? What's happening? (p 62)    [2010-10-17 21:37:15 +0100]
    • S************ ⇒ which paper is that?    [2010-10-18 01:45:35 +0100]
    • Josh Ko ⇒ It's Nordström, Peterson, and Smith's book Programming in Martin-Löf's Type Theory.    [2010-10-18 07:19:16 +0100]
    • S************ ⇒ I shall print it and take a look. :)    [2010-10-18 08:23:35 +0100]
  3. "If programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation that it is the computer's duty to execute (a difference that Dijkstra has referred to as the difference between computer science and computing science), then it no longer seems possible to distinguish the discipline of programming from constructive mathematics."    [2010-10-18 21:57:18 +0100]  [ 3 人說讚！]
    • Josh Ko ⇒ Per Martin-Löf, Constructive mathematics and computer programming. Should make a nice bedtime reading.    [2010-10-18 21:58:43 +0100]
    • Josh Ko ⇒ I think I can now confirm that I've opted for intuitionism.    [2010-10-18 22:28:11 +0100]
    • L************** ⇒ I think it is one of programming paradigms, but not the one. Furthermore, what do you mean by "constructive mathematics"? There are many variants of intuitionism, though.    [2010-10-19 00:29:47 +0100]
    • Josh Ko ⇒ Certainly. So the next step could be finding a branch that matches my thought, but it's not urgent. XD    [2010-10-19 08:28:17 +0100]
    • S************ ⇒ For a while I thought you were quoting Dijkstra himself, who emphasised whenever he could that programming is a mathematical activity whose end product happens to be executable by a machine. What Dijkstra had in mind were perhaps very different from the developments in type theory, though.    [2010-10-19 12:33:07 +0100]
    • Josh Ko ⇒ I'd say their emphases are different. My feeling is that Dijkstra emphasised that programs are entities we can reason about mathematically (so we have proofs about programs), while Martin-Löf said mathematical reasoning is indistinguishable from programming (so proofs are programs).    [2010-10-19 14:16:34 +0100]
    • L************** ⇒ So, in Dijkstra's words, programs are mathematical entities using logic. On the other hand, programs themselves are logic. Is that right to you?    [2010-10-19 16:39:59 +0100]
    • S************ ⇒ Hmm... question: in this context, how is mathematics different from logic?    [2010-10-19 16:48:07 +0100]
    • L************** ⇒ I think of mathematics as a process to model ideas into logical statements. For example, we model the notion of spaces in at least two different ways. One is topology where "point" is a primitive notion of the modelling, and the other is locale where "open set" is primitive. The difference is that proofs in topology are usually not constructive, but in locales they are usually constructive.    [2010-10-19 16:59:58 +0100]
    • L************** ⇒ Of course, these two categories are not the same. They only coincide in a subcategory called sober spaces. A sober space, by definition, is the space where points can be uniquely determined by open sets. The definition doesn't tell you very much, though.    [2010-10-19 17:03:52 +0100]
    • L*********** ⇒ I like the idea that the logic itself is also an executable program so that we can prove the logic by executing it instead of examining it carefully every time. On the other hand, programs could be mathematically reasoned is interesting but I didn't like it so much, because some crazy programs Just Work(TM) that no one really knows how they work is too hard to be reasoned, and probably no one cares as well. In addition, writing programs without sanity and just see if it would work is one of the most joyful process of programming in my mind. Sometimes it's just fun to throw random ideas in a sandbox and see if it'll burst into an universe. My two NT$, haha.    [2010-10-21 05:59:53 +0100]
  4. Subset types? Why not just Sigma types?    [2010-10-19 09:44:35 +0100]
  5. I don't quite get why we need the (or a) subset theory... Feeling aimless, it is rather annoying to follow the reconstruction of the whole theory from what a judgment is to universe construction all over again.    [2010-10-19 14:05:38 +0100]
    • Josh Ko ⇒ Guess: Is it related to proof erasure?    [2010-10-19 14:56:57 +0100]
    • Josh Ko ⇒ I'd now say it's a nice guess!    [2010-10-20 10:39:46 +0100]
  6. It's funny that in Type Theory (described by Nordström et al) a set refers to a "type" whose canonical elements are specified, while a type refers to a set in its ordinary mathematical meaning (and Martin-Löf calls it a category). (Am I interpreting these terms correctly?)    [2010-10-19 14:32:53 +0100]
    • Josh Ko ⇒ I think formally type-theoretical types and a set-theoretical sets cannot be identified, but the intuitions should be very much the same.    [2010-10-19 14:39:53 +0100]
    • L************** ⇒ Well, it depends on which type theory you concern.    [2010-10-19 17:09:26 +0100]
  7. Take a short rest. Otherwise I may not be able to make it through the two-hour categories course later...    [2010-10-19 15:16:44 +0100]
  8. After the categories course, I passed by Keble College when I was inquired where St Catherine's was. I thought it was not helpful to share with him that I went to St Catherine's by accident just a few days ago, so I simply showed him my map in my backpack.    [2010-10-19 19:04:32 +0100]
  9. is considering going to a concert by Oxford Philomusica, performing Chopin's first concerto (piano by Tatiana Kolesova) and Dvorak's 9th symphony. If he does show up there, it would be the first time he listens to a live performance of the first concerto, which has been one of his favourites for five years.    [2010-10-19 19:15:57 +0100]
    • Josh Ko ⇒ http://oxfordphil.com/4/Concerts?find=209
      I am wondering if anyone would like to join me?    [2010-10-19 19:18:34 +0100]
    • L************** ⇒ Dvorak's 9th symphony!!!    [2010-10-19 20:09:07 +0100]
    • L************** ⇒ I'd like to join you, but I hope I *can't* you because of someone. XD    [2010-10-19 20:53:45 +0100]
    • Josh Ko ⇒ Alright... XD    [2010-10-19 20:59:08 +0100]
  10. Today I tried Tesco's self-service for the second time, and it was not successful either. After I first scanned the apple juice, the machine displayed that I bought not only the apple juice but also some coffee (but I did not) and then just stuck there. The rest was okay though, after the problem was resolved by a staff.    [2010-10-19 20:02:13 +0100]
    • W************ ⇒ 天，我想Tesco的自助服務，第二次，而且沒有成功要么。 我第一次掃描後的蘋果汁，機器上顯示，我買的不僅是蘋果汁，但也有一些咖啡（但我沒有），然後就卡在那裡。 其餘的還不錯不過，問題得到解決後，由工作人員。    [2010-10-19 20:09:28 +0100]
    • W************ ⇒ = =爛翻譯    [2010-10-19 20:09:43 +0100]
    • Josh Ko ⇒ Google 翻譯 XD    [2010-10-19 20:41:44 +0100]
    • Josh Ko ⇒ 突然發現你也太晚睡了吧 XD。    [2010-10-19 20:47:51 +0100]
  11. still cannot find the right way to comprehend category theory. Recognition of "diagrammatic forms" doesn't seem to scale very well.    [2010-10-19 20:49:53 +0100]
  12. 0 degrees Celsius?! This day has finally come...    [2010-10-20 09:09:40 +0100]  [ 3 人說讚！]
    • 施** ⇒ cool!!    [2010-10-20 15:25:46 +0100]
    • S********** ⇒ take care~ :D    [2010-10-20 17:26:39 +0100]
  13. Take a deep breath and dive into the subset theory again...    [2010-10-20 11:31:54 +0100]  [ 3 人說讚！]
    • L************** ⇒ reference?    [2010-10-20 13:10:20 +0100]
    • Josh Ko ⇒ 就是 Nordström et al 的 Chapter 18. 再看一遍我還是覺得讀起來好像 early draft，匆匆忙忙寫出來的。    [2010-10-20 14:13:48 +0100]
    • Josh Ko ⇒ 就是 rules 劈頭全部寫出來這樣，沒什麼闡述。    [2010-10-20 14:18:47 +0100]
  14. Homework for Lambda calculus becomes more interesting this week...    [2010-10-20 21:11:15 +0100]  [ 3 人說讚！]
  15. borrowed Twenty-Five Years of Constructive Type Theory (again). Now he understand more about what the articles say.    [2010-10-21 11:13:52 +0100]
  16. 腦態恢復到可以在走向 Comlab 途中想到習題解答了。
    My brain state has recovered to one that's able to come up with a solution to a homework exercise on my way to Comlab.    [2010-10-21 16:12:43 +0100]  [ 1 人說讚！]
  17. 用非 Computer Modern 字型的時候要小心，因為本文和數學字型往往不一樣。
    One must be careful when using non-Computer Modern fonts, because the font for text and math are often different. ↦ http://www.facebook.com/photo.php?fbid=136162859769593&set=a.126799950705884.40277.100001276392360    [2010-10-21 17:58:50 +0100]
  18. This is purely wonderful. ↦ Detexify LaTeX handwritten symbol recognition    [2010-10-21 20:48:13 +0100]  [ 5 人說讚！]
    • S************ ⇒ Wow, this is useful!    [2010-10-22 02:52:41 +0100]
    • L*********** ⇒ 正好可以學學那些符號到底怎麼念 XD    [2010-10-22 15:06:17 +0100]
  19. 這次蘋果汁也喝太兇了吧，兩天消掉兩公升⋯    [2010-10-21 20:58:34 +0100]
    • M*********** ⇒ 是有這麼好喝嗎??!!@@    [2010-10-22 03:30:14 +0100]
    • 陳** ⇒ 是原汁的 還是工廠加工的呀@@ 兩公升快當水在喝了...    [2010-10-22 05:03:46 +0100]
    • Josh Ko ⇒ 產地濃縮運輸後加水製成的 XD。    [2010-10-22 11:29:12 +0100]
    • R********** ⇒ 那邊的水要錢嗎 XD?    [2010-10-22 13:18:52 +0100]
    • Josh Ko ⇒ 看是什麼水 XD。    [2010-10-24 15:33:04 +0100]
    • Y********** ⇒ 那邊的蘋果汁要錢嗎? XD    [2010-10-24 15:33:56 +0100]
    • Josh Ko ⇒ 要耶，除非是社交場合上提供的 XD。    [2010-10-24 15:34:41 +0100]
  20. 造型很符合 XD。 ↦ PHD Comic: The Sub-Unconscious    [2010-10-21 21:18:52 +0100]  [ 1 人說讚！]
    • 王** ⇒ XD 還真的有點像    [2010-10-22 02:58:23 +0100]
    • 曾** ⇒ XDD    [2010-10-22 04:31:32 +0100]
  21. 冰箱突然被我清空了，今晚得去大採購一番。    [2010-10-22 09:15:23 +0100]
    • 楊** ⇒ 真有錢    [2010-10-22 09:17:19 +0100]
    • R********** ⇒ 開始自己煮飯了嗎 XD?    [2010-10-22 13:14:09 +0100]
    • J******** ⇒ 自己煮飯好啊
      便宜又合自己口味    [2010-10-23 05:00:44 +0100]
    • 王** ⇒ 一樓才是真的好野人 ～～(菸)    [2010-10-23 15:44:43 +0100]
    • Josh Ko ⇒ 暫時沒有往下一階段的打算 XD。    [2010-10-24 15:33:54 +0100]
  22. 直接用 AoP 的方法證好像比較快，紙上畫 commutative diagram 很難說現在哪條跟哪條生哪條出來⋯    [2010-10-22 09:58:54 +0100]
  23. 這次的 categories 作業寫得好煩喔⋯（而且右耳正在大聲嗡嗡叫。）    [2010-10-23 17:26:09 +0100]
    • 王** ⇒ ！！！你耳朵怎麼了壓？    [2010-10-24 04:22:10 +0100]
    • 陳** ⇒ 有時嗡嗡聲是感冒的前兆，學長保重呀    [2010-10-24 05:16:30 +0100]
  24. just bought a ticket to the concert From the New World. (One ticket only, as he had anticipated.) ↦ Oxford Philomusica | Concerts    [2010-10-23 21:04:52 +0100]
  25. 來 Comlab 印、交作業。    [2010-10-24 16:22:44 +0100]
  26. 把歪七扭八的證明交出去了。這次印在 100 磅的紙上，有點太高級了。
    My distorted proofs were handed out. This time they were printed on 100g paper, whose quality was too good for that purpose.    [2010-10-24 18:25:28 +0100]
  27. Comlab on Sunday is basically empty, so the floor squeaks even more loudly.
    星期日的 Comlab 基本上沒人，所以地板嘎嘎叫得更大聲。    [2010-10-24 18:28:08 +0100]
  28. is considering bringing his camera to Comlab next weekend to record its maze-likeness.
    考慮下週末帶相機去記錄 Comlab 迷宮實況。    [2010-10-24 18:32:11 +0100]

Labels:

posted by Josh Ko @ 10:04 pm   0 項意見