《通往逻辑、数学和编程的Haskell之路》—— 一阶逻辑的形式和意义(1)
本篇的内容是关于书中第二章的内容,从计算的角度理解逻辑中的一些基本概念,例如,逻辑连接符的概念和意义,论证的有效性,逻辑学中的陈述性概念如何表示为计算中的算法概念,特别是对量词概念在计算中的再定义。
在前面的笔记中,曾经多次强调函数的重要性,这里再一次简明归纳一下:
函数的过程/映射二象性:一个函数,既可以看做是一个计算过程,也可以看做是两个集合之间的映射关系,前者又称作算法,或者函数内涵性的定义,后者称作函数的外延性定义。如果你是个程序员,可能马上理解我在说什么。在某些程序设计语言中(例如C语言),一个新的函数产生,要经过声明、定义和调用三个步骤。所谓‘声明’,就是只规定函数的接口:函数名,参数的个数和类型,以及返回值的类型。在这个阶段,我们无从知道这个函数具体内容,假定函数的参数个数为1,参数类型是整数,返回类型也是整数,那么,这个对函数的‘声明’实际上确定了函数的外延,亦即,整数集合到整数集合的映射关系:
ƒ:Z → Z
其中,ƒ代表函数名,Z是整数集合,箭头表示两个集合之间的映射关系。
在函数的‘定义’阶段,作为程序员,我们要严格、精确地描述函数的计算过程。这个过程必须是有限步骤可以完成的,完成后必须产生一个确定的结果。
最后是函数的‘调用’,将具体的对象带入到函数参数中,函数将返回一个确定的‘值’。由这个例子,我们可以有两个看待函数的视角:
静态的:只关心函数的输入和输出,亦即,集合之间的映射关系;
动态的:将函数看做是一个算法,一个由有限多个‘动作’完成的一个计算任务。
这两种看待函数的方式,我们称之为函数的“过程/映射二象性”。反之,无论是在哲学、数学、逻辑学还是计算机科学,凡是具备这种“过程/映射二象性”的对象,我们都可以称作函数。从哲学的角度来看,存在问题不再是思辨问题,不再仅仅是证明问题,而更是一个建构性的问题,只要你能够构造出要证明的对象,就可以确定其存在,而不仅仅是用反证法证明如果不存在将会导致矛盾。从数学角度,要证明某个数学对象具有某个性质,我们可以建立一个算法,例如,证明某个自然数是素数,我们可以通过有限步骤的算术运算,构造出这个数。从计算机科学的角度,我们可以编写个判定函数,经过有限次运算得到关于该自然数是否是素数的布尔值。以这种思想作为哲学、数学思想的学派,称作直觉主义,或者建构主义,这个学派的创始人是荷兰数学家布劳威尔(L.E.J. Brouwer),而将其思想发扬光大的是布劳威尔的嫡传弟子荷兰数学家海廷(Arend Heyting)、英国哲学家达米特(Michael Dummett),美国数理逻辑学家克里尼(Stephen Kleene),以及法国数学家庞加莱(Henri Poincaré)。这一派数学哲学思想,在上个世纪60年代重新受到重视,是现代计算机科学的哲学思想之一。本书的作者基本上也是秉承这个思想,将逻辑学的基本概念、定义、定理都看做是一个可构造的算法过程。这一点也和我们前面引述的SICP的基本思想一致:计算机科学的本质是对陈述性、定义性知识的过程性再定义。见微而知著,从上面关于函数“过程/映射二象性”,我们也可以体会这个思想的基本要义。这个思想是我们今后学习的理论基础。
本章的内容分为6个小节:
1. 逻辑连接符的概念和意义
本节介绍了命题逻辑的5个逻辑连接符的使用、意义以及如何在haskell的解释器环境中实现。
2. 逻辑有效性和相关的概念
有效性是逻辑推理、论证和证明的主要概念,如何将有效论证转化为复合命题句的永真式,以及在haskell语言中实现的方法。
3. 变量的语义和量词概念
如何在逻辑的语境中理解变量的概念,以及变量和量词的关系
4. lambda抽象
本节引入lambda表达式的概念,以及lambda函数式的类型表达,介绍类型论的初步概念
5. 定义和实现
本节非常短,但提出了一个非常重要的问题:如何将一个数学命题转化为算法,亦即,将陈述性知识转化为过程性知识?
6. 抽象公式与具体结构
介绍逻辑式与数学对象之间的映射关系——公式与模型,这部分属于一阶逻辑的语义论。
7. 对量词的逻辑处理
介绍量词概念和带量词的命题
8. 作为过程/程式的量词
作为第5节和第6节原则的应用,学习如何将带量词的命题转化为算法过程。
下一篇,我们将详细介绍第1节和第2节的内容。请到官网下载第二章的Haskell源码:TAMO.hs以备下次内容之需。如果不知如何下载,可参考这篇文章。
在前面的笔记中,曾经多次强调函数的重要性,这里再一次简明归纳一下:
函数的过程/映射二象性:一个函数,既可以看做是一个计算过程,也可以看做是两个集合之间的映射关系,前者又称作算法,或者函数内涵性的定义,后者称作函数的外延性定义。如果你是个程序员,可能马上理解我在说什么。在某些程序设计语言中(例如C语言),一个新的函数产生,要经过声明、定义和调用三个步骤。所谓‘声明’,就是只规定函数的接口:函数名,参数的个数和类型,以及返回值的类型。在这个阶段,我们无从知道这个函数具体内容,假定函数的参数个数为1,参数类型是整数,返回类型也是整数,那么,这个对函数的‘声明’实际上确定了函数的外延,亦即,整数集合到整数集合的映射关系:
ƒ:Z → Z
其中,ƒ代表函数名,Z是整数集合,箭头表示两个集合之间的映射关系。
在函数的‘定义’阶段,作为程序员,我们要严格、精确地描述函数的计算过程。这个过程必须是有限步骤可以完成的,完成后必须产生一个确定的结果。
最后是函数的‘调用’,将具体的对象带入到函数参数中,函数将返回一个确定的‘值’。由这个例子,我们可以有两个看待函数的视角:
静态的:只关心函数的输入和输出,亦即,集合之间的映射关系;
动态的:将函数看做是一个算法,一个由有限多个‘动作’完成的一个计算任务。
这两种看待函数的方式,我们称之为函数的“过程/映射二象性”。反之,无论是在哲学、数学、逻辑学还是计算机科学,凡是具备这种“过程/映射二象性”的对象,我们都可以称作函数。从哲学的角度来看,存在问题不再是思辨问题,不再仅仅是证明问题,而更是一个建构性的问题,只要你能够构造出要证明的对象,就可以确定其存在,而不仅仅是用反证法证明如果不存在将会导致矛盾。从数学角度,要证明某个数学对象具有某个性质,我们可以建立一个算法,例如,证明某个自然数是素数,我们可以通过有限步骤的算术运算,构造出这个数。从计算机科学的角度,我们可以编写个判定函数,经过有限次运算得到关于该自然数是否是素数的布尔值。以这种思想作为哲学、数学思想的学派,称作直觉主义,或者建构主义,这个学派的创始人是荷兰数学家布劳威尔(L.E.J. Brouwer),而将其思想发扬光大的是布劳威尔的嫡传弟子荷兰数学家海廷(Arend Heyting)、英国哲学家达米特(Michael Dummett),美国数理逻辑学家克里尼(Stephen Kleene),以及法国数学家庞加莱(Henri Poincaré)。这一派数学哲学思想,在上个世纪60年代重新受到重视,是现代计算机科学的哲学思想之一。本书的作者基本上也是秉承这个思想,将逻辑学的基本概念、定义、定理都看做是一个可构造的算法过程。这一点也和我们前面引述的SICP的基本思想一致:计算机科学的本质是对陈述性、定义性知识的过程性再定义。见微而知著,从上面关于函数“过程/映射二象性”,我们也可以体会这个思想的基本要义。这个思想是我们今后学习的理论基础。
本章的内容分为6个小节:
1. 逻辑连接符的概念和意义
本节介绍了命题逻辑的5个逻辑连接符的使用、意义以及如何在haskell的解释器环境中实现。
2. 逻辑有效性和相关的概念
有效性是逻辑推理、论证和证明的主要概念,如何将有效论证转化为复合命题句的永真式,以及在haskell语言中实现的方法。
3. 变量的语义和量词概念
如何在逻辑的语境中理解变量的概念,以及变量和量词的关系
4. lambda抽象
本节引入lambda表达式的概念,以及lambda函数式的类型表达,介绍类型论的初步概念
5. 定义和实现
本节非常短,但提出了一个非常重要的问题:如何将一个数学命题转化为算法,亦即,将陈述性知识转化为过程性知识?
6. 抽象公式与具体结构
介绍逻辑式与数学对象之间的映射关系——公式与模型,这部分属于一阶逻辑的语义论。
7. 对量词的逻辑处理
介绍量词概念和带量词的命题
8. 作为过程/程式的量词
作为第5节和第6节原则的应用,学习如何将带量词的命题转化为算法过程。
下一篇,我们将详细介绍第1节和第2节的内容。请到官网下载第二章的Haskell源码:TAMO.hs以备下次内容之需。如果不知如何下载,可参考这篇文章。
终于等到老师更新了
> 我来回应