归纳证明在类型理论中的应用研究  

Research on the Induction Proof on Type Theory

作　　者：袁晓月[1] 黎爽[2] 

机构地区：[1]江西省科学院应用物理研究所,南昌330029 [2]江西财经大学信息管理学院,南昌330013

出　　处：《江西科学》2015年第2期248-253,共6页Jiangxi Science

摘　　要：通过类型理论使得程序语言在静态可以检查是否出错,这给程序语言带来许多优势。类型理论中的重要性质包括:弱化规则、删除规则、强化规则等。首先给出了结构归纳法、良基归纳法、规则归纳法和余归纳法的形式化定义。在给出PA4WS进程代数的语法、语义的基础上给出了其类型定义。在此基础上给出了归纳法在PA4WS类型理论性质证明的应用。There are many advantages of type theory on programming checking programming scripts. The properties of type theory includ languages because it has static e ： weaken rule, deleted rule, strength rule etc. The paper formally defines structural induction, well-formed induction, rule induction and co-induction. Then the properties of type theory are proven by induction proof based on Process Algebra for Web Service （PA4WS） after PA4WS syntax, semantic, type theory are given.

关 键 词：归纳法 类型理论 类型性质证明 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]