Linguagens de programação para computação eficiente

32

É impossível escrever uma linguagem de programação que permita todas as máquinas que param em todas as entradas e nenhuma outra. No entanto, parece ser fácil definir uma linguagem de programação para qualquer classe de complexidade padrão. Em particular, podemos definir uma linguagem na qual podemos expressar todos os cálculos eficientes e apenas cálculos eficientes.

Por exemplo, para algo como : pegue sua linguagem de programação favorita e depois de escrever seu programa (correspondente à Máquina de Turing ), adicione três valores ao cabeçalho: um número inteiro , e número , e uma saída padrão . Quando o programa é compilado, imprima uma máquina de Turing que, dada a entrada do tamanho execute em para etapas . Se não parar antes que as etapas sejam executadas, faça a saída padrãoM c k d M x n M x c n k M c n k d PPMckdMxnMxcnkMcnkd. A menos que eu esteja enganado, essa linguagem de programação nos permitirá expressar todos os cálculos em e nada mais. No entanto, essa linguagem proposta é inerentemente não interessante.P

Minha pergunta: existem linguagens de programação que capturam subconjuntos de funções computáveis ​​(como todas as funções eficientemente computáveis) de uma maneira não trivial? Se não houver, existe uma razão para isso?

Artem Kaznatcheev
fonte
7
Alguns exemplos simples de linguagens de programação que capturam subconjuntos de funções computáveis: expressões regulares e gramáticas sem contexto.
Jukka Suomela
2
Na verdade, os idiomas que classe capturas complexidade como P V (o qual é definido de forma semelhante à função recursiva primitiva com recursão substituído por recursão limitada) são bastante interessante (pelo menos do ponto de vista teórico). :)PPV
Kaveh
A Programação Linear e Inteira captura subconjuntos interessantes de funções computáveis.
Diego de Estrada
O registro de dados só pode expressar algoritmos de tempo polinomial, mas não sei se ele pode expressar todos os algoritmos de tempo polinomial.
Jules
O conhecido artigo "Programação funcional total" argumenta que as linguagens de programação que não têm um problema de parada indecidível são realmente práticas e úteis. jucs.org/jucs_10_7/total_functional_programming
nenhum

Respostas:

32

Um idioma que tenta expressar apenas cálculos de tempo polinomial é o cálculo lambda suave . Seu sistema de tipos está enraizado na lógica linear. Uma tese recente trata dos cálculos polinomiais de tempo e fornece um bom resumo dos desenvolvimentos recentes com base nessa abordagem. Martin Hofmann trabalha no assunto há algum tempo. Uma lista antiga de artigos relevantes pode ser encontrada aqui ; Muitos de seus documentos continuam nessa direção.

Outros trabalhos adotam a abordagem de verificar se o programa usa uma certa quantidade de recursos, usando Tipos dependentes ou Linguagem de montagem digitada .

Ainda outras abordagens são baseadas em cálculos formais limitados por recursos , como variantes do cálculo ambiental.

Essas abordagens têm a propriedade de que programas bem digitados atendem a alguns limites de recursos pré-especificados. O recurso vinculado pode ser tempo ou espaço e, geralmente, pode depender do tamanho das entradas.

Os primeiros trabalhos nesta área são sobre cálculos fortemente normalizados, o que significa que todos os programas bem digitados são interrompidos. O sistema F , também conhecido como cálculo lambda polimórfico, está fortemente normalizando. Ele não possui um operador de ponto fixo, mas é bastante expressivo, embora eu não pense que se saiba a que classe de complexidade ela corresponde. Por definição, qualquer cálculo fortemente normalizador expressa alguma classe de cálculos finais.

A linguagem de programação Charity é uma linguagem funcional bastante expressiva que para em todas as entradas. Não sei que classe de complexidade ela pode expressar, mas a função Ackermann pode ser escrita em Charity.

Dave Clarke
fonte
O que você quer dizer com 'pelo menos' aqui?
Nponeccop
'Pelo menos' aqui significa 'alguns'. Vou mudar minha resposta para torná-la um pouco mais precisa.
Dave Clarke
Tenho certeza de que a complexidade das funções definíveis no sistema F é a classe de funções que terminam no tempo "alguma função comprovadamente total da aritmética de segunda ordem" da entrada. Não uma classe de complexidade muito convencional, mas ainda assim ...
Cody
cody: de acordo com "Teoremas de graça" de Wadler, o Sistema F pode expressar "toda função recursiva que pode ser provada total na aritmética Peano de segunda ordem" e que "inclui a função de Ackermann". Não tenho certeza se é o mesmo que você está descrevendo. A principal característica do Charity é o suporte a codados, enquanto eu acho que a verificação de término da Agda permite mais expressividade do que o Coq e o Sistema F, garantindo o término.
Blaisorblade 20/05
8

Eu também gostaria de mencionar a Teoria da Complexidade Implícita como uma abordagem para isso, já que eu a vi surgir em várias questões um pouco relacionadas. Para citar esta resposta de Neel Krishnaswami :

A técnica básica é relacionar classes de complexidade a subsistemas de lógica linear (as chamadas "lógicas lineares leves"), com a idéia de que a eliminação de corte para o sistema lógico deve estar completa para a classe de complexidade fornecida (como LOGSPACE, PTIME, etc). Então, através do Curry-Howard, você obtém uma linguagem de programação na qual precisamente os programas da classe são expressáveis.

Chris Pressey
fonte
5

Estou surpreso que ninguém tenha mencionado recursão primitiva. Ao restringir a loops limitados (ou seja, o número de iterações para cada loop deve ser calculado antes do início do loop), o programa resultante é recursivo primitivo e, portanto, total. Douglas Hofstadter propôs uma linguagem de programação, BLOOP, que permitia todas e apenas funções recursivas primitivas.

David Harris
fonte
11
É uma subclasse apropriada de todas as funções, mas chamá-la de classe de funções "eficientes" pode ser um pouco exagerada.
Raphael
PP
Outros mencionaram o Sistema F e outras linguagens fortemente normalizadoras, que de certo modo apóiam apenas a "recursão primitiva". No entanto, como eles suportam funções de primeira classe, eles permitem escrever mais programas (como a função Ackermann).
Blaisorblade