Gries, David (1998). The Science of Programming.
New York, NY: Springer-Verlag. ISBN: 0-387-96480-0. Chapter
2: Reasoning Through Equivalence Transformations (pp. 19-27).
Contents:
Is it possible to write code similar to the barber paradox that defies
standard logic? Or is English not as strict as computer code and allows things
code will not?
I really couldn't think of a question about the material. So a question
about the class: Will we be dealing with other prepositional calculi
(plural of calculus?), potentially one that can handle paradoxes?
In his discussion of the Excluded Middle Law Gries mentions that self-referential statements can possibly create paradoxes which violate the Law of Excluded Middle. He mentions that in the system we are using self-referential statements cannot be introduced. My question is are there situations within the realm of designing a programming language in which we would need to consider such statements and what type of problems can arise?
The development of any formal system requires the definition of a set of
axioms and Gries avoids doing that. 2.3.1 seems to imply that the 12 Laws on
pages 20 and 21 are axioms but their interdepence rules that out as well.
Since this formal system for expressing propositions cannot express all
our thoughts, what other systems are there?
Just like the law of contradiction which is proved from others, can we
define the law of negation from the other 11 laws?
Gries defines 12 laws of equivalence in this chapter and 1-11 seem to be very
useful. How is the 12th law (Law of Identity) useful to us?
Could you clarify what Gries means by inference rules in section 2.3?
In section 2.3, Gries separates the propositional calculus from the
notion of a tautology.. "to emphasize the nature of this calculus as
a formal system for manipulating propositions." I'm not really clear
on the distinction.. it seems like just a different way of stating the
Substitution and Transitivity rules.
Why does the proof of exercise 10 require use of conjunctive normal form?
Why isn't it sufficient to say that a tautology is true in all states by
definition and is therefore can be substituted for the value 'T'? I
feel like I am missing some important subtlety.
Is the example, 2.2.3, an actual tautology proof or just an example or how to
transform an implication into an easier to read format? It's not an actual
tautology, is it?
Concerning the rules about inference, theorems, and axioms. What is the
difference between an axiom and a theorem? One is inferred from a theorem,
the other is derived from a theorem. Is there any actual difference other
than the name (or other semantics)?
A more general question. Is this chapter implying that all our symbol
manipulation within programs will be based on the 12 laws?
Regarding exercise 7 and 8, why would one care about disjunctive normal
form and conjunctive normal form?
;
Check with Bobby