比浏览器更快的访问！
34 关系: 域理论，可计算性理论，参数，外延性，奎因，子集，不动点组合子，一阶逻辑，哥廷根大学，哈斯凱爾·加里，函數程式語言，关系语义，图灵机，B,C,K,W系统，Beta范式，结合律，直觉主义逻辑，Dana Scott，高阶函数，變數，计算，证明论，阿隆佐·邱奇，邱奇-图灵论题，自由变量和约束变量，递归，Haskell Curry，Λ演算，SASL，SKI组合子演算，柯里-霍华德同构，演绎定理，惰性求值，数理逻辑。
域理论
域理论是研究通常叫做域(domain)的特定种类偏序集合的数学分支。因此域理论可以被看作是序理论的分支。这个领域主要应用于计算机科学中，特别是针对函数式编程语言，用它来指定指称语义。域理论以非常一般化的方式形式化了逼近和收敛的直觉概念，并与拓扑学有密切联系。在计算机科学中指称语义的一个可作为替代的方式是度量空间。.
可计算性理论
在计算机科学中，可计算性理论（Computability theory）作为计算理论的一个分支，研究在不同的计算模型下哪些算法问题能够被解决。相对应的，计算理论的另一块主要内容，计算复杂性理论考虑一个问题怎样才能被有效的解决。.
新！!: 组合子逻辑和可计算性理论 · 查看更多 »
参数
在数学和统计学裡，参数（parameter）是使用通用变量来建立函数和变量之间关系（当这种关系很难用方程来阐述时）的一个数量。在不同的语境里这一术语可能有特殊用途。.
外延性
在数学中，外延性通常指称某种形式的。可追溯到莱布尼兹的原理，两个数学对象是相等的，如果没有区分它们的检验。例如，给出两个数学函数 f 和 g，我们可以说它们是相等的，如果 对于在公共函数域 X 内的所有 x。这种外延相等是平常的定义，如果函数范围 Y 对于两个也是公共的。在另一方面，如果我们在类型论的意义上通过附着到它们上的数据来区分函数，这样我们可以选择一个更大的集合比如 Z 作为它们之一的范围，则这种相等不同于“外延”意义的相等。这种意义下外延性可能会失败。另一种意义的相等考虑“函数被计算的过程”，如果这么考虑，通常会同外延性相抵触。 在公理化集合论中，外延性被表达为外延公理，它声称两个集合是相等的，当且仅当它们包含相同的元素。在 lambda 演算中，外延性被表达为 eta-变换规则，它允许在指示相同函数的任何两个表达式之间的转换。.
奎因
奎因、奎恩、昆恩、蒯因（Kween、Queen、Quin、Quine、Quinn）可以指：.
子集
子集，為某個集合中一部分的集合，故亦稱部分集合。 若A和B为集合，且A的所有元素都是B的元素，则有：.
不动点组合子
不动点组合子（Fixed-point combinator，或不动点算子）是计算其他函数的一个不动点的高阶函数。 函数 f 的不动點是將函數應用在輸入值 x 時，會傳回與輸出值相同的值，使得 f(x).
新！!: 组合子逻辑和不动点组合子 · 查看更多 »
一阶逻辑
一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统。 過去一百多年，一階邏輯出現過許多種名稱，包括：一阶斷言演算、低階斷言演算、量化理論或斷言逻辑（一個較不精確的用詞）。一階邏輯和命題邏輯的不同之處在於，一階邏輯有使用量化變數。一個一階邏輯，若具有由一系列量化變數、一個以上有意義的斷言字母及包含了有意義的斷言字母的純公理所組成的特定論域，即是一個一階理論。 一階邏輯和其他高階邏輯不同之處在於，高階邏輯的斷言可以有斷言或函數當做引數，且允許斷言量詞或函數量詞的（同時或不同時）存在。在一階邏輯中，斷言通常和集合相關連。在有意義的高階邏輯中，斷言則會被解釋為集合的集合。 存在許多對一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）的演繹系統。雖然一階邏輯的邏輯歸結只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯定理，如勒文海姆–斯科倫定理及緊緻性定理。 一階邏輯是數學基礎中很重要的一部份，因為它是公理系統的標準形式邏輯。許多常見的公理系統，如一階皮亞諾公理和包含策梅洛-弗蘭克爾集合論的公理化集合論等，都可以形式化成一階理論。然而，一階定理並沒有能力去完整描述及範疇性地建構如自然數或實數之類無限的概念。這些結構的公理系統可以由如二階邏輯之類更強的邏輯來取得。.
新！!: 组合子逻辑和一阶逻辑 · 查看更多 »
哥廷根大学
哥廷根的格奥尔格·奥古斯特大学（Georg-August-Universität Göttingen），简称哥廷根大学，位于德国西北部下萨克森州南端的大学城哥廷根市，因德国汉诺威公爵兼英国国王格奥尔格二世创建而得名。始建于1734年，于1737年向公众开放。同德国的海德堡大学、佛莱堡大学、圖宾根大学相似，哥廷根大学属于传统的大学城，是“没有校门和围墙的大学”。 哥廷根拥有十分辉煌的历史，名人辈出，蜚声世界。2007年10月至2012年5月期间为德国第二轮“精英大学”所评选的德国九所精英大学之一。.
新！!: 组合子逻辑和哥廷根大学 · 查看更多 »
哈斯凱爾·加里
#重定向 哈斯凯尔·柯里.
新！!: 组合子逻辑和哈斯凱爾·加里 · 查看更多 »
函數程式語言
函數式編程（functional programming）或称函数程序设计，又稱泛函編程，是一種編程典範，它將電腦運算視為數學上的函數計算，並且避免使用程序状态以及易变物件。函數程式語言最重要的基礎是λ演算（lambda calculus）。而且λ演算的函數可以接受函數當作輸入（引數）和輸出（傳出值）。 比起指令式編程，函數式編程更加強調程序执行的结果而非执行的过程，倡导利用若干简单的执行单元让计算结果不断渐进，逐层推导复杂的运算，而不是设计一个复杂的执行过程。.
新！!: 组合子逻辑和函數程式語言 · 查看更多 »
关系语义
Kripke 语义(也叫做关系语义或框架语义，并经常混淆于可能世界语义)是模态逻辑系统的形式语义，于 1950 年代晚期和 1960 年代早期由索尔·阿伦·克里普克建立。它后来为另一个非经典逻辑，最重要的直觉逻辑所接受。Kripke 语义的发现是非经典逻辑开发中重大突破，因为这种逻辑的模型论在 Kripke 之前实际上是不存在的。.
新！!: 组合子逻辑和关系语义 · 查看更多 »
图灵机
图灵机（），又称确定型图灵机，是英国数学家艾倫·图灵于1936年提出的一种抽象计算模型，其更抽象的意义为一种数学逻辑机，可以看作等价于任何有限逻辑数学过程的终极强大逻辑机器。.
B,C,K,W系统
1930年哈斯凱爾·加里在他的博士论文《Grundlagen der kombinatorischen Logik》中提议了一个組合子邏輯系統。它带有基本组合子B、C、K和W（采用了现在的命名）。.
新！!: 组合子逻辑和B,C,K,W系统 · 查看更多 »
Beta范式
在 lambda 演算中，一个项是beta 范式（规范型），如果没有“beta 归约”是可能的。一个项是 beta-eta 范式，如果既没有 beta 归约又没有“eta 归约”是可能的。一个项是头部范式，如果没有“在头部位置的 beta-可规约式”。.
新！!: 组合子逻辑和Beta范式 · 查看更多 »
结合律
在數學中，結合律(associative laws)是二元運算可以有的一個性質，意指在一個包含有二個以上的可結合運算子的表示式，只要運算元的位置沒有改變，其運算的順序就不會對運算出來的值有影響。亦即，重新排列表示式中的括號並不會改變其值。例如： 上式中的括號雖然重新排列了，但表示式的值依然不變。當這在任何實數的加法上都成立時，我們說「實數的加法是一個可結合的運算」。 結合律不應該和交換律相混淆。交換律會改變表示式中運算元的位置，而結合律則不會。例如： 是一個結合律的例子，因為其中的括號改變了（且因此運算子在運算中的順序也改變了），而運算元5、2、1則在原來的位置中。再來， 則不是一個結合律的例子，因為運算元2和5的位置互換了。 可結合的運算在數學中是很常見的，且事實上，大多數的代數結構確實會需要它們的二元運算是可結合的。不過，也有許多重要且有趣的運算是不可結合的；其中一個簡單的例子為向量積。.
直觉主义逻辑
觉主义逻辑或构造性逻辑是最初由阿蘭德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的证实性而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有存在性质，这使它还适合其他形式的数学构造主义。.
新！!: 组合子逻辑和直觉主义逻辑 · 查看更多 »
Dana Scott
#重定向 达纳·斯科特.
新！!: 组合子逻辑和Dana Scott · 查看更多 »
高阶函数
在数学和计算机科学中，高阶函数是至少满足下列一个条件的函数：.
新！!: 组合子逻辑和高阶函数 · 查看更多 »
變數
在初等數學裡，變數或變元、元是一個用來表示值的符號，該值可以是隨意的，也可能是未指定或未定的。在代數運算時，將變數當作明確的數值代入運算中，可以於單次運算時解出多個問題。一個典型的例子為一元二次公式，該公式可以解出每個一元二次方程的值，只需要將方程的系數代入公式中的變數即可。 變數這個概念在微積分中非常重要。一般，一個函數y.
计算
計算（Calculation）是一種將「單一或多個的輸入值」轉換為「單一或多個的結果」的一種思考過程。 計算的定義有許多種使用方式，有相當精確的定義，例如使用各種算法進行的「算术」，也有較為抽象的定義，例如在一場競爭中「策略的計算」或是「計算」兩人之間關係的成功機率。 將7乘以8（7x8）就是一種簡單的算術。 利用布莱克-斯科尔斯模型（Black-Scholes Model）來算出財務評估中的公平價格（fair price）就是一種複雜的算術。 從投票意向計算評估出的選舉結果（民意調查）也包含了某種算術，但是提供的結果是「各種可能性的範圍」而不是單一的正確答案。.
证明论
证明论是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。 证明论也可视为哲学逻辑的分支，其主要兴趣在于证明论语义学的思想，该思想依赖于结构证明论的技术型想法才可行。.
阿隆佐·邱奇
阿隆佐·邱奇（Alonzo Church，）是美国数学家，1936年发表可计算函数的第一份精确定义，对算法理论的系统发展做出巨大贡献。邱奇在普林斯顿大学受教并工作四十年，曾任数学与哲学教授。1967年迁往加利福尼亚大学洛杉矶分校。 解决算法问题包括构造一个能解决某一指定集及其他相关集的算法，如果该算法无法构建，则表明该问题是不可解的。证明此种问题不可解性的定理是算法理论中的一大突破，邱奇的算法即为该类算法的首例。邱奇证明了基本几何问题的算法不可解性。同时证明了一阶逻辑中真命题全集的解法问题是不可解的。.
新！!: 组合子逻辑和阿隆佐·邱奇 · 查看更多 »
邱奇-图灵论题
#重定向 邱奇－图灵论题.
新！!: 组合子逻辑和邱奇-图灵论题 · 查看更多 »
自由变量和约束变量
在数学和其他涉及形式语言的学科中，包括数理逻辑和计算机科学，自由变量是在表达式中用于表示一个位置或一些位置的符号，某些明确的代换可以在其中发生，或某些运算（比如总和或量化）可以在其上发生。这个概念有关于占位符（它是以后会被所替换），或表示未指定符号的通配符，但更加深入和复杂。 变量 x 成为约束变量，比如 或 在任何这种命题中，是否使用 x 或其他什么字母在逻辑上不重要。但是，在复合命题的其他地方再次使用同一个字母可能导致冲突。就是说，自由变量变成了约束的，并在支持公式的格式化的进一步工作中在某种意义上退休了。.
新！!: 组合子逻辑和自由变量和约束变量 · 查看更多 »
递归
递归（Recursion），又译为--，在数学与计算机科学中，是指在函数的定义中使用函数自身的方法。递归一词还较常用于描述以自相似方法重复事物的过程。例如，当两面镜子相互之间近似平行时，镜中嵌套的图像是以无限递归的形式出现的。也可以理解为自我复制的过程。.
Haskell Curry
#重定向 哈斯凯尔·柯里.
新！!: 组合子逻辑和Haskell Curry · 查看更多 »
Λ演算
λ演算（英語：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演算。.
SASL
#重定向 简单认证与安全层.
新！!: 组合子逻辑和SASL · 查看更多 »
SKI组合子演算
SKI组合子演算是一个计算系统，它是对无类型版本的Lambda演算的简约。这个系统声称在Lambda演算中所有运算都可以用三个组合子S、K和I来表达。 在这个系统中的所有函数可以只使用S、K、I的字母表和圆括号（分组符号）来表达。通常假定组合子是左结合的，从而在不影响执行次序的情况下精简表达式中的圆括号。.
新！!: 组合子逻辑和SKI组合子演算 · 查看更多 »
柯里-霍华德同构
柯里-霍華德对应是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算（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），是一个计算机编程中的一个概念，它的目的是要最小化计算机要做的工作。它有两个相关而又有区别的含意，可以表示为“延迟求值”和“最小化求值”，本条目专注前者，后者请参见最小化计算条目。除可以得到性能的提升外，惰性计算的最重要的好处是它可以构造一个无限的数据类型。 惰性求值的相反是及早求值，这是一个大多数编程语言所拥有的普通计算方式。.
新！!: 组合子逻辑和惰性求值 · 查看更多 »
数理逻辑
数理逻辑是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。 数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑（相对于哲学逻辑），又称元数学，后者的使用现已局限于证明论的某些方面。.
新！!: 组合子逻辑和数理逻辑 · 查看更多 »
