Cálculo lambda digitado - Typed lambda calculus

Um cálculo lambda digitado é um formalismo digitado que usa o símbolo lambda ( ) para denotar a abstração de função anônima. Nesse contexto, os tipos geralmente são objetos de natureza sintática atribuídos a termos lambda; a natureza exata de um tipo depende do cálculo considerado (veja os tipos abaixo). De um certo ponto de vista, cálculos lambda digitados podem ser vistos como refinamentos do cálculo lambda não digitado , mas de outro ponto de vista, eles também podem ser considerados a teoria mais fundamental e cálculo lambda não digitado um caso especial com apenas um tipo. ${\ displaystyle \ lambda}$

Os cálculos lambda digitados são linguagens de programação fundamentais e são a base das linguagens de programação funcional digitada , como ML e Haskell e, mais indiretamente, linguagens de programação imperativa digitada . Os cálculos lambda digitados desempenham um papel importante no projeto de sistemas de tipos para linguagens de programação; aqui, a tipabilidade geralmente captura as propriedades desejáveis ​​do programa (por exemplo, o programa não causará uma violação de acesso à memória).

Os cálculos lambda digitados estão intimamente relacionados à lógica matemática e à teoria da prova por meio do isomorfismo de Curry-Howard e podem ser considerados como a linguagem interna de classes de categorias ; por exemplo, o cálculo lambda simplesmente digitado é a linguagem das categorias fechadas cartesianas (CCCs).

Tipos de cálculos lambda digitados

Vários cálculos lambda digitados foram estudados. O cálculo lambda simplesmente digitado tem apenas um construtor de tipo , a seta , e seus únicos tipos são tipos básicos e tipos de função . O Sistema T estende o cálculo lambda simplesmente digitado com um tipo de números naturais e recursão primitiva de ordem superior; neste sistema, todas as funções comprovadamente recursivas na aritmética de Peano são definíveis. O sistema F permite o polimorfismo usando a quantificação universal sobre todos os tipos; de uma perspectiva lógica, pode descrever todas as funções que são comprovadamente totais na lógica de segunda ordem . Cálculos lambda com tipos dependentes são a base da teoria dos tipos intuicionistas , o cálculo de construções e a estrutura lógica (LF), um cálculo lambda puro com tipos dependentes. Baseado no trabalho de Berardi sobre sistemas de tipo puro , Henk Barendregt propôs o cubo Lambda para sistematizar as relações de cálculos lambda tipados puros (incluindo cálculo lambda simplesmente digitado, Sistema F, LF e o cálculo de construções). ${\ displaystyle \ to}$ ${\ displaystyle \ sigma \ to \ tau}$

Alguns cálculos lambda digitados introduzem uma noção de subtipagem , ou seja, se for um subtipo de , então todos os termos de tipo também têm tipo . Digitado lambda cálculos com subtipos são o cálculo lambda simplesmente tipado com tipos conjuntivas e Sistema F _<: . ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A}$${\ displaystyle B}$

Todos os sistemas mencionados até agora, com exceção do cálculo lambda não tipado, são fortemente normalizados : todos os cálculos terminam. Portanto, eles não podem descrever todas as funções computáveis ​​de Turing . Como outra consequência, eles são consistentes como uma lógica, ou seja, existem tipos desabitados. Existem, no entanto, cálculos lambda digitados que não são fortemente normalizados. Por exemplo, o cálculo lambda de tipo dependente com um tipo de todos os tipos (Tipo: Tipo) não está normalizando devido ao paradoxo de Girard . Este sistema também é o sistema de tipo puro mais simples, um formalismo que generaliza o cubo Lambda. Os sistemas com combinadores de recursão explícitos, como a " Linguagem de programação para funções computáveis " (PCF) de Plotkin , não estão normalizando, mas não devem ser interpretados como uma lógica. Na verdade, o PCF é uma linguagem de programação funcional tipificada, prototípica, em que os tipos são usados ​​para garantir que os programas se comportem bem, mas não necessariamente que estejam sendo encerrados.

Aplicativos para linguagens de programação

Na programação de computadores , as rotinas (funções, procedimentos, métodos) de linguagens de programação fortemente tipadas correspondem de perto a expressões lambda tipadas.

Veja também

• Cálculo Kappa - um análogo do cálculo lambda tipado que exclui funções de ordem superior

Notas

Leitura adicional

• Barendregt, Henk (1992). "Lambda Calculi with Types" . Em Abramsky, S. (ed.). Antecedentes: Estruturas Computacionais . Handbook of Logic in Computer Science. 2 . Imprensa da Universidade de Oxford. pp. 117–309. ISBN   9780198537618 .