Discrimination by parallel observers: The algorithm

The main result of the paper is a constructive proof of the following equiv alence: two pure A-terms are observationally equivalent in the lazy concurr ent A-calculus iff they have the same Levy-Longo trees. An algorithm which allows to build a context discriminating any two pure A-terms with differen t Levy-Longo trees is described, It follows that contextual equivalence coi ncides with behavioural equivalence (bisimulation) as considered by Sangior gi, Another consequence is that the discriminating power of concurrent lamb da contexts is the same as that of Boudol-Laneve's contexts with multiplici ties, (C) 1999 Academic Press.