{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T17:22:28Z","timestamp":1694625748466},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1998,9,1]],"date-time":"1998-09-01T00:00:00Z","timestamp":904608000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1998,9]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            <jats:sc>Computing Science is a new subject, and we have not yet achieved the unification of theories that should support a proper understanding of its structure<\/jats:sc>\n            . CAR Hoare and He Jifeng, 1998.\n          <\/jats:p>\n          <jats:p>\n            In this paper we use\n            <jats:sc>Priestley duality<\/jats:sc>\n            and\n            <jats:sc>J\u00f3nsson\/Tarski duality<\/jats:sc>\n            to translate between four versions of program semantics: the relational model, predicate transformer semantics, information systems, and powerdomains. Our point of entry is the relational model, a kind of Kripke semantics, in which programs are thought of as input-output relations over a structured state space. Specifically, we present the state space as a certain kind of Priestley space, and programs as certain structure-preserving relations over such a space. We then derive, in circular fashion, a predicate transformer semantics from the relational model, an information system from the predicate transformer semantics, a powerdomain from the information system, and the original relational model back again from the powerdomain. The information system is also shown to be related to Hoare logic. To clarify the intuition behind this approach we present a case study, which is a \u2018Priestley version\u2019 of the so-called\n            <jats:sc>universal domain<\/jats:sc>\n            due to Plotkin, and we explicate various ideas about properties of programs and predicates in terms of this case study.\n          <\/jats:p>","DOI":"10.1007\/pl00003923","type":"journal-article","created":{"date-parts":[[2006,2,17]],"date-time":"2006-02-17T14:53:18Z","timestamp":1140187998000},"page":"1-29","source":"Crossref","is-referenced-by-count":0,"title":["Unification of Four Versions of Program Semantics"],"prefix":"10.1145","volume":"10","author":[{"given":"Ingrid","family":"Rewitzky","sequence":"first","affiliation":[{"name":"Department of Mathematics and Applied Mathematics, University of Cape Town, South Africa, , , , , , ZA"}]},{"given":"Chris","family":"Brink","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Applied Mathematics, University of Cape Town, South Africa, , , , , , ZA"}]}],"member":"320","reference":[{"key":"p_1","first-page":"1","article-title":"Domain theory in logical form","author":"Abramsky S.","year":"1991","journal-title":"Annals of Pure and Applied Logic 51."},{"key":"p_2","first-page":"1","volume-title":"S Abramsky, DM Gabbay and TSE Maibaum (eds), Handbook of Logic in Computer Science Vol III","author":"Abramsky S.","year":"1994"},{"key":"p_3","first-page":"181","volume-title":"Defining liveness. Information Processing Letters 21","author":"Alpern B.","year":"1985"},{"key":"p_4","volume-title":"Models and Ultraproducts","author":"Bell J. L.","year":"1971","edition":"2"},{"key":"p_5","first-page":"301","volume-title":"AM Borzyszkowski and S Sokolowoski (eds), Mathematical Foundations of Computer Science","author":"Bonsangue M.","year":"1993"},{"key":"p_6","series-title":"Lecture Notes in Computer Science 789.","doi-asserted-by":"crossref","first-page":"822","DOI":"10.1007\/3-540-57887-0_127","volume-title":"M Hagiya and JC Mitchell (eds), Proceedings of TACS'94, Sendai, Japan","author":"Bonsangue M.","year":"1994"},{"key":"p_7","first-page":"79","volume-title":"Duality beyond sober spaces: Topological spaces and observable frames. Theoretical Computer Science 151 (1). (Special Issue dedicated to AMAST\/MASK Workshop on Topology and Completion in Semantics","author":"Bonsangue M.","year":"1993"},{"key":"p_8","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0021-8693(81)90179-4","article-title":"Boolean modules","author":"Brink C.","year":"1981","journal-title":"Journal of Algebra 71."},{"key":"p_9","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/BF01196091","article-title":"Power structures","author":"Brink C.","year":"1993","journal-title":"Algebra Universalis 30."},{"key":"p_10","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF01215410","article-title":"Peirce algebras","author":"Brink C.","year":"1994","journal-title":"Formal Aspects of Computing 6."},{"key":"p_11","volume-title":"Propositional logic, powerdomains and information. To appear in Logic at Work: Essays in Honour of Helena Rasiowa. E. Orlowska (ed)","author":"Brink C.","year":"1998"},{"key":"p_12","unstructured":"[BrR9?] Brink C. and Rewitzky I.: Power Structures and Program Semantics. Manuscript of a book to appear in the series Studies in Logic Language and Information."},{"key":"p_13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-8130-3","volume-title":"A Course in Universal Algebra","author":"Burris S.","year":"1981"},{"issue":"9","key":"p_14","first-page":"341","article-title":"Distributive and modular laws in the arithmetic of relation algebras","volume":"1","author":"Chin L. H.","year":"1951","journal-title":"University of California Publications in Mathematics"},{"key":"p_15","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/BF00383451","article-title":"Remarks on Priestley duality for distributive lattices","author":"Cignoli R.","year":"1991","journal-title":"Order 8."},{"key":"p_16","volume-title":"Introduction to Lattices and Order","author":"Davey B.","year":"1990"},{"issue":"8","key":"p_17","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","article-title":"Guarded commands, nondeterminacy and formal derivation of programs","volume":"18","author":"Dijkstra E. W.","year":"1975","journal-title":"Communications of the ACM"},{"key":"p_18","volume-title":": A Discipline of Programming","author":"Dijkstra E. W.","year":"1976"},{"key":"p_19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"Dijkstra E. W.","year":"1990"},{"key":"p_20","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0304-3975(90)90097-2","article-title":"Nondeterministic information systems and their domains","author":"Droste M.","year":"1990","journal-title":"Theoretical Computer Science 75."},{"key":"p_21","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(93)90056-Y","article-title":"I-Categories as a framework for solving domain equations","author":"Edalaat A.","year":"1993","journal-title":"Theoretical Computer Science 115."},{"key":"p_22","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0168-0072(89)90032-8","article-title":"Varieties of complex algebras","author":"Goldblatt R.","year":"1989","journal-title":"Annals of Pure and Applied Logic 44."},{"key":"p_23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"Gries D.","year":"1981"},{"key":"p_24","first-page":"136","volume-title":"Proceedings of the 4th International Colloquium on Automata, Languages and Programming","author":"Guerreiro P.","year":"1980"},{"key":"p_25","series-title":"Lecture Notes in Computer Science 137","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-11494-7_12","volume-title":"Another characterisation of weakest preconditions","author":"Guerreiro P.","year":"1982"},{"key":"p_26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9855-7","volume-title":": Lectures on Boolean Algebras","author":"Halmos P. R.","year":"1974"},{"key":"p_27","first-page":"37","article-title":"A duality for Boolean algebras with operators","author":"Hansoul G.","year":"1983","journal-title":"Algebra Universalis 17."},{"key":"p_28","volume-title":"Cylindric Algebras Part 1","author":"Henkin L.","year":"1985"},{"issue":"10","key":"p_29","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare C. A. R.","year":"1969","journal-title":"Communications of the ACM"},{"key":"p_30","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/27651.27653","article-title":"Laws of programming","author":"Hoare C. A. R.","year":"1987","journal-title":"Communications of the ACM 30."},{"key":"p_31","volume-title":"Unifying Theories of Programming","author":"Hoare C. A. R.","year":"1998"},{"key":"p_32","first-page":"135","article-title":"Consistent and complementary formal theories of the semantics of programming languages","author":"Hoare C. A. R.","year":"1974","journal-title":"Acta Informatica 3."},{"key":"p_33","doi-asserted-by":"crossref","DOI":"10.4324\/9780203290644","volume-title":"A New Introduction to Modal Logic","author":"Hughes G. E.","year":"1996"},{"key":"p_34","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BF00290146","article-title":"General correctness: A unification of partial and total correctness","author":"Jacobs D.","year":"1985","journal-title":"Acta Informatica 22."},{"key":"p_35","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF02483728","article-title":"Varieties of relation algebras","author":"J\u00f3nsson B.","year":"1982","journal-title":"Algebra Universalis 15."},{"key":"p_36","doi-asserted-by":"crossref","first-page":"891","DOI":"10.2307\/2372123","article-title":"Boolean algebras with operators I","author":"J\u00f3nsson B.","year":"1951","journal-title":"American Journal of Mathematics 73."},{"key":"p_37","doi-asserted-by":"crossref","first-page":"127","DOI":"10.2307\/2372074","article-title":"Boolean algebras with operators II","author":"J\u00f3nsson B.","year":"1952","journal-title":"American Journal of Mathematics 74."},{"key":"p_38","volume-title":": Stone Spaces","author":"Johnstone P. T.","year":"1982"},{"key":"p_39","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0304-3975(93)90090-G","article-title":"Concrete domains","author":"Kahn G.","year":"1993","journal-title":"Theoretical Computer Science 121."},{"key":"p_40","first-page":"67","article-title":"Semantic analysis of modal logic. Zentrum f\u00fcr Mathematik","author":"Kripke S.","year":"1963","journal-title":"Logik und Grundl. Mathematik 9."},{"key":"p_41","volume-title":"Proceedings of the Oxford Topology Symposium","author":"Kwiatkowska M. Z.","year":"1989"},{"key":"p_42","series-title":"Lecture Notes in Computer Science 298.","first-page":"134","volume-title":"M. Main, A. Melton, M. Mislove, D. Schmidt (eds), Proceedings of the Third Workshop on Mathematical Foundations of Programming Language Semantics","author":"Lawson J. D.","year":"1987"},{"key":"p_43","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1016\/0020-0190(80)90048-4","article-title":"A simple relation between relational and predicate transformer semantics for nondeterministic programs","author":"Majster-Cederbaum M. E.","year":"1980","journal-title":"Information Processing Letters 4."},{"key":"p_44","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9452-5","volume-title":": Mathematical Logic","author":"Monk J. D.","year":"1976"},{"key":"p_45","volume-title":"Handbook of Boolean Algebras Vol I","author":"Monk J. D.","year":"1989"},{"issue":"4","key":"p_46","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/69558.69559","article-title":"A generalisation of Dijkstra\u2019s calculus","volume":"11","author":"Nelson G.","year":"1989","journal-title":"ACM Transactions of Programming Languages and Systems"},{"key":"p_47","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1137\/0205035","article-title":"A powerdomain construction","author":"Plotkin G. D.","year":"1976","journal-title":"SIAM Journal of Computing 5."},{"key":"p_48","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0022-0000(78)90006-5","article-title":"T \u03c9 as a universal domain","author":"Plotkin G. D.","year":"1978","journal-title":"Journal of Computer and System Sciences 17."},{"key":"p_49","series-title":"Lecture Notes in Computer Science 86.","first-page":"525","volume-title":"D. Bjorner (ed), Proceedings of the 1979 Copenhagen Winter School in Abstract Software Specifications","author":"Plotkin G. D.","year":"1980"},{"key":"p_50","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1112\/blms\/2.2.186","article-title":"Representation of distributive lattices by means of ordered Stone spaces","author":"Priestley H. A.","year":"1970","journal-title":"Bulletin of the London Mathematical Society 2."},{"key":"p_51","first-page":"507","volume-title":"Proceedings of the London Mathematical Society 24 (3).","author":"Priestley H. A.","year":"1972"},{"key":"p_52","first-page":"39","article-title":"Ordered sets and duality for distributive lattices","author":"Priestley H. A.","year":"1984","journal-title":"Annals of Discrete Mathematics 23."},{"key":"p_53","series-title":"Lecture Notes in Pure and Applied Mathematics 101.","first-page":"237","volume-title":"RE Hoffmann and KH Hoffmann (eds), Continuous Lattices and their Applications","author":"Priestley H. A.","year":"1985"},{"key":"p_54","article-title":"Spectral spaces","volume":"101","author":"Priestley H. A.","year":"1994","journal-title":"Journal of Pure and Applied Algebra 94. pp."},{"key":"p_55","first-page":"78","volume-title":"Eighth Summer Conference at Queen\u2019s College (G Itzkowitz et al. (ed)). Annals of the New York Academy of Sciences 728","author":"Priestley H. A.","year":"1994"},{"issue":"2","key":"p_56","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/BF01211604","article-title":"Predicate transformers as power operations","volume":"7","author":"Rewitzky I.","year":"1995","journal-title":"Formal Aspects in Computing"},{"key":"p_58","series-title":"Lecture Notes in Computer Science 140.","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1007\/BFb0012801","volume-title":"M. Nielsen and E.M. Schmidt (eds), Proceedings of ICALP 9","author":"Scott D. S.","year":"1982"},{"key":"p_59","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0022-0000(78)90048-X","article-title":"Power domains","author":"Smyth M. B.","year":"1978","journal-title":"Journal of Computer and System Sciences 16."},{"key":"p_60","series-title":"Lecture Notes in Computer Science 154.","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/BFb0036946","volume-title":"J. Diaz (ed), Proceedings of ICALP 10","author":"Smyth M. B.","year":"1983"},{"key":"p_61","volume-title":"S Abramsky, DM Gabbay, TSE Maibaum (eds), Handbook of Logic in Computer Science.","author":"Smyth M. B.","year":"1992"},{"key":"p_62","first-page":"37","article-title":"The theory of representations for Boolean algebras","author":"Stone M. H.","year":"1936","journal-title":"Transactions of the American Mathematical Society 40."},{"key":"p_63","doi-asserted-by":"crossref","first-page":"177","DOI":"10.4064\/fm-24-1-177-198","article-title":"Zur Grundlegung der Boole\u2019schen Algebra I","author":"Tarski A.","year":"1935","journal-title":"Fundamenta Mathematicae 24."},{"key":"p_64","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/2268577","article-title":"On the calculus of relations","author":"Tarski A.","year":"1941","journal-title":"Journal of Symbolic Logic 6."},{"key":"p_65","volume-title":"Topology via Logic","author":"Vickers S.","year":"1989"},{"key":"p_66","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/S0022-0000(77)80006-8","article-title":"A characterisation of weakest preconditions","author":"Wand M.","year":"1977","journal-title":"Journal of Computer and System Sciences 15."},{"key":"p_67","volume-title":"General Topology","author":"Willard S.","year":"1970"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/PL00003923.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/PL00003923\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/PL00003923","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:28:41Z","timestamp":1641482921000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/PL00003923"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,9]]},"references-count":66,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,9]]}},"alternative-id":["10.1007\/PL00003923"],"URL":"https:\/\/doi.org\/10.1007\/pl00003923","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,9]]}}}