[Haskell-cafe] use of models in proving program properties

[Ben Franksen]

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.
>