Proving that C++'s grammar is undecidable | Hacker News Reader

Proving that C++'s grammar is undecidable

medium.com

76 pointsvitaut64 comments

The algorithm in the article has an important bug. It’s a basic search: pop an element from a queue, see if it’s a match and, if not, push two new elements. If the queue is empty, declare failure. Think about this for a moment. Each iteration, the queue length increases by one. Of course it’s never empty. So the algorithm will eventually declare success on a positive input and will run forever on negative input. It has to be this way, since PCP is equivalent to the halting problem. There is no algorithm that solves it correctly and always halts. This is the whole point.

This means that this program does not prove that parsing C++ is undecidable in the way the author thinks. There is no term that is a type or a value depending on the solution to an undecidable problem. Instead, there is a term that can not be resolved in finite time. This is a necessity property of pretty much any Turing-complete metaprogramming system.

(What I think is actually going on that’s a bit unique to C++ is that C++ cannot be parsed unambiguously. The fact that the grammar depends on whether a term is a type or value and that you can’t determine this from the AST without doing things like expanding templates is nasty.)

Am I missing something? The author says that a solution to the Post Correspondence Problem with infinite dominoes in finite time is impossible. He then writes a bunch of C++ code that can solve the PCP for any arbitrary list of dominoes. Did he realize that this list must be finite since it’s written into the C++ code? If the list had infinitely many dominoes it would require infinite space to store and infinite time to compile anyways, PCP or not. That’s like saying Java is undecidable because you can write List<List<List<List<...>>>> and have something take infinitely long to compile.

> The author says that a solution to the Post Correspondence Problem with infinite dominoes in finite time is impossible.

He doesn't say an infinite set, though:

> Turns out, there exists no algorithm that says “yes” or “no” to the Post Correspondence Problem in finite time, given any set of dominoes as input.

That means any finite set of dominos.

It's similar to the idea behind the halting problem, it's not checking whether an infinitely long program will halt, but whether any possible finite program will halt.

It may take an infinite amount of time to solve the Post Correspondence Problem even with a finite number of dominoes, but you can't know whether it really will hang forever or whether you just haven't run your program long enough to find the answer. You don't need infinite space or time for the ones that are solveable, just an unknowably large amount.

So if you make a C++ program that compiles if the equivalent arbitrary Post Correspondence Problem is solvable, and compiles forever otherwise, you've proven that C++ compilation is not decidable.

There is a finite set of Domino "prototypes" (a pair of strings), and you are allowed to use as many of each prototype as you like.

What you are missing is that in the Post Correspondence Problem you have an unlimited supply of each type of domino. So a finite list of domino types could require an unlimited number of dominos to decide.

Now we can write programs that attempt some sort of clever reasoning to figure out whether or not there is a solution at all. But given any specific program that does that, there is a finite arrangement of dominos such that either the program produces the wrong answer, or cannot possibly finish. In other words, for any algorithm there is a finite problem that cannot be properly decided by that algorithm.

Given an axiom system such as ZFC, we can write a program that searches through all proofs in ZFC for a proof or disproof that a particular case of the Post Correspondence Problem is solvable. This, being an algorithm, has a finite input that it will either produce a wrong answer for (meaning that ZFC contradicts itself) or else will never finish. Whether or not that case has an answer is not decidable within ZFC!

Ideally we want the answer to be "there is no solution" in this case. But if we introduce the axiom that there is a solution, we will never find a contradiction and never be aware of any disturbing conclusion beyond, "That solution must be really, really big." It turns out that, no matter how hard we try, first order logic cannot correctly encode the concept of "finite".

This is what we mean by "undecidable".

Isn't it well known that C++ templates are Turing complete? Aren't most metaprogramming facilities in other languages as well?

I could be mistaken but doesn't that just mean the value computed into a compile time constant can do arbitrary computation? Whereas I think this is saying that the Turing completeness leaks up to the parsing level.

