Tratamiento N-categorial de la lógica de la programación

Abstract

En el contexto de las técnicas de validación de programas, de las
estructuras de axiomatización de la programación planteadas por
Hoare y del desarrollo de la Lógica de la Programación que
Dijkstra realiza con el operador wp, hemos dotado a los elementos
esenciales que intervienen en dicho desarrollo de una estructura
que permite su estudio en el ámbito de las categorias.
En este trabajo se demuestra que el conjunto de precondiciones de
un fragmento de programa anotado tiene estructura de N-categoría
y que sucede lo mismo con el conjunto de postcondiciones. Más
aún, se ha puesto de manifiesto (y probado) que el operador wp
actúa como un funtor entre estos pares de N-categorías.
Además, los conjuntos de guardas surgen de un modo natural en la
lógica de la programación, han sido tratados desde el punto de
vista de la semántica denotacional (Wlrth para el PASCAL y Scott
y otros, después, en un enfoque más general) y presentados por
Manes y Arbib en su semántica parcialmente aditiva. Pues bien, en
este trabajo se demuestra que los conjuntos de guardas tienen también estructura de N-categoría y gue cualguier N-categoría
dotada de una suma definida adecuadamente tiene estructura de
conjunto de guardas, de tal modo, además, gue el preorden
inducido por la suma en el conjunto de guardas coincide con la
flecha de la N-categoría.
Esta suma es, en concreto, la disyunción exclusiva, lo que
adicionalmente supone una sorprendentemente sencilla definición
alternativa a la suma de las categorías parcialmente aditivas
definida por Manes y Arbib.
Con todo esto, se aportan herramientas conceptuales para
entender mejor y resolver más eficientemente los problemas que
tiene planteados la lógica de la programación, pues se dispone de
un punto de vista distinto y nuevo y de toda una familia de
instrumentos adicionales.---ABSTRACT---In the context of program validation techniques, Hoare's systems
for programming and Dijkstra's development of the logic of
programming, based on the operator wp, we have endowed the
essential features of this development with a structure that
permits to study them in the frame of category theory.
In this thesis we show that the set of preconditions of an
annotated program segment is an N-category, and the same happens
for the set of postconditions. Even more, it is shown that the
operator wp acts as a functor between those pairs of Ncategories.
Furthermore, guard sets come out in a natural way in the logic of
programming, they have been considered from a denotational
semantics point of view (Wirth for Pascal and afterwards Scott
and al. in a more general setting) and they have been embodied
by Manes and Arbib in their partially additive semantics. Then,
it is shown in this thesis that the above mentioned guard sets
also have the structure of an N-category and that any N-category with an appropiately defined sum has the structure of a guard
set in such a way that, besides, the preorder defined in the
guard set by the sum operation coincides with the arrows of the
N-category. This sum is just the exclusive or of Boolean
Logic and this fact adds a surprisingly simple alternative
definition for the sum operation in Manes and Arbib partially
additive categories.
The present work, in summary, makes a contribution of conceptual
tools for a better understanding and a more efficient solution of
the problems posed to the logic of programming and it does so by
providing a new different point of view and a whole family of
additional techniques.