I recently was listening to a few talks on loop invariant indicating the meaning of a loop, when implemented in procedural languages.
It then occurred to me that the manner predicates are relationally defined over successive states-- aren’t these precisely expressions of loop invariants.
Hence declarative programming in fact means making loop invariants describe relational meaning which then also does the work.
And, aren’t hence, (pure) prolog declaration the basis for proofing correctness of the algorithm so implemented …
All those talks looked at working out what the loop invariant is based on some imperative code – i guess, in prolog the programmer thinks hard to explicitly work out the loop invariant – which is, essentially, the code that performs the computation via prolog.
In Hoare logic, which is often used in the context of verifying procedure correctness, loop invariants are used to make explicit some implicit property that the loop maintains, but the loop invariant does not indicate the meaning of the loop per se. Instead, the loop invariant simply refers to the assertion P in the while rule of Hoare logic:
{P /\ b} c {P}
---------------While
{P} while b do c {P /\ -b}
Where b is a boolean expression and c is some command (the body of the loop).
So the loop invariant is nothing less and nothing more than an assertion P whose conjunction with the boolean condition of the loop b entails that P remains true after the body of the loop, hence if the loop terminates we are guaranteed that P and the negation of b both hold. From P /\ -b together we may be able to prove that the result of the while loop is correct is respect to some stated property (which may be “the meaning of the loop”).
In the end, our loops are recursive predicates and these typically follow the scheme of a mathematical proof by induction. At least, that is my naive view on this. Educated in Eindhoven, where Dijkstra (I think the inventor of loop invariants) was professor, I can’t say I used this way of thinking for Prolog.
When mathematical induction is applied to describe the evolution of states, that’s when I thought, the inductive description becomes the loop invariant in that it describes what is true at the beginning and each end of a loop.
anyway, its just a little mind-game to see if concepts across different discipline relate …