[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Re: Hyperbook Question 6.4

Dr. Lamport,

The correct interpretation looks rather obvious when you point it out, but I can speculate about why I was confused. I was looking for templates of the form "iff X, then Y" which could be converted to "X <=> Y". I had mentally inserted a "then" into the sentence at, "... specification of H, *then* the behavior sigma ...", and I believe that is where I went off track. Just so I'm sure I understand, you are saying that the entire sentence translates to something like:

(H implements A) <=> (\A sigma \in the_set_of_all_behaviors : sigma satisfies H => sigma satisfies A)

So a more correct template would have been "X iff Y", translated to "X <=> Y". It has been many years since I spent any time reading mathematics, so the prose style definitely confuses me. For instance, the first few paragraphs of section 6.8 in the hyperbook were confusing for me, but the treatment of the same material in "The Temporal Logic of Actions" was straightforward, as it was presented using formulas instead of prose.

Thank you,
Charles

On Tuesday, December 1, 2015 at 1:50:37 PM UTC-8, Leslie Lamport wrote:

Dear Charles,

As a side note, the definition of what it means for H to implement A
reads (in part):

We say that H implements A ...  iff, for each behavior sigma
satisfying the behavior specification of H, the behavior sigma
satisfies the behavior specification of A.

Is it correct to read that as (roughly):

\A sigma \in the_set_of_all_behaviors :
sigma satisfies H <=> sigma satisfies A

No, it is not.  I will explain why not, and I would appreciate
knowing why you missed what I regard to be the correct interpretation
of that sentence.  The parsing of the sentence is

(We say that H implements A ...)  iff
(for each behavior sigma satisfying the behavior specification
of H, the behavior sigma satisfies the behavior specification of A.)

The clause (for each ... of A.) is of the form

for every s satisfying A: s satisfies B

which means

\A s : (s satisfies A) => (s satisfies B)

Hence, the correct interpretation is

\A sigma \in the_set_of_all_behaviors : sigma satisfies H => sigma satisfies A

with => rather than <=> .

I believe that any mathematician would interpret the sentence this
way.  However, mathematicians tend to assume that their particular
literary style is unambiguously rigorous and don't appreciate how what
they write can be understood differently by intelligent people who are not
familiar with that literary style.  So, I would appreciate knowing
what led to your interpretation so I can learn how to write more
clearly for non-mathematicians.

Thanks,

Leslie