MathIS: Reorientando a matemática para a sociedade da informação

No interior das Sociedades da Informação uso efetivo da Matemática tem um enorme potencial económico, na medida em que, como Dijkstra notou, "a high technology so celebrated today is essentially a mathematical technology".

Neste contexto o projeto MathIS visou explorar a dinâmica da resolução algorítmica de problemas e o raciocínio por cálculo. Assim, procurou-se promover o uso efetivo, “industrial” da lógica, através de métodos que escalassem da aula de matemática para a mesa de trabalho do engenheiro que lida com problemas reais muito complexos.

Luís Barbosa, coordenador do projeto MathIS, revela que “o apoio do COMPETE foi essencial para viabilizar este projeto, suportar experiências concretas em escolas e na indústria de software e promover a divulgação dos seus resultados a nível internacional.”

Apoiado pelo COMPETE – Programa Operacional Fatores de Competitividade no âmbito do Sistema de Incentivos à Investigação e Desenvolvimento Tecnológico (SI I&DT), o projeto MathIS envolveu um investimento elegível de 54 mil euros, correspondendo a um incentivo FEDER de 46 mil euros.

A Sociedade da Informação requer profissionais altamente qualificados que possam conceber sistemas complexos com níveis cada vez maiores de fiabilidade e segurança. Mas requer também do conjunto da sociedade um grau elevado de "fluência matemática", entendendo-se por esta a capacidade de recorrer à linguagem e ao método matemático para modelar problemas e situações e raciocinar produtivamente no interior desses modelos. Tal capacidade e literacia tornou-se um elemento fundamental da cidadania democrática.

De facto, nas Sociedades da Informação o uso efetivo da Matemática tem um enorme potencial económico, na medida em que, como Dijkstra notou, "a high technology so celebrated today is essentially a mathematical technology".

Neste contexto, o projeto MathIS procurou explorar a dinâmica da resolução algorítmica de problemas e o raciocínio por cálculo, tanto ao nível da educação matemática como da prática da engenharia informática. O seu ponto de partida forma duas décadas de investigação em conceção de programas "correct-by-construction" de onde emergiu toda uma disciplina de resolução de problemas e, em particular, a sistematização de um estilo de raciocínio por cálculo que, procedendo de modo formal e essencialmente sintático, revolucionou as provas semiformais em linguagem natural e pobres em conteúdo algorítmico.

Pretendeu-se estudar e exemplificar o uso efetivo, “industrial” da lógica, através de métodos que escalassem da bancada escolar para a mesa de trabalho de engenheiro, que lida com problemas reais muito complexos.

Assim, a atividade do projeto desenvolveu-se em duas vertentes:

1. Ao nível educacional, o MathIS procurou reformular a abordagem de um conjunto de temas na matemática pré-universitária de acordo com as linhas acima enunciadas, assim como avaliar os seus méritos não apenas no desenvolvimento de competências algorítmicas, mas também como uma ferramenta para descoberta. Recorde-se, por exemplo, que foi através da manipulação formal das equações de Maxwell que se conjeturou a existência das ondas eletromagnéticas.

O projeto produziu diverso material (teaching scenarios) para uma abordagem orientada ao cálculo de diversos conteúdos na formação (secundária e profissional), tendo animado diversas workshops com alunos e professores de Matemática nesses graus de ensino. O esforço de investigação associado, suportado pelo COMPETE, conduziu a várias publicações, a uma tese de doutoramento sobre resolução algorítmica de problemas e a protótipos para a edição e registo de texto matemático manuscrito.

2. Ao nível da engenharia de software, o MathIS contribuiu no desenvolvimento de novos cálculos de programas aplicáveis na área emergente da computação global para garantirem o desenvolvimento correto e verificável de sistemas computacionais.

O projeto desenvolveu novos cálculos para o projeto e desenvolvimento correto (i.e. matematicamente verificável) de software, baseados em i) conexões de Galois, como ferramenta de transposição de resultados entre universos semânticos distintos, e ii) co álgebras, enquanto abstração de sistemas computacionais e seu comportamento.  

Uma das duas teses de doutoramento realizadas no âmbito desta componente do projeto veio a ser distinguida com o Prémio Científico IBM 2010, atribuído à então bolseira Alexandra Silva, hoje professora na Universidade de Nijmegen, Holanda.

Em termos quantitativos, o projeto MathIS originou:

