La equivalencia es solo equivalencia en la teoría equational en discusión. En este caso, es la teoría esbozada en la Tabla 1. Tenga en cuenta que esta teoría no incluye : hacerlo haría que la teoría fuera extensional, y el punto es que respeta la , mientras que haría CL parcialmente extensional No estoy seguro de por qué la otra respuesta menciona .η ξ λ ηληξλη
Tenga en cuenta que en :λ
(M=βN)⟹(λx.M=βλx.N)(1)
Esto debería ser intuitivamente obvio: si es -convertible a cuando está solo, entonces también es -convertible a cuando es un subterm de .β N β N λ x . METROMβNβNλx.M
La regla , definida como
hace posible esta inferencia directamente cuando es parte de una teoría de . Su análogo CL sería:
Mξ λ M
M(λx.M)=N=(λx.N)(ξλ)
λM(λ∗x.M)=N=(λ∗x.N)(ξCL)
Ahora, el punto es que en CL, lo siguiente no se cumple :
( M=wnorte) ⟹ ( λ∗x . METRO=wλ∗x . norte)(2)
En otras palabras, si dos términos son débilmente iguales, entonces esto no es necesariamente cierto para sus versiones pseudo-abstraídas.
En consecuencia, si agregamos a una teoría CL, entonces comenzamos a equiparar términos que tienen diferentes formas normales.ξCL
Nota. Aquí, denota igualdad débil. Significa que puede convertirse en (y viceversa) mediante una serie de y (posiblemente también , si es parte de la teoría). Como probablemente sepa, es el análogo de CL de .M N S K I = w = βMETRO=wnorteMETROnorteSKyo=w=β
λ∗ es el pseudo-abstractor como se define en la página 5 de su documento. Tiene la siguiente propiedad:
(λ∗x.M)N⊳w[N/x]M(3)
Esta propiedad facilita encontrar un análogo CL para cualquier -term: simplemente cambie a y aplique las traducciones de acuerdo con la definición de .λ λ ∗ λ ∗λλλ∗λ∗
Para ser claros, el 'contraejemplo' en esta respuesta no es un contraejemplo para (2). Porque si tenemos:
N = ( λ ∗ z . Z ) x
M=x(4)
N=(λ∗z.z)x(5)
Entonces denota realmente (aplicando las traducciones de la página 5, y el hecho de que se define como al final de la página 4):I S K KNISKK
N=(λ∗z.z)x=Ix=SKKx(6)
Desde , tenemos, de hecho que . Sin embargo, si se trata de un contraejemplo, deberíamos tener eso . Pero si traducimos, en realidad obtenemos:M = w N ( λ ∗ y . M ) ≠ w ( λ ∗ y . N )SKKx⊳wKx(Kx)⊳wxM=wN(λ∗y.M)≠w(λ∗y.N)
( λ ∗ y . N ) = ( λ ∗ y . S K K x ) = K ( S K K x )
(λ∗y.M)=(λ∗y.x)=Kx(7)
(λ∗y.N)=(λ∗y.SKKx)=K(SKKx)(8)
Y es fácil verificar que (7) y (8) siguen siendo débilmente iguales, para:
K(SKKx)⊳wK(Kx(Kx))⊳wKx(9)
Ahora, un contraejemplo apropiado para (2) sería:
N = x
M=Kxy
N=x
Desde , definitivamente tenemos que . Sin embargo, si traduce cuidadosamente para las versiones resumidas, verá que ambas son formas normales distintas, y que no pueden ser convertibles de acuerdo con el teorema de Church-Rosser.M = w NKxy⊳wxM=wN
Primero verificamos :M′
M′(
M′=λ∗x.Kxy=S(λ∗x.Kx)(λ∗x.y)=S(λ∗x.Kx)(Ky)=S(S(λ∗x.K)(λ∗x.x))(Ky)=S(S(λ∗x.K)(I))(Ky)=S(S(λ∗x.K)(SKK))(Ky)=S(S(KK)(SKK))(Ky)
Aquí puede verificar que es una forma normal.
Aquí puede verificar que , como es de esperar si se supone que se comporta como un abstractor para CL.
M′(λ∗x.Kxy)P⊳wPλ∗
Ahora verificamos :
N′
N′=λ∗x.x=I=SKK
Que obviamente es una forma normal diferente de , entonces por el teorema de Church-Rosser. Tenga en cuenta también que , es decir, y 'producen la misma salida' para entradas arbitrarias .M ′ ≠ w N ′ N ′ P ⊳ w P M ′ N ′ PM′M′≠wN′N′P⊳wPM′N′P
Ahora hemos demostrado que (2) no se cumple en CL, y que una teoría CL que incorpore equivaldría, por lo tanto, a términos que no son débilmente iguales. ¿Pero por qué nos importa?ξ
Bueno, en primer lugar, hace que la interpretación combinatoria de imperfecta: aparentemente no todas las propiedades metateóricas se trasladan.λ
Además, y quizás lo más importante, si bien existen teorías extensionales de y CL, se mantienen originalmente y comúnmente en forma intensiva. La intencionalidad es una buena propiedad porque y la computación del modelo CL como proceso, y desde esta perspectiva, dos programas diferentes (específicamente, términos que tienen una forma normal diferente) que siempre producen los mismos resultados (con entradas iguales) no deben ser igualados. respeta este principio en , y si queremos hacer extensional, podríamos agregar, por ejemplo, . Pero la introducción deλ ξ λ λ η ξ ξλλξλληξen CL ya no lo haría completamente intensional (de hecho, solo parcialmente). Y esta es la razón de la 'notoriedad' de , como dice el artículo.ξ
EDITAR Esta respuesta es incorrecta, como el otro respondedor señaló correctamente. Usé la traducción a la lógica combinatoria de Asperti & Longo, que es sutilmente diferente de la de Selinger.
De hecho, esto ilustra un punto crucial: "la interpretación combinatoria" del cálculo lambda no es una sola cosa. Diferentes autores lo hacen de manera ligeramente diferente.
Dejo mi respuesta aquí para la posteridad, pero la otra respuesta es mejor.
La equivalencia en este contexto se define en las Tablas 1 y 2 en el documento de Selinger. Sin embargo, una axiomatisfacción ligeramente diferente puede aclarar un poco las cosas.
Lo que realmente significa es que dos términos son convertibles en la teoría . Podemos definir "convertibilidad" por los siguientes dos axiomas:λ
Además, por supuesto, los axiomas habituales y las reglas de inferencia necesarias para hacer una congruencia. A partir de esto, debería ser obvio que cualquier contraejemplo dependerá de la condición de variable libre en la regla se rompa.η= η
Creo que este es probablemente el más simple:
N = ( λ z . Z ) x
Puedes verificar por ti mismo que , pero sus respectivas interpretaciones combinatorias no son iguales bajo las reglas de la Tabla 2.λy.M=λy.N
fuente