Freie Theoreme, wo?

8

Ich habe diese Webanwendung gefunden, mit der Sie einen kostenlosen Satz für einen bestimmten Typ erstellen können.

Die generierten Theoreme quantifizieren über Typen und Beziehungen zu diesen Typen. Diese Sätze (Formeln) sind Sätze von welcher Theorie / welchem ​​logischen System? In welcher Beziehung steht dieses System zur Gleichungstheorie der Sprache?

lo.logic functional-programming type-systems parametricity logical-relations user13264
quelle
3
Dies scheint ein Repost der gleichen Frage zu Stack Overflow zu sein , wo sie als nicht zum Thema gehörend angesehen wurde und nur eine flüchtige Antwort erhielt, die auf das Papier "Theorems for Free" verweist. Auch dieser Link ist relevant.
CA McCann
Danke für den Hinweis. Ich habe Wadlers Zeitung gesehen, aber ich verstehe sie nicht wirklich. Er arbeitet mit der Rahmensemantik, dann scheinen die Beziehungen zwischen Elementen in diesen Rahmen zu bestehen. In welcher Beziehung stehen die Beziehungen zwischen diesen Elementen zur Gleichungslogik der Sprache (in Wadlers Fall System F)? Er instanziiert Beziehungen zu Funktionen. Müssen diese Funktionen in System F berechenbar sein?
user13264
Die Web-App ist ausgefallen. Gibt es irgendwo Spiegel?
user833970

Antworten:

14

Die Formeln sind Formeln der Abadi-Plotkin-Logik, die sie in ihrer Arbeit A Logic for Parametric Polymorphism beschreiben .

Die Semantik von System F, mit der Abadi und Plotkin ihre Logik interpretierten, findet sich in Bainbridge, Freyd, Scedrov, Scotts Artikel Functorial Polymorphism .

Neel Krishnaswami
quelle
2
Danke, das erste Papier scheint meine erste Frage zu beantworten. Wenn man sagt "durch Parametrizität, wenn I: / \ XX-> X, dann a. I {A} = I {A '}. A für a: A -> A'", sagt man nicht "wenn | - I: / \ XX-> X und "| - a: A -> A 'dann a. I {A} ist Beta-eta-etwas-Äquivalent zu I {A '}. a "? Wo kommt diese Beziehung zur operativen Semantik vor? Was wäre ein nicht parametrisches Modell von System F, und wäre es nicht inkonsistent mit seiner operativen Semantik?
user13264
Dieser Vortrag zeigt ein Beispiel für eine nicht parametrische Funktion (die in System F nicht ausgedrückt werden kann). mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf Im Übrigen müssen Sie die Entsprechung zwischen denotationaler und operativer Semantik und das Verhältnis der Solidität kennenlernen . Ein Modell kann Funktionen enthalten, die keinen Programmen entsprechen. Dies verletzt die vollständige Abstraktion, aber nicht die Solidität.
Blaisorblade
7

Ich mag Wadlers Artikel The Girard-Reynolds Isomorphism sehr gern, der zeigt, dass es eine Übersetzung von system zu und von Predicate Logic zweiter Ordnung gibt (eine Version mit Typen höherer Ordnung). Eine Richtung ist "Abhängigkeitslöschung", eine wichtige Idee bei abhängigen Typen, und die andere ist der "Parametrizitätssatz" oder der Satz ohne Typ eines Typs.F

Wadler zeigt, dass diese Transformationen unter bestimmten Bedingungen umgekehrt sind.

Um Ihre Frage zu beantworten: Die kostenlosen Theoreme können in Form einer Logik zweiter Ordnung ausgedrückt werden, die in dem oben genannten Artikel beschrieben wird.

Cody
quelle