Algebraic specifications: missing the proof that operators respect the quotient induced by the AF?

[favonia]

I'd like to discuss a possible oversight in Section 6.9: in the batched queue example, it is emphasized that for two abstract queues q and q', they are equal if AF(q) = AF(q') where AF is the abstraction function. However, this also means that the actual equation 4b should be

Lemma: if AF(q) = AF(q'), then deq (enq x q) = enq x (deq q')

not just

Lemma: deq (enq x q) = enq x (deq q)

That is, we also have to prove the cases where two equivalent queues are represented differently. Or, in other words, we have to prove that all operators respect the quotient induced by the AF. I wonder if I missed something here?

[clarksmr]

We're on spring break this week, but I'll take a look later when we are back.

[clarksmr]

Sorry, it took me much longer to get back to the textbook than expected. I had calendar year 2023 off from teaching the course, but I'm back to it now in 2024.

[clarksmr]

Thanks for the suggestion. I think your generalized lemma is already a corollary of what we have?

The intent was to add AF(e) = AF(e') -> e = e' as an axiom. With it, we then proved deq (enq x q) = enq x (deq q).

Now suppose we want to show if AF(q) = AF(q'), then deq (enq x q) = enq x (deq q'). By the antecedent, we have AF(q) = AF(q'). By the axiom, we have q = q'. By Leibniz substitution of q' for q in the proved lemma, we transform deq (enq x q) = enq x (deq q) into deq (enq x q) = enq x (deq q'). Qed.

What do you think?

[favonia]

@clarksmr I agree that under that axiom there's no difference. However, when we are proving the lemma, we only do induction on the (raw) syntax of q/q' without actually considering the possibility that maybe things are equal due to the new axiom. The potential mismatch between the additional axiom AF(e) = AF(e') -> e = e' and the actual practice in proving is what I was trying to point out. That said, I understand that this subtle point perhaps does not deserve much attention for teaching purposes.

[clarksmr]

@favonia So sorry, I apologize that I'm not following you...

1. When you say "do induction", where do you mean? I don't see any use of induction in the proof of lemma 4b, which starts as follows:

https://github.com/cs3110/textbook/blob/7b86c499bf2e19c62902b3d9b4cbb61991a5d2b4/src/chapters/correctness/alg_spec.md?plain=1#L425-L428

Did you mean the case analysis?

2. I also don't understand what mismatch you are pointing out w.r.t. the actual practice in proving. The additional axiom is used in the proof here:

https://github.com/cs3110/textbook/blob/7b86c499bf2e19c62902b3d9b4cbb61991a5d2b4/src/chapters/correctness/alg_spec.md?plain=1#L506-L508

Were you expecting it to be used in a different way? How would making it an antecedent improve the proof?

3. You mention it's a subtle point. I hope I'm not being dense... :)

[favonia]

@clarksmr Hi, sorry that I'm not sure how soon I can re-check the textbook and respond meaningfully to your comments and questions. On the other hand I don't want to leave this unresolved forever. When would you touch this part in your course?

[clarksmr]

@favonia Somewhere around the first week of March 2024 I expect.

[favonia]

@clarksmr Sorry that my backlog prevented me from checking the textbook again. Given that this textbook has been used for so many semesters, I believe it would be fine even if there's an actual issue. :slightly_smiling_face: Thank you again for your great work and I really appreciate it.

[clarksmr]

No problem! I'll close this issue but if you ever want to reopen it again you know what to do. :)