Newtonsan on Nostr: Na Ciência da Computação, há vários candidatos fortes, e um deles é ...

Na Ciência da Computação, há vários candidatos fortes, e um deles é particularmente próximo da AdS/CFT em espírito: uma equivalência profunda entre modelos aparentemente diferentes.

Os principais são:

1. Correspondência de Curry–Howard (o candidato mais forte)



Como a Ciência da Computação teórica nasceu em grande parte da lógica matemática, a Correspondência de Curry–Howard é igualmente fundamental aqui.

Ela identifica:

proposições ↔ tipos;

provas ↔ programas;

normalização ↔ execução.


Essa correspondência fundamenta linguagens funcionais, compiladores, verificação formal e assistentes de prova.

É uma verdadeira ponte entre lógica e computação.

2. Tese de Church–Turing



Proposta independentemente por Alonzo Church e Alan Turing.

Ela afirma que todos os modelos "razoáveis" de computação possuem o mesmo poder computacional.

Por exemplo:

máquinas de Turing;

λ-cálculo;

funções recursivas;

sistemas de Post.


Todos calculam exatamente as mesmas funções.

Essa é uma das maiores unificações da computação.

Curiosamente, ela não é um teorema, mas uma tese, porque o conceito informal de "algoritmo" não possui definição matemática independente.

3. Equivalência entre modelos de computação



Ao longo do século XX descobriu-se que diversos modelos muito diferentes são equivalentes:

Máquina de Turing;

λ-cálculo;

combinadores de Schönfinkel;

autômatos adequados;

linguagens funcionais.


Essas equivalências são teoremas profundos.

4. Classes de complexidade



Resultados como

\text{IP}=\text{PSPACE}

ou

\text{MIP}^*=\text{RE}

mostram equivalências completamente inesperadas entre modelos computacionais distintos.

Por exemplo, o teorema MIP = RE*, provado em 2020 por uma equipe que incluiu Thomas Vidick, Anand Natarajan, John Wright, Zhengfeng Ji e Henry Yuen, conectou sistemas interativos com entrelaçamento quântico à teoria da computabilidade de uma forma que surpreendeu especialistas.

5. Isomorfismo de programas



Na teoria das categorias e na semântica denotacional, diferentes programas podem ser demonstrados equivalentes porque representam o mesmo morfismo ou a mesma função matemática.

Essa ideia permeia a otimização de compiladores e a verificação formal.

Qual é o mais parecido com a AdS/CFT?

Depende do aspecto que você deseja enfatizar:

Se o foco é uma equivalência estrutural entre dois domínios inteiros, a Correspondência de Curry–Howard é a melhor comparação.

Se o foco é uma grande unificação de modelos diferentes, a Tese de Church–Turing ocupa esse papel.

Se o foco é um resultado recente que mudou profundamente a teoria da computação, MIP = RE* é um dos melhores exemplos.


A comparação geral fica assim:

Área Ideia mais profunda

Física AdS/CFT
Matemática Programa de Langlands
Lógica Correspondência de Curry–Howard
Ciência da Computação Correspondência de Curry–Howard / Tese de Church–Turing


Há um detalhe interessante. A AdS/CFT relaciona duas descrições da mesma realidade física. A Correspondência de Curry–Howard relaciona duas descrições da mesma estrutura formal: um objeto pode ser visto tanto como uma prova lógica quanto como um programa executável. Essa mudança de perspectiva foi tão influente que hoje ela sustenta áreas inteiras da ciência da computação, da teoria das linguagens de programação à verificação formal e aos assistentes de prova. É por isso que muitos pesquisadores a consideram uma das ideias mais profundas já descobertas na disciplina.