摘要
通过类型理论使得程序语言在静态可以检查是否出错,这给程序语言带来许多优势。类型理论中的重要性质包括:弱化规则、删除规则、强化规则等。首先给出了结构归纳法、良基归纳法、规则归纳法和余归纳法的形式化定义。在给出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.
出处
《江西科学》
2015年第2期248-253,共6页
Jiangxi Science
关键词
归纳法
类型理论
类型性质证明
induction proof
type theory
properties proofs of type theory
