Transfinite Structured Programming
摘要
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.