形式语义学之连续函数

形式语义学FormalSemanticsofProgrammingLanguages2011.09内容回顾关于论域完全半序集半序集=集合+半序关系最小元任何一个递增链都有最小上届一个集合可以扩展为平坦集(最小元+平坦关系)；平坦集一定是完全半序集；任何一个集合一定可以扩展成完全半序集；论域是完全半序集论域构造：论域表达式原始论域论域构造符：，+，*，2020/2/132第二章函数式抽象描述方法2.1论域理论基础(DomainTheory)2.1.0集合的基本概念2.1.1完全半序集(completepartialorderset,CPO)2.1.2连续函数(continuousfunctions)2.1.3最小不动点(leastfixedpoint)2020/2/1332.1.2连续函数主要内容相关概念部分函数(partialfunction)全函数(totalfunction)自然开拓函数单调函数(monotonicfunction)严格函数(strictfunction)连续函数(continuousfunction)相关性质2020/2/134相关概念部分函数：设f是D1到D2的函数，如果存在dD1使得f(d)没有定义，则称f为部分函数；全函数：设f是D1到D2的函数，如果对于任意dD1都存在d’D2使得f(d)=d’，则称f为全函数；2020/2/135相关概念自然开拓函数：设fD1……DnD,且当(d1,……,dn)中有一个di是i时，f(d1,……,dn)=，则称f为自然开拓函数。部分函数开拓成全函数的方法：设有部分函数f[D1D2]；分别扩充D1和D2为D1和D2；扩充函数f为f’，使得2，当d1=1f’(d1)=2，当f(d1)无定义f(d1)，其他2020/2/136相关概念单调函数：设全函数f[D1D2]，且D1和D2是半序集。对于任意x,yD1，如果x≼1y则有f(x)≼2f(y)，那么称f是单调函数.严格函数：设全函数f[D1D2]，D1和D2是半序集，且分别有最小元1和2。如果f满足条件f(1)=2，则称f为严格函数。2020/2/137相关概念连续函数：设全函数f[D1D2]，且D1和D2是完全半序集。如果f满足如下条件则称f为连续函数：if(Xi)=f(iXi)2020/2/138连续函数的应用描述程序语义时，要求连续函数(部分函数全函数连续函数)域都是完全半序集解决递归的问题：最小不动点连续函数必有最小不动点，而且唯一；对连续函数有求最小不动点的方法；2020/2/1392020/2/1310一些经常用到的函数常函数：f[D1D2]满足xD1都有f(x)=c，其中c是D2中的一个固定常数。恒等函数：f[DD]满足xD都有f(x)=x。复合函数：设f[D1D2]，g[D2D3]，则称h是f和g的复合函数，记作gf，其中h[D1D3]，而且xD1都有h(x)=g(f(x))。2020/2/1311一些经常用到的函数条件函数(算子)：设b[DBOOL]，f1,f2[DM]，则条件函数cond定义如下：cond[DM]，而且xD都有f1(x)，如果b(x)=tt；cond(x)=f2(x)，如果b(x)=ff；，如果b(x)=；2020/2/1312一些经常用到的函数联合函数：设fiDDi(1≤i≤m)，则联合函数f(简记为[f1,…,fm])定义如下：fDD1…Dm，而且xD都有f(x)=(f1(x),…,fm(x))。更新函数：设f[D1D2]，且aD1,bD2,则更新函数f’定义如下：f’[D1D2],而且对于任意xD1如果x=a则f’(x)=b,否则f’(x)=f(x)，更新函数简记为f[b/a]。2020/2/1313一些经常用到的函数Curry函数(算子)：设f[D1D2D]，xD1，yD2curry[D1D2D][D1D2D]curryfxy=f(x,y)，curryfx是一个D2D上的函数，xD1curryf是一个D1D2D上的函数2020/2/1314Curry算子的解释Curry算子，分解定义域，使其升级为高阶函数；例子函数f的定义:f(x,y)=x+y函数f的函数空间:(INTINTINT)Curry:(INTINTINT)(INTINTINT)Curryfxy:f(x,y),Curryf12=f(1,2)=1+2=3Curryfx:INTINT,Curryf1=f(1,y)=1+yCurryf:INTINTINT,Curryf=f(x,y)=x+y令g=Curryf，对于任意xINT,g(x)的函数空间为INTINT，g={1{12,23,……},2{13,24,……},……}即g(1)={12,23,……},….2020/2/1315相关性质连续函数必是单调函数(反之未必)；平坦集上的严格函数是单调函数；常函数是单调函数；恒等函数是单调函数；自然开拓函数是单调函数；单调函数的复合函数还是单调函数；证明略。2020/2/1316相关性质平坦集上的严格函数是连续函数；常函数是连续函数；恒等函数是连续函数；自然开拓函数是连续函数；连续函数的复合函数还是连续函数；连续函数的联合函数还是连续函数；连续函数的更新函数还是连续函数；连续函数的条件函数还是连续函数；Curry算子相关函数还是连续函数；2020/2/1317重要结论任何集合可以扩展成平坦集；任何集合可以扩展成完全半序集；任何集合可以扩展成论域；定义在平坦集上的严格函数是连续函数；常用的函数都可以开拓成连续函数；用连续函数定义的程序语义是有解的（最小不动点；第二章函数式抽象描述方法2.1论域理论基础(DomainTheory)2.1.0集合的基本概念2.1.1完全半序集(completepartialorderset,CPO)2.1.2连续函数(continuousfunctions)2.1.3最小不动点(leastfixedpoint)2020/2/13182.1.3最小不动点相关概念不动点最小不动点最小不动点的性质最小不动点的例子2020/2/13192.1.3最小不动点问题的提出递归定义X=F(X)，包括函数、类型和程序确定解的方法：计算规则过程式程序设计语言采用这种方式；不同的计算规则得到的未必相同；最小不动点确定而且唯一；存在一个简明的最小不动点计算规则；存在证明最小不动点性质的强有力的方法；2020/2/1320相关概念不动点：设f[DD]，且dD，如果有f(d)=d，则称d为f的不动点。最小不动点：设f[DD]，且f有不动点，则称f的所有不动点中的最小者为最小不动点，记作f。说明：要求函数的定义域和值域相同；一个函数不一定都有不动点；一个函数可能有多个不动点，但是不一定有最小不动点；2020/2/13212020/2/1322不动点和最小不动点例子没有不动点情形：函数fINTINT,f(x)=x+1；多个不动点，但没有最小不动点D={{},{a},{b}},函数gDD,g(x)=(x={}{a},x)；不动点：{a},{b}没有最小不动点：因为{a}和{b}之间没有关系；2020/2/1323不动点和最小不动点例子多个不动点，最小不动点D={{},{a},{b}},函数gDD,g(x)=x；不动点：{},{a},{b}最小不动点：{}2020/2/1324最小不动点的性质最小不动点的唯一性：设f[DD]，如果f有最小不动点，则必唯一。如果a和b都是最小不动点a≼b,b≼aa=b最小不动点的存在性：若f[DD]是连续函数，则f有最小不动点，且有f=fi()，其中fi+1()=f(fi()),f0()=。连续函数必有最小不动点；最小不动点的计算方法；-25-证明f=fi()的存在性1.证明序列{fi()}是D上的链：函数f的单调性有≼f()f()≼f2()fi()≼fi+1()2.证明fi()是f的不动点：函数f的连续性有f(fi())=f(fi())=fi+1()=fi()3.证明fi()是f的最小不动点:假设d是函数f的任一不动点即f(d)=d函数f的单调性和d不动点性有f0()≼f0(d)=df1()≼f1(d)=dfi+1()=f(fi())≼f(d)=d2020/2/1326最小不动点的计算方法对于一个连续函数f[DD];是D的最小元；x1=f(),x2=f(x1),……直到存在n,xn=f(xn),最后确定f=xn，即xn就是最小不动点2020/2/1327最小不动点例子最小不动点的简单例子函数F：DD，D=pow{a，b，c}，Fx=x{a，b}函数F有两个不动点：{a，b}和{a，b，c}F{a，b}={a，b}{a，b}={a，b}F{a，b，c}={a，b}{a，b，c}={a，b，c}最小不动点：{a，b}D的最小元D={};FD={}{a，b}={a，b}F{a，b}={a，b}{a，b}={a，b}，收敛{a,b}就是最小不动点；-28-最小不动点-复杂例子1设有如下的类型声明：typedefx=INT;typedefy=x;typedefz=y;该类型声明建立了如下的类型环境：(TEnv:IDTYPE):[x|-INT,y|-(x),z|-(y)]形成一个递归函数：:TEnvTEnv即有递归方程()=下面求解该函数的最小不动点：()1.首先求出函数定义域的最小元，即类型环境TEnv的最小元，=[xT,yT,zT],T是TYPE上的最小元；2.然后开始迭代：0()=={xT,yT,zT}=01()=(0())=(0)={xINT,yT,zT}=12()=(1())=(1)={xINT,yINT,zT}=23()=(2())=(2)={xINT,yINT,zINT}=34()=(3())=(3)=33是最小不动点-29-最小不动点-复杂例子2设有如下的类型声明：typedefx=y;typedefy=z;typedefz=INT;该类型声明建立了如下的类型环境：(TEnv:IDTYPE):[x|-(y),y|-(z),z|-INT]形成一个递归函数：:TEnvTEnv即有递归方程()=下面求解该函数的最小不动点：()1.首先求出函数定义域的最小元，即类型环境TEnv的最小元，=[xT,yT,zT],T是TYPE上的最小元；2.然后开始迭代：0()=={xT,yT,zT}=01()=(0())=(0)={xT,yT,zINT}=12()=(1())=(1)={xT,yINT,zINT}=23()=(2())=(2)={xINT,yINT,zINT}=34()=(3())=(3)=33是最小不动点2020/2/13302.1小结目的：为语义形式化提供一个理论基础平台；任何一个集合可以扩展为平坦集；平坦集一定是完全半序集；论域表达式定义