Hablando en términos generales, con una integración profunda de una lógica, (1) define un tipo de datos que representa la sintaxis de su lógica, y (2) proporciona un modelo de la sintaxis y (3) demuestra que los axiomas sobre su sintaxis son sólidos con respeto a la modelo. Con una incrustación superficial, omite los pasos (1) y (2), y simplemente comienza con un modelo, y demuestra las implicaciones entre las fórmulas. Esto significa que las incrustaciones superficiales generalmente requieren menos trabajo para despegar, ya que representan un trabajo que normalmente terminaría haciendo de todos modos con una incrustación profunda.
Sin embargo, si tiene una inserción profunda, generalmente es más fácil escribir procedimientos de decisión reflexivos, ya que está trabajando con fórmulas que realmente tienen una sintaxis sobre la que puede recurrir. Además, si su modelo es extraño o complicado, generalmente no desea trabajar directamente con la semántica. (Por ejemplo, si usa la biortogonalidad para forzar el cierre admisible, o usa modelos de estilo Kripke para forzar las propiedades del marco en lógicas de separación o juegos similares). Sin embargo, las incrustaciones profundas casi seguramente lo obligarán a pensar mucho sobre el enlace variable y las sustituciones , lo que llenará tu corazón de ira, ya que esto es (a) trivial y (b) una fuente interminable de molestia.
La secuencia correcta que debe tomar es: (1) intente sobrevivir con una incrustación poco profunda. (2) Cuando eso se agote, intente usar tácticas y citas para ejecutar los procedimientos de decisión que desea ejecutar. (3) Si eso también se agota, abandona y usa una sintaxis de tipo dependiente para tu incrustación profunda.
- Planifique tomarse un par de meses el (3) si esta es su primera vez. Usted va a necesitar para familiarizarse con la fantasía características de su asistente prueba a mantenerse sano. (Pero esta es una inversión que dará sus frutos en general).
- Si su asistente de pruebas no tiene tipos dependientes, quédese en el nivel 2.
- Si su lenguaje de objetos se tipea de forma dependiente, permanezca en el nivel 2.
Además, no intente subir gradualmente la escalera. Cuando decidas subir la escalera de la complejidad, da un paso completo a la vez. Si haces las cosas poco a poco, obtendrás muchos teoremas que son raros e inutilizables (por ejemplo, obtendrás múltiples sintaxis a medias y teoremas que mezclan la sintaxis y la semántica de formas extrañas), lo que obtendrás finalmente tiene que tirar.
EDITAR: Aquí hay un comentario que explica por qué subir la escalera gradualmente es tan tentador y por qué conduce (en general) al sufrimiento.
A⋆BIA⋆B⟺B⋆A(A⋆B)⋆C⟺A⋆(B⋆C)(I⋆A)⋆(B⋆C)A⋆(B⋆(C⋆I))
⋆
¡Esto es cierto y funciona! Sin embargo, tenga en cuenta que la conjunción también es ACUI, y también lo es la disyunción. Entonces pasará por el mismo proceso en otras pruebas, con diferentes tipos de datos de lista, y luego tendrá tres sintaxis para diferentes fragmentos de lógica de separación, y tendrá metateoremas para cada uno de ellos, que inevitablemente serán diferentes, y te encontrarás queriendo un metateorema que probaste para separar la conjunción para la disyunción, y luego querrás mezclar sintaxis, y luego te volverás loco.
Es mejor apuntar al fragmento más grande que pueda manejar con un esfuerzo razonable, y simplemente hacerlo.
Es importante entender que hay un espectro de profundo a poco profundo. Si modelas profundamente las partes de tu lenguaje que de alguna manera deberían participar en algún argumento inductivo sobre la construcción del mismo, el resto queda mejor en la visión superficial de la semántica directa del sustrato de la lógica.
Por ejemplo, cuando desea razonar sobre Hoare Logic, puede modelar el lenguaje de expresión de una manera superficial, pero el esquema del lenguaje de asignar si es un tipo de datos concreto. No necesita ingresar la estructura de x + y o a <b, pero necesita trabajar con
while
etc.En las otras respuestas hubo alusiones a tipos dependientes. Esto recuerda el antiguo problema de representar idiomas con ligantes de una manera sensata, de modo que sean lo más superficiales posible, pero aún admitan algunos argumentos inductivos. Mi impresión es que el jurado todavía está juzgando sobre todos los diferentes enfoques y documentos que han surgido en los últimos 10-20 años sobre ese tema. El "desafío POPLmark" para las diferentes comunidades de asistentes de prueba también fue sobre eso en cierta medida.
Curiosamente, en el HOL clásico sin tipos dependientes, el enfoque HOL-Nominal de C. Urban funcionó bastante bien para la encuadernación superficial, aunque no alcanzó los cambios culturales en estas comunidades de formalización del lenguaje de programación.
fuente