Variações sobre o cálculo-lambda call-by-value

Abstract

Plotkin apresentou em 1975 a primeira proposta para o cálculo-lambda call-by-value, um sistema formal que modela uma linguagem de programação call-by-value, e vários outros sistemas têm sidos pro postos desde então. No entanto, este sistema é incompleto para a semântica CPS (continuation-passing style), ou seja, existem termos com a mesma semântica que não podem ser provados iguais no cálculo de Plotkin. Nesta dissertação estudamos a extensão de Sabry-Felleisen, o cálculo computacional de Moggi e o cálculo-𝜆𝑄 de Dyckhoff-Lengrand, três sistemas formais com origens diferentes, que são uma resposta ao problema da incompletude do cálculo de Plotkin relativamente à semântica CPS. Provamos que existe uma correspondência equacional entre a extensão de Sabry-Felleisen e o cálculo computacional. Propomos uma simplificação do cálculo-𝜆𝑄 e identificamos o núcleo correspondente. Por fim, provamos que existe uma correspondência equacional entre o núcleo do cálculo-𝜆𝑄 simplificado e o núcleo do cálculo computacional.

In 1975 Plotkin presented the very first call-by-value lambda-calculus, a formal system that models a call-by-value programming language. Since then, many other systems has been presented. Nevertheless, this system turned out to be incomplete for the CPS (continuation-passing-style) semantics. In other words, there are terms with the same semantic that are not proved equal in Plotkin’s lambda-calculus. In this dissertation, we study Sabry-Felleisen’s extension of Plotkin’s calculus, Moggi’s computational lambda-calculus and Dyckhoff-Lengrand’s 𝜆𝑄-calculus, three formal systems with different origins, that are an answer to Plotkin’s incompleteness problem with respect to CPS semantics. We prove that there is an equational correspondence between Sabry-Felleisen’s extension and the computational calculus. We present a simplified 𝜆𝑄-calculus and we identify its kernel. Finally, we prove that there is an equational correspondence between the kernel of the simplified 𝜆𝑄-calculus and the kernel of the computational lambda-calculus.