On The Expressiveness Of Higher Order π-Calculus In A Model Independent Framework

One of the most concerned research direction of process calculus is the expressiveness study,as it aims at exploring the nature of a model's neccesity and the relative expressiveness to othermodels. Lots of work has been done in concrete models and have been criticzed for lacking aset of model independent criteria, which makes it hard to justify the merits of the previous work.Focusing on the general principle of process models , Fu presented a model independent framworkto compare the expressiveness of two di?erent models. The two core concetts of this theory are theabsolute equality relation within a model and the subbisimlarity relation among models.Motivated by the attempt to study the process theory in an integrated way, we give a system-atic study of the higher orderπ-calculus with respect to the model independent framework. Thecontributions of the thesis can summarized as follows:We give a coincidence result of the well-known context bisimulation and the so-called ab-solute equality in higher orderπ-calculus. The correctness of our characterization is thenguaranteed by the model independence of the absolute equality.We restudy the relative expressiveness ofπ-calculus and higher orderπ-calculus and showthat the latter can be encoded into the former in a very strong sense. That is, the encodingsatis?es the subbisimilarity requirement.In order to prove the subbisimilarity relation in the above encoding, we have made use of theup to expansion technique. This is the ?rst time that such technique is applied in the study ofmodel independent framework.