Induction variables in very high level languages

Abstract

We explore the notion of an induction variable in the context of a set-theoretic programming langugage. An appropriate definition, we believe, involves both the necessity that changes in the variable around a loop be easily computable and that they be small. We attempt to justify these requirements and show why they are independent assumptions. Next the question of what operators on sets play the role of +, − and * for arithmetic languages is explored, and several theorems allowing us recursively to detect induction variables in a loop are given. It is shown that most of the usual set operations do fit nicely into the theory and help form induction variables. The reason most variables fail to be induction variables concerns the structure of control flow, more than it does the operators applied.