¿Error tipográfico en el cálculo de construcciones de papel?

En el papel clásico de cálculo de construcciones hay una regla que establece

(página 7 del pdf, página 101 del documento original)

Esta regla significaría que cualquier contexto es reducible a un miembro de ese contexto. Parece que esto no debería ser correcto, ya que implicaría

1 ≅ Nat
3 ≅ Nat
1 ≅ 3

si Nat es un contexto.

Creo que la mejor interpretación es que el delta inferior estaba destinado a ser una M. Especialmente teniendo en cuenta las reglas que figuran en la página siguiente.

Entonces, ¿esto es simplemente un error tipográfico o alguna regla lógica sutil que no entiendo?

lo.logic calculus-of-constructions sequent-calculus usuario833970
fuente

Respuestas:

\frac{Γ ⊢ M : Δ}{Γ ⊢ M ≅ M}

$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M}$

$\Gamma\vdash N\cong M$

Un poco contra-intuitivamente, probar que el sistema con conversión mecanografiada es equivalente al que no tiene tipos es muy difícil, y fue resuelto en 2010 por Siles y Herbelin .

cody
fuente

Aquí, "tratamientos modernos" significa "tratamientos de ciencias de la computación que están más interesados en la computación".

Andrej Bauer

Lo suficientemente justo. Casi mencioné las escuelas de teoría de tipos "suecas" versus "francesas", pero no estoy seguro de que esa distinción exista realmente.

cody

No existe tal distinción, como lo demuestra el hecho de que Thierry Coquand vive en Suecia. Todos son computacionales.

Andrej Bauer

@cody: pensé que casi todos los tratamientos modernos de informática utilizan juicios mecanografiados, porque es la forma más conveniente de obtener el eta para pi / sigma. (Ciertamente, Coq y Agda apoyan eso.)

Neel Krishnaswami

@NeelKrishnaswami La conversión mecanografiada es necesaria para que eta tenga sentido en la mayoría de las situaciones, pero tenía la impresión de que podría hacer que la metateoría sea considerablemente más complicada. Tal vez estoy completamente equivocado y en realidad hace que todo sea simple. También está la cuestión de optimizar la verificación de conversión para hacer la menor cantidad de trabajo, incluidas las obligaciones adicionales de verificación de tipo. Seguramente esta sería una gran pregunta de seguimiento.

cody