Countable nondeterminism and random assignment

Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalenc...

Full description

Saved in:
Bibliographic Details
Published in:Journal of the ACM 1986-10, Vol.33 (4), p.724-767
Main Authors: APT, K. R, PLOTKIN, G. D
Format: Article
Language:English
Subjects:
Applied sciences
Completeness
Computer science
control theory
systems
Continuity
Equivalence
Exact sciences and technology
Programming languages
Recursion
Recursive
Semantics
Software
Transformations
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c355t-ade63cece0043365768da875cdb3757c2356c8766df2d7fbea44fddb1ae3ede3
cites cdi_FETCH-LOGICAL-c355t-ade63cece0043365768da875cdb3757c2356c8766df2d7fbea44fddb1ae3ede3
container_end_page 767
container_issue 4
container_start_page 724
container_title Journal of the ACM
container_volume 33
creator APT, K. R
PLOTKIN, G. D
description Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. A Hoare-like proof system for total correctness is also introduced and its soundness and completeness in an appropriate sense are shown. Finally, the recursion theoretic complexity of the notions introduced is studied. Admission of countable nondeterminism results in a lack of continuity of various semantic functions, and this is shown to be necessary for any semantics satisfying appropriate conditions. In proofs of total correctness, one resorts to the use of (countable) ordinals, and it is shown that all recursive ordinals are needed.
doi_str_mv 10.1145/6490.6494
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_miscellaneous_28897010</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>1808054063</sourcerecordid><originalsourceid>FETCH-LOGICAL-c355t-ade63cece0043365768da875cdb3757c2356c8766df2d7fbea44fddb1ae3ede3</originalsourceid><addsrcrecordid>eNp9kE1Lw0AQhhdRsFYP_oMeRPSQOJv97FGKX1Dw0oO3sNmdSCTZ1J304L93S4tHL-_MwDPvMC9j1xxKzqV60HIJZRZ5wmZcKVMYoT5O2QwAZKEk5-fsgugrj1CBmbFyNe7i5JoeF3GMASdMQxc7GhYuhkXKMuaWqPuMA8bpkp21rie8OtY52zw_bVavxfr95W31uC68UGoqXEAtPHrMV4XQymgbnDXKh0YYZXwllPbWaB3aKpi2QSdlG0LDHQoMKObs9mC7TeP3Dmmqh4489r2LOO6orqxdGuCQwbt_QW7BgpKgRUbvD6hPI1HCtt6mbnDpp-ZQ77Or99ntRWb25mjryLu-zTn4jv4WbCWW-SXxC_-fbX0</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>1808054063</pqid></control><display><type>article</type><title>Countable nondeterminism and random assignment</title><source>Association for Computing Machinery:Jisc Collections:ACM OPEN Journals 2023-2025 (reading list)</source><creator>APT, K. R ; PLOTKIN, G. D</creator><creatorcontrib>APT, K. R ; PLOTKIN, G. D</creatorcontrib><description>Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. A Hoare-like proof system for total correctness is also introduced and its soundness and completeness in an appropriate sense are shown. Finally, the recursion theoretic complexity of the notions introduced is studied. Admission of countable nondeterminism results in a lack of continuity of various semantic functions, and this is shown to be necessary for any semantics satisfying appropriate conditions. In proofs of total correctness, one resorts to the use of (countable) ordinals, and it is shown that all recursive ordinals are needed.</description><identifier>ISSN: 0004-5411</identifier><identifier>EISSN: 1557-735X</identifier><identifier>DOI: 10.1145/6490.6494</identifier><identifier>CODEN: JACOAH</identifier><language>eng</language><publisher>New York, NY: Association for Computing Machinery</publisher><subject>Applied sciences ; Completeness ; Computer science; control theory; systems ; Continuity ; Equivalence ; Exact sciences and technology ; Programming languages ; Recursion ; Recursive ; Semantics ; Software ; Transformations</subject><ispartof>Journal of the ACM, 1986-10, Vol.33 (4), p.724-767</ispartof><rights>1987 INIST-CNRS</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c355t-ade63cece0043365768da875cdb3757c2356c8766df2d7fbea44fddb1ae3ede3</citedby><cites>FETCH-LOGICAL-c355t-ade63cece0043365768da875cdb3757c2356c8766df2d7fbea44fddb1ae3ede3</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,777,781,27905,27906</link.rule.ids><backlink>$$Uhttp://pascal-francis.inist.fr/vibad/index.php?action=getRecordDetail&amp;idt=8239768$$DView record in Pascal Francis$$Hfree_for_read</backlink></links><search><creatorcontrib>APT, K. R</creatorcontrib><creatorcontrib>PLOTKIN, G. D</creatorcontrib><title>Countable nondeterminism and random assignment</title><title>Journal of the ACM</title><description>Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. A Hoare-like proof system for total correctness is also introduced and its soundness and completeness in an appropriate sense are shown. Finally, the recursion theoretic complexity of the notions introduced is studied. Admission of countable nondeterminism results in a lack of continuity of various semantic functions, and this is shown to be necessary for any semantics satisfying appropriate conditions. In proofs of total correctness, one resorts to the use of (countable) ordinals, and it is shown that all recursive ordinals are needed.</description><subject>Applied sciences</subject><subject>Completeness</subject><subject>Computer science; control theory; systems</subject><subject>Continuity</subject><subject>Equivalence</subject><subject>Exact sciences and technology</subject><subject>Programming languages</subject><subject>Recursion</subject><subject>Recursive</subject><subject>Semantics</subject><subject>Software</subject><subject>Transformations</subject><issn>0004-5411</issn><issn>1557-735X</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>1986</creationdate><recordtype>article</recordtype><recordid>eNp9kE1Lw0AQhhdRsFYP_oMeRPSQOJv97FGKX1Dw0oO3sNmdSCTZ1J304L93S4tHL-_MwDPvMC9j1xxKzqV60HIJZRZ5wmZcKVMYoT5O2QwAZKEk5-fsgugrj1CBmbFyNe7i5JoeF3GMASdMQxc7GhYuhkXKMuaWqPuMA8bpkp21rie8OtY52zw_bVavxfr95W31uC68UGoqXEAtPHrMV4XQymgbnDXKh0YYZXwllPbWaB3aKpi2QSdlG0LDHQoMKObs9mC7TeP3Dmmqh4489r2LOO6orqxdGuCQwbt_QW7BgpKgRUbvD6hPI1HCtt6mbnDpp-ZQ77Or99ntRWb25mjryLu-zTn4jv4WbCWW-SXxC_-fbX0</recordid><startdate>19861001</startdate><enddate>19861001</enddate><creator>APT, K. R</creator><creator>PLOTKIN, G. D</creator><general>Association for Computing Machinery</general><scope>IQODW</scope><scope>AAYXX</scope><scope>CITATION</scope><scope>7SC</scope><scope>8FD</scope><scope>JQ2</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope></search><sort><creationdate>19861001</creationdate><title>Countable nondeterminism and random assignment</title><author>APT, K. R ; PLOTKIN, G. D</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c355t-ade63cece0043365768da875cdb3757c2356c8766df2d7fbea44fddb1ae3ede3</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>1986</creationdate><topic>Applied sciences</topic><topic>Completeness</topic><topic>Computer science; control theory; systems</topic><topic>Continuity</topic><topic>Equivalence</topic><topic>Exact sciences and technology</topic><topic>Programming languages</topic><topic>Recursion</topic><topic>Recursive</topic><topic>Semantics</topic><topic>Software</topic><topic>Transformations</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>APT, K. R</creatorcontrib><creatorcontrib>PLOTKIN, G. D</creatorcontrib><collection>Pascal-Francis</collection><collection>CrossRef</collection><collection>Computer and Information Systems Abstracts</collection><collection>Technology Research Database</collection><collection>ProQuest Computer Science Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><jtitle>Journal of the ACM</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>APT, K. R</au><au>PLOTKIN, G. D</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Countable nondeterminism and random assignment</atitle><jtitle>Journal of the ACM</jtitle><date>1986-10-01</date><risdate>1986</risdate><volume>33</volume><issue>4</issue><spage>724</spage><epage>767</epage><pages>724-767</pages><issn>0004-5411</issn><eissn>1557-735X</eissn><coden>JACOAH</coden><abstract>Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. A Hoare-like proof system for total correctness is also introduced and its soundness and completeness in an appropriate sense are shown. Finally, the recursion theoretic complexity of the notions introduced is studied. Admission of countable nondeterminism results in a lack of continuity of various semantic functions, and this is shown to be necessary for any semantics satisfying appropriate conditions. In proofs of total correctness, one resorts to the use of (countable) ordinals, and it is shown that all recursive ordinals are needed.</abstract><cop>New York, NY</cop><pub>Association for Computing Machinery</pub><doi>10.1145/6490.6494</doi><tpages>44</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 0004-5411
ispartof Journal of the ACM, 1986-10, Vol.33 (4), p.724-767
issn 0004-5411
1557-735X
language eng
recordid cdi_proquest_miscellaneous_28897010
source Association for Computing Machinery:Jisc Collections:ACM OPEN Journals 2023-2025 (reading list)
subjects Applied sciences
Completeness
Computer science
control theory
systems
Continuity
Equivalence
Exact sciences and technology
Programming languages
Recursion
Recursive
Semantics
Software
Transformations
title Countable nondeterminism and random assignment
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-19T21%3A13%3A48IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Countable%20nondeterminism%20and%20random%20assignment&rft.jtitle=Journal%20of%20the%20ACM&rft.au=APT,%20K.%20R&rft.date=1986-10-01&rft.volume=33&rft.issue=4&rft.spage=724&rft.epage=767&rft.pages=724-767&rft.issn=0004-5411&rft.eissn=1557-735X&rft.coden=JACOAH&rft_id=info:doi/10.1145/6490.6494&rft_dat=%3Cproquest_cross%3E1808054063%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c355t-ade63cece0043365768da875cdb3757c2356c8766df2d7fbea44fddb1ae3ede3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=1808054063&rft_id=info:pmid/&rfr_iscdi=true