摘要
Symbolic bisimulation avoids the infinite branching problem causedby instantiating input names with all names in the standard definition of bisimulation in л-calculus. However, it does not automatically lead to an efficient algorithm,because symbolic bisimulation is indexed by conditions on names,and directly manipulating such conditions can be computationally costly. In this paper a new notionof bisimulation is introduced, in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names. It is shownthat the new notion captures symbolic bisimulation in a precise sense. Based on thenew definition an efficient algorithm, which instantiates input names 'on-the-fly', ispresented to check bisimulations for finite-control л-calculus.
Symbolic bisimulation avoids the infinite branching problem causedby instantiating input names with all names in the standard definition of bisimulation in л-calculus. However, it does not automatically lead to an efficient algorithm,because symbolic bisimulation is indexed by conditions on names,and directly manipulating such conditions can be computationally costly. In this paper a new notionof bisimulation is introduced, in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names. It is shownthat the new notion captures symbolic bisimulation in a precise sense. Based on thenew definition an efficient algorithm, which instantiates input names 'on-the-fly', ispresented to check bisimulations for finite-control л-calculus.
