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

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+·
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/s0168-0072(99)80002-5
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 58,425
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

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

Citations of this work BETA

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

Add more citations

Similar books and articles

< I> M_< Sup> Ω Considered as a Programming Language.Karl-Heinz Niggl - 1999 - Annals of Pure and Applied Logic 99 (1):73-92.
Understanding Programming Languages.Raymond Turner - 2007 - Minds and Machines 17 (2):203-216.
Programming Languages as Technical Artifacts.Raymond Turner - 2014 - Philosophy and Technology 27 (3):377-397.
Abpl.Mike Ainsworth - 1993 - Acta Biotheoretica 41 (1-2):43-51.
Domains and Lambda-Calculi.Roberto M. Amadio - 1998 - Cambridge University Press.
On the Relation Between SPARQL1.1 and Answer Set Programming.Axel Polleres & Johannes Peter Wallner - 2013 - Journal of Applied Non-Classical Logics 23 (1-2):159-212.


Added to PP index

Total views
15 ( #654,147 of 2,420,822 )

Recent downloads (6 months)
4 ( #192,268 of 2,420,822 )

How can I increase my downloads?


My notes