Mω considered as a programming language

Annals of Pure and Applied Logic 99 (1-3):73-92 (1999)
  Copy   BIBTEX

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 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 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 0 if the program denotes the “undefined” object. Thus, Rω can be considered a primitive recursive version of Plotkin's PA+·

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 94,045

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Intuitionistic fixed point logic.Ulrich Berger & Hideki Tsuiki - 2021 - Annals of Pure and Applied Logic 172 (3):102903.
A Conjecture on Numeral Systems.Karim Nour - 1997 - Notre Dame Journal of Formal Logic 38 (2):270-275.
Logic of Domains.Guo-Qiang Zhang - 2012 - Springer Verlag.
Term rewriting theory for the primitive recursive functions.E. A. Cichon & Andreas Weiermann - 1997 - Annals of Pure and Applied Logic 83 (3):199-223.
Introduction to clarithmetic III.Giorgi Japaridze - 2014 - Annals of Pure and Applied Logic 165 (1):241-252.

Analytics

Added to PP
2014-01-16

Downloads
22 (#700,182)

6 months
5 (#837,836)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The Computational Power of ℳω.Dag Normann & Christian Rørdam - 2002 - Mathematical Logic Quarterly 48 (1):117-124.

Add more citations

References found in this work

Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
Subrecursive hierarchies on Scott domains.Karl-Heinz Niggl - 1993 - Archive for Mathematical Logic 32 (4):239-257.

View all 9 references / Add more references