最近，我一直在为λ演算发明一个可视化的书写系统。
兰姆达演算(λ演算)是一种原始函数式编程，最初是由阿隆佐·丘奇发明的，当时他正试图解决导致图灵发明图灵机的相同问题。这是关于计算的另一种推理方式。
Python的λ是从λ演算中借用的一个想法。在Python中，您可以使用如下所示的lambda表达式来定义返回数字平方的函数：
在λ演算中，想法是相同的：我们使用λ创建一个函数，以指定函数接受哪些参数，然后给出函数返回值的表达式。纯lambda演算不包括任何类型的运算符--只是应用于其他函数的函数--因此，如果我们试图编写一个平方函数，我们必须假设乘法是已经定义的两个变量的函数：
一旦定义了Square函数，就可以将其应用于参数并计算为更简单的值。
平方4=(λx乘x x)4=乘4 4=16。
关于λ演算最酷的事情之一是，我们可以使用λ演算来表示最常见的编程抽象，即使它只是一些函数：数字、算术、布尔值、列表、IF语句、循环、递归…。名单还在继续。在介绍我一直在使用的可视化书写系统之前，让我们先绕个弯，讨论一下如何使用lambda演算来表示数字和算术。
阿隆佐·丘奇(Alonzo Church)想出了如何将数字表示为λ函数；这些数字被称为教会数字。
只要我们有两件事，我们就可以表示任何非负整数：(1)0的值；(2)后继函数，它对任何数字n返回n+1。要将数字表示为函数，我们需要将z(零)和s(后继)作为参数传入，然后从那里开始。每个数字实际上都是这两个输入的函数。
Zero=λs.Z.λZ.Zone=λs.λZ.s zTwo=λs.λZ.s(S Z)Three=λs.λZ.s(s(S Z))。
如何实现ZERO和后继者的实际细节应该像其他人的问题一样实现-我们没有它们也可以生存。我们所关心的是我们的数字做了正确的事情，考虑到某人可能提供的任何零和后继者。
加法呢？加法是一个函数，它接受两个数字(让我们称它们为x和y)，并产生一个表示它们总和的数字。为了将它们加在一起，我们需要生成一个数字，该数字应用于s(后继函数)，总共x+y次。例如，我们可以先将它应用于零y次，然后再对该结果应用x次。
PLUS=λx.λy.(λs.λZ.x s(Y S Z))。
让我们试着证明一加一等于二。在λ演算中，这个证明如下所示：
One=λs.λZ.s zTwo=λs.λZ.s(S Z)加上=λx.λy.(λs.λZ.x s(Y S Z))加上一=(λx.λy.(λs.λZ.x s(Y S Z)One One=λs.λZ.One s(One S Z)=λs.λz.(λs.λZ.s z)s(One S Z)=λs.λZ.s。Z)s z)=λs.λz.s(S Z)=2。
在那个证明中，有很多拉姆达斯、括号和论点被推来推去。在脑海中匹配括号是一件烦人的事。Scope特别烦人：在λs.λz.(λs.λZ.s z)s(One S Z)中，我又在看哪一个s，内部的还是外部的？
线性的lambdas和圆括号字符串对于为正在进行的计算提供直观来说是一种无效的方式。这个问题也不是lambda演算独有的；请考虑尝试使用线性字符串表示二叉树：
毫不含糊，但不是很直观。将该表示与我们试图在黑板上解释相同的二叉树时使用的图表进行对比，这是一种更直观的表示法：
我记得，当我能像这样直观地推理构造时，编程构造会更好：当我想象将数组切成两半进行二进制搜索时，当我想象链表中的指针被拖来拖去插入新元素时，当我想象上下遍历二叉树的分支时，我记得编程更好。
为什么Lambda微积分不能以同样的方式获得一些视觉直觉呢？Lambda演算是流经函数并被函数操纵的变量的舞蹈，我想要一个Lambda演算的书写系统，它将直观地显示这种舞蹈。它看起来不应该像一串串括号和符号：它应该创造视觉直觉。
经过反复试验，以下是我想出的系统。我瞄准的是类似电路的东西。
值沿着连接流动，它们可以作为参数传递给函数，也可以作为函数本身应用。有些是输入，有些是输出。
函数表示为方框，一边应用于它们的输入，另一边生成单个输出。符号必须指明应用哪个函数；这可以在框本身内绘制，也可以从其他值连接到框的中间。
参数表示为输入，来自图的右侧；这些参数可能通过函数传递，也可能是要应用的函数本身。如果参数尚未传入，则它是开始连接的空箭头；如果已传入参数，则将其值附加到连接。参数总是按照从上到下的顺序传递。
例如，下面的函数接受两个函数f和g，然后是值x，并返回f(G X)：
作为另一个示例，下面是M组合符M=λx.x x(To Mock a Mockingbird中的“Mockingbird”)：
这里是教会数字4=λs.λZ.s(S Z))，用λ电路画出：
让我们从前面的证明中得到一加一等于二的证明。取而代之的是，在λ电路中绘制校样是什么样子的？
我们也可以考虑乘法。乘法函数将接受两个数字m和n，并计算一个新的数字，该数字是它们的乘积。在λ微积分中，我们会这样写：
Lambda电路的优点之一是它完全消除了对变量名的需要。
λ演算还有另一个符号也可以做到这一点：de Bruijn指数。用de Bruijn索引编写的lambda表达式指出了使用正整数的地方使用了哪些变量；整数越小，它引用的参数传入的时间就越近。
例如，身份函数λx.x可以用de Bruijn索引写成，如下所示：
代表两个人的教会数字λs.λZ.s(S Z)可以这样写：
加法函数λx.λy.(λs.λz.x s(Y S Z))可以这样写：
加1=(λλ(λλ4 2(3 2 1))(λλ2 1)(λλ2 1)=(λ(λλ(λλ2 1)2(3 2 1))(λλ2 1)=λλ(λλ2 1)2((λλ2 1)2 1)=λλ(λλ2 1)2(2 1)=λλ2(2 1)。
编写λ演算解释器的一个棘手问题是正确的重命名规则；de Bruijn索引很方便，因为它们消除了对此的需要。Lambda电路在本质上类似于de Bruijn索引，因为它根本不需要变量名，而是通过将值直接连接到指示它们何时传入的箭头来指示哪些变量被传递到何处。
我将提供更多示例来进一步演示符号在不同情况下的工作方式。让我们考虑“参数切换”函数C，其中Cfxy返回fyx。(这实际上是C组合器。)。
假设我们尝试将其应用于一个愚蠢的函数f，其中f x y丢弃y，只返回x，然后，Cf应该切换f的参数，创建一个返回y的函数。让我们来检查一下：
F=λx.λy.xc f=λf.λx.λy.(F Y X)f=λx.λy.f y x=λx.λy.(λx.λy.x)y x=λx.λy.y。
我们也可以尝试一个函数g，其中g x y返回x y，然后C g x y应该返回y x。让我们检查一下：
G=λx.λy.x yc g x y=λf.λx.λy.(F Y X)g x y=g y x=(λx.λy.x y)y x=y x。
练习：演示应用C两次可使其反转。也就是说，表明对于任何f，C(Cf)都返回f。(请注意，Cf是一个函数，它接受两个参数x和y，并返回f y x。像这样将C仅应用于f是部分应用。)。
“解剖一只知更鸟”描述了一种符号，它实际上与我描述的符号非常相似，并在“模拟一只知更鸟”中的各种问题上进行了演示。我喜欢这样看起来，特别是每个函数都被圆的两半包围起来，这使得该函数可以如何应用变得显而易见。我的符号没有这个功能，但因此需要绘制更少的封闭方框。
Visual lambda(代码、基础、纸张)将lambda表达式表示为彩色气泡，并提供操作它们的界面。
鳄鱼蛋是一个基于λ演算的益智游戏的描述，它恰好也提供了一种使用和计算lambda表达式的可视化方式。
后两个恰好没有满足我个人的审美目标：它们使用颜色来代表变量名称，而我想要的是在精神上更接近de Bruijn指数的东西，通过仔细放置符号或导线来提供计算意义-但它们仍然很漂亮。
可以在维基百科：Lambda演算以及教科书类型和编程语言中找到关于Lambda演算的一些更具体、更具体的细节的解释。
“模仿一只知更鸟”是一本很棒的益智书，也是组合子微积分的入门；我读了它并写出了一些校对，找到了λ电路符号中一些问题的答案，我从中获得了很多乐趣。