python作的lambda 演算示例

全部關於函數式編程的介紹中都指明 lambda演算是函數式編程的數學基礎。死了很多腦細胞研究了一下維基百科上關於lambda演算的介紹文章。

參考：http://en.wikipedia.org/wiki/Lambda_calculus

普通的數學運算用這個純抽象的符號演算來定義，計算結果只能在腦子裏存在。因此寫了點代碼，來驗證文章中介紹的演算規則。

咱們來驗證文章裏介紹的天然數及天然數運算規則。說到天然數，今天還百度了一下，據度娘說，1993年後國家規定0是屬於天然數。先定義天然數及天然數的運算規則：

用lambda表達式定義天然數（邱齊數）

0 := λf.λx.x
1 := λf.λx.f x
2 := λf.λx.f (f x)
3 := λf.λx.f (f (f x))
...

上面定義直觀的意思就是數字n, 是f(x)的n階函數。1就是f(x), 2就是f(f(x))....，嚴格來講，這樣表述並不許確。其實每一個邱奇數都是一個二階函數，它有兩個變量f和x。用二元命名函數來表達就是：

0 -> num0(f,x)=x
1 -> num1(f, x)=f(x)
2 -> num2(f,x)=f(f(x))
3 -> num3(f,x)=f(f(f(x)))
...

 其中參數f是一個函數。這一段有點繞，可是不能理解這個，對後面的lambda演算理解會比較困難。

首先用遞歸法，定義邱齊數（天然數）

• 0是天然數，  度娘說1993年後，國家規定0是屬於天然數。

• 每一個天然數，都有一個後續。

用代碼表達就是：

NUM0=lambda f: lambda x:x
SUCC=lambda n: lambda f: lambda x: f(n(f)(x))

後面則是定義運算符，包括加法，乘法，減法和冪。維基文章裏沒有介紹除法，估摸着除法定義比較複雜，一時講不清楚。那咱們也不驗證了。

################################################
#define number calculus rules
################################################

#define Church numeral inductively.
#0 := λf.λx.x
#1 := λf.λx.f x
#2 := λf.λx.f (f x)
#3 := λf.λx.f (f (f x))
#...
NUM0=lambda f: lambda x:x
SUCC=lambda n: lambda f: lambda x: f(n(f)(x))

#define Operator
PLUS=lambda m: lambda n: m(SUCC)(n)
MULT= lambda m: lambda n: m(PLUS(n))(NUM0)
#define predecessor to obtain the previous number.
PRED= lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda u:x)(lambda u:u)
SUB=lambda m: lambda n: n(PRED)(m)
POW=lambda b: lambda e: e(b)

定義完了什麼是天然數和天然數的運算子。那麼天然數的運算，就能夠用lambda演算的方式計算了。

問題是上面的定義都是抽象的符號演算，咱們須要有一個編碼器來把上面的抽象的Church numeral符號編碼成能夠人來閱讀的形式，還需把人輸入的數字解碼成抽象符號。

################################################
#create encoder to input/output Church numeral
################################################

class LambdaEncoding:
    @staticmethod
    def encoding(exp,encoder):
        return encoder().encoding(exp)
    @staticmethod
    def decoding(s, decoder):
        return decoder().decoding(s)
    
class NumEncoder:
    def encoding(self,num):
        f=lambda x:x+1
        return str(num(f)(0))
    def decoding(self,s):
        n=int(s)
        num=NUM0
        for i in range(n):
            num=SUCC(num)
        return num

嗯，有了編碼器，就能夠方便的來驗證了。

################################################
#calculus demo
################################################
print("demo number calculus.\n"
      "don't input large number,"
      "it will cause to exceed maximum recursion depth!\n")

n1=input('input a number: ')
n2=input('input anohter number: ')
#decode string to Church numeral
num1=LambdaEncoding.decoding(n1,NumEncoder)
num2=LambdaEncoding.decoding(n2,NumEncoder)
    
#add
result=PLUS(num1)(num2)

print('{0} + {1} = {2}'.format(
    n1,
    n2,
    LambdaEncoding.encoding(result, NumEncoder)))

#mult
result=MULT(num1)(num2)
print('{0} X {1} = {2}'.format(
    n1,
    n2,
    LambdaEncoding.encoding(result, NumEncoder)))
#sub
result=SUB(num1)(num2)
print('{0} - {1} = {2}'.format(
    n1,
    n2,
    LambdaEncoding.encoding(result, NumEncoder)))

#POW
result=POW(num1)(num2)
print('{0} ^ {1} = {2}'.format(
    n1,
    n2,
    LambdaEncoding.encoding(result, NumEncoder)))

測試結果以下：

>>> 
demo number calculus.
don't input large number,it will cause to exceed maximum recursion depth!

input a number: 4
input anohter number: 3
4 + 3 = 7
4 X 3 = 12
4 - 3 = 1
4 ^ 3 = 64
>>>

神奇吧。