Implementación de idiomas "internos"

11

Una de las consecuencias más prácticas de la correspondencia "Curry-Howard-Lambek" es que la sintaxis de muchas lambda-calucli / lógicas puede usarse para realizar construcciones en una categoría suficientemente estructurada.

Por ejemplo, la Geometría diferencial sintética tiene modelos en topoi que contienen e incrustan la categoría de múltiples suaves, por lo que puede usar lógica de orden superior para construir funciones suaves y resolver ecuaciones diferenciales.

Como otro ejemplo, en este documento , se dan cuenta de que la "indexación por pasos" en realidad solo funciona con preajustes sobre los naturales (otro topos), por lo que puede usar la sintaxis de la lógica de orden superior para definir relaciones lógicas indexadas por pasos sin el tedioso manipulación de pasos.

Finalmente, Andrej Bauer muestra en esta pregunta de MO que puedes hacer mucho con el "lenguaje interno" de los topos de los gráficos.

Mi pregunta es, ¿ alguien se ha dado cuenta de esta visión literalmente en un probador de teoremas ? Por ejemplo, si demuestro que una categoría que me importa es Cerrada cartesiana, podría pasar al "modo interno" donde escribo la sintaxis de cálculo lambda (con algunos axiomas específicos del modelo) y luego puedo volver al "modo externo" y manipularlos como objetos en mi modelo?

En el extremo, incluso me gustaría contar con teoría y lógica de orden superior, para poder escribir mis relaciones lógicas indexadas por pasos sin pasos, o enseñar mecánica clásica con un probador de teoremas usando SDG. Esto me parece una idea muy poderosa, ya que alguien podría implementar la teoría del tipo dependiente extensional una vez y proporcionar herramientas agradables y luego usarla con aplicaciones muy diferentes como se describió anteriormente.

Max nuevo
fuente
Solo por razones de claridad: ¿se pregunta si alguien ha reescrito alguna vez una teoría matemática en el lenguaje interno de la categoría subyacente (por usar el comprobador de teoremas para probar cosas en tales teorías matemáticas)? ¿O le interesa saber si alguien ha hecho teoría de modelos en la teoría de tipos (de algún tipo de categoría)?
Giorgio Mossa
No estoy preguntando sobre el trabajo que la gente ha hecho en un lenguaje interno particular en un probador de teoremas (aunque las referencias para eso serían bienvenidas). Me pregunto si alguien ha hecho el trabajo de implementar "Lenguajes internos" como esencialmente DSL en un comprobador de teoremas para poder usar el lenguaje interno para cualquier modelo en particular que me interese y obtener todos los beneficios de una buena sintaxis. Para los CCC esto parece fácil ya que la sintaxis se puede expresar fácilmente en Coq / Agda, etc., pero Topoi parece más difícil.
Max New

Respuestas:

7

En Extending Type Theory with Forcing, de Guilhem Jaber, Nicolas Tabareau y Matthieu Sozeau, 2012, el forzamiento intuicionista se presenta como una internalización de la construcción previa a la intemperie, implementada como una traducción de preservación de tipo al estilo de la traducción de parametricidad de Bernardy y Lasson .

Esto significa que puede definir términos en su teoría de tipos habitual y luego "traducirlos" en una "capa forzada" donde se interpretan como traducciones en un tipo de traducción diferente. Por ejemplo, la traducción inducida por la indexación sobre números naturales decrecientes le permite usar sus términos habituales en una teoría posterior a la traducción donde una latermodalidad es definible. Esto suena bastante cercano a su idea de trabajar internamente en los topos de los árboles.

Parece que tienen un plugin Coq nuevo y más simple que implementa estas ideas en CoqHott / coq-forcing , y en particular SI.v construye esta traducción forzada para la indexación por pasos. Desafortunadamente, si bien hace el trabajo de construir el modelo, no hay ningún ejemplo de usarlo para definiciones indexadas por pasos en la práctica (lo único traducido en lugar de definido en la capa forzada es Forcing Translate eq, lo que no es terriblemente informativo). Podría intentar experimentar para ver qué tan conveniente es usarlo.

gasche
fuente
5

Si va a trabajar solo en el idioma interno, puede usar un asistente de prueba. Hay un tecnicismo menor de tener o no tener conjuntos de poder, ya que los asistentes de prueba son típicamente teorías de tipo, pero Coq Propes consistente con una interpretación de Coq en un topos.

Sin embargo, sugiere utilizar la máquina como una especie de herramienta de traducción que lo llevaría del lenguaje interno a la interpretación en un modelo. Esta es una buena idea, excepto que creo que no sería tan útil como cabría esperar. Es cierto que la traducción del lenguaje interno al modelo es mecánica, pero desafortunadamente produce traducciones complicadas que necesitan mucho masaje antes de que sean útiles. (Si alguna vez trató de usar la interpretación de Lawvere-Tierney de la lógica de topos en un topos de gavilla, lo sabrá).

Hay un problema más, a saber, la traducción inversa . A menudo comenzamos con un concepto u objeto conocido en el modelo, y nos gustaría una buena descripción o axomatización del mismo en el lenguaje interno. Esto es típicamente trabajo duro y matemática real. No veo cómo los asistentes de prueba actuales podrían ayudar.

En el aspecto técnico de las cosas, uno debería preocuparse por formalizar:

  • la sintaxis y las reglas del lenguaje interno
  • el modelo
  • la interpretación

λ

En resumen, usar un asistente de prueba para ayudar a verificar que no estás haciendo nada malo en el lenguaje interno es una buena idea (de hecho, es una muy buena idea, como lo atestigua la teoría del tipo de homotopía, donde utilizamos Coq y Agda desarrollar nuevos teoremas que luego no fueron formateados en inglés), pero es poco probable que usarlo para obtener declaraciones sobre modelos funcione sin mucho trabajo adicional. ¡Lo que no quiere decir que no deberías intentarlo!

Andrej Bauer
fuente
¿Tiene una referencia para Type Theory + Prop ~~ topos? Esta era mi intuición, pero no he visto a nadie más decirlo hasta ahora.
Max Nuevo
Además, para las lógicas específicas del modelo, los axiomas específicos serán específicos para los modelos, pero la estructura de la lógica general sigue siendo solo lógica de orden superior, ¿verdad? Me imagino que caracterizaría externamente las características de su modelo (como el Functor de la próxima vez en el documento de indexación por pasos) y luego las reflejaría como axiomas en su idioma interno. Encontrar axiomatizaciones agradables y completas aún sería una matemática difícil, pero espero que la máquina pueda automatizar parte de la plomería.
Max Nuevo
Para la indexación por pasos, en particular, tendría sentido extender la lógica topos con un operador modal. En general, esto será una característica de cualquier situación en la que te preocupes por una subtopos, o si tienes una (co) mónada que deseas estudiar, etc.
Andrej Bauer
Para la teoría de tipos + Prop, simplemente observa cada regla y ve que si interpreta Prop como el clasificador de subobjetos, todo es válido en un topos.
Andrej Bauer