精华内容
下载资源
问答
  • lambda演算

    2021-02-03 15:37:00
    lambda演算 初版 public class TestLambda1 { public static void main(String[] args) { ILike like = new Like(); like.lambda(); } } interface ILike{ void lambda(); } class Like implements ILike{ ...

    lambda演算

    初版

    public class TestLambda1 {
    
        public static void main(String[] args) {
            ILike like = new Like();
            like.lambda();
        }
    }
    
    interface ILike{
        void lambda();
    }
    
    class Like implements ILike{
    
        @Override
        public void lambda() {
            System.out.println("i like lambda");
        }
    }
    

    进阶版1.0

    public class TestLambda1 {
        /**
         * 静态内部类
         */
        static class Like implements ILike{
            @Override
            public void lambda() {
                System.out.println("i like lambda");
            }
        }
        public static void main(String[] args) {
            ILike like = new Like();
            like.lambda();
        }
    }
    
    /**
     * 定义一个函数式接口
     */
    interface ILike{
        void lambda();
    }
    

    进阶版2.0

    public class TestLambda1 {
        public static void main(String[] args) {
            /**
             * 局部内部类
             */
            class Like implements ILike{
                @Override
                public void lambda() {
                    System.out.println("i like lambda");
                }
            }
    //        方法调用
            ILike like = new Like();
            like.lambda();
        }
    }
    
    /**
     * 定义一个函数式接口
     */
    interface ILike{
        void lambda();
    }
    

    进阶3.0

    public class TestLambda1 {
        public static void main(String[] args) {
            /**
             * 匿名部类(PS:没有类的名称,必须借助接口或父类)
             */
            ILike like = new ILike() {
                @Override
                public void lambda() {
                    System.out.println("i like lambda");
                }
            };
            like.lambda();
        }
    }
    
    /**
     * 定义一个函数接口
     */
    interface ILike{
        void lambda();
    }
    

    进阶4.0

    public class TestLambda1 {
        public static void main(String[] args) {
            /**
             * lambda表达式
             */
            ILike like = ()->{
                System.out.println("i like lambda");
            };
            like.lambda();
        }
    }
    
    /**
     * 定义一个函数式接口
     */
    interface ILike{
        void lambda();
    }
    

    进阶4.0(同理可得出有参的)

    public class TestLambda1 {
        public static void main(String[] args) {
            /**
             * lambda表达式
             */
            ILike like = (int i)->{
                System.out.println("i like lambda" + i);
            };
    //        调用方法
            like.lambda(123);
        }
    }
    
    /**
     * 定义一个函数接口
     */
    interface ILike{
        void lambda(int i);
    }
    

    完善4.1

    public class TestLambda1 {
        public static void main(String[] args) {
            /**
             * lambda表达式:简化参数类型
             */
            ILike like = (i)->{
                System.out.println("i like lambda" + i);
            };
    //        调用方法
            like.lambda(123);
        }
    }
    
    /**
     * 定义一个函数接口
     */
    interface ILike{
        void lambda(int i);
    }
    

    完善4.2

    public class TestLambda1 {
        public static void main(String[] args) {
            /**
             * lambda表达式:简化括号
             */
            ILike like = i->{
                System.out.println("i like lambda" + i);
            };
    //        调用方法
            like.lambda(123);
        }
    }
    
    /**
     * 定义一个函数接口
     */
    interface ILike{
        void lambda(int i);
    }
    

    完善4.3

    public class TestLambda1 {
        public static void main(String[] args) {
            /**
             * lambda表达式:简化去掉花括号
             */
            ILike like = i->
                System.out.println("i like lambda" + i);
    //        调用方法
            like.lambda(123);
        }
    }
    
    /**
     * 定义一个函数接口
     */
    interface ILike{
        void lambda(int i);
    }
    

    总结

    1、lambda表达式只能有一行代码的情况下才能简化成为一行,如果有多行,那么就用代码块包裹

    2、前提是接口为函数式接口(只有一个抽象类)

    3、多个参数也可以去掉参数类型,要去掉就都去掉,必须加上括号

    展开全文
  • Lambda演算

    2020-12-18 09:39:59
    Lambda演算 1.括号省略 (1)单独出现的λ项:最外层()可省略 (2)应用型λ项:左结合 (\x.x x) n m n = ((\x.x x) n ) m n = n n m n (\x.\y.x y) n m n = ((\x.\y.x y)n m)n = n m n a (\x.x ) b 无结果,而a ...

    Lambda演算

    1.括号省略

    (1)单独出现的λ项:最外层()可省略

    (2)应用型λ项:左结合

    (\x.x x) n m n = ((\x.x x) n ) m n = n n m n
    (\x.\y.x y) n m n = ((\x.\y.x y)n m)n = n m n
    a (\x.x ) b 无结果,而a ( (\x.x) b ) = a b

    (3)抽象型λ项:

    \x.\y.x y a \z.z = \x.\y.(x y a \z.z)
    (\x.\y.x y) a \z.z = a \z.z
    \g.(\x.g(x x))\x.g(x x) = \g.( (\x.g(x x)) \x.g(x x) )

    2.不完全结合

    ###(1)(\x.\y.x y \z.z)a = \y.a y \z.z
    (2)(\y.a y \z.z)b c = a b (\z.z) c 由于左结合原理,该算式是一个λ项
    3.符号替换
    I = \x.x
    S = \x.\y.\z.x z (y z)
    L = S I
    求L m n
    (\x.\y.\z.x z (y z)) \x.x m n = \x.x n (m n) = n (m n)
    自带括号,是应用型,不是抽象型,遵循左结合原理

    展开全文
  • Lambda演算的类型 我们已经掌握了直觉逻辑(Intuitionistic Logic,IL),我们再回到lambda演算:我们已经得到了我们需要定义模型的逻辑工具。 当然,在没有更简单的事情了,对吧? 到目前为止我们讨论的都是简单...

    Lambda演算的类型


    我们已经掌握了直觉逻辑(Intuitionistic Logic,IL),

    ------------------------------------------------------------------------------------
    PS:这一小段是笔者扩充说明下:直觉逻辑。总所周知,最为著名的“经典逻辑(classical logic)/一阶逻辑”是学习逻辑的一个起点,以及其他逻辑作为参照的标杆。经典逻辑侧重“真值”,陈述的“真值”是其“绝对”特征。一个无歧义的合式陈述(well-formed statement)或真或假。假即非真,真即非假,是为“排中律”。它强调排中律。例如:基于经典逻辑,我们可以“非构造地”证明一个命题。如下图:

                                     
    上面的证明虽然在经典逻辑里没有问题,但我们仍无法确定究竟哪一种情况是正确的。除此之外,我们还可以做出一个构造性证明(constructive proof):对于 x= \sqrt2 \ ,y = 2 log_2\ 3, 我们有 x^y =3 \in Q。这种“构造式”的推理方式对应着“直觉主义逻辑”(intuitionistic logic)。直觉主义逻辑的哲学基础是,不存在绝对真理,只存在理想化数学家(创造主体)的知识和直觉主义构建。逻辑判断为真当且仅当创造主题可以核实它。所以,直觉主义逻辑不接受排中律

    直觉主义命题逻辑,或称直觉主义命题演算(Intuitionistic propositional calculus, IPC),的语言和经典命题逻辑的语言是一样的。直觉主义逻辑里的语义不是通过真值表来判断的,而是通过构建模式来解释的。这就是著名的BHK释义(Brouwer-Heyting-Kolmogorov interpretation)。Heyting 是 Brouwer的学生。Kolmogorov有个著名的学生叫Martin-Löf。如下:   

                                    
    有很多逻辑式在经典逻辑里是重言式(tautology),但在直觉主义逻辑里却没有构造。如常见的排中律、双重否定消除、De Morgan定律、反证法等等。直觉主义逻辑的一个证明系统是自然演绎系统  ,其中J代表直觉主义逻辑。NK是经典逻辑的自然演绎系统。

    布尔代数是经典逻辑的一种语义诠释,而海廷代数则是直觉主义逻辑的代数语义学。在直觉主义逻辑里,我们关注的首要问题是“可证明性”(provability),而非“真值”。 详情除了上述的链接外,还可以参考:直觉主义逻辑

    ------------------------------------------------------------------------------------

    我们再回到lambda演算:我们已经得到了我们需要定义模型的逻辑工具。 当然,在没有更简单的事情了,对吧?

    到目前为止我们讨论的都是简单的无类型lambda演算。一如丘奇首次提出LC的第一个版本。但它存在一些问题,为了解决这些问题,人们引入了「类型」(type)的概念,于是出现了简单类型lambda演算,之后出现了各种变种 —— SystemT,SystemF,Lambda立方(和时间立方没啥关系:-))等等。最终,人们意识到无类型lambda演算实际上是类型化lambda演算的一个简单到病态的特例 —— 只有一个类型的LC。

    lambda演算的语义在类型化演算中最容易理解。现在,我们来看看最简单的类型化LC,叫做「简单类型化lambda演算」(simply typed lambda calculus);以及它如何在语义上等同于直觉逻辑。(其实上,每个种类型化LC都对应于一种IL,而且每个LC中的beta规约都对应于IL中的一步推理,这就是为什么我们需要先跑去介绍直觉逻辑,然后再回到这里。)

    类型化lambda演算的主要变化是增加了一个叫做「基类型」(base types)的概念。在类型化lambda演算中,你可以使用一些由原子值构成的论域(universe), 这些值分为不同的简单类型。基类型通常由单个的小写希腊字母命名,然而这正好是Blogger的痛处(普通html文本打不出希腊字母),我只好用大写英文字母来代替类型名称。因此,例如,我们可以有一个类型「N」,它由包含了自然数集合,也可以有一个类型「B」,对应布尔值true / false,以及一个对应于字符串类型的类「S」。

    现在我们有了基本类型,接下来我们讨论函数的类型。函数将一种类型(参数的类型)的值映射到的第二种类型(返回值的类型)的值。对于一个接受类型A的输入参数,并且返回类型B的值的函数,我们将它的类型写为A -> B 。「 ->」叫做函数类型构造器(function type constructor),它是右关联的,所以 A -> B -> C 表示 A -> (B -> C)。

    为了将类型应用于lambda演算,我们还要做几件事情。首先,我们需要更新语法,使我们可以包含类型信息。第二,我们需要添加一套规则,以表示哪些类型化程序是合法的。

    语法部分很简单。我们添加了一个「:」符号; 冒号左侧是表达式或变量的绑定,其右侧是类型规范。 它表明,其左侧拥有其右侧指定的类型。举几个例子:

    • lambda x : N . x + 3。表示参数x 类型为N ,即自然数。这里没有指明函数的结果的类型;但我们知道,函数「+」的类型是 N -> N ,于是可以推断,函数结果的类型是N。
    • (lambda x . x + 3) : N -> N,这和上面一样,但类型声明被提了出来,所以它给出了lambda表达式作为一个整体的类型。这一次我们可以推出 x : N ,因为该函数的类型为 N -> N,这意味着该函数参数的类型为 N 。
    • lambda x : N, y : B . if y then x * x else x。这是个两个参数的函数,第一个参数类型是 N ,第二个的类型是 B 。我们可以推断返回类型为 N 。于是整个函数的类型是 N -> B -> N 。乍看之下有点奇怪;但请记住,lambda演算实际上只有单个参数;多参数函数的写法只是柯里化的简写。所以实际上这个函数是:lambda x : N . (lambda y : B . if y then x * x else x);内层lambda的类型是 B -> N ; 外层类型是 N -> (B -> N)

    为了讨论程序是否关于类型合法(即「良类型的」(well-typed) ),我们需要引入一套类型推理规则。当使用这些规则推理一个表达式的类型时,我们称之为类型判断(type judgement)。类型推理和判断使我们能推断lambda表达式的类型;如果表达式的任一部分和类型判断结果不一致,则表达式非法。(丘奇开始研究类型化LC的动机之一是区分「原子」值和「谓词」值,他通过使用类型以确保谓词不能操作谓词,以试图避免的哥德尔式的悖论。)

    我将采用一套不太正规的符号表示类型判断;标准符号太难用我目前使用的软件渲染了。常用的符号跟分数有点像;分子由我们已知为真的语句组成;分母则是我们可以从分子中推断出来的东西。 我们经常在分子中使用一个叫「上下文」(context)的概念,它包含了一组我们已知为真的语句,通常表示为一个大写的希腊字母。这里我用大写的希腊字母的名称表示。如果一个类型上下文包含声明”x : A,我会写成 CONTEXT |- x : A。对于分数形式的推理符号,我用两行表示,分子一行标有「Given: 」,分母一行标有「Infer: 」。 (正常符号用法可以访问维基百科的STLC页 。)

    **规则1:(类型标识) **

    Given: nothing 
    Infer: x : A |- x : A 
    

    最简单的规则:如果我们只知道变量的类型声明,那么我们知道这个变量是它所声明的类型。

    **规则2:(类型不变式) **

    Given: GAMMA |- x : A, x != y 
    Infer: (GAMMA + y : B) |- x : A 
    

    这是不干涉语句。 如果我们知道 x : A,那么我们可以推断出其他任何类型判断都不能改变我们对x的类型推断。

    规则3:(参数到函数的推理)

    Given: (GAMMA + x : A) |- y : B 
    Infer: GAMMA |- (lambda x : A . y) : A -> B 
    

    这个语句使我们能够推断函数的类型:如果我们知道函数参数的类型是 A,而且该函数返回值的类型是 B ,那么我们可以推出函数的类型为 A -> B 。

    最后,Rule4:(函数应用推理)

    Given: GAMMA |- x : A -> B, GAMMA |- y : A 
    Infer: GAMMA |- (x y) : B 
    

    如果我们知道一个函数的类型为 A -> B ,且把它应用到类型为A的值上,那么结果是类型为 B 的表达式。

    规则就是这四个。如果我们有一个lambda表达式,且表达式中每一项的类型判断都保持一致,那么表达式就是良类型化的(well-typed)。如果不是,则表达式非法。

    下面我们找点刺激,描述下SKI组合子的类型。这些都是不完整的类型——我用的是类型变量,而不是具体的类型。 在真正使用组合子的程序中,你可以找到实际类型来替换类型变量。 别担心,我会用一个例​​子来阐明这一点。

    • I组合子: (lambda x . x) : A -> A
    • K组合子: (lambda x : A . ((lambda y : B . x) : B -> A)): A -> B -> A
    • S组合子: (lambda x : A -> B-> C . (lambda y : A -> B . (lambda z : A . (x z : B -> C) (y z : B)))) : (A -> B -> C) -> (A -> B) -> C

    现在,让我们来看一个简单的lambda演算表达式:lambda x y . y x。由于没有任何关于类型的声明或参数,我们无法知道确切的类型。但是,我们知道,x一定具有某种类型,我们称之为A;而且我们知道,y是一个函数,它以x作为应用的参数,所以它的参数类型为A,但它的结果类型是未知的。因此,利用类型变量,我们有 x : A, y : A -> B。我们可以通过看分析完整的具体表达式来确定A 和 B 。所以,让我们用x = 3,和y = lambda a : N. a * a 来计算类型。假设我们的类型上下文已经包含了 * 的类型为 “N -> N -> N“。

    • (lambda x y . y x) 3 (lambda a : N . a * a)
    • 3是整数,所以它的类型是: 3 : N 。
    • 根据规则4,我们可以推出出表达式 a * a 的类型是 N,其中 a : N (*的类型:N -> N -> N),因此,由规则3,lambda表达式的类型是 N - > N 。 于是,我们的表达式现在变成了:(lambda x y . y x) (3 : N) (lambda a : N . (a * a) : N) : N -> N
    • 所以 —— 现在我们知道,第一个lambda的参数 x 须是 N 类型,以及 y是 N -> N 类型 。根据规则4我们知道,应用表达式的类型 y x 一定是 N ,然后根据规则3,表达式的类型为: N -> (N -> N) -> N 。
    • 所以此处的类型 A 和 B 最后都是N

    所以,现在我们得到了一个简单的类型化lambda演算。说它是简单的类型化,是因为这里对类型的处理方式很少:建立新类型的唯一途径就是通过「 ->」 构造器。其他的类型化lambda演算包括了定义「参数化类型」(parametric types)的能力,它将类型表示为不同类型的函数。

     

    终章,Lambda演算建模——程序即证明!


    我们已经讲过直觉逻辑(intuitionistic logic)和它的模型;从无类型的Lambda演算讲到了简单类型化Lambda演算;终于,我们可以看看Lambda演算模型了。而这正是真正有趣的地方。

    先来考虑简单类型化Lambda演算中的类型。任何可以从下面语法生成的形式都是Lambda演算类型:

    type ::= primitive | function | ( type ) 
    primitive ::= A | B | C | D | ... 
    function ::= type -> type 
    

    这个语法中的一个陷阱是,你可以创建一个类型的表达式,而且它们是合法的类型定义,但是你无法你写出一个拥有该类型的单独的,完整的,封闭表达式。(封闭表达式是指没有自由变量的表达式。)如果一个表达式类型有类型,我们说表达式「居留」(inhabit)该类型,而该类型是一个居留类型。如果没有表达式可以居留类型,我们说这是「不可居留的」(uninhabitable) 。

    那么什么是居留类型和不可居留类型之间的区别?

    答案来自一种叫做「柯里-霍华德同构」(Curry-Howard isomorphism)的理论。这种理论提出,每个类型化的lambda演算,都有相应的直觉逻辑;类型表达式是可居留的当且仅当该类型是在对应逻辑上的定理。

    先看类型 A -> A。现在,我们不把 -> 看作函数类型构造器,而把它视作逻辑蕴涵。A 蕴含 A 显然是直觉主义逻辑的定理。因此,类型 A -> A 是可居留的。

    再来看看 A -> B 。这不是一个定理,除非在某个上下文中能证明它。作为一个函数类型,这表示一类函数,在不包括任何上下文的情况下,以A类型作为参数,并返回一个不同类型B。你没法做到这一点——必须有某个上下文提供B类型的值——为了访问这个上下文,必须存在某种允许函数访问它的上下文的方式:一个自由变量。这一点在逻辑上和lambda演算上是一样的:你需要某种上下文建立 A->B 作为一个定理(在逻辑上)或可居留的类型(在lambda演算上)。

    下面就容易理解些了。如果有一个封闭LC表达式,其类型是在相应的直觉逻辑中的定理,那么,该类型的表达式就是定理的一个证明。每个Beta规约则等同于逻辑中的一个推理步骤。对应于这个lambda演算的逻辑就是它的模型。从某种意义上说,lambda演算和直觉逻辑,只是同一件事的不同反映。

    有两种方式可以证明这个同构:一种是柯里当初采用的,组合子演算的方式;另一种则用到了所谓的「相继式演算」(Sequent calculus)。我会组合子证明的版本,所以下面我会快速的过一遍。以后,很可能下个礼拜,我会讲相继式演算的版本。

    让我们回忆一下什么是模型。模型是一种表示演算中的每条声明(statement)在某些具体值域上都合法的方式——所以存在具体实体和演算中的实体的对应关系,凡演算中的声明都对应真正的实体的某些声明。所以我们实际上并不需要做充分的同构;我们只需要一个从演算到逻辑的同态(homomorphism)。(同构是双向的,从演算到逻辑和逻辑到演算;而同态只从演算到逻辑。)

    所以我们需要做的是取任意完整的lambda演算表达式,然后将其转化为一系列合法的的直觉逻辑语句。由于直觉逻辑本身已被证明是合法的,如果我们可以把lambda演算翻译成IL,这样我们就证明了lambda演算的合法性——这意味着我们将表明,在lambda演算中的计算是合法的计算,以及lambda演算是一个完全的,合法的,有效的计算系统。

    我们如何从组合子(它们只是省去了变量的lambda演算的简写)得到直觉逻辑?它实际上简单得令人难以相信。

    直觉逻辑中的所有证明可以归结为一系列的步骤,其中的每一步都是使用了以下两个基本公理之一的推理:

    • A implies B implies A
    • (A implies B implies C) implies ((A implies B) implies (A implies C))

    让我们用箭头重写它们,让它们看起来像一个类型:A -> B -> A ;及(A -> B -> C) -> ((A -> B) -> (A -> C))

    眼熟吗?不熟的话再回头看看简单类型化lambda演算。这就是S和K组合子的类型。

    接下来的建模步骤就很明显了。lambda演算的类型对应于直觉逻辑的原子类型。函数是推理规则。每个函数可以规约为一个组合子表达式;每个组合子表达式是直觉逻辑的某个基本推理规则的实例。于是,函数就成了相应逻辑里的定理的一个构造性证明。

    酷吧?

    (任何正常人看完会说“什么?”,但,我显然不是正常人,我是一个数学怪咖。)

    展开全文
  • 依赖类型 Lambda 演算 概括 这是我在围绕依赖类型扭曲我的头的存储库。 贡献 是的,请这样做! 有关指南,请参阅。 执照 参见。 版权所有 (c) 2015 Jeremy Bi。
  • lambda演算简介

    2016-04-16 21:30:28
    lambda演算简介
  • lambda 演算

    千次阅读 2006-12-03 12:00:00
    λ演算维库,知识与思想的自由文库 Jump to: navigation, search页面分类(2): 计算理论 | 递归论λ演算是一套用于...它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世纪三十年代引入,Church 运用 lambda 演算

     

    λ演算

    维库,知识与思想的自由文库

     
    Jump to: navigation, search

    λ演算是一套用于研究函数定义、函数应用和递归形式系统。它由 Alonzo ChurchStephen Cole Kleene 在 20 世纪三十年代引入,Church 运用 lambda 演算在 1936 年给出 判定性问题 (Entscheidungsproblem) 的一个否定的答案。这种演算可以用来清晰地定义什么是一个可计算函数。关于两个 lambda 演算表达式是否等价的命题无法通过一个通用的算法来解决,这是不可判定性能够证明的头一个问题,甚至还在停机问题之先。Lambda 演算对函数式编程有巨大的影响,特别是Lisp 语言

    Lambda 演算可以被称为最小的通用程序设计语言。它包括一条变换规则 (变量替换) 和一条函数定义方式,Lambda 演算之通用在于,任何一个可计算函数都能用这种形式来表达和求值。因而,它是等价于图灵机的。尽管如此,Lambda 演算强调的是变换规则的运用,而非实现它们的具体机器。可以认为这是一种更接近软件而非硬件的方式。

    本文讨论的是 Church 的“无类型 lambda 演算”,此后,一些有类型 lambda 演算已经被研究出来。

    目录

    [隐藏]
    <script type="text/javascript"> if (window.showTocToggle) { var tocShowText = "显示"; var tocHideText = "隐藏"; showTocToggle(); } </script>

    历史

    最开始,Church 试图创制一套完整的形式系统作为数学的基础,当他发现这个系统易受罗素悖论的影响时,就把 lambda 演算单独分离出来,用于研究可计算性,最终导致了他对判定性问题的否定回答。

    非形式化的描述

    在 lambda 演算中,每个表达式都代表一个只有单独参数的函数,这个函数的参数本身也是一个只有单一参数的函数,同时,函数的值是又一个只有单一参数的函数。函数是通过 lambda 表达式匿名地定义的,这个表达式说明了此函数将对其参数进行什么操作。例如,“加 2”函数 f(x) = x + 2 可以用 lambda 演算表示为 λ x. x + 2 (λ y. y + 2 也是一样的,参数的取名无关紧要) 而 f(3) 的值可以写作 (λ x. x + 2) 3。函数的作用 (application) 是左结合的:f x y = (f x) y。考虑这么一个函数:它把一个函数作为参数,这个函数将被作用在 3 上:λ f. f 3。如果把这个 (用函数作参数的) 函数作用于我们先前的“加 2”函数上:(λ f. f 3) (λ x. x+2),则明显地,下述三个表达式:

    f. f 3) (λ x. x+2)   与    (λ x. x + 2) 3    与    3 + 2

    是等价的。有两个参数的函数可以通过 lambda 演算这么表达:一个单一参数的函数的返回值又是一个单一参数的函数 (参见 Currying)。例如,函数 f(x, y) = x - y 可以写作 λ x. λ y. x - y。下述三个表达式:

    x. λ y. x - y) 7 2    与    (λ y. 7 - y) 2    与    7 - 2

    也是等价的。然而这种 lambda 表达式之间的等价性无法找到一个通用的函数来判定。

    并非所有的 lambda 表达式都可以规约至上述那样的确定值,考虑

    x. x x) (λ x. x x)

    x. x x x) (λ x. x x x)

    然后试图把第一个函数作用在它的参数上。 (λ x. x x) 被称为 ω 组合子,((λ x. x x) (λ x. x x)) 被称为 Ω,而 ((λ x. x x x) (λ x. x x x)) 被称为 Ω2,以此类推。

    若仅形式化函数作用的概念而不允许 lambda 表达式,就得到了组合子逻辑

    形式化定义

    形式化地,我们从一个标识符 (identifier) 的可数无穷集合开始,比如 {a, b, c, ..., x, y, z, x1, x2, ...},则所有的 lambda 表达式可以通过下述以 BNF 范式表达的上下文无关文法描述:

    1. <expr> ::= <identifier>
    2. <expr> ::= (λ <identifier> . <expr>)
    3. <expr> ::= (<expr> <expr>)

    头两条规则用来生成函数,而第三条描述了函数是如何作用在参数上的。通常,lambda 抽象 (规则 2) 和函数作用 (规则 3) 中的括号在不会产生歧义的情况下可以省略。如下假定保证了不会产生歧义:(1) 函数的作用是左结合的,和 (2) lambda 操作符被绑定到它后面的整个表达式。例如,表达式 ((λ x. (x x)) (λ y. y)) 可以简写成 (λ x. x x) λ y.y

    类似 λ x. (x y) 这样的 lambda 表达式并未定义一个函数,因为变量 y 的出现是自由的,即它并没有被绑定到表达式中的任何一个 λ 上。变量出现次数的绑定是通过下述规则 (基于 lambda 表达式的结构归纳地) 定义的:

    1. 在表达式 V 中,V 是变量,则这个表达式里变量 V 只有一次自由出现。
    2. 在表达式 λ V . E 中 (V 是变量,E 是另一个表达式),变量自由出现的次数是 E 中变量自由出现的次数,减去 EV 自由出现的次数。因而,E 中那些 V 被称为绑定在 λ 上。
    3. 在表达式 (E E' ) 中,变量自由出现的次数是 EE' 中变量自由出现次数之和。

    在 lambda 表达式的集合上定义了一个等价关系 (在此用 == 标注),“两个表达式其实表示的是同一个函数”这样的直觉性判断即由此表述,这种等价关系是通过所谓的“alpha-变换规则”和“beta-归约规则”。


    α-变换

    Alpha-变换规则表达的是,被绑定变量的名称是不重要的。比如说 λx.x 和 λy.y 是同一个函数。尽管如此,这条规则并非像它看起来这么简单,关于被绑定的变量能否由另一个替换有一系列的限制。

    Alpha-变换规则陈述的是,若 VW 均为变量,E 是一个 lambda 表达式,同时 E[V/W] 是指把表达式 E 中的所有的 V 的自由出现都替换为 W,那么在 W 不是 E 中的一个自由出现,且如果 W 替换了 VW 不会被 E 中的 λ 绑定的情况下,有

    λ V. E == λ W. E[V/W]

    这条规则告诉我们,例如 λ x. (λ x. x) x 这样的表达式和 λ y. (λ x. x) y 是一样的。

    β-归约

    Beta-归约规则表达的是函数作用的概念。它陈述了若所有的 E' 的自由出现在 E [V/E' ] 中仍然是自由的情况下,有

    ((λ V. E ) E' ) == E [V/E' ]

    成立。

    == 关系被定义为满足上述两条规则的最小等价关系 (即在这个等价关系中减去任何一个映射,它将不再是一个等价关系)。

    对上述等价关系的一个更具操作性的定义可以这样获得:只允许从左至右来应用规则。不允许任何 beta 归约的 lambda 表达式被称为范式。并非所有的 lambda 表达式都存在与之等价的范式,若存在,则对于相同的形式参数命名而言是唯一的。此外,有一个算法用户计算范式,不断地把最左边的形式参数替换为实际参数,直到无法再作任何可能的规约为止。这个算法当且仅当 lambda 表达式存在一个范式时才会停止。Church-Rosser 定理 说明了,当且仅当两个表达式等价时,它们会在形式参数换名后得到同一个范式。

    η-变换

    前两条规则之后,还可以加入第三条规则,eta-变换,来形成一个新的等价关系。Eta-变换表达的是外延性的概念,在这里外延性指的是,两个函数对于所有的参数得到的结果都一致,当且仅当它们是同一个函数。Eta-变换可以令 λ x . f xf 相互转换,只要 x 不是 f 中的自由出现。下面说明了为何这条规则和外延性是等价的:

    fg 外延地等价,即,f a == g a 对所有的 lambda 表达式 a 成立,则当取 a 为在 f 中不是自由出现的变量 x 时,我们有 f x == g x,因此 λ x . f x == λ x . g x,由 eta-变换 f == g。所以只要 eta-变换是有效的,会得到外延性也是有效的。

    相反地,若外延性是有效的,则由 beta-归约,对所有的 y 有 (λ x . f x) y == f y,可得 λ x . f x == f,即 eta-变换也是有效的。

    lambda 演算中的运算

    在 lambda 演算中有许多方式都可以定义自然数,但最常见的还是邱奇数,下面是它们的定义:

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

    以此类推。直观地说,lambda 演算中的数字 n 就是一个把函数 f 作为参数并以 fn 次幂为返回值的函数。换句话说,Church 整数是一个高阶函数 -- 以单一参数函数 f 为参数,返回另一个单一参数的函数。

    (注意在 Church 原来的 lambda 演算中,lambda 表达式的形式参数在函数体中至少出现一次,这使得我们无法像上面那样定义 0) 在 Church 整数定义的基础上,我们可以定义一个后继函数,它以 n 为参数,返回 n + 1:

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

    加法是这样定义的:

    PLUS = λ m. λ n. λ f. λ x. m f (n f x)

    PLUS 可以被看作以两个自然数为参数的函数,它返回的也是一个自然数。你可以试试验证

    PLUS 2 3    与    5

    是否等价。乘法可以这样定义:

    MULT = λ m. λ n. m (PLUS n) 0,

    m 乘以 n 等于在零的基础上 n 次加 m。另一种方式是

    MULT = λ m. λ n. λ f. m (n f)

    正整数 n 的前驱元 (predecessesor) PRED n = n - 1 要复杂一些:

    PRED = λ n. λ f. λ x. ng. λ h. h (g f)) (λ u. x) (λ u. u)

    或者

    PRED = λ n. ng. λ k. (g 1) (λ u. PLUS (g k) 1) k) (λ l. 0) 0

    注意 (g 1) (λ u. PLUS (g k) 1) k 表示的是,当 g(1) 是零时,表达式的值是 k,否则是 g(k) + 1。

    逻辑与断言

    习惯上,下述两个定义 (称为 Church 布尔值) 被用作 TRUE 和 FALSE 这样的布尔值:

    TRUE = λ u. λ v. u
    FALSE = λ u. λ v. v

    断言是指返回布尔值的函数。最基本的一个断言 ISZERO,当且仅当其参数为零时返回真:

    ISZERO = λ n. nx. FALSE) TRUE

    断言的运用与上述 TRUE 和 FALSE 的定义,使得 "if-then-else" 这类语句很容易用 lambda 演算写出。

    递归

    递归是一种以函数自身迭代自身变元的算法,一般是通过函数自身来定义函数的方式实现。表面看来 lambda 演算不允许递归,其实这是一种对递归的误解。考虑阶乘函数 f(n) 一般这样递归地定义:

    f(n) = 1, 若 n = 0; n·f(n-1), 若 n>0.

    λ语言:

    FACT = λ n. nu. MULT n (FACT (PRED n))) 1

    用 Y-组合子 在 λ语言 中合法地定义:

    FACT = Y (λ g. λ n. nu. MULT n (g (PRED n))) 1)
    Y = λ f. ((λ x. f (x x)) (λ x. f (x x)))

    参见

    外部链接

     
     
    展开全文
  • lambda演算学习

    2019-03-14 23:13:21
    λ演算的学习资料,英文版,可计算函数和lambda演算规则
  • lambda演算解释器 什么: 用C ++编写的小型lambda演算解释器。 它支持α转换和β减少,以及精确跟踪替换和重命名的输出。 如何: 支持标准的lambda演算语法,例如: (λz.(((λx.(λy.x)) z) ((λx.(λy.x)) z)))...
  • T2 计算理论 第六章 Lambda演算模型 主要内容 纯Lambda演算理论 纯Lambda演算实例 纯Lambda演算的扩展 2.4 Lambda演算理论 Lambda演算形式系统主要有两部分 表达式的形式系统 变换规则的形式系统 2.4 Lambda演算...
  • Lambda 演算

    千次阅读 2009-09-22 20:02:00
    Lambda 表达式是“Lambda-Calculus”,即 “Λ-演算”的关键概念。由 Λ-演算发展出的理论,成为计算机科学与技术诞生和发展的基础。Λ-演算之概念、定义、公理、命题定义一:Λ-项集建立在一个无限变量集 V
  • lambda演算和图灵机

    2019-11-08 14:35:59
    λ演算(lambda calculus)是一套用于研究函数定义、函数应用和递归的形式系统。它由阿隆佐·邱奇和他的学生斯蒂芬·科尔·克莱尼...“代入”就是用lambda演算中的β-归约概念。而“替换”就是lambda演算中的α-变换。
  • lambda演算资料集合

    2015-10-14 18:50:49
    个人收集的一些关于lambda演算的国内外资料和课件,请笑纳
  • 最近在学习lambda演算的相关内容,由于资料不全,学习的过程很是痛苦,下面这篇文章主要给大家介绍了关于如何利用Ruby简单模拟Lambda演算的相关资料,需要的朋友可以参考借鉴,下面来随着小编一起学习学习吧。
  • lambda演算解释器 这是lambda演算解释器lc的代码。 lc会按正常顺序(从最左到最先)减少beta和eta。 lc将重命名绑定变量以防止捕获变量。 建筑 我没有做GNU风格的autoconf脚本。 我确实编写了相当严格的ANSI C(我...
  • Lambda演算Lambda演算是一种非常小的编程语言,由Alonzo Church于1936年发明。 它的功能等效于PHP中的Turing Machine lambda-php Lambda演算解释器。 Lambda演算Lambda演算是一种非常小的编程语言,由Alonzo Church...
  • 拉姆达.js JavaScript 中的 Lambda 演算 安装 用法
  • lambda演算系统

    2014-08-01 15:47:11
    详细演示lambda演算过程,最后给出Y组合字实现匿名递归
  • Scala 中的类型级 lambda 演算 此存储库演示了 Scala 类型中 lambda 演算的实现。 无类型 lambda 演算 import lambda . _ case class Equals [ A > : B < : B , B ]() // this checks type equality type S = x ...
  • malc-制作Lambda演算 关于 Malc是用于以任何支持编程语言实现无类型的指南和规范。 λ演算有时被称为世界上最小的编程语言。 它是一个完全由功能和功能应用组成的符号。 甚至“原始值”也表示为组合器,即没有全局...

空空如也

空空如也

1 2 3 4 5 ... 20
收藏数 3,327
精华内容 1,330
关键字:

lambda演算