Como estão relacionadas as linguagens de programação e os fundamentos da matemática?

30

Basicamente, eu estou ciente de três fundamentos para a matemática

  1. Teoria de conjuntos
  2. Teoria dos tipos
  3. Teoria das categorias

Então, de que maneiras as linguagens de programação e os fundamentos da matemática estão relacionados?

EDITAR

A pergunta original era "Linguagens de programação baseadas em fundamentos da matemática"

com o paragarfo adicionado de

E implementações da teoria
1. Teoria dos tipos em Coq
2. Teoria dos conjuntos em SETL
3. Teoria das categorias em Haskell

Com base em uma sugestão, isso foi alterado para "Como as linguagens de programação e os fundamentos da matemática estão relacionados"

Como essa é uma daquelas perguntas em que eu não sabia o suficiente sobre o que estava perguntando, mas queria aprender alguma coisa, estou modificando a pergunta para torná-la mais valiosa para a aprendizagem e outras, deixando os detalhes para não A resposta atual de Andrej Bauer parece fora de tópico.

Obrigado por todos os comentários e respostas até agora, estou aprendendo com eles.

Guy Coder
fonte
1
Não tenho certeza se entendi a pergunta ou as suposições contidas nela. Coq não é uma linguagem de programação, tanto quanto eu entendo. Os programas podem ser extraídos das provas Coq, mas isso não a torna uma linguagem de programação. Também a teoria das categorias e a teoria dos tipos estão intimamente relacionadas, por isso não tenho certeza se podemos categorizá-las como você. Não sei sobre o SETL. Veja também a lista de assistentes de provas na Wikipedia.
Kaveh
3
Haskell não é "uma implementação da teoria das categorias" e, em qualquer caso, os fundamentos da matemática servem a um propósito diferente das linguagens de programação. Embora possa ser feito algum tipo de comparação, não é tão bom tentar forçar a comparação a um relacionamento formal.
Andrej Bauer
1
Link relevante sobre a santíssima trindade
gardenhead
De interesse: Fundações de Software
Guy Coder

Respostas:

29

[Nota: esses parágrafos agora estão desatualizados.] O título da sua pergunta contém uma suposição injustificada, ou seja, que as linguagens de programação são "baseadas em fundamentos da matemática". Geralmente, esse não é o caso, embora as duas áreas tenham relacionamentos importantes. Uma declaração mais precisa seria que (algumas) linguagens de programação foram projetadas usando técnicas fundamentais. Uma pergunta melhor a ser feita seria "como as linguagens de programação e os fundamentos da matemática estão relacionados?"

A conexão mais geral é incorporada no slogan provas como programas , que pode ser feito para funcionar de várias maneiras. A correspondência de Curry-Howard é a mais óbvia. Com ele, relacionamos de uma só vez teoria, lógica e programação de tipos. Mas deve-se enfatizar que a correspondência de Curry-Howard não funciona muito bem na presença de recursão geral (porque todo tipo se torna habitado), suportado por toda linguagem de programação de uso geral.

Uma maneira mais sutil de fazer funcionar o slogan de provas como programas é usar a realização . Também aqui relacionamos provas e programas, mas agora a direção vai de provas para programas: toda prova fornece um programa, mas nem todo programa é necessariamente uma prova.

O principal exemplo de uma linguagem de programação baseada em uma fundação é o Agda , que simplesmente é uma implementação da teoria dos tipos dependentes. No entanto, o Agda não é uma linguagem de programação de uso geral porque não suporta recursão geral. Todas as funções do Agda são totais e existem funções computáveis ​​que não podem ser implementadas no Agda. Na prática, os programadores não perceberão isso, mas perceberão que a Agda não permite valores indefinidos, por exemplo, loops infinitos.

Coq não é uma linguagem de programação, mas um assistente de prova. No entanto, também possui recursos de extração que fornecem programas de provas. Assistentes de prova e linguagens de programação não devem ser confundidos.

Não devemos esquecer que o prólogo e outras linguagens de programação lógica se inspiram na idéia de que a computação é uma prova de pesquisa . É claro que isso os relaciona de perto com a lógica.

Haskell é uma linguagem de programação de uso geral baseada na teoria de domínio . Ou seja, sua semântica é teórica do domínio, porque deve levar em conta funções parciais e recursão. A comunidade Haskell desenvolveu várias técnicas inspiradas na teoria das categorias, das quais as mônadas são mais conhecidas, mas não devem ser confundidas com as mônadas . De maneira mais geral, os recursos avançados de programação geralmente são tratados com uma combinação de teoria de domínio e teoria de categoria, mas isso não é algo que o programador Haskell na rua é adepto. A chamada "categoria sintática" dos tipos de Haskell é a visão de um leigo de como Haskell e a teoria da categoria se correspondem.

