use of models in proving program properties

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

use of models in proving program properties

Ben Franksen
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

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: use of models in proving program properties

Danny Gratzer-2
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.
Reply | Threaded
Open this post in threaded view
|

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


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