No, constexpr is not the same thing as template expansion. The decidability problem as I understand it is, "does the template expansion halt?" And since the template syntax in C++ is Turing complete, the answer is "you can't know." I'm just confused how this is significant or different from any other recursive macro expansion, it doesn't seem surprising to me.

No -- the Turing completeness of templates that people refer to just talks about the fact that templates are powerful enough to compute anything. It's a different issue from parsing the template syntax in the first place, which is the problem they talk about here.

Turing completeness and undecidable parsing grammars are completely orthogonal concepts.

The problem here is that C++'s metaprogramming facilities have leaked into the parser to the extent that it's undecidable whether to parse that final declaration as a variable declaration or a function declaration.

So: arguably the grammar is decidable, but to parse C++ you need more than the grammar, you need the full metaprogramming machinery. That is, C++ has ended up in the same state as a language that simply provides Turing-complete macros.

This is what I love about C++ that isn't provided by [m]any of the "modern" languages (not including Lisp). I want programs in my programs dangit!

If you really want that, it seems better to provide them properly like Rust proc-macros than to provide them in C++'s awful half-baked form.

Rust’s compile-time meta programming is lacking at the moment, unfortunately. It doesn’t have const generics yet, and the standard library is a bit anemic and this extends to the type programming utilities as well.

> If you really want that, it seems better to provide them properly like Rust proc-macros than to provide them in C++'s awful half-baked form.

- C++-17 (-20) constexpr is one century in advance in front of rust macro in term of power and what you can do with it. It is not even comparable.

- C++20 compile time execution is currently pretty clean and has nothing to do with this template mess shown here. Definitively not "half baked".

Yes. From what I understand, Rust's macros/generics are not Turing complete.

They are. Procedural macros especially are a function that takes tokens and returns tokens, and have the full language at their disposal.

Ah interesting. But I imagine that token-based macros don't give you access to the types in the program being compiled do they? i.e. a c++ template can tell when two types are the same but a token level macro wouldn't be able to do that I think.

Correct.

Compile-time function evaluation is quite a different feature from macros. Most of what you would do with macros (e.g. output entirely new definitions of functions, types, etc) can't be done with constexpr at all.

And vice-versa.

C++'s awful half-baked form comes with 40 years of IDEs, libraries, GUI tooling, OS and GPGPU SDKs, so while I do like Rust, I rather use C++ for the time being, as clunky as it might be.

You can do it in Haskell with Template Haskell. You can also lift some computation to the type level with means they will run at compile time during type checking.

This kind of makes me laugh. Is this due to the relentless changes they've been making to the language the last decade or two? I thought it kinda went off the rails a while ago.

Nope, nothing new here. I mean, it uses some new spellings for certain template concepts, but they are fairly easy to create yourself with a years-old version of C++.

> typeOrValue is a type int if the solution to the Post Correspondence Problem is “yes”, and a value 0 of type int if the solution is “no”, using SFINAE

Isn't this where the `typename` keyword comes in? `typename` is required when using a qualified (meaning ::) dependent (it references a template parameter) identifier as a type. My understanding is that uses of types without typename is a common helpful extension but is not strictly conforming.

C++ language lawyers, please check my work...

I think typename is only required inside of template definitions.

> The keyword typename must only be used in template declarations and definitions and only in contexts in which dependent names can be used.

https://en.cppreference.com/w/cpp/language/dependent_name

The example given in the original post involves a dependent name

It has to be both dependent and inside of a template definition. The example is a normal function declaration. The linked article has a couple examples.

By this logic, any language with metaprogramming is undecidable because you can write undecidable programs as a metaprogram. Execution is not the same as parsing.

The execution is necessary for the parse to complete, as until then it’s unknown what the identifier is as it’s dependent on the result of the undecidable expression.

If that metaprogramming is Turing complete then yes. The point of this article is to show that metaprogramming in C++ is Turing complete. It had already been widely known but this article presents an explicit demonstration of it.

god knows there are easier ways to make a C++ compiler vomit on you

