Listas: Una Formalización Relacional

Abstract

Las Fork Álgebras constituyen un poderoso cálculo relacional para la derivación de programas. Esta clase de álgebras resulta de extender las álgebras relacionales con un nuevo operador, llama.do Jork que permite la introducción, por definición, de proyecciones. En este a.rtículo damos una axiomatización del tipo de datos lista expresada en el lenguaje de las fork álgebras. La importancia de contar con una teoría de listas expresada en dicho lenguaje, con una notación uniforme y precisa, es imperiosa, ya que buena parte de la tarea de construcción formal de programas recae en el adecuado manejo de los tipos de datos. El método utilizado consiste en introducir constantes de relaciones junto con axiomas que las mismas deben cumplir para expresar las operaciones básicas sobre listas. Además, se prueban algunas propiedades conocidas utilizando los axiomas y se definen algunas operaciones derivadas para operar con listas.