Mω considered as a programming language

AbstractThe paper studies a simply typed term system Mω providing a primitive recursive concept of parallelism in the sense of Plotkin. The system aims at defining and computing partial continuous functionals. Some connections between denotational and operational semantics → for Mω are investigated. It is shown that → is correct with respect to the denotational semantics. Conversely, → is complete in the sense that if a program denotes some number k, then it is reducible to the numeral nk.Restricting to the primitive recursive kernel ℘Rω of Mω, it is shown that → is strongly normalising with uniquely determined normal forms. The twist is the design of fixed point style conversion rules for constants μl accounting for parallelly bounded parallel search such that correctness and strong normalisation hold. Thereupon, minor alternations to → bring about that every reduction sequence for a program of ℘Rω terminates either in a numeral nk if the program denotes k, or in the term (⊂-1)0 if the program denotes the “undefined” object. Thus, ℘Rω can be considered a primitive recursive version of Plotkin's LPA+∃·