- Yuxi Fu. Theory Defined by Process, 2010. (pdf, last updated on 23 April, 2010)
Theories de ned in a process model are formalized and studied. A theory in a process calculus is a set of well-founded processes that
are perpetually available, each can be regarded as a service, an agent
behind the scene or an axiom. The operational and observational semantics of the theories are investigated. The power of the approach is
demonstrated by interpreting the asynchronous π-calculus as a theory,
the asynchronous theory, in the π-calculus. A complete axiomatic system
is constructed for the asynchronous theory, which gives rise to a proof
system for the weak asynchronous bisimilarity of the asynchronous π.
- Yuxi Fu, Han Zhu. The Name-Passing Calculus, 2010. (pdf, last updated on 23 April, 2010)
Name-passing calculi are foundational models for mobile computing. Research into these models
has produced a wealth of results ranging from relative expressiveness to programming pragmatics.
The diversity of these results call for clari cation and reorganization. This paper applies a model independent approach to the study of the name-passing calculi,
leading to a uniform presentation and simpli cation. The technical tools and the results studied in the paper form the foundation for a theory of name-passing calculus.
- Xiaojuan Cai, Yuxi Fu. The λ-Calculus in the
π-Calculus, 2009. (pdf, last updated on 9 December, 2009.)
A general approach is proposed that transforms, in the
framework of the pi calculus, objects to methods in an on-
the-fly manner. The power of the approach is demonstrated
by applying it to generate an encoding of the full lambda
calculus in the pi calculus. The encoding is proved to preserve
and reflect the beta reduction and is shown to be fully
abstract with respect to Abramsky's applicative bisimilarity.
- Yuxi Fu, Hao Lu. On the Expressiveness of
Interaction. Theoretical Computer Science, 411:1387-1451, 2010. (pdf)
Subbisimilarity is proposed as a general tool to classify the relative expressive power of process calculi. The expressiveness of several variants of CCS is compared in terms of the subbisimilarity relationship. Similar investigation is also carried out for the variants of the pi calculus. The relative expressiveness of the different forms of the choice operation and the different ways of introducing infinite behaviors are systematically studied in both the frameworks of CCS and pi. Some issues concerning the expressiveness of both CCS and pi are clarified. Several open problems are solved along the way. The subbisimilarity approach and the relative expressiveness results are applied to show the independence of the operators of the pi calculus. The definition of the subbisimilarity relationship can be further strengthened with computational requirement, leading to a uniform treatment of computation and interaction.
- Yuxi Fu. The χ-calculus. In Advances in
Computing Science, Proceedings of the 1997 International Conference on
Advances in Parallel and Distributed Computing (APDC'97), pages
74-81. IEEE Computer Society Press, 1997. (pdf)
The paper proposes a new process algebra, called
χ-calculus. The language differs from π-calculus in several
aspects. First it takes a more uniform view on input and
output. Second, the closed names of the language is homogeneous in the
sense that there is only one kind of bound names. Thirdly, the effects
of communications in χ-calculus are delimited by localization
operators, not by sequentiality combinator. Finally, the language
cherishes more freedom of parallelism than χ-calculus. The
algebraic properties of χ-processes are studied in terms of local
bisimulation. It is shown that local bisimilarity is a congruence
equivalence on χ-processes.
- Yuxi Fu. A proof theoretical approach to
communications. In Proceedings of the 24th International Colloquium
on Automata, Languages and Programming (ICALP'97), volume 1256
of Lecture Notes in Computer Science, pages 325-335, Bologna,
Italy, July 1997. Springer. (pdf)
The paper investigates a concurrent computation
model, chi calculus, in which communications resemble cut eliminations
for classical proofs. The algebraic properties of the model are
studied. Its relationship to sequential computation is illustrated by
showing that it incorporates the operational semantics of the
call-by-name lambda calculus. Practically the model has pi calculus as
a submodel.
- Yuxi Fu. Reaction graph. Journal of Computer
Science and Technology, 13:510-530, 1998. (pdf)
The paper proposes reaction graphs as graphical
representations of computational objects. A reaction graph is a
directed graph with all its arrows and some of its nodes
labeled. Computations are modeled by graph rewriting of a simple
nature. The basic rewriting rules embody the essence of both the
communications among processes and cut-eliminations in proofs. Calculi
of graphs are identified to give a formal and algebraic account of
reaction graphs in the spirit of process algebra. With the help of the
calculi, it is demonstrated that reaction graphs capture many
interesting aspects of computations.
- Yuxi Fu. Bisimulation lattice of chi
processes. In Proceedings of the 4th Asian Computing Science
Conference (ASIAN'98), volume 1538 of Lecture Notes in Computer
Science, pages 245-262, Manila, The Philippines, December
1998. Springer. (pdf)
Chi calculus was proposed as a process algebra that
has a uniform treatment of names. The paper carries out a systematic
study of bisimilarities for chi processes. The notion of
L-bisimilarity is introduced to give a possible classification of
bisimilarities on chi processes. It is shown that the set of
L-bisimilarities forms a four element lattice and that well-known
bisimilarities for chi processes fit into the lattice hierarchy. The
four distinct L-bisimilarities give rise to four congruence
relations. Complete axiomatization system is given for each of the
four relations. The bisimulation lattice of asynchronous chi processes
and that of asymmetric chi processes are also investigated. It turns
out that the former consists of two elements while the latter twelve
elements. Finally it is pointed out that the asynchronous asymmetric
chi calculus has a bisimulation lattice of eight elements.
- Yuxi Fu. Open bisimulations on chi processes.
In Proceedings of the 10th International Conference on Concurrency
Theory (CONCUR'99), volume 1664 of Lecture Notes in Computer
Science, pages 304-319, Eindhoven, The Netherlands, August 1999.
Springer. (pdf)
The paper carries out a systematic investigation
into the axiomatization problem of the asymmetric chi calculus. As a
crucial step in attacking the problem, an open style bisimilarity is
defined for each of the eighteen L-bisimilarities and the two are
proved to be equal. On top of the open bisimilarities, explicit
definitions of the eighteen L-congruences are given, which suggest
immediately possible axioms for the congruence relations. In addition
to the axioms for strong bisimilarity, the paper proposes altogether
twenty one additional axioms, three of which being the well-known tau
laws and the other eighteen being new. These axioms help to lift a
complete system for the strong bisimilarity to complete systems for
the eighteen L-congruences.
- Yuxi Fu. Variations on mobile processes.
Theoretical Computer Science, 221:327-368,
1999. (pdf)
The paper investigates a concurrent computation
model, chi calculus, in which communications resemble cut eliminations
for classical proofs. Two bisimilarities, local bisimilarity and
barbed bisimilarity, on chi processes are studied and are shown to be
congruence relations. The former equivalence turns out to be strictly
stronger than the latter. It is shown that chi calculus is capable of
modeling sequential computation in that it captures the operational
semantics of call-by-name lambda calculus. A translation from pi
calculus to chi calculus is given, demonstrating that, practically
speaking, pi is a sublanguage of chi. A higher order version of chi
calculus is proposed and examined. It combines the communication
mechanism of chi calculus and the recursion mechanism of full lambda
calculus, and therefore extends both.
- Yuxi Fu and Zhengrong Yang. Chi calculus with
mismatch. In Proceedings of the 11th International Conference on
Concurrency Theory (CONCUR'00), volume 1877 of Lecture Notes in
Computer Science, pages 596-610, Pennsylvania, USA, August
2000. Springer. (pdf)
The theory of chi processes with the mismatch
operator is studied. Two open congruence relations are
investigated. These are weak early open congruence and weak late open
congruence. Complete systems are given for both congruence
relations. These systems use some new tau laws. The results of this
paper correct some popular mistakes in literature.
- Yuxi Fu and Zhengrong Yang. The ground congruence
for chi calculus. In Proceedings of the 20th Conference on the
Foundations of Software Technology and Theoretical Computer Science
(FSTTCS'00), volume 1974 of Lecture Notes in Computer
Science, pages 385-396, New Delhi, India, December
2000. Springer. (pdf)
The definition of open bisimilarity on the
χ-processes does not give rise to a sensible relation on the
χ-processes with the mismatch operator. The paper proposes ground
open congruence as a principal open congruence on the χ-processes
with the mismatch operator. The algebraic properties of the ground
congruence is studied. The paper also takes a close look at barbed
congruence. This relation is similar to the ground congruence. The
precise relationship between the two is worked out. It is pointed out
that the sound and complete system for the ground congruence can be
obtained by removing one tau law from the complete system for the
barbed congruence.
- Yuxi Fu. Axiomatization without prefix combinator.
In Klaus Keimel et al., editors, Domains and Processes, pages
245-273. Kluwer Academic Publishers, 2001. (pdf)
The chi calculus proposed several years ago enjoys
some properties unknown from the experience with pi calculus, one of
which is the ability to model concurrent computation without the use
of prefix combinator. The atomic chi calculus studied in this paper is
obtained from polyadic chi calculus by leaving out the prefix
operator. This omission is impossible in the pi framework because it
would render the input actions of pi useless. This paper focuses on
complete systems of strong equivalence relations on finite atomic chi
processes. The two equivalence relations investigated in this paper
are strong bisimilarity and strong asynchronous bisimilarity. These
bisimilarities are required to be closed under substitution on each
bisimulation step. By exploring some properties enjoyed by the atomic
chi calculus, it is shown that they coincide respectively with their
ground counterparts. In the definitions of strong ground bisimilarity
and strong asynchronous ground bisimilarity closure under substitution
is not explicitly required. Based upon this fact complete systems are
given for both relations. The axiomatic systems are novel in that they
use none of the prefix, choice and match combinators.
- Yuxi Fu, Zhengrong Yang. Understanding the mismatch
combinator in chi calculus. Theoretical Computer Science,
290:779-830, 2003. (pdf)
The theory of chi processes with the mismatch
operator is studied. Four congruence relations are investigated. These
are late open congruence, early open congruence, ground congruence and
barbed congruence. The late and early open congruence relations are
the chi calculus counterparts of the weak late and early congruence
relations of pi calculus. Both turn out to be special cases of the
ground congruence and the barbed congruence. The ground congruence is
essentially the open congruence. Complete systems are given for all
the four congruence relations. These systems use some interesting tau
laws unknown from previous studies of the chi calculus without the
mismatch combinator. The results of this paper point out that the
mismatch operator changes the algebraic semantics of chi calculus
dramatically. They also correct some common mistakes in
literature.
- Yuxi Fu. Bisimulation congruences of chi
calculus. Information and Computation, 184:201-226,
2003. (pdf)
Chi calculus was proposed as a process calculus that
has a uniform treatment of names. Preliminary properties of chi
calculus have been examined in literature. In this paper a more
systematic study of bisimilarities for chi processes is carried
out. The notion of L-bisimilarity is introduced to give a possible
classification of bisimilarities on chi processes. It is shown that
the set of L-bisimilarities form a four element lattice and that
well-known bisimilarities for chi processes fit into the lattice
hierarchy. The four distinct L-bisimilarities give rise to four
congruence relations. Complete axiomatization system is given for each
of the four congruences.
- Xiaoju Dong and Yuxi Fu. Observing asymmetry and
mismatch. In Proceedings of the 1st Asian Symposium on Programming
Languages and Systems (APLAS'03), volume 2895 of Lecture Notes
in Computer Science, pages 2-19, Beijing, China, November
2003. Springer. (pdf)
The chi calculus is studied in the framework
incorporating two constructions widely useful in applications:
asymmetric communication and mismatch condition. The barbed
bisimilarity is used to give a general picture of how the two
constructions affect the observational theory. Both the operational
properties and the algebraic properties of the enriched calculus are
investigated to support an improved understanding of the bisimulation
behaviors of the model.
- Yuxi Fu. Symmetric π-calculus. Journal of
Computer Science and Technology, 13:202-208, 1998.
- Yuxi Fu. A functional presentation of pi
calculus. Science in China (Series F, Information Sciences),
44(1):20-32, 2001.
- Yuxi Fu. Testing congruence for mobile
process. Journal of Computer Science and Technology,
17(1):73-82, 2002.
- Yuxi Fu, Zhengrong Yang. Tau laws for pi
calculus. Theoretical Computer Science, 308:55-130,
2003. (pdf)
The paper investigates the non-symbolic algebraic
semantics of the weak bisimulation congruences on finite pi
processes. The weak bisimulation congruences are studied both in the
absence and in the presence of the mismatch operator. Some interesting
phenomena about the open congruences are revealed. Several new tau
laws are discovered and their relationship is discussed. The
contributions of the paper are mainly as follows: It is proved that
Milner's three tau laws fail to lift a complete system for the strong
open congruence to a complete system for the weak open congruence in
the absence of both the mismatch operator and the restriction
operator. A fourth tau law is proposed to deal with the match operator
under the prefix operation. It is shown that for this calculus a
complete system for the strong open congruence extended with all the
four tau laws is complete for the weak open congruence. It is verified
that the four tau laws are also enough for the weak open congruence of
the pi calculus without the mismatch operator. A complete system using
distinctions is given. It is pointed out that the standard definition
of the weak open congruence gives rise to a bad equivalence relation
in the presence of the mismatch operator. Two alternatives are
proposed. These are the late open congruence and the early open
congruence. Their difference is similar to that between the weak late
congruence and the weak early congruence. Complete axiomatic systems
for the two weak open congruences are given.
- Yuxi Fu. A schematic axiom for open
congruence. Science in China (Series F), 48:67-77,
2005. (pdf)
A schematic law dealing with localization operator
is proposed for pi calculus. It is shown that the law renders the use
of distinction unnecessary in the axiomatic theory of open
congruence.
- Yuxi Fu. On quasi open bisimulation. Theoretical
Computer Science, 338:96-126, 2005. (pdf)
Quasi open bisimilarity is a variant of the open
bisimilarity based on a closer examination of the observationality of
local names. The paper investigates two alternative characterizations
of the quasi open bisimilarity and provides a complete system for the
weak quasi open congruence.
- Yuxi Fu. Checking equivalence for higher order
process, 2006. Working Paper. (pdf)
In a higher order process calculus, recursion can be
achieved by higher order communications. The Turing complete property
rules out any algorithm to decide the equivalence between two higher
order processes. The paper takes a look at a variant of the calculus
of higher order processes that embodies the idea of resource
sensitiveness. Resource sensitiveness means that a process received
through a communication can only be used once. Two complete systems
are given for the finite higher order pi-processes and the finite
higher order CCS processes. These systems immediately suggest how to
derive algorithms to check the equivalences on the finite higher order
processes.