Tesis doctoral de Narciso Marti Oliet
La logica lineal ha sido desarrollada recientemente por girard como una logica de acciones que parece muy adecuada para computacion concurrente. En la parte i estudiamos algunas relaciones entre logica lineal y concurrencia, en especial redes de petri, desde el punto de vista de su semantica categorica, basada en la idea de meseguer y montanari de ver una «red de petri como un monoide». El comportamiento de una red de petri puede describirse usando la conectiva lineal; los estados de la red se convierten en proposiciones de logica lineal y sus computaciones en deducciones. Establecemos una correspondencia triangular que identifica, por un lado objetos en una categoria monoidal, estados de una red de petri y proposiciones en el fragmento de la logica lineal, y por otro morfismos en la categoria, computaciones en la red y pruebas en ese fragmento de la logica lineal. presentamos ademas una nueva axiomatizacion algebraica de modelos de la logica lineal con negacion, basada en el concepto de objeto dualizante. Una categoria lineal es una categoria con un objeto dualizante y productos finitos. Esta nueva axiomatizacion es mucho mas simple que una previa debida a seely, basada en la nocion de categoria -autonoma de barr. La adjuncion entre teorias lineales y categorias lineales demuestra que la logica lineal es una logica categorica. Estudiamos varias clases de modelos de logica lineal definidas ecuacionalmente, asi como relaciones entre ellas, y realizamos una detallada comparacion entre las nociones de categoria con un objeto dualizante y de categoria autonoma. en la parte ii proponemos un marco en el que dos relaciones de subtipo como inclusion y de subtipo como conversion implicita se distinguen e integran. desarrollamos una semantica funtorial para el algebra con tipos ordenados, basada en categorias con productos y una estructura de inclusiones, que llamamos pi-categorias. probamos que la categoria de algebras y
Datos académicos de la tesis doctoral «Sobre dos logicas categoricas: logica lineal y algebra con tipos ordenados«
- Título de la tesis: Sobre dos logicas categoricas: logica lineal y algebra con tipos ordenados
- Autor: Narciso Marti Oliet
- Universidad: Complutense de Madrid
- Fecha de lectura de la tesis: 01/01/1991
Dirección y tribunal
- Director de la tesis
- Jose Messeguer Guaita
- Tribunal
- Presidente del tribunal: Ignacio Sols Lucia
- Fernando Orejas Valdés (vocal)
- Ugo Montanari (vocal)
- Fernandez-prida De Carlos José (vocal)