The Expressiveness Of π-Calculus Via Programming

Many investigations showed that theπ-calculus has captured much of the ex-pressiveness of the computing models proposed so far. Therefore it is of great signif-icance for other models to compare their expressiveness againstπ. The comparisonsprovide the means to study sequential computing models in richer context with welldeveloped tools inπ-calculus. As for several seemingly more expressive computingmodels, such as the Ambient calculi, the comparisons can offer significant tests of theexpressiveness ofπand helps in getting deeper insights into its theory. Some of thesecomparisons have been successfully made, while some have not yet, among whichlies a famous one—- the existence of the encoding from the fullλ-calculus intoπ.In this paper theπ-calculus is studied as a programming language. The idea is touse the programming ability ofπto help compare the expressiveness of theπ-calculusand other models, such asλ-calculus and Ambient calculi.The contributions of this thesis are threefold:1. Expressiveness and programming inπ. Most studies ofπemphasize particu-larly on algebraic properties. As a programming language, theπ-calculus hasnot been properly investigated. In this paper, theπ-calculus is studied as a pro-gramming language to code up data structures and their operations, such as Listand Tree.Encoding is one of the most effective methods to compare expressiveness of onemodel with another. However the sharp differences between two models makethe encoding a tough issue. As the syntax and semantics of most models can beconstrued as programs, a strategy based on programming inπis proposed inthis paper to assist in designing the encoding from models intoπ. 2.λandπ. A successful application of the above strategy is demonstrated a so-lution to a prolonged open problem of whether there exists a good encodingfrom the fullλ-calculus toπ-calculus. An interpretation of Lazyλ-calculus withπwas given by Milner, and the difficulties in translating the fullλintoπwerediscussed.With the programming ability ofπ, the encoding from the fullλ-calculus toπ-calculus is worked out by translatingλ-term to tree structures and programmingthese structures inπ-calculus. The encoding is proved to preserve and re?ectthe beta reduction and is shown to be fully abstract with respect to Abramsky'sapplicative bisimilarity.3. Ambient calculi andπ. Ambient calculi model mobile computations in mobiledevices with special operators in , out and open . Whether they are absolutelymore expressive thanπhas been studies since the pioneering Ambient Calculus– Mobile Ambient was proposed. In this paper the nonexistence of fully abstractencodings from Safe Ambient and Fair Ambient toπis proved. After the hier-archy of Mobile Ambient simulated by the ?atten structure ofπ-calculus withrenaming strategy, an encoding from Mobile Ambient calculus toπis proposedby equipping each ambient with List of name-pairs. This encoding preserves thereduction, but is not fully abstract with respect to the barbed congruence. Usingthe anonymous process (m)m[in n] , we prove that there does not exist a goodencoding from Mobile Ambient toπ-calculus.To sum up, a technique based on programming inπis proposed in this paper toconstruct the encoding from various models intoπ. Successful applications includethe encoding fromλtoπand the translation of Mobile Ambient withπ。The perfectquality of the encoding ofλadds weight to the expressive power ofπand makes itpossible to studyλin a concurrent scenario. The translation of Mobile Ambient pro-motes the proof of negative result which means mobile devices are difficult to simulatewith mobile computations. Both applications are significant for the study of expres-siveness.