科学网 › 标签 › 类型论

标签: 类型论

相关帖子	版块	作者	回复/查看	最后发表

没有相关内容

相关日志

语言学研究之浅见: 热度 2 saif 2017-9-29 22:01; 这些年来，稍稍远离了主流的语言学理论，也没有对具体的语言现象加以注意，大部分精力都放到了语言学之外的学习，主要是逻辑学的学习，从一阶逻辑、模型论、证明论、类型论到和计算有关的可计算函数理论、包括lambda演算和组合子逻辑。除此之外就是数学的学习，包括集合论、抽象代数和范畴论的学习。当然，学习的主要动机仍然和语言学有关，在经历了生成语法（GB、HPSG、LFG、TAG）、范畴语法（的各种变种）、蒙太古形式语义学（及其后续理论）之后，我希望能够找到其中最本质的东西——在这些语言理论和形式框架背后的基本思想和方法论。这个探索过程经过了语法框架——语法框架的形式基础——一阶逻辑——类型论——lambda演算——组合逻辑，过程充满了乐趣和艰辛。而探索的动机来源于对现存所有语言学理论的怀疑——这个怀疑可以由许许多多的问题构成，但最后仍然归结为我们坐在教室第一天听《语言学概论》时的第一个问题：什么是语言学？这个迷惘和困扰一直在缠绕着我，直到“遇到”一位从未谋面的伟大作者Max Cresswell，一位“差点”和Montague齐名的新西兰的逻辑学家。他在《Logics and Languages》这样写道： “至少存在着两种研究语言的方法：一种方法是把语言看做是现实中的人类现象，深入其中、研究发现的现象；第二种方法是研究各种形式语言，对这种语言我们可以先规定一些严格可控的的定义，再把这些定义引入这些形式语言；然后在这些形式语言中一点点加入自然语言的成分。” 毫不讳言，作者的这个思想我本人也具备，我在《闲聊语义学》中曾经提到Montague研究自然语言语义学也是从谓词逻辑开始一点点加入更多的东西。而且，从一个基本的、微小的原型(prototype)出发，逐步构建系统也是任何科学研究和程序设计、软件工程的一个基本方法。但是作者的这段话仍然深深地打动了我，对着这段文字我凝神良久，突然在一霎那有一种“顿悟”的感觉，它把我多年想表达但是表达不清或者不到位的思想，一步到位地说清楚了。我一直在找寻一种方法想把“形式语法理论”的基本思想、以及这种理论和其它语言学理论的区别说清楚，一次次尝试终无法如愿。这个区别，在Cresswell的论述中变得清澈透明，一眼望到底。这段话，现在看来有几个意义：第一，对初学者来说，当你跨进语言学大门的时候，应当意识到你将来的学习、研究的对象是什么？研究的方法是什么？第二，对于正在学习语言学而且有了一定基础的人来说，回过头来看已经学过的内容，应当问问自己，你真的相信你学的这些理论能够解决语言问题？第三，对于研习语言学多年，对各种语言学理论大致了解之后，就应当问问自己，我是否真的知道语言学是什么？ “语言学是什么”，这个问题在Cresswell的著作中被剖析的清清楚楚：要么你去研究各种纷繁复杂语言现象，汉语的、英语的，然后学习一些时髦的语言理论，再利用“代入法”用这些理论的现成结论说明所研究语言的某些现象；要么投入到各种抽象的形式系统，先找到一个安全的基础，确保自己将来赖以生存的理论基础不会被人“撤梯子”。然后，认真学习各种形式科学的理论，包括逻辑、数学、计算理论以及本体论和知识论，从中找到真正的科学方法，然后试着说明一小部分语言现象，并力图完全说清楚。前者，对于有世间承诺的人来说，例如升学、读研、毕业论文等显然是捷径，有数不清的文献资料、有众多的学长、老师可以帮助你，一句话，可利用资源无穷无尽。而后一种，没有人可以帮你，没有现成的道路，也没有众多的资源可以利用，唯一的指望就是你的读书与思考：读别人的书，想自己的路。第四，明确对自己的定位：当我说“语言学”的时候，我的真正意思是什么！按照Cresswell的划分，我自己可以说是从第一种过渡到第二种的那种类型，但是这种过渡是潜意识的，懵懵懂懂的，但是一旦明确了，我会毫不犹豫地将自己划分到第二种类型。那么第一种呢？直接对语言现象进行研究、特别是田野调查、归纳整理方言资料、抢救濒危语言等等，难道不是有意义的语言学研究？用计算机搞计算语言学研究，建立语料库对语言数据进行标注，做语言的数据分析，难道不是有意义的语言学研究？研究汉语，然后可以更有效地在全世界传播汉语和中国文化，难道不是有意义的语言学研究？掌握语言学理论，并将其运用到外语教学中去，使更多的人用更少的时间更高的效率学习外语，难道不是有意义的语言学研究？是的，就像是人类本身是个多面体一样，语言作为人类的精神、社会、民族、文化、地域等因素的综合结合体，有着多方面的研究角度和相应学科。而且对语言进行研究甚至根本不用什么语言学理论，而把语言现象当做一种半随机现象，以统计概率、模式识别和神经网络的方法也可以进行。因此，在某种意义上，对语言研究视角的选择其实也是你对语言学是什么这个问题的个性回答。Cresswell在阐述这个问题时强调的是“至少”有两种方法研究语言。选择“形式语法理论”就意味着，第一、相信自然语言是有规律的，尽管有许许多多的规律之外的”例外“。第二，人类不可能在最近的将来搞清楚语言理解和生成的大脑机制，任何以此为前提进行”假说“的理论都是靠不住的。第三，人类理性思维的最高形式是推理——逻辑推理，对这种推理的研究人类已经进行了两千年了，无论是中国、希腊还是印度，都具有悠久的逻辑研究传统。而作为明确的科学逻辑学——符号逻辑学在近代科学发展史上起到了引领、指南的作用，已成为多个学科共同的理论基础和灵感来源。第四，计算机科学的发展，使人类更深入地了解过去看似常识甚至比常识更微不足道的现象，而且这方面的研究更促进了哲学中本体论和知识论的研究，最大的收获就是，一些看以来非常trivial的现象和问题实际上比表面看上去复杂的问题更困难。而这些非常trivial的问题有时甚至成为某个学科产生发展的基本动机。而语言，作为人类天生来就掌握的技能，有许多是母语话者通过直觉就可以判断解决的问题，但是要想进行详细周密的分析，仍然需要像用显微镜那样的工具，和相应的科学方法，这就是形式语法理论的本质。作为汉语的使用者，我们的语言学研究迟早会转向我们的母语。而汉语，从西方语言学的传统动机来看，缺乏研究的意义(significance)，因为汉字转化为拉丁字母后，已经失去了汉语的”精血“，只剩下一些没有任何形态关联、令人感到无趣的开音节符号，没有曲折、没有时态、没有格、没有任何句法标识、不构成任何语言学意义上的兴趣。因此，站在西方语言学的角度，研究汉语动机的相当一部分不是出于语言学本身。汉语研究的未来应当是同时熟悉西方语言理论和汉语语言的中国的年轻学子。在吃透了西方语言学发展的基本动机、研究方法、哲学思想和使用工具的基础上，应当建立和西方语言学理论相对接的(compatible)的以汉语为基础的普世语言学理论。这个理论，也许在最近的将来不会出现，但只要有人在努力就一定有希望。对此，提出下列不成熟的想法和关心汉语研究的朋友分享： 1. 真正立足汉语本身的语言理论必须以汉字作为”原码“而绝对不可以转换成拉丁文字或任何拼音文字。 2. 由于”汉语“是一个非常模糊的概念，我们这里对汉语实例的定义只限制在它的书面形式：汉字串的集合，或者，汉字的文本。 3. 作为书面形式的汉语又分为文言文和白话文，但又不是绝对，白话文中掺杂文言也是现代汉语常见的现象，但是各自的组合规则却有着极大的不同。汉语的造句规则和造词规则是平行的。 4. 汉语没有西方语言的那些词尾变化、时态、没有性数格等feature，但是目前汉语的词类的分类仍然是在西方语言学中的八大品词分类的框架中，可以说是貌合神离，甚至是削足适履。 5. 汉语中其基本元素是汉字，而汉字的固定的物理成分只有形和义。在这个意义上进行汉语的研究，本质上就是研究汉字作为基本元素符号组合规律，包括造词规律、造句规律、或者作文规律。汉语的表达能力完全依赖于汉字千变万化的组合。因此，研究汉语，特别是从形式语法理论的角度研究汉语，其本质就是研究汉字的分布与组合规则。如果以上这些观点可以成立，那么，从逻辑——类型论——lambda演算——组合子逻辑开始就是一条非常有希望的研究路线。以上这些特别是关于汉语的想法可以说是我”独自“的想法，也是这些年来的学习后所获得的认知，这个认知如果用一句话概括就是——作为形式语言的自然语言。; 个人分类: 语言学|8150 次阅读|2 个评论

