Mω considered as a programming language

Abstract

The 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 PRω 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 μ7 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 PRω 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, PRω can be considered a primitive recursive version of Plotkin's ℒPA+∃. © 1999 Elsevier Science B.V. All rights reserved.