1.什么是解释系统

宇宙的表象，即，宇宙中的符号。

符号背后有意义。

为了表达符号背后的意义，需要解释系统，来将符号映射至意义。

所以解释系统，就是，宇宙中的符号（或宇宙的表象）与意义之间的映射规则。

人类就是这样一个解释系统。

人类可以感知宇宙表象，获得表象背后的意义，意义在人感知到的就是一种体验。所以人类的体验就是解释系统的产物。

人类为了描述自身这个解释系统，将描述输出到物质上，例如文字，图像，声音。就出现了两类，模拟人的解释系统的次级解释系统。

这两类次级解释系统，分别是，逻辑系统，和直觉系统。

逻辑系统的代表是数学系统。

直觉系统的代表是艺术系统。

单说，逻辑系统，其目的是，映射符号代表的意义，即，映射符号的语义。

Lambda演算等价于数学系统，所以Lambda演算本质上就是一个系统，就是一个解释系统。就是一个模拟人的解释系统（感知系统）的次级解释系统。就是一个所谓的解释器。

所以，反过来看，数学系统也是一个解释器。

Lambda演算可以看成一个编程语言。

所以，反过来看，数学系统也是一个编程语言。

2.家谱

2.1之前的认知：

逻辑系统是爷爷

数学系统是爸爸

Lambda演算是儿子

2.2现在的认知：

宇宙第一义是爷爷

逻辑系统是爸爸，直觉系统是妈妈

数学系统是哥哥，Lambda演算是弟弟。（弟弟比哥哥更严肃）

艺术系统是姐姐。

3.Lambda演算于数学系统的区别

Lambda演算和数学系统的本质区别是，Lambda演算是一个更严谨的人，数学系统是一个更随意的人。

他们俩个虽然能力一样，性质一样，但是做事风格不一样。

如果是做工程，显然选择严肃规范理性的的人更合适。

另一个比喻，数学系统是橡皮泥，Lambda演算是乐高玩具。虽然他们都可以做玩具（业务），都可以映射小汽车（语义）。

乐高块相比橡皮泥更加规范，更加容易协作。接口一致，容易连接。（见下图）

橡皮泥 乐高

所以Lambda的优势，就在于构建复杂，需要多人协作的工程。

计算机行业，显然属于需要多人协作的工程，所以自然选择了Lambda演算作为底层解释器。

4.Lambda演算的结构？

4.1Lambda演算的地基

Lambda表达式的3条律则

1）变量（Variable）：

    形式：x

    变量名可能是一个字符或字符串，它表示一个参数（形参）或者一个值（实参）。

    e.g. z var

    本质是表示空间。   

    图像模型：乐高玩具的材料分子。

2）抽象体（Abstraction）：

    形式：λx.M

    它表示获取一个参数x并返回M的lambda函数，M是一个合法lambda表达式，且符号λ和.表示绑定变量x于该函数抽象的函数体M。简单来说就是表示一个形参为x的函数M。

    e.g. λx.y λx.(λy.xy)

    本质是函数的标准规范

    本质还是定义了Lambda演算的基础块。

    图像模型：乐高2*4的基础块（见下图）

乐高基础块

    3）应用（Application）

    形式：M N

    它表示将函数M应用于参数N，其中M、N均为合法lambda表达式。简单来说就是给函数M输入实参N。

    e.g. (λx.x) y, (λx.x) (λx.x)

    本质是Lambda表达式的连接，或者，Lambda系统基础块的连接。

    图像模型：乐高基础块的连接（见下图）

乐高基础块的连接

以上是Lambda演算（Lambda系统，我更喜欢称之为Lambda系统，因为本质上他是一个系统）的基础定义部分，也可以理解为Lambda演算的底层规则定义。属于对于实体、静态部分的定义。

下面还会有，运行、动态部分的定义。

4.2Lambda演算的运行定义

Lambda运算的2条规则：

