Trabajo de fin de grado sobre los sistemas de reescritura tutorizado por Jose A. Alonso y María José Hidalgo.
Supongamos que tenemos la ecuación 2x - 2 = 0
. Para resolverla
utilizaremos varias reglas, para simplificar tomaremos dos; Dividir por constante
y Despejar
. La primera divide los dos miembros de la
ecuación por la constante que multiplica a x
, la segunda despeja
constantes al miembro derecho. A continuación, tenemos dos maneras de
proceder,
-
2x - 2 = 0
~Despejar
~2x = 2
~Dividir por constante
~x = 1
-
2x - 2 = 0
~Dividir por constante
~x - 1 = 0
~Despejar
~x = 1
Como hemos observamos, ambos terminan (pues no podemos aplicar
ninguna regla más) y además en el mismo resultado. Sin embargo
esto no siempre puede ocurrir. Si entre nuestras reglas tuvieramos
Despejar hacia Izq
el proceso no terminaría,
2x - 2 = 0
~Despejar
~2x = 2
~Despejar hacia Izq
~2x - 2 = 0
~Despejar
~2x = 2
...
Y si añadieramos la regla Acaba con cero
que transforma una ecuación
sin resolver a x= 0
, el orden a la hora de aplicar es fundamental,
pues dependiendo de las reglas que elijamos podremos acabar en x = 0
o en x = 1
.
Por ello, debemos formalizar que es un elemento al que se le pueden aplicar reglas, que reglas podemos tener, y que caracteristicas tienen esos elemenos con esas reglas.
En los capítulos 1, 2 y 3 introduciremos álgebra de relaciones de elementos, términos (los elementos que anteriormente hablamos), sistemas de reescritura y unificación.
En los capítulos 4, 5, 6 nos centraremos en estudiar propiedades de los sistemas reescritura, en concreto sobre cuando terminan, si todos terminan en el mismo término, y si podemos realizar alguna modificación a las reglas para que las anteriores propiedades se verifiquen.
Los algorítmos que se estudian durante este trabajo serán presentados en Haskell, siguiendo el código OCaml del libro Term rewriting and all that ~F. Baader T. Nipkow.
Cualquier duda, sugerencia o errata es bienvenida, puedes ponerte en contacto comingo mediante Github o via email