目录
24 关系: 不动点组合子，希尔伯特演绎系统，一种新科学，代数逻辑，哈斯凯尔·柯里，B,C,K,W系统，简单类型λ演算，类型论，用於數學、科學和工程的希臘字母，表示式，高阶函数，计算模型 (数学)，计算机逻辑，邱奇－图灵论题，自由变量和约束变量，逻辑，Λ演算，S (消歧义)，SKI组合子演算，抽象代数逻辑，柯里-霍华德同构，演绎定理，惰性求值，数理逻辑。
不动点组合子
不动点组合子（Fixed-point combinator，或不动点算子）是计算其他函数的一个不动点的高阶函数。 函数 f 的不动點是將函數應用在輸入值 x 時，會傳回與輸出值相同的值，使得 f(x).
查看 组合子逻辑和不动点组合子
希尔伯特演绎系统
在逻辑特别是数理逻辑中，希尔伯特风格演绎系统是归功于弗雷格和希尔伯特的一类形式演绎系统。这种演绎系统最经常为一阶逻辑而研究，但对其他逻辑也是有价值的。 所有演绎系统都在逻辑公理和推理规则之间作出取舍平衡。希尔伯特风格的演绎系统可以刻画为选择了大量的逻辑公理模式和少量的推理规则。最常研究的希尔伯特风格演绎系统只有一个推理规则即肯定前件和几个无限公理模式。 自然演绎系统做了相反的取舍，包括了很多演绎规则但有非常少甚至没有公理模式。.
一种新科学
《一种新科学》由斯蒂芬·沃尔夫勒姆所著，出版于2002年。它包括关于计算系统的实证和系统研究，如元胞自动机。斯蒂芬·沃尔夫勒姆把这些系统称为简单的程序，并且认为适用于简单程序研究的科学哲学和方法与其他科学领域相关。.
查看 组合子逻辑和一种新科学
代数逻辑
在數理邏輯中，代數邏輯使用抽象代數方法形式化邏輯。.
查看 组合子逻辑和代数逻辑
哈斯凯尔·柯里
哈斯凱爾·布魯克·加里（Haskell Brooks Curry ，），生于美國麻薩諸塞州米里鎮，數理邏輯學家，專長於组合子逻辑理論。尽管组合子逻辑的概念始于的一纸论文，其大部分发展工作是由柯里完成的。柯里也因为他的和柯里-霍华德同构而闻名。 三个程式語言Haskell、、Curry，以及柯里化的概念都是以他的名字來命名的。.
B,C,K,W系统
1930年哈斯凱爾·加里在他的博士论文《Grundlagen der kombinatorischen Logik》中提议了一个組合子邏輯系統。它带有基本组合子B、C、K和W（采用了现在的命名）。.
简单类型λ演算
单类型 lambda 演算(\lambda^\to)是连接词只有 \to (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、陪积或自然数(系统 T)甚至完全的递归(如PCF)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。.
类型论
在最广泛的层面上，类型论是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。在这种意义上，它与类型的形而上学概念有关。现代类型论在部分上是响应罗素悖论而发明的，并在伯特兰·罗素和阿弗烈·诺夫·怀海德的《数学原理》中起到重要作用。 在计算机科学分支中的编程语言理论中，类型论提供了设计分析和研究类型系统的形式基础。实际上，很多计算机科学家使用术语“类型论”来称呼对编程语言的类型语言的形式研究，尽管有些人把它限制于对更加抽象的形式化如有类型lambda演算的研究。.
查看 组合子逻辑和类型论
用於數學、科學和工程的希臘字母
希臘字母被用於數學、科學、工程和其他方面。在數學方面，希臘字母通常用於常數、特殊函數和特定的變數，而且通常大寫和小寫都有分別，而且互不相關。有一些希臘字母和拉丁字母一樣，而且不被使用：A, B, E, H, I, K, M, N, O, P, T, X, Y, Z。除此之外，由於小寫的ι（iota），ο（omicron）和υ（upsilon）跟拉丁字母i，o和u相似，所以很少被使用。有時，希臘字母的字體變種在數學數有特定的意思，例如φ（phi）和π（pi）。 在金融數學中，有些會用來表示投資風險的變數。 母語為英語的數學家在讀希臘字母時，他們不會用現在的或古時的發音，但用傳統的英語發音。例如θ，數學家會讀成/ˈθeɪtə/。（古時：，現在：）.
表示式
表示式亦称表達式、運算式或數學表達式，在數學領域中是一些符號依據上下文的規則，有限而定義良好的組合。數學符號可用於標定數字（常量）、變量、操作、函數、括號、標點符號和分組，幫助確定操作順序以及有其它考量的邏輯語法。.
查看 组合子逻辑和表示式
高阶函数
在数学和计算机科学中，高阶函数是至少满足下列一个条件的函数：.
查看 组合子逻辑和高阶函数
计算模型 (数学)
在可计算性理论和計算複雜性理論中，计算模型（model of computation）描述了如何根据一组输入值计算得出输出值，也包含了负责运算、存储和通讯等结构的具体组织方式。它可以用于测量一个算法在时间和/或空间上的复杂度。通过计算模型的抽象化总结，我们可以分析出算法的性能，而避免在具体程序层面，被不同的技术和实现方式造成的性能差异所误导。.
计算机逻辑
计算机逻辑描述应用于计算机科学和人工智能的逻辑。它包括：.
查看 组合子逻辑和计算机逻辑
邱奇－图灵论题
邱奇-图灵论题（Church–Turing thesis，又称邱奇-图灵猜想，邱奇论题，邱奇猜想，图灵论题）是一个关于可计算性理论的假设。该假设论述了关于函数特性的，可有效计算的函数值（用更现代的表述来说--在算法上可计算的)。简单来说，邱奇-图灵论题认为“任何在算法上可计算的问题同样可由图灵机计算”。 20世纪上半叶，对可计算性进行公式化表示的尝试有：.
自由变量和约束变量
在数学和其他涉及形式语言的学科中，包括数理逻辑和计算机科学，自由变量是在表达式中用于表示一个位置或一些位置的符号，某些明确的代换可以在其中发生，或某些运算（比如总和或量化）可以在其上发生。这个概念有关于占位符（它是以后会被所替换），或表示未指定符号的通配符，但更加深入和复杂。 变量 x 成为约束变量，比如 或 在任何这种命题中，是否使用 x 或其他什么字母在逻辑上不重要。但是，在复合命题的其他地方再次使用同一个字母可能导致冲突。就是说，自由变量变成了约束的，并在支持公式的格式化的进一步工作中在某种意义上退休了。.
逻辑
邏輯（λογική；Logik；logique；logic；意大利语、西班牙语、葡萄牙语: logica），又稱理則、論理、推理、推論，是对有效推論的哲學研究。邏輯被使用在大部份的智能活動中，但主要在哲學、心理、学习、推论统计学、脑科学、數學、語義學、 法律和電腦科學等領域內被視為一門學科。邏輯討論邏輯論證會呈現的一般形式，哪種形式是有效的，以及其中的謬論。 邏輯通常可分為三個部份：歸納推理、溯因推理和演繹推理。 在哲學裡，邏輯被應用在大多數的主要領域之中：形上學/宇宙論、本體論、知識論及倫理學。 在數學裡，邏輯是指形式逻辑和数理邏輯，形式逻辑是研究某個形式語言的有效推論。主要是演繹推理。 在辯證法中也會學習到邏輯。数理邏輯是研究抽象邏輯关系和数学基本的问题。 在心理、脑科学、語義學、 法律裡，是研究人类思想推理的处理。 在学习、推论统计学裡，是研究最大可能的结论。主要是歸納推理、溯因推理。 在電腦科學裡， 是研究各种方法的性质，可能性，和实现在机器上。主要是歸納推理、溯因推理，也有在歸納推理的研究。 从古文明开始（如古印度、中國和古希臘）都有對邏輯進行研究。在西方，亞里斯多德將邏輯建立成一門正式的學科，並在哲學中給予它一個基本的位置。.
查看 组合子逻辑和逻辑
Λ演算
λ演算（英語：lambda calculus，λ-calculus）是一套從數學邏輯中發展，以變數綁定和替換的規則，來研究函式如何抽象化定義、函式如何被應用以及遞迴的形式系統。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。Lambda演算作為一種廣泛用途的計算模型，可以清晰地定義什麼是一個可計算函式，而任何可計算函式都能以這種形式表達和求值，它能模擬單一磁帶图灵机的計算過程；儘管如此，Lambda演算強調的是變換規則的運用，而非實現它們的具體機器。 Lambda演算可比擬是最根本的編程語言，它包括了一條變換規則（變數替換）和一條將函式抽象化定義的方式。因此普遍公認是一種更接近軟體而非硬體的方式。對函數式編程語言造成很大影響，比如Lisp、ML语言和Haskell语言。在1936年邱奇利用λ演算給出了對於判定性問題（Entscheidungsproblem）的否定：關於兩個lambda運算式是否等價的命題，無法由一個「通用的演算法」判斷，這是不可判定效能夠證明的頭一個問題，甚至還在停机问题之先。 Lambda演算包括了建構lambda項，和對lambda項執行歸約的操作。在最簡單的lambda演算中，只使用以下的規則來建構lambda項： 產生了諸如：(λx.λy.(λz.(λx.zx)(λy.zy))(x y)的表達式。如果表達式是明確而沒有歧義的，則括號可以省略。對於某些應用，其中可能包括了邏輯和數學的常量以及相關操作。 本文讨论的是邱奇的“无类型lambda演算”，此后，已经研究出来了一些有类型lambda演算。.
查看 组合子逻辑和Λ演算
S (消歧义)
S是英语字母表的第19个字母。 S 可以指代：.
SKI组合子演算
SKI组合子演算是一个计算系统，它是对无类型版本的Lambda演算的简约。这个系统声称在Lambda演算中所有运算都可以用三个组合子S、K和I来表达。 在这个系统中的所有函数可以只使用S、K、I的字母表和圆括号（分组符号）来表达。通常假定组合子是左结合的，从而在不影响执行次序的情况下精简表达式中的圆括号。.
抽象代数逻辑
抽象代数逻辑(AAL)是研究代数类关联于逻辑系统的方式和这些代数类如何与逻辑系统交互的数理逻辑领域。.
查看 组合子逻辑和抽象代数逻辑
柯里-霍华德同构
柯里-霍華德对应是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算（computational calculus）之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·加里和逻辑学家William Alvin Howard独立发现的。.
演绎定理
在数理逻辑中，演绎定理声称如果公式 F 演绎自 E，则蕴涵 E → F 是可证明的(就是或它可以自空集推导出来)。用符号表示，如果 E \vdash F ，则 \vdash E \rightarrow F 。 演绎定理可以推广到假定公式的可数序列，使得从 E_1, E_2,...
查看 组合子逻辑和演绎定理
惰性求值
在程式語言理論中，惰性求值（Lazy Evaluation），又譯為惰性计算、懒惰求值，也稱為傳需求調用（call-by-need），是一个计算机编程中的一个概念，它的目的是要最小化计算机要做的工作。它有两个相关而又有区别的含意，可以表示为“延迟求值”和“最小化求值”，本条目专注前者，后者请参见最小化计算条目。除可以得到性能的提升外，惰性计算的最重要的好处是它可以构造一个无限的数据类型。 惰性求值的相反是及早求值，这是一个大多数编程语言所拥有的普通计算方式。.
查看 组合子逻辑和惰性求值
数理逻辑
数理逻辑是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。 数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑（相对于哲学逻辑），又称元数学，后者的使用现已局限于证明论的某些方面。.
查看 组合子逻辑和数理逻辑
亦称为 组合子。