I'd very much look forward to seeing a full write-up of this proof. I suspect that many will prefer it to any of mine. In fact, one of the people who prefer your proof might be me.

It is very common in math to publish new proofs of old results. In any field, the first statement of something is seldom either the clearest or the most elegant.

Let's find a program where the prototype is non-deterministic and affects context.

BEGIN {
    *call_to_inspect = ( rand() < 0.5
        ? sub ($) {}
        : sub (@) {}
    );
}
[download]

You can detect some changes in the compile-time state of a prototype by its effect on context.

BEGIN {
    *call_to_query = ( rand() < 0.5
        ? sub ($) {}
        : sub (@) {}
    );
}

sub inspector { print wantarray ? 1 : 0, "\n" }
call_to_inspect(inspector());
[download]

Let's observe:

>perl a.pl
1

>perl a.pl
1

>perl a.pl
0

>perl a.pl
1
[download]

Therefore, there exists a function call in a program for which two instance of the Perl parser have different prototypes for the named function.

Therefore, there exists a program for which two instance of the Perl parser produce different output.

Or for short, Perl cannot be parsed.

The proof looks like it goes through. One reason mathematicians do multiple proofs (aside from the fact that subsequent ones tend to be better) is that they are rhetorical devices. Different proofs speak to different audiences. Allow me to comment on a trade-off made in this version.

This proof uses Perl's rand builtin, while my efforts treat Perl as a Turing machine. The rand-based proof could be read as stating "Perl parsing is undecidable if you use rand, time or some other non-deterministic builtin".

Similarly, you could read the Turing-machine-based proofs as saying "Perl parsing is undecidable if you use Turing-equivalent control constructs." If you allow no transfers of control at all, clearly the compile phase will terminate, and my proofs no longer go through.

The different proof tactics give the two proofs different rhetorical effect. It's subjective, but subjective matters. A lot depends on whether you see Turing-equivalent control flow constructs or non-deterministic builtins as "core" features.

One thing you might do, if you're interested, is a reduction of Perl parsing to some form of Goldbach's Conjecture. This would not be a proof of undecidability, unless and until Goldbach's Conjecture is found undecidable. Instead it would amount to proof that Perl parsing is equivalent to a really hard and currently unsolved problem.

Saying "two instances of the parser" produce different things (on the same given code, presumably) makes it sound simply like the parser is non-deterministic or randomized.

It is more like two possible syntactic interpretations/parses of the same piece of code,

And what produces those two possible parses? Two parser instances. We're saying the same thing.

Saying "two instances of the parser" produce different things (on the same given code, presumably) makes it sound simply like the parser is non-deterministic or randomized.

Good.

I don't know what the halting problem has to do with non-deterministic or randomized programs. The perl parser is deterministic, and it does not toss random coins. You can certainly insert randomness into a BEGIN block, but that's not what's going on here and it doesn't mean that parsing itself is randomized. Jeffrey's examples & undecidability proofs all involve deterministic BEGIN phases. If you run the parser a billion times on a deterministic program, you will get the same result every time. Different instances of the parser do not give different parses. The only way to get different parses is by having different behavior within the BEGIN block.

blokhead

However, you tried to prove this by counter-proof.

Actually, no. The whole presentation of the counter-argument only attempts to prove that that line of counter-argument (which has been put forward in a few variations) fails. It doesn't attempt to prove Perl Unparseability. If that was your expectation I can certainly see why you saw it as falling short. My presentation of the counter-argument is like an exposition of a variation on the Sicilian Defense intending to show a chess maven why he should never play it.

Arguably the post might have been stronger without it. I've dumped it into a "readmore".

The proof is given in three forms in the TPR articles. The strongest form is the one that uses Rice's Theorem. The other two may be considered explanations intended to help those trying to understand why Perl Parsing Undecidability is provable.