A teoria dos conjuntos (clássica ou construtiva) parece inspirar idéias em linguagem de programação em menor grau. Obviamente, a teoria dos conjuntos construtivos tem sua conexão com a programação por meio da lógica construtiva. Uma aplicação importante da teoria dos conjuntos intuicionista às linguagens de programação foi dada por Alex Simpson, que a usou para fazer a teoria do domínio sintético funcionar. Mas isso é algo bastante avançado, talvez veja esses slides . Jean-Louis Krivine desenvolveu uma marca muito interessante de realizabilidade para a teoria clássica dos conjuntos. Essa parece uma boa maneira de relacionar a teoria dos conjuntos clássica e a programação.

Em resumo, a teoria das linguagens de programação utiliza técnicas fundamentais. Isso não é surpreendente, pois consideramos a computação um conceito fundamental. Mas é ingênuo dizer que as linguagens de programação são "baseadas" em certas bases. De fato, a tricotomia das fundações "teoria dos conjuntos - teoria dos tipos - teoria das categorias" é novamente apenas uma observação de alto nível útil que pode ser matematicamente precisa de várias maneiras, mas não há nada necessário. É um acidente histórico.

Andrej Bauer
fonte
"a ideia de que computação é prova de pesquisa ". Estou confuso com esta afirmação. Certamente, a pesquisa de provas é uma forma de cálculo, mas nem todo o cálculo é a pesquisa de provas? No contexto desta pergunta, também há verificação de prova, verificação de tipo. De maneira mais geral, basta adicionar 5 + 3. O que você quer dizer com esta afirmação?
user56834 26/02
6

este é um tópico muito complexo e há muitos livros excelentes sobre o assunto, um recente é chamado Catedral de Turings, origens do universo digital e também Motores de lógica, matemáticos e origens do computador .

as linguagens de computador evoluíram ao longo de muitas décadas, mas acredite ou não, existem duas linguagens de programação originais que mostram que a matemática e a ciência da computação estão intimamente entrelaçadas:

existem duas figuras-chave que cruzaram os limites matemáticos e da ciência da computação em "linguagens de programação":

  • A teoria da informação, pioneira em Shannon, mostra as profundas conexões entre matemática e ciência da computação

  • outra figura-chave que cruza a matemática e a ciência da computação é Von Neumann . ele inventou a arquitetura von neumann de armazenar programas na memória.

ainda mais "linguagens de programação":

  • a palavra em inglês "computador" originalmente significava algo mais como uma "calculadora" que usava operações matemáticas em números e seu significado mudou substancialmente para o conceito de programação de uso geral de hoje. portanto, há uma conexão entre linguagens de programação e calculadoras iniciais.
  • os cartões perfurados usados ​​nos teares do final do século XIX e início do século XX eram uma "linguagem de programação" para os padrões de tecelagem. note que cartões perfurados foram usados ​​para programar mainframes nos anos 60. estes eram originalmente vistos como "máquinas de calcular" (usando a matemática!), não como computadores modernos e de uso geral.
  • Babbage e Ada Lovelace desenvolveram os primeiros conceitos rudimentares de "linguagens de programação" em meados do século XIX em um "mecanismo de cálculo"
  • álgebra booleana era originalmente um conceito puramente matemático inventado por Boole
  • o antigo ábaco (milênios) para cálculo matemático é visto como o precursor do computador moderno. mas pode-se dizer que as operações para manipulá-lo eram uma espécie de "linguagem de programação" (seguida por humanos)

no entanto, nas linguagens de programação modernas, à medida que a abstração aumenta e aumenta, a conexão clara e direta com a matemática diminuiu um pouco ao longo das décadas, mas sempre será bastante intrínseca e, de certa forma, foi fortalecida. por exemplo, linguagens como Java, com seus tipos estritos, tem conexões com a matemática e, no início dos anos 90, as principais linguagens de computador (por exemplo, c ++, Java, Ruby etc.) começaram a implementar explicitamente muitos objetos matemáticos de nível superior, como primitivos no idiomas como conjuntos, árvores (por exemplo, Btrees ou hashmaps), etc.

vzn
fonte