В ответ на другой вопрос, « Расширения бета-теории лямбда-исчисления» , Евгений предложил ответ:
бета + правило {s = t | s и t закрытые неразрешимые условия}
где термин М разрешим , если мы можем найти последовательность терминов , такие , что M приложение «s для них равно I .
Ответ Евгения дает эквациональную теорию для лямбда-исчисления, но не та, которая характеризуется системой редукции, т. Е. Слитным, рекурсивным набором правил переписывания.
Давайте назовем невидимую эквивалентность над теорией лямбда-исчисления, системой редукции, которая приравнивает некоторый нетривиальный набор замкнутых неразрешимых лямбда-членов, но не добавляет никаких новых уравнений, включающих разрешимые члены.
Есть ли какие-то невидимые эквивалентности над бета-теорией лямбда-исчисления?
Постскриптум Пример, характеризующий невидимую эквивалентность, но не слитый. Пусть M = (λx.xx) и N = (λx.xxx) , два неразрешимых члена. Добавление правила перезаписи NN в MM индуцирует невидимую эквивалентность, содержащую MM = NN , но имеет плохую критическую пару, где NN сводится к MM и MMN , каждая из которых имеет одну доступную перезапись, которая переписывает сама.
источник
Ответы:
Да. С M = (λx.xx) за вопрос рассмотрим переписывание ζ, которое переводит MM p в MM .
Он сливается и поэтому характеризует систему редукции по лямбда-исчислению. Набросок аргумента для слияния: поскольку MM замкнут, нам нужно рассмотреть только критические пары вида MMN 1 ... N k . Это может быть решено.
Это невидимая эквивалентность, потому что члены вида MMI ... I (с нулем или более I s) являются замкнутыми неразрешимыми членами, которые сводятся только к себе в базовом лямбда-исчислении и, таким образом, различны, и поэтому бесконечное множество этих члены нетривиальны и, очевидно, приравниваются к ζ.
Мне не нравится принимать мой ответ на мой вопрос, поэтому я приму ответ от кого-то, кто приводит менее абсурдно неполный аргумент слияния.
источник