Trung tâm cá nhân
sách gpt4 ai đã đi

Lập trình hàm từ đầu (2) - ChurchBoolean Coding

In lại 作者：撒哈拉 更新时间：2025-02-11 19:16:04 57 4
mua khóa gpt4 Nike

[!quote] 关于λ表达式…… 详见λ表达式 。

⚠ 本文导出自Obsidian，可能存在格式偏差（例如链接、Callout等） 本文地址：https://www.cnblogs.com/oberon-zjt0806/p/18710283 。

Mục lục
  • λ演算与λ代数
    • Church 编码
      • Church-Boolean 逻辑编码
        • 条件选择函数
        • 真与假 | True | False
        • 逻辑运算 | AND | OR | NOT
          • 合取 | 且 | AND
          • 析取 | 或 | OR
          • 反转 | 非 | NOT

λ演算与λ代数

上一整节我们利用λ符号体系构建了一套表达式系统，从这里开始，我们将正式开始利用这套系统进行代数应用，在进行演算之前，需要先利用符号体系构建一个代数运算系统.

[!note] 命名终究只是命名 虽然我们之前使用了很多诸如(+ x 1)等等这样的形式，但它们只是我们定义的命名，所以无论是x还是+和1，都只是一个记号而已，尽管我们根据以往的经验为这些符号赋予了某些我们所熟知的含义，但在当前的λ演算语境下，这些东西都还没定义过.

Church 编码

为了使λ演算能够具体应用到计算机和程序上，那么就意味着λ代数系统必须能够表示如下两种东西—— 。

  • 数值（逻辑值、整数……）
  • 运算（算符、函数、操作……）

也就是说，这些东西要在λ演算中映射为λ表达式（使用表达式来表示）.

[!tip] 粗暴地说，Church编码就是一种把数值和运算编码为λ表达式的过程.

  • 但注意！Church编码并非唯一的编码方式，还有其他的编码方式，如Scott编码等。
  • Church编码的特点在于以数值表示为起点进行编码，并在基础上构建其他编码。

Church-Boolean 逻辑编码

[!abstract] Church-Boolean 编码汇总 为了方便查阅，这里将本节所有的编码定义列出来，正文是比较冗长的推导过程 。

DEF T = λx.λy.x DEF F = λx.λy.y DEF AND = λP.λQ.(P Q P) DEF OR = λP.λQ.(P P Q) DEF NOT = λP.λQ.(P F T)

首先我们需要通过Church编码构建出布尔运算系统。之所以先选择布尔代数，是因为布尔代数的结构简单，性质清晰，比较容易构建.

布尔代数（Boolean Algebra）包含的内容非常简单—— 。

  • 布尔域\(\mathbb B\)中只包含两个元素\(\mathrm T\)Và\(\mathrm F\)
  • 支持三种基本运算\(\wedge\) ,\(\vee\),\(\neg\) .
  • 运算对域封闭，且对于\(\wedge\)Và\(\vee\)都在\(\mathbb B\)上分别存在上界和下界

条件选择函数

在介绍Church-Boolean中的真假值前，我们先来考察条件选择函数，所谓条件选择函数就是下面这样的一个三元函数—— 。

\[\operatorname{COND} (c,x,y) = \begin{cases} x, &c=\mathrm{T} \\ y, &c=\mathrm{F} \end{cases} \]

其中\(c\)是条件值，条件选择函数根据\(c\)的值就在\(x\)和\(y\)中做出选择。可以发现，实际上，这个条件选择函数就对应了大多数编程语言中的三元运算符c ? x : y.

我们将这个运算表示为IF-THEN-ELSE形式，可以表示为—— 。

IF c THEN x ELSE y

可以发现这里分为3个子部—— 。

  • IF c ：判断c的条件；
  • THEN x：当c == true被满足时，选择x;
  • ELSE y：上述条件不成立时，选择và;

至此，我们可以把这三个部分抽象为三个λ表达式.

DEF cond = λc.λx.λy.(c x y)

由于真假值承载于c中，因此我们就利用c来对真假值进行编码.

真与假 | True | False

基于上面的想法，我们就能够通过Church编码定义出逻辑的真值T和假值F。讨论c的情况，根据定义，cond函数应当满足—— 。

cond T x y => λc.λx.λy.(c x y) T x y => λx.λy.(T x y) x y => T x y => x COND F x y => λc.λx.λy.(c x y) T x y => λx.λy.(F x y) x y => F x y => y

