Unificação por transformação

Question

Estou escrevendo um unificação algoritmo em F# para uso com AST transformações usando "Reescrita de termos e tudo mais" (Gato Selvagem) por Franz Baader e Tobias Nipkow.Para a seção 4.6 Unificação por transformação, havia muita teoria matemática com os exemplos, e não tão claro quanto eu gostaria.

Alguém pode dar ou apontar exemplos mais simples que fazem uso de transformações:

Excluir, decompor, orientar, eliminar.

Answer 1

Excluir: t = t é inútil e pode ser removido do conjunto de equações.

1 =? 1 -> nil

Orientar:Queremos todas as equações na forma de x =? t, então inverta quaisquer equações na forma de t =? x.

2 =? x1 -> x1 =? 2

Eliminar:Dado x =? t, altere todas as outras equações para substituir todas as instâncias de x com t.

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

Decompor:Precisamos pegar quaisquer funções e eliminá-las para obter equações na forma de x =? t.Observe que esse processo tecnicamente remove apenas uma função por vez.

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

Espero que isso ajude.