Tautological Inductive Invariant in "Euclid Writes an Algorithm: A Fairytale"

[Alex Weisberger]

Hi everyone,

I recently came across the great resource by Mr. Lamport - Euclid Writes an Algorithm: A Fairytale: https://lamport.azurewebsites.net/pubs/euclid.pdf

One thing that jumped out to me as I was reading is something that I keep bumping into when writing specs: the inductive invariant of a spec is often tautological.

For example, the paper specifies an algorithm (Euclid's algorithm) for the greatest common divisor of two numbers. The inductive invariant used is:

∧ x ∈ Number 

∧ y ∈ Number 

∧ GCD(x , y) = GCD(M , N )

where GCD(x, y) is defined independently of the algorithm presented in the paper. 

My question is, isn't this tautological, since we are comparing two different algorithms for computing the same thing? It's like saying "the algorithm is correct if it matches the output of the algorithm." I've run into this when writing specs practically, because I often can't think of an inductive variant other than "the algorithm does what it's supposed to." 

Do other people run into this? I wonder if I'm looking at this in the wrong way.

-Alex

[Stephan Merz]

Hello,

allow me to respectfully disagree: in logic, a tautology is a formula that is true in every interpretation [1]. Although any tautology is trivially an inductive invariant, it is useless because it carries no information and does not help you prove any property.

More to the point, comparing the outcomes of the executions of an algorithm to an independent definition is not tautological, and the example of Euclid's algorithm illustrates this quite well. The GCD operator is defined "declaratively" as the least common divisor of the two inputs to the algorithm, whereas the specification of the algorithm is operational, based on successive subtraction. These two concepts are very different: in particular, the algorithm doesn't involve division or modulus, and the definition of GCD doesn't involve subtraction.

The idea of verifying the algorithm against the mathematical (declarative) definition is that you trust the latter a priori and gain confidence in the former by checking that it returns the same result for any valid inputs. Perhaps the idea doesn't get fully across because (1) the algorithm is so small and familiar and (2) the relevant mathematical facts that are used in the proof of the algorithm are stated without proof, but I don't see why you consider the comparison tautological.

Stephan

[1] https://en.wikipedia.org/wiki/Tautology_(logic)

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/109f9d64-5feb-458c-a59f-d39383d261cbn%40googlegroups.com.

[Alex Weisberger]

Thanks for answering.

This is exactly what I was looking for, don't worry about disagreeing with me. I was doubting my understanding, and this does clear it up. 

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/98409D54-4FDD-4885-B383-4701033BB8C5%40gmail.com.