Eu sei que a complexidade da maioria das variedades de cálculos lambda digitados sem a primitiva combinadora Y é limitada, ou seja, somente funções de complexidade limitada podem ser expressas, com o limite se tornando maior à medida que a expressividade do sistema de tipos cresce. Lembro que, por exemplo, o Cálculo de Construções pode expressar no máximo uma complexidade duplamente exponencial.
Minha pergunta é se o cálculo lambda digitado pode expressar todos os algoritmos abaixo de um determinado limite de complexidade ou apenas alguns? Por exemplo, existem algoritmos de tempo exponencial não expressáveis por qualquer formalismo no Cubo Lambda? Qual é a "forma" do espaço de complexidade que é completamente coberto por diferentes vértices do Cubo?
Respostas:
Vou dar uma resposta parcial, espero que outros preencham os espaços em branco.
Em digitado -calculi, pode-se dar um tipo de representações usuais de dados ( N um t para Church (unários) inteiros, S t r para cadeias binárias, B o o l para Booleans) e saber o que é a complexidade das funções / problemas representáveis / decidíveis por termos digitados. Conheço uma resposta precisa apenas em alguns casos e, no caso de digitação simples, depende da convenção usada ao definir "representável / decidível". De qualquer forma, não conheço nenhum caso em que exista um limite superior duplamente exponencial.λ N a t S t r B o o l
Primeiro, uma breve recapitulação do Cubo Lambda. Seus 8 cálculos são obtidos ativando ou desativando os 3 tipos de dependências a seguir no calccul simplesmente digitado (STLC):λ
(A dependência de termos em termos está sempre lá).
Adicionando polimorfismo yields Sistema F. Aqui, você pode digitar os números inteiros igreja com e da mesma forma para cadeias binárias e booleanos. Girard provou que o Sistema F termos de tipo N uma t → N uma t representam exatamente as funções numéricas cuja totalidade é demonstrável em segunda ordem aritmética de Peano. Isso é praticamente a matemática do dia-a-dia (embora sem qualquer forma de escolha), então a classe é enorme, a função Ackermann é uma espécie de micróbio minúsculo nela, muito menos a função 2 2N um t : = ∀X. ( X→ X) → X→ X N a t → N a t . Não conheço nenhuma função numérica "natural" que não possa ser representada no Sistema F. Os exemplos geralmente são criados por diagonalização ou codificando a consistência do PA de segunda ordem ou outros truques autorreferenciais (como decidir aigualdadeβno Sistema F em si). Obviamente, no Sistema F, você pode converter entre números inteiros unáriosNate sua representação bináriaStr, e depois testar, por exemplo, se o primeiro bit é 1, de modo que a classe de problemas decidíveis (por termos do tipoStr→Bool) é igualmente enorme.22n β N a t S t r S t r → B o o l
Os outros três cálculos do Cubo Lambda que incluem polimorfismo são, portanto, pelo menos tão expressivos quanto o Sistema F. Estes incluem o Sistema F ω (polimorfismo + ordem superior), que pode expressar exatamente as funções provadamente totais em PA de ordem superior e o Cálculo de Construções (CoC), que é o cálculo mais expressivo do Cubo (todas as dependências estão ativadas). Não conheço uma caracterização da expressividade do CoC em termos de teorias aritméticas ou de conjuntos, mas deve ser bem assustador :-)ω
Sou muito mais ignorante em relação aos cálculos obtidos ao ativar apenas tipos dependentes (essencialmente a teoria dos tipos de Martin-Löf sem igualdade e números naturais), tipos de ordem superior ou ambos. Nesses cálculos, os tipos são poderosos, mas os termos não podem acessar esse poder, então não sei o que você recebe. Computacionalmente, não acho que você tenha muito mais expressividade do que com tipos simples, mas posso estar enganado.
Então, ficamos com o STLC. Até onde eu sei, esse é o único cálculo do Cubo com limites superiores de complexidade interessante (ou seja, não monstruosamente grande). Há uma pergunta não respondida sobre isso no TCS.SE e, de fato, a situação é um pouco sutil.
Primeiro, se você fixa um átomo e define N a t : = ( X → X ) → X → X , há o resultado de Schwichtenberg (eu sei que há uma tradução em inglês desse artigo em algum lugar da Web, mas não consigo encontrá-lo now), que informa que as funções do tipo N a t → N a t são exatamente os polinômios estendidos (com if-then-else). Se você permitir alguma "folga", ou seja, permitir que o parâmetro X seja instanciado à vontade e considerar os termos do tipo N a t [X N um t : = (X→ X) → X→X N a t → Na t X com um arbitrária, muito mais pode ser representada. Por exemplo, qualquer torre de exponenciais (para que você possa ir muito além de duplamente exponencial), bem como a função predecessora, mas ainda sem subtração (se você considerar funções binárias e tentar digitá-las com N a t [ A ] → N a t [ A ′ ] → N a t ). Portanto, a classe de funções numéricas representáveis no STLC é um pouco estranha, é um subconjunto estrito das funções elementares, mas não corresponde a nada conhecido.N a t [A]→ N a t UMA N a t [A]→ N a t [ A′] → N um t
Em aparente contradição com o exposto, há este papel por Mairson que mostra como codificar a função de transição de um arbitrária máquina de Turing , a partir do qual se obter um termo do tipo N uma t [ A ] → B O O G (por algum tipo A dependendo de M ) que, dado um número inteiro da Igreja n como entrada, simula a execução de M iniciando em uma configuração inicial fixa para um número de etapas no formato 2 2 ⋮ 2 n ,M N a t [A]→ B o o l UMA M n M
De fato, o STLC é extremamente fraco no que pode decidir "uniformemente". Chamemos a classe de linguagens decidível por termos simplesmente digitadas do tipo S t r [ A ] → B o o l para alguns A (como acima, você permitir "folga" arbitrária na digitação). Até onde eu sei, falta uma caracterização precisa de C S T. No entanto, sabemos que C S T ⊊ L I N T I M ECST Str[A]→Bool A CST CST⊊LINTIME (tempo linear determinístico). Tanto a contenção quanto o fato de ser rigoroso podem ser mostrados por argumentos semânticos muito puros (usando a semântica denotacional padrão do STLC na categoria de conjuntos finitos). O primeiro foi mostrado recentemente por Terui . Este último é essencialmente uma reformulação dos resultados antigos de Statman. Um exemplo de problema em é MAJORITY (dada uma cadeia binária, diga se ela contém estritamente mais 1s que 0s).LINTIME∖CST
(Muito) Mais tarde add-on: Eu só descobri que a classe eu chamo acima realmente não têm uma caracterização precisa, que é, aliás, extremamente simples. Em este belo papel 1996 , Hillebrand e Kanellakis provar, entre outras coisas, queCST
(Este é o Teorema 3.4 em seu artigo).
(Aliás, compartilhei minha surpresa nesta resposta a uma pergunta do MO sobre "teoremas desconhecidos").
fonte
Resposta a uma pergunta que Damiano levantou em sua excelente resposta:
Não sei qual é a força do cálculo impredicativo das construções, se você adicionar tipos indutivos e grandes eliminações.
fonte
Vou tentar complementar a excelente resposta de Damiano.
Em geral, essa é uma grande avenida de pesquisa, por isso vou me referir a uma das minhas respostas anteriores .
fonte