Bigraph反应系统中赋类与归纳类型表述及其相互关系研究

在Bigraph反应系统(Bigraphical Reactive System，BRS)的研究中，赋类与归纳类型是其模型精化和应用的关键。如何对BRS的赋类与归纳类型进行形式化的表述以及两种表述间存在的关系仍然是该研究领域的热点和难点问题。本项目拟构造具有子类型及多态类型的BRS形式系统，给出对应类型系统Lambda演算的BRS描述并证明类型保持性、可靠性等性质；对类型化的BRS进行范畴描述，给出具有简单类型、子类型和多态类型的BRS元模型的Fibration形式；用其类型系统的Fibration构造各类型系统相应的谓词逻辑。在赋类与谓词对应研究的基础上，讨论逻辑等价下赋类BRS和归纳类型BRS间的关系及其衍生标号迁移系统的互模拟关系。深入研究BRS的赋类与归纳类型的表述及其相互关系将不仅有助于完善BRS的形式化语义模型，而且也有助于利用BRS建立移动分布式系统核心理论框架体系。

Research of sortings and inductive type systems over bigraphical reactive systems (BRS) plays a key role in the refinements of this model and its practical applications.It is one of focus and difficulty problems in this field how to depict sortings and inductive type systems over bigraphical reactive systems formally and to discuss the relationship between them.The main research work of this project includes: firstly, we develop simply type systems with subtyping and polymorphism type over bigraphical reactive systems, moreover, we model the simply.typed lambda calculi with subtyping and polymorphic typed lambda calculus with corresponding typed bigraphical reative systems respectively. And then subject reduction and type soundness are proved. Secondly, typed bigraphical reative systems are represented by fibred category, that is, simply type systems, simply type systems with subtyping and polymorphism type systems over bigraphical.reactive systems can be described by fibration.Thirdly, the logic over every fibration is given to describe the properties of the corresponding typed systems with the principle that a logic is always a logic over a type. Lastly, based on the research of correspondence relationship between sortings and predicate, we discuss the relationship between sorted bigraphical reactive systems and typed.bigraphical reactive systems if they have the same predicate. And in the same condition we discuss the relationship between their derived labeled transition systems also.We believe that further research on sortings and inductive type systems over bigraphical reactive systems not only improve formal semantics model of bigraphical reactive systems, but also contribute to modeling of theoretical framework of mobile distributed systems.