Скажем, у меня есть два отношения R1 и R2. Если мне нужно решить проблему индукцией по члену R1 A (R2 B C), мне нужно сначала сделать remember R2 B C, иначе я потеряю информацию о том, что второй аргумент R1 был равен R2 B C. Есть ли вариант индукции такой тактики, который не требует от меня иметь дело с этим?
Вариант индукционной тактики, не требующий использования слова «запомнить» в подтермах
Ответы (1)
Ответ - нет.
Как работает индукция, она заменяет каждый экземпляр каждого из аргументов значениями, которые появляются в том же месте в конструкторах индуктивных предикатов. Чтобы упростить эту задачу, тактика remember заменяет составное выражение (R2 B C) переменной. Иногда этого можно избежать, если в вашей цели появляется (R2 B C), но это бывает редко.
person
Yves
schedule
10.04.2020
