`
lobin
  • 浏览: 436739 次
  • 性别: Icon_minigender_1
  • 来自: 上海
社区版块
存档分类
最新评论
阅读更多
λ-calculus:α-conversion,β-reduction以及η-conversion

lambda abstraction:
(λx.t)
lambda abstraction是一个匿名函数定义:它有一个输入x,然后将输入x替换为t。它其实定义的是这样一个匿名函数:传入x,返回t。例如:λr.3.14 * r2为
f(r)= 3.14 * r2的lambda abstraction。

lambda abstraction的函数定义为仅仅"sets up"了一个函数,相当于定义了一个函数,但并不调用。

lambda abstraction同样抽象为:绑定变量x到t。


application:
(ts)
application表示将一个函数t应用于输入s,也就是说,它表示一个函数调用:t(s),t为调用的函数,s为输入。

lambda abstraction和application的本质区别为:
1、应用到函数上,前者为定义,后者为调用。
2、应用到变量上,前者为定义,后者为使用。

α-conversion:
λx.t


β-reduction:
((λV.E) E′)

下面例子就是一个((λV.E) E′)的形式定义: 表示将一个函数t应用于输入s, t就是这里的(λV.E),s就是这里的E′,也就是说,它表示一个函数调用:t(s),t为调用的函数(λV.E),s为输入E′。

在这里定义了一个匿名函数,对应形式中的(λV.E),形式中它接收V作为输入,替换为E。在例子中实际上定义了两个函数的重载:一个接收两个参数, 一个无参。

reduce的函数定义:
有两种形式, 第一种形式:
(reduce f coll)
第二种形式:
(reduce f val coll)

f should be a function of 2 arguments. If val is not supplied,
returns the result of applying f to the first 2 items in coll, then
applying f to that result and the 3rd item, etc. If coll contains no
items, f must accept no arguments as well, and reduce returns the
result of calling f with no arguments.  If coll has only 1 item, it
is returned and f is not called.  If val is supplied, returns the
result of applying f to val and the first item in coll, then
applying f to that result and the 2nd item, etc. If coll contains no
items, returns val and f is not called.

=> (reduce (fn
  #_=>           ([]
  #_=>            0)
  #_=>           ([va1 va2]
  #_=>            (+ va1 va2)))
  #_=>         [1 2 3 4 5])
15

可以拆解为:
=> (def fx (fn
  #_=>           ([]
  #_=>            0)
  #_=>           ([va1 va2]
  #_=>            (+ va1 va2))))
#'user/fx
=> (reduce fx [1 2 3 4 5])
15

=> (reduce fx [6])
6

=> (reduce fx [])
0


如果应用的函数定义为无参:
=> (def fx (fn
  #_=>          []
  #_=>          0))
#'user/fx

=> (reduce fx [1 2 3 4 5])

ArityException Wrong number of args (2) passed to: user/fx

=> (reduce fx [6])
6

=> (reduce fx [])
0

如果应用的函数定义为只接收一个参数:
=> (def fx (fn
  #_=>          [va]
  #_=>          va))
#'user/fx

=> (reduce fx [1 2 3 4 5])

ArityException Wrong number of args (2) passed to: user/fx

=> (reduce fx [6])
6

=> (reduce fx [])

ArityException Wrong number of args (0) passed to: user/fx

如果应用的函数定义为只接收两个参数:
=> (def fx (fn
  #_=>          [va1 va2]
  #_=>          (+ va1 va2)))
#'user/fx

=> (reduce fx [6])
6

=> (reduce fx [])

ArityException Wrong number of args (0) passed to: user/fx


如果应用的函数定义为只接收多于两个的参数:
=> (def fx (fn
  #_=>           [va1 va2 va3]
  #_=>           (+ va1 va2 va3)))
#'user/fx

=> (reduce fx [1 2 3 4 5])

ArityException Wrong number of args (2) passed to: user/fx

=> (reduce fx [6])
6

=> (reduce fx [])

ArityException Wrong number of args (0) passed to: user/fx


η-conversion:
λx.(f x)


只需要前两个:α-conversion及β-reduction就可以实现任何情况下的形式推演。

public Function<Input, Boolean> fx() {
    return Input -> (result(Input));
}
分享到:
评论

相关推荐

    pi-calculus

    这一时期,许多研究人员都在寻找一种能够像 λ 演算之于函数式编程那样为并发编程提供核心框架的形式化方法。其中,Milner 提出了通信顺序进程(CCS)[2],而 Tony Hoare 则提出了 CSP(Communicating Sequential ...

    A Tutorial Introduction to the Lambda.pdf

    Lambda演算(λ-calculus)是由美国逻辑学家阿隆佐·邱奇在20世纪30年代提出的一种形式系统,它最初被设计为研究有效可计算函数数学特性的工具。经过几十年的发展,λ-calculus不仅成为理论计算机科学的基础之一,...

    the pi-calculus: a theory of mobile processes (缺页部分)

    Pi演算的核心概念在于其对通信和进程移动的建模,这与传统的λ演算(用于描述计算过程)有所不同。在π演算中,计算过程被看作是可以动态交互和位置变迁的实体,这一特性使其成为研究移动计算和网络通信的理想工具。...

    惯有类型推导的幻灯片

    文档中提到的“Whatisλ-calculus?”表明,文档可能涉及到λ-演算的介绍和基础概念。 2. λ-演算中的三种基本术语是变量(variable)、函数(function)和函数应用(function application)。文档中描述的...

    lambda-calculus-js-old:Lambda 微积分的解析器和求解器

    lambda-calculus.js Lambda 微积分的解析器和求解器 下载 (右键单击链接,然后选择“另存为”) 用法 偏爱 将[removed] path/to/lambda-calculus.js [removed] 添加到&lt;head&gt;...&lt;/head&gt; 基本用法 var...

    lambda calculus

    Lambda学习,不错的资料参考 ...The λ-calculus was begun at Princeton, and the purpose of this report is to show how it has been recycled every decade after the 1930s in new and useful ways.

    Pi演算经典入门教程1

    - **λ-calculus的编码**:展示了如何将λ-calculus中的函数抽象和应用编码到Pi演算中。 - **组合代数**:探讨了如何用Pi演算来表示组合代数中的基本运算,这对于理解复杂的数据结构非常有用。 - **进程作为值的传输...

    An Introduction to the Lambda Calculus

    It is surprising that despite the simplicity of its syntax, the λ-calculus hosts a large body of notation, abbreviations, naming conventions, etc. Our aim, as far as the notation throughout this work...

    lambda-calculus-translation-grant:由GitHub Classroom创建的lambda-calculus-translation-grant

    在给定的资源"lambda-calculus-translation-grant"中,我们可以看到它与GitHub Classroom关联,可能是一个教学项目或挑战,旨在帮助学生理解和翻译Lambda演算的表达式到JavaScript。Racket是一种强大的编程语言,它...

    programming languages and lambda calculi

    #### Theλ-Calculus:λ演算 第二章转向λ演算的核心概念,它是整个文档的重点。λ演算是一种基于函数应用的计算模型,它可以用来表达任何形式的计算。作者首先介绍了λ演算中的函数定义,然后展示了其语法结构和...

    Practical.Foundations.for.Programming.Languages.2nd

    Chapter 21 The Untyped λ-Calculus Chapter 22 Dynamic Typing Chapter 23 Hybrid Typing Part X Subtyping Chapter 24 Structural Subtyping Chapter 25 Behavioral Typing Chapter Part XI Dynamic Dispatch ...

    lambda-calculus-translation-wickham-and-alex:GitHub Classroom创建的lambda-calculus-translation-wickham

    λC编译器 亚历克斯·麦克林(Alex MacLean),贝利·威克姆(Bailey Wickham) 安装 make 用法 ./transpiler c|python infile &gt;&gt; ./transpiler python examples/fact.lc

    Lambda-Calculus-and-The-Krivine-Abstract-Machine:第二年函数式编程模块的课程工作,其中我们负责在Haskell中实现Lambda-Calculus和Krivine抽象机

    Krivine抽象机(KAM)是一种基于λ演算的计算模型,由Jean-Louis Krivine提出,用于模拟λ表达式的求值过程。KAM使用堆栈来存储和操作λ表达式,它的主要操作有:应用、复制、跳跃和停止。在KAM中,函数应用是通过将...

    函数式程序设计入门

    在函数式程序设计中,λ演算(λ-Calculus)占据着核心地位。λ演算是一种形式系统,它使用抽象的函数应用来表示计算过程。它是函数式编程理论的基础,也为理解函数式编程语言提供了数学模型。λ演算包括了几种不同...

    C++实现的一个可以写递归lambda的Y函数

    最近学习C++11的variadic template argument,终于可以摆脱用...当然这仍然需要用普通的C++递归来实现,并不是λ-calculus那个高大上的Y Combinator。 #include #include #include #include using namespace s

    Lambda-Calculus-Interpreter:Lambda演算解释器,CS 4110研究的应用

    在`Lambda-Calculus-Interpreter-main`这个项目中,可能包含了实现上述功能的源代码文件、测试用例和相关的文档。通过阅读和理解这些文件,学生可以学习到如何将理论知识转化为实际代码,进一步加深对Lambda演算及其...

    java8stream源码-test:测试

    (λ-calculus - Alonzo Church 1936):创建函数的方法,数学逻辑中的形式系统,用于表达基于函数抽象的计算以及使用变量绑定和替换的应用。 编程语言中的新东西? 自 1958 年 Lisp 以来就有了 Lambda 句法 阴影 与...

    Sequent Calculus as a Compiler Intermediate Language - ICFP (2016)-计算机科学

    The λ-calculus is popular as an intermediate language for practical compilers. But in the world of logic it has a lesser-known twin, born at the same time, called the sequent calculus. Perhaps that ...

Global site tag (gtag.js) - Google Analytics