Sobre la correspondencia de la introducción a la izquierda y la eliminación de la implicación en el cálculo secuencial y en la deducción natural resp.
8
¿Podría alguien dar una explicación intuitiva ( no intuitiva) de la correspondencia de la introducción a la izquierda y la eliminación de la implicación en el cálculo secuencial (SC) y la deducción natural (ND) respectivamente? Sé que deberían hacerlo por la simetría de SC pero no veo cómo se corresponden entre sí. En términos más generales, no entiendo cómo la introducción izquierda de un conectivo en SC hace que su eliminación en ND sea exactamente intuitiva.
En términos computacionales, un término de cálculo posterior es una secuenciación de un término lambda. Es decir, visto como un sistema de tipos, el cálculo secuencial puede verse como un orden de evaluación de un término lambda.
Así, supongamos y gamma ⊢ e 2 : Una .Γ ⊢ e1: A → BΓ ⊢ e2: A
En la deducción natural, el término para la eliminación de implicaciones es - es decir, aplicación. Sin embargo, tenga en cuenta que esto no nos dice si debemos evaluar e 1 primero o e 2 primero.Γ⊢e1e2:Be1e2
En el cálculo posterior, una asignación de término de prueba correspondiente debe verse como
letf=e1inletv=e2inletx=fvinx
o de lo contrario debe verse
letv=e2inletf=e1inletx=fvinx
e1e2
Para lenguajes puramente funcionales, esta explicidad no importa, pero a medida que agrega efectos, resulta más fácil trabajar con cálculos posteriores. Esta es la razón por la cual cosas como el cálculo de los efectos de control / lógica clásica se presentan típicamente como cálculo secuencial.
Neel, gracias también por esta interesante interpretación desde el punto de vista del cálculo.
día
Neel, ¿puedes dar documentos o capítulos de libros donde puedas encontrar más detalles?
bellpeace
8
Solo para recapitular: en ND, la eliminación de un conectivo nos dice cómo usarlo:
A∧B −−− A
A∧B −−− B
A∧BAB
Del mismo modo, en SC:
Γ,A⊢Δ −−−−−− Γ,A∧B⊢Δ
Γ,B⊢Δ −−−−−− Γ,A∧B⊢Δ
ABA∧BAB
En general, las reglas de introducción a la izquierda del SC nos dicen "cuándo" podemos usar un conectivo, y las reglas de eliminación de ND nos dicen "cómo" usar un conectivo.
Solo para recapitular: en ND, la eliminación de un conectivo nos dice cómo usarlo:
Del mismo modo, en SC:
En general, las reglas de introducción a la izquierda del SC nos dicen "cuándo" podemos usar un conectivo, y las reglas de eliminación de ND nos dicen "cómo" usar un conectivo.
Ahora, por implicación, en ND tenemos:
En SC:
fuente