Noções de computação eficiente

11

Um algoritmo de máquina de Turing em tempo polinomial é considerado eficiente se seu tempo de execução, na pior das hipóteses, estiver limitado por uma função polinomial no tamanho da entrada. Estou ciente da forte tese de Church-Turing:

Qualquer modelo razoável de computação pode ser eficientemente simulado em máquinas de Turing

No entanto, não conheço a teoria sólida para analisar a complexidade computacional dos algoritmos de -calculus.λ

Temos uma noção de eficiência computacional para todo modelo conhecido de computação? Existem modelos úteis apenas para questões de computabilidade, mas inúteis para questões de complexidade computacional?

Mohammad Al-Turkistany
fonte

Respostas:

9

Até onde eu sei, os principais modelos de computabilidade são o cálculo λ, máquinas de Turing e funções recursivas . Não estou ciente da situação relativa à complexidade nas funções recursivas, elas podem ou não ser inúteis para a complexidade.

n

O cálculo λ puro era inútil em termos de complexidade. No entanto, um sistema de tipos simples entrou em ação e permitiu garantias de rescisão para alguns termos λ de uma maneira muito fácil. Em seguida, alguns outros sistemas (sistemas T , F , ..) permitiram uma grande expressividade, mantendo o término.

Eficiência ou complexidade, sendo um refinamento da terminação e tipos intimamente relacionados à lógica, mais tarde surgiram lógicas lineares leves que caracterizam várias classes de complexidade. ( Elementar , P e algumas variações para PSPACE e outras). A pesquisa nesse domínio é muito ativa e não se restringe a essas classes de complexidade, nem ao cálculo λ.

tl; dr: λ-calculus foi útil para a computabilidade, terminação e teoria da complexidade.

No entanto, para dar crédito onde o crédito é devido As máquinas de Turing são uma maneira boa e unânime de definir o que é complexidade, mas isso é verdade apenas para limites frouxos como "polinomial", não para limites restritos para os quais os modelos semelhantes a PRAM são mais adequados.

jmad
fonte
Por que, então, fazemos a maioria de nossas análises de tempo de execução usando modelos semelhantes a RAM?
Raphael
O(1 1)O(registro|memory|)nregistro27
@ Rafael: você estava reagindo à minha última frase, certo?
Jmad
Sim, eu fiz (pelo bem do leitor inexperiente).
Raphael
1

β

(λx.term)vterm[x: =v]
1 1

fonte
β
@ Gilles: Como não sabemos qual é o custo real (modelo unitário) da implementação da redução ideal, sua observação não é realmente relevante. Por enquanto, esses estudos fornecem apenas um refinamento do problema indicado nesta resposta.
Stéphane Gimenez
1

Sobre a inclusão do cálculo λ no modelo de complexidade padrão, aqui está o resumo de algumas (muito) novas pesquisas sobre o assunto. Dá uma resposta a esta pergunta para alguma forma restrita de redução β. Basicamente, a complexidade no modelo de custo padrão é semelhante à contagem de etapas de redução β quando restrita à redução de cabeças (que inclui estratégias de chamada por nome e chamada por valor).

Sobre a invariância do modelo de custo unitário para redução de cabeça por Beniamino Accattoli e Ugo Dal Lago. (WST2012, link para o processo )

O cálculo λ é um modelo computacional amplamente aceito de programas funcionais de ordem superior, mas não existe nenhum modelo de custo direto e universalmente aceito para ele. Como conseqüência, a dificuldade computacional de reduzir os termos-λ para sua forma normal é normalmente estudada pelo raciocínio em algoritmos de implementação concretos. Aqui, mostramos que, quando a redução de carga é a dinâmica subjacente, o modelo de custo unitário é de fato invariável. Isso melhora os resultados conhecidos, que lidam apenas com uma redução fraca (chamada por valor ou chamada por nome). A invariância é comprovada por meio de um cálculo linear de substituições explícitas, que permite decompor bem qualquer etapa de redução de carga no cálculo λ em etapas de substituição mais elementares, facilitando assim o raciocínio combinatório da redução de carga.

Stéphane Gimenez
fonte
λ