8
$\begingroup$

I've found this webapp which lets you generate a free theorem for a given type.

The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which theory/logical system? How does this system relate to the equational theory of the language?

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ This seems to be a repost of the same question on Stack Overflow, where it was considered off-topic, and garnered only a cursory answer linking to the "Theorems for Free" paper. Again, this link is relevant. $\endgroup$ – C. A. McCann Jan 8 '13 at 13:06
  • $\begingroup$ Thanks for the reference. I've seen Wadler's paper, but I don't really understand it. He's working with frame semantics, then the relations seem to be between elements in these frames. How does the relations between these elements relate to the equational logic of the language (in Wadler's case, System F)? He instantiates relations with functions, do these functions need to be computable in System F? $\endgroup$ – user13264 Jan 8 '13 at 13:16
  • $\begingroup$ the web app is down, are there mirrors anywhere? $\endgroup$ – user833970 Jun 21 '18 at 18:07
14
$\begingroup$

The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism.

The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism.

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ Thanks, the first paper seems to answer my first question. When one says "by parametricity if I : /\X.X->X, then a . I{A} = I{A'} . a for a : A -> A'", isn't one saying "if |- I : /\X.X->X and "|- a : A -> A' then a . I{A} is beta-eta-something-equivalent to I{A'} . a"? Where does this relationship with operational semantics happen? What would be a non-parametric model of System F, and wouldn't it be inconsistent w.r.t. its operational semantics? $\endgroup$ – user13264 Jan 8 '13 at 17:07
  • $\begingroup$ This talk shows an example of a non-parametric function (which can't be expressed in System F). mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf For the rest, you need to learn about the correspondence between denotational and operational semantics, and the relation of soundness. A model can contain functions which don't correspond to programs. This violates full abstracion, but not soundness. $\endgroup$ – Blaisorblade Mar 22 '14 at 2:23
7
$\begingroup$

I'm quite fond of Wadler's paper The Girard-Reynolds Isomorphism which shows that there is a translation from system $\mathrm{F}$ to and from Second Order Predicate Logic (a version with higher-order types). One direction is "dependency erasure", an important idea in dependent types, and the other is the "parametricity theorem" or theorem-for-free of a type.

Wadler shows that in some conditions, these transformations are inverses of each other.

So to answer your question: the theorems-for-free can be expressed in a form of second-order logic, which is described in the aforementioned paper.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.