Loading…
Programming as a Mathematical Exercise [and Discussion]
This paper contains a formal framework within which logic, set theory and programming are presented together. These elements can be presented together because, in this work, we no longer regard a (procedural) programming notation (such as PASCAL) as a notation for expressing a computation; rather, w...
Saved in:
| Published in: | Philosophical transactions of the Royal Society of London. Series A: Mathematical and physical sciences 1984-10, Vol.312 (1522), p.447-473 |
|---|---|
| Main Authors: | , , , |
| Format: | Article |
| Language: | English |
| Subjects: | |
| Citations: | Items that this one cites |
| Online Access: | Get full text |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| cited_by | |
|---|---|
| cites | cdi_FETCH-LOGICAL-c421t-3abf336bd3d473bff052b242e889aee77068745ac9a9a5fb67fbfa84d7d26ee3 |
| container_end_page | 473 |
| container_issue | 1522 |
| container_start_page | 447 |
| container_title | Philosophical transactions of the Royal Society of London. Series A: Mathematical and physical sciences |
| container_volume | 312 |
| creator | Abrial, J. R. Shepherdson, J. C. Hillmore, J. S. Constable, R. L. |
| description | This paper contains a formal framework within which logic, set theory and programming are presented together. These elements
can be presented together because, in this work, we no longer regard a (procedural) programming notation (such as PASCAL)
as a notation for expressing a computation; rather, we regard it as a mere extension to the conventional language of logic
and set theory. The extension constitutes a convenient (economical) way of expressing certain relational statements. A consequence
of this point of view is that the activity of program construction is transformed into that of proof construction. To ensure
that this activity of proof construction can be given a sound mechanizable foundation, we present a number of theories in
the form of some basic deduction and definition rules. For instance, such theories compose the two logical calculi, a weaker
version of the standard Zermelo--Fraenkel set theory, as well as some other elementary mathematical theories leading up to
the construction of natural numbers. This last theory acts as a paradigm for the construction of other types such as sequences
or trees. Parallel to these mathematical constructions we axiomatize a certain programming notation by giving equivalents
to its basic constructs within logic and set theory. A number of other non-logical theories are also presented, which allows
us to completely mechanize the calculus of proof that is implied by this framework. |
| doi_str_mv | 10.1098/rsta.1984.0070 |
| format | article |
| fullrecord | <record><control><sourceid>jstor_highw</sourceid><recordid>TN_cdi_highwire_royalsociety_roypta_312_1522_447</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><jstor_id>37445</jstor_id><sourcerecordid>37445</sourcerecordid><originalsourceid>FETCH-LOGICAL-c421t-3abf336bd3d473bff052b242e889aee77068745ac9a9a5fb67fbfa84d7d26ee3</originalsourceid><addsrcrecordid>eNp9j0tLxDAUhYMoqKNbF666cNsxrybtSsQ3KIrOQhAJt20yk2GmLUlHHX-96VSEQXSVXO4595wPoQOChwRn6bHzLQxJlvIhxhJvoB3CJYlpJuhm-DPB4wSz52206_0UY0JEQneQfHD12MF8bqtxBD6C6A7aiZ5DawuYRRcf2hXW6-gFqjI6t75YeG_r6nUPbRmYeb3__Q7Q6PJidHYd395f3Zyd3sYFp6SNGeSGMZGXrOSS5cbghOaUU52mGWgtJRap5AkUGWSQmFxIkxtIeSlLKrRmAzTszxau9t5poxpn5-CWimDVUauOWnXUqqMOhqPe0IAPAMZBFfr_uDIsBQ1NBoj1MlcvQ_26sLpdqmm9cFUY_z7u_3M9Po1OScb4GyPUkoRShVNGsGSCJOrTNqtznUAFgbLeL7RaydZjfqce9qlT39buB4VJzpOwxP1yYseTd-u0WusWhiYc6_JWSXzFfvKvpUsv6qrVVbtmVGYxm6mmNOwLMju_mg</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>Programming as a Mathematical Exercise [and Discussion]</title><source>JSTOR Archival Journals and Primary Sources Collection</source><source>Royal Society Publishing Jisc Collections Royal Society Journals Read & Publish Transitional Agreement 2025 (reading list)</source><creator>Abrial, J. R. ; Shepherdson, J. C. ; Hillmore, J. S. ; Constable, R. L.</creator><creatorcontrib>Abrial, J. R. ; Shepherdson, J. C. ; Hillmore, J. S. ; Constable, R. L.</creatorcontrib><description>This paper contains a formal framework within which logic, set theory and programming are presented together. These elements
can be presented together because, in this work, we no longer regard a (procedural) programming notation (such as PASCAL)
as a notation for expressing a computation; rather, we regard it as a mere extension to the conventional language of logic
and set theory. The extension constitutes a convenient (economical) way of expressing certain relational statements. A consequence
of this point of view is that the activity of program construction is transformed into that of proof construction. To ensure
that this activity of proof construction can be given a sound mechanizable foundation, we present a number of theories in
the form of some basic deduction and definition rules. For instance, such theories compose the two logical calculi, a weaker
version of the standard Zermelo--Fraenkel set theory, as well as some other elementary mathematical theories leading up to
the construction of natural numbers. This last theory acts as a paradigm for the construction of other types such as sequences
or trees. Parallel to these mathematical constructions we axiomatize a certain programming notation by giving equivalents
to its basic constructs within logic and set theory. A number of other non-logical theories are also presented, which allows
us to completely mechanize the calculus of proof that is implied by this framework.</description><identifier>ISSN: 1364-503X</identifier><identifier>ISSN: 0080-4614</identifier><identifier>EISSN: 1471-2962</identifier><identifier>EISSN: 2054-0272</identifier><identifier>DOI: 10.1098/rsta.1984.0070</identifier><identifier>CODEN: PTRMAD</identifier><language>eng</language><publisher>London: The Royal Society</publisher><subject>Applied sciences ; Computer science; control theory; systems ; Exact sciences and technology ; Logical proofs ; Mathematical functions ; Mathematical logic ; Mathematical relations ; Mathematical sequences ; Mathematical set theory ; Mathematical sets ; Mathematics education ; Natural numbers ; Ordinal notation ; Software ; Software engineering</subject><ispartof>Philosophical transactions of the Royal Society of London. Series A: Mathematical and physical sciences, 1984-10, Vol.312 (1522), p.447-473</ispartof><rights>Copyright 1984 The Royal Society</rights><rights>Scanned images copyright © 2017, Royal Society</rights><rights>1985 INIST-CNRS</rights><lds50>peer_reviewed</lds50><woscitedreferencessubscribed>false</woscitedreferencessubscribed><cites>FETCH-LOGICAL-c421t-3abf336bd3d473bff052b242e889aee77068745ac9a9a5fb67fbfa84d7d26ee3</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktopdf>$$Uhttps://www.jstor.org/stable/pdf/37445$$EPDF$$P50$$Gjstor$$H</linktopdf><linktohtml>$$Uhttps://www.jstor.org/stable/37445$$EHTML$$P50$$Gjstor$$H</linktohtml><link.rule.ids>314,780,784,27924,27925,58238,58471</link.rule.ids><backlink>$$Uhttp://pascal-francis.inist.fr/vibad/index.php?action=getRecordDetail&idt=9076247$$DView record in Pascal Francis$$Hfree_for_read</backlink></links><search><creatorcontrib>Abrial, J. R.</creatorcontrib><creatorcontrib>Shepherdson, J. C.</creatorcontrib><creatorcontrib>Hillmore, J. S.</creatorcontrib><creatorcontrib>Constable, R. L.</creatorcontrib><title>Programming as a Mathematical Exercise [and Discussion]</title><title>Philosophical transactions of the Royal Society of London. Series A: Mathematical and physical sciences</title><addtitle>Phil. Trans. R. Soc. Lond. A</addtitle><description>This paper contains a formal framework within which logic, set theory and programming are presented together. These elements
can be presented together because, in this work, we no longer regard a (procedural) programming notation (such as PASCAL)
as a notation for expressing a computation; rather, we regard it as a mere extension to the conventional language of logic
and set theory. The extension constitutes a convenient (economical) way of expressing certain relational statements. A consequence
of this point of view is that the activity of program construction is transformed into that of proof construction. To ensure
that this activity of proof construction can be given a sound mechanizable foundation, we present a number of theories in
the form of some basic deduction and definition rules. For instance, such theories compose the two logical calculi, a weaker
version of the standard Zermelo--Fraenkel set theory, as well as some other elementary mathematical theories leading up to
the construction of natural numbers. This last theory acts as a paradigm for the construction of other types such as sequences
or trees. Parallel to these mathematical constructions we axiomatize a certain programming notation by giving equivalents
to its basic constructs within logic and set theory. A number of other non-logical theories are also presented, which allows
us to completely mechanize the calculus of proof that is implied by this framework.</description><subject>Applied sciences</subject><subject>Computer science; control theory; systems</subject><subject>Exact sciences and technology</subject><subject>Logical proofs</subject><subject>Mathematical functions</subject><subject>Mathematical logic</subject><subject>Mathematical relations</subject><subject>Mathematical sequences</subject><subject>Mathematical set theory</subject><subject>Mathematical sets</subject><subject>Mathematics education</subject><subject>Natural numbers</subject><subject>Ordinal notation</subject><subject>Software</subject><subject>Software engineering</subject><issn>1364-503X</issn><issn>0080-4614</issn><issn>1471-2962</issn><issn>2054-0272</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>1984</creationdate><recordtype>article</recordtype><recordid>eNp9j0tLxDAUhYMoqKNbF666cNsxrybtSsQ3KIrOQhAJt20yk2GmLUlHHX-96VSEQXSVXO4595wPoQOChwRn6bHzLQxJlvIhxhJvoB3CJYlpJuhm-DPB4wSz52206_0UY0JEQneQfHD12MF8bqtxBD6C6A7aiZ5DawuYRRcf2hXW6-gFqjI6t75YeG_r6nUPbRmYeb3__Q7Q6PJidHYd395f3Zyd3sYFp6SNGeSGMZGXrOSS5cbghOaUU52mGWgtJRap5AkUGWSQmFxIkxtIeSlLKrRmAzTszxau9t5poxpn5-CWimDVUauOWnXUqqMOhqPe0IAPAMZBFfr_uDIsBQ1NBoj1MlcvQ_26sLpdqmm9cFUY_z7u_3M9Po1OScb4GyPUkoRShVNGsGSCJOrTNqtznUAFgbLeL7RaydZjfqce9qlT39buB4VJzpOwxP1yYseTd-u0WusWhiYc6_JWSXzFfvKvpUsv6qrVVbtmVGYxm6mmNOwLMju_mg</recordid><startdate>19841001</startdate><enddate>19841001</enddate><creator>Abrial, J. R.</creator><creator>Shepherdson, J. C.</creator><creator>Hillmore, J. S.</creator><creator>Constable, R. L.</creator><general>The Royal Society</general><general>Royal Society of London</general><scope>IQODW</scope><scope>AAYXX</scope><scope>CITATION</scope></search><sort><creationdate>19841001</creationdate><title>Programming as a Mathematical Exercise [and Discussion]</title><author>Abrial, J. R. ; Shepherdson, J. C. ; Hillmore, J. S. ; Constable, R. L.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c421t-3abf336bd3d473bff052b242e889aee77068745ac9a9a5fb67fbfa84d7d26ee3</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>1984</creationdate><topic>Applied sciences</topic><topic>Computer science; control theory; systems</topic><topic>Exact sciences and technology</topic><topic>Logical proofs</topic><topic>Mathematical functions</topic><topic>Mathematical logic</topic><topic>Mathematical relations</topic><topic>Mathematical sequences</topic><topic>Mathematical set theory</topic><topic>Mathematical sets</topic><topic>Mathematics education</topic><topic>Natural numbers</topic><topic>Ordinal notation</topic><topic>Software</topic><topic>Software engineering</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Abrial, J. R.</creatorcontrib><creatorcontrib>Shepherdson, J. C.</creatorcontrib><creatorcontrib>Hillmore, J. S.</creatorcontrib><creatorcontrib>Constable, R. L.</creatorcontrib><collection>Pascal-Francis</collection><collection>CrossRef</collection><jtitle>Philosophical transactions of the Royal Society of London. Series A: Mathematical and physical sciences</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Abrial, J. R.</au><au>Shepherdson, J. C.</au><au>Hillmore, J. S.</au><au>Constable, R. L.</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Programming as a Mathematical Exercise [and Discussion]</atitle><jtitle>Philosophical transactions of the Royal Society of London. Series A: Mathematical and physical sciences</jtitle><stitle>Phil. Trans. R. Soc. Lond. A</stitle><date>1984-10-01</date><risdate>1984</risdate><volume>312</volume><issue>1522</issue><spage>447</spage><epage>473</epage><pages>447-473</pages><issn>1364-503X</issn><issn>0080-4614</issn><eissn>1471-2962</eissn><eissn>2054-0272</eissn><coden>PTRMAD</coden><abstract>This paper contains a formal framework within which logic, set theory and programming are presented together. These elements
can be presented together because, in this work, we no longer regard a (procedural) programming notation (such as PASCAL)
as a notation for expressing a computation; rather, we regard it as a mere extension to the conventional language of logic
and set theory. The extension constitutes a convenient (economical) way of expressing certain relational statements. A consequence
of this point of view is that the activity of program construction is transformed into that of proof construction. To ensure
that this activity of proof construction can be given a sound mechanizable foundation, we present a number of theories in
the form of some basic deduction and definition rules. For instance, such theories compose the two logical calculi, a weaker
version of the standard Zermelo--Fraenkel set theory, as well as some other elementary mathematical theories leading up to
the construction of natural numbers. This last theory acts as a paradigm for the construction of other types such as sequences
or trees. Parallel to these mathematical constructions we axiomatize a certain programming notation by giving equivalents
to its basic constructs within logic and set theory. A number of other non-logical theories are also presented, which allows
us to completely mechanize the calculus of proof that is implied by this framework.</abstract><cop>London</cop><pub>The Royal Society</pub><doi>10.1098/rsta.1984.0070</doi><tpages>27</tpages></addata></record> |
| fulltext | fulltext |
| identifier | ISSN: 1364-503X |
| ispartof | Philosophical transactions of the Royal Society of London. Series A: Mathematical and physical sciences, 1984-10, Vol.312 (1522), p.447-473 |
| issn | 1364-503X 0080-4614 1471-2962 2054-0272 |
| language | eng |
| recordid | cdi_highwire_royalsociety_roypta_312_1522_447 |
| source | JSTOR Archival Journals and Primary Sources Collection; Royal Society Publishing Jisc Collections Royal Society Journals Read & Publish Transitional Agreement 2025 (reading list) |
| subjects | Applied sciences Computer science control theory systems Exact sciences and technology Logical proofs Mathematical functions Mathematical logic Mathematical relations Mathematical sequences Mathematical set theory Mathematical sets Mathematics education Natural numbers Ordinal notation Software Software engineering |
| title | Programming as a Mathematical Exercise [and Discussion] |
| url | http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-01T03%3A53%3A13IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-jstor_highw&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Programming%20as%20a%20Mathematical%20Exercise%20%5Band%20Discussion%5D&rft.jtitle=Philosophical%20transactions%20of%20the%20Royal%20Society%20of%20London.%20Series%20A:%20Mathematical%20and%20physical%20sciences&rft.au=Abrial,%20J.%20R.&rft.date=1984-10-01&rft.volume=312&rft.issue=1522&rft.spage=447&rft.epage=473&rft.pages=447-473&rft.issn=1364-503X&rft.eissn=1471-2962&rft.coden=PTRMAD&rft_id=info:doi/10.1098/rsta.1984.0070&rft_dat=%3Cjstor_highw%3E37445%3C/jstor_highw%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c421t-3abf336bd3d473bff052b242e889aee77068745ac9a9a5fb67fbfa84d7d26ee3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_jstor_id=37445&rfr_iscdi=true |