5
$\begingroup$

I've been wondering if there's a connection between "good logics" and "good programming languages". It seems that logics are shown to be "locally sound and complete" whereas programming languages are shown to be "type safe" (preservation and progress).

If there's a relationship could you please explain it and give some references so that I can follow up on it.

$\endgroup$
  • 1
    $\begingroup$ A good starting point is the Curry-Howard correspondence. $\endgroup$ – Alexis Jun 1 '16 at 2:19
  • 2
    $\begingroup$ Do you mean "local soundness" and "local completeness" in the sense that Frank Pfenning uses them (e.g., cs.cmu.edu/~fp/courses/15317-f08/lectures/03-harmony.pdf)? $\endgroup$ – Noam Zeilberger Jun 1 '16 at 16:27
  • $\begingroup$ @NoamZeilberger yes, that's what I was thinking of. $\endgroup$ – Steven Shaw Jun 2 '16 at 2:42
  • $\begingroup$ Okay, that is a bit more specific than the concepts of "soundness" and "completeness" relative to a model as suggested in the title of your question (and as in Andrej's answer). I'll try to address those in another answer below... $\endgroup$ – Noam Zeilberger Jun 2 '16 at 7:43
6
$\begingroup$

The concepts of "local soundness" and "local completeness" (which is Frank Pfenning's terminology, originally introduced in his paper with Rowan Davies, A Judgmental Reconstruction of Modal Logic) are a bit more specific than the standard concepts of "soundness" and "completeness" relative to a model as suggested in the title of your question (and as in Andrej's answer). Under the Curry-Howard correspondence, local soundness and local completeness correspond exactly to $\beta$-reduction and $\eta$-expansion of typed terms, respectively.

These are not quite preservation and progress, but preservation is closely related to (and usually relies on the fact that) $\beta$-reduction is type-preserving. The type safety theorem that results from combining preservation + progress is somewhat related to "global soundness" (in the sense of these lecture notes), which is just another name for the normalization/cut-elimination theorem for (a proof system for) a logic. Type safety is a weaker statement, though, since combining preservation with progress only guarantees that a term $t:A$ will either eventually reduce to a value $t \leadsto^* v$ such that $v:A$ or else fail to terminate. In contrast, the normalization theorem for a logic says that any proof $\pi$ of $A$ can definitely be reduced to a normal proof of $A$.

PL designers have typically paid less attention to $\eta$-expansion, although this is starting to change in languages with more sophisticated type systems (such as proof assistants). In such languages, $\eta$-expansion (and hence local completeness) is closely related to the definitions of equality and/or subtyping.

There is a bit more discussion of local soundness and completeness and their Curry-Howard interpretation in Pfenning's Logical Frameworks — A Brief Introduction.

$\endgroup$
7
$\begingroup$

Soundness and completeness of logic are semantic notions which say that logic and its models fit together nicely. We can find similar theorems in the theory of programming languages but they are not necessarily about mathematical models of programming languages.

A general way to understand soundness is that "bad things do not happen" (logic does not prove invalid things). A general way to understand completeness is that "good things happen" (there are sufficiently many models).

A programming language typically has several kinds of semantics:

  • static semantics explains how to assign types to programs
  • dynamics (operational) semantics explains how to run programs, more or less
  • denotational semantics is more akin to models in logic and it explains how to map programs to mathematical objects.

There are theorems which relate these semantics. For instance:

Preservation: If a program p has type T and p evaluates to p' then p' has type T.

This is like soundness (bad things don't happen, namely a program will not become untyped). Another one is:

Progress: If a program p has type T then it is either a value (it's finished) or it has another step of execution.

This is like completeness (good things happen, namely a program will make the next step).

When we put these two together, we get safety.

Another kind of theorems relates denotational semantics to operational semantics. For instance:

Adequacy: if p and q are denoted by the same mathematical object then they are observationally equivalent.

Full abstraction: if p and q are observationally equivalent then they are denoted by the same mathematical object.

Adequacy says that the model is not too small and full abstraction that it is not too big. It makes a bit less sense to relate these two to soundness and completeness, but if I had to, I would say that full abstraction is like soundness and adequacy is like completeness.

$\endgroup$
  • $\begingroup$ Thanks for responding. I had another thought since posting the question. My understanding is that for logics, locally sound and complete is enough to show consistency. For PLs, I believe this would make them decidable terminating. So perhaps there's a small gap between a good logic and a good PL? Also, would you recommend and books or other references. Cheers! $\endgroup$ – Steven Shaw Jun 2 '16 at 2:57
  • 4
    $\begingroup$ A good general introduction to PL is Bob Harper's Practical Foundations for Programming Languages and Benjamin Pierces Types and Programming Languages. $\endgroup$ – Andrej Bauer Jun 2 '16 at 7:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.