Programação coindutiva: calculos e aplicações

Abstract

Como estruturas formais, tanto as álgebras iniciais como as coalgebras finais fornecem descrições abstractas de uma variedade de fenómenos em programação, em particular, das estruturas de dados e dos comportamentos, respectivamente. As propriedades universais que as definem oferecem métodos de definição e princípios de prova, i.e., uma base para o desenvolvimento de cálculos de programas directamente baseados em (em rigor, orientados por) especificações de tipos. Mais ainda, tais propriedades universais podem ser codificadas em combinadores e usadas, não apenas para calcular programas, mas também para programar. Na programação funcional o papel destes combinadores tornou-se fundamental como base de toda uma disciplina de derivação e de transformação de algoritmos. Do lado coalgébrico, modelar coalgebricamente sistemas dinâmicos e raciocinar por coindução tem emergido recentemente como uma área de pesquisa activa. Neste contexto, a actual dissertação tem como principal objectivo o estudo de estruturas coalgébricas e a sua aplicação à construção de programas. A ênfase é colocada nos princípios que permitem raciocinar sobre tais estruturas, conduzindo a uma aproximação por cálculo à coindução que evita a construção explícita das bissimulações. A aproximação é discutida no contexto de dois casos de estudo: um em torno do cálculo de sequências infinitas e outro da especificação coindutiva da álgebras de processos clássicas. Todas as construções e exemplos apresentados são prototipados na linguagem funcional HASKELL.

As formal structures, both initial algebras and final coalgebras provide abstract descriptions of a variety of phenomena in programming, in particular of data and behavioural structures, respectively. Being defined by universal properties, both entail definitional and proof principles, i.e., a basis for the development of program calculi directly based on (actually driven by) type specifications. Moreover, such properties can be turned into programming combinators and used, not only to calculate programs, but also to program with. In functional programming the role of such universals has been fundamental to a whole discipline of algorithm derivation and transformation. On the coalgebraic side, coalgebraic modelling of dynamical systems and reasoning by coinduction has recently emerged as an active area of research. Such is the context of the present dissertation: the study of coalgebraic structures and their application to systemsâ construction. Its main focus, however, is placed on reasoning principles for such structures, introducing an entirely calculational approach to coinduction which avoids the explicit construction of bisimulations, and, therefore, promotes a reasoning style closer to the actual program construction practice. The approach is discussed in the context of two case-studies: a calculus of infinite sequences and a coinductive formulation of classical process algebras. All constructions and examples presented are prototyped in the functional language HASKELL.