神圣的三位一体

基督教教义三位一体指出,上帝以三种人显现:父,子和圣灵,一起共同构成了三位一体的清单。计算机领域三位一体的教义认为,计算常表现为三种形式:命题证明、类型程序和结构之间映射。这三个方面又产生了三个教派:需要首先给出证明和命题的逻辑、程序和类型为优先的语言和映射与结构为优先的范畴Categories。计算三元论的中心教条认为,逻辑,语言和范畴只是一个神圣的计算概念的三个表现。 没有首选的启示途径:每个方面都提供了包括我们生活中计算经验的见解。

计算三元论意味着任何一个方面出现的概念都应该从另外两个角度来看必须具有意义。 如果你得到对逻辑,语言和范畴的重要性的洞察力,那么你可能会确信你已经阐明了计算领域中的一个基本概念 - 你已经做出了永久的科学发现。 我们对计算的理解的进展可能来自从许多方式获得的洞察(任何数据是都有用的并相关的),但是它们的基本真理不取决于它们的受欢迎程度。

逻辑告诉我们存在什么命题(我们希望表达什么样的想法)和什么构成一个证明(我们如何将我们的想法传达给他人)。 语言(在编程的意义上)告诉我们什么类型存在(我们希望表达什么计算现象)和什么构成一个程序(我们如何可以产生这种现象)。范畴告诉我们什么结构存在(我们必须使用什么数学模型)和什么构成它们之间的映射(它们如何相互关联)。

在这个意义上所有三个都有本体论的强迫force;他们编纂的是什么,而不是如何来形容给于了我们什么。 在这个意义上说它们是基础 ; 如果我们假设它们仅仅是描述性的,我们就只剩下这些先前产生这些概念之前出现的问题,而再次引领我们回到基础。 这是我希望在这里描述的基础,因为我相信它将有助于澄清关于命题,类型和结构这些概念的一些共同的误解。这里特别感兴趣的是,“类型系统” 不是强加先前的程序给定概念(是否写有水平线,或没有)的条件的任意集合。它是,一种方式来说,首先程序是什么,作为证明和作为映射程序意味着什么。

在这里,我将勾勒逻辑,语言和范畴之间的基本对应关系。

逻辑的基本概念是蕴涵 ,表示为P1....Pn|-P ,意思是导 P可从 P...Pn推导而出,这意味着 P 可以从逻辑规则推导出来,假设 Pi 作为公理 。这种形式的蕴涵不能表达隐式!特别是,一个蕴涵是从未显式为真。
(这里用普通语言脑补了蕴涵的定义:
语言学中 presuposition与 entailment的区别:
entailment 蕴含:a真b则真,b假a则假;a假b或真或假,b真a或真或假
a. He has been to France. 他去了法国。
b. He has been to Europe.他去了欧洲。

presupposition 预设:a不管真假b都为真,b真a或真或假,b假a无真假可言。
a. John didn't pass math.约翰没有通过数学考试。
b. John took math.约翰参加了数学考试。

此处省略原文中逻辑、语言和范畴本质是一样的证明过程。。。

我发现有关计算三位一体迷人之处,它是美丽的! 想象一下,这个世界是逻辑,编程和数学统一的,其中每个证明对应一个程序,每个程序到一个映射,每个映射到一个证明! 想象一下,代码其实是数学,其中有推理和执行,数学的语言和计算的语言之间是没有差异,它们之间没有分离。 三位一体是计算理论的集成统一的核心组织原则 ,丰富化了逻辑,编程和数学语言。它提供一个框架用于发现以及分析。一方面的创新必须对另一方面有影响;一个方面好主意是另外一个方面的好主意,无论以什么形式出现(无论以三位什么形式出现,本质是一体的)。如果一个想法在逻辑上,范畴上和类型中都没有好的意义,那么它就不可能是神圣的显现。

The Holy Trinity | Existential Type