观察倒数两步归约，我们发现 。

  • 欲使T x y => x，那么就要求(T x) y必须发生η归约.
    • 也就是说(T x)ở giữa约束不生效，可以构建自由表达式(T x) == λb.x
      • 再脱去对x的运用，解开约束对，意味着我们需要引入一个新的约束变量
      • 于是我们就可以得到T == λa.λb.a.
  • 欲使F x y => y，那么就要求(F x) y必须发生β归约.
    • 而且更进一步地，(F x) == identity == λb.b
      • 类似地，再脱去对x的运用，解开约束对，引入另外的约束变量 λa
      • 于是F == λa.λb.b

[!tip] 反归约技巧 我们知道对于运用(f x)进行归约时，会将f中受约束的变量替换为参数x，例如(λa.a x) => x 那么，反过来对于已知的某一表达式x如果想要引入约束，或者把x作为参数提出来，那么就需要引入新的不冲突的约束命名，x => (λy.y x)。 利用这种性质在已知(f x)的情况下可以展开f == λa.(f a) 。

^9b9507 。

经过α转换，将a更名为x，b更名为y，我们就可以得出T和F的定义 。

DEF T = λx.λy.x DEF F = λx.λy.y

这种定义下的T和F被映射为λ函数，因此可以作为一种条件选择函数来运用.

可以将上述定义代入表达式(c x y)通过[[λ表达式#归约 消解|归约]]来证明这个编码的正确性—— 。

[!warning] 注意 归约化简时，不要忘记变量约束的右结合律和函数运用的左结合律 。

(T T F) => (λx.λy.x λx.λy.x λx.λy.y) β|=> (λx.λy.(λx.λy.x) λx.λy.y) α|=> (λy.(λa.λb.a) λx.λy.y) η|=> (λa.λb.a) α|=> (λx.λy.x) => T (F T F) => (λx.λy.y λx.λy.x λx.λy.y) η|=> (λy.y λx.λy.y) β|=> (λx.λy.y) => F // alternatively, ==> identity F => F

逻辑运算 | AND | OR | NOT

接下来要对逻辑运算进行Church编码，这里先给出三种基本逻辑运算的真值表—— 。

MỘT B MỘT AND B MỘT OR B NOT MỘT
F F F F T
F T F T T
T F F T F
T T T T F

XOR、NAND之类的都可以在这三种基本运算的基础上组合出来。所以我们姑且只定义上面三个基本运算即可.

在正式开始之前，我们先考察一个东西——既然T和F都被映射为函数，那么意味着他们可以相互作为函数和参数构成约束对进行运用，那么约束对能否归约，以及归约后的结果是什么，这里给出两个基本函数相互运用的归约结果—— 。

T T => (λx.λy.x) (λx.λy.x) β|=> λy.(λx.λy.x) α|=> λy.(λa.λb.a) => λy.T T F => (λx.λy.x) (λx.λy.y) β|=> λy.(λx.λy.y) α|=> λy.(λa.λb.b) => λy.F [i.e.] T P => λy.P T P Q => P F T => (λx.λy.y) (λx.λy.x) η|=> λy.y => identity F F => (λx.λy.y) (λx.λy.y) η|=> λy.y => identity [i.e.] F P => λy.y => identity F P Q => Q

^6686a8 。

需要注意的是，归约结果中的T和F中的x和y和外层约束的y没有任何关系，而是出现了命名冲突（如果要展开那么需要进行一次α转换），所以实际上这里的T是自由表达式。在上面的归约过程中，我们可以归纳出如下性质—— 。

  • 如果以T作为函数运用(T P)（其中P,Q in {T, F}），那么会通过β归约Sẽx替换为P从而得到一个新的函子λy.P，且Q不受và的约束。
    • 把这个结果λy.P再作为函数并传入参数Q构成约束对，那么下一步将发生η归约，消去λy约束，最终只会剩下P（T P Q => λy.Q Q => Q)
  • 如果以F作为函数，那么由于Fcủaλx并没有进行约束，所以先进行η归约，消去λx约束，最终总会留下λy.y，好巧不巧地，这正好是恒等函数identity
    • 那接下来就很清晰了，如果再传入参数Q，由于identity的性质，或者直接通过β归约替换，则会只留下后面的这个参数P（F P Q => identity Q => λy.y Q => Q)

![Church T F.svg]] 。

完成上面的工作有助于我们通过Church编码来定义逻辑运算.

合取 | 且 | AND

