El zipper relacional: Una verificación formal

Ponente(s): Fernando Abigail Galicia Mendoza

Realizar cambios locales en una estructura de datos funcional, por ejemplo actualizar el valor de un nodo en un árbol, puede resultar ineficiente ya que la solución usual consiste en la destrucción total de la estructura para llegar al punto donde se debe realizar el cambio (a lo cual le llamamos el foco), para finalmente reconstruir la estructura de datos en su totalidad. Gérard Huet en respuesta a esta problemática define una estructura de datos, llamada zipper, cuyo fin es particionar una estructura en una descripción de la misma hasta donde se encuentra el foco en cuestión y una subestructura correspondiente a dicho foco. Por otra parte, Yuta Ikeda y Susumu Nishimura mencionan que las funciones que destruyen y reconstruyen la estructura a partir del zipper son funciones parciales no inyectivas, ocasionando que la composición de estas resulte en errores de cómputo indeseables, solucionando este problema empleando un lenguaje relacional. En esta plática se construirá el zipper relacional y se hará una verificación formal del enfoque recién mencionado con el apoyo del asistente de pruebas COQ (http://coq.inria.fr/). Este trabajo se realiza en el marco del proyecto UNAM PAPIME proyecto PE102117.