计算机科学的基石 逻辑学 数学

如果单论计算(机)科学的话,个人感觉其基础是数理逻辑和代数理论。

https://www.zhihu.com/question/20817490

逻辑与代数是计算机科学最重要的基础

http://www.docin.com/p-816879207.html

数理逻辑又称符号逻辑、理论逻辑。它既是数学的一个分支,也是逻辑学的一个分支。是用数学方法研究逻辑或形式逻辑的学科。

用数学的方法研究逻辑的系统思想一般追溯到莱布尼茨,他认为经典的传统逻辑必须改造和发展,使之更为精确和便于演算。后人基本是沿着莱布尼茨的思想进行工作的。

简而言之,数理逻辑就是精确化、数学化的形式逻辑。它是现代计算机技术的基础。

http://www.baike.com/wiki/数理逻辑

1. 形式化方法

在计算机科学中,尤其在软件工程和硬件工程领域,

形式化方法(Formal method),是一种数学方法,用于软件和硬件系统的描述(specification)、开发(development)和验证(verification)。旨在能像其它工程学科一样,通过用数学进行分析,来提高设计的可靠性(reliability)和健壮性(robustness)。

为了让系统表现的和规范(specification)一致,现代软件工程采用了一系列的形式化方法。其中包括一些强有力的框架,例如,霍尔逻辑(Hoare logic),Algebraic specification language(Specification language),模态逻辑(Modal logic),指称语义(Denotational semantics)。它们虽然功能强大,但是对程序员来说门槛较高。

另一方面,还有一些轻量级的技术,可以被植入编译器,连接器或程序分析器中,进行自动校验。从而,那些不熟悉底层理论的程序员也可以使用它们。模型检测(Model checking),运行时验证(Runtime verification)和类型系统(Type system)是常见的轻量级形式化方法。其中类型系统最流行,发展最完善。

2. 历史

在计算机科学中,最早的类型系统用来区别数字的整数和浮点数。

在20世纪五六十年代,这种分类扩展到了结构化的数据和高阶函数中。

70年代,研究者们引入了几个更为丰富的概念,例如,参数化类型,抽象数据类型,模块系统,子类型等等,类型系统作为一个独立的领域形成了。

计算机科学家们也开始意识到,程序语言中的类型与直觉主义逻辑中的命题,之间的联系,称为Curry–Howard correspondence,开始了两方面的交叉研究。后经范畴论(category theory)的探索,得到了三方面的同构关系,Curry-Howard-Lambek correspondence。

https://zhuanlan.zhihu.com/p/34200056

然后是程序语言理论和数理逻辑:

程序语言                Mathematical logic 

类型系统                type theory, proof theory 

结构操作语义            term writing, proof theory, recursion theory 

抽象机器                recursion theory 

指称语义                Domain theory, model theory, set theory 

逻辑编程语言            proof theory 

综合性的                categorical logic

作者:rainoftime

链接:https://www.zhihu.com/question/37050853/answer/71367630

来源:知乎

著作权归作者所有。商业转载请联系作者获得授权,非商业转载请注明出处。

19世纪的布尔最伟大的成就在于将逻辑代数化,构建了逻辑体系。 该逻辑体系下, 与、或、非构成了基本的逻辑符号, 而这是计算机数字电路的理论基础。 20世纪的香农发表了论文《对继电器和开关电路中的符号分析》,论证了构造 与、或、非电路的可行性。

原文地址:https://www.cnblogs.com/feng9exe/p/10594818.html