Iteration and Labelled Iteration
Bram Geron, Paul Blain Levy · Electronic Notes in Theoretical Computer Science · 2016
We analyse the conventional sum-based representation of iteration from the perspective of programmers, and show that the syntax they suggest is fundamentally not a good representation of Java-style iteration with for, while, break, and continue. We present an alternative syntax, which we call “labelled iteration”, where loops are identified using labels. The languages are analysed: we give denotational and operational semantics, adequacy proofs for both languages, and a translation function from sum-based iteration to labelled iteration.