Jueves 28, 17:30hs

Dr. Eduardo Bonelli, LIFIA, Fac. de Informática, UNLP

Resumen:

La teoría de reescritura estudia los sistemas de reescritura: formalismos que permiten transformar un objeto (término, expresión, programa) en otro a partir de una serie de reglas de transformación. Su generalidad y simplicidad ha cautivado el interés de numerosas áreas en computación incluyendo la de lenguajes de programación, asistentes de prueba, verificación de sistemas, resolución de ecuaciones, etc. (Digresión: gracias a ello, este año la conferencia más importante del área, a saber Rewriting Techniques and Applications (RTA), cumple veinte años!)

Presentaremos dos formalismos de reescritura y consideraremos la relación que existe entre ellos. El primero de ellos es el de los sistemas de reescritura de primer orden. Los objetos que son transformados son términos algebraicos. Su estudio sistemático data de los años 40 y actualmente se cuenta con un gran cuerpo de conocimientos sobre los mismos.

El segundo formalismo es el de los sistemas de reescritura de alto orden. Aquí los objetos a ser transformados son términos en los que pueden aparecer variables ligadas y operaciones de sustitución. Estos sistemas son más recientes (principios de los 80). También son más complicados: muchos resultados válidos para sistemas de primer orden dejan de serlo para los de alto orden. Sin embargo, dado que las nociones de variable ligada y sustitución se encuentran omnipresentes en computación, son de marcado interés para muchas áreas (tales como aquellas ya mencionadas).

Concretamente, mostraremos cómo a través de los llamados cálculos de sustituciones explícitas podemos establecer un nexo entre sistemas de reescritura de primer orden y sistemas de reescritura de alto orden. Se espera que, a través de éste nexo, se puedan aprovechar propiedades de los sistemas de primer orden en el marco de los de alto orden.