Charakteryzowanie niewidocznych równoważników za pomocą konfluentnych reguł przepisywania

W odpowiedzi na inne pytanie, Rozszerzenia beta teorii rachunku lambda , Evgenij podał odpowiedź:

beta + reguła {s = t | s i t są zamkniętymi nierozwiązywalnymi warunkami}

gdzie termin M jest rozwiązywalne, czy możemy znaleźć sekwencję kategoriach takich, że M aplikacja „s do nich jest równa I .

Odpowiedź Evgenija podaje teorię równań nad rachunkiem lambda, ale nie taką, która charakteryzuje się systemem redukcji, tj. Zbieżnym, rekurencyjnym zbiorem reguł przepisywania.

Nazwijmy niewidzialną równoważność nad teorią rachunku lambda, systemem redukcyjnym, który zrównuje niektóre nietrywialne zbiory zamkniętych nierozwiązywalnych terminów lambda, ale nie dodaje żadnych nowych równań obejmujących rozwiązywalne terminy.

Czy są jakieś niewidoczne odpowiedniki teorii beta rachunku lambda?

Postscript Przykład, który charakteryzuje niewidoczną równoważność, ale nie jest zbieżny. Niech M = (λx.xx) i N = (λx.xxx) , dwa nierozwiązywalne terminy. Dodanie reguły przepisującej NN do MM indukuje niewidoczną równoważność zawierającą MM = NN , ale ma złą parę krytyczną, w której NN redukuje się zarówno do MM, jak i MMN , z których każda ma dostępne jedno przepisanie, które przepisuje się do siebie.

Tak. Przy M = (λx.xx) dla pytania, rozważ przepisanie ζ, które przenosi MM p na MM .

Jest zbieżny, a zatem charakteryzuje się systemem redukcji w stosunku do rachunku lambda. Szkic argumentu dla zbiegu: ponieważ MM jest zamknięty, musimy wziąć pod uwagę tylko krytyczne pary postaci MMN ₁ ... N _k . Można to rozwiązać.

Jest to równoważne niewidoczne, ponieważ pod względem formy MMI ... I (zero lub więcej I e) są zamknięte nierozwiązywalne warunki, które ograniczają się jedynie do siebie w rachunku podstawy lambda zatem są różne, a więc nieskończenie tych zestawów warunki są nietrywialne i oczywiście są równe ζ.

Nie lubię akceptować mojej odpowiedzi na moje pytanie, więc przyjmuję odpowiedź od kogoś, kto przedstawia mniej absurdalnie niekompletny argument o zbiegu.