No ultimo dia 6 de fevereiro, teve início o Workshop de Tecnologia Adaptativa (WTA 2014), na Escola Politécnica da USP. O tradicional evento, que chega este ano a sua oitava edição, contou com palestras, tutoriais e debates acerca do horizonte da tecnologia adaptativa.
No primeiro dia do evento, houve, entre outras, a palestra do professor Marcus Vinícius Midena Ramos. Formado na Poli, ele é professor Universidade Federal do Vale do São Francisco (UNIVASF). O tema faz parte do trabalho que ele desenvolve em seu doutorado, que envolve a formalização da teoria de linguagens e autômatos por meio de assistentes de prova.
Grosso modo, assistentes de prova, também conhecidos como provadores interativos de teoremas, são ferramentas que verificam, por meio de um conjunto de regras de inferência de um cálculo fundamental, se estão corretas as demonstrações efetuadas ou os programas construídos. Eles são muito úteis porque, tanto no campo da matemática quanto da programação, há muita informalidade, pois os programas e teoremas em questão podem ser de difícil verificação ou demonstração. Os assistentes de prova, portanto, auxiliam neste trabalho, e para isso fazem uso de uma formalização matemática, que o professor apresentou como “a matemática codificada no computador”.
A palestra foi dividida em duas partes. A primeira envolveu principalmente o embasamento teórico por trás dos assistentes de prova. Outra, a aplicação prática desses assistentes, sobretudo no setor industrial, focando no “Coq”, um assistente de prova específico, tido como um dos mais importantes. Aquela parte ocorreu no dia 6 e esta no dia 7.
O autor sugere, a partir do isomorfismo de Curry-Howard (que aponta para uma relação direta e bidirecional entre matemática e programação), que se use assistentes de prova para realizar a verificação tanto da matemática quanto da programação. “Todas as características, todas as propriedades observadas em um programa, nós também encontramos na prova de um teorema, e vice-versa”, afirmou Marcus Vinícius.
Essa correspondência é a base da chamada Teoria de Tipos. Esta teoria é o que permite que se usem os resultados obtidos a partir do raciocínio lógico-matemático na construção de programas e se utilize, também, técnicas da programação na prova de teoremas. “Essas duas áreas que são aparentemente desconectadas têm, na verdade, uma associação muito forte que é benéfica para ambas”, diz o pesquisador.
Assim, o professor sugere que o uso de tais ferramentas pode ser fundamental para a tecnologia adaptativa. Por meio deles, torna-se mais fácil a prova/verificação de teoremas matemáticos/programas. Atualmente, esse é um trabalho que, dependendo da complexidade do teorema/programa, pode levar anos.
Com informações da Jornalismo Júnior (ECA – USP), por Otávio Fernandes Nadaleto
