可计算性理论模型初识(一):巴斯克范式(BNF)与λ演算

  • A+
所属分类:RChain知识库

Greg Meredith近期在Youtube上教授一门课程Introduction to the Designof Computational Calculi (DoCC) ,每周更新。主要为了让RChain爱好者们理解可计算理论及其包含的演算模型,详解rho演算是如何应用在RChain项目中并教授大家如何基于该演算模型设计RChain相关应用。

由于该课程技术性很强,其理念过于深奥且难以理解。因此本系列文章即是想以一种通俗易懂的方式来帮助大家理解课程中的一些基本概念。行文也会尽可能的保持严谨并遵循课程中想要传递的核心信息。

前几篇文章将作为DoCC课程所需的一些背景材料。首先会介绍可计算性理论的一些基础知识,比如λ演算、π演算以及作为RChain理论基础的ρ演算的语法语义等内容;在此基础上,后续也会每周更新文章来帮助我们更深入的理解DoCC课程。

首先,我们需要理解巴斯克范式及λ演算,这里我们先来讨论基本语法及操作语义。

巴斯克范式(BNF, Baukus-Naur form)

按照编程语言世界的经典规范,我们将要讨论的各类演算的语法语义都以巴斯克范式呈现。巴斯克范式可以用一种精简且准确的方式描述演算的语法规则(这里有点类似我们算法笔试中所用到的伪码,但是BNF描述的更加规范准确且没有歧义,被计算机科学界广泛接受并使用)。这里我们通过λ演算作为例子,来具体看下BNF是什么。

λ演算

语法

λ演算是一种通用的计算模型,由数学家AlonzoChurch在20世纪30年代提出。 用BNF描述λ演算的语法表示如下:

M,N ::= λx.M |(M N)  (1.1)

我们暂时不需要知道这个公式是什么意思,只需要了解这是三种不同基本形式的λ项(terms),对应了构造λ项的三种不同的规则。即M, N λ项可以由x或λx.M 或(M N) 形式组成。这些λ项是可递归构建的,因此在语言中我们可以使用相当复杂的λ项,也可以使用这些λ项在语言中做出各种合理的组合。

这可以类比为一个游戏,该游戏中,有三个规则用于描述如果构建λ项,并且有个盒子可以抽名字出来。每轮,首先给定一个λ项M,然后做如下选择:(1)从帽子中抽出名字x;(2)抽出一个名字x并组合成一个λ抽象λx.M; (3)选择另一个λ项N并组成一个应用(MN)。 规则就是这样,之后就可以通过多次重复该游戏来组成不同的λ项。(比如第一次选择(2)第二次选择(3),第一次选择后得到λ项λx.M,第二次选择后得到λ项(λx.M N))

我们可以从集合X中选择一个变量x,作为我们第一个λ项x。之后就可以构造其他的λ项了,比如λx.x 及(x x)。还有什么其他的λ项可以构造么?

这里我们先回到BNF表达式(1.1),可以看到等号右面的变量x来自于一个变量集合X,而游戏规则是我们只从集合X中取变量,集合X中的内容是我们可以控制的,并且改变集合X会改变我们语言中的表达式的合规性。因此我们可以称这个语法在变量X中是参数化的。所以有些人会把这个λ演算的BNF表达式写的有点奇怪,用X集合来显示的放入表达式中:

