找lambda演算的感觉
初看，感觉因符号系统不熟悉，导致完全没感觉，所以先改写成自己稍微熟悉的符号。
λx.x+2
改写规则1：在此式中，将λ后的符号，在.后的符号找到，改写为( )，且将λx.删除。
λx.x+2改写为( )+2。
(λx.x+2)3
改写规则2：在此式中，将左括号删除，右括号改写为｜。
(λx.x+2)3改写为( )+2｜3。
多个参数，左结合。
λx.λy.x-y改写为λy.( )-y｜改写为( )-( )｜｜
至此，λ演算就可以改写为较为熟悉的形式了。
上面的例子其实非常不好，因为lambda演算的规则和中缀法是冲突的，反而误导了初学者。
(λx. x x)(λz.u) → (λz.u) (λz.u)
在这个例子中，为何不是归约为x (λz.u)呢？
这就用到beta规约的规则：
(λx.M)N → M[x/N] 如果N中所有变量的自由出现都在M[x/N]中保持自由出现
这句话用了条件状语后置，上例中不能用x代入到x中，就是因为，x在x中不是自由出现，而是绑定。
看到别人的评论，mark一下。
在wiki中lambda calculus的Formal definition一节中，有这样的描述：“The body of an abstraction extends as far right as possible”，也就是说λx.ab 等价于 λx.(ab)，而不是(λx.a) b。
所谓的“左结合”法则，指的是应用(application)，而非抽象(abstraction)： M N P 等价于 (M N) P。
终于把lambda演算梳理清楚了，感觉lambda演算本身的逻辑还是很棒的，但是符号还是有很大的问题，是理解lambda演算最大的障碍。
没错说的就是括号，在lambda演算中，括号至少起了两个作用，
1.对语句做划分；
2.beta规则本身的一部分：被右括号分隔开的表达式E)x是代入，被左括号分隔开的表达式E(x则不是代入。
按照语言学的观点，括号即用于划分语法结构，又用于做论元标记了。
所幸没有决定优先级的作用，但也正因为没有优先级，lambda演算的规约过程和结果都不是唯一的。
接下来尝试用lambda演算构造一下集合论。
抽象一个音系，辅音集C、复辅音集CC、元音集V、复元音集VV，允许的组合方式{V,CV,CCV,CVV,CCVV,CVC,CCVC,CVCC,CCVCC...}
看怎么把lambda表达式映射到这个集合中去。
然后大概想了下lambda演算到底是什么，元素、映射，映射分为按规则的映射，比如fx，也就是施用型表达式APPLY，（为了方便自己理解，自己先命名为内涵映射），和按象的映射，比如\x.x，也就是抽象型表达式ABSTRACTION，（为了方便自己理解，自己先命名为外延映射）。
其他的论域理论、施用型的左结合、抽象型的右结合、beta变换，都可以看作是一种论元标记规则，不是最重要的。改变这些规则会产生lambda演算的新的表达形式，以后可以尝试。
这块的想法也可以在图灵机和lambda演算的等价性证明中看看是否可靠。
2016年01月03日开始构造集合论
首先观察布尔函数的构造方法
已知T,F,AND分别定义为
λxy.x
λxy.y
λab.abF
求相应的OR,NOT的lambda编码
发现小规律
通过摆弄AND T T,AND T F,AND F T,AND F F发现，AND是个框架，最后实质上参与运算的是T和F；
所以就先看看T和F的运算规律，有：
- TTT → T
- TTF → T
- TFT → F
- TFF → F
- FFT → T
- FFF → F
- FTT → T
- FTF → F
差不多可以认为有个天生的λabc.abc这样一个布尔函数。
AND T T的可能形式：
- TTT → T
- FTT → T
- TTF → T
AND T F和AND F T的可能形式：
- TFT → F
- TFF → F
- FTF → F
AND F F的可能形式：
- FFF → F
- TFF → F
- FTF → F
然后怎么把AND的形式从中抓出来呢？
巧的是AND T F和AND F T的返回值都是F，都在TFT,TFF,FTF中，那么只需看TFT,TFF,FTF中的对称性。
结果：TFF和FTF这一对满足对1,2位的交换对称，TFT和FTF满足F,T的置换对称。
这样，就可以推测出AND的四种形式：
- λab.abF
- λab.baF
- λab.aba
- λab.bab
将以上四种形式代入AND T T和AND F F检验，全部满足。这四种形式也说明了AND满足交换律的性质。
至此，就基本掌握了寻找OR,NOT的lambda编码的一些方法。
用同样的方法得到OR的四种形式：
- λab.aTb
- λab.bTa
- λab.aab
- λab.bba
NOT只有一种形式： λab.abT。
接下来构造IFTHENELSE
因为返回值不在T,F中，就要用到另一种性质了：
- TT → RT
- TF → RF
- FF → I
- FT → I
其中RX是replace，将无论什么东西都替换为X，形式为λa.b（b为自由出现）。I是不变操作，无论什么东西都变为它本身，形式为λa.a。
尝试后，不行，再接着减少数量，用F,T的性质。发现IFTHENELSE形式很简洁漂亮：
λpmn.pmn
有(λpmn.pmn)TMN → M，(λpmn.pmn)FMN → N
然后搞自然数这块
已知Church数的形式，以及后继运算SUCC的形式。
- λnfx.f(nfx)
考虑前继PRED，加PLUS，乘MULT，乘方EXP的形式。
通过观察发现后继的原理：
- λnfx.f(nfx) n用于带入Church数，和布尔函数的做法没分别;
- λnfx.f(nfx) fx用于替换参数的λfx头部，这一点和布尔系统有区别，布尔系统的返回值的λ头部用的是参数自己的λ头部;
- λnfx.f(nfx) f用于增加返回值的f数量，完成“后继”的功能。
考虑PLUS的形式：
连续两次SUCC:
- (λnfx.f(nfx))((λnfx,f(bfx))n)
抽象一下就是f(fx),易知对n后继m次（也就是n+m）就是$$SUCC^m n$$。
接着抽象，(λfx.f^m x) SUCC n，发现前面的λfx.f^m x就是Church数m，这里我们也就开始理解Church数的意义了，其实就是个递归函数，对吧？
接着抽象，就得到PLUS的一种形式:
- λmn.m SUCC n
但是，这种形式展开写肯定很麻烦，要简洁，只能到更底层中去。已经知道λnfx.f(nfx)中的f主要完成增加f的后继功能，直接增加这里的f:
- λnfx.f^m (nfx)
抽象一下:
- λnfx.(λx.f^m x)(nfx)
搞成Church数:
- λnfx.(λfx.f^m x)f(nfx)
把其中的Church数m抽象出来:
- λmnfx.mf(nfx)
PLUS就搞好了
考虑MULT的形式：
先把m + n改写成n + n，因为乘肯定是一堆相同的数相加:
- λnfx.nf(nfx)
递归的形式已经显而易见了，那么，m个n连加:
- λnfx.(nf)^m x
抽象:
- λnfx.(λf.f^m x)(nf)
把x的带入换到内层，不过分吧？
- λnf.(λfx.f^m x)(nf)
是啊，就是为了构造Church数，把所有的递归都换成Church数:
- λmnf.m(nf)
MULT也搞好了
考虑EXP的形式：
把m * n改写成n * n:
- λnf.n(nf)
嗯，还是熟悉的味道，搞成递归:
- λnf.n^m f
抽象:
- λnf.(λfx.f^m x) nf
Church数代入:
- λmnf.mnf
反思，构造完这些函数，自然从函数怎么构造、怎么工作，开始想参数（TRUE,FALSE,Church数）是怎么构造的、怎么工作的。
可以说，Church数天生就是为了构造PLUS,MULT,EXP而构造的，PLUS,MULT,EXP本身就是一层一层递归的关系，所以将Church数构造为“将x在f中递归n次”再合适不过。
时隔一年，2016年12月23日
继续考虑如何给lambda演算设计语音方案。现在觉得搞语音方案的一个阻碍是括号，这个不用多说了，口语要表达括号、语法层次，一直是个老难题。
假如定义一个表达式K，使得 KABC = A(BC)，那么可以用 K 表达 A(BCD) 吗？
也是可以的： KKKABCD = K(KA)BCD = (KA)(BC)D = KA(BC)D = A(BCD)。
只要摆脱括号的束缚，就可以进一步和语音的单向线性结构对应上了。但K的表达式是什么呢？
还是统协体告诉我这就是组合子逻辑SKI基中的B组合子。
