Hi Danny thanks for your answer. It confirms the suspicion I had, namely that my understanding of what a model is was wrong or perhaps taken from the wrong context. Wikipedia says (https://en.wikipedia.org/wiki/Model_theory): "A set of sentences in a formal language is called a theory; a model of a theory is a structure (e.g. an interpretation) that satisfies the sentences of that theory." In your diction, this definition of a model implies completeness, but not (necessarily) soundness and this is how I understood the word. So, model means something different in CS or Type Theory than in Model Theory? More concretely, the relational model of System F really is sound (in the sense in which you defined it below), yes? So, using the above Wikipedia definition, it would make more sense to say that System F is a model of "types as relations"... (sorry for being unable to express this more precisely). Cheers Ben Am 12.06.2017 um 11:09 schrieb Danny Gratzer:
Let me fix some notation for my answer, we'll say that our theory validates some proposition/judgment P with |- P and that some model M validates a proposition with M |= P. Now, when we define a model there are two properties which are mainly of interest.
- Soundness: the most basic property of a model is that if M |= P then |- P. - Completeness: if |- P then M |= P
Do note that which direction is "soundness" and which direction is "completeness" varies wildly between different sources. The idea with something like System F is that we'll establish a sound model and, knowing this, it's sufficient to show that our model validates a given proposition in order to conclude that it holds in System F. In parametricity papers for instance "P" would be something expressing "this program is contextually equivalent to that program". Now most models in programming languages fail to complete, meaning that they might not capture every aspect of the theory in question. When we're discussing mainly equality, this property is called "full abstraction" and is sort of the "holy grail" for a model. Don't let this suggest that sound but incomplete models aren't useful, to the contrary they are often the only known way to establish certain equivalence results when it comes to programming languages. Most logical relations (a form of PER model if you like) for general references are incomplete if we disallow appeals to things like biorthogonality or closure under contextual equivalence.
Your example with groups is sort of canonically the opposite, there you have a complete but unsound model. This direction is useful for abstract algebra where the goal is to understand the model using the theory. In programming languages we usually have the opposite problem, we don't understand the theory very well but we have a comparatively strong understanding of the model.
As for why it's a useful trick to construct models in the first place, remember that directly showing the proof is often incredibly difficult. While it may be in theory possible to circumvent a model it's often the only feasible way of proving something.
Hopefully some of that makes some amount of sense.
Danny
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.