浅谈类型论——背景知识: 热度 1 saif 2017-1-10 06:24; 在语义学“闲聊”系列中，我们曾经把逻辑语义学归纳为对应理论，它的核心概念有两个：符号体系和模型。不过在这个系列中我们并没有严格区分“世界”和“模型”之间的关系，更多的内容是在符号与其它系统的对应关系上。世界，其实是一个非常模糊的概念，分开来看，“世”是指人类所处的自然和人类自身的环境的总称，而“界”则表示“范围”。因此引申来看，就是有一定范围的客体对象存在的环境、或者叫做空间。用这个引申定义我们就可以获得甚至创造各种不同的世界。我们“获得的”世界，例如我们身体所处的现实世界，媒体发布的新闻就是告诉你这个世界每天在发生什么。我们的身体内部是另一个世界。我们可以通过体表特征、诊断仪器或者专业人员（医生）的主观判断间接知道这个世界发生什么。我们可以“创造”世界，文学作品（包括文字、语音、影像）、电脑游戏、虚拟现实可以让我们体验一个和日常生活完全不同的世界。人类所谓的“知识”其实就是我们对各种“世界”认识、了解的概念体系：在这个体系中，有各种各样的“概念”，有对这些概念的陈述，有对概念和概念之间关系的陈述，如何从一个概念得到另一个概念的陈述。例如，玩电脑游戏就有通关秘籍，大概就是玩家对游戏中的世界认识了解后得到的“知识”。如果这些知识只是反映了个人的感觉、体验，那么这些知识一般会被称作“经验”(experience)。经验，是一种体会，是人的特定感官与某一特定世界互动（包括观察、体验、实践）中产生的知识和能力（技能）。这种知识通常有三个特点，第一、适用于特定、局部的事件和场景；第二、通常没有成体系的、或者说通用方法论支持，因此对已知知识、技能的掌握理解与宿主的“悟性”、天资有关；第三、由于前二个原因，作为学习者所得到知识能力高低参差、没有可预测性。俗话说“师傅领进门、修行在个人”，这表明经验的习得并不是一个均等的过程，每个人在这个过程中的获得并不相同。经验的另一种外在表现形式是物化的产品。这些产品的“能力”通过“效用”体现。而对效用的评估基础则是统计学原理。如果人类对世界的知识可以从小的局部认知归纳为大的局部认知，进而获得对某个世界“全局”的认知，这个“认知”就称为“理论”。如果对这个过程更详细地探究的话，基本上是这样一个过程：对某个事件、认识对象A总结出经验α；对另一个事件、认识对象B总结出经验β，对第三个事件、认识对象C总结出经验γ；后来，在（α、β、γ）中又发现了更一般的知识P，P不仅适用A，也可以适用B和C，这样我们的认知水平就提高了一个“层次”（order）。如果在完全不同的“世界”，也寻着这个过程得到知识Q，或许P与Q的层次相同，但适用的世界、要解决的问题、应对的事件和对象完全不同，如果我们剥离具体事象，发现其共同之处，亦即、在（P、Q）发现了层级更高的知识𝜞，那么说明我们对世界的认识又有了更高层次的认识。可以说，人类的所有科学活动都是在重复这个过程。读者可根据自己的专业进行相应脑补，这里就不在举例。这是人类对世界的认识过程。不过作为后来人，我们学习前人已经掌握的知识并将获取的知识向下一代传承时，我们所经历的过程往往是相反的。通常是先得到概念，定义，换句话说就是，学习者和知识发现者的认知过程是相反的：从抽象到具体。在国内、或者说在东亚，这种状况可以说达到了极致：我们的大脑通常是在没有任何时空背景的情况下“突然”被塞进许多莫名的“概念”、“定义”，“规则”，然后就是一堆习题。我们的任务就是将这些东西背下来，然后通过大量的习题建立大脑与这些“概念、定义、规则”的机械式条件反射，这就造成了21世纪中国人的“前端知识”发达而“后端知识”严重欠缺的现象。许多人的文章、深奥名词、概念、公式满天飞，令人景仰，但令人无法接近（inaccessible），因为在这些大多数人看不懂的符号、概念公式之后我们无法判断其背后的思想，更无法知道作者要表达什么。当然，如果是给同行看的学术论文这无可厚非，但更多的则是高深符号背后的思想浅薄。用我们以前的语义学术语说就是：既不知道名称、符号的指称义也不知道它们感知义。我们唯一的印象就是作者很高大上，说出一些我们这些凡人外行听不懂看不明白的句子；而且我们必须要学会装作很欣赏，试着说和作者“同水平”句子，否则、否则…（画外音）“就你这水平（做鄙视态）…”。 “前端知识”、“后端知识”是我的造语，意思是，我们很多人的知识停留在前人总结过的概念、定义和总结上，而对这些知识的纵向来由和横向的结构关系并不了解，对其底层的思想更无兴趣追究。这跟我们要讨论的“类型论”有什么关系？类型论是这样一种学科，它试图要把我们要阐述的概念说清楚。把概念说清楚其实包括两个层面：一种是种类的区别，例如橘子和苹果的差别，或者下位种类的区别，例如橘和柑的区别；另一种是概念层级或者说抽象度的区别：3头牛、3只鸡和3的区别、3,4,5和自然数的区别，自然数和数的区别。对前一种区分，数学、逻辑和哲学的研究所使用的主要工具是集合论，而后一种就是我们要讨论的类型论。而对这些思想的表述就是我们前面提到过的逻辑语言。语义论研究的是符号系统和模型之间的关系，而类型论则是研究模型本身。而模型中的概念定义首要条件就是每个概念的定义、推理不会产生矛盾。所谓产生矛盾是这样一种情况：概念A本身没问题，概念B本身也没问题，但是用概念A或者用概念B适用于A或B自身时所产生的命题却是永假，或者概念A与概念B相互适用时也出现命题永假的情况。这个问题我们以后再详谈，这里只想说“类型论”是我们认识知识本源的工具。这里并不想把“类型论”形容成“心灵鸡汤”，但是透过这个理论背后的思想而不是那些唬人的拉丁字母、希腊字母符号我们确实能感受到其哲学的深邃。牛顿创建了“牛顿三定律”最终却走向神学，19世纪末20世纪初的许多数学家最后的归宿却是哲学，而历经300百年的分析学最后的问题最终归结到“什么是数”这样一个如此“纯真”的问题。说明什么？简单的东西后面有着深刻的思想，复杂的、令人无法理解的东西可能掩盖着思想的贫乏和哲学的贫困。扯远了，现在我们回到正题：类型论是对我们对世界“建模”所产生的“模型”的研究。而“模型”就其哲学意义来说是我们对某一特定领域的概念体系。对这个概念体系的第一要求，就是我们上面所说，概念间不能出现矛盾。我们下面要谈的“模型”概念，可能比一些专业人士心目中的所谓“数学模型”——用一些统计概念公式或其它什么公式的表示稍微宽泛一些。它的具体内涵就是，我们如何表达从（P、Q）上升为𝜞的知识。第一个问题便是，用什么语言？第二个问题是，如何确定模型？如果我们把概念看做是一个“知识”的最基本“片段”（a fundamental piece），那么如何确定这个“片段”？如何保证这个知识“片段”和其它知识“片段”的“和谐”从而使这个模型体系不会出现前后不一致从而保证其完整性？所有知识片段的组合所形成的架构是什么样的？而第三个问题是：如何建立世界与模型的对应关系？亦即，所建模的原始对象和模型中元素的对应关系是什么？对这三个问题，我们先从第三个问题谈起。如果说我们初始的经验知识（α、β、γ）是对我们日常上千次上万次体验的总结，使我们在面对同样情况、事件、对象不必从头思考，那么这个总结过程我们就可以看做是“抽象”，这里的“抽象”用作动词：排除每次经历中无关紧要的部分和没有共同点的部分，归纳出共同点和通用点，形成第一次认识上的“飞跃”（毛泽东《实践论》语）。如果将“抽象”得来的知识通过一种特定的语言表达出来，我们就可以将这种语言所表述的客体、事件、事实看做是“模型”。例如做菜用的“菜谱”就是可以看做是面对“做菜”这个事件的“模型”：它舍弃了许多和做菜通用规律无关的细节，例如，到哪里去买食材、用什么品牌的调味品、使用的加热器是煤气炉还是电炉还是烧煤炉等等，只将做菜所必须、而且每次通用的部分【按顺序】列出，并给出流程实施时必要的参数：需要的食材种类、数量（份量）、调味料的多少、火候的大小、加热时间长短等。可以说，一个菜谱就是应对做某道菜这个事件的抽象模型。当然，如果有人从做菜“悟”到了别的什么，使得菜谱中的一些法则适用于比做菜这个事件更大的范围（也就是我们所说的其它世界），那么，菜谱中所含的抽象就升高到另外一个层次。例如，我们可以把菜谱中“做菜”这一场景“虚化”，从中抽取到“流程”（procedure）和“参数”（parameter），最后我们看到不仅是做菜，所有解决问题的过程都是如此，如果我们可以让这个过程变成机械的、通用的过程，亦即不必再费思量地每次要考虑每次流程的具体情况，那么这个模型所对应的世界就不在仅仅限于做菜，也不仅限于具体的操作流程，而变成一种通用“理论”，那么，这个模型就称为人类通用知识的一部分。而且反过来，这个诞生于厨房的知识就可以用在意想不到的其它领域，例如计算机科学。因此，模型的本质是所对应的世界，说白了就是所适用的场景。世界的范围决定了模型的通用程度。如果我们可以从现实世界抽取到“流程”和“参数”这样抽象的概念，那么，我们的模型要回答的下一个问题是，对一个特定的“流程”，我们是否可以接纳所有现实世界的对象作为“参数”？如果答案是“否”，那么下一个问题就是：如何确定参数，换句话说就是什么样的对象可以作为这个流程的操作对象。正如我们上面所述，代表世间对象的种类区分有两种，一是种属不同，二是层次不同，这个层次更正规的说法就是“阶”（order）。而类型论的核心就是研究后者。因此从最广泛的意义上说，类型论的研究属于数学与哲学的范围。数学和哲学，大概是人类历史上最通用的知识了。数学，不用说，它是人类所有知识体系中最严格、最理性的领域。而哲学，则是一个宽泛的具有多种歧义的概念。我们这里所说的哲学大致上是指以逻辑作为推理法则的、以探讨哲学基本问题：存在和概念为中心内容的思想体系，可以容纳在这个体系的具体学说包括19世纪中叶兴起的分析哲学以及后续的各种学派，包括逻辑主义、形式主义、直觉主义和结构主义，以及从这些学派派生的现代哲学流派。从性质上来说，大致属于“科学哲学”的范畴，从而排除了其它包括宗教哲学、历史哲学、伦理哲学以及辩证哲学、艺术哲学、美学哲学等专注于某个人文科学领域的哲学学说。具体地说这样的哲学包括了两大领域：本体论（ontology）和知识论（epistemology），前者探讨的问题是哲学的中心问题：什么是存在？后者讨论的问题是：概念世界的结构以及这个结构的形式化表达。我们所讨论的类型论在这些学科中的作用就是，我们对世界的认知模型如何建立，在这个模型中的概念，我们如果区分，区分的依据是什么？而数学则是一个特殊领域。虽然数学在现实世界中，有着广泛的应用，许多数学概念也具有现实世界的实用背景，但最为一个体系，数学的世界仍然是个“先验”的体系，数学领域的成果不是对自然界某些现象的发现，而是证明，纯粹的理性推理结果。因此和其它领域不同的是，数学世界和为其建立的模型实际上是不同概念体系之间的对应。例如自然数所对应的模型是数轴、有序对对应的模型是二维平面等。而类型论则是在这些形式系统中出现的个体对象发现其恰当的适用范围和精确的定义。这样就引申出一个问题：建构模型的基础是什么？对这个问题的探讨是形式科学最本质的问题，也是数学哲学讨论的基本问题。这个问题就是：在一个形式系统中，最小的原始元素是什么？它们是如何聚合在一起构成更大的单位，最终形成一个统一的系统？这些原始的、中间的元素之间有着什么样的关系，它们之间又是如何互动从而产生新的元素？对这个问题的答案很多，但大致归纳起来有两大类：第一，存在性；第二，建构性。存在性的意思是，形式系统内的所有元素，首先要证明它们的存在，而证明的手段，就是符号逻辑；而建构性是指，只要通过一定的程式、规则“建立”其元素我们就可以证明其存在。第一种存在性，就是大部分数学定理证明的理论依据，亦即，一个假说、猜想只有通过数学证明才能证明其存在（假说、猜想为真）；而现代计算机程序则是建构性的典型案例：如何知道最大公约数存在？通过一个算法，在机器上实现这个算法，对给定的一组数，得到相应的公约数，从而“证明其存在”。而无论是存在论还是建构论其实都面对着一个共同的问题：那就是形式系统的“结构”。学数学的大概都知道布尔巴基学派，这个学派曾经试图统一所有的数学领域，提出所有数学问题都可以归结为“数学结构”问题，“结构”是统一所有数学分支的一般性概念。虽然到目前为止这个观点并未被所有学者接受，但是在实际的科学活动中结构已成为解释一般形式系统的最基础概念。例如，在“结构”这个概念下，构成“结构”的基本组成部分的“集合”，确实已经成为数学各个分支的共同概念和基础。而现代代数学，以“结构”为基本思想，其研究对象“群、环、域”等，已经超出了对数的研究，开始走向更一般的对象的结构的研究，产生了“泛代数”（universal algebra）这样的数学分支。因此，结构是我们建立论域模型的基础。我们将在今后的讨论中详细探讨结构的概念，这里只勾勒一个大概的全景图： 1. 问题的论域（universe of discourse），它的数学表示就是一个集合； 2. 论域内的对象（object）：对象可以是单个原子元素，也可以是原子元素的集合，亦即、在论域集合上的子集。有些理论将函数看做论域的基本元素，不过这里“函数”的概念已经超出了传统的数学观念，甚至比计算机程序设计语言中的“函数”概念还要宽泛，例如组合逻辑以及其后续发展的组合范畴逻辑，这里暂且不表，我们仍然利用直观的“个体”、“属性”等表示论域中的基本对象。 3. 对论域元素的操作（operation）：可以陈述论域元素的性质、论域元素的关系，以及从给定元素产生新元素的操作方法和规则；这样的一个系统，我们就称之为结构。下面我们谈谈上述的第一个问题：语言问题。首先要说的是，什么是语言？美国生成语法学家乔姆斯基把语言形式化地定义为“句子的集合”，更确切地说就是：给定一个语法，由这个语法所能产生的所有合法句子的总和就是语言。这个定义明确、清晰，因为在生成语法的语境下我们可以明确定义语法，可以明确定义什么是语言理论，因此作为语言理论-语法-句子的集合-语言的派生过程是透明的。不过这个定义的一个缺陷就是没有定义语言的与其它系统的对应关系，亦即语义。当然，从语言的形式化研究角度语义并不是一个语言成立的必要条件，尤其是非自然语言的研究。但是，当一个语言要被用来表示某个模型时，语义就是语言研究的重点了。在我们研究类型论时，我们所关心的仍然是对模型的精确、严格的描述问题，因此最合适的语言就非形式语言莫属。当下最成熟的形式语言有两类：逻辑语言和计算机程序设计语言。但是对这两种语言的语义研究前者比后者更加成熟，故我们这里只考虑前者。基于这个思想我们这里所指的语言，基本上沿袭了乔氏的定义：语言是句子的集合，不过，由于我们的语言是用来表述（denote）某个特定的模型，因此只说语言是句子的集合就远远不够了，应当是：对于某个特定的模型，使得所定义的语言是由其命题为真的句子组成，这样的句子我们称之为“断言”（assertion）。站在语言的角度，我们通常把“模型”说成是“论域”（universe of discourse）。而作为语言研究的基本内容包括了句法（syntax）和语义（semantics）。而作为对模型的完整描述，语言还要包含一套推理规则（deductive rules），这个规则的目的就是在确定了对论域一小部分对象的断言之后，能够得到新的断言，前者我们称作“公理”、“定义”，后者称之为“定理”。其中，“公理”、“定义”是原生的，所以又称为“设定”（assumption），而定理则是派生而来，因此其明确的派生、推理过程——证明就是这个语言的重要部分。证明对于模型本身也是很重要的，其中哥德尔的最伟大成就就是确认了模型与证明之间的关系。关于这个问题，我们以后再谈。这里想强调的就是：语言问题是现代逻辑学、数学和哲学研究的中心问题之一。关于第二个问题，如何确定模型？如何确定模型的基本元素，如何从基本元素派生新的元素，如何保证整个模型不会出现前后矛盾？对这些问题的回答，就不是一两句话就可以说清楚了。例如我们上面提到了“流程”，如何保证一个“流程”可以完成预期的任务？如果这个“流程”只能在“理论上”可以完成任务但现实中所需要占用的资源大大超出了我们的预期，造成实际上无法完成任务。最重要一点，我们如何事先知道这个流程能否有“能力”完成预期任务？它对“参数”的限制是什么？例如，如果这个流程拿自己当参数加入到该流程中会产生什么？这一系列的问题，催生了许多边缘学科，如计算理论，包括可计算性和计算复杂性、可计算函数（前二者可归约成后者）、递归函数理论，以及我们现在正在讨论的类型论以及相应的形式化——λ-演算。我们无法在这样的小文中探讨所有这些题目，类型论是我们当前关注的重点。但有一点是要记住的：这些学科并不是互相孤立地存在，相互之间你中有我我中有你，我们在探讨类型论时，随时会谈到上述有关的话题。最后，我们应当了解的是，除了集合论、类型论之外，从上个世纪40年代开始又出现了范畴论，其目的和类型论相似，但基本思想或者说对问题的接近方法（approach）却大不相同，核心概念是映射叠加和同构，该理论目前已成为理论计算机科学的一个热点。不过，集合论、类型论和范畴论，其哲学理念是想通的，按我的理解是对哲学观念的数学化。; 个人分类: 计算|2297 次阅读|1 个评论

