Uma linguagem computacional para a reescrita de expressões matemáticas por via axiomática

Abstract

A simplificação de expressões algébricas pode ser feita ao nível mais atómico ou elementar. Esta tese introduz um novo método de simplificar expressões algébricas, utilizando métodos de unificação e reescrita de termos de 1ª ordem. As expressões algébricas são vistas como estruturas triangulares, de profundidade finita, e são reescritas, axiomaticamente, num número finito de formas equivalentes que conduzem à sua normalização. A reescrita é feita comparando essas expressões com o lado esquerdo de fórmulas matemáticas com a mesma estrutura triangular. O método de simplificação, defendido nesta tese, produz soluções simbólicas completas, e não apenas respostas directas, numéricas ou simbólicas. Uma solução simbólica é uma solução que reflecte o raciocínio matemático que está por trás do processo de resolução simbólica. A pesquisa em computação simbólica tem produzido resultados bastante significativos na área da unificação e reescrita de termos. O nosso método de simplificação foi desenvolvido com base nos resultados obtidos dessa pesquisa. Com o conceito de estrutura triangular, foi possível desenvolver formas bastante eficientes de comparar expressões algébricas e regras matemáticas por classes de equivalência. O método de simplificação, que é defendido nesta tese, é baseado no método convencional de unificação e na composição lógica de expressões matemáticas, utilizando construtores funcionais e regras de reescrita condicional de 1ª ordem. O método foi implementado em Prolog e utiliza o DCG como processador da linguagem corrente de expressões matemáticas. A maioria dos sistemas de computação algébrica (CAS), como por exemplo o Maple™ e o Mathematica™, utilizam lógicas de ordem superior e não produzem soluções simbólicas ao nível elementar. O programa MathXPert™ e o sistema de derivação desenvolvido para o programa EPGY da Universidade de Stanford produzem esse tipo de solução mas utilizando também lógicas de ordem superior. A nossa contribuição foi o desenvolvimento da estrutura triangular como uma estrutura lógica para a computação simbólica de expressões matemáticas. Foi graças a este tipo de estrutura que foi possível desenvolver soluções simbólicas para problemas de simplificação algébrica, utilizando apenas lógicas de 1ª ordem.

The simplification of algebraic expressions can be accomplished at the most atomic or elementary step. This thesis introduces a new method of simplifying algebraic expressions, using 1st order unification and term rewriting methods. Algebraic expressions are viewed as triangular structures, of finite depth, and are rewritten, axiomatically, into a finite set of equivalent forms that leads to their normalization. Rewriting is done by matching these expressions with the left sides of mathematical formulas with the same triangular structure. The simplification method, defended by this thesis, produces complete symbolic solutions as opposed to straight, either numeric or symbolic, answers. A symbolic solution is a solution that reflects the mathematical reasoning behind the resolution process. Research in symbolic computing has already produced many outstanding results in the area of term unification and rewriting. Our simplification method is built on this research. By viewing these expressions as triangular structures, it was possible to develop very efficient ways of matching algebraic expressions and mathematical rules by classes of equivalence. The method that is defended in this thesis is based on standard unification and logic composition of mathematical expressions, using 1st order functional constructors and oriented conditional term rewriting. The method was implemented on Prolog and uses DCG as a natural language processor for mathematical expressions. The majority of computer algebra systems (CAS), such as Maple™ and Mathematica™, use higher order logics and do not produce symbolic solutions at the elementary level. The program MathXPert™ and the derivation system developed for the EPGY program of the University of Stanford produce these kinds of solutions but use also higher order logics. Our contribution was the development of a triangular structure as a logic structure for symbolic computation. It was thanks to this kind of structure that it was possible to develop complete symbolic solutions to algebraic simplification problems using only 1st order logic.