Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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?

share|improve this question
3  
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. –  C. A. McCann Jan 8 '13 at 13:06
    
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? –  user13264 Jan 8 '13 at 13:16
    
I'm not sure what you mean by 'free theorem', but to answer the pun in your question I don't believe in freedom, only in 'tight control' vs 'loose control'. The thing is that both freedom and tight control can be diverted to provoke chaos, while this seems harder to achieve with loose control if the majority shows initiative and acts rationally.. –  NisaiVloot Apr 3 at 16:28

2 Answers 2

up vote 13 down vote accepted

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.

share|improve this answer
2  
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? –  user13264 Jan 8 '13 at 17:07
    
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. –  Blaisorblade Mar 22 at 2:23

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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