There are barely any high-level imperative languages for implementing transfinite algorithms. We construct one by taking the standard model of structured programming—a language of while-programs built from assignment operations with selection, sequencing, and iteration, and equip it with a denotational semantics. We show while-programs are equivalent in expressive power to (unstructured) register programs, thus demonstrating a transfinite structured program theorem. We additionally provide a native operational semantics and prove its correctness. Finally, we show how to implement a transfinite insertion sort with exactly the same code one might use in the finitary setting. Our work shows how the basic theory of imperative programming lifts cleanly to the transfinite setting and suggests the outline of a theory of infinite data structures and transfinite algorithms.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Transfinite Structured Programming

  • Siddharth Bhaskar

摘要

There are barely any high-level imperative languages for implementing transfinite algorithms. We construct one by taking the standard model of structured programming—a language of while-programs built from assignment operations with selection, sequencing, and iteration, and equip it with a denotational semantics. We show while-programs are equivalent in expressive power to (unstructured) register programs, thus demonstrating a transfinite structured program theorem. We additionally provide a native operational semantics and prove its correctness. Finally, we show how to implement a transfinite insertion sort with exactly the same code one might use in the finitary setting. Our work shows how the basic theory of imperative programming lifts cleanly to the transfinite setting and suggests the outline of a theory of infinite data structures and transfinite algorithms.