比浏览器更快的访问！
43 关系: 停机问题，可计算函数，可计算性，可數集，外延性，巴科斯范式，上下文无关文法，不动点组合子，形式系統，归纳法，当且仅当，列表構造函數，函式庫，函数，图灵机，Beta范式，第一類物件，等价关系，结合律，组合子逻辑，罗素悖论，真值，階乘，高阶函数，语法糖，阿隆佐·邱奇，邱奇-图灵论题，邱奇数，链表，自由变量和约束变量，自然数，集合，逻辑运算符，递归，递归函数，Haskell，LISP，ML语言，SKI组合子演算，柯里化，歸約，決定性問題，有类型λ演算。
停机问题
停机问题（）是逻辑数学中可计算性理论的一个问题。通俗地说，停机问题就是判断任意一个程序是否能在有限的时间之内结束运行的问题。该问题等价于如下的判定问题：是否存在一个程序P，对于任意输入的程序w，能够判断w会在有限时间内结束或者死循环。 艾伦·图灵在1936年用對角論證法证明了，不存在解决停机问题的通用算法。这个证明的关键在于对计算机和程序的数学定义，这被称为图灵机。停机问题在图灵机上是不可判定问题。这是最早提出的决定性问题之一。 用数学语言描述，则其本质问题为: 给定一个图灵机T，和一个任意语言集合S，是否T会最终停机于每一个 s \in S。其意义相同于可确定语言。显然任意有限 S 是可判定性的，可数的（countable）S 也是可停机的。 停机问题包含了自我指涉，本质是一阶逻辑的不自洽性和不完备性，类似的命题有理发师悖论、全能悖论等。.
可计算函数
在可计算性理论中，可计算函数（computable function）或图灵可计算函数是研究的基本对象。它们使我们直觉上的算法概念更加精确。使用可计算函数来讨论可计算性而不提及任何具体的计算模型，如图灵机或寄存器机。但是它们的定义必须提及某种特殊的计算模型。 在可计算函数的精确定义之前，数学家经常使用非正式术语可有效计算的。这个术语因此可以被认同为可计算函数。尽管这些函数被叫做有效的，它们可能极其困难。可行可计算性和计算复杂性研究可有效计算的函数。 依据邱奇-图灵论题，可计算函数精确的是使用给出无限数量的时间和存储空间的机器计算设备来计算的函数。等价的说，这个论题声称有算法的任何函数都是可计算的。 可以使用Blum公理来在可计算函数的集合上定义抽象计算复杂性理论。在计算复杂性理论中，确定一个可计算函数的复杂性的问题叫做功能性问题。.
可计算性
可计算性（calculability）是指一个实际问题是否可以使用计算机来解决．从广义上讲如“为我烹制一个汉堡”这样的问题是无法用计算机来解决的（至少在目前）．而计算机本身的优势在于数值计算，因此可计算性通常指这一类问题是否可以用计算机解决．事实上，很多非数值问题（比如文字识别，图象处理等）都可以通过转化成为数值问题来交给计算机处理，但是一个可以使用计算机解决的问题应该被定义为“可以在有限步骤内被解决的问题”，故哥德巴赫猜想这样的问题是不属于“可计算问题”之列的，因为计算机没有办法给出数学意义上的证明，因此也没有任何理由期待计算机能解决世界上所有的问题．分析某个问题的可计算性意义重大，它使得人们不必浪费时间在不可能解决的问题上（因而可以尽早转而使用除计算机以外更加有效的手段），集中资源在可以解决的问题上．.
可數集
在数学上，可数集，或称可列集、可数无穷集合，是与自然数集的某个子集具有相同基數（等势）的集合。在这个意义下不是可数集的集合称为不可数集。这个术语是康托尔创造的。可数集的元素，正如其名，是“可以计数”的：尽管计数永远无法终止，集合中每一个特定的元素都将对应一个自然数。 “可数集”这个术语也可以代表能和自然数集本身一一对应的集合。例子参见两个定义的差别在于有限集合在前者中算作可数集，而在后者中不算作可数集。 为了避免歧义，前一种意义上的可数有时称为至多可数，参见.
外延性
在数学中，外延性通常指称某种形式的。可追溯到莱布尼兹的原理，两个数学对象是相等的，如果没有区分它们的检验。例如，给出两个数学函数 f 和 g，我们可以说它们是相等的，如果 对于在公共函数域 X 内的所有 x。这种外延相等是平常的定义，如果函数范围 Y 对于两个也是公共的。在另一方面，如果我们在类型论的意义上通过附着到它们上的数据来区分函数，这样我们可以选择一个更大的集合比如 Z 作为它们之一的范围，则这种相等不同于“外延”意义的相等。这种意义下外延性可能会失败。另一种意义的相等考虑“函数被计算的过程”，如果这么考虑，通常会同外延性相抵触。 在公理化集合论中，外延性被表达为外延公理，它声称两个集合是相等的，当且仅当它们包含相同的元素。在 lambda 演算中，外延性被表达为 eta-变换规则，它允许在指示相同函数的任何两个表达式之间的转换。.
巴科斯范式
巴科斯范式（Backus Normal Form，縮寫為 BNF），又称为巴科斯-诺尔范式（Backus-Naur Form，縮寫同樣為 BNF，也譯为巴科斯-瑙尔范式、巴克斯-诺尔范式），是一种用于表示上下文无关文法的语言，上下文无关文法描述了一类形式语言。它是由约翰·巴科斯（John Backus）和彼得·诺尔（Peter Naur）首先引入的用来描述计算机语言语法的符号集。 尽管巴科斯范式也能表示一部分自然语言的语法，它还是更广泛地使用于程序设计语言、指令集、通信协议的语法表示中。大多数程序设计语言或者形式语义方面的教科书都采用巴科斯范式。在各种文献中还存在巴科斯范式的一些变体，如扩展巴科斯范式 EBNF 或扩充巴科斯范式 ABNF。.
上下文无关文法
上下文无关文法（context-free grammar，縮寫為CFG），在计算机科学中，若一个形式文法 G.
新！!: Λ演算和上下文无关文法 · 查看更多 »
不动点组合子
不动点组合子（Fixed-point combinator，或不动点算子）是计算其他函数的一个不动点的高阶函数。 函数 f 的不动點是將函數應用在輸入值 x 時，會傳回與輸出值相同的值，使得 f(x).
新！!: Λ演算和不动点组合子 · 查看更多 »
形式系統
在邏輯與數學中，一個形式系統（Formal system）是由兩個部分組成的，一個形式语言加上一個推理規則或轉換規則的集合。一個形式系統也許是純粹抽象地制定出來，只是為了研究其自身。另一方面，也可能是為了描述真實現象或客觀現實的領域而設計的。.
归纳法
归纳法可以指：.
当且仅当
当且仅当（If and only if）（中国大陆又称作当且--仅当，臺灣又称作若且--唯若），在--邏輯中，逻辑算符反互斥或閘（exclusive or）是对两个运算元的一种邏輯分析类型，符号为XNOR或ENOR或\Leftrightarrow。与一般的邏輯或非NOR不同，當兩兩數值相同為是，而數值不同時為否。在数学、哲学、逻辑学以及其他一些技术性领域中被用来表示“在，并且仅仅在这些条件成立的时候”之意，在英语中的对应标记为iff。“A当且仅当B”其他等价的说法有“当且仅当A則B”；“A是B的充分必要条件（充要條件）”。 一般而言，當我們看到“A当且仅当B”，我們可以知道“如果A成立時，則B一定成立；如果B成立時，則A也一定成立”；“如果A不成立時，則B一定不成立；如果B不成立時，則A也一定不成立”。.
列表構造函數
列表構造函數是用來構造列表的基本函數，在大多數 LISP 體系的計算機編程語言中，使用的函數名稱是cons。 cons構成了存放兩個變量與其指針的記憶體物件，這個物件被稱為（cons）單元、非原子的 S 表達式或（cons 對）。LISP 編程中表達要把 x 加入 y 的語法：(cons x y)，構造了一個新物件。產生的結果具備了左半部，稱為car（第一元素或暫存器位址的內容）；以及右半部稱為cdr（其餘元素或遞減暫存器的內容）。 以上約略地和物件導向的構造器概念相關，即產生一個給定參數的新物件，而其與代數數據類型系統的構造函數，有更密切相關。“cons”和諸如“cons onto”的詞句，也是函數編程的通用術語。有時運算子有類似作用，特別是在列表處理的情況下，被讀作“CONS”。（例如 ML，Scala，F＃和 Elm 編程的::運算符，或 Haskell 編程的:運算符，都是向列表的開頭添加一個元素。）.
新！!: Λ演算和列表構造函數 · 查看更多 »
函式庫
在计算机科学中，库（library）是用于开发软件的子程序集合。库和可执行文件的区别是，库不是独立程序，他们是向其他程序提供服务的代码。 库链接是指把一个或多个库包括到程序中，有两种链接形式：静态链接和动态链接，相应的，前者链接的库叫做静态库后者的叫做动态库。.
函数
函數在數學中為兩集合間的一種對應關係：輸入值集合中的每項元素皆能對應唯一一項輸出值集合中的元素。例如實數x對應到其平方x2的關係就是一個函數，若以3作為此函數的輸入值，所得的輸出值便是9。 為方便起見，一般做法是以符號f,g,h等等來指代一個函數。若函數f以x作為輸入值，則其輸出值一般寫作f(x)，讀作f of x。上述的平方函數關係寫成數學式記為f(x).
图灵机
图灵机（），又称确定型图灵机，是英国数学家艾倫·图灵于1936年提出的一种抽象计算模型，其更抽象的意义为一种数学逻辑机，可以看作等价于任何有限逻辑数学过程的终极强大逻辑机器。.
Beta范式
在 lambda 演算中，一个项是beta 范式（规范型），如果没有“beta 归约”是可能的。一个项是 beta-eta 范式，如果既没有 beta 归约又没有“eta 归约”是可能的。一个项是头部范式，如果没有“在头部位置的 beta-可规约式”。.
新！!: Λ演算和Beta范式 · 查看更多 »
第一類物件
一類物件（First-class object）在電腦科學中指可以在執行期創造並作為參數傳遞給其他函數或存入一個變數的實體。將一個實體變為第一類物件的過程叫做「物件化」（Reification）。 「第一類物件」這一名稱最早由克里斯托弗·斯特雷奇在1960年代發明，原稱「第一類公民」（First-class citizen），意指函數可作為電腦語言中的第一類公民。英文中也稱「First-class entity」或「First-class value」。.
等价关系
等價關係（equivalence relation）即设R是某個集合A上的一个二元关系。若R满足以下條件：.
结合律
在數學中，結合律(associative laws)是二元運算可以有的一個性質，意指在一個包含有二個以上的可結合運算子的表示式，只要運算元的位置沒有改變，其運算的順序就不會對運算出來的值有影響。亦即，重新排列表示式中的括號並不會改變其值。例如： 上式中的括號雖然重新排列了，但表示式的值依然不變。當這在任何實數的加法上都成立時，我們說「實數的加法是一個可結合的運算」。 結合律不應該和交換律相混淆。交換律會改變表示式中運算元的位置，而結合律則不會。例如： 是一個結合律的例子，因為其中的括號改變了（且因此運算子在運算中的順序也改變了），而運算元5、2、1則在原來的位置中。再來， 則不是一個結合律的例子，因為運算元2和5的位置互換了。 可結合的運算在數學中是很常見的，且事實上，大多數的代數結構確實會需要它們的二元運算是可結合的。不過，也有許多重要且有趣的運算是不可結合的；其中一個簡單的例子為向量積。.
组合子逻辑
组合子逻辑是Moses Schönfinkel和哈斯凱爾·加里介入的一种符号系统，用来消除数理逻辑中对变量的需要。它最近在计算机科学中被用做计算的理论模型和设计函数式编程语言的基础。它所基于的组合子是只使用函数应用或早先定义的组合子来定义从它们的参数得出的结果的高阶函数。.
罗素悖论
罗素悖论（Russell's paradox），也称为理发师悖论，是英國哲學家罗素於1901年提出的悖论，一个关于类的内涵问题。罗素悖论当时的提出，造成了第三次数学危机。.
真值
在逻辑中，真值（truth value），又稱逻辑值（logical value），是指示一个陈述在什么程度上是真的。在計算機編程上多稱做布林值、布爾值。 在经典逻辑中，唯一可能的真值是真和假。但在其他逻辑中其他真值也是可能的：模糊逻辑和其他形式的多值逻辑使用比简单的真和假更多的真值。 在代数上说，集合形成了简单的布尔代数。可以把其他布尔代数用作多值逻辑中的真值集合，但直觉主义逻辑把布尔代数推广为海廷代数。 在topos理论中，topos的主客对象分类器接管了真值集合的位置。.
階乘
一个正整数的階乘（factorial）是所有小於及等於該數的正整數的積，并且有0的阶乘为1。自然數n的階乘寫作n!。1808年，基斯頓·卡曼引進這個表示法。 亦即n!.
高阶函数
在数学和计算机科学中，高阶函数是至少满足下列一个条件的函数：.
语法糖
语法糖（Syntactic sugar），也译为糖衣语法，是由英国计算机科学家彼得·蘭丁发明的一个术语，指计算机语言中添加的某种语法，这种语法对语言的功能没有影响，但是更方便程序员使用。语法糖让程序更加简洁，有更高的可读性。 举例来说，许多程序语言提供专门的语法来对数组中的元素进行引用和更新。从理论上来讲，一个数组元素的引用涉及到两个参数：数组和下标向量，比如这样的表达式，get_array(Array, vector(i, j))。然而，许多语言支持这样直接引用 Array。同理，数组元素的更新涉及到三个参数，set_array(Array, vector(i, j), value)，但是很多语言提供这样直接赋值，Array.
阿隆佐·邱奇
阿隆佐·邱奇（Alonzo Church，）是美国数学家，1936年发表可计算函数的第一份精确定义，对算法理论的系统发展做出巨大贡献。邱奇在普林斯顿大学受教并工作四十年，曾任数学与哲学教授。1967年迁往加利福尼亚大学洛杉矶分校。 解决算法问题包括构造一个能解决某一指定集及其他相关集的算法，如果该算法无法构建，则表明该问题是不可解的。证明此种问题不可解性的定理是算法理论中的一大突破，邱奇的算法即为该类算法的首例。邱奇证明了基本几何问题的算法不可解性。同时证明了一阶逻辑中真命题全集的解法问题是不可解的。.
新！!: Λ演算和阿隆佐·邱奇 · 查看更多 »
邱奇-图灵论题
#重定向 邱奇－图灵论题.
新！!: Λ演算和邱奇-图灵论题 · 查看更多 »
邱奇数
邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式，最常见的形式是邱奇数，它是使用lambda符号的自然数的表示法。这种方法得名于阿隆佐·邱奇，他首先以这种方法把数据编码到lambda演算中。 在其他符号系统中通常被认定为基本的项（比如整数、布尔值、有序对、列表和tagged unions）都被映射到使用 邱奇编码的高阶函数；根据邱奇-图灵论题我们知道任何可计算的运算符（和它的运算数）都可以用邱奇编码表示。 很多学数学的学生熟悉可计算函数集合的哥德尔编号；邱奇编码是定义在lambda抽象而不是自然数上的等价运算。.
链表
链表（Linked list）是一种常见的基础数据结构，是一种线性表，但是并不会按线性的顺序存储数据，而是在每一个节点里存到下一个节点的指针(Pointer)。由于不必须按顺序存储，链表在插入的时候可以达到O(1)的复杂度，比另一种线性表顺序表快得多，但是查找一个节点或者访问特定编号的节点则需要O(n)的时间，而顺序表相应的时间复杂度分别是O(logn)和O(1)。 使用链表结构可以克服数组链表需要预先知道数据大小的缺点，链表结构可以充分利用计算机内存空间，实现灵活的内存动态管理。但是链表失去了数组随机读取的优点，同时链表由于增加了结点的指针域，空间开销比较大。 在计算机科学中，链表作为一种基础的数据结构可以用来生成其它类型的数据结构。链表通常由一连串节点组成，每个节点包含任意的实例数据（data fields）和一或两个用来指向上一个/或下一个节点的位置的链接（"links"）。链表最明显的好处就是，常规数组排列关联项目的方式可能不同于这些数据项目在记忆体或磁盘上顺序，数据的存取往往要在不同的排列顺序中转换。而链表是一种自我指示数据类型，因为它包含指向另一个相同类型的数据的指针（链接）。链表允许插入和移除表上任意位置上的节点，但是不允许随机存取。链表有很多种不同的类型：单向链表，双向链表以及循环链表。 链表可以在多种编程语言中实现。像Lisp和Scheme这样的语言的内建数据类型中就包含了链表的存取和操作。程序语言或面向对象语言，如C/C++和Java依靠易变工具来生成链表。.
自由变量和约束变量
在数学和其他涉及形式语言的学科中，包括数理逻辑和计算机科学，自由变量是在表达式中用于表示一个位置或一些位置的符号，某些明确的代换可以在其中发生，或某些运算（比如总和或量化）可以在其上发生。这个概念有关于占位符（它是以后会被所替换），或表示未指定符号的通配符，但更加深入和复杂。 变量 x 成为约束变量，比如 或 在任何这种命题中，是否使用 x 或其他什么字母在逻辑上不重要。但是，在复合命题的其他地方再次使用同一个字母可能导致冲突。就是说，自由变量变成了约束的，并在支持公式的格式化的进一步工作中在某种意义上退休了。.
新！!: Λ演算和自由变量和约束变量 · 查看更多 »
自然数
数学中，自然数指用于计数（如「桌子上有三个苹果」）和定序（如「国内第三大城市」）的数字。用于计数时称之为基数，用于定序时称之为序数。 自然数的定义不一，可以指正整数 (1, 2, 3, 4, \ldots)，亦可以指非负整数 (0, 1, 2, 3, 4, \ldots)。前者多在数论中使用，后者多在集合论和计算机科学中使用，也是 标准中所采用的定义。 数学家一般以\mathbb代表以自然数组成的集合。自然数集是一個可數的，無上界的無窮集合。.
集合
集合可以指：.
逻辑运算符
在形式逻辑中，逻辑运算符或逻辑联结词把语句连接成更复杂的复杂语句。例如，假设有两个逻辑命题，分别是“正在下雨”和“我在屋里”，我们可以将它们组成复杂命题“正在下雨，并且我在屋里”或“没有正在下雨”或“如果正在下雨，那么我在屋里”。一个将两个语句组成的新的语句或命题叫做复合语句或复合命题。.
递归
递归（Recursion），又译为--，在数学与计算机科学中，是指在函数的定义中使用函数自身的方法。递归一词还较常用于描述以自相似方法重复事物的过程。例如，当两面镜子相互之间近似平行时，镜中嵌套的图像是以无限递归的形式出现的。也可以理解为自我复制的过程。.
递归函数
在数理逻辑和计算机科学中，递归函数或μ-递归函数是一类从自然数到自然数的函数。直觉上递归函数是"可计算的"。事实上在可计算性理论中已经证明了它确实是图灵机的可计算函数。递归函数与原始递归函数相关，而且递归函数的归纳定义（见下）建立在原始递归函数之上。但不是所有递归函数都是原始递归函数——其中最著名的是阿克曼函数。 其他等价的函数类是λ-递归函数和马尔可夫算法可计算的函数。 所有递归函数的集合叫做R。.
Haskell
Haskell（）是一种标准化的，通用的纯函數程式語言，有非限定性语义和强静态类型。它的命名源自美国逻辑学家哈斯凱爾·加里，他在数理逻辑方面上的工作使得函数式编程语言有了广泛的基础。在Haskell中，“函数是第一類物件”。作为一门函數程式語言，主要控制结构是函数。Haskell语言是1990年在编程语言Miranda的基础上标准化的，并且以λ演算为基础发展而来。这也是为什么Haskell语言以希腊字母「λ」（Lambda）作为自己的标志。Haskell具有“证明即程序、命题为类型”的特征, with 2 sections by William Craig, see paragraph 9E。.
新！!: Λ演算和Haskell · 查看更多 »
LISP
LISP是具有悠久歷史的計算機編程語言家族，有獨特和完全括號的前綴符號表示法。起源於西元1958年，是現今第二悠久而仍廣泛使用的高階編程語言。只有FORTRAN編程語言比它更早一年。LISP編程語族已經演變出許多種方言。現代最著名的通用編程語種是Common Lisp和Scheme。 LISP最初創建時受到阿隆佐·邱奇的lambda演算的影響，用來作為計算機程序實用的數學表達。因為是早期的高階編程語言之一，它很快成為人工智能研究中最受歡迎的編程語言。在計算機科學領域，LISP開創了許多先驅概念，包括：.
ML语言
ML是一个通用的函數式編程语言，它是由爱丁堡大学的Robin Milner及他人在二十世纪七十年代晚期开发的。它的语法是从ISWIM得到的灵感。作为元语言的ML是为了帮助在LCF定理证明机中寻找证明策略而构想出来的。（之前的元语言是pplambda，它联合了一阶逻辑演算和有类型的多态的λ演算）。它使用了Hindley-Milner类型推论算法来推测大多数值的类型，而不需要四处使用注解。 ML一般被归为非纯函数式编程语言，因为它允许副作用和指令式编程。这一点和纯函数式编程语言——例如Haskell——很不一样。 ML特性包括：傳值呼叫（Call by value）的求值策略，一级函数，带有垃圾收集的自动内存管理，参数多态，静态数据类型，类型推论，代数数据类型，模式匹配和异常处理。 不像Haskell，ML使用及早求值，也就是说所有的子表达式总是被求值。导致的一个结果是你不能使用无穷表。然而，惰性求值产生的无穷表可以通过使用匿名函数来模拟。 今天在ML家族中有好几种语言：两种主要的方言是Standard ML和Caml，其他的包括F#－针对Microsoft.NET平台的开放研究项目。ML中的思想影响了众多的语言，例如Haskell，Cyclone和Nemerle。 ML的实力大多被用于语言设计和操作（编译器、分析器、定理证明机），但是它作为通用语言也被用于生化，金融系统，和宗谱数据库，一个P2P的客户／服务器程序等等。.
SKI组合子演算
SKI组合子演算是一个计算系统，它是对无类型版本的Lambda演算的简约。这个系统声称在Lambda演算中所有运算都可以用三个组合子S、K和I来表达。 在这个系统中的所有函数可以只使用S、K、I的字母表和圆括号（分组符号）来表达。通常假定组合子是左结合的，从而在不影响执行次序的情况下精简表达式中的圆括号。.
新！!: Λ演算和SKI组合子演算 · 查看更多 »
柯里化
在计算机科学中，柯里化（Currying），又译为卡瑞化或加里化，是把接受多个参数的函数变换成接受一个单一参数（最初函数的第一个参数）的函数，并且返回接受余下的参数而且返回结果的新函数的技术。这个技术由克里斯托弗·斯特雷奇以逻辑学家哈斯凱爾·加里命名的，尽管它是Moses Schönfinkel和戈特洛布·弗雷格发明的。 在直觉上，柯里化声称「如果你固定某些参数，你将得到接受余下参数的一个函数」。所以对于有两个变量的函数y^x，如果固定了y.
歸約
在可計算性理論與計算複雜性理論中，所謂的歸約是將某個轉換為另一個問題的過程。可用歸約法定義某些問題的複雜度類（因轉換過程而異）。 以直覺觀之，如果存在能有效解決問題B的算法，也可以作為解決問題A的子程序，則將問題A稱為「可歸約」到問題B，因此求解A並不會比求解B更困難。 一般寫作A ≤m B，通常也在≤符號下標使用的歸約類型（m：映射縮小，p：多項式縮減）。 將一組問題歸約到特定類型所產生的數學結構，通常形成预序关系，其等價類可用於定義求解難度和複雜度。.
決定性問題
在可計算性理論與計算複雜性理論中，所謂的決定性問題（Decision problem）是一個在某些形式系統回答是或否的問題。例如：「給兩個數字x與y，x是否可以整除y？」便是決定性問題，此問題可回答是或否，且依據其x與y的值。 決定性問題與功能性問題（Function problem，或複雜型問題）密切相關，功能性問題的答案內容，較簡單的是與非複雜許多。範例問題：「給予一個正整數x，則哪些數可整除x？」 另一個與上述兩類問題相關的是最佳化問題（Optimization problem），此問題關心的是尋找特定問題的最佳答案。 解決決定性問題的方法稱為決策程式或演算法。一個針對決定性問題的演算法將說明給予參數x和y的情況下如何決定x是否整除y。若是某些決定性問題可以被一些演算法所解決，則稱此問題可決定。 計算複雜度的領域中，分類可決定問題的依據在於此問題有多難被解決。在此標準下，所謂的難是以解決某問題最有效率的演算法所花費的計算資源為依據。在遞迴理論中，非決定性問題由圖靈度決定，指的是一種在任何解答中隱含的不可計算性量詞。 計算性理論的研究集中在決定性問題上。在與功能性問題的等值問題中，並沒有失去其普遍性。.
有类型λ演算
有类型 lambda 演算是使用 lambda 符号（\lambda）指示匿名函数抽象的一种有类型的形式化。有类型 lambda 演算是基础编程语言并且是有类型的函数式编程语言如 ML 和 Haskell 和更间接的指令式编程语言的基础。它们通过 Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型 lambda 演算是笛卡尔闭范畴（CCC）的语言。 传统上，有类型 lambda 演算被看作无类型lambda演算的精细化。更现代的观点把有类型 lambda 演算看做更基础的理论，而把无类型 lambda 演算看作它的只有一个类型的特殊情况。.
新！!: Λ演算和有类型λ演算 · 查看更多 »
