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

[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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170612/3e91570c/attachment.html>