Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

[flagged]


That does not really apply. A compiler can compile itself, it can check if its own code is valid.


[flagged]


The fact that someone might make a mistake in doing something does not show it cannot be done. More generally, You seem to be mistaking validating a program's source with the question of whether it performs its intended purpose. These are different things, and attempting to conflate them will only lead to confusion.


> You seem to be mistaking validating a program's source with the question of whether it performs its intended purpose.

In general, that is a useful distinction to make, but you forgot about the edge case where the distinction is meaningless.

A self-hosting compiler's intended purpose is to validate its own source code.


Then your mistake appears to be in failing to see that your perceived edge case does not invalidate the first sentence of my reply. If the sole purpose of a parser is to syntactically validate its own source (which is not the case for a compiler's parser, by the way, not even if we expand 'its own source' to 'arbitrary input'), then if it does that correctly, that's all there is to it.


[flagged]


Godel incompleteness only applies to sufficiently powerful formal systems.


Indeed. Type 0 Grammars are the most powerful grammars we have.

https://en.wikipedia.org/wiki/Chomsky_hierarchy#Type-0_gramm...

In this type of grammar Godel's incompleteness theorem is equivalent to the Halting problem.


And which programming language did you have in mind?


All of them.

"Type-0 grammars include all formal grammars. They generate exactly all languages that can be recognized by a Turing machine."


I see - you have the complexity relation the wrong way round.


Are you sure you aren't mistaken? :-)


Go ahead - show me wrong.


I have already done that, what I am unsure of is how to go about convincing you.

With compilers - I just fix the bug myself. With humans, I have to convince the human to self-correct.

Common problem in distributed systems that - leader election.


It is a general rule that those who avoid answering a question do not have an answer, and this is no exception. Here, You completely misunderstand Chomsky’s hierarchy: By your inverted-hierarchy argument, the simplest regular language would be complex enough that incompleteness would be an issue in its validation.


Well, this looks like abuse of Cunningham's law, but I'll bite.

It is a general rule that general rules have exceptions. And you have (incorrectly) asserted that this is not an exception.

Q.E.D

Even the most powerful languages (Type 0 in the hierarchy) cannot solve the halting problem. Which is equivalent to Godel's incompleteness theorem.

https://www.scottaaronson.com/blog/?p=710

If a Type 3 grammar can recursively prove its own correctness, it's not a Type 3 grammar!

But if you desperately want to be right, I will happily lie to you (you are right, I am wrong), so I can move on with my life.


Your second paragraph is just a direct begging-of-the-question.

More significantly, verifying that sentences are well-formed in some language is not the same as proving the language’s correctness.

As a response to you argument, consider this regular language:

A


Curry-Howard isomorphism.

Proving that a sentences are “well-formed” is the same as implementing an algorithm which takes a string and returns a Boolean.

You can call this function “is_well_formed?”

I await your proof in the regular language you have specified above.


Please also stop.


Please stop.


A self-hosted compiler is definitely not a case of the liars paradox, so I don’t think this applies. In fact, it doesn’t matter what the parser is written in, at some point you do have to trust that it actually follows the spec, probably through testing.


So what you have to trust is that the spec doesn't produce lies ? ;)

FYI. I am just having some philosophical fun with GIGO.

Ultimately, computers are just instruments which amplify human intention, it's not the computers's job to be ultimate moral arbiter of our words.

Gödel's incompleteness theorem already tells us that a system cannot prove its own correctness.


The "liar" only says "I can proofread Essays" and not "I am lying".


The "liar" is saying that the Essay is free of errors. (To the best of the "liar's" ability to detect them).

The liar's knowledge is incomplete.

https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...


Free of English errors. Not semantic errors. We don't even know it's a "liar".


Precisely, but as far as a compiler/interpreter is concerned syntax is semantics.

You can't codify moral judgments.


Not sure if you are trolling, but here we go...

In the case at hand, correctness of the validator expression V clearly means "V determines well-formedness of any regular expressions" which is clearly not implied by "V is well-formed" (a much weaker statement because ".*" is well-formed but matches everything). Therefore, when applying V to itself, we only learn if a weak requirement for V's correctness holds.

Similar, perhaps, to validating whether a given number is a Gödel number of a well-formed logical statement rather than assessing the verity of the logical statement it encodes.

Also, I am not saying whether it is or is not possible to build such a regular expression. Rather, the question just doesn't tick the boxes of either, the Liar's Paradox, nor Gödel's Incompleteness result -- contrary to what was suggested. So you could still be right but for different reasons.


You are axiomatically assuming that the proposition "V determines well-formedness of any regular expressions" to be true.

I am asking you to prove that. Constructively.


It's not possible to do this for regular expressions, but it is possible to do it for context free grammars. You can write a context-free grammar in Backus-Naur form that recognizes all context-free grammars in Backus-Naur form:

   <syntax>         ::= <rule> | <rule> <syntax>
   <rule>           ::= <opt-whitespace> "<" <rule-name> ">" <opt-whitespace> "::=" <opt-whitespace> <expression> <line-end>
   <opt-whitespace> ::= " " <opt-whitespace> | ""
   <expression>     ::= <list> | <list> <opt-whitespace> "|" <opt-whitespace> <expression>
   <line-end>       ::= <opt-whitespace> <EOL> | <line-end> <line-end>
   <list>           ::= <term> | <term> <opt-whitespace> <list>
   <term>           ::= <literal> | "<" <rule-name> ">"
   <literal>        ::= '"' <text1> '"' | "'" <text2> "'"
   <text1>          ::= "" | <character1> <text1>
   <text2>          ::= '' | <character2> <text2>
   <character>      ::= <letter> | <digit> | <symbol>
   <letter>         ::= "A" | "B" | "C" | "D" | "E" | "F" | "G" | "H" | "I" | "J" | "K" | "L" | "M" | "N" | "O" | "P" | "Q" | "R" | "S" | "T" | "U" | "V" | "W" | "X" | "Y" | "Z" | "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i" | "j" | "k" | "l" | "m" | "n" | "o" | "p" | "q" | "r" | "s" | "t" | "u" | "v" | "w" | "x" | "y" | "z"
   <digit>          ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
   <symbol>         ::=  "|" | " " | "!" | "#" | "$" | "%" | "&" | "(" | ")" | "*" | "+" | "," | "-" | "." | "/" | ":" | ";" | ">" | "=" | "<" | "?" | "@" | "[" | "\" | "]" | "^" | "_" | "`" | "{" | "}" | "~"
   <character1>     ::= <character> | "'"
   <character2>     ::= <character> | '"'
   <rule-name>      ::= <letter> | <rule-name> <rule-char>
   <rule-char>      ::= <letter> | <digit> | "-"
I got this from Wikipedia: https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form#Furth...


Sure. Total functional programming (provably terminating code) comes at the cost of Turing-completeness.

The choice exists.

https://en.wikipedia.org/wiki/Total_functional_programming

Observe though that BNF is just a notation. Parsers for BNF are not implemented in BNF. Bison. Yacc.


:-)


So we agree then that when the system says "I am free of errors", some (most?) of the time it's a lie ? ;)

All models are wrong - some are useful.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: