Hacker News Reader

Comment by thaumasiotes | Hacker News Reader

> It's sound (Rejects all incorrect programs), decidable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect).

Isn't that the definition of "semidecidable" as distinct from "decidable"? A decidable question is one where you can determine the answer, whatever that answer may be. A semidecidable question is one where, if the answer is yes, you can determine that, and if the answer is no, you may not be able to determine that.

If you can always show that a program is incorrect, but you can't necessarily show that a program is correct, then the correctness of a program isn't decidable.

View on HN

Decide-ability here means "Can we come to an answer in a known amount of steps". If you have an algorithm for type checking; then that answer is yes! You're _always_ able to come up with an answer that is yes or no.

For example the following algorithm is for typechecking is decideable:

    typechecks :: Program -> Bool
    typechecks _ = false

We always come to decision. There is no "semi" here. Just a clear yes/no answer.

The algorithm is even sound. It rejects all incorrect programs.

However it is not complete. It might also reject correct programs (In this case it rejects all correct programs).

Of course you want a as little conservative typechecker without getting into trouble. But it's always conservative to some extent. Preferably you would both be sound _and_ complete. But the problem is that any reasonable logic system can't proof its own consistency. Hence we can't have both. However we can get "as close as we possibly can".

> We always come to decision. There is no "semi" here.

That's not really how I understand the "semi" in the terminology. For a decidable question, you can recognize when the answer is yes, and you can recognize when the answer is no. For a semidecidable question, you can recognize when the answer is yes.

It doesn't take much of a stretch to describe that as cutting your capabilities in "half".

The way I usually think about this is that with full decidability, you can rule something in or out. With semidecidability, you can rule something in, but you can't rule things out.

That framework extends well to the situation described above, where if the compiler chooses to compile a program, then the typing in that program was valid, and if the compiler chooses to complain about the typing, we can't draw any conclusions. It doesn't match your example; you can't rule anything in or out.

I believe you're explaining what a computable function is. A decidable set S of a type T is defined to be one for which there is a computable function f : T -> Bool such that the set of values x with f x = true is equal to S. A semidecidable set S of a type T is defined to be one for which there is a partial computable function f : T -> Bool such that whenever x is in S, then f x is computable and equals true.

Given a definition for a well-typed program, you get a set W of Program of the well-typed programs. You can ask whether W is decidable or semidecidable -- i.e., whether there is some (partial) computable function f : Program -> Bool with the above properties.

The example you give is certainly computable, but it has nothing to do with the set W, so it says nothing about (semi)decidability of the typechecking decision problem.

However, it is a valid trying to find the largest subset of W that is (semi)decidable. Or trying to redefine what it means to be well-typed so that it is (semi)decidable!

One interesting case of a programming language without a semidecidable typechecking problem is Lean. The typechecker they've implemented will both reject or time out on valid programs (so the typechecker is at least a computable function in a sense), but in practice these cases don't really occur.

Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. It's the same as having a generator that generates every correct formula eventually.

In my opinion, OP is incorrect and those systems are sound but indecidable.

> Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer.

By this definition, program incorrectness isn't semidecidable either - the compiler will accept all correct [incorrect] formulas, and will either reject or accept incorrect [correct] formulas.

Not really, because for undecidable problems semidecidability can only hold one-way. If it held in both ways then the language would be decidable.

Take the Halting program for example: For a program p which halts, you can determine whether it will halt in finite time (because by definition it halts). However, there is no semidecidable algorithm for "this program runs infinitely long".

I don't understand what you're trying to say. What are you contradicting with "Not really"? The claim above you is "by this definition, program incorrectness isn't semidecidable either". You're saying that it is?

Reply on news.ycombinator.com