An Encoding From λ-Calculus To π-Calculus

Human being advanced while they solved problems. The appearance of computernot only highly accelerated the speed and efficiency in resolving but also brought somecorrespond problems. To solve some questions that occurred frequently, people alwaystried to find the best solution in order to shorten the total time that spent on solvingthese problems. The mathematical models became the key when people tried to finda systematical way. Problems was divides into two parts, modeling and resolving. Inthat situation, some wonderful model was proposed, and the best of them are TuringMachine andλ-Calculus. In fact, their expressiveness are equivalent.With the development of computer and computer science, parallel became themain research object instead of sequential. Sequential computation was built on Tur-ing Machine andλ-Calculus, while there was not such a classical model in parallelcomputation. To solve this problem, Milner created CCS and Hoare invented CSP.Both of them were excellent model of parallel computation. However, these two mod-els were not complete and unable to characterize parallel computing for their disabilityon mobile and interaction. In the 1990s, Milner proposed another powerful calculus,π-calculus to increase the expressiveness of calculus in parallel field. It's really acomplete model, and will help computer scientist in their research.Nevertheless, the problem hasn't been solved completely. Computer scientistsneed to know the relationship of expressiveness of sequential and parallel models.And it's easy to know that, if there is an encoding of sequential model in parallelmodel, it means that parallel model was more powerful. In this case, we would like todiscuss the relationship betweenλ-calculus andπ-calculus. When Milner first talkedaboutπ-calculus in his paper, he considered this problem and raised a solution forthat. However, the target calculus is quit weak and simple, so that he was failed tosolve the problem of expressiveness. Cai and Fu tried to solve it in a creative way. They gave a full-abstraction of fullλ-calculus in a variant ofπ-calculus with matchand mismatch operators. This variant was strictly more expressive than the classicalone. But the target was so strong that we cannot deny the possibility that some kindsof full abstraction still existed in a weaker form. This paper proposed a technology toeliminate match and mismatch operators inπ-calculus, and proved that an equivalencerelation was reserved by the encoding.