Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/85093
Título: | Variações sobre o cálculo-lambda call-by-value |
Outro(s) título(s): | Variations about the call-by-value lambda-calculus |
Autor(es): | Mendes, Filipa Simões |
Orientador(es): | Espírito Santo, José |
Palavras-chave: | Cálculo-lambda Call-by-value Call-by-name Continuation-passing-style Linguagens de programação funcionais Cálculo de sequentes Lógica intuicionista Lambda-calculus Funcional programming languages Sequent calculus Intuicionistic logic |
Data: | 11-Jan-2023 |
Resumo(s): | 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. |
Tipo: | Dissertação de mestrado |
Descrição: | Dissertação de mestrado em Matemática e Computação |
URI: | https://hdl.handle.net/1822/85093 |
Acesso: | Acesso aberto |
Aparece nas coleções: | BUM - Dissertações de Mestrado DMAT - Dissertações de Mestrado |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Filipa Simoes Mendes.pdf | Dissertação de Mestrado | 436,82 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons