In the paper two formats of higher-order rewriting are compared: CombinatoryReduction Systems and Higher-order Rewrite Systems. Although it always has been obvious that both formats are closely related to each other, up to now the exact relationship between them has not been clear. The authors present two translations, one from Combinatory Reduction Systems into Higher-Order Rewrite Systems and one vice versa, based on a detailed comparison of both formats. Since the translations are very 'neat' in the sense that the rewrite relation is preserved and (almost) reflected, the authors can conclude that as far as rewrite theory is concerned, Combinatory Reduction Systems and Higher-Order Rewrite Systems are equivalent, the only difference being that Combinatory Reduction Systems employ a more 'lazy' evaluation strategy. Moreover, due to this result it is the case that some syntactic properties derived for the one class also hold for the other.
展开▼
