我们正在努力恢复Google Play商店上的Unionpedia应用程序
传出传入
🌟我们简化了设计以优化导航!
Instagram Facebook X LinkedIn

Λ演算

指数 Λ演算

λ演算(英語: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演算。.

目录

  1. 16 关系: 基本的電腦科學主題列表可计算函数不动点组合子不可判定问题列表函数空间系统F组合子逻辑Erlang高阶函数计算模型 (数学)邱奇数F♯SKI组合子演算柯里化斯蒂芬·科尔·克莱尼普林斯顿大学人物列表

基本的電腦科學主題列表

電腦科學是資訊及理論基礎的研究以及電子計算機領域中的執行及應用,電腦科學中一個有名的主題分類系統是,它是由美國電腦協會所設計的,再電腦科學中一個基本的主題列表包括:.

查看 Λ演算和基本的電腦科學主題列表

可计算函数

在可计算性理论中,可计算函数(computable function)或图灵可计算函数是研究的基本对象。它们使我们直觉上的算法概念更加精确。使用可计算函数来讨论可计算性而不提及任何具体的计算模型,如图灵机或寄存器机。但是它们的定义必须提及某种特殊的计算模型。 在可计算函数的精确定义之前,数学家经常使用非正式术语可有效计算的。这个术语因此可以被认同为可计算函数。尽管这些函数被叫做有效的,它们可能极其困难。可行可计算性和计算复杂性研究可有效计算的函数。 依据邱奇-图灵论题,可计算函数精确的是使用给出无限数量的时间和存储空间的机器计算设备来计算的函数。等价的说,这个论题声称有算法的任何函数都是可计算的。 可以使用Blum公理来在可计算函数的集合上定义抽象计算复杂性理论。在计算复杂性理论中,确定一个可计算函数的复杂性的问题叫做功能性问题。.

查看 Λ演算和可计算函数

不动点组合子

不动点组合子(Fixed-point combinator,或不动点算子)是计算其他函数的一个不动点的高阶函数。 函数 f 的不动點是將函數應用在輸入值 x 時,會傳回與輸出值相同的值,使得 f(x).

查看 Λ演算和不动点组合子

不可判定问题列表

這是一個不可判定问题列表。.

查看 Λ演算和不可判定问题列表

函数空间

在数学中,函数空间是从集合X到集合Y的给定种类的函数的集合。它叫做空间是因为在很多应用中,它是拓扑空间或向量空间或这二者。.

查看 Λ演算和函数空间

系统F

系统F,也叫做多态lambda演算或二阶lambda演算,是有类型lambda演算。它由逻辑学家Jean-Yves Girard和计算机科学家John C. Reynolds独立发现的。系统F形式化了编程语言中的参数多态的概念。 正如同lambda演算有取值于(rang over)函数的变量,和来自它们的粘合子(binder);二阶lambda演算取值自类型,和来自它们的粘合子。 作为一个例子,恒等函数有形如A→ A的任何类型的事实可以在系统F中被形式化为判断 这里的α是类型变量。 在Curry-Howard同构下,系统F对应于二阶逻辑。 系统F,和甚至更加有表达力的lambda演算一起,可被看作Lambda立方体的一部分。.

查看 Λ演算和系统F

组合子逻辑

组合子逻辑是Moses Schönfinkel和哈斯凱爾·加里介入的一种符号系统,用来消除数理逻辑中对变量的需要。它最近在计算机科学中被用做计算的理论模型和设计函数式编程语言的基础。它所基于的组合子是只使用函数应用或早先定义的组合子来定义从它们的参数得出的结果的高阶函数。.

查看 Λ演算和组合子逻辑

Erlang

Erlang()是一種通用的----,它由喬·阿姆斯特朗(Joe Armstrong)在瑞典電信設備製造商愛立信所轄的電腦科學研究室開發,目的是創造一種可以應付大規模開發活動的--和執行環境。Erlang於1987年釋出正式版本,最早是愛立信擁有的私有軟體,經過十年的發展,於1998年發表開放源碼版本。 Erlang是運作於虛擬機的--,但是現在也包含有烏普薩拉大學高性能Erlang計劃(HiPE)開發的原生程式碼編譯器,自R11B-4版本開始,Erlang也支持--。在編程範型上,Erlang屬於多重典範程式語言,涵蓋函數式、--及--。循序執行的Erlang是一个及早求值, 單次賦值和--的函數式程式語言。.

查看 Λ演算和Erlang

高阶函数

在数学和计算机科学中,高阶函数是至少满足下列一个条件的函数:.

查看 Λ演算和高阶函数

计算模型 (数学)

在可计算性理论和計算複雜性理論中,计算模型(model of computation)描述了如何根据一组输入值计算得出输出值,也包含了负责运算、存储和通讯等结构的具体组织方式。它可以用于测量一个算法在时间和/或空间上的复杂度。通过计算模型的抽象化总结,我们可以分析出算法的性能,而避免在具体程序层面,被不同的技术和实现方式造成的性能差异所误导。.

查看 Λ演算和计算模型 (数学)

邱奇数

邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式,最常见的形式是邱奇数,它是使用lambda符号的自然数的表示法。这种方法得名于阿隆佐·邱奇,他首先以这种方法把数据编码到lambda演算中。 在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和tagged unions)都被映射到使用 邱奇编码的高阶函数;根据邱奇-图灵论题我们知道任何可计算的运算符(和它的运算数)都可以用邱奇编码表示。 很多学数学的学生熟悉可计算函数集合的哥德尔编号;邱奇编码是定义在lambda抽象而不是自然数上的等价运算。.

