use of models in proving program properties
This is something that has left me puzzled for years. My understanding is that a model is a concrete realization of an abstract structure in terms of some other mathematical structure, such that all the laws from the first are satisfied in the latter. A simple example might be the abstract (algebraic) structure "group" and a concrete realization e.g. the integers with addition. Finding models for abstract theories is certainly useful, for instance it shows that the theory is actually 'inhabited'; it may also shed light on the theory and give us ideas about new theorems that might generalize to the abstract setting. However, nobody would claim that from a theorem about integers I can deduce one for abstract groups in general. But exactly this kind of reasoning appears to be valid when proving things about e.g. the polymorphic lambda calculus (aka System F). For instance, in the famous "free theorems" paper by Wadler, the free theorems appear as a consequence of modeling types in system F as relations (this is most probably oversimplified, i can't remember the details but I think they are not important here). The question is: How can that imply anything about system F itself? Wouldn't it be necessary to prove that these free theorems hold for /all/ models of System F, not just one particular? Besides, if such proofs using a suitable model are really valid, why does it seem to be impossible to 'translate the proof back' from the model to the original system and thus arrive at a direct proof? I am sure there is something wrong with my understanding of these things but I can't figure out what. Cheers Ben
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
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.
participants (2)
-
Ben Franksen -
Danny Gratzer