Beefy Boxes and Bandwidth Generously Provided by pair Networks
There's more than one way to do things
 
PerlMonks  

Re^3: Perl Cannot Be Parsed: A Formal Proof (obvious)

by tye (Sage)
on Jan 22, 2008 at 05:26 UTC ( [id://663504]=note: print w/replies, xml ) Need Help??


in reply to Re^2: Perl Cannot Be Parsed: A Formal Proof (meh)
in thread Perl Cannot Be Parsed: A Formal Proof

I don't really find "If you don't try to solve the halting problem, then you can parse Perl" to be a "stronger" conclusion than "If you don't do something random, then you can parse Perl", other than, of course, the presence of high-falutin' comp sci lingo in the former.

It is a rather simple fact that you can't reliably parse Perl without running Perl code (arbitrary Perl code). It reminds me of showing my kids a clock face and asking them to list the properties of the numbers on it. They never mention that they are sorted, because that just seems too obvious.

The fact that you can't parse Perl is obvious. Adding useless complication to the conjecture makes it sound more like a rigorous proof, but I don't believe it actually helped your proof.

A proof that you can't parse Perl, is:

BEGIN { my $proto= ""; $proto= "()" if run_some_perl_code(); eval "sub whatever$proto { }"; } whatever / 6; # /;

The fact that run_some_perl_code() can be any arbitrary Perl code is quite clear. I guess this then boils down to the argument that somehow static analysis could be used to predict the results of run_some_perl_code() without actually running it. But the rand example clearly shows that not to be the case. As does using if @ARGV or if <STDIN> =~ /^y/i or if LWP::Simple::get("http://perlmonks.org/secretAlgorithm.pl") =~ /true/ or if unlink "/etc/passwd" or if find_prime_of_length( ~0 ) % 3 == 1.

Sure, the fact that run_some_perl_code() could be trying to solve the halting problem also demonstrates something. Of course, if I'm writing Perl support for an IDE, I'm not seriously concerned that the declaration of function prototypes is being based on answers to instances of the halting problem, so I'm likely to just dismiss your proof (based on your own reaction to the rand case). I find "You might have to run arbitrary Perl code" to be both a stronger statement of the result and a more interesting and useful one.

I also think there is a flaw in your proof in that it confuses solving the halting problem with running code that may or may not halt. So your conclusion would need to be more like "Here is some code that will either determine that whatever() is nullary or that will never terminate." Since just because the code has been taking 400 years doesn't mean that you can determine that it will never halt, so your code doesn't even have the potential of solving the halting problem.

So the lemma that is needed here is that "Static analysis of a program in a Turing-complete language (along with its 'input') can be insufficient to determine its output". Frankly, this is where it becomes uninteresting to me.

(Minor updates applied during the 15 minutes after first posting.)

- tye        

Replies are listed 'Best First'.
Re^4: Perl Cannot Be Parsed: A Formal Proof (obvious)
by exussum0 (Vicar) on Jan 22, 2008 at 11:23 UTC
    I don't really find "If you don't try to solve the halting problem, then you can parse Perl" to be a "stronger" conclusion than "If you don't do something random, then you can parse Perl", other than, of course, the presence of high-falutin' comp sci lingo in the former.

    You're kind of right. It's called minimalization. If I can solve this base problem, I can solve this more complex problem. Ex: If I can prove I can sort, I can sort in reverse, I can sort using other means etc etc etc. If I can do those things and have proven those things, I can do even more, chaining all the way.

    You're minimalizing directly to undeterministic behaviour, as opposed to the halting problem. Most people chain minimalized behaviour to save time. You don't have to prove the halting problem since it's already proven. Your intuition is right. It's only awkward by the convention of, "most people don't do it like that."

    I'm amused the conversation is taking place though. You're both arguing cherry pie or apple pie to be tasty. :)

Log In?
Username:
Password:

What's my password?
Create A New User
Domain Nodelet?
Node Status?
node history
Node Type: note [id://663504]
help
Chatterbox?
and the web crawler heard nothing...

How do I use this?Last hourOther CB clients
Other Users?
Others about the Monastery: (7)
As of 2024-03-28 21:43 GMT
Sections?
Information?
Find Nodes?
Leftovers?
    Voting Booth?

    No recent polls found