1）beta | β 归约

    替换，例如：(λx.x+1)(3) = 3+1，左边等价于右边。

    本质是，函数的装载，即，将3作装入了函数的x变量中，函数体就变形成了3+1。

    本质还是，揭示了计算机的运行的本质是什么。运行的本质就是函数装载，就是变量替换，就是β 归约。

    本质还有，揭示了，运行本质上是非连续的。

    本质还有，揭示了，能量守恒，从整体能量的视角来看，根本没有变化。

    本质还有，宇宙的运行本质，也是β 归约，因为量子级别的电子跃迁就是非连续的。

    启发是，如果想改变你的生活状态，就去断舍离，宇宙规律β 归约会导致你的生活状态变化，因为本质是替换，能量守恒。

    图像模型：俄罗斯套娃，如果乐高能实现基础块连接后的压缩，就像俄罗斯套娃那样，就附和β 归约。

（见下图）

俄罗斯套娃

2）alpha | α 转换

    这条规则就是说，一个lambda函数抽象在更名绑定变量前后是等价的。

    形式：α: λx.x ≡ λy.y

    本质是，改变函数的电线颜色。目的是区分函数内的老变量和装载进来的新变量。

    图像模型：改变乐高块的颜色，目的是区分老乐高和新连接的乐高。

5.基础块已经定义OK，开始用基础块拼装第一个玩具吧

Lambda系统的基础已经定义OK，即，Lambda基础块，可以用这些基础块拼出第一个玩具（业务）了。

第一个玩具（业务）就是描述自然数。

描述自然数，换句话说，就是如何解释自然数，也就是，建立符号于意义的映射规则。

而，由于，Lambda系统已经有了一个底层的映射规则，我们表达自然数，就可以利用，基于这些基础块来比较方便的构建映射规则，即，更方便。

先看看其它系统如何描述自然数：

1）英语系统：｛zero，one，two，three......｝

2）汉语系统：｛零，壹，贰，叁..................}

3）阿拉伯系统：{0, 1, 2, 3............................}

4)  乐高系统:      {1个基础块, 2个基础块连接, 3个基础块连接,  4个基础块连接.....}

5)  皮亚诺公理：  {0,S(0),S(S(0)),...}

6）Lambda演算：

0 ≡ λf.λx.x

1 ≡ λf.λx.fx

2 ≡ λf.λx.f(fx)

3 ≡ λf.λx.f(f(fx))...

本质就是，用函数的连接次数，来表示自然数的语义。类比乐高块的多个块的连接。

所以，可以看出来，Lambda演算，可以用基础定义，来组装出任何数学系统的等价业务。

所以，Lambda演算，可以描述任何数学问题，数学公式。

所以，Lambda演算，等价于图灵机。

6.Lambda演算、Lambda表达式、函数、数学系统这几个概念的关系？

Lambda演算＝Lambda系统

Lambda表达式＝Lambda系统的基础，Lambda的底层解释器，定义Lambda系统中的实体。

Lambda表达式的定义＝最底层的，符合到意义的关系映射规则。

Lambda演算和数学系统都在描述函数，只不过Lambda演算中，对函数的表达更标准，因为有Lambda表达式的3条律则，作为规范。而数学对于函数的描述就很自由散漫。

函数比Lambda演算和数学系统更加抽象。函数更加接近抽象的语义。

函数不是数学系统的子集，反之，数学系统是函数的子集。

函数不是Lambda系统的子集，反之，Lambda系统是函数的子集。

万物皆函数，艺术系统也是由函数构成，数学系统也是由函数构成。

7.Lambda演算的哲学启发

1）抽象更接近语义。Lambda演算是一个系统，是一个抽象系统，抽象更接近本质，即，抽象更接近语义。

2）函数具有三位一体的特性：

    信息：函数依据的算法

    能量：函数运行的状态

    物质：函数体的代码

3）特色是舍出来的。乐高的伟大之处在于对基础块的坚守。所以，Lambda系统的伟大之处，就在于对抽象体的定义。

