Ir al contenido

Documat


Double pushout transformation of algebras

  • Autores: Maria de la Mercè Llabrés Segura Árbol académico
  • Directores de la Tesis: Francesc Andreu Rosselló Llompart (dir. tes.) Árbol académico
  • Lectura: En la Universitat de les Illes Balears ( España ) en 2001
  • Idioma: inglés
  • Tribunal Calificador de la Tesis: Llorenç Valverde García (presid.) Árbol académico, Joan Torrens Sastre (secret.) Árbol académico, Peter Burmeister (voc.) Árbol académico, Martín Grosse-Rhode (voc.) Árbol académico, Gabriel Valiente Feruglio (voc.) Árbol académico
  • Texto completo no disponible (Saber más ...)
  • Resumen
    • La transformación de pushout doble (DPO) de grafos, introducida a principios de los años setenta, es en la actualidad un formalismo de reescritura bien establecido, que ha sido generalizado a diversas categorias de estructuras relacionales y unarias, y que se usa como una tecnica basada en reglas para la especificación formal de sistemas de software, El objetivo final de esta tesis es establecer los fundamentos para el desarrollo de la transformación de DPO de algebras parciales y totales de un tipo arbitario, que permitiria la especificacion de sistemas de software con estados complejos.

      Para ello hemos trabajado en la categoria Alg de álgebras parciales con tipo arbitrario , y su subcategoria plena Alg de algebras cuyas operaciones pertenecientes a un conjunto fijado de simbolos operacionales son totales. Esta ultima categoria cubre el caso de las álgebras totales y de los grafos atribuidos. Tambien hemos considerado la categoria TCF-Alg de álgebras parciales de tipo unario con los conformismos totales como morfismos, porque la transformacion DPO en esta categoria crea un nuevo tipo de transformación de algebras parciales unarias.

      En dichas categorias hemos resuelto los siguientes problemas, los cuales son previos al desarrollo de la transformacion DPO. El problema de la aplicación:

      ¿Cuando podemos aplicar una regla a través de un morfismo? La solución viene dada por lo que suele llamar una condición de pegado: una condición necesaria y suficiente sobre dos morfismos f:k-->A y m:A-->B para la existencia de un complemento de pushout. El problema de la unicidad: ¿para que reglas es siempre único (salvo isomorfismo) el resultado de su aplicación a traves de cada morfismo? La solución viene dada por una condición de unicidad:

      una condición necesaria y suficiente sobre un morfismo f:k-->A para la unicidad salvo isomorfismo del complemento de pushout(caso de existir) de f y cada morfismo m: A-->B.


Fundación Dialnet

Mi Documat

Opciones de tesis

Opciones de compartir

Opciones de entorno