Joshua Tauber
Conclusão Semana 5
Minha área de pesquisa é em métodos formais de verificação da computação
distribuída. Uma das principais metas do nosso grupo de pesquisa (e, em
p a r t i c u l a r , d o m e u p r o g r a m a d e p e s qu i s a ) é a u m e n t a r a a u t o m a t i z a ç ã o d o
raciocínio sobre a exatidão dos projetos de sistemas distribuídos e sua
implementação.
Uma das principais ferramentas utilizadas é o Larch Prover (LP). LP é um
assistente de provas automatizado. Na taxonomia de Donald MacKenzie, LP é um
provador interativo que gera provas não-humanas. Gerar uma "prova" com o LP
consiste em um processo interativo muito parecido com o que Boyer descreveu.
Um ser humano registra uma hipótese que o LP, em seguida, tenta provar. O LP
a p l i c a r á u m a o u m a i s d e s u a s r e g r a s d is p o n í v e i s p a r a g e r a r ( p r o v a v e l m e n t e d e
forma mais simples) submetas para provar. Muito provavelmente, o LP ficará
preso em algum lugar no processo e necessitará de orientação para continuar.
Por exemplo, o usuário precisaria sugerir um valor para instanciar em um
quantificador existencial, a fim de descarregar parte de uma análise de casos. Ao
término de uma interação bem-sucedida, o resultado é uma afirmação por parte
do LP de que a hipótese desejada foi provada.
O ponto interessante é examinar o que restou deste processo. O usuário do LP
a g o r a t e m u m " s c r i p t " p a r a p r o v a r o t e o r e m a . S cript é u m a s é r i e d e c o m a n d o s
que o usuário insere para conseguir que o LP concorde que a hipótese é
v e r d a d e i r a . A s e n t r a d a s n o script p o d e m i n c l u i r a l g u m a s e t a p a s ó b v i a s q u e
qualquer matemático reconhecerá (pelo menos logo que eles sejam
decodificados), como: "iniciar utilização por A" ou "instanciar B como D+E". Por
o u t r o l a d o , o script p o d e i n c l u i r c o m a n d o s q u e p e d e m a o L P q u e e x e c u t e g r a n d e s
operações, como: "utilizar pares críticos" (uma operação relacionada à
r e s o l u ç ã o ) . N o e n t a n t o , o m a i s i n t e r e s s a n t e é o_que_não_está_lá .
O_que_não_está_lá é o t e x t o r e a l d o q u e s e r i a r e c o n h e c i d o c o m o u m a p r o v a
f o r m a l . O u s e j a , o script d e p r o v a consiste_apenas_em d i c a s ( c o m a n d o s ) a s e r e m
dadas ao LP quando ele ficar preso.
Na verdade, alguém poderia pedir ao LP que listasse a maior parte das etapas
intermediárias em detalhes minuciosos. Na prática, porém, ninguém o faz. Por
que? Por três motivos:
P r i m e i r o , o s d e t a l h e s d a s p r o v a s f o r m a is n ã o s ã o m u i t o i n t e r e s s a n t e s . A s e t a p a s
exatas não cumprem a função explicativa. Esta é a mesma razão pela qual
nenhum texto completo de provas formais foi publicado. Os matemáticos querem
q u e a s etapas_formais_possam s e r r e a l i z a d a s , m a s e l e s n ã o s e p r e o c u p a m c o m o
que elas são de fato.
Segundo, em parte intencionalmente, o LP não tende a pular as "grandes etapas"
sozinho. Assim, as partes interessantes da prova (sua estrutura, por exemplo)
t e n d e a a c a b a r n o script d e p r o v a . S e v o c ê t i v e r s o r t e , a s p a r t e s i n t e r e s s a n t e s
não serão trocadas por detalhes irrelevantes.
Terceiro, nós confiamos no LP para fazer o trabalho pesado de forma perfeita. O
LP pode não ser muito "inteligente" e provavelmente não irá até o fim de uma
p r o v a s o z i n h o . N o e n t a n t o , c o n f i a m o s n a e xa t i d ã o d a s e t a p a s q u e e l e v e r i f i c a .
Sob vários aspectos, este terceiro ponto diferencia toda a área de pesquisa dos
provadores de teorema e assistentes automatizados de prova de teorema do tipo
d e p r o v a a u x i l i a d a p o r c o m p u t a d o r r e al i z a d a p o r A p p e l e H a k e n . N a p r o v a d o
teorema das quatro cores, Appel e Haken utilizaram um programa de computação
específico (e se meu antigo consultor, David Gries, for confiável, pobremente
estruturado) para verificar certos casos de prova. O próprio fato de que este
programa foi escrito como parte da prova torna a verificação do programa parte
da verificação da prova.
E m c o n t r a p a r t i d a , o s p r o v a d o r e s d e t e o r e m a s ã o u s a d o s , e x a mi n a d o s , e s t e n d i d o s
e depurados repetidamente por alguns anos. O próprio fato de que uma
comunidade de usuários existe por causa de uma determinada ferramenta
p r o p o r c i o n a a s e g u r a n ç a d e q u e e l a r e al i z a s u a s t a r e f a s d e s i g n a d a s q u a n d o
s o l i c i t a d a s . D e c e r t a f o r m a , a p r ó p r i a e xa t i d ã o d o p r o v e d o r d e t e o r e m a é u m a
hipótese distinta aos teoremas onde ela é usada para verificação. E este acervo
de evidências da exatidão de um provador de teorema se constitui em prova no
sentido matemático? Talvez não. Mas justamente por isso, nem a crítica de um
colega nem a publicação de uma suposta "prova" constituem prova definitiva de
que a publicação é, na verdade, correta.
D e c e r t a f o r m a , o s scripts d e p r o v a d o L P s ã o m a i s f á c e i s d e s e v e r i f i c a r d o q u e
u m g r a n d e t r a t a d o m a t e m á t i c o . P o r e x e mp l o , d e s c o n f i o q u e s e j a m a i s f á c i l
escrever meu próprio assistente de prova de teorema para verificar novamente
u m script d e L P d o q u e e u v e r i f i c a r a s e t a p a s n a p r o v a d e A n d r e w W i l e s s o b r e a
hipótese de Taniyama-Shimura.
O s scripts d e p r o v a s d o L P c u m p r e m a s f u n ç õ e s e x p l a n a t ó r i a s ? T a l v e z . A o l o n g o
do tempo, nosso grupo de pesquisas desenvolveu um acervo de tecnologia de
provas no sentido matemático. Como resultado, as provas sobre o sistema
distribuído apresentadas pelo nosso grupo seguem uma forma muito estilizada.
(Esta forma estilizada é o que levou à iniciativa para a automatização das
t é c n i c a s d e p r o v a . ) P o r i s s o , a p a r t e d a p r o v a q u e t e r m i n a n o script d e p r o v a s d o
LP tende a ser a parte que torna esta determinada prova diferente da anterior.
A s s i m , o script d e p r o v a s n a v e r d a d e d e s t a c a a s p a r t e s i n t e r e s s a n t e s d a p r o v a .
No entanto, eu discutiria que nem todas as provas precisam ser explanatórias.
A l g u m a s t ê m , n a v e r d a d e , f i n a l i d a d e s p r á ti c a s . O u s e j a , p r o v a r q u e u m s i s t e m a é
correto só é interessante até que alguém se preocupe com isso e que mais tarde
não haja nenhuma implicação adicional na construção de estruturas matemáticas
. Ne s t e s c a s o s , o s scripts d e p r o v a s s e t o r n a m m u i t o ú t e i s . E m p a r t i c u l a r , q u a n d o
um projeto de sistema é modificado, muitas vezes é mais fácil verificar o sistema
novamente usando o LP a refazer à mão uma prova informal que talvez fosse
extremamente trabalhosa.