M[X]::= λX.M[X] | (M[XM[X])

用于强调λ项M[X]对X的依赖性。本段文字有点跑题,主要是想要强调λ项对给定变量的依赖性。

另一个在(1.1)中值得注意的内等容是几个M和N出现在BNF表达式的两侧。这意味着如果我们有两个λ项M和N,我们有一些选项可以递归创建新的λ项:

  • x(变量;从集合X中选择一个变量,诚然这与M和N没什么关系,变量本身也是个λ项)
  • λx.M(抽象;将变量x绑定在M中,即在M中声明x变量,抽象也是λ项)
  • (M N)(应用;将 λ项M“应用”到λ项N,应用同样也是λ项)

基本上λ演算就是上面这样了。我们总是可以从一些符合规范的λ项组成另一些符合规范的λ项。我们来看几个例子:

1.λx.λy.x是符合规范的λ项(这是一个重要的例子,因为它是λ演算中布尔函数True的编码)

证明:x是符合规范⇒M=λy.x符合规范⇒λx.M=λx.λy.x符合规范

2. (λx.xy)是符合规范的λ项(这也是一个重要的例子,因为λx.x充当λ演算中的恒等函数)

证明:λx.x符合规范⇒(λx.xy)符合规范(将λx.x应用于y)

3.  xλx。是不正确的语法⇒不是一个可接受的λ项

以上就是我们需要知道的关于构造λ项的所有知识了。但是,这并没有告诉我们这些λ项是如何相互作用的。为此,我们还需要讨论下操作语义。

 

操作语义

λ演算可以映射为函数的概念:抽象(λx.M)从一个函数中选择变量,应用(M N)用函数来评估变量。这个思想指导了这些结构间的相互作用,称之为操作语义。在λ演算中主要有两种关系,α-变换和β-规约:

  • α-变换

λx.M{x}→ λy.M{y}

该规则认为,只是“绑定变量”名称不同的两个λ项的可以认为是“结构上等同”的。“结构上等同”的意思是这些λ项从计算的角度上看是没有区别的。“绑定变量”的指的是表达式λx.M{x}中的x。变量x出现在λ项M中(被写为M{x})并且λ在这个表达式中绑定x,即λ在M中声明变量x。另一种等价的解释方式是函数f可以将x作为变量,写作f(x),或者它可以用y作为变量,写作f(y),不管我们用哪个变量名,这个函数表达的含义相同。这就是α转换的本质。也即告诉我们λx.M和λy.M{y / x}是等价项(译者注:这里λy.M{y / x}的意思应该是α-变换的一个约束,即y的变化不能超过x变量的取值范围,该变换才能成立)。

  • β-规约

(λx.MN)→M {N / x}

β规约主要表达函数的应用。(λx.MN)中,前半部分是λ抽象λx.M,后面的N用于替代λx.M中的x,也即λx.M应用于N。这即是一个简单的函数评估:在函数M中声明变量x并用其评估N,即用N代替x。这也可以被认为是功能组合,如果我们将函数f(x)应用于g(y),我们可以得到函数f(g(y))。这与替换x=g(y)效果完全相同。

 

下面举一些便于理解操作语义的例子:

1,λx.(x z)→λy.(y z)

设M {x} =(xz)和M {y} =(yz),所以我们直接α-转换得到λx.(xz)=λx.M{x}→λy.M{y}=λy.(yz)。 即使在λx.(x y)中存在抽象和应用,它也不是β规约。请思考为什么?(对比上文β规约内容显然)

2,(λx.(x x)y)→(y y)

这是一个β规约,因为我们将抽象λx.(x x)应用于项y。设M {x} =(x x), 代入M{x}后通过β规约有(λx.(x x)y)=(λx.My)→M {y / x} =(x x){y / x} =(y y)。

3,(λx.(λy.(x y)u)v)→(v u)

这里有两轮β规约。 第一轮,让M {x} =(λy.(x y)u)。 然后(λx.(λy.(xy)u)v)=(λx.Mv)→M {v / x} =(λy.(xy)u){v / x} =(λy.(vy)u)。 最后我们对剩余的表达式使用直接的β规约得到(λy.(v y)u)→(v u)。

综上,我们简单介绍了λ演算的语法及两个主要的操作语义。如果您之前没有了解过该内容,初识可能会觉得该部分内容有些难以理解。本文中也确实没有告诉我们λ演算是如何与算术是相关联的,但是该系列后面的文章会很快触达具体的内容。我们一步一步来。

 

译者:由于现代计算机编程语言基本上完全按照λ演算的规则来实现,若有编程经验的同学应该很容易看出来λ演算与编程语言语法中函数的关联性。这里就个人理解做一个简单的总结性类比:

  • x:变量声明,int x
  • λx.M:函数声明, def M(x)
  • (M N):M(x)和N(y)都是函数,表示M(N(y)), 要求N(y)的结果与变量x声明的类型一致或取值范围一致,此例子中为int型。

语义:

α-变换: 函数的内容一致时,修改函数变量名函数的功能是没区别的,f(x)与f(y)等价,α-变换避免了不同函数中变量名称冲突的问题

β-规约:两个函数f(x)和g(y),当x= g(y)时候,可以表示为f(g(y))

*补充,η-变换:如果两个函数在变量相同时总有f(x)===g(x),则f=g

 

参考资料

[1] Computational Calculi Primer Part 1:Lambda calculus & BNF (https://blog.rchain.coop/computational-calculi-primer/)

[2] Wikipedia-Lambda calculus (https://en.wikipedia.org/wiki/Lambda_calculus)

 

本文由微信公众号:Rchain中文社区 翻译

查看原文

  • 作者微信
  • weinxin
  • 微信公众号
  • weinxin
avatar

发表评论

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: