规范化性质
在数理逻辑和理论计算机科学中，一个重写系统有规范化性质，如果所有项都是强规范化的；就是说所有重写序列都最终终止于规范形式的项。 纯粹无类型 lambda 演算不是强规范化的。考虑项 \lambda x . x x x。它有如下重写规则: 对于任何项 t， : (\mathbf{\lambda} x . x x x) t \rightarrow t t t 但是考虑在应用 \lambda x . x x x 于自身时所发生的: 所以项 (…
标签：#Λ演算
共 17 篇文章
邱奇数
邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式，最常见的形式即邱奇数，它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇，他首先以这种方法把数据编码到lambda演算中。 透過邱奇編碼，在其他符号系统中通常被认定为基本的项（比如整数、布尔值、有序对、列表和tagged unions）都會被映射到高阶函数。在無型別lambda演算，函數是唯一的原始型別。 邱奇編碼本身並非用來實踐原始型別，而是透過它來展現我們不須額外原始…
Β范式
在λ演算中，若一个项不能β归约，则称为β范式（β规范型）；如果既不能β归约，又不能η归约，则称为β-η范式。如果不能在头部β归约，则称为头部范式。 β归约 在λ演算中，β可归约式(redex)是如下形式的项 : ((\mathbf{\lambda} x . A(x)) t) 这里的A(x)是（可能）涉及变量x的项。 “在头部位置的β归约”是把如下重写规则应用于一个β可归约式 : ((\mathbf{\lambda} x . A(x)) …
Λ演算
λ演算（英語：lambda calculus，λ-calculus）是一套從數學邏輯中發展出的形式系統，以變數綁定和替換的規則，來研究函式如何抽象化定義、函式如何被應用以及遞迴。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。lambda演算作為一種廣泛用途的計算模型，可以清晰地定義什麼是一個可計算函式，而任何可計算函式都能以這種形式表達和求值，它能模擬單一磁帶图灵机的計算過程；儘管如此，lambda演算強調的是變換規則的運用，而非實…
构造演算
构造演算(CoC)是高阶有类型 lambda 演算，这里的类型是一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数，同从整数到整数的函数一样。CoC 是强规范化的。 CoC 最初由 Thierry Coquand 开发。 CoC 是 Coq 定理证明器早期版本的基础；它后来的版本建造在归纳构造演算之上，这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中，归纳数据类型必须模拟为它们的多态解构函数。 构…
逻辑框架
在类型论中，LF 逻辑框架提供了定义(或表示)逻辑的一种方式。它基于了通过有依赖类型的lambda 演算方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 Per Martin-Löf 文章中的系统的风格来处理。 要描述一个逻辑框架，你必须提供如下: 1. 对要表示的那一类对象-逻辑的特征描述； 2. 适当的元-语言； 3. 对表示对象-逻辑的机制的特征描述。 总结为: :“框架 = 语言 + 表示”。 在 LF 逻辑框架的…
蒙塔古語法
蒙塔古文法（），又譯為蒙太古文法、蒙太格文法，由美國邏輯學家理查德·蒙塔古提出，用來研究自然語言語義學。他認為自然語言與形式語言在基本文法邏輯上是一致的，於1970年至1973年間提出一系列論文，形成蒙塔古文法，可用於自然語言處理。
柯里化
在计算机科学中，柯里化（），又译为卡瑞化或加里化，是把接受多个参数的函数变换成接受一个单一参数（最初函数的第一个参数）的函数，并且返回接受余下的参数而且返回结果的新函数的技术。这个技术由克里斯托弗·斯特雷奇以逻辑学家哈斯凱爾·加里命名的，尽管它是Moses Schönfinkel和戈特洛布·弗雷格发明的。 在直觉上，柯里化声称「如果你固定某些参数，你将得到接受余下参数的一个函数」。所以对于有两个变量的函数y^x，如果固定了y=2，则得到…
简单类型λ演算
简单类型 lambda 演算(\lambda^\to)是连接词只有 \to (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、陪积或自然数(系统 T)甚至完全的递归(如PCF)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在…
有类型λ演算
有类型lambda演算是使用lambda符号（\lambda）指示匿名函数抽象的一种有类型的形式化。有类型lambda演算是基础编程语言并且是有类型的函数式编程语言如ML和Haskell和更间接的指令式编程语言的基础。它们通过Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型lambda演算是笛卡尔闭范畴（CCC）的语言。 传统上，有类型lambda演算被看作无类型lambda演算的精细化。更现…
高阶函数
在数学和计算机科学中，高阶函数是至少满足下列一个条件的函数： 接受一个或多个函数作为输入 输出一个函数 在数学中它们也叫做算子（运算符）或泛函。微积分中的导数就是常见的例子，因为它映射一个函数到另一个函数。 在无类型lambda演算，所有函数都是高阶的；在有类型lambda演算中，高阶函数一般是那些函數型別包含多于一个箭头的函数。在函数式编程中，返回另一个函数的高阶函数被称为Curry化的函数。 一般性例子 在很多函数式编程语言中能找到…
不动点组合子
不动点组合子（，或不动点算子）是计算其他函数的一个不动点的高阶函数。 函数 f 的不动點是將函數應用在輸入值 x 時，會傳回與輸入值相同的值，使得 f(x) = x。例如，0 和 1 是函数 f(x) = x2 的不动点，因为 02 = 0 而 12 = 1。鉴于一阶函数（在简单值比如整数上的函数）的不动点是个一阶值，高阶函数 f 的不动点是另一个函数 g 使得 f(g) = g。那么，不动点算子 fix 的定義是 : x = f\ x…
系统F
系统F，也叫做多态lambda演算或二阶lambda演算，是有类型lambda演算。它由逻辑学家和计算机科学家独立发现的。系统F形式化了编程语言中的参数多态的概念。 正如同lambda演算有取值于（range over）函数的变量，和来自它们的粘合子（binder）；二阶lambda演算取值自类型，和来自它们的粘合子。 作为一个例子，恒等函数有形如A→ A的任何类型的事实可以在系统F中被形式化为判断 :\vdash \Lambda\al…
类型居留问题
在简单类型lambda演算中，类型居留（Type inhabitation）问题是如下问题：给定一个类型 \tau，是否存在一个 \lambda-项 M 使得对于某个类型环境 \Gamma 有 \Gamma \vdash M : \tau？在空的类型环境中，如果回答是肯定的，则 M 被称为 \tau 的居留元（inhabitant）。 因为在简单类型的 lambda 演算中类型对应于极小蕴涵逻辑(参见 Curry-Howard 同构)，…
匿名函数
匿名函数（）在计算机编程中是指一类无需定义标识符（函数名）的函数或子程序，普遍存在于多种编程语言中。 1958年LISP首先采用匿名函数，自此之后，越来越多编程语言陆续采用，主流的编程语言如PHP和C++也陸續采用。 用途 排序 尝试将类按名称排序： a = [10, '10', 10.0] a.sort(lambda x,y: cmp(x.class.name, y.class.name)) print a [10.0, 10, '1…
Λ演算骑士团
λ演算骑士团（）是一个由LISP专家和Scheme黑客组成的的半虚构组织。这个名字指代的是Λ演算，一个由阿隆佐·邱奇创造的数学形式体系。此体系与LISP紧密相关，而λ演算骑士团之名称引用自圣殿骑士团。 其实并没有组织叫λ演算骑士团；它主要只在黑客文化内作为内部笑话而存在。这个概念可能起源自MIT（麻省理工学院）。例如，在《计算机程序的构造和解释》的[http://www.swiss.ai.mit.edu/classes/6.001/ab…
Λ立方
在数理逻辑和类型论中，λ立方是探索Coquand的构造演算中细化轴的框架，以简单类型λ演算（在立方图中写作λ→）作为原点放在立方体的顶点，而构造演算（即高阶依赖类型化λ演算，在图中写作λPω）则是其空间对顶点。立方体的每个轴都表示一种新的抽象形式： 值依赖类型，或多态。系统F，即二阶λ演算（图中写作λ2）就是通过只加入此性质得到的。 类型依赖类型，或类型构造器。带类型构造器的简单类型λ演算（图中为\lambda\underline{\o…