• 3 Teses de doutoramento;
• 2 Capítulos de livro;
• 6 Artigos em revista;
• 15 Publicações em conferências internacionais com revisão por pares;
• 3 Protótipos de software.

Os excertos abaixo são de uma comunicação que fiz no âmbito da atribuição do Prémio IBM 2010 à Alexandra Silva, que resume algumas das intuições que estiveram presentes na génese e no desenvolvimento do projeto MathIS, que desse modo viu reconhecida uma das dimensões do seu plano de trabalho:

(...) A tese de doutoramento da Alexandra generaliza um dos resultados maiores das Ciências da Computação: o teorema de Kleene. Stephen Kleene formalizou nos anos cinquenta um modelo para a dinâmica da computação, o autómato de estados finitos, e introduziu uma linguagem, as expressões regulares, para especificar o seu comportamento. O célebre teorema que tem o seu nome enuncia a equivalência entre uns e outras, fornecendo uma abstração de um processo computacional e um modo rigoroso de descrever/prescrever o seu comportamento.

Durante anos a herança de Kleene foi inspiração e desafio. Nomeadamente na procura de axiomatizações que permitissem a manipulação expedita dessas expressões, na conceção de algoritmos eficientes para o seu processamento, e sobretudo na tentativa de generalização deste resultado a modelos comportamentais mais complexos.

Ora é exatamente neste ponto que a contribuição científica da Alexandra se situa. O seu trabalho tornou possível a derivação uniforme de linguagens para especificação de um conjunto muito vasto de modelos computacionais, das respetivas axiomatizações  e, para cada caso, de um resultado de equivalência no espírito do teorema de Kleene. Não apenas a sua abordagem cobre todos os casos documentados na literatura, para muitos dos quais apenas se conheciam soluções ad hoc, como permitiu tratar outros com solução até então desconhecida, nomeadamente modelos para sistemas com evolução incerta muito relevantes em aplicações onde a probabilidade de falha e o controlo de exceções tem de ser rigorosamente considerado.

(...) Finalmente, na medida em que permite modelar, calcular e verificar o comportamento de sistemas muito complexos, o trabalho tem implicações práticas de relevo para a conceção de sistemas informáticos confiáveis, isto é em que literalmente possamos confiar. Que não colapsam, que não se degradam, que fazem aquilo que muito prosaicamente se espera que façam.

(...) Infelizmente popularizou-se uma visão redutora que identifica a Informática com uma coleção de tecnologias e o desenvolvimento de software com um conjunto de metodologias empíricas e boas práticas. Habituamo-nos a conviver com “os erros do sistema”, a desculpar os seus pretensos estados de alma, a aceitar irrefletidamente que ao comprar um pacote de software recebamos não uma garantia, mas uma limitação de responsabilidade.

Não foi esta visão frouxa e sem ambição que motivou o projeto MathIS e trabalho da Alexandra e que o Prémio Científico IBM tão justamente distinguiu.

E ainda bem. Porque, de facto, se o que estiver em causa for o funcionamento de um dispositivo médico que me mantém ligado à vida ou o controlador do avião em que viajo, não estou interessado em meias certezas. Não me interessam testes em curso de execução, de resultados duvidosos para a minha sobrevivência, não quero saber de volumosos e verbosos cadernos de encargos nem de argumentos legais. Sobre a correção, a segurança e o desempenho desses sistemas não quero nada menos que o grau de certeza que me dá uma prova matemática. E não desempenha hoje a noção de prova automaticamente verificável um papel chave na garantia da segurança de uma compra on-line? Ou na certificação de software crítico cuja pertinência é já reconhecida pela indústria mais atenta e inovadora?

A verdade é que a Informática experimentou um desenvolvimento tecnológico vertiginoso bem antes de se haver constituído como ciência. E, no entanto, a complexidade crescente das suas aplicações exige a solidez e o rigor formal a que nos habituamos em outros domínios da Engenharia. Temos que construir os seus fundamentos e operacionalizá-los em técnicas e cálculos. Vivemos, mas a uma velocidade acelerada, o nosso século XVII. O trabalho hoje distinguido, e toda a área de investigação em que se insere, são parte essencial, assim o creio, do nosso passaporte para o futuro.

Por Luís Barbosa, coordenador do projeto MathIS

Este artigo foi escrito ao abrigo do novo acordo ortográfico.                                                                   

Por: Cátia Silva Pinto | Núcleo de Comunicação