ChurchNumber和函数式初探
前言
挺早就在ctf里见到有关lambda表达式来出题，当时啥也不懂，就xjb调一调，弄一弄，猜一猜还真给做出来了。大概之后又过了几个月又见到lambda的题了，那次好好研究了一下，最后做出来了，也感受到了函数式编程的妙，以及了解了邱奇数和邱奇布尔值的一些知识，当时很自信，感觉会了。然后再xctf上就被lambda revenge暴打了，看了一天没做出来，赛后放源码看了看，发现自己还是太naive，这里稍微做些总结，免得下次再有lambda的题到处去搜表达式。
因为lambda表达式有很多种写法，这里统一使用python代码作为表示形式，感觉比较工程。
函数式编程
在函数式编程的世界里，函数被视为一等公民。这一概念在许多地方都能看到，所以不再赘述。从我自己的感受来说，函数式编程中的所有事物都可以看作是一个过程，或者也可以称之为函数。只有当我们向这个函数传入具体的参数时，这个过程才会产生一个结果。
在函数式编程中，一个函数的输入和输出都可能是另一个函数。这使得复杂的过程可以被拆分成简单函数的组合。换句话说，一个复杂的功能函数可以被拆分成许多底层的简单函数。整个过程在传入具体值之前可能没有实际意义，又或者根据传入的函数不同会有不同的功能。这种拆分和组合为函数式编程带来了强大的表达能力和灵活性。
柯里化
柯里化是一种把函数标准化的方式，有的函数可能接收很多参数，柯里化就是将这种接收很多参数的函数变为接收一个参数的函数。
例如：
1 | # 未柯里化 |
add函数是一个接收两个参数的函数，柯里化后的add_k函数是接收一个参数的函数。实际上add_k在接收到第一个参数后会返回一个接收一个参数的函数，这个时候再将第二个参数传入才会最终执行加法。
柯里化之后的lambda表达式更容易处理，下文的所有式子也都是柯里化后的表达式。
ChurchNumber
邱奇数
邱奇数是定义在函数上的一类数，它本身也是一个函数，可以传入参数。
邱奇数的前几个数定义如下：
ZERO = lambda f: lambda x: x
ONE = lambda f: lambda x: f(x)
TWO = lambda f: lambda x: f(f(x))
简单来说，如果x外部套c了层f，这个表达式对应的数字就是c。
可以使用函数来将邱奇数转换成对应的整数，只要传入f = lambda n: n+1和x = 0，代码如下：
1 | f = lambda n: n+1 |
邱奇数的运算
有了数的定义，接下来是一些运算的定义：
后继： SUCC = lambda n: lambda f: lambda x: f(n(f)(x))
这个式子相当于再n外面再套了一层f，所以结果是n+1。
加法：ADD = lambda n: lambda m: lambda f: lambda x: m(f)(n(f)(x))
这个式子相当于把m最里面的x替换成了n，所以结果是n+m。
乘法：MUL = lambda n: lambda m: lambda f: lambda x: m(n(f))(x)
这个式子相当于把m里面的f替换成了n个f，所以结果是n*m。
指数：EXP = lambda n: lambda m: lambda f: lambda x: n(m)(f)(x)
这个式子稍微化一下：
1 | lambda n: lambda m: lambda f: lambda x: n(m)(f)(x) |
所以结果是m**n
前驱：PRED = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda h: x)(lambda h: h)
好像没啥简便的证法，最后结果是n-1。需要注意的是PRED(ZERO)结果还是ZERO。
减法：SUB = lambda n: lambda m: n(PRED)(m)
一种naive的想法是直接运行n次PRED，由于church数的定义就是将f运行n次，所以m-n可以简单地定义为n(PRED)(m)，同理，当m-n<0的时候会返回ZERO。
除法：太复杂了。。
邱奇布尔值
简单定义一下True和False
TRUE = lambda x: lambda y: x
FALSE = lambda x: lambda y: y
True和False区别在于选择第一个参数还是第二个参数。
邱奇布尔值的运算
与：AND = lambda x: lambda y: x(y)(x)
如果x为真则返回y，否则返回x，所以结果是x and y。
或：OR = lambda x: lambda y: x(x)(y)
如果x为真则返回x，否则返回y，所以结果是x or y。
非：NOT = lambda x: x(FALSE)(TRUE) 或者 NOT = lambda n: lambda x: lambda y: n(y)(x)
条件判断：IF = lambda n: lambda x: lambda y: n(x)(y)
如果n为真则返回x，否则返回y。
布尔运算相对简单，也很容易推导。
函数式运算
这一部分相当杂项，而且很多定义也并不唯一。
IsZero
永假表达式：ALWAYS_FALSE = lambda x: FALSE
判断是否为0：ISZERO = lambda n: n(ALWAYS_FALSE)(TRUE)
只有当n == ZERO的时候ISZERO会返回TRUE。
Pair
定义pair：PAIR = lambda x: lambda y: lambda b: b(x)(y)
PAIR操作定义了一个二元组，首先传入二元组中的两个元素x和y，之后根据传入的b决定返回x还是y。
有了PAIR我们可以继续定义FIRST和SECOND操作，分别对应从pair中取出第一个元素和第二个元素。
first操作：FIRST = lambda p: p(TRUE)
first操作：SECOND = lambda p: p(FALSE)
用法如下：
1 | p = PAIR(ONE)(TWO) |
List
接下来定义list，list是一个pair的嵌套，以Null结尾。
为了定义list，我们先要定义Null和判断是否为Null。
Null：NULL = lambda x: TRUE
判断是否为Null：ISNULL = lambda v: v(lambda x: lambda y: FALSE)
判断是否为Null只能在list中使用，更准确的说，传入的v必须是NULL或者是接收两个参数的函数。
另一种减法
使用pair实现pred操作，需要首先定义一个函数next。
next：_NEXT = lambda x: PAIR(SECOND(x))(SUCC(SECOND(x)))
如果传入的是(x-1, x)则会返回(x, x+1)。
在这个基础上实现的pred操作。
pred：_PRED = lambda n: FIRST(n(_NEXT)(PAIR(ZERO)(ZERO)))
由于church数的定义，n(_NEXT)(PAIR(ZERO)(ZERO))实际上就是在(0, 0)的基础上调用n次_NEXT，所以最后FIRST出来的结果就是n-1。
与church数的减法类似，也可以定义新的减法操作。
sub：_SUB = lambda n: lambda m: n(_PRED)(m)
结果为m-n。
IsEqual
判断相等：EQ = lambda n: lambdam: AND(ISZERO(SUB(n)(m)))(ISZERO(SUB(m)(n)))
Y Combinator
Y Combinator：YCOMB = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x)))
可以用来实现递归。
示例：
1 | fib = lambda f: lambda n: n if n < 2 else f(n-1) + f(n-2) |
上面这个东西在python里跑会直接爆栈，可能是python求值策略导致无限展开了。
不过有个替代品ZCOMP可以用：ZCOMP = lambda f: (lambda x: (lambda m: f(x(x))(m)))(lambda x: (lambda m: f(x(x))(m)))
1 | assert ZCOMP(fib)(7) == 13 |
可以使用递归和ISNULL判断来实现list遍历。
总表
一键导入lambda函数。
1 | ZERO = lambda f: lambda x: x |