Teoremas libres, ¿dónde?

8

He encontrado esta aplicación web que te permite generar un teorema gratuito para un tipo dado.

Los teoremas generados cuantifican sobre tipos y relaciones sobre estos tipos. Estos teoremas (fórmulas) son teoremas de qué teoría / sistema lógico? ¿Cómo se relaciona este sistema con la teoría de la ecuación del lenguaje?

lo.logic functional-programming type-systems parametricity logical-relations usuario13264
fuente
3
Esto parece ser un reenvío de la misma pregunta en Stack Overflow , donde se consideró fuera de tema, y ​​obtuvo solo una respuesta superficial que se vincula con el documento "Theorems for Free". De nuevo, este enlace es relevante.
CA McCann
Gracias por la referencia He visto el artículo de Wadler, pero realmente no lo entiendo. Está trabajando con la semántica de cuadros, entonces las relaciones parecen ser entre elementos en estos cuadros. ¿Cómo se relacionan las relaciones entre estos elementos con la lógica equitativa del lenguaje (en el caso de Wadler, Sistema F)? Instancia relaciones con funciones, ¿estas funciones deben ser computables en el Sistema F?
user13264
la aplicación web no funciona, ¿hay espejos en alguna parte?
user833970

Respuestas:

14

Las fórmulas son fórmulas de la lógica de Abadi-Plotkin, que describen en su artículo A Logic for Parametric Polymorphism .

La semántica del Sistema F que Abadi y Plotkin usaron para interpretar su lógica se puede encontrar en Bainbridge, Freyd, Scedrov, el papel de Scott Funmorial Polymorphism .

Neel Krishnaswami
fuente
2
Gracias, el primer artículo parece responder a mi primera pregunta. Cuando uno dice "por parametricidad si I: / \ XX-> X, entonces a. I {A} = I {A '}. A para a: A -> A'", no se dice "if | - I: / \ XX-> X y "| - a: A -> A 'y luego a. I {A} es beta-eta-algo equivalente a I {A '}. un "¿De dónde viene esta relación con la semántica operacional suceden lo que sería un modelo no paramétrico de System F, y no sería inconsistente WRT sus semántica operacional???
user13264
Esta charla muestra un ejemplo de una función no paramétrica (que no se puede expresar en el Sistema F). mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf Por lo demás, debe aprender sobre la correspondencia entre la semántica denotativa y operativa, y la relación de solidez . Un modelo puede contener funciones que no corresponden a programas. Esto viola la abstracción completa, pero no la solidez.
Blaisorblade
7

F

Wadler muestra que, en algunas condiciones, estas transformaciones son inversas entre sí.

Entonces, para responder a su pregunta: los teoremas de forma gratuita se pueden expresar en una forma de lógica de segundo orden, que se describe en el documento mencionado anteriormente.

cody
fuente