Specifying and Verifying a Transformation of Recursive Functions into Tail-Recursive Functions

Autores/as

  • Axel Suárez Polo Benemérita Universidad Autónoma de Puebla
  • José de Jesús Lavalle Martínez Benemérita Universidad Autónoma de Puebla
  • Iván Molina Rebolledo Benemérita Universidad Autónoma de Puebla

DOI:

https://doi.org/10.13053/cys-27-1-4529

Palabras clave:

Dependent types, formal specification and verification, tail recursion, accumulation, program transformation

Resumen

It is well known that some recursive functions admit a tail recursive counterpart which have a more efficient time-complexity behavior. This paper presents a formal specification and verification of such process. A monoid is used to generate a recursive function and its tail-recursive counterpart. Also, the monoid properties are used to prove extensional equality of both functions. In order to achieve this goal, the Agda programming language and proof assistant is used to generate a parametrized module with a monoid, via dependent types. This technique is exemplified with the length, reverse, and indices functions over lists.

Descargas

Publicado

2023-03-30

Número

Vol. 27 Núm. 1 (2023): 27(1) 2023

Sección

Articles of the Thematic Section (2)

Licencia

Transfiero exclusivamente a la revista “Computación y Sistemas”, editada por el Centro de Investigación en Computación (CIC), los Derechos de Autor del artículo antes mencionado, asimismo acepto que no serán transferidos a ninguna otra publicación, en cualquier formato, idioma, medio existente (incluyendo los electrónicos y multimedios) o por desarrollar.

Certifico que el artículo, no ha sido divulgado previamente o sometido simultáneamente a otra publicación y que no contiene materiales cuya publicación violaría los Derechos de Autor u otros derechos de propiedad de cualquier persona, empresa o institución. Certifico además que tengo autorización de la institución o empresa donde trabajo o estudio para publicar este Trabajo.

El autor, representante acepta la responsabilidad por la publicación del Trabajo en nombre de todos y cada uno de los autores.

Esta Transferencia está sujeta a las siguientes reservas:

  • Los autores conservan todos los derechos de propiedad (tales como derechos de patente) de este Trabajo, con excepción de los derechos de publicación transferidos al CIC, mediante este documento.
  • Los autores conservan el derecho de publicar el Trabajo total o parcialmente en cualquier libro del que ellos sean autores o editores y hacer uso personal de este trabajo en conferencias, cursos, páginas web personal, etc.