Iteration and Labelled Iteration

详细信息    查看全文

• 作者：Bram Geron ^{bxg314@cs.bham.ac.uk" class="auth_mail" title="E-mail the corresponding author} ; Paul Blain Levy ^{P.B.Levy@cs.bham.ac.uk" class="auth_mail" title="E-mail the corresponding author}
• 关键词：iteration ; loops ; lexical binding ; operational semantics ; denotational semantics ; higher-order language ; lambda calculus ; de Bruijn indices
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2016
• 出版时间：5 October 2016
• 年：2016
• 卷：325
• 期：Complete
• 页码：127-146
• 全文大小：298 K

文摘

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.