Caracterización de equivalencias invisibles mediante reglas de reescritura confluentes

14

En respuesta a otra pregunta, Extensiones de la teoría beta del cálculo lambda , Evgenij ofreció la respuesta:

beta + la regla {s = t | syt son términos cerrados sin solución}

donde un término M es soluble si podemos encontrar una sucesión de términos tales que M aplicación 's para ellos es igual a I .

La respuesta de Evgenij ofrece una teoría ecuación sobre el cálculo lambda, pero no una caracterizada por un sistema de reducción, es decir, un conjunto confluente y recursivo de reglas de reescritura.

Llamemos una equivalencia invisible sobre una teoría del cálculo lambda, un sistema de reducción que iguala un conjunto no trivial de términos lambda cerrados no resueltos, pero no agrega ninguna ecuación nueva que implique términos solucionables.

¿Hay alguna equivalencia invisible sobre la teoría beta del cálculo lambda?

Postdata Un ejemplo que caracteriza una equivalencia invisible, pero no es confluente. Sean M = (λx.xx) y N = (λx.xxx) , dos términos sin solución . Agregar la regla de reescritura de NN a MM induce una equivalencia invisible que contiene MM = NN , pero tiene el par crítico malo donde NN se reduce a MM y MMN , cada uno de los cuales tiene una reescritura disponible, que se reescribe a sí misma.

pl.programming-languages lambda-calculus lo.logic Charles Stewart
fuente
La noción de equivalencia invisible está relacionada con la noción de extensión conservadora . Una extensión conservadora de una teoría es una colección de términos y ecuaciones adicionales a la teoría que no agregan nuevas ecuaciones entre términos en la teoría original.
Dave Clarke el
@supercooldave: los términos insolubles son términos normales de la teoría, como (λx.xx) (λx.xx) , y son reducibles a otros términos (insolubles), por lo que son parte de la teoría normal del cálculo lambda. El punto es que son ortogonales a la semántica del cálculo lambda que obtenemos del teorema de Böhm.
Charles Stewart el
λβ
@Evgenij: Sí. Es crucial que las nuevas reglas sean confluentes y, por supuesto, triviales para encontrar ejemplos si no lo son. Agregaré un ejemplo para mostrar el problema.
Charles Stewart el

Respuestas:

6

Si. Con M = (λx.xx) según la pregunta, considere la reescritura ζ que lleva MM p a MM .

Es confluente y caracteriza un sistema de reducción sobre el cálculo lambda. Bosquejo del argumento para la confluencia: dado que MM está cerrado, solo necesitamos considerar pares críticos de la forma MMN 1 ... N k . Estos pueden ser resueltos.

Es una equivalencia invisible, porque los términos de la forma MMI ... I (con cero o más I s) son términos cerrados sin solución que se reducen solo a sí mismos en el cálculo lambda base, por lo tanto, son distintos y, por lo tanto, el conjunto infinito de estos los términos no son triviales y obviamente se equiparan con ζ.

No me gusta aceptar mi respuesta a mi pregunta, así que aceptaré una respuesta de alguien que proporcione un argumento de confluencia menos absurdamente incompleto.

Charles Stewart
fuente