zoukankan      html  css  js  c++  java
  • lambda演算

    先了解下相关的知识点(以下都只用先了解简单的概念,建议wiki):

    BNF范式,上下文无关文法,函数柯里化。

    lambda读书笔记演算:

    http://www.blogjava.net/wxb_nudt/archive/2005/05/15/4311.aspx

    lambda演算实例

    关于lambda演算的定义和解释的确有点让人迷糊,主要不是因为lambda演算有多复杂,而是一些基本概念没有归入正确位置的原因。

    这里先写一点草稿,在实践中学习和领悟lambda演算到底是个什么东西。

    一:自然数运算:

    在lambda演算中的邱奇数定义
    0 = λf.λx.x
    1 = λf.λx.f x
    2 = λf.λx.f (f x)
    3 = λf.λx.f (f (f x))

    SUCC = λn.λf.λx.f(n f x)

    SUCC是一个有三个自由变量的函数

    计算
    SUCC 0
    =λn.λf.λx.f (n f x) 0 //将0代入n
    =λf.λx.f (0 f x) //0=λf.λx.x
    =λf.λx.f (λf.λx.x f x) //λf.λx.x f x是将两个参数的函数λf.λx.x应用于(f x)这两个值的结果,结果等于x
    =λf.λx.f x //正好等于1的邱奇数定义

    SUCC 1
    =λn.λf.λx.f (n f x) 1 //将1代入n
    =λf.λx.f (1 f x) //0=λf.λx.x
    =λf.λx.f (λf.λx.(f x) f x) //λf.λx.(f x) f x是将两个参数的函数λf.λx.(f x)应用于(f x)这两个值的结果,结果等于(f x)
    =λf.λx.f (f x) //正好等于2的邱奇数定义

    小节:
    不妨把lambda演算看做一个自动机,你输入一个式子(一个λ项),它就给你输出一个演算结果,至于输入和输出有什么意义,是我们自己赋予的。

    比如为了计算0的后继,我们只是输入(λn.λf.λx.f(n f x) λf.λx.x)给这个机器,这个机器就会给我们输出λf.λx.f x。在解释这个输入输出关系时,我们会说,SUCC 0 = 1,这样就赋予这个运算一个意义。这个自动机知道自己在做加1操作吗?其实它什么也不知道。

    为什么邱奇数这样定义?其实不妨把它们看做是被偶然发现的一些λ项,这些λ项的组合项的演算结果恰好能对应于自然数的运算而已。定义自然数还有别的定义方式,邱奇数及对应的运算符只是其中的一种而已。

    比如我们又发现一个λ项PLUS
    PLUS = λm.λn.λf.λx.m f (n f x)
    先不要管什么意义,试试下面这个组合起来的λ项

    PLUS 2 3
    = λm.λn.λf.λx.m f (n f x) 2 3 //将3和2应用于m,n这两个自由变量上
    =λf.λx.3 f (2 f x) //(2 f x) = (λf.λx.(f (f x)) f x) = f (f x)
    =λf.λx.3 f (f (f x)) //3=λf.λx.f (f (f x))
    =λf.λx.(λf.λx.f (f (f x)))) f (f (f x)) //将f 和 (f (f x)) 应用于f和x这两个自由变量上
    =λf.λx.f (f (f (f (f x)))) //我们发现正好等于5的邱奇数定义

    很奇妙的性质,我们用PLUS(λm.λn.λf.λx.m f (n f x) )这样的λ项作用于代表2和3的邱奇数时,得到的演算结果恰恰是代表5的邱奇数。

    此外,还可以构造出乘法和除法等各种运算符。



    二、逻辑运算:

    TRUE := λx y.x
    FALSE := λx y.y
    AND := λp q.p q FALSE
    OR := λp q.p TRUE q
    NOT := λp.p FALSE TRUE
    IFTHENELSE := λp x y.p x y

    需要重复加以强调的是,这些λ项都是一些构造,我们构造它们的原因是,这些项的组合所得到的演算结果恰恰符合我们对逻辑运算的认识,所以我们才赋予它们以逻辑运算符的意义,也正因为这些构造,我们才可以让那个演算自动机代替我们去做各种逻辑运算。

    计算:

    AND TRUE TRUE
    =λp q.p q FALSE (TRUE TRUE)//用TRUE和FALSE替换自由变量p和q
    =TRUE TRUE FALSE //TRUE = λx y.x
    =λx y.x (TRUE FALSE) //用TRUE和FALSE替换自由变量x和y
    =TRUE //y没有在函数体中出现,所以等于TRUE

    三、有序对
    CONS := λx y.λp.IF p x y
    CAR := λx.x TRUE
    CDR := λx.x FALSE

    这里很有趣的一点是,和lisp的实现对照,我们发现car和cdr是在lisp的基本运算符中的,但实际上,它们仍然可以用λ项来表示。

    我们先构造一个有序对
    CONS m1 m2
    =λx y.λp.IF p x y (m1 m2) //很简单,用m1和m2替换x和y就行了
    =λp.IF p m1 m2


    然后计算这个有序对的CAR
    CAR (IF p m1 m2)
    =λx.(x TRUE) (λp.IF p m1 m2) //x用(λp.IF p m1 m2)替换
    =(λp.IF p m1 m2) TRUE //p用TRUE替换
    =IF TRUE m1 m2 //根据IF的含义我们知道结果就是m1
    =m1

    CDR (IF p m1 m2)
    = λx.x FALSE (λp.IF p m1 m2)
    =(λp.IF p m1 m2) FALSE
    =IF FALSE m1 m2
    =m2

    四、Y不动点

    考虑一下这台λ演算自动机,它再简单不过了,只是按照非常简单的规则应用函数,将值绑定到自由变量,然后继续演算,直到最终结果。

    在开始计算时,我们输入的都是长长的λ项,甚至连SUCC,CDR这些简写都没有,比如要做一个2+3的加法,我们会输入 λm.λn.λf.λx.m f (n f x) (λf.λx.f (f x)) (λf.λx.f (f (f x))),然后这台演算自动机会给我们输出λf.λx.f (f (f (f (f x))))这个结果。

    这样问题就来了,如果函数要递归调用自己,那该怎么办呢?在lambda演算中,无法定义包含自身的函数(虽然在lisp中可以)。
    构造出这样一个Y
    Y = λf.(λx.f(x x)) (λx.f(x x))
    Y g
    = (λf.(λx.f(x x))(λx.f(x x))) g //用g替换f
    = λx.g(x x) (λx.g(x x)) //用λx.g(x x)替换x这个自由变量
    = g (λx.g (x x) λx.g (x x)) //我们发现λx.g (x x) λx.g (x x)恰好等于Y g
    = g (Y g)
    继续
    = g (λx.g (x x) λx.g (x x))
    = g (g (λx.g (x x) λx.g (x x)))
    = g (g (g (λx.g (x x) λx.g (x x))))
    = ... ...

    这里我们能看出来了,如果给这个演算自动机输入Y g,也就是实际上输入了这样一个λ项(λf.(λx.f(x x)) (λx.f(x x)) g)之后,演算自动机将不会停机,永远递归下去,直到耗尽所有内存。

    从这里可以看出来,虽然lambda演算表面上不能自己调用自己,因为无法给自己起一个名字,但实际上可以构造出这样一个λ项,可以让计算递归下去。

    接下来,看如何利用这一特殊的λ项的性质,来完成一些有用的计算:

    计算阶乘的数学公式如下:
    fact(n) = if n=0 then 1 else n * fact(n-1)

    构造如下的λ项,计算5的阶乘,其中Y=λf.(λx.f(x x)) (λx.f(x x)),而g=λf n.(ISZERO n 1 MULT n·f(n-1)),都是λ项的形式。

    (λn.(ISZERO n 1 (MULT n ((Y g)(n-1)))) 5
    =
    (按照维基百科上的计算过程,改写为容易懂的if then else形式)

    if 5 = 0 then 1 else 5·(g(Y g,5-1))
    5·(g(Y g)4)
    5·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 4)
    5·(if 4 = 0 then 1 else 4·(g(Y g,4-1)))
    5·(4·(g(Y g)3))
    5·(4·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 3))
    5·(4·(if 3 = 0 then 1 else 3·(g(Y g,3-1))))
    5·(4·(3·(g(Y g)2)))

  • 相关阅读:
    [CTF隐写]png中CRC检验错误的分析
    Bugku
    Bugku
    【CTF 攻略】CTF比赛中关于zip的总结
    sqlserver中利用Tran_sql把逗号分隔的字符串拆成临时表
    H5摇一摇遇到的问题
    C# MVC 微信支付之微信模板消息推送
    各种大型网站技术架构
    ORM框架详解
    显示实现接口
  • 原文地址:https://www.cnblogs.com/foohack/p/3972607.html
Copyright © 2011-2022 走看看