A incomputabilidade da complexidade de Kolmogorov segue o Teorema de Ponto Fixo de Lawvere?

17

Muitos teoremas e "paradoxos" - diagonalização de Cantor, indecidibilidade de hatling, indeciabilidade da complexidade de Kolmogorov, incompletude de Gödel, incompletude de Chaitin, incompletude de Chaitin, paradoxo de Russell etc. - todos têm essencialmente a mesma prova de diagonalização (observe que isso é mais específico do que pode ser). tudo isso é provado pela diagonalização; parece que todos esses teoremas realmente usam a mesma diagonalização; para mais detalhes, por exemplo , Yanofsky , ou para uma descrição muito mais breve e menos formalizada, minha resposta a essa pergunta ).

Em um comentário sobre a questão acima mencionada, Sasho Nikolov apontou que a maioria desses casos eram especiais do Teorema de Ponto Fixo de Lawvere . Se todos fossem casos especiais, essa seria uma boa maneira de capturar a idéia acima: realmente haveria um resultado com uma prova (de Lawvere), da qual todas as anteriores foram seguidas como corolários diretos.

Agora, para a incompletude e indecidibilidade de Gödel do problema da parada e de seus amigos, é sabido que eles seguem o Teorema de Ponto Fixo de Lawvere (ver, por exemplo, aqui , aqui ou Yanofsky ). Mas não vejo imediatamente como fazer isso pela indecidibilidade da complexidade de Kolmogorov, apesar do fato de que a prova subjacente é de alguma forma "a mesma". Então:

A indecidibilidade da complexidade de Kolmogorov é um corolário rápido - que não requer diagonalização adicional - do Teorema de Ponto Fixo de Lawvere?

lo.logic computability ct.category-theory kolmogorov-complexity Joshua Grochow
fonte
2
Devo dizer que tudo o que soube sobre esse tópico aprendi neste post de Andrej Bauer: math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem
Sasho Nikolov
11
@MaxNew: Let ser uma função computável, calculado por alguns TM M . Deixe- M k ser a seguinte TM: na entrada vazia, ele começa a passar por cordas um de cada vez até encontrar um x com f ( x ) ≥ | x | > ke saída x . Note-se que | M k | ≤ log 2 ( k ) + c para alguns c, dependendo apenas de | M | . Então, para qualquer k tal quefMMkxf(x)≥|x|>kx|Mk|≤log2⁡(k)+cc|M|k(qualquer k suficientemente grandeserve), ou não existe x (nesse caso, f ≠ C ) ou M k gera algum x tal que f ( x ) ≥ | x | > k (por construção), mas o fato de que M k produz x implica que C ( x ) ≤ | M k | < k , então fk>|Mk|kxf≠CMkxf(x)≥|x|>kMkxC(x)≤|Mk|<k . f(x)≠C(x)
Joshua Grochow 23/03
2
@NealYoung: Semelhante, mas esses não respondem completamente à minha pergunta. Reduzir do problema de interrupção está levando o HALT a ser a "fonte" de desconformidade e, em seguida, o uso de reduções. Mas (por exemplo) a prova que dei nos comentários acima mostra que você também pode considerar a complexidade K como a "fonte de incomputabilidade", mas por uma prova muito semelhante à do HALT. Essa prova semelhante pode realmente ser mostrada a mesma em algum sentido técnico? (Nesse caso, mostrando que todos são exemplos do Teorema de Lawvere, o que me parece mais forte do que muitos tipos de redução.) É disso que eu realmente busco.
Joshua Grochow 23/03
11
@NealYoung: Sim, ele generaliza o teorema do ponto fixo de Roger. Mas se você pensar nisso apenas como o Teorema de Roger, estará perdendo o ponto; o ponto é que o de Lawvere é geral o suficiente para capturar a estratégia de provas de muitas provas diferentes, além da de Roger. O artigo de Yonofsky vinculado à pergunta pretende ser uma exposição "livre de categoria" do Teorema de Lawvere, amigável para pessoas para quem a teoria da categoria de Lawvere pode ser intimidadora.
Joshua Grochow 23/03
3
Veja também cstheory.stackexchange.com/a/2830
András Salamon

Respostas:

14

EDIT: Adicionando a ressalva de que o teorema do ponto fixo de Roger pode não ser um caso especial do de Lawvere.

Aqui está uma prova que pode ser "próxima" ... Ela usa o teorema do ponto fixo de Roger em vez do teorema de Lawvere. (Veja a seção de comentários abaixo para mais discussões.)

Seja a complexidade de Kolmogorov da cadeia x . K(x)x

lema . não é computávelK .

Prova .

  1. Suponha, por contradição, que é computável.K

  2. Defina como o comprimento mínimo de codificação de qualquer Máquina de Turing M com L ( M ) = { x } . K′(x)ML(M)={x}

  3. Existe uma constante tal que | K ( x ) - K ′ ( x ) | ≤ c para todas as cadeias x .c|K(x)−K′(x)|≤cx

  4. Função de definir tal que f ( ⟨ M ⟩ ) = ⟨ M ' ⟩ onde L ( M ' ) = { x } tal que x é a string mínimo tal que K ( x ) > | ⟨ M ⟩ | + c . ff(⟨M⟩)=⟨M′⟩L(M′)={x}xK(x)>|⟨M⟩|+c

  5. Como é computável, o mesmo é f .Kf

  6. Pelo teorema de ponto fixo de Roger , tem um ponto fixo, isto é, existe uma máquina de Turing M 0 de tal modo que L ( H 0 ) = L ( M ' 0 ) onde ⟨ H ' 0 ⟩ = f ( ⟨ H 0 ⟩ ) .fM0L(M0)=L(M0′)⟨M0′⟩=f(⟨M0⟩)

  7. Pela definição de na linha 4, temos L ( M 0 ) = { x } tal que K ( x ) > | ⟨ M 0 ⟩ | + c .fL(M0)={x}K(x)>|⟨M0⟩|+c

  8. As linhas 3 e 7 implicam . K′(x)>|⟨M0⟩|

  9. Mas pela definição de na linha 2, K ′ ( x ) ≤ | ⟨ M 0 ⟩ | , contradizendo a linha 8.K′K′(x)≤|⟨M0⟩|

Neal Young
fonte
4
Até onde eu sei, o teorema do ponto fixo de Roger não é uma instância do teorema do ponto fixo de Lawvere. É uma variante, no entanto, porque nos topos efetivos se lê da seguinte maneira: se é uma rejeição com o mesmo valor , A possui a propriedade de ponto fixo. (Teorema de Lawvere nos topos eficazes é: se f : B → A B é um surjection então A tem a propriedade de ponto fixo.)f:N⇉ANAf:B→ABA
Andrej Bauer
Acima da minha classificação salarial, @AndrejBauer - não conheço a teoria das categorias. Tentei ler isso e sua resposta aqui . Ainda não entendi. Você pode me dizer, no seu comentário acima, sobre o teorema de Rogers, o que você considera para a função (com o tipo f : N → → A N ) e o que é A ? Ou talvez sugira um tutorial apropriado? ff:N→→UMANUMA
Neal Young
4
Slides 45 e 46 em math.andrej.com/wp-content/uploads/2007/05/syncomp-mfps23.pdf (a boa notícia é que agora tenho um plano definido e um prazo para escrever um extenso artigo sobre computação sintética )
Andrej Bauer 26/03