宗文's profile方寸之间PhotosBlogLists Tools Help

Blog


    August 20

    论数学的基础

        数学家罗素曾经这样说过,“数学是这样的一门学问,它既不知道自己说的是什么,也不知道自己说得是否正确”(大意,找不到原文了)。这句话看上去很让人吃惊,毕竟大部分人认为数学是最精确最不会出错的学科。
        其实他的话可以这么来理解。
        数学的各种命题都会涉及到很多概念,有些概念是用另外的概念定义的。比如“三角形是三个首尾相接的线段组成的图形”,这里三角形是用线段来定义的。那么总会有些概念是无法定义的,这些被成为原子概念。比如几何学里面的“点”、“线”、“面”等。这样这些原子概念数学就不在追究它们究竟是什么,于是“数学就不知道自己说得是什么了”。
        数学里面有很多定理,很多定理都是通过其它定理来证明的。三国时期吴国的赵爽曾经用“面积定理”来证明“勾股定理”,参见http://www.mmit.stc.sh.cn/telecenter/CnHisScience/ggdl.htm。这样一定也存在一些没有办法证明的定理,这些定理一般被称为公理。几何学里面比较有名的公理是“平行公理”,即过直线外一点只能作一条平行线,该公理被提出来以后的一千多年里一直有人试图证明它但都失败了。这些公理究竟是否正确,数学也是不关心的,所以说“数学也不知道自己说得是否正确”。
        这么说,岂不是大事不妙,我们怎么能依赖这个胡说八道的数学呢?
        其实,可以从两个方面来考虑。
        首先,关于概念的问题,只是一个“名”和“实”的问题。数学大师希尔伯特也说,“我们必须可以用桌子、椅子、啤酒杯而不是点、线、面来同样展开我们的几何学”,原子概念不可定义又有什么关系呢,毕竟这些概念间的关系是才是最重要的也是我们最关心的。
        其次,关于公理的问题,这个比较复杂,又涉及到三个问题。
        其一是,数学公理和概念是否代表实际,代表到什么程度。你在地球表面上尽可能画两条平行的直线,因为地球是圆的,它们迟早要相交。在空间,光线的路径应该是直线吧,可是根据爱因斯坦的广义相对论,光线会被引力场弯曲。这样我们知道了,没有纯粹的点,也没有纯粹的直线和平面,所以概念以及概念之上的公理并不能完全地符合实际。但是在小范围内还是符合得很好,数学大师高斯和黎曼就证明了曲面局部性质和平面几何是一致的。
        其二是,公理之间是不是协调的,有没有矛盾。有矛盾的意思是,在公理系统中通过逻辑推理可以推出互相否定的定理来。这个问题的一个附属问题是,公理之间是否是独立的,就是说,其中的某个公理是不是不需要,可以从别的公理推出来。研究某个公理是否独立,就是用将该公理以其否定了来代替看替换过后的体系是否是协调的来判定。哥德尔、科恩等逻辑学家已经证明了我们目前采用的数学公理体系是没有矛盾的相互独立的。
        其三是,公理体系是不是完备的。完备的意思是,这个体系能否证明所有理论上可能的定理,当然其中的某些证明实际上可能需要很多时间和人力。哥德尔第一不完备性定理回答了这个问题,该定理说一切包含算术系统的公理体系,要么是有矛盾的,要么是不完备的。换句话说,所有包含算术系统在内的无矛盾的公理体系都是不完备的,有些定理是无法证明的。这个结果看上去很悲观,但实际上才充分说明了数学是不可穷尽的,是丰富多彩的。很多数论上有名的问题得不到回答可能就是这个原因。
        嗯,从上面说的这些,我们可以看出,罗素的话看上去不可思议,其实正好说明了数学的严谨,也就是说数学对自己究竟能解决哪些问题不能解决哪些问题这个涉及到本身的问题也有着精确的回答。这,就是严密的精确的美丽的数学。
     
    August 14

    在VC6中安装STLport

    进入DOS命令行(cmd)
    进入VC安装目录下的vc98\bin子目录
    执行vcvars32.bat设置cl需要的环境变量
    解压缩到随便一个目录,以下称为目录X
    进入目录X下的src子目录
    set INCLUDE=目录X\stlport;%INCLUDE%
    set LIB=目录X\stlport;%LIB%
    copy vc6.mak makefile
    nmake clean all
    nmake install
    此时安装完毕, 头文件被安装到VC安装目录的vc98\include\stlport目录下, 库文件被安装到vc98\lib目录下, DLL被安装到WIN32系统目录下了.
    在VC的集成环境中将头文件目录(VC安装目录的vc98\include\stlport)增加在最开始即可
    STLport相对于VC6 STL的优点:
    1.和linux上用的STL一致
    2.增加了hash,超长字符串等不在标准内但常用的模板类
    3.代码可读性好
    4.Warning少
    August 09

    先有鸡还是先有蛋?

    还记得十七年前上大学时候的一个晚上,我们宿舍的八个人不知怎么就热烈讨论起“是先有鸡还是先有蛋?”的问题。我那个时候以为这是一个关于名词定义的哲学问题,是无解的。但是对这类问题的兴趣却一直深深埋在我的心底。后来有空读了一些生物学尤其是进化论方面的科普书籍,其中《自私的基因》《进化是什么》等几本书更是让我看了一个又一个通宵。这之后的某天,突然我明白了,“鸡与蛋”的问题并非是一个哲学问题,而是一个进化论的问题,是可以有精确的答案的。
    达尔文的进化论的一个基本论点是所有的生物拥有共同的祖先,这个论点已经被大量的生物学研究所证实,《伊甸园之河》这本书里面还用了相当多的篇幅论证了这个论点。而且进化的历史就是物种分化的历史,就是博物学上物种分类的依据。因此我们可以断定最早的鸡一定有其父母,而且既然这是最早的鸡,那么其父母就不会和其是同一物种(“鸡”)。注意,我们为什么说两种生物不是一个物种呢?物种又是靠什么来区分的呢?只能是其基因型。所以说最早的鸡和其父母的基因型一定不同。我们知道,作为卵生动物的鸡,是从一个受精卵细胞通过有丝分裂逐步长成的,在细胞有丝分裂的过程中,不会产生变异,因此,这只鸡来源的那个受精卵(“蛋”)的基因和这只鸡也是相同的。所以这个蛋就是最早的鸡“蛋”。
    也就是说,先有蛋(受精卵),后有鸡。
    那么有人问,那这颗蛋哪里来的呢?回忆一下高中生物书就知道了,这颗蛋产生于其父母的精子和卵子的结合,而精子和卵子是由父亲和母亲的细胞通过减数分裂得到的,在减数分裂的过程中,同源染色体会发生基因交换和变异。正是这些变异导致这颗蛋不同于其父母的基因型。新的物种就是这样产生的。
    总结来说,要点就是:“鸡”必须从“蛋”来,但是“蛋”可未必一定要从“鸡”来。
    呵呵,后来我搜索google才发现很多人早就得出这个结论了。比如“http://www.iambencn.com/blog/2006/05/29/chicken-and-egg-debate-unscrambled/”。不过我还是蛮高兴自己独立推导出这个答案。

    Linux的核心启动流程(FC5)

    下面以RedHat Fedora Core5(Linux 2.6.15-1.2054_FC5)为基础说说Linux的启动流程。
    打开计算机电源后,第一个执行的程序是ROM BIOS,该程序根据设置选择一个引导设备,比如软盘、硬盘、光盘或者USB盘等,然后读入引导设备上的一小段程序(称为BootLoader,常见的有lilo,grub等)。
    BootLoader会读入相关的引导选单并执行。一般的引导选单上会指定从哪个设备的哪个分区读入操作系统内核,给操作系统传入哪些命令行参数(cmdline)、初始的RAMDISK(initrd)等等。BootLoader将系统核心以及initrd读入内存并传递好cmdline/initrd后就结束了自己的使命,控制权转移到Linux kernel。
    我采用的BootLoader是grub,被安装在第一个SCSI盘的第一个分区上,其上的grub.conf内容如下(#后的注释是我加的,下同):
    default=0
    timeout=5
    splashimage=(hd0,0)/grub/splash.xpm.gz
    title Fedora Core (2.6.15-1.2054_FC5)
            root (hd0,0) # 指定操作系统内核(Kernel)文件所在的磁盘和分区
            kernel /vmlinuz-2.6.15-1.2054_FC5 ro root=LABEL=/ # 指定操作系统的文件名称以及cmdline
            initrd /initrd-2.6.15-1.2054_FC5.img # 指定initrd
    title MiniLinux-USB (2.6.15-1.2054_FC5)
            root (hd1,0)
            kernel /boot/vmlinuz-2.6.15-1.2054_FC5 ro root=/dev/ram0
            initrd /boot/initrd-minilinux-usb.img
    操作系统内核(Kernel)会执行各种必要的初始化如内存页表、进程表等等数据结构,初始化被编译到Kernel的内核模块以及设备驱动等等,很多初始化都需要分析cmdline以便在多个策略中选择。
    接下来的启动流程分为两个分支:
    1) 如果BootLoader指定了initrd,则解压initrd指定的初始RAM DISK映像到/dev/ram0并挂装/dev/ram0作为根文件系统,然后执行/init。
    /init的目的一般是装载最终的根文件系统所必须的文件系统内核模块,建立一些设备特别文件并挂装最终的根文件系统(如果不是/dev/ram0)。
    我安装的RedHat FC5的initrd-2.6.15-1.2054_FC5.img文件是个gzip压缩过的cpio文件,在启动完成后位于/boot目录下(因为启动分区被安装在/boot目录下, 参见下篇“linux的应用启动流程”一文)。我们可以执行下述命令提取其内容
    mkdir -p xxx
    cd xxx
    gunzip -c /boot/initrd-2.6.15-1.2054_FC5.img | cpio -idv
    我们可以看到下面有很多目录和文件:
    bin/ dev/ etc/ init* lib/  proc/ sbin@ sys/ sysroot/
    ./bin:
    insmod* modprobe@ nash*
    ./dev:
    console null ram@ ram1 systty tty0 tty10 tty12 tty3 tty5 tty7 tty9  ttyS1 ttyS3
    mapper/ ptmx ram0 rtc  tty    tty1 tty11 tty2  tty4 tty6 tty8 ttyS0 ttyS2 zero
    ./dev/mapper:
    ./etc:
    ./lib:
    BusLogic.ko  ext3.ko  jbd.ko  scsi_mod.ko  sd_mod.ko
    ./proc:
    ./sys:
    ./sysroot:
    其中/init内容如下:
    #!/bin/nash #由/bin/nash解释执行
    mount -t proc /proc /proc #挂装proc文件系统
    setquiet #安静模式
    echo Mounting proc filesystem
    echo Mounting sysfs filesystem
    mount -t sysfs /sys /sys #挂装sysfs文件系统
    echo Creating /dev
    mount -o mode=0755 -t tmpfs /dev /dev
    mkdir /dev/pts
    mount -t devpts -o gid=5,mode=620 /dev/pts /dev/pts
    mkdir /dev/shm
    mkdir /dev/mapper
    echo Creating initial device nodes
    mknod /dev/null c 1 3
    mknod /dev/zero c 1 5
    mknod /dev/systty c 4 0
    mknod /dev/tty c 5 0
    mknod /dev/console c 5 1
    mknod /dev/ptmx c 5 2
    mknod /dev/rtc c 10 135
    mknod /dev/tty0 c 4 0
    mknod /dev/tty1 c 4 1
    mknod /dev/tty2 c 4 2
    mknod /dev/tty3 c 4 3
    mknod /dev/tty4 c 4 4
    mknod /dev/tty5 c 4 5
    mknod /dev/tty6 c 4 6
    mknod /dev/tty7 c 4 7
    mknod /dev/tty8 c 4 8
    mknod /dev/tty9 c 4 9
    mknod /dev/tty10 c 4 10
    mknod /dev/tty11 c 4 11
    mknod /dev/tty12 c 4 12
    mknod /dev/ttyS0 c 4 64
    mknod /dev/ttyS1 c 4 65
    mknod /dev/ttyS2 c 4 66
    mknod /dev/ttyS3 c 4 67 #以上创建必要的设备特别文件
    echo Setting up hotplug.
    hotplug # 设置可以热插拔的设备插拔时的处理程序
    echo Creating block device nodes.
    mkblkdevs # 利用sysfs文件系统自动创建当前发现的块设备的特别文件,关于sysfs将是另一篇文章的内容了
    echo "Loading jbd.ko module"
    insmod /lib/jbd.ko
    echo "Loading ext3.ko module"
    insmod /lib/ext3.ko
    echo "Loading scsi_mod.ko module"
    insmod /lib/scsi_mod.ko
    echo "Loading sd_mod.ko module"
    insmod /lib/sd_mod.ko
    echo "Loading BusLogic.ko module"
    insmod /lib/BusLogic.ko # 前面几个insmod装载接下来挂装最终的根文件系统所必需的驱动程序模块
    mkblkdevs # 创建刚刚这些驱动程序发现并注册到sysfs文件系统中的块设备的特别文件
    echo Creating root device.
    mkrootdev -t ext3 -o defaults,ro /dev/root # 分析kernel cmdline寻找根文件设备并创建一个特别文件指向该设备(如果是以“LABEL=”开始则自动寻找分区表上对应该LABEL的分区)并加入到/etc/fstab中
    echo Mounting root filesystem.
    mount /sysroot #将最终的根文件系统临时挂装到/sysroot下
    echo Setting up other filesystems.
    setuproot # 设置proc,sys等文件系统到/sysroot下
    echo Switching to new root and running init.
    switchroot # 将/sysroot切换为最终的根文件系统,并执行其上的/init,见后
    2) 如果BootLoader没有指定initrd,直接挂装cmdline上指定的root设备作为根文件系统,接下来按照下面的顺序寻找init程序并建立第一个进程:
    run_init_process("/sbin/init"); // 找到就建立第一个进程(pid=0),不会返回了,下面三行同此
    run_init_process("/etc/init");
    run_init_process("/bin/init");
    run_init_process("/bin/sh");
    panic("No init found.  Try passing init= option to kernel."); // 寻找不到,打印错误信息,系统挂起
    不管是哪个分支,到此为止,核心启动流程结束,后面由最终的根文件系统上的init控制转入应用启动流程,这个待下篇文章再说吧。