新型计算模型和顺序交互的数学计算机科学导论第九讲市公开课一等奖百校联赛特等奖课件.pptx

新型计算模型和新型计算模型和次序次序交互数学交互数学计算机科学导论第九讲计算机科学导论第九讲计算机科学技术学院计算机科学技术学院陈意云陈意云0551-63607043,http:/ 程程 内内 容容课程内容课程内容围绕学科理论体系中模型理论围绕学科理论体系中模型理论,程序理论和计算理论程序理论和计算理论1.模型理论关心问题模型理论关心问题 给定模型给定模型M，哪些问题能够由模型，哪些问题能够由模型M处理处理；怎样；怎样比较模型表示能力比较模型表示能力2.程序理论关心问题程序理论关心问题给定模型给定模型M，怎样用模型，怎样用模型M处理问题处理问题包含程序设计范型、程序设计语言、程序设计、包含程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等形式语义、类型论、程序验证、程序分析等3.计算理论关心问题计算理论关心问题给定模型给定模型M和一类问题和一类问题,处理该类问题需多少资源处理该类问题需多少资源2本讲座概要介绍交互计算特本讲座概要介绍交互计算特点及相关一些数学知识点及相关一些数学知识第2页讲讲 座座 提提 纲纲基本知识基本知识人人 机机 物三元世界、云计算、未来网、物联网、物三元世界、云计算、未来网、物联网、泛在网、图灵机计算模型、网域计算模型泛在网、图灵机计算模型、网域计算模型交互计算交互计算经典计算与交互计算经典计算与交互计算、交互特点交互特点、交互机器模型、交互机器模型、能描述交互演算能描述交互演算从归纳到余归纳从归纳到余归纳良基集、非良基集、余归纳、互模拟良基集、非良基集、余归纳、互模拟从代数到余代数从代数到余代数笛卡尔积笛卡尔积,可区分并可区分并,余代数余代数,代数和余代数区分代数和余代数区分3第3页人人 机机 物三元世界物三元世界由由计计算算机机网网络络世世界界(也也称称计计算算世世界界,cyber world)、物物理理世世界界和和人人类类社社会会组组成成人人机机物物协协同同社社会会，是是多多人人、多多机机和和多多物物组组成成动动态态开开放放并并协协同同工工作作网网络络社社会会计计算算机机科科学学是是研研究究人人机机物物三三元元世世界界中中计计算算现现象象这这个共同根本科学个共同根本科学站站在在三三元元世世界界高高度度，有有利利于于了了解解云云计计算算、未未来来网网、物联网、泛在网物联网、泛在网(ubiquitous network)新技术趋势新技术趋势基基 本本 知知 识识4第4页云计算云计算把把资资源源集集中中于于互互联联网网上上数数据据中中心心，由由这这种种云云中中心心提供给用层、平台层和基础设施层提供给用层、平台层和基础设施层集中服务集中服务强强调调信信息息资资源源聚聚集集、优优化化、动动态态分分配配和和回回收收，经经过过提提升升数数据据中中心心效效率率，处处理理传传统统IT系系统统零零碎碎性性带带来低效率，降低信息化成本、降低能耗来低效率，降低信息化成本、降低能耗向向公公众众提提供供一一个个新新高高效效计计算算模模式式，兼兼有有互互联联网网服服务便利与廉价和大型计算机能力务便利与廉价和大型计算机能力云云计计算算可可为为物物联联网网和和泛泛在在网网提提供供后后端端处处理理能能力力与与应用平台应用平台基基 本本 知知 识识5第5页未来网（未来互联网，未来网（未来互联网，post-IP network）基基于于TCP/IP协协议议互互联联网网伴伴随随其其广广泛泛应应用用，在在可可扩扩展展性性、移移动动性性、安安全全性性、服服务务质质量量和和可可靠靠性性等等方方面都暴露出本质缺点面都暴露出本质缺点近十多年来渐进式改进未能从根本上处理问题近十多年来渐进式改进未能从根本上处理问题美美国国和和欧欧盟盟等等已已开开展展“从从零零开开始始”革革命命方方式式研研究究未来互联网未来互联网未未来来网网可可为为云云计计算算、物物联联网网和和泛泛在在网网提提供供愈愈加加高高效安全效安全网络基础技术网络基础技术基基 本本 知知 识识6第6页物联网物联网实现物物互联网络实现物物互联网络与与互互联联网网区区分分：物物物物互互联联，物物机机互互联联，而而不不是是局局限于机机互联限于机机互联实实现现对对物物理理世世界界（包包含含自自然然界界和和人人造造物物）精精准准感感知知，感感知知信信息息实实时时或或及及时时传传输输，针针对对物物理理世世界界限限制制处处理理与与决决议议，以以及及对对物物理理世世界界控控制制，提提供供高高效效智能应用服务智能应用服务更更高高层层次次：经经过过独独立立个个体体之之间间局局部部即即时时交交互互和和分分布布式式智智能能，使使物物体体含含有有自自组组织织、自自计计算算和和自自反反馈馈功效，实现功效，实现物物之间智能交互物物之间智能交互基基 本本 知知 识识7第7页基基 本本 知知 识识泛在网泛在网是是指指基基于于个个人人和和社社会会需需求求，实实现现人人与与人人、人人与与物物、物物与与物物之之间间按按需需进进行行信信息息获获取取、传传递递、存存放放、认认知、决议和使用等服务知、决议和使用等服务含有超强环境感知、内容感知及智能性含有超强环境感知、内容感知及智能性环境感知环境感知(environment perception)：指系统含有周围环境指系统含有周围环境 参数采集、语义表示、语义查询解析和语义推理能力参数采集、语义表示、语义查询解析和语义推理能力内容感知内容感知(content aware)网络服务：意在更细致地感知网络服务：意在更细致地感知 终端（终端（PC、手机、平板电脑等）、手机、平板电脑等）网络（网络（3G，Wifi等移动网络）等移动网络）业务类型（游戏、视频、电子商务、微博等）业务类型（游戏、视频、电子商务、微博等）不一样需求不一样需求,提供更有针对性处理方案和更有价值服务提供更有针对性处理方案和更有价值服务8第8页基基 本本 知知 识识泛在网泛在网是是指指基基于于个个人人和和社社会会需需求求，实实现现人人与与人人、人人与与物物、物物与与物物之之间间按按需需进进行行信信息息获获取取、传传递递、存存放放、认认知、决议和使用等服务知、决议和使用等服务含有超强环境感知、内容感知及智能性含有超强环境感知、内容感知及智能性经经过过各各种种联联网网智智能能人人机机交交互互设设备备，为为个个人人和和社社会会提供无所不在信息服务和应用提供无所不在信息服务和应用9第9页基基 本本 知知 识识区分性概括区分性概括未未来来网网：强强调调对对当当今今互互联联网网变变革革，是是未未来来信信息息化化网络基础网络基础云云计计算算：一一个个新新应应用用模模式式，强强调调应应用用层层信信息息综综合合处理，可作为物联网后端处理和应用平台处理，可作为物联网后端处理和应用平台物物联联网网：强强调调对对物物感感知知和和物物物物互互联联,方方便便人人类类对对物物理世界感知和控制，是走向泛在网主要一步理世界感知和控制，是走向泛在网主要一步泛泛在在网网：对对未未来来信信息息社社会会综综合合预预见见，是是上上述述这这些些概念集成概念集成10第10页基基 本本 知知 识识图灵机计算模型图灵机计算模型把把物物理理世世界界数数字字化化，建建立立数数学学模模型型，经经过过计计算算和和数数据据处处理理方方法法，对对自自然然界界存存在在规规律律进进行行模模拟拟仿仿真真；计计算算类类应应用用和和数数据据处处理理应应用用都都是是遵遵照照这这么么计计算算模模型型按按照照“输输入入 计计算算 输输出出”过过程程，产产生生全全部部结结果果都都是能够预知是能够预知它它是是一一个个计计算算世世界界（computation world），是是对对人人类类认认知知一一个个数数字字化化。这这个个数数字字世世界界与与人人类类社社会会、物理世界是正交物理世界是正交11第11页基基 本本 知知 识识网域计算模型网域计算模型把信息化扩大到人类社会一个计算模型把信息化扩大到人类社会一个计算模型经经过过移移动动数数据据方方式式，把把人人类类社社会会中中真真实实工工作作与与生生活活搬搬到到计计算算机机网网络络空空间间（cyberspace,简简称称网网域域），即网域能够看成是对人类社会一个映射即网域能够看成是对人类社会一个映射Cyberspace is the national environment in which communication over computer networks occurs.其其基基础础是是经经过过互互联联网网、上上网网本本(netbook)、智智能能手手机和网络设备等伎俩实现人与人之间通信机和网络设备等伎俩实现人与人之间通信比比如如，社社会会计计算算和和舆舆情情分分析析等等都都是是经经过过对对网网域域空空间计算来发觉人类社会规律间计算来发觉人类社会规律12第12页基基 本本 知知 识识网域计算模型网域计算模型网域空间计算与图灵机计算有本质不一样网域空间计算与图灵机计算有本质不一样不存在不存在“停机停机”问题问题算算法法不不是是独独立立,而而是是交交互互算算法法网网络络(a network of interacting algorithms)存存在在涌涌现现现现象象(emergent phenomena)，即即在在混混沌沌网上世界中能产生新知识与智能网上世界中能产生新知识与智能13第13页计算与交互计算与交互经典计算（简称计算）经典计算（简称计算）计计算算主主体体和和它它环环境境之之间间是是一一个个简简单单接接口口，即即按按照照“输入输入 计算计算 输出输出”过程完成所要求任务过程完成所要求任务计算表达出从输入到输出函数性计算表达出从输入到输出函数性交互计算（简称交互）交互计算（简称交互）交交互互计计算算是是在在完完成成任任务务过过程程中中包包含含了了与与外外部部世世界界通信计算通信计算计计算算主主体体含含有有与与不不受受它它控控制制外外部部环环境境交交互互输输入入和和输出动作输出动作14第14页交互特点交互特点基于交互模型和基于图灵机算法模型区分基于交互模型和基于图灵机算法模型区分交交互互任任务务并并非非都都能能简简化化为为函函数数，比比如如永永远远运运行行操操作系统不能由算法模拟作系统不能由算法模拟在在交交互互模模型型中中，计计算算环环境境是是模模型型一一部部分分，而而且且经经过过动动态态地地向向计计算算系系统统或或计计算算主主体体提提供供输输入入并并消消费费其输出值而表达为交互计算中活跃一部分其输出值而表达为交互计算中活跃一部分在在交交互互模模型型中中，其其中中计计算算能能够够是是并并行行，一一个个计计算算主体能够和它环境以及其它计算主体并行工作主体能够和它环境以及其它计算主体并行工作计算与交互计算与交互15第15页交互影响交互影响交交互互为为计计算算现现象象提提供供一一个个新新概概念念模模型型,它它强强调调交交互互而而不不是是算算法法。并并行行、分分布布、反反应应式式(reactive)、嵌嵌入入式式、面面向向部部件件、面面向向主主体体和和面面向向服服务务系系统统都都是是奠定此概念模型主要范例奠定此概念模型主要范例全全部部新新型型计计算算本本质质特特点点是是交交互互，交交互互是是当当代代计计算算问题和复杂性根源问题和复杂性根源交交互互与与计计算算统统一一理理论论是是计计算算机机科科学学基基础础，以以支支撑撑计算机科学整套理论体系计算机科学整套理论体系怎怎样样为为经经典典计计算算和和当当代代计计算算建建立立统统一一理理论论框框架架?这这是近几十年来计算机科学面临重大挑战是近几十年来计算机科学面临重大挑战计算与交互计算与交互16第16页计算与交互计算与交互交互机器模型交互机器模型图灵机图灵机TM或冯或冯诺依曼计算机体系结构不适合作诺依曼计算机体系结构不适合作为交互机器模型为交互机器模型1.次序交互次序交互机机SIM(sequential interactive machine)SIM:M=(S,I,f)S:可枚举状态集，可枚举状态集，I:可枚举输入串集可枚举输入串集 f:S I S OTM可计算函数，即可计算函数，即(s,i)(s,o)从从sk-1到到sk状态转移：原子状态转移：原子I/O序对序对(ik,ok)输入不确定性输入不确定性:动态输入动态输入ik不可预测不可预测(依赖于依赖于ok-1)输出确实定性输出确实定性:ok由由ik确定确定(很轻易扩展到很轻易扩展到ok不确定不确定)SIM行为由行为由I/O流流(i1,o1),(i2,o2),(i3,o3),刻画刻画17第17页计算与交互计算与交互交互机器模型交互机器模型2.持久图灵机持久图灵机PTM：，表示能力等价于，表示能力等价于SIM3.多带交互机多带交互机MIM：，表示能力大于，表示能力大于SIM但都不足以作为先前提到各种交互计算主要范但都不足以作为先前提到各种交互计算主要范例统一机器模型例统一机器模型能描述交互演算能描述交互演算 演算是对前述挑战最成功回应演算是对前述挑战最成功回应 演演算算两两个个主主要要特特色色：行行为为（或或观观察察）等等价价概概念念，以及对交互行为模式分类新类型理论以及对交互行为模式分类新类型理论 演演算算已已经经被被应应用用到到编编程程语语言言设设计计、分分布布式式系系统统分分析和验证等领域，产生了广泛影响析和验证等领域，产生了广泛影响18第18页次序交互数学模型次序交互数学模型在计算表示力上从算法到次序交互延伸在数学在计算表示力上从算法到次序交互延伸在数学上表现为一系列延伸上表现为一系列延伸在集合表示力上：在集合表示力上：从良基集到非良基集延伸从良基集到非良基集延伸 非良基集作为无限流次序行为形式模型非良基集作为无限流次序行为形式模型在数学对象定义表示力上：在数学对象定义表示力上：从归纳到余归纳从归纳到余归纳延伸延伸 比比如如，表表示示了了从从字字符符串串到到无无限限字字符符流流转转变变，这这是算法到交互转变基础是算法到交互转变基础在代数表示力上：在代数表示力上：从代数到余代数延伸从代数到余代数延伸 余代数为无限流演算提供工具余代数为无限流演算提供工具从归纳到余归纳从归纳到余归纳19第19页非良基集非良基集良基关系良基关系集合集合A A上一个关系上一个关系 是是良基良基，若不存在，若不存在A A上元上元素无穷递减序列素无穷递减序列a0 a1 a2 （a b iff b a）良基集良基集直观解释：直观解释：不存在无穷递减序列集合不存在无穷递减序列集合非良基关系非良基关系集合集合A A上一个关系是非上一个关系是非良基良基，若存在，若存在A A上元上元素无穷递减序列素无穷递减序列非良基集非良基集直观解释：不恪守上述对良基集限制集合直观解释：不恪守上述对良基集限制集合从归纳到余归纳从归纳到余归纳20第20页从归纳到余归纳从归纳到余归纳解释两个记号：笛卡尔积解释两个记号：笛卡尔积对两个集合对两个集合X和和Y，其笛卡儿积是以下序对集合，其笛卡儿积是以下序对集合X Y x,y|x X,y Y 射影函数射影函数Proj1:X Y X和和Proj2:X Y Y满足满足等式等式(1)Proj1(x,y)=x(2)Proj2(x,y)=y21第21页从归纳到余归纳从归纳到余归纳解释两个记号：可区分并（又称和、余积）解释两个记号：可区分并（又称和、余积）对两个集合对两个集合X和和Y，其可区分并是以下序对集合，其可区分并是以下序对集合X+Y 0,x|x X 1,y|y Y 内射函数内射函数(又称余射影函数又称余射影函数)InLeft:X X+Y和和InRight:Y X+Y 满足等式满足等式 InLeft(x)=0,x InRight(y)=1,y 22第22页集合方程最小解与最大解集合方程最小解与最大解下面集合方程最小解是下面集合方程最小解是A上字符串集上字符串集t unit+(A t)t,A和和unit分别是集合变量分别是集合变量,字符集和某个特殊字符集和某个特殊元素集合；元素集合；unit元素代表空集元素代表空集 “”表示两边同构而不是相等表示两边同构而不是相等下面集合方程最大解是下面集合方程最大解是A上无限字符流集上无限字符流集t (A t)(与上面方程比较与上面方程比较,没有没有unit)表达出延伸出来概念与原来概念对偶性表达出延伸出来概念与原来概念对偶性对偶性在代数和余代数上表达得最清楚对偶性在代数和余代数上表达得最清楚从归纳到余归纳从归纳到余归纳23第23页从归纳到余归纳从归纳到余归纳归纳与余归纳比较归纳与余归纳比较1.归纳归纳是结构主义方法，用它定义数据时，可分解成是结构主义方法，用它定义数据时，可分解成三个基本步骤：基本情况、迭代规则和最小化条件三个基本步骤：基本情况、迭代规则和最小化条件 比如，数据集比如，数据集A上上有限表有限表集可归纳地定义以下集可归纳地定义以下(1)基础情况：基础情况：nil(空表空表)是是有限表有限表(2)迭代规则：迭代规则：若若a A且且 是有限表，则是有限表，则cons(a,)是有限表是有限表(3)最小化条件：另外最小化条件：另外,有限表集中不含其它元素有限表集中不含其它元素 最小化规则指所定义集合是满足最小化规则指所定义集合是满足(1)和和(2)两条两条约束最小集合，约束最小集合，无无任何垃圾在其中任何垃圾在其中24第24页从归纳到余归纳从归纳到余归纳归纳与余归纳比较归纳与余归纳比较1.归纳归纳可计算函数可计算函数 f:X Y 在两个层次上是归纳在两个层次上是归纳 (1)归纳定义静态值域：归纳定义静态值域：X是归纳定义是归纳定义 例：字符串集定义例：字符串集定义:t unit+(A t)最小解最小解 (2)归纳定义动态计算：归纳定义动态计算：f 计算过程是归纳计算过程是归纳定义定义图灵机也是类似地经过归纳定义状态转换步骤图灵机也是类似地经过归纳定义状态转换步骤,对归纳定义串进行变换，图灵机局限也是源于对归纳定义串进行变换，图灵机局限也是源于其基于归纳其基于归纳25第25页从归纳到余归纳从归纳到余归纳归纳与余归纳比较归纳与余归纳比较2.余归纳余归纳用用余余归归纳纳定定义义数数据据时时，可可分分解解成成两两个个基基本本步步骤骤：迭代规则和最大化条件。与归纳相比，它删去基迭代规则和最大化条件。与归纳相比，它删去基础情况，修改迭代规则，用最大化取代最小化础情况，修改迭代规则，用最大化取代最小化 比如比如,数据集数据集A上上无限表无限表集可集可余余归纳地定义以下归纳地定义以下(1)迭代规则：迭代规则：若若a A且且 是是无无限表，则限表，则cons(a,)是是无无限表限表(2)最最大大化条件：化条件：数据集数据集A上无上无限表集限表集是满足迭代是满足迭代规则最大集合规则最大集合26第26页从归纳到余归纳从归纳到余归纳归纳与余归纳比较归纳与余归纳比较2.余归纳余归纳最大化条件表示全部未被最大化条件表示全部未被迭代规则迭代规则(1)排除元素排除元素都被包含在所定义集合中，即该集合中任何无限都被包含在所定义集合中，即该集合中任何无限表都能够经过应用规则表都能够经过应用规则(1)若干次而得到若干次而得到交互计算在两个层次上是余归纳交互计算在两个层次上是余归纳 (1)余归纳定义静态值域余归纳定义静态值域 例，无限字符流集定义：例，无限字符流集定义：t (A t)最大解最大解 (2)余归纳定义动态下一步动作余归纳定义动态下一步动作(后面有例子后面有例子)27第27页从归纳到余归纳从归纳到余归纳归纳与余归纳比较归纳与余归纳比较3.例：例：有限表有限表结构算子结构算子(constructor)有有nil和和cons无限表结构算子仅有无限表结构算子仅有cons两种表都有两种表都有观察算子观察算子head和运算算子和运算算子tail，合称为，合称为解构算子解构算子(destructor)而且都有性质而且都有性质 head(cons(a,)=a tail(cons(a,)=二者分别对应二者分别对应 集合方程集合方程t unit+(A t)最小解最小解 集合方程集合方程t (A t)最大解最大解28第28页从归纳到余归纳从归纳到余归纳归纳和余归纳定义函数比较归纳和余归纳定义函数比较1.归纳定义函数归纳定义函数在在计算计算有限表有限表表长表长函数函数length归纳定义中，归纳定义中，需要定义需要定义length作用于全部结构算子值：作用于全部结构算子值：length(nil)=0 length(cons(a,)=1+length()怎样给出一个函数在余归纳定义集合上余归纳怎样给出一个函数在余归纳定义集合上余归纳定义？定义？29第29页从归纳到余归纳从归纳到余归纳归纳和余归纳定义函数比较归纳和余归纳定义函数比较2.余归纳定义函数余归纳定义函数考虑字符集考虑字符集A上无限表，现在有函数上无限表，现在有函数f:A A定义定义f 拓展函数拓展函数ext(f)，它把，它把f 应用到无限表应用到无限表 每个每个元素，得到新无限表元素，得到新无限表ext(f)()余归纳定义即定义解构算子在每个余归纳定义即定义解构算子在每个ext(f)()上值上值 head(ext(f)()=f(head()tail(ext(f)()=ext(f)(tail()在这些等式左边，在这些等式左边，f 出现在解构算子出现在解构算子“里面里面”在归纳定义中，在归纳定义中，length出现在结构算子出现在结构算子“外面外面”：length(nil)=0,length(cons(a,)=1+length()30第30页从归纳到余归纳从归纳到余归纳互模拟互模拟例例：无限表无限表上上odd运算运算 odd：忽略全部：忽略全部偶数位置元素偶数位置元素后组成无限表后组成无限表 head(odd()=head()tail(odd()=odd(tail(tail()用等式演算可得用等式演算可得 head(tail(odd()=head(odd(tail(tail()=head(tail(tail()不难证实，对全部自然数不难证实，对全部自然数n head(tail(n)(odd()=head(tail(2n)()31第31页从归纳到余归纳从归纳到余归纳互模拟互模拟例例：无限表无限表上上odd运算运算 odd：忽略全部：忽略全部偶数位置元素偶数位置元素后组成无限表后组成无限表 head(odd()=head()tail(odd()=odd(tail(tail()顺便说一句：顺便说一句：从计算角度，欲求从计算角度，欲求head(odd()结果，不能等结果，不能等odd()结果算出后，再交给结果算出后，再交给head函数函数(不终止不终止)须用惰性计算方法：须用惰性计算方法：在在head函数需要下一个数据函数需要下一个数据时，时，odd才计算下一个数据并提供给才计算下一个数据并提供给head32第32页从归纳到余归纳从归纳到余归纳互模拟互模拟怎样证实怎样证实余归纳定义数据和函数性质余归纳定义数据和函数性质1、一些性质、一些性质能够用归纳法来证实能够用归纳法来证实，比如证实，比如证实head(tail(n)(odd()=head(tail(2n)()2、互模拟、互模拟余归纳证实专用方法余归纳证实专用方法从数学上刻画系统（如对象、进程等）行为等价从数学上刻画系统（如对象、进程等）行为等价这个直观概念这个直观概念指两个系统从观察者角度看，能够相互模拟对方指两个系统从观察者角度看，能够相互模拟对方行为行为33第33页从归纳到余归纳从归纳到余归纳互模拟互模拟 经过无限表上例子来解释经过无限表上例子来解释 先前已定义先前已定义oddhead(odd()=head()tail(odd()=odd(tail(tail()定义定义eveneven=odd tail 定义定义mergehead(merge(,)=head()tail(merge(,)=merge(,(tail()34第34页从归纳到余归纳从归纳到余归纳互模拟互模拟基于互模拟证实基于互模拟证实merge(odd(),even()=互模拟是满足下面条件关系互模拟是满足下面条件关系R：若若 ,R，则，则 head()=head()而且而且 tail(),tail()R基于互模拟余归纳证实原理是：基于互模拟余归纳证实原理是：对互模拟关系对互模拟关系R，若，若 ,R，则，则 =按上述原理，先定义关系按上述原理，先定义关系 R=merge(odd(),even(),|是无限表是无限表 只要证实只要证实R是互模拟关系即可是互模拟关系即可 35第35页从归纳到余归纳从归纳到余归纳互模拟互模拟第一个条件证实第一个条件证实 head(merge(odd(),even()=head(odd()=head()第二个条件证实第二个条件证实 需证需证 tail(merge(odd(),even(),tail()也在也在R中中1.tail(merge(odd(),even()=merge(even(),tail(odd()36依据依据tail(merge(,)=merge(,(tail()第36页从归纳到余归纳从归纳到余归纳互模拟互模拟第一个条件证实第一个条件证实 head(merge(odd(),even()=head(odd()=head()第二个条件证实第二个条件证实 需证需证 tail(merge(odd(),even(),tail()也在也在R中中1.tail(merge(odd(),even()=merge(even(),tail(odd()=merge(odd(tail(),odd(tail(tail()37 依据依据even=odd tail 和和 tail(odd()=odd(tail(tail()第37页从归纳到余归纳从归纳到余归纳互模拟互模拟第一个条件证实第一个条件证实 head(merge(odd(),even()=head(odd()=head()第二个条件证实第二个条件证实 需证需证 tail(merge(odd(),even(),tail()也在也在R中中1.tail(merge(odd(),even()=merge(even(),tail(odd()=merge(odd(tail(),odd(tail(tail()=merge(odd(tail(),even(tail()38依据依据even=odd tail 第38页从归纳到余归纳从归纳到余归纳互模拟互模拟第一个条件证实第一个条件证实 head(merge(odd(),even()=head(odd()=head()第二个条件证实第二个条件证实 需证需证 tail(merge(odd(),even(),tail()也在也在R中中1.tail(merge(odd(),even()=merge(even(),tail(odd()=merge(odd(tail(),odd(tail(tail()=merge(odd(tail(),even(tail()2.merge(odd(tail(),even(tail(),tail()在在R中中,故故 tail(merge(odd(),even(),tail()也在也在R中中39因为因为 merge(odd(),even(),在在R中中,把把 代换成代换成tail()可得可得第39页从归纳到余归纳从归纳到余归纳互模拟互模拟 利用归纳和等式演算，也能够证实利用归纳和等式演算，也能够证实merge(odd(),even()=但没有这么简练但没有这么简练 需用归纳法先证实下面几个等式：需用归纳法先证实下面几个等式：head(tail(n)(odd()=head(tail(2n)()head(tail(2n)(merge(,)=head(tail(n)()head(tail(2n+1)(merge(,)=head(tail(n)()然后利用等式演算证实然后利用等式演算证实head(tail(n)(merge(odd(),even()=head(tail(n)()40第40页从代数到余代数从代数到余代数笛卡尔积（先前已给出）笛卡尔积（先前已给出）对两个集合对两个集合X和和Y，其笛卡儿积是以下序对集合，其笛卡儿积是以下序对集合X Y x,y|x X,y Y 射影函数射影函数Proj1:X Y X和和Proj2:X Y Y满足满足等式等式 Proj1(x,y)=x Proj2(x,y)=y41第41页从代数到余代数从代数到余代数笛卡尔积笛卡尔积对对任意任意函数函数f:Z X和和g:Z Y,存在唯一存在唯一“配配对对”函数函数 f,g:Z X Y 使得使得Proj1 f,g =f 且且Proj2 f,g =g即对即对z Z，f,g(z)=f(z),g(z)X Y注：注：f,g 看成函数名看成函数名二元积二元积这些性质在范围论中这些性质在范围论中能够用交换图表能够用交换图表(右图右图)表示表示可推广到可推广到n元积情况元积情况YZ f,g X YXProj1gfProj242第42页从代数到余代数从代数到余代数可区分并（又称和、余积）可区分并（又称和、余积）（先前已给出）（先前已给出）对两个集合对两个集合X和和Y，其可区分并是以下序对集合，其可区分并是以下序对集合X+Y 0,x|x X 1,y|y Y 内射函数内射函数(又称余射影函数又称余射影函数)InLeft:X X+Y和和InRight:Y X+Y 满足等式满足等式 InLeft(x)=0,x InRight(y)=1,y 43第43页从代数到余代数从代数到余代数可区分并（又称和、余积）可区分并（又称和、余积）对对任意任意函数函数f:X Z和和g:Y Z,存在唯一存在唯一余余配配对函数对函数f,g:X+Y Z使得使得 f,g InLeft =f 且且f,g InRight=g即对即对w X+Y,f,g(w)=二元和二元和这些性质在范围论中这些性质在范围论中能够用交换图表能够用交换图表(右图右图)表示表示可推广到可推广到n元和情况元和情况注注:f,g看成函数名看成函数名YZf,gX+YXInLeftgfInRight f(x),w=0,x g(y),w=1,y 44第44页从代数到余代数从代数到余代数笛卡尔积和可区分并笛卡尔积和可区分并它们交换图表区分是：箭头恰好相反它们交换图表区分是：箭头恰好相反可区分并用于描述代数可区分并用于描述代数,笛卡尔积用来描述余代数笛卡尔积用来描述余代数从它们交换图表对偶性来体会代数和余代数关系从它们交换图表对偶性来体会代数和余代数关系这是介绍这部分目标这是介绍这部分目标YZf,gX+YXInLeftgfInRightYZ f,g X YXProj1gfProj245第45页从代数到余代数从代数到余代数自然数代数自然数代数自然数自然数N N 上零和后继函数上零和后继函数0:unit N N（0是归纳定义基础情况）是归纳定义基础情况）S:N N N N（S是结构算子）是结构算子）组成函子组成函子F代数代数 N N,0,S:F(N N)N N ,其中其中N N 称称为载体，为载体，F(N N)=unit+N N。函数。函数0,S称为该代数代称为该代数代数结构数结构 函子是范围之间保结构函子是范围之间保结构映射，深入了解需要映射，深入了解需要范围论知识范围论知识N NN N0,Sunit+N NunitInLeftS0InRight46第46页从代数到余代数从代数到余代数一个简单余代数一个简单余代数两个集合两个集合U(状态集状态集)和和 A(可观察数据集可观察数据集)和函数和函数value:U A（value是观察算子）是观察算子）next:U U（next是运算算子）是运算算子）组成函子组成函子G余代数余代数 U,value,next:U G(U),其中其中U称为该余代数载体，称为该余代数载体，G(U)=A U。函数。函数 value,next 称为该余代数称为该余代数余代数结构余代数结构 因为余代数经常描述因为余代数经常描述动态系统，载体也叫做动态系统，载体也叫做状态空间状态空间UU value,next A UAProj1nextvalueProj247第47页从代数到余代数从代数到余代数例：例：有两个按键有两个按键value和和next机器机器 按按value键时不影响机器内部状态，并产生数据集键时不影响机器内部状态，并产生数据集A某个元素某个元素(可见属性可见属性)，连续按，连续按value键产生一样结键产生一样结果果 按按next键时机器转移到另一个状态，该状态性质键时机器转移到另一个状态，该状态性质可经过按可经过按value键来观察键来观察 该机器能够用状态空间该机器能够用状态空间U上下述余代数来描述上下述余代数来描述 value,next :U A U 其中其中 value,next 由两个函数由两个函数value:U A和和next:U U组成组成48第48页从代数到余代数从代数到余代数例：例：有两个按键有两个按键value和和next机器机器 该机器能够用状态空间该机器能够用状态空间U上下述余代数来描述上下述余代数来描述 value,next :U A U其中其中 value,next 由由 value:U A和和next:U U组组成成 连续地交替按连续地交替按next键和键和value键，能够产生无限序键，能够产生无限序列列(a1,a2,)它能够看成它能够看成N N A上一个函数，其中上一个函数，其中ai=value(next(i)(u)A 若若u1,u2 U给出一样可观察序列，则给出一样可观察序列，则u1和和u2从观察从观察角度不可区分角度不可区分49第49页从代数到余代数从代数到余代数余代数和代数区分余代数和代数区分本质上这是结构和观察之间区分本质上这是结构和观察之间区分 代数由载体集合代数由载体集合U和射入和射入U函数函数a:F(U)U 组成，组成，它通知怎样结构它通知怎样结构U元素元素 余代数由载体集合余代数由载体集合U和逆向函数和逆向函数c:U F(U)组成，组成，此时不知道怎样形成此时不知道怎样形成U元素，仅有作用在元素，仅有作用在U上操作，上操作，它给出关于它给出关于U一些信息一些信息50第50页小小 结结本讲座小结本讲座小结从从三三元元世世界界高高度度概概述述地地介介绍绍云云计计算算、未未来来网网、物物联网和泛在网及计算模型联网和泛在网及计算模型强强调调当当代代计计算算与与经经典典计计算算最最主主要要区区分分之之一一是是交交互互性性介绍次序交互数学模型介绍次序交互数学模型研究方向研究方向怎样为经典计算与新型计算建立统一理论框架怎样为经典计算与新型计算建立统一理论框架各种交互计算机器模型各种交互计算机器模型各种交互计算数学模型各种交互计算数学模型51第51页小小 结结参考文件参考文件孙凝晖等，海计算：物联网新型计算模型，中孙凝晖等，海计算：物联网新型计算模型，中国计算机学会通讯，国计算机学会通讯，6(7)，.7曹爱文等译曹爱文等译,计算机数学计算机数学,清华大学出版社清华大学出版社,林惠民等译，移动与通信系统：林惠民等译，移动与通信系统：演算，清华大学演算，清华大学出版社，出版社，Goldin,D;Smolka,S.A;Wegner,P.(Eds.),Interactive Computation:The New Paradigm,Bart Jacobs and Jan Rutten.A Tutorial on Coalgebras and Coinduction.The Hyper bulletin of the European Association for Theoretical ComputerScience,62:222-259（本讲座理论部分源于此）（本讲座理论部分源于此）52第52页小小 结结相关课程相关课程网络计算与高效算法（研）、高级计算机体系结网络计算与高效算法（研）、高级计算机体系结构（研）、程序设计语言理论（研）构（研）、程序设计语言理论（研）53第53页