[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
....................................................................