Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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.
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.
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:
There are theorems which relate these semantics. For instance:
Preservation: If a program
phas typeTandpevaluates top'thenp'has typeT.
This is like soundness (bad things don't happen, namely a program will not become untyped). Another one is:
Progress: If a program
phas typeTthen 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
pandqare denoted by the same mathematical object then they are observationally equivalent.Full abstraction: if
pandqare 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.
