From pg. 45. "In Hilbert's conception, the construction of a formal mathematical system begins with definitions, axioms, and rules for constructing theorems from axioms."
My Take:
- The regular expressions that are used by in the Lexical Analysis phase of the compiler are Definitions .
- The productions of the grammar rules, used in the Syntax Analysis phase, are Axioms. The output is an Abstract Syntax Tree (AST)
- Finally the Semantic Analysis phase is the one where the rules of the language are used to extract the operations that are implied by the AST. The output is an Intermediate Representation (IR). That is where the front end of a compiler ends. Subsequent steps are transformations to make the code execute on some CPU
- Thus the IR output of the compiler is a theorem constructed from axioms.
- The rules and axioms are coded in to the compiler.
- A compiler therefore qualifies as a formal mathematical system.
From pg. 46. " ... but the rules also imply the syntax of a well formed formula ... that is possible within the system. You can assemble a well-formed formula without first deriving it from your system, and then you can attempt to show that it's a consequence of the axioms by applying the axioms and rules in a proof."
My Take:
- When we write a program in a high-level language we in fact "assemble a well-formed formula without first deriving it from your system".
- Then when we successfully compile it we in fact show that "it's a consequence of the axioms by applying the axioms and rules in a proof"
From pg. 47. "Provability is a syntactic concept; it is based on the axioms of the system and the rules used to derive theorems. Truth, however, is semantic concept that depends upon the actual meaning we give to the symbols in the system."
My Take:
- Successful compilation proves Validity.
- Successful compilation does not prove Veracity (Truth).
- There is no getting away from well designed tests. Such tests are close approximations of a "proof" of Veracity.
No comments:
Post a Comment