首先来看一下合取运算，合取的要求是只有当两个输入均为T，才可以被归约为T，其他情形全部为F—— 。

AND T Q => Q AND T => (F P) AND F Q => F AND F => (T P)

观察上面的形式，对于AND P Q ，我们可以做出如下归纳 。

  • khiP==Tgiờ,AND P Q => AND T Q => Q
    • 这种情况对应[[#^6686a8|上面]]的(F P)，于是AND T Q => F P Q
  • khiP==Fgiờ,AND P Q => AND F Q => F
    • 这种情况对应[[#^6686a8|上面]]的(T P)，于是AND F Q => T P Q

[!question] 麻烦了 目前我们归纳出的结论是AND P == (NOT P) P，然而问题在于我们还没有定义过NOT， 这怎么办呢?

[!tip] 还好 AND满足交换律，也就是说应当有AND P Q == AND Q P 。

通过交换律将AND P Q换成AND Q P，不影响先前的结论，除了讨论对象此时从AND P变成了AND Q.

AND Q P[P:=T] => Q AND Q => (T Q) AND Q P[P:=F] => AND Q F => F AND Q => (F Q) AND Q => (P Q)

终于我们可以得出AND的Church编码—— 。

DEF AND = λP.λQ.(P Q P)
析取 | 或 | OR

与合取类似，析取也具有交换律，并且我们也可以效仿刚才的过程完成OR的定义，首先考察 。

OR T Q => T OR T => (T P) OR F Q => Q OR F => (F P)

这次无需交换律了，直接替换就能够得到OR的定义—— 。

DEF OR = λP.λQ.(P P Q)
反转 | 非 | NOT

NOT比较特别，因为NOT是一个一元运算，需要单独讨论.

NOT T == NOT λx.λy.x => F == λx.λy.y NOT F == NOT λx.λy.y => T == λx.λy.x

简单来说，输入的参数是选择其中一个，那么NOT的输出总是选择另外一个。考虑到真假值T和F均是通过cond定义的，那么，如果直接反转cond的定义是不是就能够得到相反的输出?

cond == λc.λx.λy.(c x y) ncond == λc.λx.λy.(c y x)

于是我们得到了一种NOT的定义形式 。

DEF NOT1 = λP.λx.λy.(P y x)

这个形式看起来比较底层，我们能不能利用已有的逻辑值来定义呢?

再次考察 cond P —— 。

cond P => λP.λx.λy.(P x y) P => λx.λy.(P x y)

如果考虑将x替换为F，y替换为T，也能达成同样的效果，于是我们进一步提供参数—— 。

cond P F T => λx.λy.(P x y) F T => P F T

于是我们得到了另一种NOT的定义—— 。

DEF NOT2 = λP.(P F T)

通过归约可证明，NOT1 <=> NOT2 。

至此，两个逻辑值和三个基本逻辑运算被定义完毕，Church-Boolean编码完成，可以使用λ表达式进行逻辑演算了.

[!question] 思考 不妨试试用类似的方式定义出更多的逻辑运算，例如异或XOR、与非NAND等…… 。

最后此篇关于从零开始的函数式编程(2)——ChurchBoolean编码的文章就讲到这里了,如果你想了解更多关于从零开始的函数式编程(2)——ChurchBoolean编码的内容请搜索CFSDN的文章或继续浏览相关文章，希望大家以后支持我的博客！ 。

57 4 0
Bài viết được đề xuất: Những tính năng mới nào đã được nâng cấp từ JDK8 lên JDK17? Những loại nào khác thường được sử dụng và hữu ích?
Bài viết được đề xuất: Một cuộc thảo luận ngắn gọn về các nguyên tắc cơ bản của hệ thống cấu trúc bộ nhớ .NETCore (môi trường Windows)
Bài viết được đề xuất: AI định hình lại thị trường lao động như thế nào: phân tích chuyên sâu dựa trên dữ liệu của Claude
Bài viết được đề xuất: Một cách tiếp cận mới để hiện thực hóa tương tác gốc Blazor/MAUI (Phần 2)
Sa mạc Sahara
Hồ sơ cá nhân

Tôi là một lập trình viên xuất sắc, rất giỏi!

Nhận phiếu giảm giá Didi Taxi miễn phí
Mã giảm giá Didi Taxi
Các bài viết nóng hổi trên toàn bộ trang web
Giấy chứng nhận ICP Bắc Kinh số 000000
Hợp tác quảng cáo: 1813099741@qq.com 6ren.com