Relating the λσ- and λs-styles of explicit substitutions
Two methods of explicit substitutions, λσ- 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: λσ; λσ↑; λv; λs; λt; and λu. Results proved that λt is more adequate than λv and that λu is more adequ...
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | JOUR |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_0955792X_v10_n3_p349_Kamareddine |
| Aporte de: |
| Sumario: | Two methods of explicit substitutions, λσ- 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: λσ; λσ↑; λv; λs; λt; and λu. Results proved that λt is more adequate than λv and that λu is more adequate that λv, λσ↑, and λs. Counterexamples is given to show that all other comparisons are impossible according to the criterion. |
|---|