SimpleLambda: uma linguagem funcional didática com tradução para o Cubo Lambda

Abstract

Cálculo Lambda é um modelo de computação proposto por Alonzo Church. É baseado na definição e aplicação de funções anônimas, sendo o comportamento dos termos definido por meio da substituição de parâmetros por argumentos. Em continuação desses estudos, Church também propõe uma variação com tipos, o Cálculo Lambda Simplesmente Tipado (STLC). Com a adição de um sistema de tipos, o cálculo perde expressividade e deixa de ser Turing Completo, mas adquire uma propriedade nova, a Normalização Forte. Todos os termos bem-tipados do STLC garantidamente chegam a uma forma normal, ou seja terminam a sua execução. Nas décadas seguintes, outros cálculos tipados foram desenvolvidos, adicionando funcionalidades como: polimorfismo, construtores de tipos e tipos dependentes. Essas funcionalidades aumentam a expressividade em relação ao STLC e mantêm a Normalização Forte. Posteriormente foi proposta uma estrutura de organização para relacionar esses cálculos, o Cubo Lambda. Partindo de STLC, cada aresta representa a adição de uma dessas funcionalidades, e cada vértice representa o cálculo resultante. Na disciplina de Tópicos Especiais em Cálculo Lambda e Teoria de Tipos do curso de Ciência da Computação da UFRGS, esses cálculos são vistos com o suporte de simuladores onde se pode definir e avaliar termos de cálculo lambda tipado. Esses simuladores foram desenvolvidos pelo professor Rodrigo Machado do Instituto de Informática da UFRGS, e oferecem diversas funcionalidades para a definição e visuali zação dos termos. Para cada cálculo visto na disciplina há um simulador diferente com uma sintaxe própria para expressar as funcionalidades do cálculo que está simulando, o que pode dificultar o processo de relacionar esses cálculos entre eles. Este trabalho propõe uma linguagem de programação funcional simples chamada SimpleLambda, e desenvolve uma aplicação web onde o código SimpleLambda pode ser compilado para os simuladores dos quatro cálculos vistos na disciplina de Cálculo Lambda e Teoria de Tipos.

Lambda Calculus is a model of computation proposed by Alonzo Church. It is based on the definition and application of anonymous functions, with each term’s behavior be ing defined by the substitution of parameters for arguments. Continuing these studies, Church also proposes a typed variation, Simply Typed Lambda Calculus (STLC). With the addition of a type system, the calculus loses expressive power and is no longer Turing Complete, it does however, acquire a new property: Strong Normalization. All well typed STLC terms are guaranteed to reach a normal form, that is, finish its execution. In the following decades, many other typed calculi were developed, adding functionalities such as: polymorphism, type constructors and dependent types. These functionalities increase the expressive power compared to STLC and retain Strong Normalization. A structure was later proposed to organize and draw relations between the calculi, it was named the Lambda Cube. Starting with STLC, each edge represents the addition of one of these functionalities, and each vertex represents the resulting calculus. In the Special Topics in Lambda Calculus and Type Theory class of the Computer Science curriculum at UFRGS, these calculi are studied with the support of online simulators where terms can be defined and evaluated. These simulators were developed by professor Rodrigo Machado of the Institute of Informatics of UFRGS, and they offer many functionalities to define and visu alize lambda terms. There is a different simulator for each of the studied calculi, with its own syntax to express the functionalities of calculus being simulated, which can make it more difficult to draw relations between these calculi. This work proposes a simple func tional programming language called SimpleLambda and implements a web application where SimpleLambda code can be compiled to the simulators of any of the four calculi studied in the Lambda Calculus and Type Theory class.