两道λ演算作业

客官°小女子只卖身不卖艺 2022-08-05 19:58 137阅读 0赞

由于作业需要，开始学习λ演算，顺便开始写博客，也记录一下学习历程。

下面简单介绍λ演算的三个规则（红色部分非原创，参考自[wxb\_nudt][wxb_nudt]的博客《[Lambda演算学习笔记][Lambda]》）。

### λ-项是左结合的，λx.xx＝(λx.x)x ###

### α-变换 ###

α变换表达了λ演算中约束变量的名称是不重要的，例如λx.x和λy.y是相同的函数。因此，将某个函数中的所有约束变量全部换名是可以的。

首先是一个说明：如果M，N是λ-项，x在M中有自由出现，若以N置换M中所有x的自由出现（M中可能含有x的约束出现），我们得到另一个λ-项，记为M\[x/N\]。

α-变换规则如下：

*λx.M=λy.M\[x/y\]  如果y没有在M中自由出现，并且只要y替换M中的x，都不会被M中的一个λ绑定。*

例子：λx.( λx.x)x = λy(λx.x)y

α-变换主要用来表达函数中的变量换名规则，需要注意的是被换名的只能是M（函数体）中变量的自由出现。

### β-归约 ###

β-归约表达的是函数应用或者函数代入的概念。前面提到MN是合法的λ-项，那么MN的含义是将M应用到N，通俗的说是将N作为实参代替M中的约束变量，也就是形参。β-归约的规则如下：

*(λx.M)N-->M\[x/N\] 如果N中所有变量的自由出现都在M\[x/N\]中保持自由出现*

β-归约是λ演算中最重要的概念和规则，它是函数代入这个概念的形式化表示。

一些例子如下：

(lx.ly.y x)(lz.u)®ly.y(lz.u) (lx. x x)(lz.u)®(lz.u) (lz.u) (ly.y a)((lx. x)(lz.(lu.u) z))®(ly.y a)(lz.(lu.u) z) (ly.y a)((lx. x)(lz.(lu.u) z))→(ly.y a)((lx. x)(lz. z)) (ly.y a)((lx. x)(lz.(lu.u) z))→((lx. x)(lz.(lu.u) z)) a

### η-变换（η-conversion） ###

η-变换表达了“外延性”（extensionality）的概念，在这种上下文中，两个函数被认为是相等的“当且仅当”对于所有的参数，它们都给出同样的结果。我理解为，对于所有的实参，通过β-归约都能得到同样的λ-项，或者使用α-变换进行换名后得到同样的λ-项。

例如λx.fx与f相等，如果x没有在f中自由出现。

### 由β-归约，对所有的 y 有 (λ x . f x) y = f y，可得 λ x . f x = f，故η-变换成立。 ###

两道作业题目及解答如下(如有错误，欢迎指正)：

1.有函数：Y = λg. (λf.g(f f))(λf .g(ff))，试证 YF = F(YF)\[F是任意函数\].

证明：YF=λg.(λf.g(ff))(λf.g(ff))F

=(λf.F(ff))(λf.F(ff))        (1)α变换，\[g/F\]

=ww                             (2)令w=(λf.F(ff))

=(λf.F(ff))w

=F(ww)                        (3)β规约，将w代入f

=F(YF)                         由(2)知ww==YF

证毕。

2.  利用λ规约法则将(**λp.λq.λr.p**** q r)(****λp.λq.p**** q r****)**化到最简

解：(λp.λq.λr.p q r)(λp.λq.p q r)

=(λp.λq.λr.p qr)(λq.r q)             β规约，将r代入p

=(λp.λq.λr.p qr)r                       η变换

=(λp.λq.λw.p q w)r                   α变换，\[r/w\]

=λq.λw.r q w                             β规约，将r代入p

[wxb_nudt]: http://www.blogjava.net/wxb_nudt/
[Lambda]: http://www.blogjava.net/wxb_nudt/archive/2005/05/15/4311.aspx

发表评论取消回复

表情：

评论列表（有 0 条评论，137人围观）

还没有评论，来说两句吧...

相关阅读

相关两道“数学”题

[\[NOIP2001\]一元三次方程求解 (nowcoder.com)][NOIP2001_ _nowcoder.com] ![9f7427e767c445b8a8238f

谁践踏了优雅/ 2023年09月23日 22:51/ 0 赞/ 68 阅读

相关虚函数不能完全代替λ

[见上篇][Link 1] 上面,虽然一定程度上,可以继承. 但矛盾在于,`上篇`的这个`并坑`,`扩展性`不好. 因为,其`虚函数`无法使用.这只是个`结构`.

一时失言乱红尘/ 2023年01月16日 11:20/ 0 赞/ 119 阅读

相关函数式编程的λ演算

λ演算是数理逻辑中的一个形式系统，在函数抽象和应用的基础上，使用变量绑定和替换来表达计算。讨论λ演算离不开形式化的表达。在本文中，咱们尽可能集中在与编程相关的基本概念上，而不拘

不念不忘少年蓝@/ 2022年10月16日 06:11/ 0 赞/ 131 阅读

相关 lambda演算

> 由简入深，适时复习，温故知新。 — housir > > λ演算基于最简单的定义函数的思想： > 一为函数抽象λx.E，由λ说明的x在函数体E中出现均为形参变元。E是

旧城等待，/ 2022年08月09日 17:57/ 0 赞/ 195 阅读

相关两道λ演算作业

由于作业需要，开始学习λ演算，顺便开始写博客，也记录一下学习历程。下面简单介绍λ演算的三个规则（红色部分非原创，参考自[wxb\_nudt][wxb_nudt]的博客《[L

客官°小女子只卖身不卖艺/ 2022年08月05日 19:58/ 0 赞/ 138 阅读

相关两道面试题

1.请随机返回链表里面的一个节点（链表长度未知，不允许改变链表，不要占用太多的空间）。函数原型:ListNode\ random\_node(ListNode\ head);

末蓝、/ 2022年08月03日 05:29/ 0 赞/ 236 阅读

相关 JAVA大作业 - 五道三星题

写在前面：看了一下我的博客，发现距离上一篇博文的发表已经快一年了，深感自己的颓废，所以打算重新写博客（其实是记录= =），于是从上学期的JAVA大作业开始慢慢整理一下，就是

末蓝、/ 2022年07月26日 12:25/ 0 赞/ 184 阅读

相关 RSA加密演算法

转载出处：[https://zh.wikipedia.org/zh/RSA%E5%8A%A0%E5%AF%86%E6%BC%94%E7%AE%97%E6%B3%95][http

爱被打了一巴掌/ 2022年07月17日 00:15/ 0 赞/ 177 阅读

相关神奇的λ演算

现在时兴讲函数式编程，弄得如果不会写两句λ表达式你都不好意思跟人说自己是敲代码的。所以我也就趁着这阵风头，琢磨琢磨了这个函数式编程。怎么算来，也有个三年两载了，出师还不敢说，将

短命女/ 2022年06月16日 06:50/ 0 赞/ 173 阅读

相关 Hadoop综合大作业&补交作业两次

一、用Hive对爬虫大作业产生的文本文件词频统计。 ①启动hadoop： ![1023856-20180525193431890-948863887.png][] ②将文

左手的ㄟ右手/ 2021年09月20日 13:58/ 0 赞/ 329 阅读