Os avaliadores ótimos são realmente ótimos?

10

O termo a seguir (usando índices bruijn):

BADTERM = λ((0 λλλλ((((3 λλ(((0 3) 4) (1 λλ0))) λλ(((0 4) 3) (1 0))) λ1) λλ1)) λλλ(2 (2 (2 (2 (2 (2 (2 (2 0)))))))))

Quando aplicado a um número de igreja, Navalia rapidamente a forma normal em vários avaliadores existentes, incluindo ingênuos . No entanto, se você codificar esse termo para redes de interação e avaliá-lo usando o Algoritmo Abstrato de Lamping, será necessário um número exponencial de reduções beta em relação a N. No Optlam, especificamente:

N   interactions(betas)     (BADTERM N)
1   129(72)                 λλλ(1 (2 (2 (2 (2 (2 (2 (2 0))))))))
2   437(205)                λλλ(2 (1 (2 (2 (2 (2 (2 (2 0))))))))
3   976(510)                λλλ(1 (1 (2 (2 (2 (2 (2 (2 0))))))))
4   1836(1080)              λλλ(2 (2 (1 (2 (2 (2 (2 (2 0))))))))
5   3448(2241)              λλλ(1 (2 (1 (2 (2 (2 (2 (2 0))))))))
6   6355(4537)              λλλ(2 (1 (1 (2 (2 (2 (2 (2 0))))))))
7   11888(9181)             λλλ(1 (1 (1 (2 (2 (2 (2 (2 0))))))))
8   22590(18388)            λλλ(2 (2 (2 (1 (2 (2 (2 (2 0))))))))
9   43833(36830)            λλλ(1 (2 (2 (1 (2 (2 (2 (2 0))))))))
10  85799(73666)            λλλ(2 (1 (2 (1 (2 (2 (2 (2 0))))))))
11  169287(147420)          λλλ(1 (1 (2 (1 (2 (2 (2 (2 0))))))))
12  335692(294885)          λλλ(2 (2 (1 (1 (2 (2 (2 (2 0))))))))
13  668091(589821)          λλλ(1 (2 (1 (1 (2 (2 (2 (2 0))))))))
14  1332241(1179619)        λλλ(2 (1 (1 (1 (2 (2 (2 (2 0))))))))
15  2659977(2359329)        λλλ(1 (1 (1 (1 (2 (2 (2 (2 0))))))))

Em avaliadores semelhantes, como o BOHM, são necessárias muito menos etapas beta, mas mais interações. Se os avaliadores ótimos são ótimos, como eles podem avaliar termos assintoticamente mais lentos que os avaliadores existentes?

Esse link tem uma explicação sobre a origem do termo, bem como uma implementação da mesma função que se comporta de maneira oposta, de maneira quase bizarra: deve ser executado em tempo exponencial - é executado em tempo exponencial na maioria dos avaliadores - ainda assim, ideal avaliadores normalizam em tempo linear!

MaiaVictor
fonte

Respostas:

5

Eficiência do optlam

Não estudei os detalhes do BADTERM nem da implementação do avaliador do optlam, mas acho bastante estranho que o optlam realize várias interações ß drasticamente diferentes de outro avaliador ideal como o BOHM. Esse número deve ser, por definição, basicamente o mesmo em um determinado termo. Você tem certeza da correção do núcleo do optlam?

Eficiência de avaliadores ótimos

Lembre-se de que a noção de otimização desses avaliadores é mais conhecida como otimização de Lévy, e não é ingênua, uma vez que uma estratégia de redução executando o número mínimo de ß-etapas não é computável. O que é minimizado, então, é o número de etapas de redução ß paralelas executadas em uma família inteira de redex, que é aproximadamente o conjunto obtido pelo fechamento simétrico e transitivo da relação que liga dois redexos quando um é copiado do outro. Em geral, não deveria surpreender ver discrepâncias entre o número de etapas ß e o restante das etapas de duplicação, pois sabemos que a maior parte da carga de normalização pode ser transferida da primeira para a segunda, como mostram Asperti, Coppola e Martini [1].

Também não deveria nos surpreender ver que o número total de interações necessárias para normalizar um termo com um avaliador ideal é menor do que com um avaliador comum, pois a observação empírica anterior já mostrava melhorias notáveis ​​no desempenho. Apesar disso, um salto de complexidade tão grande, do tempo exponencial para o tempo linear, é talvez o primeiro de seu tipo a ser descoberto. (Vou verificar isso.)

Por outro lado, os resultados teóricos sobre a eficiência da redução ótima (que é sua grande questão) ainda são poucos e ainda não gerais, pois estão limitados a redes de prova do tipo EAL (que é basicamente a mesma restrição de avaliador, se bem entendi), mas todos são levemente positivos, uma vez que, no pior dos casos, a complexidade da redução de compartilhamento é limitada pela ordinária por um fator constante [2,3].

Referências

  1. A. Asperti, P. Coppola e S. Martini, (Optimal) Duplicação não é recursiva elementar , Information and Computation, vol. 193, 2004.
  2. P. Baillot, P. Coppola e U. Dal Lago, Light logics e redução ótima: Completude e complexidade , Information and Computation, vol. 209, n. 2, pp. 118-142, 2011.
  3. S. Guerrini, T. Leventis e M. Solieri, Profundamente otimizados - complexidade e correção do compartilhamento da implementação de lógicas limitadas , DICE 2012, Tallin, Estônia, 2012.
Marco Solieri
fonte
Such a number must be, by definition, basically the same on a given termentão eu pensei. Isso me surpreendeu, pois o Optlam fornece o mesmo número de betas que o BOHM em muitos casos que testei. Em alguns casos, isso dá menos, devido à sua estratégia de chamada por necessidade. Alguém me disse que a redução sem o oráculo não é realmente ideal e agora não sei mais. Ao todo, estou profundamente confuso. Mas não, definitivamente não há prova de que o Optlam funcione corretamente. Estou pensando no resto do seu comentário - obrigado.
MaiaVictor
Além disso, encontrei muitos termos diferentes que se comportam exatamente como Badterm. Estou estudando mais a questão para encontrar termos mais simples que a replicem.
MaiaVictor
Uma espécie de estratégia paralela chamada por necessidade é padrão para avaliadores ótimos, incluindo o BOHM, pois é necessária para a própria otimização da Lévy. O oráculo não é estritamente necessário para reduzir otimamente quaisquer termos λ: termos estratificados, como os do tipo EAL, não precisam dele.
Marco Solieri
Oh, meu mal, então. De qualquer forma, apenas para garantir que eu entenda, quando você considera duplicação (não apenas betas), pode haver termos assintoticamente mais lentos para reduzir os avaliadores ideais, mesmo no caso do tipo EAL? Nesse caso, eu me pergunto por que é significativo para contar a poucos passos beta e se há realmente nenhum benefício no uso de redes de interação com a finalidade de redução λ-cálculo ...
MaiaVictor
11
Aha! Portanto, existem termos não tipificáveis ​​da EAL que podem ser reduzidos sem o oráculo? Presumi que, se o Optlam o reduzisse, era tipável pela EAL (já que não tenho um inferenciador do tipo EAL). Se não for esse o caso, tudo faz sentido agora. Como o subconjunto de termos tipificados pela EAL tem poder suficiente para expressar qualquer algoritmo de politempo como a classificação, acho que seria sensato tentar especificamente projetar termos tipáveis ​​pela EAL. Eu me pergunto como isso poderia ser feito na prática. Muito obrigado.
MaiaVictor