4）底层规则越稳定，上层业务才能越繁荣。Lambda系统对于函数的规范定义，就是稳定的底层规则。

8.总结一下：

Lambda表达式的本质是符号与意义之间的映射关系规则。

规则有3条：

1）变量（Variable）：定义空间，原子～无穷大。

2）抽象体（Abstraction）：函数的标准化，基础块，舍弃其它之后的特色样子。

3）应用（Application）：本质是连接，基础块之间的连接。

用乐高来比喻

1）变量（Variable）＝乐高的材料，即，塑料原子。

2）抽象体（Abstraction）＝乐高的2*4基础块

3）应用（Application）＝乐高块的连接能力

Lambda运算的本质是函数表达式的变量装载。

规则有2条：

1）β 归约：函数的变量替换，本质是运行。

2） α 转换：函数内部变量的颜色变化，本质是区分老旧变量。

参考：

1.λ演算(Lambda Calculus)入门基础（一）：定义与归约：https://www.jianshu.com/p/ebae04e1e47c

2.λ演算(Lambda Calculus)入门基础（二）：丘奇编码(Church Encoding)：https://www.jianshu.com/p/b157217ba13d

3.https://www.cnblogs.com/hugetong/p/9723870.html

个人理解：原来一切都是从lambda运行演进出来的，数据结构，谓词，逻辑操作，Ture，False，运算符。不过细节都没有认真的读。比较学术，应该好好读一下。

所以，整个函数式编程世界里的一切，都是基于lambda演算的定义，已经基于这个定义的推演组成的。

说一个不准确的类比，整个数学世界都是通过自然数和加法演化出来的。而自然数是通过数字0和加一函数演化出来的。我们可以理解成：0和加一的定义，就是lambda演算的定义。

如果有人让你用简单一句话说明数理逻辑和普通逻辑有什么本质不同，你该怎么说呢？回答就是：数理逻辑有函数，而普通逻辑没有。

既然逻辑的形式本质上就是函数，那么，对逻辑学的研究其实就是对函数的研究。

逻辑学由于插上了函数的翅膀才可以催生、演变为计算理论——可计算函数的研究，它的实质就是计算机科学最本质的问题：可计算性问题和计算复杂性的研究。

所谓lambda-演算，就是把函数的研究进一步抽象化，研究函数的的抽象形态、抽象形态对具体值的应用，以及函数值的最终的“实现”——β-归约。

后来甚至有人把函数的概念推广到了哲学。所以从某个程度、某个方面来说，20世纪的形式科学就是函数的科学，函数，已经成为学习计算机科学、数学、逻辑学、语言学和哲学的跨学科的共同语言。

有了函数，无论是数学、逻辑、自然语言都可以用这种统一的方式表达，这就是我们为什么要用编程语言、用Lisp、Haskell表示逻辑的最基本动机和理由。因此，熟悉这两种语言、进而熟悉它们的通用形式化表达——lambda-演算的关键，就是对函数概念的透彻理解，这里面包含了三个层次：

(1) 函数的内涵表达式——抽象；

(2) 函数符号和参数的关系——应用；

(3) 函数的代入求值。

最后，函数的外延表达式：有序对的集合和外延性原理。因为(3)的理论基础就是基于外延性原理的可替换原则。

如果对函数有了透彻的理解，你获得了一种洞见，洞若观火之见，那就是，逻辑和计算是一回事，是一个统一体的两个侧面。

4.https://blog.csdn.net/Lu_ming/article/details/1427620

λ演算是一套用于研究函数定义、函数应用和递归的形式系统。它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世纪三十年代引入，Church 运用 lambda 演算在 1936 年给出 判定性问题 (Entscheidungsproblem) 的一个否定的答案。这种演算可以用来清晰地定义什么是一个可计算函数。关于两个 lambda 演算表达式是否等价的命题无法通过一个通用的算法来解决，这是不可判定性能够证明的头一个问题，甚至还在停机问题之先。Lambda 演算对函数式编程有巨大的影响，特别是Lisp 语言。