简单类型λ演算

易经学习

天地变化的道理

分类目录

使用率很高网站

文章列表

生活要常常分享

维基百科

您身边百科全书

简单类型λ演算

点击查看词条快照

简单类型 lambda 演算(formula_1)是连接词只有 formula_2 (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、陪积或自然数(系统 T)甚至完全的递归(如PCF)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。类型. 简单类型 lambda 演算的类型构造自基本类型(或类型变量) formula_3，给定类型 formula_4 我们能构造 formula_5。邱奇只使用了两个基本类型，formula_6 是命题的类型，formula_7 是个体的类型。这种演算经常只有一个基本类型，通常考虑为 formula_6。 formula_2 是右结合的: 我们读 formula_10 为 formula_11。对每个类型 formula_12 我们指派一个数字 formula_13，它是 formula_12 的阶。对于基本类型，我们设置 formula_15，而对于函数类型我们递归的定义 formula_16。项. 要定义有给定类型的 lambda 项的集合，我们介入定类型上下文 formula_17，它们是形如 formula_18 的类型假定的序列，这里的 formula_19 是变量。我们介入判断 formula_20，它意味着 formula_21 在上下文 formula_22 中是类型 formula_12 的项，它们由下列定类型规则给出: 换句话说，闭合项的例子有: 它们是组合子逻辑的基本组合子的有类型 lambda 演算的表示。简单类型 lambda 演算通过 Curry-Howard同构密切相关于只有蕴涵(formula_2)作为连接词的直觉逻辑(极小逻辑): 闭合项所居留的类型正好是极小逻辑的重言式。相同类型的项通过 formula_41-等价来识别，它是通过方程 formula_42 生成的，这里的 formula_43 代表 formula_21 带有 formula_19 的所有自由出现都被替代为 formula_46，而 formula_47，如果 formula_19 在 formula_21 中不自由出现。简单类型 lambda 演算(带有 formula_41-等价)是笛卡儿闭范畴(CCC)的内部语言。这是 Lambek 首先观察到的。

台湾道

柠檬茶

弗拉基米尔·雅罗斯拉维奇

弗拉基米尔·雅罗斯拉维奇 (普隆斯克)

失智症

玄坛

巴伐利亚王位继承顺序

罗比·福勒

台中市私立慈明高级中学

围头话

韩浩 (东汉)

霍尔-赖伐尔协定