El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor


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.


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, 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
Página de inicio:36
Página de fin:63


  • 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),; 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


---------- APA ----------
Bonelli, E., Kesner, D., Lombardi, C. & Ríos, A. (2017) . On abstract normalisation beyond neededness, 672, 36-63.
---------- CHICAGO ----------
Bonelli, E., Kesner, D., Lombardi, C., Ríos, A. "On abstract normalisation beyond neededness" 672 (2017) : 36-63.
---------- MLA ----------
Bonelli, E., Kesner, D., Lombardi, C., Ríos, A. "On abstract normalisation beyond neededness" , vol. 672, 2017, pp. 36-63.
---------- VANCOUVER ----------
Bonelli, E., Kesner, D., Lombardi, C., Ríos, A. On abstract normalisation beyond neededness. 2017;672:36-63.