C++ is legitamately gross to read these days, unless you sit there reading it every day.

The syntax has become so ridiciously complicated, I have developed an involuntary gag relfex every time I read any kind of "modern" C++ code (i.e. heavy use of templates / generics / keywords).

I like it. After working in golang for a while I miss more robust languages that can express themselves in complicated and creative ways. I hate makefiles though.

New projects using C++20's module system will greatly ease the pain of makefiles.

How do they ease the pain of makefile? When trying to understand what C++20 modules are trying to solve, that's really not that obvious to me that makefile will be simplified.

By using build2, CMake or IDE specific project files.

I spent the past 3 years working professionally with Go, and while I enjoy it for $WORK it can also feel limiting in the way you expressed. I found out about D recently, and it seems to be a quite nice compromise between C++ and Go, giving you more way to express yourselves without having the pitfalls of C++.

Maybe something you would be interested into: http://dlang.org/.

I'm not sure what you mean by heavy use of keywords, but C++20 allows you to express templates basically as generics so if the <> syntax offends you you can do without it completely.

Do you also object to Lisp Macros?

This is exactly the problem with C++. Let's fix ugly syntax by providing yet another way to write something that accomplishes the same thing.

Over-evolution isn't a good thing.

Just like breaking backwards compatibility usually leads to 17 years delay in adoption. Can't please everyone.

Not OP but D has better templates implementation [1] and it has no macros, yeay!

[1]https://github.com/PhilippeSigaud/D-templates-tutorial

Templates were an attempt to get macros into the language.

What bugs me is that you don't even need to use templates to run into syntax traps. Braced initialization is crazy and I don't understand it (having first touched C++ sometime in the 90's, done it professionally, and even writing in my own pidgin subset now)

https://twitter.com/timur_audio/status/1119160309573242880?l...

I can understand having crazy syntax for rare and exotic things. But variable initialization is not one of those things...

> Braced initialization is crazy and I don't understand it

It's a disambiguation thing: https://en.wikipedia.org/wiki/Most_vexing_parse

The simple recommendation is to just always use {} when you want to construct an object, see https://isocpp.github.io/CppCoreGuidelines/CppCoreGuidelines...

Unfortunately it’s not perfect and can do strange or undesirable things sometimes, especially when interacting with auto.

C++17 improved the auto situation. It looks pretty much as I'd expect now.

This "problem" has been there in C++ like forever, it's not new.

Templates are Turing complete. Once you have that, it's pretty simple right?

I can't decide if C++ has a grammar at all.

Please have a sense of humor.

This doesn't prove C++'s grammar is undeciable. Template expansion is seperate from parsing. Besides you can do the same thing in any language that can do Turing complete compile time programming.

Template expansion is not separate from parsing in C++. That's the very thing this article explicitly demonstrates. A program will end up being parsed in two different ways depending on the solution to an instance of Post's Correspondence Problem. In one solution a declaration of x parses into a variable, in another solution a declaration of x parses into a function. Which of those two parse trees is actually correct? That question is not decidable and hence C++'s grammar is undecidable.

You are right! I didn't realize this.

The code in the OP are images, e.g., cannot be cut and pasted.

Sadly Medium seems to lack the tools to make decent standalone code snippets.

I don't know what qualifies as "decent" for you, but instead of an image, I'd vastly prefer a plain old blockquote element combined with whatever html one uses these days to specify a monospace font.

<pre> or <code>? That would be nice, but I don’t think Medium has that.

The fact that the code compiles on godbolt.org makes me doubtful that this particular instance proves that the grammar is undecidable.

The fact that it compiles does that this particular setup halts. This isn’t true in general.

The color scheme on the syntax highlighting makes me crave cotton candy...

Can do a "constexpr void inf() { for (int i = 0; i < 2; ++i) i = 0; }" as a shorter proof.

That’s not the grammar, though; that’s compile-time evaluation.

Reply on news.ycombinator.com