Hardware Hacking on Linux

一些增加生活质量的, 软件层面的硬件使用:

Keyboard Mapping

CapsLock是个大bug, 十分不常用(其实是完全可以不用), 但占了一块好位置, 还比别的键大, 简直不能忍.

尽管BIOS里能将Left Ctrl与Fn互换, 如果能把CapsLock映射到Ctrl的话, 对生活质量仍然是有极大提高的, 毕竟Ctrl太常用了, 对不写代码的人也是一样(但是不写代码的人不用Linux吧..). 我们可以用xmodmap工具来实现这一点.

Explode Tuple in C++11

std::tuple是C++11中的一个好东西. 它功能上算是std::pair的扩展, 但有一些其他的用法.

例如, 可以借用tuple来模拟多值返回(python中也是这样), SugarCpp 中就是使用tuple实现了简洁的多值返回语法:

tuple<TTsort<T>(a: T, b: T)
    return a < b ? (a, b) : (b, a)

tuple也可以用于模拟python中的Parallel Assignment:

Boole's New Proof of Gödel's Incompleteness Theorem

前些日子查资料的时候发现逻辑学家George Boolos (不是boolean类型的George Boole) 曾经给出过Gödel定理的一个新证明. 看了之后觉得十分有趣.

Review of Gödel's Proof

关于Gödel的原始证明, 网上已有许多解释, 如刘未鹏的这篇文章. 这里再从数理逻辑角度简单回顾一下, 因为Boolos的证明用了许多Gödel的思想.

证明的第一步是建立Gödel Numbering, 也即建立一套编码系统, 使得形式系统中任意公式可与自然数一一对应. 这种思想及其方法在有了计算机的今天是十分轻易的, 在Gödel的文章里, 他用了不同素数表示形式系统中的最基本符号, 从而实现了这一点, 这种方法后来被称为Gödel Numbering.

Blogging with Hexo

一直都想写blog, 总觉得很多想法值得写一写的。 下定决心要写是在看了刘未鹏神牛的 暗时间 之后。 于是先是在blogspot上随便搞了一个,没指望有人看。后来就删了那边,把东西都迁移到了hexo上。

hexo 是一个基于Node.js的static blogging system。 它的作者是台湾人, 可以看到github issue里 有好多中文的。它的使用与Octopress 类似,也兼容Octopress的好多插件,但以快速简洁为亮点, 因为前者是ruby写的。

Problem of Two Eggs

在知乎上看到这么一道题, 原题描述的不太严谨, 其大意是:

一幢 200 层的大楼,给你两个鸡蛋. 如果在第 n 层扔下鸡蛋,鸡蛋不碎,那么从前 n-1 层扔鸡蛋都不碎. 这两只鸡蛋一模一样,不碎的话可以扔无数次. 已知鸡蛋在0层扔不会碎.

提出一个策略, 要保证能测出鸡蛋恰好会碎的楼层, 并使此策略在最坏情况下所扔次数最少.

清华的数学学习

貌似中文标题的都偏吐槽向.

现状

清华的"工科数学基础课", 课堂教学方式大致都是 抄课本.

当然, 抄有不同的抄法. 有的老师抄在黑板上, 有的抄在一学期改一页的ppt上. 一般他们在抄的同时会把文字部分匹配出来读一读, 遇到公式的话有的会读, 有的用指示代词替换掉了, 每个知识点下面抄一个例题. 总之像是个可以写程序控制机器人来完成的活.

Facts About David Hilbert

没错, 这篇文章其实是Cantor, Gödel, Turing这个主题. 我发现只要关于他们的东西都很容易让我看high..

最近在看那本The Annotated Turing. 书中第三章以David Hilbert为主线, 介绍了20世纪初的几十年里数理逻辑与集合论的发展. 想一想的话, Hilbert的确是将Cantor, Gödel, Turing联系起来的关键人物, 然而这段历史我以前知道的并不细致, 而且关于Hilbert's Program, Hilbert's Problems 的故事各个地方说的都乱七八糟的自己也不清楚了, 于是做个记录.