Unificación por transformación

Question

Estoy escribiendo una Unificación algoritmo en F # para usar con ast transformaciones usando " Término de reescritura y todo eso " (>Woldcat ) por Franz Baeder y Tobias Nipkow.Para la sección 4.6 Unificación por transformación, fue una teoría de la matemática con los ejemplos, y no tan clara como me hubiera gustado.

¿Puede alguien dar o señalar ejemplos más simples que hacen uso de transformaciones:

Eliminar, descomponer, orientar, eliminar.

Answer 1

Eliminar: t = t no tiene sentido y se puede quitar del conjunto de ecuaciones.

1 =? 1 -> nil

Orient: Queremos todas las ecuaciones en forma de x =? t, así que voltea cualquier ecuación en la forma de t =? x.

2 =? x1 -> x1 =? 2

Eliminar: Dado x =? t, cambie todas las demás ecuaciones para reemplazar todas las instancias de x con t.

x1 + x2 = 7, x2 = 5 -> x1 + 5 = 7, x2 = 5

descomponer: debemos tomar cualquier función y eliminarlos para obtener ecuaciones en forma de x =? t.Tenga en cuenta que este proceso técnicamente solo elimina una función a la vez.

x1 + 5 = 7 -> x1 = 2
2 * (x1 + x2) = 14 -> x1 + x2 = 7

Esperemos que esto ayude.