| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 320.98 KB | Adobe PDF |
Authors
Advisor(s)
Abstract(s)
Kleene Algebra (KA) is an algebraic system that has many applications both in mathematics and
computer science. It was named after Stephen Cole Kleene who extensively studied regular
expressions and finite automata [Kle56].
Moreover it is often used to reason about programs, as it can represent sequential composition,
choice and finite iteration. Furthermore, the need to reason about actions which can be executed
concurrently, spawned SKA. SKA is an extension of KA introduced by Cristian Prisacariu
in [Pri10] that adopts a notion of concurrent actions.
Laguange equivalence is an imperishable problem in computer science. In this thesis we present
the reader with a detailed explanation of a decision procedure for SKA terms and an OCaml
implementation of said procedure as well.
A Kleene Algebra (KA) é um sistema algébrico que tem bastantes aplicações quer no campo da matemática como também da informática. Foi batizada com o nome do seu inventor Stephen Cole Kleene, que ao longo da sua carreira fez um estudo intensivo sobre expressões regulares e autómatos finitos [Kle56]. Quando há necessidade de raciocinar equacionalmente sobre programas, recorre-se frequentemente à Kleene Algebra, visto que esta consegue exprimir noções de escolha, composição sequencial e até a noção de iteração. A necessidade de raciocinar equacionalmente sobre ações que podem ser executadas de forma concorrente levou ao aparecimento da Algebra de Kleene Síncrona ou Synchronous Kleene Algebra (SKA). Esta última foi introduzida por Cristian Prisacariu em 2010 no seu artigo [Pri10] como uma extensão à Kleene Algebra mas que contém uma noção de ação concorrente. A equivalência de linguagens é um problema perene em ciências da computação. Nesta dissertação iremos apresentar ao leitor uma explicação detalhada de um processo de decisão para termos de Synchronous Kleene Algebra (SKA) bem como a sua implementação utilizando a linguagem de programação OCaml.
A Kleene Algebra (KA) é um sistema algébrico que tem bastantes aplicações quer no campo da matemática como também da informática. Foi batizada com o nome do seu inventor Stephen Cole Kleene, que ao longo da sua carreira fez um estudo intensivo sobre expressões regulares e autómatos finitos [Kle56]. Quando há necessidade de raciocinar equacionalmente sobre programas, recorre-se frequentemente à Kleene Algebra, visto que esta consegue exprimir noções de escolha, composição sequencial e até a noção de iteração. A necessidade de raciocinar equacionalmente sobre ações que podem ser executadas de forma concorrente levou ao aparecimento da Algebra de Kleene Síncrona ou Synchronous Kleene Algebra (SKA). Esta última foi introduzida por Cristian Prisacariu em 2010 no seu artigo [Pri10] como uma extensão à Kleene Algebra mas que contém uma noção de ação concorrente. A equivalência de linguagens é um problema perene em ciências da computação. Nesta dissertação iremos apresentar ao leitor uma explicação detalhada de um processo de decisão para termos de Synchronous Kleene Algebra (SKA) bem como a sua implementação utilizando a linguagem de programação OCaml.
Description
Keywords
Álgebra de Kleene Álgebra de Kleene Síncrona Processo de Decisão