Usando cálculo lambda para derivar complexidade de tempo?

Existem benefícios no cálculo da complexidade de tempo de um algoritmo usando o cálculo lambda? Ou existe outro sistema projetado para esse fim?

Todas as referências serão apreciadas.

Ohad está certo sobre os problemas que o cálculo lambda enfrenta como base para falar sobre classes de complexidade. Muito trabalho foi feito para caracterizar a complexidade da redutibilidade no cálculo lambda, particularmente em torno do trabalho sobre reduções rotuladas e ótimas da tese de doutorado de Lèvy. De um modo geral, bons modelos de custo para o cálculo lambda não devem atribuir um peso constante a todas as reduções beta: intuitivamente, substituir um subtermo grande em muitos locais com escopo diferente deve custar mais do que contratar um pequeno redex K, e se alguém quiser uma certa quantia invariância de custo sob diferentes estratégias de reescrita, isso se torna essencial.

Dois links:

1. Lawall e Mairson, 1996, Optimalidade e ineficiência: o que não é um modelo de custo do cálculo lambda? (.ps.gz) - Pesquisa seminal de questões relacionadas à escolha do modelo de custo e por que muitas idéias plausíveis não funcionam.
2. Dal Lago & Martini, 2008, O fraco cálculo lambda como uma máquina razoável - Oferece um modelo de custo para o cálculo lambda de valor por valor, juntamente com uma boa discussão da literatura.

$\lambda$$\lambda$

Para algo mais próximo da sua pergunta, existe um projeto atual que desenvolve e estuda um sistema de tipos (uma linguagem de programação funcional) que pela análise estática pode determinar os limites de tempo de execução (polinomial) dos programas (além de outros recursos usados ​​por programas). Portanto, de certa forma, isso pode sugerir que pode haver alguma vantagem no uso da programação funcional para analisar a complexidade do tempo de execução. A página inicial do projeto está aqui .

Um artigo possivelmente representativo desse projeto é: Jan Hoffmann, Martin Hofmann. Análise de recursos amortizados com potencial polinomial - uma inferência estática de limites polinomiais para programas funcionais. Em Anais do 19º Simpósio Europeu de Programação (ESOP'10). ligação

$\lambda$$\lambda$

$\lambda$

http://arxiv.org/abs/1405.3311

Existe uma linha de trabalho muito interessante baseada na lógica linear, chamada teoria da complexidade implícita, que caracteriza várias classes de complexidade ao impor várias disciplinas de tipos no cálculo lambda. No IIRC, esse trabalho começou quando Bellantoni e Cook e Leivant descobriram como usar o sistema de tipos para ligar a recursão primitiva para capturar várias classes de complexidade.

Em geral, a atração de trabalhar com os cálculos lambda é que às vezes é possível encontrar caracterizações mais extensionais (isto é, mais matematicamente tratáveis) de várias características intensionais que dão poder a modelos como máquinas de Turing. Por exemplo, uma diferença entre as máquinas de Turing e o cálculo lambda puro é que, uma vez que Turing recebe códigos de programas, um cliente pode implementar manualmente tempos limite, para implementar o encaixe - e, portanto, pode calcular paralelo ou. No entanto, os tempos limites também podem ser modelados metricamente, e Escardo conjeturou (não sei seu status) que os modelos de espaço métrico do cálculo lambda são totalmente abstratos para tempos limite PCF +. Os espaços métricos são objetos matemáticos muito bem estudados, e é muito bom poder fazer uso desse corpo de teoria.

No entanto, a dificuldade de usar o cálculo lambda é que ele o força a enfrentar fenômenos de ordem superior desde o portão inicial. Isso pode ser muito sutil, uma vez que a tese de Church-Turing falha no tipo superior - os modelos naturais de computação diferem no tipo superior, pois diferem no que você tem permissão para fazer com as representações dos cálculos. (Paralelamente - ou é um exemplo simples desse fenômeno, pois exibe uma diferença entre LC e TMs.) Além disso, não há sequer uma inclusão estrita entre os diferentes modelos, pois a contravariância do espaço de função significa um poder mais expressivo em uma ordem implica poder menos expressivo, uma ordem mais alta.

Até onde eu sei, o cálculo lambda é inadequado para esse propósito, pois é difícil formular a noção de complexidade de tempo / espaço no cálculo lambda.

O que é 1 unidade de complexidade de tempo? Uma redução beta? E as unidades de complexidade do espaço? O comprimento da corda?

O cálculo Lambda é mais adequado para manipulação abstrata de algoritmos, pois é muito mais facilmente composível do que as máquinas de Turing.

Você também pode procurar cálculos de substituições explícitas que dividem a substituição de meta-nível do cálculo lambda em uma série de etapas explícitas de redução. Isso toca no ponto de Charles de que todas as substituições não devem ser consideradas iguais ao considerar a complexidade do tempo.

Veja Nils Anders Danielsson, Análise de complexidade de tempo semiformal leve para estruturas de dados puramente funcionais, que é implementada como uma biblioteca na Agda. As citações dadas no artigo também parecem muito promissoras.

Um argumento importante para mim é que é apropriado / útil / razoável / semi-automatizável derivar a complexidade de tempo dos algoritmos no cálculo lambda simplesmente digitado, especialmente se esses algoritmos são facilmente expressáveis ​​nele (ou seja, puramente funcionais) e muito especialmente se esses algoritmos fazem uso essencial de, por exemplo, semântica de chamada por nome. Junto com isso, é provavelmente o ponto óbvio de que não se calcula a complexidade apenas "no cálculo lambda", mas no cálculo lambda sob uma determinada estratégia de avaliação.