Abstract:
We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focusing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first prove a normalisation theorem for abstract rewrite systems (ARS), a general rewriting framework encompassing many rewriting systems developed by P-A. Melliès [20]. The theorem states that multistep strategies reducing so called necessary and never-gripping sets of redexes at a time are normalising in any ARS. Gripping refers to an abstract property reflecting the behaviour of higher-order substitution. We then apply this result to the particular case of PPC, a calculus of patterns and to the lambda-calculus with parallel-or. © 2017 Elsevier B.V.
Registro:
Documento: |
Artículo
|
Título: | On abstract normalisation beyond neededness |
Autor: | Bonelli, E.; Kesner, D.; Lombardi, C.; Ríos, A. |
Filiación: | Departamento de Ciencia y Tecnología, Univ. Nacional de Quilmes, Roque Sáenz Peña 352 (1876), Bernal, Prov. de Buenos Aires, Argentina CONICET, Av. Rivadavia 1917 (1033), C.A. Buenos Aires, Argentina IRIF, CNRS and Univ. Paris-Diderot, Case 7014, Cedex 13, Paris, 75205, France Univ. de Buenos Aires, Pabellón I, Ciudad Universitaria (1428), C.A. Buenos Aires, Argentina
|
Palabras clave: | Neededness; Normalisation; Pattern calculi; Rewriting; Sequentiality; Biomineralization; Differentiation (calculus); Neededness; Normalisation; Pattern calculi; Rewriting; Sequentiality; Calculations |
Año: | 2017
|
Volumen: | 672
|
Página de inicio: | 36
|
Página de fin: | 63
|
DOI: |
http://dx.doi.org/10.1016/j.tcs.2017.01.025 |
Título revista: | Theoretical Computer Science
|
Título revista abreviado: | Theor Comput Sci
|
ISSN: | 03043975
|
CODEN: | TCSCD
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03043975_v672_n_p36_Bonelli |
Referencias:
- Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C., A nonstandard standardization theorem (2014) POPL '14, pp. 659-670. , S. Jagannathan P. Sewell ACM
- Accattoli, B., Dal Lago, U., Beta reduction is invariant, indeed (2014) CSL-LICS '14, pp. 81-8:10. , T. Henzinger D. Miller ACM
- Antoy, S., Middeldorp, A., A sequential reduction strategy (1996) Theoret. Comput. Sci., 165 (1), pp. 75-95
- Balabonski, T., On the implementation of dynamic patterns (2010) HOR '10, Electronic Proceedings in Theoretical Computer Science, 49, pp. 16-30. , E. Bonelli July
- Balabonski, T., Optimality for dynamic patterns: extended abstract (2010) PPDP '10, pp. 16-30. , M. Fernández July T. Kutsia July W. Schreiner July ACM July
- Barendregt, H.P., The Lambda Calculus: Its Syntax and Semantics (1984), Elsevier Amsterdam; Berry, G., Bottom-up computations of recursive programs (1976) RAIRO Theor. Inform. Appl., 10 (3), pp. 47-82
- Bonelli, E., Kesner, D., Lombardi, C., Ríos, A., Normalisation for dynamic pattern calculi (2012) RTA, LIPIcs, 15, pp. 117-132. , A. Tiwari Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik
- Bonelli, E., Kesner, D., Lombardi, C., Ríos, A., An abstract normalisation result with applications to non-sequential calculi (2014), http://arxiv.org/abs/1412.2118; Baader, F., Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press Cambridge; Boudol, G., Computational semantics of term rewriting systems (1985) Algebraic Methods in Semantics, pp. 169-236. , M. Nivat J.C. Reynolds Cambridge University Press
- Curry, H.B., Feys, R., Combinatory Logic (1958), North-Holland Publishing Company Amsterdam; Endrullis, J., Grabmayer, C., Klop, J.-W., van Oostrom, V., On equal μ-terms (2011) Theoret. Comput. Sci., 412 (28), pp. 3175-3202
- Huet, G.P., Lévy, J.-J., Computations in orthogonal rewriting systems, I and II (1991) Computational Logic – Essays in Honor of A. Robinson, pp. 395-443
- Jay, B., Pattern Calculus: Computing with Functions and Structures (2009), Springer Publishing Company, Incorporated; Jay, B., Kesner, D., Pure pattern calculus (2006) ESOP '06, LNCS, 3924, pp. 100-114. , Peter Sestoft Springer-Verlag
- Jay, B., Kesner, D., First-class patterns (2009) J. Funct. Programming, 19 (2), pp. 191-225
- Kennaway, R., Sequential evaluation strategies for parallel-or and related reduction systems (1989) Ann. Pure Appl. Logic, 43 (1), pp. 31-56
- Klop, J.-W., Combinatory Reduction Systems (1980), PhD thesis Utrecht University; Melliès, P.-A., Description abstraite des Systèmes de Réécriture (1996), PhD thesis Université Paris VII; O'Donnell, M.J., Computing in Systems Described by Equations (1977) LNCS, 58. , Springer-Verlag
- Sekar, R.C., Ramakrishnan, I.V., Programming in equational logic: beyond strong sequentiality (1993) Inform. and Comput., 104 (1), pp. 78-109
- van Oostrom, V., Normalisation in weakly orthogonal rewriting (1999) RTA, LNCS, 1631, pp. 60-74. , P. Narendran M. Rusinowitch Springer-Verlag
- van Raamsdonk, F., Confluence and Normalisation for Higher-Order Rewriting (1996), PhD thesis Vrije University; van Raamsdonk, F., Outermost-fair rewriting (1997) TLCA, LNCS, 1210, pp. 284-299. , P. de Groote Springer-Verlag
- van Raamsdonk, F., van Oostrom, V., The dynamic pattern calculus as a higher-order pattern rewriting system (2014) HOR '14, , K. Rose July
Citas:
---------- APA ----------
Bonelli, E., Kesner, D., Lombardi, C. & Ríos, A.
(2017)
. On abstract normalisation beyond neededness. Theoretical Computer Science, 672, 36-63.
http://dx.doi.org/10.1016/j.tcs.2017.01.025---------- CHICAGO ----------
Bonelli, E., Kesner, D., Lombardi, C., Ríos, A.
"On abstract normalisation beyond neededness"
. Theoretical Computer Science 672
(2017) : 36-63.
http://dx.doi.org/10.1016/j.tcs.2017.01.025---------- MLA ----------
Bonelli, E., Kesner, D., Lombardi, C., Ríos, A.
"On abstract normalisation beyond neededness"
. Theoretical Computer Science, vol. 672, 2017, pp. 36-63.
http://dx.doi.org/10.1016/j.tcs.2017.01.025---------- VANCOUVER ----------
Bonelli, E., Kesner, D., Lombardi, C., Ríos, A. On abstract normalisation beyond neededness. Theor Comput Sci. 2017;672:36-63.
http://dx.doi.org/10.1016/j.tcs.2017.01.025