形式语义学之连续函数.ppt

《形式语义学之连续函数.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、形式语义学FormalSemanticsofProgrammingLanguages2011.09内容回顾关于论域完全半序集半序集=集合+半序关系最小元任何一个递增链都有最小上届一个集合可以扩展为平坦集(最小元+平坦关系)；平坦集一定是完全半序集；任何一个集合一定可以扩展成完全半序集；论域是完全半序集论域构造：论域表达式原始论域论域构造符：，+，*，2021/7/312第二章函数式抽象描述方法2.1论域理论基础(DomainTheory)2.1.0集合的基本概念2.1.1完全半序集(completepartialo

2、rderset,CPO)2.1.2连续函数(continuousfunctions)2.1.3最小不动点(leastfixedpoint)2021/7/3132.1.2连续函数主要内容相关概念部分函数(partialfunction)全函数(totalfunction)自然开拓函数单调函数(monotonicfunction)严格函数(strictfunction)连续函数(continuousfunction)相关性质2021/7/314相关概念部分函数：设f是D1到D2的函数，如果存在dD1使得f(d)没有定

3、义，则称f为部分函数；全函数：设f是D1到D2的函数，如果对于任意dD1都存在d’D2使得f(d)=d’，则称f为全函数；2021/7/315相关概念自然开拓函数：设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)，其他2021/7/316相关概念单调函数：

4、设全函数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为严格函数。2021/7/317相关概念连续函数：设全函数f[D1D2]，且D1和D2是完全半序集。如果f满足如下条件则称f为连续函数：if(Xi)=f(iXi)2021/7/318连续函数的应用描述程序语义时，要求连续函数(部分函数全函数连续函数)域都是完全半序

5、集解决递归的问题：最小不动点连续函数必有最小不动点，而且唯一；对连续函数有求最小不动点的方法；2021/7/319一些经常用到的函数常函数：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))。2021/7/3110一些经常用到的函数条件函数(算子)：设b[DBOOL]，f1,

6、f2[DM]，则条件函数cond定义如下：cond[DM]，而且xD都有f1(x)，如果b(x)=tt；cond(x)=f2(x)，如果b(x)=ff；，如果b(x)=；2021/7/3111一些经常用到的函数联合函数：设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

7、D1如果x=a则f’(x)=b,否则f’(x)=f(x)，更新函数简记为f[b/a]。2021/7/3112一些经常用到的函数Curry函数(算子)：设f[D1D2D]，xD1，yD2curry[D1D2D][D1D2D]curryfxy=f(x,y)，curryfx是一个D2D上的函数，xD1curryf是一个D1D2D上的函数2021/7/3113Curry算子的解释Curry算子，分解定义域，使其升级为高阶函数；例子函数f的定义:f(x,y)=x+y函数f的函数空间:(INTIN

8、TINT)Curry:(INTINTINT)(INTINTINT)Curryfxy:f(x,y),Curryf12=f(1,2)=1+2=3Curryfx:INTINT,Curryf1=f(1,y)=1+yCurryf:INTINTINT,Curryf=f(x,y)=x+y令g=Curryf，对于任意xINT,