Характеризуя невидимые эквивалентности с помощью правил слияния

14

В ответ на другой вопрос, « Расширения бета-теории лямбда-исчисления» , Евгений предложил ответ:

бета + правило {s = t | s и t закрытые неразрешимые условия}

где термин М разрешим , если мы можем найти последовательность терминов , такие , что M приложение «s для них равно I .

Ответ Евгения дает эквациональную теорию для лямбда-исчисления, но не та, которая характеризуется системой редукции, т. Е. Слитным, рекурсивным набором правил переписывания.

Давайте назовем невидимую эквивалентность над теорией лямбда-исчисления, системой редукции, которая приравнивает некоторый нетривиальный набор замкнутых неразрешимых лямбда-членов, но не добавляет никаких новых уравнений, включающих разрешимые члены.

Есть ли какие-то невидимые эквивалентности над бета-теорией лямбда-исчисления?

Постскриптум Пример, характеризующий невидимую эквивалентность, но не слитый. Пусть M = (λx.xx) и N = (λx.xxx) , два неразрешимых члена. Добавление правила перезаписи NN в MM индуцирует невидимую эквивалентность, содержащую MM = NN , но имеет плохую критическую пару, где NN сводится к MM и MMN , каждая из которых имеет одну доступную перезапись, которая переписывает сама.

Чарльз Стюарт
источник
Понятие невидимой эквивалентности связано с понятием консервативного расширения . Консервативное расширение теории - это набор дополнительных терминов и уравнений в теории, которые не добавляют новые уравнения между терминами в исходной теории.
Дэйв Кларк
@supercooldave: неразрешимые термины являются нормальными терминами теории, такими как (λx.xx) (λx.xx) , и сводятся к другим (неразрешимым) терминам, поэтому являются частью нормальной теории лямбда-исчисления. Дело в том, что они ортогональны семантике лямбда-исчисления, которую мы получаем из теоремы Бёма.
Чарльз Стюарт
λβ
@ Евгений: Да. Крайне важно, чтобы новые правила были слиты, и, конечно, тривиально найти примеры, если их нет. Я добавлю пример, чтобы показать проблему.
Чарльз Стюарт

Ответы:

6

Да. С M = (λx.xx) за вопрос рассмотрим переписывание ζ, которое переводит MM p в MM .

Он сливается и поэтому характеризует систему редукции по лямбда-исчислению. Набросок аргумента для слияния: поскольку MM замкнут, нам нужно рассмотреть только критические пары вида MMN 1 ... N k . Это может быть решено.

Это невидимая эквивалентность, потому что члены вида MMI ... I (с нулем или более I s) являются замкнутыми неразрешимыми членами, которые сводятся только к себе в базовом лямбда-исчислении и, таким образом, различны, и поэтому бесконечное множество этих члены нетривиальны и, очевидно, приравниваются к ζ.

Мне не нравится принимать мой ответ на мой вопрос, поэтому я приму ответ от кого-то, кто приводит менее абсурдно неполный аргумент слияния.

Чарльз Стюарт
источник