[Prev][Next][Index][Thread]
Communication errors in the polyadic pi-calculus are undecidable
Dear all,
Polyadic-pi error processes are those that reduce to a process
containing a bad-redex (say, a().P | a<z>) not under a prefix.
Whether a given process is an error or not is undecidable - we all
know that. Antonio Ravara and I engaged in the exercise of writing a
simple proof.
Communication Errors in the pi-Calculus are Undecidable
Vasco T. Vasconcelos Ant\'onio Ravara
University of Lisboa Technical University of Lisbon
We present an undecidability proof of the notion of communication
errors in the polyadic pi-calculus. The demonstration follows a
general pattern of undecidability proofs -- reducing a well-known
undecidable problem to the problem in question. We make use of an
encoding of the lambda-calculus into the pi-calculus to show that the
decidability of communication errors would solve the problem of
deciding whether a lambda term has a normal form.
The paper can be obtained at
http://www.di.fc.ul.pt/~vv/papers/commerrors.pdf
Best regards,
vasco
....................................................................
Vasco Thudichum Vasconcelos http://www.di.fc.ul.pt/~vv
Faculdade de Ciências da Universidade de Lisboa, Dep. de Informática
Bloco C5 - Piso 1, Campo Grande, 1700 Lisboa Portugal
Tel: +351-1-750 0087, Fax: +351-1-750 0084, Email: vv@di.fc.ul.pt
....................................................................