Reprodução livre, em Português Brasileiro, do texto original
de Donald Mackenzie para fins de estudo, sem vantagens pecuniárias
envolvidas.
Todos os direitos preservados.
Free reproduction, in Brazilian Portuguese,
of Donald Mackenzie’s original text for study purposes.
No pecuniary advantagens involved. Copyrights preserved.
Donald Mackenzie
(tradução de Fernando Manso)
Sistemas computacionais têm sido um objeto de considerável interesse para os cientistas sociais desde os anos 60. Sua difusão, seus prováveis efeitos sobre as organizações, sobre os níveis de emprego e sobre a sociedade de uma forma geral, a evolução da indústria computacional, são, dentre outros, tópicos que tem recebido considerável atenção. No entanto, sistemas computacionais como entidades matemáticas têm permanecido em grande medida assunto de especialistas técnicos. Neste artigo, eu tento restabelecer esse equilíbrio argumentando que sistemas computacionais oferecem estudos de caso interessantes e contra-intuitivos para a sociologia da matemática.
O artigo discute dois aspectos diferentes de sistemas computacionais enquanto entidades matemáticas. O primeiro é o computador (e as calculadoras digitais avançadas) enquanto uma ferramenta aritmética. A intuição poderia sugerir que a aritmética feita por computador ou por calculadoras fosse totalmente não problemática. A aritmética, afinal de contas, é o próprio paradigma do conhecimento seguro e consensual, e certamente, a calculadora ou o computador simplesmente eliminam o tédio e a propensão a erro da aritmética efetuada por seres humanos. No entanto tal não é o caso. Não apenas é necessária uma considerável habilidade, usualmente desconsiderada, para efetuar aritmética confiavelmente mesmo em simples calculadoras[1]; além disso, tem havido disputas significativas com relação a natureza da aritmética a ser implementada, pelo menos quando os números a serem trabalhados não são inteiros. Diferentes aritméticas computacionais têm sido propostas, e a mais próxima aproximação de uma aritmética computacional consensual, o padrão do Instituto dos Engenheiros Elétricos e Eletrônicos para a aritmética de ponto flutuante, teve de ser negociado e não deduzido a partir da aritmética humana existente.
O segundo aspecto de sistemas computacionais que será discutido aqui é a prova matemática da exatidão de programas ou de projetos de hardware. Na medida em que sistemas computacionais são, cada vez mais, usados em situações onde a segurança nacional e vidas humanas dependem deles, tem havido uma demanda crescente por tais provas matemáticas no lugar de, ou em acréscimo aos, testes empíricos. Isto tem interesse do ponto de vista da sociologia do conhecimento porque desloca a “prova” do mundo dos matemáticos e lógicos para o mundo dos engenheiros, corporações e advogados.
Embora a prova matemática seja buscada exatamente por conta da certeza que ela usualmente carrega, a construção de provas da exatidão de sistemas computacionais, novamente, revela-se não ser uma simples “aplicação” da matemática. Ela envolve negociar o que consiste uma prova. Em 1987, Pelaez, Fleck e eu predissemos que a demanda por provas da exatidão de sistemas computacionais levaria inevitavelmente a que os tribunais regulamentem sobre a natureza da prova matemática. Este capítulo desenvolve a discussão do capítulo precedente sobre a controvérsia que quase já confirmou essa predição; ele também explora questões mais gerais sobre a “sociologia da prova” no contexto de sistemas computacionais.
A aritmética humana é consensual nas sociedades industriais avançadas. Tipicamente, não há discordâncias sobre o resultado correto de qualquer cálculo. Por exemplo, até onde eu sei, nunca houve disputas científicas nas quais as partes tivessem discordado ao nível da aritmética. Além disso há certas leis “ideais” que, todos concordamos, mantêm-se independentemente de qualquer cálculo particular. Por exemplo, nós concordamos que a adição e a multiplicação dos números reais devem ser comutativa e associativa, isto é:
a + b = b + a
(a + b) + c = a + (b + c)
a x b = b x a
(a x b) x c = a x (b x c)
quaisquer que sejam os valores de a, b, e c.
Na verdade esse status consensual da aritmética tem sido tomado como uma indicação de um limite auto-evidente da sociologia do conhecimento. Poderia parecer que implementar a aritmética numa calculadora ou num computador fosse simples e direto. No entanto esse não é o caso.
As dificuldades são maiores na forma de aritmética usada no tipo de cálculo tipicamente encontrado em trabalhos científicos: a aritmética de ponto flutuante, que é o análogo computacional da conhecida “notação científica” para expressar números. Nesta notação, um número é expresso em três partes: um sinal positivo ou negativo (o primeiro usualmente implícito); um conjunto de dígitos decimais (o significando ou mantissa), incluindo o ponto decimal; e um segundo conjunto de dígitos (expoente), que é uma potência de 10. Assim 1.245.000 poderia ser expresso em “notação científica” como +1,245 x 106, e - 0.0006734 como - 6,734 x 10-4. A vantagem da notação científica é que permitindo o ponto decimal “flutuar” desta forma leva a um formato mais econômico e mais facilmente manipulável do que a representação padrão, onde o ponto decimal é “fixo” em sua posição.
A aritmética computacional de ponto flutuante mantém essa flexibilidade e é bastante similar, exceto nos seguintes aspectos:
A representação decimal (base 10) é hoje incomum; as representações hexadecimal (base 16) e binária (base 2) são mais comuns. Uma vez que o episódio que quero discutir se refere a aritmética binária, vamos nos concentrar nela. Cada dígito é 1 ou 0: o decimal 3, por exemplo, é expresso como 11, o decimal 4 como 100 e assim por diante. O expoente é uma potência de 2, e o equivalente do ponto decimal é conhecido como ponto binário. O sinal, similarmente, é expresso com um dígito binário, tipicamente 0 para números positivos e 1 para números negativos.
Uma importante decisão tem de ser tomada a respeito do número de dígitos binários (bits) no significando e no expoente. Na aritmética a ser discutida o formato básico tem um dígito binário para expressar o sinal, oito bits para expressar o expoente e 23 para a mantissa, totalizando 32 bits. O número total de bits (algumas vezes chamado de “comprimento da palavra”) é de considerável importância, uma vez que a maioria dos computadores modernos procura processar todos os bits que constituem um número em paralelo e não um após o outro. Quanto maior o número de bits a ser processado simultaneamente, maior a complexidade do hardware necessário.
Qualquer sistema de ponto flutuante, em princípio, permite múltiplas representações do mesmo número. Por exemplo, -0.0006734 poderia ser expresso como –67.34 x 10-5 assim como também –6.734 x 10-4 ou -0.6734 x 10-3. No entanto, sistemas computacionais de ponto flutuante, tipicamente, empregam uma representação “normal” única de cada número não nulo. Nesta representação, há sempre um bit não nulo a esquerda do ponto binário. Na medida em que este bit tem de ser 1, ele não precisa ser guardado explicitamente, e apenas a parte do significando a direita do ponto binário (conhecido por razões óbvias como a fração) é explícita.
Há portanto várias decisões a serem tomadas para implementar a aritmética computacional de ponto flutuante. Que base deve ser usada? Que tamanho de palavra, que tamanho de significando, que tamanho de expoente? Deve um bit de sinal de 1 representar números negativos ou positivos? Como o zero deve ser representado? Que métodos de arredondamento devem ser usados? O que deve ser feito se o resultado de um cálculo exceder o maior valor absoluto expressável no sistema escolhido (i.e. se ele “overflows”), ou se ele cai abaixo do menor (i.e., se ele underflows)? O que deve ser feito se um usuário tenta uma operação sem sentido aritmético, tal como dividir zero por zero?
Diferentes fabricantes de computador (como também, uma vez que se tornou possível implementar aritmética de ponto flutuante em calculadoras eletrônicas, diferentes fabricantes de calculadoras) adotaram soluções diferentes para essas questões. Isto foi, patentemente, uma fonte de alguma dificuldade prática, uma vez que tornou difícil usar um programa numérico escrito para um computador num outro, mesmo quando uma linguagem de programação padrão tal como o Fortran era usada. Mas isso importa mais profundamente do que essa dificuldade? Os resultados de diferentes decisões eram realmente aritméticas diferentes ou eles eram simplesmente diferentes mas formas essencialmente equivalentes de implementar a única aritmética verdadeira?
A resposta depende da reação ao que pode ser chamado de cálculos anômalos. Em algumas circunstâncias máquinas diferentes produzem resultados substancialmente diferentes para o mesmo cálculo. Em outros casos, a aritmética da máquina viola leis consensuais da aritmética humana. Pequenas diferenças entre o mesmo cálculo realizado em máquinas diferentes são comuns, e especialistas no campo podem produzir casos de resultados que diferem consideravelmente. Um especialista cita um problema de juros compostos que produziu quatro respostas diferentes quando feito em calculadoras de quatro tipos diferentes: $331.667,00, $293.539,16, $334.858,18, e $331.559,38. Ele identifica máquinas em que a/1 não é igual a a (como deveria ser na aritmética humana) e ep - pe não é igual a zero.
Diferentes reações aos cálculos anômalos podem ser categorizadas segundo o esquema desenvolvido por Imre Lakatos na sua celebrada análise da evolução do teorema de Euler sobre o relacionamento entre o número de faces (F), arestas (E) e vértices (V) de um poliedro. Lakatos mostrou que tentativas de provar o relacionamento V – E + F = 2 esbarravam em contra-exemplos: figuras que poderiam ser tidas por poliedro mas que não obedeciam à lei. Uma resposta a estas “figuras anômalas” foi o que Lakatos chamou “excetuando a exceção primitiva”: simples indiferença a sua existência. Esta resposta caracteriza bem o que parece ter sido a maioria das respostas aos cálculos anômalos do computador e das calculadoras. A maioria dos usuários está provavelmente inconsciente da possibilidade de cálculos anômalos ou não se preocupam com eles no mesmo sentido que continuamos a atravessar pontes tranqüilamente embora tenhamos conhecimento de que algumas caíram. E também, para muitos projetistas de computador, cálculos anômalos parece ter estado bem baixo na lista de assuntos exigindo atenção, se é que o item está na lista.
Uma estratégia do tipo “excetuando a exceção” mais sofisticada foi citar o vasto volume de cálculos que são executados de forma perfeitamente satisfatória, e argumentar que os cálculos anômalos ocorrem em problemas que não foram “bem formulados”. Um problema bem formulado era um no qual pequenas alterações nos dados provocavam apenas pequenas alterações nos resultados; a solução empregava um algoritmo que era neste sentido “numericamente estável”. A técnica de “análise de erros para trás”, recentemente desenvolvida, foi usada, como justificativa dessa resposta, para discriminar entre problemas bem formulados e aqueles que não estavam bem formulados. Computadores e calculadoras funcionavam confiavelmente para problemas bem formulados. Se cálculos “patológicos” e problemas “degenerados” fossem evitados (o uso desses termos pode ser tomado como uma indicação que o “excetuando a exceção” estava se transformando naquilo que Lakatos chamou “excetuando monstros”) não haveria dificuldades.
No entanto, um pequeno número de cientistas da computação positivamente procurava “monstros”. Um líder entre eles era o professor W. Kahan que mantinha uma lotação conjunta no Departamento de Matemática e no Departamento de Engenharia Elétrica e Ciências da Computação em Berkeley. A abordagem de Kahan é um exemplo do que Lakatos chama a estratégia “dialética”, segundo a qual “anomalias e irregularidades são bem vindas e vistas como a justificativa para novas abordagens, novos conceitos e novos métodos.” Kahan tem sido um reformador não satisfeito com o corrente estado da aritmética de ponto flutuante do computador e calculadoras e constantemente procurando conceber, e construir suporte para, formas de melhorá-la. Ele procurava deliberadamente descobrir e publicar anomalias que pudessem ser usadas para mostrar que as diferenças entre as aritméticas computacionais eram sérias e conseqüentes.
A primeira oportunidade que teve Kahan de reformar a aritmética na direção que desejava foi uma competição entre dois importantes fabricantes de calculadoras sofisticadas, a Texas Instruments e a Hewlett- Packard. TI questionava a precisão das calculadoras HP. A HP respondia alegando que as máquinas de sua competidora apresentavam mais anomalias. Um executivo da Hewlett-Packard, Dennis Harms, viu uma vantagem em tentar fortalecer a posição de sua companhia a esse respeito, e empregou Kahan como consultor para o projeto da aritmética das calculadoras de nova geração, possibilitando assim que Kahan incorporasse suas idéias nas calculadoras.
A próxima oportunidade de Kahan aconteceu em 1977 quando a firma líder de microprocessadores, Intel, começou a desenvolver um chip de silício especificamente para executar a aritmética de ponto flutuante. Os microprocessadores existentes implementavam a aritmética de ponto flutuante em software em vez de em hardware, enquanto as unidades de ponto flutuante dos grandes computadores eram multichip. O Intel i8087, como o chip foi posteriormente batizado, foi projetado para ser um “coprocessador de ponto flutuante”, trabalhando ao lado do chip principal processador num microprocessador para melhorar sua performance aritmética.
Jonh Palmer, o engenheiro chefe do projeto do i8087 havia assistido aulas com Kahan como aluno de graduação e foi com ele se aconselhar. Palmer rejeitou a idéia de adotar a “aritmética IBM” apesar de seu uso muito difundido; Kahan acreditava que essa aritmética era inferior. A aritmética do fabricante líder de minicomputadores, a Digital Equipment Corporation, também foi rejeitada. Palmer, estava, no entanto, procurando não apenas “diferenciação de produto”. Ele estava preocupado com o fato de que se decisões erradas fossem tomadas seria impossível compartilhar alguns programas entre “diferentes caixas todas estampando o logotipo Intel”, e ele queria evitar, para a aritmética de ponto flutuante em microprocessadores “a situação caótica que ora existia nos ambientes de mainframes e minicomputadores.”
A Intel e outras fabricantes de chips do vale do Silício suportaram o estabelecimento de um comitê para considerar padrões para a aritmética de ponto flutuante. A iniciativa do comitê partiu de um consultor independente, Robert Stewart, que era ativo na Sociedade da Computação do Instituto dos Engenheiros Elétricos e Eletrônicos (IEEE), sob cuja égide o comitê foi estabelecido. Stewart recrutou para o comitê Kahan e representantes da Intel, outros fabricantes de chips, e fabricantes de minicomputadores. Richard Delp foi designado por Stewart como o primeiro chefe do grupo de trabalho. A Intel, que trabalhava em outros projetos, concordou em retardar a conclusão da aritmética do i8087 enquanto o comitê deliberava, muito embora ela claramente esperava que o padrão final seria similar ao que ela já havia desenvolvido.
Negociar a aritmética revelou ser um longo processo. O comitê iniciou seus trabalhos em setembro de 1977 e o padrão 754 da IEEE só foi adotado em 1985. A natureza geral dos interesses envolvidos era clara. A menos que o comitê seguisse a rota fácil de escrever um padrão geral que abarcasse as aritméticas existentes mais amplamente utilizadas (uma opção que foi considerada mas rejeitada); ou a menos que ele optasse por uma aritmética que fosse radicalmente diferente de qualquer outra existente, o que quer que ele decidisse favoreceria às empresas cujas práticas existentes fossem mais próximas do padrão e prejudicaria as empresas cujas práticas fossem mais distantes do padrão. Estas últimas empresas seriam forçadas a uma escolha desfavorável. Se elas mantivessem suas aritméticas existentes, seus mercados poderiam diminuir como um resultado de os usuários preferirem máquinas que implementassem o padrão. Se elas mudassem, estariam jogando fora um investimento considerável de tempo e dinheiro, e poderia haver embaraçosas incompatibilidades entre suas novas máquinas e as velhas.
No final das contas, o comitê chegou a duas aritméticas proximamente alinhadas com os grandes interesses corporativos. Uma era essencialmente a aritmética empregada pela Digital Equipment Corporation (DEC), fabricante líder de minicomputadores. As máquinas VAX da DEC eram amplamente utilizadas em computação científica e sua aritmética era considerada boa e respeitável mesmo pelos seus críticos. A outra era uma aritmética proposta por Kahan, seu aluno de graduação Jerome Coonem, e Harold Stone, Diretor de Arquiteturas Avançadas do Laboratório Yorktown Heights da IBM. Não surpreendentemente, em vista da colaboração entre Kahan e Palmer da Intel, esta proposta era muito similar a que a Intel estava em vias de implementar.
O esquema Kahan-Coonen-Stone tinha vários aspectos interessantes, tais como o tratamento do zero. Em seu formato básico, eles optaram por aquilo que é chamado de “zero normalizado”. O zero é expresso apenas por um significando zero e um expoente zero (0 x 20). A combinação do significando zero com um expoente não nulo (0 x 21, 0 x 22, etc.) não é permitida. Mas eles permitem que o bit de sinal assuma os dois valores, e permitem que seu valor seja significativo. Em outras palavras, diferente da aritmética humana consensual, que contém apenas um zero, sua aritmética contem um zero positivo e um zero negativo com a regra, por exemplo, que a raiz quadrada de –0 é –0.
Este e outros aspectos de sua aritmética eram, contudo, relativamente incontroversos. O ponto mais controverso entre sua proposta e a principal aritmética alternativa era o underflow. Diferente da aritmética dos números reais, onde não há um número “próximo de zero”, e números indefinidamente pequenos são possíveis, a aritmética computacional contém um limite inferior para o tamanho do número que pode ser representado. Por exemplo, 2-126 ou aproximadamente 10-38, é o menor número possível na representação normal do formato básico do esquema Kahan-Coonen-Stone. Como a maioria das aritméticas computacionais existentes, a aritmética do DEC simplesmente representava todos os números tão precisamente quanto possível até que o número próximo a zero fosse alcançado. Se um cálculo desse um resultado menor do que este número pequeno, o resultado era armazenado como zero. “Flush-to-zero underflow” é como este esquema foi geralmente chamado.
Kahan e seus colegas propuseram um princípio diferente de “underflow gradual”. Eles introduziram um conjunto especial de números desnormalizados menores do que o menor número no formato normal. Como foi notado acima, no formato normal de ponto flutuante o dígito à esquerda do ponto binário é sempre 1. Num número desnormalizado é zero. Números desnormalizados são criados deslocando-se para a direita o significando de tal forma que o expoente sempre permaneça dentro do domínio expressável. Num sistema onde o menor número normal é 2-126, 2-127 poderia ter a expressão desnormalizada ½ (0.1 em binário) x 2-126, e 2-128 ¼ (0.01 em binário) x 2-126 e assim por diante. É claro que isso significa que a precisão diminuiria, na medida em que um ou mais dígitos significativos são perdidos no deslocamento para a direita do significando. Mas isso pareceu aos proponentes um preço aceitável a pagar por essa aproximação mais gradual ao zero. Seu argumento contra o que muitos tomaram como sendo o procedimento “óbvio” da DEC era que, usando esse último, na medida em que se aproxima do zero as diferenças entre números sucessivos diminui até o menor número, cuja distância a zero era muito maior que a distância ao próximo maior. No underflow gradual as diferenças entre números sucessivos diminuíam monotonicamente até o zero.
O underflow gradual se tornou o foco de ataques na aritmética proposta por Kahan, Coonen, e Stone:
A interconectividade dos aspectos básicos do padrão proposto complicou as tentativas de se opor a ele. Os primeiros desafios dentro do sub-comitê não eram facilmente focados em aspectos simples do sistema de numeração proposto e de sua codificação, uma vez que muitas das escolhas de projeto eram interconectadas. Esses desafios, em última análise, focavam na proposta como um todo e, naturalmente, tendiam a se mover para seu ponto de menos resistência. Assim, foi possível para o underflow gradual – um dos aspectos mais tranqüilos do sistema – tornar-se seu mais contencioso.
Não havia nenhum argumento decisivo que provasse a superioridade de algum dos dois esquemas. Os proponentes do esquema Kahan-Coonen-Stone apontavam anomalias causadas, segundo eles, pelo esquema flush to zero que seriam corrigidas pelo underflow gradual:
Considere a simples computação (Y – X) + X quando (Y - X) underflows. O esquema gradual sempre retornará Y exatamente, flush to zero retornará X ... Poderíamos olhar isso como um outro exemplo isolado, mas eu prefiro vê-lo como a preservação da lei associativa da adição. Ou seja, com o underflow gradual sempre teremos (Y - X) + X = Y + (-X + X). Isto é decisivo, em minha opinião.
Os defensores do esquema DEC mais tradicional poderiam, contudo, também apontar problemas potenciais com o underflow gradual.
Multiplicação de números desnormalizados por números maiores do que 1 (ou divisão por números menores do que 1) pode gerar imprecisões significativas. Se tal produto (ou quociente) está na faixa ordinária de números, ele não pode ser representado na forma desnormalizada por conta do bit escondido usado na aritmética KCS. No entanto, o operando desnormalizado tem menos bits (talvez muito menos) do que o número prescrito (de bits) para o seu nível de precisão. Assim o produto (ou quociente) pode no pior caso conter apenas um bit válido. KCS especifica dois modos de lidar com este problema. O primeiro modo, dito “modo advertência”, é obrigatório: um flag de invalidez é ligado, e um símbolo NaN (não um número) é armazenado como resultado ... O outro modo, dito “normalizar”, é opcional: se presente, e selecionado, o produto possivelmente muito impreciso é armazenado como um número ordinário, nenhum flag é ligado, e, obviamente, o acompanhamento do efeito do underflow original é impossível.
Nesta vez, uma exceção de operação ilegal é avisada quando um número desnormalizado é multiplicado por um valor de 2 ou maior. Mas em inspeção mais próxima, há números desnormalizados próximos da faixa normalizada que exibem um comportamento mais errático. O número desnormalizado ¾ x 2-126, por exemplo, gerará uma exceção de operação inválida quando multiplicado por 5, mas não quando multiplicado por 6. Quando multiplicado por 8 uma exceção será novamente gerada ... Este efeito é causado porque a exceção para a multiplicação ocorre quando se tenta armazenar um número desnormalizado no formato básico. Quando multiplicado por 8 = 1 x 23, o resultado é ¾ x 2-123 que é desnormalizado. Mas a multiplicação por 6 = 3/2 x 22 dá 9/8 x 2-124, que é normalizado.
Estas objeções poderiam, por sua vez, ser refutadas:
Como qualquer ferramenta nova, é possível utilizar mal a facilidade e ela falhar ... Eu não acredito que a facilidade introduza falhas em processos que previamente funcionavam [no esquema flush to zero].
A propensão das duas aritméticas a gerar erros e cálculos anômalos não era a única questão a ser considerada. Havia, por exemplo, pouca dúvida que o underflow gradual era mais complicado de implementar do que o flush-to-zero; ele teria, portanto, custos em dinheiro e (talvez) no tempo devido às operações aritméticas tais como a multiplicação. Ele poderia dificultar o policiamento do padrão proposto, uma vez que dado sua complicação, os fabricantes poderiam escolher implementá-lo em software e não em hardware. Finalmente, o esquema DEC tinha simplesmente a enorme vantagem de ser aquele já empregado nos minicomputadores científicos mais populares no mundo.
Assim, nada abstrato garantia que o esquema Kahan- Coonen-Stone venceria: nas palavras do professor Kahan “não era uma conclusão inevitável.” Em seu favor estava a composição do grupo de trabalho, os fatos da geografia, e seu status como documento de trabalho original do grupo. Mary Payne da DEC baseada em Massachusets comentou:
Os membros ativos (e votantes) do grupo de trabalho são não na maioria de fabricantes de minicomputadores e semicondutores, da Academia, e de fornecedores de software portátil. Não há virtualmente nenhuma representação da indústria de mainframes e de “usuários ordinários”- pessoas que escrevem programas para seu uso próprio (ou de seus empregadores). A maioria dos membros ativos é da área da baía de São Francisco, e todos os encontros se deram nessa área, a menos de um.
Outros, contudo, apontam para a influência da personalidade forte e persuasiva de Kahan. O próprio Kahan entende como importante duas demonstrações da viabilidade técnica do underflow gradual (a Intel o implementou no software microcódigo do protótipo i8087, e um dos alunos de Kahan, George Taylor, projetou uma placa de processador para VAX da DEC que foi reconhecida como uma executora bem sucedida do underflow gradual), junto com o suporte qualificado para o underflow gradual dado pelo bem conhecido analista de erros, Professor G. W. Stewart III da Universidade de Maryland, que havia sido contratado para investigar o caso pela DEC.
Na primavera de 80, numa votação do comitê, o esquema KCS obteve a maioria necessária de 2/3 de votos para adoção. O esquema ainda levou vários anos para passar pelos altos comitês do Instituto de Engenheiros Elétricos e Eletrônicos, e foi finalmente aprovado pelo Conselho de Padrões do IEEE em março de 85 e pelo Americam National Standards Institute (ANSI/IEEE) como o padrão 754 em julho de 85.
Não é um padrão universal. A maioria dos supercomputadores (como os Cray), mainframes (como as máquinas IBM) e minicomputadores (como os VAXs da DEC) não o cumprem. No entanto não se chegou a nenhum outro padrão coletivo competidor. Assim, existe um ciclo virtuoso: na medida em que o padrão 754 IEEE se torna mais popular, os problemas envolvidos em portar programas numéricos entre máquinas diminuem, e mais software é escrito para o padrão 754, o que aumenta sua popularidade. Os proponentes de novas tecnologias adotam o padrão 754 para que os usuários não tenham de reescrever programas para mover para essas novas tecnologias.
O que aconteceu é assim uma versão de uma forma de “fechamento” típico dentro da tecnologia. Nas palavras de Brian Arthur:
Freqüentemente, tecnologias mostram retornos crescentes de adoção – quanto mais elas são adotadas mais elas são melhoradas... Quando duas ou mais tecnologias de retornos crescentes competem por adotantes, eventos fortuitos insignificantes podem dar a uma das tecnologias uma vantagem inicial de adoção. Então mais experiência é ganha com a tecnologia e assim ela melhora; ela é então mais adotada, e melhora mais. Assim, a tecnologia que por sorte tenha um bom começo pode eventualmente “açambarcar o mercado” dos adotantes potenciais, desbancando, gradativamente as outras tecnologias.
Há os que negam que tenha sido institucionalizada a melhor aritmética computacional possível, e os que atribuem a adoção do padrão a eventos fortuitos e não aos méritos intrínsecos que lhe atribuem seus proponentes. Essa disputa, contudo, é agora em certo sentido irrelevante: o próprio processo da institucionalização do padrão lhe dá vantagens práticas que tornam improvável sua substituição por um competidor.
Conforme notado no capítulo 7, tem sido argumentado influentemente que a complexidade de sistemas computacionais limita a extensão até onde o teste empírico pode demonstrar a exatidão de um software ou de um projeto de hardware. Na medida em que o teste de programas não pode normalmente ser exaustivo, ele “pode ser uma forma muito efetiva de mostrar a presença de falhas, mas ele é inadequado para mostrar sua ausência”. Cientistas computacionais “matematizantes” têm percebido que só há uma rota segura para programas ou projetos de hardware serem implementações demonstravelmente corretas de suas especificações: prova matemática dedutiva. “A única forma efetiva de se aumentar significativamente o nível de confiança de um programa é dar um prova convincente de sua exatidão.”
Nos anos 80, esses argumentos, originalmente acadêmicos, começaram a ser adotados pelos responsáveis por sistemas computacionais que fossem críticos para as áreas de segurança nacional ou segurança humana. O primeiro a atuar sobre eles foi o Departamento de Defesa americano que em 1983 estabeleceu seus Critérios de Avaliação de Sistemas Computacionais Confiáveis, conhecido como Livro Laranja pela cor da capa do documento que os continha. O Livro Laranja estabelecia uma hierarquia de critérios a serem aplicados a sistemas computacionais que continham informação crítica à segurança nacional. Para obter a avaliação mais alta – Classe A1 (“Projeto Verificado”) - exigia-se uma prova matemática de que o projeto do sistema se conformava a um modelo formal do que constituía “segurança”.
Na Europa, a demanda por prova matemática fez-se mais presente sobre sistemas computacionais críticos à segurança humana do que à segurança nacional (embora critérios Europeus análogos aos do Livro Laranja tenham sido emitidos). Em 1986, o Conselho Assessor de Pesquisa Aplicada e Desenvolvimento do governo britânico passou a exigir prova matemática para o caso de sistemas cuja falha pudesse resultar em mais que dez mortes, e em 1991 o padrão interino 00-55 da Defesa passou a exigir prova matemática de que os programas mais cruciais à segurança fossem implementações corretas de suas especificações.
Nesses documentos, com exceção do mais recente (o Padrão 00-55 da Defesa, discutido abaixo), a noção de “prova” foi tipicamente usada como se seu significado não fosse problemático. Em 1987, Pelaez, Fleck e eu especulamos que este uso não problemático não sobreviveria à entrada da prova nos domínios comerciais e legais. Predissemos que não tardaria o dia em que “os tribunais teriam que decidir sobre o que constitui um procedimento de prova matemática.” Esta predição estava baseada em considerações da sociologia do conhecimento esboçadas no capítulo 1 e na variação considerável, revelada pela história da matemática, das formas de argumento que tem sido tomadas como constituindo provas. Por exemplo, Judith Grabiner mostrou como argumentos que satisfizeram matemáticos no século XVIII foram rejeitados como não constituindo provas pelos seus sucessores no século XIX, tal como Cauchy. Nossa predição se baseava no pressuposto de que tentativas de provar a exatidão do projeto de sistemas computacionais trariam à luz discordâncias similares sobre a natureza da prova.
Em 1991, a predição de litígio emergiu na disputa, discutida no capítulo 7, sobre se a cadeia de raciocínio – como era então referida – conectando o projeto do microprocessador VIPER a sua especificação poderia ser legitimamente chamada de “prova”. A falência da litigante, Charter Technologies Ltd., evitou que o caso fosse para os tribunais.
A disputa sobre a VIPER não deveria ser vista como inteiramente sui generis. O que estava em questão (pelo menos potencialmente) não era meramente o status de uma cadeia específica de raciocínio matemático, mas também o significado de “prova” matemática – um assunto que claramente vai além das particularidades deste episódio. Este será o foco do restante do presente capítulo.
Um significado de prova é sumariado por Robert Boyer e J. Strother Moore, importantes proponentes do uso de sistemas computacionais para provar teoremas matemáticos (e colegas de dois dos críticos da prova do VIPER, Bishop Brock e Warren Hunt), como se segue: “Uma prova matemática formal é uma seqüência finita de fórmulas, onde cada elemento é um axioma ou o resultado da aplicação de um conjunto fixo de regras mecânicas a fórmulas prévias na seqüência”. A aplicação deste critério ao VIPER não foi nunca publicamente desafiada antes ou durante o litígio. A defesa do ministério contra as alegações do litigante é um documento confidencial. A resposta publicada (de conhecimento deste autor) por um membro do time VIPER para criticar a alegação da prova não tentou uma refutação. De qualquer forma, o réu no processo era o ministério e não os membros individuais do time, de tal forma que a linha de argumentos adotada pode não ter sido deles.
No entanto, um ataque à noção formal de prova foi a base da defesa da VIPER montada, após o encerramento do litígio, por Martyn Thomas, diretor da software house Práxis:
Nós temos que ter cuidado ao restringir o termo prova a uma abordagem extremamente formal da verificação. Se prova significa apenas uma verificação axiomática através de provadores de teoremas, a maior parte da matemática é não provada e não provável. Os processos “sociais” da prova são suficientemente bons para engenheiros em outras disciplinas, suficientemente bons para os matemáticos e suficientemente bons para mim... Se nós reservarmos a palavra “prova” para as atividades dos seguidores de Hilbert estaremos desperdiçando uma palavra útil e correndo o risco de extrapolar os resultados de suas atividades.
David Hilbert (1862 – 1943) era um matemático formalista cuja definição de prova era em grande parte similar àquela dada acima de Boyer e Moore. A tradição formalista encabeçada por Hilbert procurava quebrar a conexão entre símbolos matemáticos e seus referentes físicos ou mentais. Símbolos, dizia o formalista, são apenas marcas sobre o papel, destituídos de significado intrínseco. Provas são construídas pela manipulação desses símbolos segundo as regras de transformação da lógica formal – regras que assumem uma precisa forma mecânica.
Apesar da considerável influência do formalismo dentro da matemática, nem todas as provas matemáticas têm essa forma. A maioria é mais curta, de mais alto nível, e mais informais. Parte da razão para isso é o simples tédio de se produzir provas formais, e o seu tamanho; isto explica também uma grande parte da atração dos sistemas geradores de provas automáticos e semi-automáticos, tais como o sistema HOL usado na prova do VIPER ou o provador automático de teoremas desenvolvido por Boyer e Moore.
A natureza relativamente informal de muito das provas matemáticas foi um recurso para a defesa da alegação de prova do VIPER, conforme mostra a citação acima de Thomas. Ela também foi a base de um ataque geral amplamente debatido sobre verificação formal de programas, um artigo de 1979 de Richard de Millo do Instituto de Tecnologia da Geórgia e Richard Lipton e Alan Perlis do Departamento de Ciência da Computação da Universidade de Yale. Provas de teoremas em matemática e verificações formais de programas de computador eram entidades radicalmente diferentes, eles argumentavam:
Uma prova não é um bonito objeto abstrato com uma existência independente. Nenhum matemático compreende uma prova, se recolhe na cadeira, e suspira feliz com o conhecimento que ele pode agora estar certo da verdade do seu teorema. Ele corre para o hall e procura alguém para escutá-lo. Ele invade a sala de colegas e toma conta do quadro negro. Ele dispensa compromissos e leva sua nova idéia a seminários. Ele tira seus alunos graduados de suas dissertações para ouvi-lo. Ele se põe ao telefone e conversa com seus colegas no Texas, Toronto...
Após internalização suficiente, transformação suficiente, generalização suficiente, uso suficiente e conexão suficiente, a comunidade matemática decide, eventualmente, que os conceitos centrais no teorema original, agora talvez já bastante alterados, têm estabilidade. Se as várias provas parecem corretas e os resultados são examinados de suficientes ângulos, então a verdade do teorema é considerada estar estabelecida. O teorema, então, é tido como verdadeiro no sentido clássico - isto é, no sentido de que ele poderia ser demonstrado por lógica dedutiva formal, embora para quase todos os teoremas tal dedução nunca ocorreu e nem ocorrerá.
Provas matemáticas aumentam nossa confiança na verdade das afirmações matemáticas, apenas após elas terem passado pelos mecanismos sociais da comunidade matemática. Estes mesmos mecanismos condicionam as chamadas provas de software, as longas verificações formais que correspondem, não ao trabalho da prova matemática, mas a estrutura lógica imaginária que o matemático evoca para descrever seu sentimento de crença. Verificações não são mensagens; uma pessoa que procure outros para lhes contar de sua última verificação vai se sentir um pária social. Ninguém vai estar interessado. Verificações não podem ser lidas prontamente. Algum leitor pode até, num esforço heróico, dar uma vista d’olhos em uma das menores, mas isso não é leitura. Sendo ilegíveis e, literalmente, incontáveis, verificações não podem ser internalizadas, transformadas, generalizadas, usadas, conectadas a outras disciplinas e posteriormente incorporadas em uma consciência comunitária. Elas não podem adquirir credibilidade gradualmente, como um teorema matemático pode. Ou se acredita nelas cegamente como um puro ato de fé, ou elas são sumariamente rejeitadas.
O artigo de De Millo-Lipton-Perlis provocou uma crítica áspera dos defensores da prática da verificação de programas. Um desses escreveu: “Eu sou um desses clássicos que acredita que um teorema pode ou não pode ser derivado a partir de um conjunto de axiomas. Eu não acredito que a veracidade de um teorema possa ser decidida por eleições”. Edsger Dijkstra, um dos líderes do movimento de matematização da ciência computacional, descreveu o artigo de De Millo-Lipton-Perlis como “um panfleto político da idade média”. Interessante o registro, no entanto, de que Dijkstra defendia provas de programas curtas, elegantes e humanas (não mecânicas). Ele aceitava que as “comunicações entre matemáticos são um ingrediente essencial da nossa cultura matemática”, e concedia que “longas provas formais são não convincentes”. E acrescentava: “com relação a idéia de que provas são tão chatas que não podemos confiar nelas a menos que sejam verificadas mecanicamente, eu tenho objeções quase filosóficas, porque considero provas matemáticas como uma reflexo do meu entendimento e entendimento é algo que nós não podemos delegar a outra pessoa nem a uma máquina”.
Pelo menos três posições disputavam no debate provocado por De Millo, Lipton e Perlis: a verificação formal e mecânica de programas e projetos de hardware; a negação de que a verificação confere validade como a conferida pela prova em matemática; e a superioridade da prova humana sobre a prova da máquina. Nenhum fechamento definitivo do debate foi alcançado dentro da ciência da computação, e a validade da analogia entre provas em matemática e verificações formais de sistemas computacionais permanece controversa.
Dentro da matemática, também, o status das provas apoiadas por computador tem sido objeto de controvérsia. A controvérsia cristalizou mais claramente em torno da prova baseada em computador, feita em 1976, por Kenneth Appel e Wolfgang Haken sobre a conjectura das quatro cores. Os defensores desta prova sumariaram pelo menos algumas objeções e sua defesa como se segue:
A maioria dos matemáticos que foram educados antes do desenvolvimento dos rápidos computadores tende a não ver o computador como uma ferramenta rotineira para ser usada em conjunção com outras ferramentas mais velhas e mais teóricas no avanço do conhecimento matemático. Assim eles sentem intuitivamente que se um argumento contem partes, que não são verificáveis pelo cálculo manual, ele está num terreno bastante inseguro. Há uma tendência de sentir que a verificação dos resultados do computador por programas de computador independentes não é tão certa quanto a verificação manual independente da prova dos teoremas, provados na forma padrão.
Este ponto de vista é razoável para aqueles teoremas cujas provas são de tamanho moderado e altamente teóricas. Quando as provas são longas e altamente computacionais, pode ser argumentado que mesmo quando a verificação manual é possível, a probabilidade de erro humano é consideravelmente maior do que a do erro da máquina.
Embora a questão geral do status das provas formais geradas por computador permaneça em disputa, há sinais de que no nível do estabelecimento de padrões para os sistemas de computador críticos quanto a segurança, nacional ou humana, a disputa está sendo vencida na prática pelos proponentes da verificação formal. A demanda por verificação no Livro Laranja representa uma vitória dessa posição, embora controversa, porque tem havido críticas tanto ao modelo de “segurança” subjacente ao Livro Laranja, e quanto aos procedimentos para certificação segundo os critérios do Livro Laranja. O Livro Laranja não trata diretamente a questão da natureza da prova. Mais recentemente, no entanto, o documento Def Stan 00-55, representando a política oficial do Ministério da Defesa britânico fez isso, tratando explicitamente da questão do status relativo de formas diferentes de argumento matemático. Ele diferencia entre “Prova Formal” e “Argumento Rigoroso”:
Uma prova formal é uma seqüência estritamente bem formada de fórmulas lógicas tais que cada uma é implicada pelas fórmulas anteriores na seqüência ou axiomas da teoria lógica ...
Um Argumento Rigoroso está no nível de um argumento matemático na literatura científica que será submetido à revisão pelos pares ...
Segundo o Ministério, prova formal é preferível ao argumento rigoroso:
A criação de provas [formais] ... consumirá uma quantidade considerável de tempo do pessoal habilitado. O Padrão portanto também admite um nível mais baixo de garantia de projeto; este nível é conhecido como um Argumento Rigoroso. Um Argumento Rigoroso não é uma Prova Formal e não é um substituto para ela ...
Permanece incerto em que medida as práticas da indústria de software serão influenciadas pelo Def Stan 00-55 e por padrões similares de outros setores que podem se seguir – um procedimento admitindo exceções às demandas rígidas do 00-55 está incorporado no documento. Provas formais de programas “reais” ou projetos de hardware ainda são relativamente raras. Se elas se tornarem mais comuns, eu prediria que um novo nível de disputa e litígio emergirá. Isto dirá respeito, não ao status geral das provas formais geradas em computador (embora essa questão certamente retornará), mas a uma questão que até o momento não produziu controvérsia: a estrutura interna de provas formais. Mesmo que todos concordem que provas devam consistir da manipulação de fórmulas segundo as regras “mecânicas” da lógica, não se segue que todos concordarão com o que devem ser essas fórmulas. As histórias da prova matemática e da lógica formal revelam escopo para discordâncias significativas.
A disputa mais conhecida se refere à lei do terceiro excluído (que afirma que uma proposição ou sua negação é verdadeira) e assim a aceitabilidade de provar que um objeto matemático existe mostrando que sua não existência implicaria uma contradição. Formalistas, tais como Hilbert, não entendem essas provas como problemáticas; “construtivistas” e “intuicionistas”, notadamente L. E. Brouwer, se recusam a empregá-las, pelo menos para conjuntos infinitos.
Outros exemplos são aqueles por vezes chamados de os princípios de Lewis, assim denominado por conta do lógico Clarence Irving Lewis. Estes princípios dizem que uma contradição implica qualquer proposição, e que uma tautologia é implicada por qualquer proposição. Eles decorrem de axiomatizações da lógica formal intuitivamente sugestivas, no entanto eles têm sido considerados dúbios por alguns. É razoável, por exemplo, inferir, como permite o primeiro princípio de Lewis, que “A lua é feita de queijo verde” decorre de “João é um homem e João não é um homem”? Nas palavras de um texto: “Pessoas diferentes reagem de formas diferentes aos princípios de Lewis. Para alguns eles são convidados bem vindos, enquanto para outros eles são estranhos e suspeitos. Para alguns, não é mais questionável em lógica dizer que uma [contradição] implica todas as fórmulas do que é em aritmética dizer que x0 é sempre igual a 1 ... Para outros, contudo, os princípios de Lewis são inaceitáveis porque a fórmula antecedente pode não ter nada a ver com a fórmula conseqüente”. Os críticos têm de encarar o problema que qualquer sistema lógico que desista dos princípios de Lewis parece ter que desistir de pelo menos um axioma lógico, mais básico, “intuitivamente óbvio”.
Estas regras controversas da lógica são achadas nos sistemas dos quais a prova formal de programas e hardware depende. A lei do terceiro excluído é amplamente usada em prova automática de teoremas (por exemplo, no sistema HOL usado para a prova formal do VIPER). O primeiro princípio de Lewis – que uma contradição implica qualquer proposição – é achado em quase todos sistemas de raciocínio automatizado (e.g., entre as regras de inferência básica do influente Vienna Development Metho).
Até hoje, essas regras não têm provocado dentro da ciência da computação o tipo de controvérsia que as tem envolvido em metamatemática e lógica formal. Tem havido algum conflito intelectual entre os proponentes dos provadores de teoremas “clássicos”, que empregam a lei do terceiro excluído, e os “construtivistas” que não a emprega. Esse conflito não tomou, até hoje, a forma de uma disputa filosófica cerrada, e, até onde sabe o autor, nenhuma prova baseada em computador foi recusada por conta de seu uso do terceiro excluído ou dos princípios de Lewis. Considerações pragmáticas - colocar os sistemas para “trabalhar”, escolher a lógica apropriada ao contexto particular – têm prevalecido sobre questões filosóficas mais amplas.
Podemos assumir, contudo, que uma situação de pragmatismo e coexistência pacífica entre diferentes sistemas lógicos continuará? Meu sentimento é de que não podemos; esta situação é um produto da fase acadêmica experimental do desenvolvimento da prova da exatidão de sistemas computacionais. Na medida em que provas se tornem de maior significância comercial e legal, interesses poderosos se desenvolverão em defesa ou como crítica de provas particulares. Algumas vezes, pelo menos, esses interesses conflitarão. Numa tal situação, a validade das regras da lógica formal será inevitavelmente levada para dentro da disputa, e para dentro dos tribunais.
Há uma diferença importante entre a aritmética computacional de ponto flutuante e a prova de sistemas computacionais. No primeiro caso havia uma aritmética humana consensual e estável perante a qual a aritmética computacional poderia ser julgada. A aritmética humana foi, contudo, insuficiente para determinar a melhor forma da aritmética computacional. Foi, na verdade, uma questão de julgamento de qual era melhor, e julgamento contestado a esse respeito. A aritmética humana provia um recurso, utilizado diferentemente pelos diferentes participantes, e não um conjunto de regras que poderia simplesmente ser aplicado na aritmética computacional. Há até evidência tentativa de que interesses sociais, particularmente os interesse diferentes da Intel e da Digital influenciaram os julgamentos. Similarmente, o resultado – “fechamento” em favor do esquema Kahan-Coonen-Stone – pode ter sido influenciado por fatores contingentes tais como a proximidade dos encontros do comitê do Vale do Silício, casa da Intel e outras firmas semicondutoras, a base Berkeley de Kahan.
No caso da prova de sistemas computacionais, as práticas de prova existentes dentro da matemática têm sido menos decisivas. A reputação da matemática de precisão e certeza da matemática tem sido um importante recurso retórico para aqueles que procuram mudar a abordagem da exatidão de sistemas computacionais do empírico para o dedutivo. No entanto, os críticos têm argumentado que a prova da exatidão de um programa computacional e a prova de um teorema matemático são diferentes em espécie.
Uma disputa sobre a prova matemática de um sistema computacional já atingiu o estágio de litígio: a controvérsia a respeito do microprocessador VIPER. A predição desse capítulo é que o caso VIPER não será o único. Nem será ele suficiente para alcançar o consenso sobre a forma geral a ser tomada pelas provas – por exemplo, demandar que elas tomem a forma de seqüências de manipulações de símbolos realizadas segundo as regras de transformação de um sistema lógico. Se a posição adotada neste capítulo está correta, isto simplesmente empurrará a disputa para baixo, do status de tipos gerais de argumentos para a validade de etapas particulares nesses argumentos. Especificamente, esperam-se disputas sobre o sistema lógico que suporta as provas formais.
A prova formal da exatidão de sistemas computacionais é, portanto, um caso de teste interessante para a sociologia do conhecimento, porque esta predição é contrária a nossas intuições ordinárias sobre a certeza matemática. Ela se utiliza não da matemática informal ou semi-formal do tipo que até hoje tem provido a maior parte do material empírico para a sociologia do conhecimento, mas da dedução matemática da espécie mais formal: precisamente o tipo de raciocínio que, podemos imaginar, tem que compelir à concordância. Na medida em que a prova de sistemas computacionais cresce em importância e se move para dentro dos mundos comerciais e legais, nós teremos a oportunidade de ver se nossas intuições ordinárias sobre a matemática, ou se as conclusões da sociologia do conhecimento matemático estão corretas.
[1] H. M. Collins, Artificial Experts: Social Knowledge and Intelligent Machines (MIT Press, 1990), chapter 5.
Nota da Edição em HTML: As demais referências (2 a 60) não foram mantidas na tradução.