当前位置: 首页 > news >正文

【Programming Languages And Lambda calculi】4.6 Lambda表达式 递归 (重要,建议彻底弄懂)

文章目录

      • 4.6 递归
      • 4.6.1 自应用递归
        • 练习4.11
          • 题解
      • 4.6.2 从自我应用弹出
      • 4.6.3 定点与Y组合子
        • 练习 4.12
          • 题解
        • 练习 4.13
          • 题解
        • 练习 4.14
          • 题解

4.6 递归

上一小节的练习要求你用实现 add 的方法实现 mult 。类似的实现体现了数字是由函数编码的信息。

给定函数 iszero,add和 sub1,我们同样可以在不知道任何数值如何被编码的前提下实现 mult 。我们必须定义一个递归程序来检查第一个参数是否为0,如果不是,将第二个参数添加到递归调用,并递减第一个参数。
在这里插入图片描述

上述定义 mult 宏的问题为,它调用了自身,所以没有方法将 mult 展开为一个纯 lambda表达式。因此,缩写是违法的。

4.6.1 自应用递归

乘法器函数如何获得自己的句柄?在 mult 宏被定义时,乘数函数的定义暂时不可用,而该定义在稍后才可用。特别的,当我们调用乘数函数得时候,我们必须有一个乘数函数的句柄。

因此,与直接引用自身不同,乘数函数可以让我们提供一个多重函数 t (它自身) 以及用于乘法的参数。更加精确地说,采用这种策略,我们定义的宏将不再是一个乘数函数,而是一个乘法器的制造者:它接收一些函数 t 并产生一个乘数函数,此函数将会期待两个参数并将它们相乘:
在这里插入图片描述

这个 mkmult0 宏即被定义完整了。并且(mkmult0 t)产出一个乘数函数… 当 t 是乘数函数的时候!很明显,我们到目前为止仍然没有一个乘数函数。我们尝试将原来的 mult 定义本身参数化,但这样做之后就会失去 mult 的定义。

尽管我们无法提供 t 作为乘数函数,我们可以提供 t 作为乘数函数制造者。这想法会奏效,还是会造成无限的循环倒退?事实是,作为制造者确实能奏效。

假设将制造者应用于制造者就可以产生一个乘法器。则,应用于制造者的初始的参数 t 为制造者。 制造者的 body 部分,不管何处需要一个乘法器,我们使用 (t t) —— 因为 t 将会是一个制造者,并且应用一个制造者于自身将会生产出一个乘法器。下述是一个制造者 mkmult1 ,其期待一个制造者的参数:
在这里插入图片描述

如果 mkmulti1 奏效,我们可以通过应用其自身得到乘数函数:
在这里插入图片描述

我们尝试将这个函数应用在 0 和 m(随机的m)上并看返回的是不是 0 。我们将只在必要的时候展开宏,并且我们假设 iszero 和 0 将会正确实现。
在这里插入图片描述

目前为止,一切都正常。如果我们将非零的 n 乘以 m,会得到什么?
在这里插入图片描述

由于 mult = (mkmult1 mkmult1),上述过程的最后一步也可以被写作 (add m (mult (sub1 n) m))

因此,
在这里插入图片描述

这正是我们需要的 mult add sub1 0 之间的关系。

练习4.11

定义一个 mksum 宏,使得 (mksum mksum) 表现得和一个求和函数一致,它将消费一个数字 n 并且将 0 到 n 的所有自然数相加返回。

题解

mksum ≐ λt.λn if (iszero n) 0 (add ((t t) (sub1 n)) n)

4.6.2 从自我应用弹出

上小节的方法能够让我们定义任何我们想要的递归函数。不过,这有点笨拙,因为我们必须定义一个制造函数,该函数会递归应用一个初始参数于自身。为了简便,我们需要将自应用的模式拉入其自身的抽象定义中。

更具体地说,我们需要一个函数,称其为 mk,它可以接收任何像 mkmult0 这样的制造者,并且生产出函数。举例来说,(mk mkmult0) 会生产一个乘法器。
在这里插入图片描述

上述 mk 的定义是有缺陷的,但是我们可以由此糟糕的定义出发。mk 函数需要接收一个制造者 t 并且生产一个操作函数。即调用 (mk t) 则制造一个操作函数。

我们可以借助上一小节的方法来修复循环定义的 mk :
在这里插入图片描述

接下来让我们来验证 (mk mkmult0) 的行为是否与 mult 一致:
在这里插入图片描述

4.6.3 定点与Y组合子

mk 函数现在看上去或许有点神秘。不知怎么的,它使 mkmult0 有用了,尽管 mkmult0 的设定是只有将乘法器传递给它之后它才能产出乘法器!

一般来说, mkmult0 可能接收任何函数,并且得到的“乘法器”将会由各种不同的行为,输出的函数通常也会与输入的函数有很大的不同。但是 mk 设法为 mkmult0 选择了一个输入函数,这样输出函数与输入函数保持相同。换句话说,mk 会找到 mkmult0 的定点。

事实证明,mk 可以找到任何函数的定点,换句话说,如果将 mk 应用于 M 产生 N,那么应用 M 于 N 将会再次产生相同的 N。

定理 4.1 对于任何 MM (mk M) =n (mk M)

定理 4.1的证明: 由于 =n 是 →→n 的对称闭合,我们可以通过证明 M →→n M (mk M) 间接证明该定理:
在这里插入图片描述

一个类似 mk 的行为的函数被称为 定点算子 。mk 函数只是它们中的一员。更加著名的定点算子被称为 Y:
在这里插入图片描述

一般来说 Y 让我们更方便地定义递归函数。例如,我们可以这样定义 sum
在这里插入图片描述

