传统共享系统数据模型的建模方法在语义性质分析和语义行为描述方面存在不足,针对以上问题提出了一种基于Fibrations理论的共享系统数据模型。主要工作体现在两个方面:首先,应用真值函子、保持真值的提升与内涵函子并结合代数方法精确分析了语义性质,应用等式函子、保持等式的提升及商函子并结合共代数方法形式化描述了语义行为;其次,在Fibrations理论框架内构造复杂归纳与共归纳数据结构上参数化的递归与共递归操作,抽象描述具有普适意义的归纳与共归纳规则,结合实例简要介绍了Fibrations理论的应用。相对于范畴论等传统方法,简洁描述与灵活扩展的Fibrations理论对共享系统数据模型的语义性质和语义行为进行了精确分析与形式化描述,抽象描述了复杂数据结构具有普适性的归纳与共归纳规则。
There are some drawbacks for traditional modeling methods of data model of sharing system in analyzing semantic properties and describing semantic behaviors. Aiming at the problems mentioned above we present a data model of sharing system based on Fibrations theory. We contribute in the following two aspects. Firstly, we accurately analyze semantic properties by combining algebras methods with truth functor, lifting preserving-truth and comprehension functor, and formally depict semantic behaviors by combining co-algebras methods with equation functor, lifting preserving-equation and quotient functor. Secondly, in the framework of Fibrations theory we construct parameterized recursive and co-recursive operations on complex inductive and co-inductive data structure to abstractly describe inductive and co-inductive rules with universality, and briefly introduce applications of Fibrations theory by examples. Compared with traditional methods such as category theory, the Fibrations theory of brief descriptions and flexible expansibility can accurately analyze semantics properties, formally describe semantic behaviors of data model of sharing system, and abstractly depict inductive and co-inductive rules with universality of complex data structures.