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: |
| id |
todo:paper_0955792X_v10_n3_p349_Kamareddine |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_0955792X_v10_n3_p349_Kamareddine2023-10-03T15:51:47Z Relating the λσ- and λs-styles of explicit substitutions Kamareddine, F. Rìos, A. Theorem proving Explicit substitutions Differentiation (calculus) 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. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_0955792X_v10_n3_p349_Kamareddine |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Theorem proving Explicit substitutions Differentiation (calculus) |
| spellingShingle |
Theorem proving Explicit substitutions Differentiation (calculus) Kamareddine, F. Rìos, A. Relating the λσ- and λs-styles of explicit substitutions |
| topic_facet |
Theorem proving Explicit substitutions Differentiation (calculus) |
| description |
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. |
| format |
JOUR |
| author |
Kamareddine, F. Rìos, A. |
| author_facet |
Kamareddine, F. Rìos, A. |
| author_sort |
Kamareddine, F. |
| title |
Relating the λσ- and λs-styles of explicit substitutions |
| title_short |
Relating the λσ- and λs-styles of explicit substitutions |
| title_full |
Relating the λσ- and λs-styles of explicit substitutions |
| title_fullStr |
Relating the λσ- and λs-styles of explicit substitutions |
| title_full_unstemmed |
Relating the λσ- and λs-styles of explicit substitutions |
| title_sort |
relating the λσ- and λs-styles of explicit substitutions |
| url |
http://hdl.handle.net/20.500.12110/paper_0955792X_v10_n3_p349_Kamareddine |
| work_keys_str_mv |
AT kamareddinef relatingthelsandlsstylesofexplicitsubstitutions AT riosa relatingthelsandlsstylesofexplicitsubstitutions |
| _version_ |
1807315469515882496 |