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.
in reply to Re^3: Perl is not Dynamically Parseable
in thread Perl is not Dynamically Parseable
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.