Hyperbook Question 6.4

56 views
Skip to first unread message

Charles Gordon

unread,
Nov 25, 2015, 8:37:28 PM11/25/15
to tlaplus
I am working my way through the TLA+ Hyperbook and have run into some trouble with question 6.4 on page 68. The question reads:

Let Count be a specification with a single variable n whose behavior specification allows the single infinite behavior
    [n = 1] -> [n = 2] -> [n = 3] -> [n = 4] -> ... 
Show that if A is any specification whose behavior specification allows an infinite behavior, then Count implements A under some refinement mapping.

The definition of a refinement mapping is given four paragraphs earlier as:

A refinement mapping from a specification H to a specification A is an assignment of an expression v to each variable v of A, where v is defined in terms of the variables of H.

This confuses me, as the question seems to imply that it is possible to create a refinement mapping for variables that we know nothing about (the variables of A, which are not specified in the question). Furthermore, we need the refinement mapping to define the new "bar" variables in terms of the variables of Count (of which there is just one). The answer given in the hyperbook is to use an operator ev(i) which gives the value of v (from A) for state i. But wouldn't that operator need to be defined in terms of variables from A, when by definition the refinement mapping is to be defined in terms of variables from Count? What am I missing? Is this just a foreshadowing of the idea (later in this section) that all states have values assigned to all variables, so that the variables of A are actually present in the Count behavior listed in the question? 

Charles Gordon

unread,
Nov 26, 2015, 2:03:11 AM11/26/15
to tlaplus
Alright, I think I was just misunderstanding the answer given in the Hyperbook. The answer is:

Let s1 -> s2 -> s3 -> ... be an infinite behavior satisfying A's behavior specification. For any variable v of A, define v to equal ev(n), where ev(i) is the value of v in state si, for any positive integer i.

I had read that as being true for all possible infinite behaviors of A, implying that ev(n) needed to be a general mapping from Count. However, I think the intended reading is that exactly one infinite behavior of A is selected, and ev(n) is "hard coded" to the values of that behaviors states. Is that accurate? If that is the case, I believe I understand the question and its answer. If not, I'm obviously still confused!

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

The forward implication (sigma satisfies H => sigma satisfies A) seems straightforward, given the definition of a refinement mapping, but I'm having a harder time convincing myself of the backwards implication (sigma satisfies A => sigma satisfies H).

Is "The Existence of Refinement Mappings" the right paper to read for more background on refinement mappings? Is there more material elsewhere that explains this concept in another way (I just find it personally helpful to read multiple different explanations)?

Thank you!

Charles Gordon

unread,
Dec 1, 2015, 11:59:55 AM12/1/15
to tlaplus
Section six of the Hyperbook has been my personal "pons asinorum". For any current or future readers of the Hyperbook having the same difficulty, I found sure footing only after reading the first six sections of this paper:


The Hyperbook introduces a lot of terminology in section six (state predicate, property, temporal formula, theorem, formula) and it wasn't clear to me how they related to each other (or which were simply synonyms), and how they related to earlier terms (specification, invariant, predicate, behavior, state). The above paper provides very clear definitions of those terms and their relationships, which made the Hyperbook immensely easier to understand. If I were starting over again, I'd want to read the first five sections of the Hyperbook, then the first six sections of "The Temporal Logic of Actions" (linked above), then section six of the Hyperbook.

Leslie Lamport

unread,
Dec 1, 2015, 4:50:37 PM12/1/15
to tlaplus

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

 
   

Charles Gordon

unread,
Dec 1, 2015, 5:09:41 PM12/1/15
to tlaplus
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

Leslie Lamport

unread,
Dec 1, 2015, 5:32:26 PM12/1/15
to tlaplus
Dear Charles,

The "template" 

   iff X, then Y

makes no sense to me as a complete clause, and I don't think any mathematician would write it.

Leslie
Reply all
Reply to author
Forward
0 new messages