幻灭？Lambda Calculus
\(\lambda\) 演算
趁着国庆还没结束，看了 Introduction to Lambda Calculus (Barendregt-1998).
\(\lambda\) 演算的建立源于莱布尼茨的设想：
Leibniz had as ideal the following.
(1) Create a ‘universal language’ in which all possible problems can be stated.
(2) Find a decision method to solve all the problems stated in the universal language.
莱布尼茨：首要的问题是如何表示问题。
我（去年或前年）：自动推理首要的问题是如何（用计算机）表示（数学）问题。
几乎相同的问题，没想到我和丘奇不谋而合，给出了几乎相同的回答。
幻灭
丘奇的回答建立在如下定义之上：
Definition. The set of \(\lambda\)-terms (notation \(\Lambda\)) is built up from an infinite set of variables \(V = \{v, v', v'', \ldots\}\) using application and (function) abstraction.
\[x ∈ V ⇒ x ∈ Λ,\] \[M, N ∈ Λ ⇒ (MN) ∈ Λ,\] \[M ∈ Λ, x ∈ V ⇒ (λxM) ∈ Λ.\]翻译一下，这三个等式分别对应抽象，复合，再抽象。
这三条核心逻辑是我在不断实践-理论-实践中提炼出来的，没想到，竟会撞车。
差异
前功不可尽弃，我比较了方法的不同：
-
丘奇只抽象函数，同时所有量都视为函数；
-
我对函数，标量，集合，序列等都做抽象，不同量各有不同。
-
丘奇的应用是逐项进行的，应用得到的量和分别的量有层次关系，但不清晰；
-
我的复合是多项一次进行的，复合得到的量和分别的量有清晰的层次关系。
主观地认为不同的根源在于出发点的不同。
丘奇是一个数学家，做定义的时候追求极致的简洁，数学追求剔除所有可以剔除的东西。所以所有量看成函数，应用也是逐项进行的，用最简洁，最一般的方式搭建体系。
我，砖工，追求的是最合适的表达，实践遇到问题还会不停修正。
不同量分别处理是更实际的，都视为函数，或者都视为集合之类的，只会让定义看起来简洁，不会对程序的实质带来帮助，反而会加大实现的难度。
逐项进行应用简化了程序的逻辑，却增加了实现的困难。更重要的是丢失了清晰的层次关系，层次关系是自动推理的关键。
图灵
自此，两位计算机理论的上古大神终于都稍微接触了。
不管是图灵机，还是\(\lambda\)演算，都只有两个东西，编码和转换。所谓计算机理论的基础，全在于此。
\(\lambda\)演算用\(\lambda\)项编码，用\(\lambda\)项的应用进行状态转移。
图灵机用纸带符号编码，规则表转换。
有人说丘奇人气不如图灵是因为\(\lambda\)演算更难懂，曲高和寡。
不以为然，图灵抓住了计算的本质，丘奇做了同样的事但是没有明确区分编码和转换。固然可以说是因为数学家追求表达的统一，但却是没有道理的，就像统一概念和陈述一般，无益。
有人说编程就是数据结构加算法，也有人说深度学习就是数据加模型，这都可以看成编码和转换的实例。
更进一步，说面对象编程可取是说它抓住了编码先于转换这一事实，即所谓的数据先于逻辑，而不是所谓的封装，继承，多态。
编码和转换
\(\lambda\)演算追求转换的简洁，牺牲了编码的简洁，最基础的自然数编码如下：
\[0 = \lambda f.\lambda x.x\] \[1 = \lambda f.\lambda x.f x\] \[2 = \lambda f.\lambda x.f (f x)\]图灵机编码很简洁，规则表的建立相对变得复杂。
可以看到编码和转换是会相互制约的，而我的工作，从这个角度来看就是如何平衡二者。
抽象-复合-再抽象，解析器的搭建，实质是维护了多套编码。底层编码保留简洁，顶层编码追求转换的简洁。而这套追求简洁的编码，自然而然的就和同样追求简洁的\(\lambda\)演算十分相似。
初心
幻灭之余，想到的是小当家做鲶鱼面，破局的关键在回归原点。
我的原点，或曰初心，是实现这样一个自动推理体系：
-
完成自动证明，并且证明人类可读；
-
证明的内在逻辑和人类的逻辑一致。
1是受吴文俊院士启发，不同在于可读性，有了可读性才有更大的可用性。
2是基于这样一种哲学，证明机器的复杂程度必定高过能解决问题的复杂程度。数学问题领域之广，难度之大，每一个曾经致力于其中的人都能明白；证明机器要想成功，就必须依赖于已有的数学理论和思想。要想站上巨人的肩膀，其内在逻辑就必须和人类的逻辑一致。这也是我不看好现有形式化证明系统的原因。
而完成这个想法的第一步，就是问题的表示问题。
我既然有比莱布尼茨更大的想法，就需要提出比图灵丘奇更好的方法。当然不是创造力上的，我的核心想法是和已有的一致，故而重点在于剖析咀嚼已有的方法，进一步提出更深入的理解。从这个角度来说，我做的是欧几里得的工作。
或者说，想要像欧几里得那样，改写数学的历史。