Teoremas livres, onde?

8

Eu encontrei este webapp que permite gerar um teorema gratuito para um determinado tipo.

Os teoremas gerados quantificam tipos e relações nesses tipos. Esses teoremas (fórmulas) são teoremas de qual teoria / sistema lógico? Como esse sistema se relaciona com a teoria equacional da linguagem?

lo.logic functional-programming type-systems parametricity logical-relations user13264
fonte
3
Parece ser uma repostagem da mesma pergunta no Stack Overflow , onde foi considerada fora de tópico, e obteve apenas uma resposta superficial, vinculada ao artigo "Teoremas de graça". Novamente, esse link é relevante.
CA McCann
Obrigado pela referência. Eu vi o jornal de Wadler, mas realmente não o entendo. Ele está trabalhando com semântica de quadros, então as relações parecem estar entre os elementos desses quadros. Como as relações entre esses elementos se relacionam com a lógica equacional da linguagem (no caso de Wadler, Sistema F)? Ele instancia relações com funções, essas funções precisam ser computáveis ​​no Sistema F?
precisa saber é o seguinte
o aplicativo da web está inoperante, existem espelhos em algum lugar?
user833970

Respostas:

14

As fórmulas são fórmulas da lógica de Abadi-Plotkin, que descrevem em seu artigo A Logic for Parametric Polymorphism .

A semântica do sistema F que Abadi e Plotkin usaram para interpretar sua lógica pode ser encontrada em Bainbridge, Freyd, Scedrov, artigo de Scott Funymorial Polymorphism .

Neel Krishnaswami
fonte
2
Obrigado, o primeiro artigo parece responder à minha primeira pergunta. Quando alguém diz "por parametridade se eu: / \ XX-> X, então a. I {A} = I {A '}. A para a: A -> A'", não se diz "se | - I: / \ XX-> X e "| - a: A -> A 'então a. I {A} é beta-eta-algo-equivalente a I {A '}. um "Onde é que essa relação com semântica operacional acontecer Qual seria um modelo não-paramétrico de Sistema F, e não seria wrt inconsistente sua semântica operacionais??
user13264
Esta palestra mostra um exemplo de uma função não paramétrica (que não pode ser expressa no Sistema F). mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf Quanto ao resto, você precisa aprender sobre a correspondência entre a semântica denotacional e operacional e a relação da solidez . Um modelo pode conter funções que não correspondem a programas. Isso viola a abstração total, mas não a solidez.
Blaisorblade 22/03
7

F

Wadler mostra que, em algumas condições, essas transformações são inversas uma da outra.

Então, para responder à sua pergunta: os teoremas de graça podem ser expressos em uma forma de lógica de segunda ordem, descrita no artigo acima.

cody
fonte