Completeness results for the equivalence of recursive schemas

摘要

We investigate the possibilities of automating equivalence proofs for recursiveschemas. A formal proof system, adapted from work of J. W. deBakker and D. Scott, is shown to be complete with respect to provability of equivalence of pure recursive schemes. The result is obtained by showing the correspondence between operational and denotational semantics of a simple recursive language.