Two methods of explicit substitutions, ?s- and ?s-styles, are compared. A criterion of adequacy is used to simulate ß-reduction in calculi of explicit substitutions and apply it to several calculi: ?s; ?s?; ?v; ?s; ?t; and ?u. Results proved that ?t is more adequate than ?v and that ?u is more adequate that ?v, ?s?, and ?s. Counterexamples is given to show that all other comparisons are impossible according to the criterion.
|Number of pages||32|
|Journal||Journal of Logic and Computation|
|Publication status||Published - Jun 2000|