Revisa técnicas relacionadas à correspondência de Curry-Howard

Estou procurando fontes sobre a noção formalizada de programas. Isso parece estar intimamente relacionado à correspondência de Curry-Howard, mas também se pode rastrear isso na Universal Turing Machines e em sua capacidade de ler a descrição e a entrada de qualquer TM.

Ao ler sobre a correspondência de Curry-Howard, sinto que a primordialidade das UTM-s pode prejudicar a pesquisa de programas com a conclusão única de que qualquer programa pode ser reduzido a símbolos, estados e regras. Existe uma abordagem oposta, onde sistemas de computação de alto nível são definidos e examinados? Quais são os bons recursos sobre isso?

O que você deseja existe e é uma enorme área de pesquisa: é toda a teoria das linguagens de programação.

Em termos gerais, é possível visualizar a computação de duas maneiras. Você pode pensar em máquinas ou em idiomas .

Uma máquina é basicamente algum tipo de controle finito aumentado com alguma memória (possivelmente ilimitada). É por isso que as classes introdutórias do TOC passam de autômatos finitos para autômatos de empilhamento para máquinas de Turing - cada classe assume um controle finito e adiciona um pouco mais de memória a ela. (Atualmente, o controle finito é frequentemente limitado ainda mais, como nos modelos de circuito.) O essencial é que o controle finito seja dado de antemão e de uma só vez.

Uma linguagem é uma maneira de especificar toda uma família de controles, de maneira composicional. Você tem formas primitivas para controles básicos e operadores para criar controles maiores a partir de controles menores. A linguagem primordial, o cálculo lambda, na verdade não especifica nada além de controle - as únicas coisas que você pode definir são abstrações de funções, aplicativos e referências de variáveis.

$snm$

Pesquisadores em complexidade e algoritmos geralmente consideram as máquinas fundamentais, porque estão interessadas em custos e em resultados de viabilidade . Para exagerar um pouco, a questão básica da pesquisa que eles têm é:

Qual é a máquina menos poderosa que pode resolver um certo tipo de problema?

Os pesquisadores de idiomas tomam as línguas como fundamentais, porque estamos interessados ​​em resultados de expressividade e impossibilidade . Com um exagero semelhante, nossa pergunta básica de pesquisa é:

Qual é a linguagem mais expressiva que exclui um certo tipo de mau comportamento?

Como um aparte, observe como os dois bens de cada tipo de valores teóricos estão diretamente em conflito! Um bom trabalho em algoritmos e complexidade permite resolver um problema mais difícil, usando menos recursos. O bom trabalho nas linguagens permite que os programadores façam mais coisas, enquanto proíbe mais comportamentos ruins. (Esse conflito é basicamente o motivo pelo qual a pesquisa é difícil.)

Agora, você pode perguntar por que mais tipos de teoria A não usam linguagens ou por que mais pesquisadores da teoria B não usam máquinas. A razão surge da forma da questão de pesquisa básica.

Observe que a pergunta de pesquisa básica estilizada em algoritmos / complexidade é uma questão de limite inferior - você quer saber que tem a melhor solução e que não há maneira possível de fazer melhor, por mais inteligente que seja. Uma definição de linguagem corrige os meios de composição do programa e, portanto, se você provar que há um limite inferior com um modelo de linguagem, poderá ficar com a questão de saber se de alguma forma não será possível fazer melhor se você estender sua linguagem com alguma novo recurso. Um modelo de máquina oferece a você todo o controle de uma só vez, e você sabe tudo o que a máquina pode fazer desde o início.

Mas as especificações da máquina são exatamente a coisa errada para dizer coisas interessantes sobre como bloquear o mau comportamento. Uma máquina oferece a você todo um controle inicial, mas saber que um programa em particular está bom ou ruim não ajuda quando você deseja estendê-lo ou usá-lo como uma sub-rotina - como o epigrama de Perlis afirma: "Todo programa é um parte de algum outro programa e raramente se encaixa. " Como os pesquisadores de idiomas estão interessados ​​em dizer coisas sobre classes inteiras de programas, os idiomas são muito mais adequados para o propósito.