Объединение путем трансформации

Question

я пишу объединение алгоритм на F# для использования с АСТ преобразования с использованием «Переписывание терминов и все такое» (ВолкКот) Франца Баадера и Тобиаса Нипкова.В разделе 4.6 Объединение путем преобразования было слишком много математической теории с примерами, и не так понятно, как хотелось бы.

Может ли кто-нибудь дать или указать более простые примеры, в которых используются преобразования:

Удалить, разложить, сориентировать, устранить.

Answer 1

Удалить: t = t бессмысленно и может быть исключено из системы уравнений.

1 =? 1 -> nil

Восток:Мы хотим, чтобы все уравнения были в виде x =? t, поэтому переверните любые уравнения в виде t =? x.

2 =? x1 -> x1 =? 2

Устранять:Данный x =? t, измените все остальные уравнения, чтобы заменить все экземпляры x с t.

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

Разложить:Нам нужно взять любые функции и исключить их, чтобы получить уравнения в виде x =? t.Обратите внимание, что этот процесс технически удаляет только одну функцию за раз.

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

Надеюсь, это поможет.