查看 Λ演算和邱奇数

F♯

F#是由微软发展的为.NET语言提供运行环境的程序设计语言,是函數程式語言(FP,Functional Programming),函數程式語言最重要的基礎是Lambda Calculus。它是基于OCaml的,而OCaml是基于ML函数程式语言。有時F#和OCaml的程式是可以交互編譯的。 F#已經接近成熟,支援高阶函数、柯里化、惰性求值、Continuations、模式匹配、闭包、列表处理和元编程。这是一个用于显.NET在不同编程语言间互通的程序设计,可以被.NET中的任意其它代碼編譯和調用。 2002年微软開始由Don Syme帶領研發F#,從C#,LINQ和Haskell中獲取了經驗,2005年推出第一個版本,2007年7月31日释出1.9.2.9版。2007年底,微軟宣布F#進入產品化的階段。 F#已被集成在Visual Studio 2010中,版本是2.0,含有对.Net Framework的完全支持。 F#现在在Visual Studio 2015中,版本是4.0。 F#现在在Visual Studio 2017中,版本是4.1。.

查看 Λ演算和F♯

SKI组合子演算

SKI组合子演算是一个计算系统,它是对无类型版本的Lambda演算的简约。这个系统声称在Lambda演算中所有运算都可以用三个组合子S、K和I来表达。 在这个系统中的所有函数可以只使用S、K、I的字母表和圆括号(分组符号)来表达。通常假定组合子是左结合的,从而在不影响执行次序的情况下精简表达式中的圆括号。.

查看 Λ演算和SKI组合子演算

柯里化

在计算机科学中,柯里化(Currying),又译为卡瑞化或加里化,是把接受多个参数的函数变换成接受一个单一参数(最初函数的第一个参数)的函数,并且返回接受余下的参数而且返回结果的新函数的技术。这个技术由克里斯托弗·斯特雷奇以逻辑学家哈斯凱爾·加里命名的,尽管它是Moses Schönfinkel和戈特洛布·弗雷格发明的。 在直觉上,柯里化声称「如果你固定某些参数,你将得到接受余下参数的一个函数」。所以对于有两个变量的函数y^x,如果固定了y.

查看 Λ演算和柯里化

斯蒂芬·科尔·克莱尼

斯蒂芬·科尔·克莱尼(Stephen Cole Kleene,)美國數學家、逻辑學家,主要从事對可計算函數的研究,而他的遞歸理論研究有助於奠定理論電腦科學的基礎。他為數學直覺主義的基礎做出了重要貢獻,克莱尼層次結構、克莱尼代数、克莱尼星号(克莱尼閉包)、克莱尼遞歸定理和克莱尼不動點定理數學概念以他的名字命名。他也是正規表示法的發明者。.

查看 Λ演算和斯蒂芬·科尔·克莱尼

普林斯顿大学人物列表

这些是著名的普林斯顿大学人物。名单按照职业分类,各个分类里按照英文姓氏排列。.

查看 Λ演算和普林斯顿大学人物列表

亦称为 Lambda演算,Λ转换演算。