10 ms·

There are basically two important results for type systems, soundndess and completeness. Soundness means that every program that typechecks is valid. Completen

• s_kilk 9y ago
  I'm curious, given Godels incompleteness theory, isn't it impossible to have both soundness and completeness in the same language?
  • karatinversion 9y ago
    Gödel's incompleteness is for proof systems for languages which contain enough arithmetic to express its own syntax. Lots of things don't go this far - first order predicate logic is sound and complete, for example (see Gödel's completeness theorem(!)).
    • pas 9y ago
      Could you please expand on the soundness and completeness of first order logic? Isn't that false generally? Because you need a deductive/axiom system, so that you can ask the question of completeness/soundness. And ZFC is too strong, hence cannot prove its soundness and correctness at the same time. But you can formalize weaker systems in first order logic, that are provably complete and sound.
      • gpm 9y ago
        (It's been a year and a half since I took a course on this, so I apologize for any mistakes) You do need to define a deductive/axiom system before you can ask the question. We can use a few different standard deductive systems. We require that the axioms are sound. Then the system is complete. (I think one should also always be able to prove false if the axioms aren't sound... but I don't recall proving that) ZFC isn't too strong. That sounds like a contradiction, but it isn't, because we don't have a rich enough vocabularly in first order logic to state the problematic statements that make it either inconsistent or incomplete in stronger logic systems. Every true statement you can state about ZFC in first order logic is provable.
        • indexerror 9y ago
          > It's been a year and a half since I took a course on this Can you please recommend a MOOC/resource for learning more about this?
          • gpm 9y ago
            My only real exposure to it is the course I took, csc438 at UofT taught by Steven Cook. There are pretty complete notes for the course as well as assignments here [0], but not videos or planned lessons. You certainly could learn about it by reading them, but I don't know if it would be the most efficient way. [0] http://www.cs.toronto.edu/~sacook/csc438h/ http://www.cs.toronto.edu/~sacook/csc438h/
        • enugu 9y ago
          We can state a lot of things in first order logic about natural numbers or set theory which are not provable (in some given set of axioms like Peano axioms or ZFC, you can extend the axiom set but then one can generate a new unprovable statement if not a contradiction). The issue here is first order logic is complete for statements that are true for all models of the axioms. As an example, imagine a infinite land which cant be completely described by any computable map(a programmable set of facts about the territory). The map will only tell you some true things about the territory. But we can say this - if there is some statement that the map cant decide, then there are two different territories for both of which the map is accurate, and the statement is true for one territory and false for another. So the deductive system is complete description of true statements which hold for all territories for which the map applies. But if we are interested in a single given territory, no computable system of facts suffices. For example deciding whether a diophantine equation has solutions in the standard set of Natural Numbers or a more familiar example for this site, whether a program halts. No computable deductive system(ie there is a program which generates all deductions) will suffice.
    • varjag 9y ago
      Propositional calculus is sound and complete, first order predicate logic isn't.
      • jonnycomputer 9y ago
        fol logic is sound and complete (and effective). second order logic is not.
        • mcguire 9y ago
          For reference: https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...
  • snnw 9y ago
    Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.
    • vanderZwan 9y ago
      Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.
      • lmm 9y ago
        It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?
  • baq 9y ago
    you can design a complete and sound type system in which any program can be checked in polynomial time. https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
  • vilhelm_s 9y ago
    Yes, although I would appeal to Rice's theorem rather than Gödel.
• davidgay 9y ago
  Note that most common type systems "crash" type-checked programs at runtime: null-pointer check failures, array-bound check failures, and (even, Java) co-variant array write check failures. So the line is fairly fuzzy.
  • _asummers 9y ago
    Or just silently fail! Knowing the history of the Collections API and generics in Java, I know WHY this is like this, but Map.get taking an Object has resulted in way more bugs in previous code bases than I'd like to think about. If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map. You can of course wrap that call behind functions that DO check the proper input type, but until you've been burnt by it you might not think to do that.
    • brabel 9y ago
      > If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map Map map = new HashMap(); map.put("one", 1); class Whatever {} Map<Whatever, Integer> whateverToIntMap = (Map<Whatever, Integer>) map; Integer i = whateverToIntMap.get("one"); System.out.println("i = " + i); Prints: i = 1 That's a consequence of generics type-erasure for backwards compatibility with non-generic code, so there _is_ a reason for `get` accepting any Object.
      • _asummers 9y ago
        Like I said, I know the history and why it exists. I learned Java before 1.5 came out. That API existed long before generics did (I think 1.0 or earlier). If they had designed the language with generics in mind, they would have probably done it differently; hindsight is 20/20. Doesn't make it not a suboptimal API. I don't think there's a good way to fix it this late in the game without breaking old code, but such are the warts of backwards compatibility.
  • deleted 9y ago
• tel 9y ago
  While this is true, it's critical to note that "valid" here doesn't mean "valid as in it follows the intention of the programmer who wrote it" but instead "valid as in it either terminates in a well-defined error condition or completes to an identically-typed result" (preservation and progress). The engineering constraint is to ensure that the design and logic of the types themselves enable preservation-and-progress-validity to enforce meaningful semantic constraints. A sound and complete type system can still say things that aren't practically meaningful.
• jackfoxy 9y ago
  > Soundness means that every program that typechecks is valid. Completeness means that every valid program can be typed. I like this definition. Can someone link to an authoritative article that elaborates on this statement?
  • eslaught 9y ago
    This is a pretty standard definition (though sometimes the words get swapped). E.g. you see a very similar sentence in Wikipedia: > Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable. https://en.wikipedia.org/wiki/Soundness#Relation_to_completeness https://en.wikipedia.org/wiki/Soundness#Relation_to_complete... You could probably follow the references there to more authoritative sources.
    • jackfoxy 9y ago
      I was looking for something specific to type systems, but this is a good start.
    • Izkata 9y ago
      Ehh, no. The definition on Wikipedia - at least the part you quoted, the rest is too jargony for me - is circular (and makes me think it's incorrect/missing something). The GP's sentence would require a third link, which missing means it isn't circular. Programs that can be typed will not necessarily be typecheck-able successfully. (I hope what I'm trying to get at makes sense and I'm not causing more confusion... what I have in mind is things like Java's ClassCastException - everything's typed, the typecheck passes, but it wasn't actually successful. Going by the Wikipedia quote, it would mean it wasn't actually possible for this exception to be thrown.)
      • a-saleh 9y ago
        I think this might be, because the definition seems to stem from mathematical notion of logic. And logicians usually want to have their logics sound, because if you can prove false statements, what is the point of your logic, right? So to distinguish between sound/unsound typesystem, I would look at it as if it were logic, where types are my theorems, and typechecking is attempt to find a proof. Of course, type-system for a language has to have some compromises, Java explicitly tells you, that even typechcecked program still will have runtime exceptions (like ClassCastException). In haskell you can still fall into an infinite loop, even though all the types flow through the system as expected :-)