Um Estudo Sobre a Correspondência Entre Programação Funcional com Continuações e Programação Imperativa Single Assignment

Abstract

No universo das linguagens de programação existe uma diversidade grande de paradigmas, frequentemente motivados pela necessidade da resolução computacional de novos problemas, em novos contextos. Dois destes paradigmas, que atraem a atenção de programadores e cientistas da computação desde os primórdios das linguagens de programação, são o paradigma imperativo e o paradigma funcional.

Estes dois paradigmas assentam em ideias bastante diferentes. O paradigma imperativo baseia-se numa noção de estado e em programas que são sequências de comandos cuja execução vai provocando alterações ao estado. Por sua vez, o paradigma funcional baseia-se na noção matemática de função e a execução de programas (uma coleção de funções) corresponde ao cálculo do valor de uma expressão, envolvendo as funções definidas no programa.

No entanto, existem fragmentos do paradigma imperativo e do paradigma funcional que podem ser relacionados. De facto, o formato Single-Assignment (SA), do lado imperativo, e o formato Continuation- Passing Style (CPS), do lado funcional, que são usados como linguagens “intermédias” no processo de compilação de linguagens de programação mais abstratas, por facilitarem e agilizarem processos de optimização na geração de código máquina eficiente correspondem, na essência, a uma mesma linguagem.

Neste trabalho estuda-se de uma forma detalhada a relação entre programação imperativa no formato SA e programação funcional no formato CPS. Recorrendo a uma linguagem imperativa simples para representar o formato SA e a um subconjunto do λ-calculus para o formato CPS, construímos, entre eles, uma bijeção sintática (ao nível dos programas) e semântica (ao nível da execução de programas). Um resultado destas bijeções é que o formato SA pode ser pensado como uma certa escolha de representantes de classe para a noção de α-equivalência para programas imperativos correspondente a essa mesma noção para λ-termos

Durante o trabalho, foi ainda desenvolvida uma pequena ferramenta computacional, implementada na linguagem Haskell, que permitiu testar e animar os diversos conceitos envolvidos no estudo.

Alternate abstract:

In the universe of programming languages there is a wide range of paradigms that are often motivated by the need to solve new computational problems, in new contexts. Two of these paradigms, which have drawn programmers and computer scientists’ attention since the beginnig of programming languages, are the imperative programming paradigm and the functional programming paradigm.

Both paradigms are built upon different ideas. The imperative programming paradigm is based on the notion of state, its programs are built by sequencing multiple commands, and execution generates state changes. The functional programming paradigm is based on the notion of mathematical function (a program is a collection of functions) and program execution corresponds to the evaluation of expressions (involving the functions defined in the program).

Nevertheless, there are fragments within the imperative programing paradigm and the functional programming paradigm that can be related. The Single Assignment (SA) form, on the imperative programming paradigm, and the Continuation-Passing Style(CPS) form in the functional programming paradigm, are used as “intermediate” languages in the compilation process of more abstract languages, due to the fact that they simplify and make more agile the processes of optimization when it comes to the genaration of efficient machine code, they are in its essence the same language.

In this work we study in detail the relationship between imperative programming in the SA form and functional programming in the CPSform.

Using a simple imperative language to represent the SA form and a subset of λ-calculus in CPSform, we built between them a syntatic bijection (at code level) and a semantic bijection (at program execution level). We concluded that the SA form can be tought as a certain choice of class representatives in the notion of α-equivalence in imperative programs that matches that same notion in λ-terms.

During this work, we developed a small computational tool using the Haskell language which allowed us to simulate multiple concepts that are involved in the study.