fbpx
维基百科

简单类型λ演算

简单类型 lambda 演算()是连接词只有 (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。

简单类型也被用来称呼对简单类型 lambda 演算的扩展比如、陪积或自然数(系统 T)甚至完全的递归(如PCF)。相反的,介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。

类型

简单类型 lambda 演算的类型构造自基本类型(或类型变量)  ,给定类型   我们能构造  。邱奇只使用了两个基本类型,  是命题的类型,  是个体的类型。这种演算经常只有一个基本类型,通常考虑为  

  是右结合的: 我们读   。对每个类型   我们指派一个数字  ,它是   的阶。对于基本类型,我们设置  ,而对于函数类型我们递归的定义  

要定义有给定类型的 lambda 项的集合,我们介入定类型上下文  ,它们是形如   的类型假定的序列,这里的   是变量。我们介入判断  ,它意味着   在上下文   中是类型   的项,它们由下列定类型规则给出:

   
   

换句话说,

  1. 如果 x 有类型  ,我们知道 x 有类型  
  2. 如果在特定上下文中,可以推导出 x 有类型   ,且有某个不是 x 的 y,则上述上下文与 y 有类型   的事实一起,同样允许推导出 x 有类型  。即向上下文增加一个新值不改变现存的值(新值不同于旧值之一)。
  3. 如果在特定上下文中,已知 x 有类型  ,可以推导出 t 有类型  ,则在同一个上下文中,可以构造lambda 抽象  ,它有类型  
  4. 如果在特定上下文中,可以推导出 t 有类型   和 u 有类型  ,则在同一个上下文中,可以推导出表达式  有类型  。这捕获了函数应用的概念。

闭合项的例子有:

  •   (I)
  •   (K)
  •   (S)。

它们是组合子逻辑的基本组合子的有类型 lambda 演算的表示。

简单类型 lambda 演算通过 Curry-Howard同构密切相关于只有蕴涵( )作为连接词的直觉逻辑(极小逻辑): 闭合项所居留的类型正好是极小逻辑的重言式。

相同类型的项通过  -等价来识别,它是通过方程   生成的,这里的   代表   带有   的所有自由出现都被替代为  ,而  ,如果    中不自由出现。简单类型 lambda 演算(带有  -等价)是笛卡儿闭范畴(CCC)的内部语言。这是 Lambek 首先观察到的。

重要成果

  • Tait 在 1967 年证明了  -归约是强规范化的。作为必然推论  -等价是可判定性的。Statman 在 1977 年证明规范化问题不是基本递归的。纯语义规范化证明由 Berger 和 Schwichtenberg (Normalisation by evaluation) 在 1991 年给出。
  •  -等价的合一问题是不可判定的。Huet 在 1973 年证明 3 阶合一已经是不可判定的了,而 Goldfarb 在 1981 年进而证明了 2 阶合一是不可判定的。更高阶匹配(只有包含存在性变量一个项的合一)是否是可判定仍无定论。
  • 我们可以通过类型   的项(邱奇数)来编码自然数。Schwichtenberg 在 1976 年证明在   中扩展的多项式被准确的表示为在邱奇数上的函数;这些粗略的是在条件运算下闭合的多项式。
  •   的完整模型是通过解释基本类型为集合和解释函数类型为集合论的函数空间来给出。Friedman 在 1975 年证明这种解释是对  -等价是完备的,如果基本类型被解释为无限集合。Statman 在 1983 年证明  -等价是极大等价,它是典型歧义的,就是说,在类型替换下闭合(Statman's Typical Ambiguity Theorem)。它的必然推论是有限模型性质成立,就是说,有限集合就足够用来区别出不能通过  -等价识别的项。
  • Plotkin 在 1973 年介入逻辑关系来特征化可以用 lambda 项定义的模型的基础。在 1993 年 Jung 和 Tiuryn 证明了逻辑关系的一般形式(带有可变元数的 Kripke 逻辑关系)完全特征化了 lambda 定义能力。Plotkin 和 Statman 推测从有限模型生成给定元素是否是通过 lambda 项可定义的(Plotkin-Statman-conjecture)。这个推测被 Loader 在 1993 年证明为假。

引用

  • A. Church: A Formulation of the Simple Theory of Types, JSL 5, 1940
  • W.W.Tait: Intensional Interpretations of Functionals of Finite Type I, JSL 32(2), 1967
  • G.D. Plotkin: Lambda-definability and logical relations, Technical report, 1973
  • G.P. Huet: The Undecidability of Unification in Third Order Logic Information and Control 22(3): 257-267 (1973)
  • H. Friedman: Equality between functionals. LogicColl. 73, pages 22-37, LNM 453, 1975.
  • H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114.
  • R. Statman: The Typed lambda-Calculus Is not Elementary Recursive FOCS 1977: 90-94
  • W. D. Goldfarb: The undecidability of the 2nd order unification problem, TCS (1981), no. 13, 225- 230.
  • R. Statman.  -definable functionals and   conversion. Arch. Math. Logik, 23:21--26, 1983.
  • J. Lambek: Cartesian Closed Categories and Typed Lambda-calculi. Combinators and Functional Programming Languages 1985: 136-175
  • U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for Typed lambda-calculus LICS 1991: 203-211
  • Jung, A.,Tiuryn, J.:A New Characterization of Lambda Definability, TLCA 1993
  • R. Loader: , appeared in the Church Festschrift, 2001

参见

简单类型λ演算, 此條目已列出參考文獻, 但因為沒有文內引註而使來源仍然不明, 2015年12月16日, 请加上合适的文內引註来改善这篇条目, 简单类型, lambda, 演算, displaystyle, lambda, 是连接词只有, displaystyle, 函数类型, 的有类型, lambda, 演算, 这使它成为规范的, 在很多方面是最简单的有类型, lambda, 演算的例子, 简单类型也被用来称呼对简单类型, lambda, 演算的扩展比如积, 陪积或自然数, 系统, 甚至完全的递归, 如pcf, . 此條目已列出參考文獻 但因為沒有文內引註而使來源仍然不明 2015年12月16日 请加上合适的文內引註来改善这篇条目 简单类型 lambda 演算 l displaystyle lambda to 是连接词只有 displaystyle to 函数类型 的有类型 lambda 演算 这使它成为规范的 在很多方面是最简单的有类型 lambda 演算的例子 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积 陪积或自然数 系统 T 甚至完全的递归 如PCF 相反的 介入了多态类型 如系统F 或依赖类型 如逻辑框架 的系统不被当作是简单类型 简单类型 lambda 演算最初由阿隆佐 邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用 目录 1 类型 2 项 3 重要成果 4 引用 5 参见类型 编辑简单类型 lambda 演算的类型构造自基本类型 或类型变量 a b g displaystyle alpha beta gamma dots 给定类型 s t displaystyle sigma tau 我们能构造 s t displaystyle sigma to tau 邱奇只使用了两个基本类型 o displaystyle o 是命题的类型 i displaystyle iota 是个体的类型 这种演算经常只有一个基本类型 通常考虑为 o displaystyle o displaystyle to 是右结合的 我们读 s t r displaystyle sigma to tau to rho 为 s t r displaystyle sigma to tau to rho 对每个类型 s displaystyle sigma 我们指派一个数字 o s displaystyle o sigma 它是 s displaystyle sigma 的阶 对于基本类型 我们设置 o a 0 displaystyle o alpha 0 而对于函数类型我们递归的定义 o s t max o s 1 o t displaystyle o sigma to tau mbox max o sigma 1 o tau 项 编辑要定义有给定类型的 lambda 项的集合 我们介入定类型上下文 G D displaystyle Gamma Delta dots 它们是形如 x s displaystyle x sigma 的类型假定的序列 这里的 x displaystyle x 是变量 我们介入判断 G t s displaystyle Gamma vdash t sigma 它意味着 t displaystyle t 在上下文 G displaystyle Gamma 中是类型 s displaystyle sigma 的项 它们由下列定类型规则给出 x s x s displaystyle frac x sigma vdash x sigma G x s x y G y t x s displaystyle Gamma vdash x sigma quad x not y over Gamma y tau vdash x sigma G x s t t G l x s t s t displaystyle Gamma x sigma vdash t tau over Gamma vdash lambda x sigma t sigma to tau G t s t G u s G t u t displaystyle Gamma vdash t sigma to tau quad Gamma vdash u sigma over Gamma vdash t u tau 换句话说 如果 x 有类型 s displaystyle sigma 我们知道 x 有类型 s displaystyle sigma 如果在特定上下文中 可以推导出 x 有类型 s displaystyle sigma 且有某个不是 x 的 y 则上述上下文与 y 有类型 t displaystyle tau 的事实一起 同样允许推导出 x 有类型 s displaystyle sigma 即向上下文增加一个新值不改变现存的值 新值不同于旧值之一 如果在特定上下文中 已知 x 有类型 s displaystyle sigma 可以推导出 t 有类型 t displaystyle tau 则在同一个上下文中 可以构造lambda 抽象 l x s t displaystyle lambda x sigma t 它有类型 s t displaystyle sigma to tau 如果在特定上下文中 可以推导出 t 有类型 s t displaystyle sigma to tau 和 u 有类型 s displaystyle sigma 则在同一个上下文中 可以推导出表达式 t u displaystyle t u 有类型 t displaystyle tau 这捕获了函数应用的概念 闭合项的例子有 l x a x a a displaystyle lambda x alpha x alpha to alpha I l x a l y b x a b a displaystyle lambda x alpha lambda y beta x alpha to beta to alpha K l x a b g l y a b l z a x z y z a b g a b a g displaystyle lambda x alpha to beta to gamma lambda y alpha to beta lambda z alpha xz yz alpha to beta to gamma to alpha to beta to alpha to gamma S 它们是组合子逻辑的基本组合子的有类型 lambda 演算的表示 简单类型 lambda 演算通过 Curry Howard同构密切相关于只有蕴涵 displaystyle to 作为连接词的直觉逻辑 极小逻辑 闭合项所居留的类型正好是极小逻辑的重言式 相同类型的项通过 b h displaystyle beta eta 等价来识别 它是通过方程 l x s t u b t x u displaystyle lambda x sigma t u beta t x u 生成的 这里的 t x u displaystyle t x u 代表 t displaystyle t 带有 x displaystyle x 的所有自由出现都被替代为 u displaystyle u 而 l x s t x h t displaystyle lambda x sigma t x eta t 如果 x displaystyle x 在 t displaystyle t 中不自由出现 简单类型 lambda 演算 带有 b h displaystyle beta eta 等价 是笛卡儿闭范畴 CCC 的内部语言 这是 Lambek 首先观察到的 重要成果 编辑Tait 在 1967 年证明了 b displaystyle beta 归约是强规范化的 作为必然推论 b h displaystyle beta eta 等价是可判定性的 Statman 在 1977 年证明规范化问题不是基本递归的 纯语义规范化证明由 Berger 和 Schwichtenberg Normalisation by evaluation 在 1991 年给出 b h displaystyle beta eta 等价的合一问题是不可判定的 Huet 在 1973 年证明 3 阶合一已经是不可判定的了 而 Goldfarb 在 1981 年进而证明了 2 阶合一是不可判定的 更高阶匹配 只有包含存在性变量一个项的合一 是否是可判定仍无定论 我们可以通过类型 o o o o displaystyle o to o to o to o 的项 邱奇数 来编码自然数 Schwichtenberg 在 1976 年证明在 l displaystyle lambda to 中扩展的多项式被准确的表示为在邱奇数上的函数 这些粗略的是在条件运算下闭合的多项式 l displaystyle lambda to 的完整模型是通过解释基本类型为集合和解释函数类型为集合论的函数空间来给出 Friedman 在 1975 年证明这种解释是对 b h displaystyle beta eta 等价是完备的 如果基本类型被解释为无限集合 Statman 在 1983 年证明 b h displaystyle beta eta 等价是极大等价 它是典型歧义的 就是说 在类型替换下闭合 Statman s Typical Ambiguity Theorem 它的必然推论是有限模型性质成立 就是说 有限集合就足够用来区别出不能通过 b h displaystyle beta eta 等价识别的项 Plotkin 在 1973 年介入逻辑关系来特征化可以用 lambda 项定义的模型的基础 在 1993 年 Jung 和 Tiuryn 证明了逻辑关系的一般形式 带有可变元数的 Kripke 逻辑关系 完全特征化了 lambda 定义能力 Plotkin 和 Statman 推测从有限模型生成给定元素是否是通过 lambda 项可定义的 Plotkin Statman conjecture 这个推测被 Loader 在 1993 年证明为假 引用 编辑A Church A Formulation of the Simple Theory of Types JSL 5 1940 W W Tait Intensional Interpretations of Functionals of Finite Type I JSL 32 2 1967 G D Plotkin Lambda definability and logical relations Technical report 1973 G P Huet The Undecidability of Unification in Third Order Logic Information and Control 22 3 257 267 1973 H Friedman Equality between functionals LogicColl 73 pages 22 37 LNM 453 1975 H Schwichtenberg Functions definable in the simply typed lambda calculus Arch Math Logik 17 1976 113 114 R Statman The Typed lambda Calculus Is not Elementary Recursive FOCS 1977 90 94 W D Goldfarb The undecidability of the 2nd order unification problem TCS 1981 no 13 225 230 R Statman l displaystyle lambda definable functionals and b h displaystyle beta eta conversion Arch Math Logik 23 21 26 1983 J Lambek Cartesian Closed Categories and Typed Lambda calculi Combinators and Functional Programming Languages 1985 136 175 U Berger H Schwichtenberg An Inverse of the Evaluation Functional for Typed lambda calculus LICS 1991 203 211 Jung A Tiuryn J A New Characterization of Lambda Definability TLCA 1993 R Loader The Undecidability of l definability appeared in the Church Festschrift 2001参见 编辑构造演算 取自 https zh wikipedia org w index php title 简单类型l演算 amp oldid 72810162, 维基百科,wiki,书籍,书籍,图书馆,

文章

,阅读,下载,免费,免费下载,mp3,视频,mp4,3gp, jpg,jpeg,gif,png,图片,音乐,歌曲,电影,书籍,游戏,游戏。