浅谈类型论——开场白: saif 2016-12-27 01:32; 信息时代，计算所带来的科技革命彻底改变了我们的生活。一些人，一只手机在手忘记所有；一些人的网瘾堪比毒瘾，戒网戒手机已经成为21世纪初叶的心灵鸡汤，但这种景象在30年前还是难以想象的。如果你喜爱电脑，或许你还会喜欢编程。如果你喜欢编程那你一定会有心仪的程序语言；如果你懂编程语言，你或许知道面向对象和函数式编程；如果你恰好懂得函数式编程，有很大的几率你知道lambda演算，monad，但是你知道类型论吗？懂得类型论的人肯定不多，但是所有人都知道“类型”意思。类型，是一个常用词，分开看，类，物以类聚，人以群分，所以相似的对象、观念、思想我们可以归类；型，相当于一个模子，归纳一系列相似的行为、操作、流程，所以“型”又叫模式。这样看，类型其实是人类认识世界最有效的工具，用类型我们可以将世界上成千上万数也数不清的“东西”归纳成让大脑可以容纳的“类”，而“类”的性质、行为、动作可以归纳成“型”——模式，也就是我们常说的“行为模式”。类和型放在一起，就可以看做是有相同或相似行为模式的类的聚集。如果你恰好对计算机编程感兴趣，那么类型对你就有了更实在的现实意义。你知道同样是3，它的类型可能是字符也可能是数字。任何一个普通名词都可能是一种类型。从哲学的角度，类型回答了一个本体论的核心问题：什么是存在？一个实体的类型就是它存在的理由。而且客体所具有的类型越多对我们人类来说就越容易认知。如果把“幸福”当做一种类型，能说清楚它的真正意义的大概只有哲学家，而把“有车有房”当做一种类型的话，那么人人都是哲学家。但是，什么是“类型论”？这里，我们先说它不是什么。它不是人生哲学，不是心灵鸡汤，不是致富法门，更不是命理算术。类型论是一门精密严谨的科学，它即枯燥又有趣，对它的学习过程，是一种典型的“痛并快乐着”的体验。类型论在科学花园中的位置，大概处于数学、逻辑、计算和语言学的交界处，可以说它生于逻辑，长于数学，开花于计算机科学，结果于语言学。用不那么修辞式的直白说法就是：类型论是20世纪初为为解决逻辑悖论问题提出的解决方案，但是对类型论的形式化研究一直是在数学领域，类型论研究直接导致了一种计算模型的出现，成为理论计算机科学中一个重要分支。对类型的哲学讨论，虽然可以追溯到古希腊亚里士多德时代，但是近现代哲学、特别是数学哲学对类型论的讨论被认为是从弗雷格开始。而Richard Montague从上世纪70年代开始提出了基于内涵逻辑和类型论的语义学，从此类型论成为语言学中重要的工具。作为和图灵机并列的计算模型，类型论在计算机刚刚面世的10几年中并未如前者成为理论计算机科学的支配性模型，它大器晚成，直到上世纪60年代之后才逐渐为人所重视，并有所发展。其中最重大的成果就是将逻辑学中的证明论和类型论统一为一种理论。如果说图灵机是在无限长度纸带的读写过程，将计算的模型归结为是自动机，一种机器模型，那么，类型论则把计算模型当做可计算函数，它所研究的就是抽象意义的函数，它抽掉了通常数学意义的函数概念，没有数的概念，它抽掉了函数的处理过程的概念，研究函数的本质，将函数这个概念，上升到一种哲学的高度。对类型论的形式化表述，是一种介于数学和逻辑的语言，称作λ-演算，或者lambda演算，或者全中文：兰姆达演算。而在当代，这种模型逐渐成为显学，具体的表现形式就是另一种编程范式——函数式编程在上世纪80年代的兴起。类型论的出现，打破了学科之间的藩篱，让一些表面看上去毫无关联的是东西表露出其实是一件东西的本质。类型论使得函数概念不再是数学和逻辑的专利，它使得函数深入到哲学、语言学等领域。如果能对类型论有一定的理解，那么也会让我们以一种统一的模式看待数学、逻辑、计算、语言学和哲学。这也是科学的进步本质之一：用更加统一的、更加简单的模式理解这个复杂世界。本系列小文，将探讨类型论的前世今生，但不会讨论函数式编程，更不会讨论特定的编程语言，因为这方面的资源很多。我们只讨论类型论的演进过程，在历史和现实中的作用，以及它的基本内容。如果你恰好也想了解类型论的理论，那么这将是一次激动人心之旅，因为我们将看到数学、逻辑、哲学、计算和语言学中许多不同的概念如何可以统一在类型论下。中世纪的经院哲学家托马斯·阿奎那曾经说过： One should realize...that if we consider these four, namely wine, king, woman, and truth, in themselves they are not comparable because they do not belong to the same genus. Nevertheless, if they are considered in relation to some effect, they coincide in one aspect, and so can be compared each other. （应当认识到，当我们在孤立地(in themselves)谈论这些概念，亦即，红酒、国王、女人和真理时，它们是没有可比性的，因为并不属于同一类别。但是如果将其放在某种效应的关系上谈论，这些概念将在某个方面重合使得我们可以对其相互比较。）; 个人分类: 计算|4492 次阅读|0 个评论

更多...

帐号		自动登录	找回密码
密码			注册

关闭 安全验证

标签: 类型论

相关帖子

相关日志

关闭安全验证