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

*From*: Charles Gordon <charles...@xxxxxxxxx>*Date*: Tue, 1 Dec 2015 14:09:41 -0800 (PST)*References*: <1bb4f7e9-ffc4-45ee-af7a-a1035168b414@googlegroups.com> <ed2a33dc-0b55-49bc-a080-7b972651f337@googlegroups.com>

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:

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

**References**:**Hyperbook Question 6.4***From:*Charles Gordon

**Re: Hyperbook Question 6.4***From:*Leslie Lamport

- Prev by Date:
**Re: Hyperbook Question 6.4** - Next by Date:
**Re: Hyperbook Question 6.4** - Previous by thread:
**Re: Hyperbook Question 6.4** - Next by thread:
**Re: Hyperbook Question 6.4** - Index(es):