[Question][Hw0-3] Incompleteness in programming languages

[Allgot]

Hello, now I'm trying to understand 'incompleteness' concept and apply this to programming languages.

From my understanding, if a simple language containing basic arithmetic operations is given, there should be a statement that is true but cannot be proven by Gödel's incompleteness theorems. Then, this statement $S$ must not be written by both of big-step and small-step operational semantics.

Am I right? Is there really such a case in reality?

[KihongHeo]

Hello,

Let us consider a type system. Typical type systems are so-called sound but incomplete. This is conceptually the same as Godel's incompleteness.

Suppose your goal is to prove a given program is well-typed or not. However, you cannot make a type system that is sound and complete for Turing-complete languages. (slides 22-23 in lecture3.pdf). So, we typically design and implement a sound type system. That means that there always exists a program that is actually well-typed but you cannot prove automatically (i.e., with an algorithm) the correctness. In general, for any non-trivial property, this is true.

Godel mentioned this point using math (i.e., Peano arithmetics) but Turing proved the same thing with Turing machines (i.e., programs).

Sorry but I don't understand your second paragraph regarding big-step and small-step. Let me know if you are still not clear.

[Allgot]

Sorry for incomplete question, and thank you for the answer! Now I understand the real world incompleteness in programming language.

But still there are some unclear points, so let me clarify the second paragraph more. In short, how can we write the statement $S$ which is true but cannot be proven in operational semantics? Let's think about a simple imperative language in lecture2.pdf(4/33). Because we cannot derive $S$ from the axioms (in here, arthimetic/boolean expressions, commands) using inference rules, we cannot write $S$ in big-step semantics. Also, since there's no way to get $S$ from axioms, we cannot write $S$ in small-step semantics too. Then is it any other way of describing this $S$?

Or does not incompleteness theorems hold in operational sematics? Thank you.

[KihongHeo]

OK. But some things are unclear in your question.

First, what do you mean by

we write the statement $S$ which is true but cannot be proven in operational semantics

Is $S$ a program statement such as x := 1; y := x + 1? What does that mean by truth of a program execution?

If I understand correctly, your question may be as follows:

• You view the semantics of a programming language as a proof system (as we did in big-step operational semantics)
• By true, you mean there exists a well-defined program.
• By cannot be proven in operational semantics, you mean we cannot describe the operational semantics of the well-defined program.

If so, the answer is as follows:

• Big-step operational semantics cannot describe non-terminating programs: x = 0; while (true) { x = x + 1 } (try it!)
• Small-step operational semantics can describe the above program as an infinite sequence of transitions. So your argument "since there's no way to get $S$ from axioms, we cannot write $S$ in small-step semantics too." is wrong. Small-step semantics does not rely on a proof system and has different expressiveness.

Second, what do you mean by "derive $S$ from the axioms"? Do you mean automatically deriving a statement $S$ from the grammar that produces a specific output memory given an input memory? For example, automatically deriving $S$ such that $\langle S, \emptyset \rangle \Rightarrow \lbrace x \mapsto 1, y\mapsto 2 \rbrace$ from the grammar. If this is your question, this is exactly a program synthesis problem that we will discuss later this semester. This problem is also undecidable.

I will be happy to have more questions. Let me know if something is still unclear.

[Allgot]

Thank you so much! Now I realize that big-step operational semantics is different from small-step operation semantics, and thus $S$ is very uncertain expression.

Thank you!