由于我们没有必要重复一个制造者表达式,我们可以略过 中间制造者 mksum,而直接应用 Y 于制造者函数。

此外,看到上述 sum 定义地程序员,会立即注意到 Y,看到 s 是Y的参数的参数,然后发现 λn… 作为递归函数 s 的定义。

练习 4.12

证明对于任何 MM (Y M) =n (Y M)

题解

(Y M)
= ((λf.(λx.f (x x)) (λx.f (x x))) M)
nβ (λx.M (x x)) (λx.M (x x))
nβ (M ((λx.M (x x)) (λx.M (x x))))

M (Y M)
= M ((λf.(λx.f (x x)) (λx.f (x x))) M)
nβ (M ((λx.M (x x)) (λx.M (x x))))

左边=右边,因此成立。

练习 4.13

定义 Lisp 地址对的编码,它由以下宏组成:

  • null,一个常量
  • cons,两个参数,返回一个地址对
  • car,如果参数为 null ,返回 true;如果参数为 地址对 ,返回 false
  • cdr,接收地址对为参数并且返回地址对的第二个元素。

你的编码必须满足以下等式:
在这里插入图片描述
你的编码不需要为表达式指定任何特定的含义,如 (car null) 或是 (car cons)

题解
  • null ≐ ⟨true, false
  • consλM.λNfalse, ⟨M, N⟩⟩
  • isnullλM.fst M
  • carλM.fst (snd M)
  • cdrλM.snd (snd M)

练习 4.14

使用你上个练习完成的编码,定义 length,它接收一个布尔值的列表,返回列表中的地址对。布尔值列表要么是 null,要么是 (cons b l),其中 b 为 布尔值, l 是布尔值的列表。

题解

lengthY (λf.λM.if (isnull M) 0 (add1 (f (cdr M))))

相关文章:

  • 【Programming Languages And Lambda calculi】4.7~4.8 关于Lambda演算的一些事实 范式 历史 第四章完
  • 【LWC】轻巧的加载预显示行 UI组件 - loading-place-holder #lwc组件 #Salesforce #用户体验
  • 【Programming Languages And Lambda calculi】现实语言模型 5.1 ISWIM表达式
  • 【web development】输入框单击回车隐式提交表单的禁用与讨论 enter keypress inside input causing form submit
  • 【Salesforce】VSCode中找不到 Salesforce Cli 的 Org Broswer 云图标的解决办法
  • 【Salesforce】生产环境元数据版本备份 、还原完整方案 Production Metadata backup recover solution
  • 【Programming Languages And Lambda calculi】5.2 ISWIM 约化
  • 【Apex】Apex 报错 System.StringException: Invalid id: 的解决办法 / 判断查找字段非空
  • 【LWC】Lightning标准/自定义编辑表单组件中,<lightning-messages> 标签显示错误信息的两种方法 show error messages in lwc edit-form
  • npm 设置模组安装路径以及缓存路径
  • 【LWC】lightning-input-field参照字段值响应式清除失效的解决方法 #hack trick
  • 【Salesforce / LWC】LWC中使用第三方库开发 Use Third-Party JavaScript Libraries In LWC
  • 【读完掌握】JavaScript 中 Array.prototype.map() 的定义、特点、易错点、使用技巧 返回undefined的解决方法
  • 【Salesforce】 使用自定义通知功能
  • 【Salesforce】soql 中检索不到某些自定义字段的解决方法 ERROR at No such column ‘ ‘ on entity ‘ ‘
  • [译]CSS 居中(Center)方法大合集
  • 30天自制操作系统-2
  • 77. Combinations
  • android 一些 utils
  • Java-详解HashMap
  • LeetCode18.四数之和 JavaScript
  • Mac转Windows的拯救指南
  • Python打包系统简单入门
  • React-redux的原理以及使用
  • Redis学习笔记 - pipline(流水线、管道)
  • SpringBoot 实战 (三) | 配置文件详解
  • 警报:线上事故之CountDownLatch的威力
  • 码农张的Bug人生 - 初来乍到
  • 前端每日实战:70# 视频演示如何用纯 CSS 创作一只徘徊的果冻怪兽
  • 腾讯优测优分享 | Android碎片化问题小结——关于闪光灯的那些事儿
  • 微服务入门【系列视频课程】
  • 微信小程序填坑清单
  • 用Node EJS写一个爬虫脚本每天定时给心爱的她发一封暖心邮件
  • gunicorn工作原理
  • 阿里云服务器如何修改远程端口?
  • 如何用纯 CSS 创作一个货车 loader
  • #mysql 8.0 踩坑日记
  • #pragam once 和 #ifndef 预编译头
  • #pragma 指令
  • #考研#计算机文化知识1(局域网及网络互联)
  • #我与Java虚拟机的故事#连载19:等我技术变强了,我会去看你的 ​
  • %3cli%3e连接html页面,html+canvas实现屏幕截取
  • (31)对象的克隆
  • (BFS)hdoj2377-Bus Pass
  • (八)光盘的挂载与解挂、挂载CentOS镜像、rpm安装软件详细学习笔记
  • (十一)手动添加用户和文件的特殊权限
  • (已更新)关于Visual Studio 2019安装时VS installer无法下载文件,进度条为0,显示网络有问题的解决办法
  • (原創) 博客園正式支援VHDL語法著色功能 (SOC) (VHDL)
  • (原創) 如何將struct塞進vector? (C/C++) (STL)
  • (转)真正的中国天气api接口xml,json(求加精) ...
  • .NET Compact Framework 3.5 支持 WCF 的子集
  • .net core使用RPC方式进行高效的HTTP服务访问
  • .NET6使用MiniExcel根据数据源横向导出头部标题及数据
  • .NET处理HTTP请求
  • .net反混淆脱壳工具de4dot的使用