Grafos internos e multirrelações como "spans" : propriedades e composicionalidade

Abstract

Um span em uma categoria é um par ordenado de morfismos dessa categoria, ambos com origem num mesmo objeto. O destino do primeiro morfismo é a origem do span e o destino do segundo morfismo é o destino do span. Spans, embora sejam uma estrutura bastante simples numa categoria e tenham uma definição também bastante simples, são versáteis, pois, com especializações sutis apresentadas aqui, são capazes de representar outras estruturas, tais como as tratadas nesses trabalho: relações binárias, multirrelações binárias, grafos e, em conjunto com um morfismo adicional, sistemas de transições etiquetadas (LTS). Permitem ainda, como proposto nesse trabalho, definir de forma também simples, redes de Petri como sendo um endospan em uma categoria. Mostra-se que a composição de spans aplicada a essas estruturas é capaz de expresar a composição de multirrelações — mas não de relações —, uma composição de grafos cujo grafo resultante indica caminhos em que cada parte é uma aresta de um dos grafos operados, uma composição de LTS cujo LTS resultante apresenta transações que podem ser compostas por transições de diferentes LTS e uma composição de redes de Petri cujo resultado também apresenta transações compostas por transições que podem ser realizadas em redes de Petri distintas. Mostra-se algumas propriedades dessas composições, bem como suas provas. Como verificar propriedades de relações e de grafos através de spans também é proposto.