No Cover Image

E-Thesis 170 views 181 downloads

Algebraic Stream Processing / Robert Stephens

DOI (Published version): 10.23889/SUthesis.57505

Abstract

We identify and analyse the typically higher-order approaches to stream processing in the literature. From this analysis we motivate an alternative approach to the specification of SPSs as STs based on an essentially first-order equational representation. This technique is called Cartesian form spec...

Full description

Published: Swansea 1995
Institution: Swansea University
Degree level: Doctoral
Degree name: Ph.D
Supervisor: Thompson, Ben.
URI: https://cronfa.swan.ac.uk/Record/cronfa57505
first_indexed 2021-08-03T11:01:51Z
last_indexed 2023-01-11T14:37:28Z
id cronfa57505
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2022-09-29T13:17:48.9816828</datestamp><bib-version>v2</bib-version><id>57505</id><entry>2021-08-03</entry><title>Algebraic Stream Processing</title><swanseaauthors/><date>2021-08-03</date><abstract>We identify and analyse the typically higher-order approaches to stream processing in the literature. From this analysis we motivate an alternative approach to the specification of SPSs as STs based on an essentially first-order equational representation. This technique is called Cartesian form specification. More specifically, while STs are properly second-order objects we show that using Cartesian forms, the second-order models needed to formalise STs are so weak that we may use and develop well-understood first-order methods from computability theory and mathematical logic to reason about their properties. Indeed, we show that by specifying STs equationally in Cartesian form as primitive recursive functions we have the basis of a new, general purpose and mathematically sound theory of stream processing that emphasises the formal specification and formal verification of STs. The main topics that we address in the development of this theory are as follows. We present a theoretically well-founded general purpose stream processing language ASTRAL (Algebraic Stream TRAnsformer Language) that supports the use of modular specification techniques for full second-order STs. We show how ASTRAL specifications can be given a Cartesian form semantics using the language PREQ that is an equational characterisation of the primitive recursive functions. In more detail, we show that by compiling ASTRAL specifications into an equivalent Cartesian form in PREQ we can use first-order equational logic with induction as a logical calculus to reason about STs. In particular, using this calculus we identify a syntactic class of correctness statements for which the verification of ASTRAL programmes is decidable relative to this calculus. We define an effective algorithm based on term re-writing techniques to implement this calculus and hence to automatically verify a very broad class of STs including conventional hardware devices. Finally, we analyse the properties of this abstract algorithm as a proof assistant and discuss various techniques that have been adopted to develop software tools based on this algorithm.</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>1</publishedDay><publishedMonth>9</publishedMonth><publishedYear>1995</publishedYear><publishedDate>1995-09-01</publishedDate><doi>10.23889/SUthesis.57505</doi><url/><notes>Stephens, Robert. University of Wales Swansea/ University of Wales Swansea. Dept. of Computer Science. 1995 EThOS ID: uk.bl.ethos.639104 Copyright: The Author.</notes><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Thompson, Ben.</supervisor><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><apcterm/><funders/><projectreference/><lastEdited>2022-09-29T13:17:48.9816828</lastEdited><Created>2021-08-03T11:58:21.1037984</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Robert</firstname><surname>Stephens</surname><order>1</order></author></authors><documents><document><filename>57505__20524__cf9bec5a60a14f738d6f194c7259fe25.pdf</filename><originalFilename>Stephens_S_PhD_Thesis_Final.pdf</originalFilename><uploaded>2021-08-03T12:34:04.5230406</uploaded><type>Output</type><contentLength>13775205</contentLength><contentType>application/pdf</contentType><version>E-Thesis &#x2013; open access</version><cronfaStatus>true</cronfaStatus><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2022-09-29T13:17:48.9816828 v2 57505 2021-08-03 Algebraic Stream Processing 2021-08-03 We identify and analyse the typically higher-order approaches to stream processing in the literature. From this analysis we motivate an alternative approach to the specification of SPSs as STs based on an essentially first-order equational representation. This technique is called Cartesian form specification. More specifically, while STs are properly second-order objects we show that using Cartesian forms, the second-order models needed to formalise STs are so weak that we may use and develop well-understood first-order methods from computability theory and mathematical logic to reason about their properties. Indeed, we show that by specifying STs equationally in Cartesian form as primitive recursive functions we have the basis of a new, general purpose and mathematically sound theory of stream processing that emphasises the formal specification and formal verification of STs. The main topics that we address in the development of this theory are as follows. We present a theoretically well-founded general purpose stream processing language ASTRAL (Algebraic Stream TRAnsformer Language) that supports the use of modular specification techniques for full second-order STs. We show how ASTRAL specifications can be given a Cartesian form semantics using the language PREQ that is an equational characterisation of the primitive recursive functions. In more detail, we show that by compiling ASTRAL specifications into an equivalent Cartesian form in PREQ we can use first-order equational logic with induction as a logical calculus to reason about STs. In particular, using this calculus we identify a syntactic class of correctness statements for which the verification of ASTRAL programmes is decidable relative to this calculus. We define an effective algorithm based on term re-writing techniques to implement this calculus and hence to automatically verify a very broad class of STs including conventional hardware devices. Finally, we analyse the properties of this abstract algorithm as a proof assistant and discuss various techniques that have been adopted to develop software tools based on this algorithm. E-Thesis Swansea 1 9 1995 1995-09-01 10.23889/SUthesis.57505 Stephens, Robert. University of Wales Swansea/ University of Wales Swansea. Dept. of Computer Science. 1995 EThOS ID: uk.bl.ethos.639104 Copyright: The Author. COLLEGE NANME COLLEGE CODE Swansea University Thompson, Ben. Doctoral Ph.D 2022-09-29T13:17:48.9816828 2021-08-03T11:58:21.1037984 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Robert Stephens 1 57505__20524__cf9bec5a60a14f738d6f194c7259fe25.pdf Stephens_S_PhD_Thesis_Final.pdf 2021-08-03T12:34:04.5230406 Output 13775205 application/pdf E-Thesis – open access true true eng
title Algebraic Stream Processing
spellingShingle Algebraic Stream Processing
,
title_short Algebraic Stream Processing
title_full Algebraic Stream Processing
title_fullStr Algebraic Stream Processing
title_full_unstemmed Algebraic Stream Processing
title_sort Algebraic Stream Processing
author ,
author2 Robert Stephens
format E-Thesis
publishDate 1995
institution Swansea University
doi_str_mv 10.23889/SUthesis.57505
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description We identify and analyse the typically higher-order approaches to stream processing in the literature. From this analysis we motivate an alternative approach to the specification of SPSs as STs based on an essentially first-order equational representation. This technique is called Cartesian form specification. More specifically, while STs are properly second-order objects we show that using Cartesian forms, the second-order models needed to formalise STs are so weak that we may use and develop well-understood first-order methods from computability theory and mathematical logic to reason about their properties. Indeed, we show that by specifying STs equationally in Cartesian form as primitive recursive functions we have the basis of a new, general purpose and mathematically sound theory of stream processing that emphasises the formal specification and formal verification of STs. The main topics that we address in the development of this theory are as follows. We present a theoretically well-founded general purpose stream processing language ASTRAL (Algebraic Stream TRAnsformer Language) that supports the use of modular specification techniques for full second-order STs. We show how ASTRAL specifications can be given a Cartesian form semantics using the language PREQ that is an equational characterisation of the primitive recursive functions. In more detail, we show that by compiling ASTRAL specifications into an equivalent Cartesian form in PREQ we can use first-order equational logic with induction as a logical calculus to reason about STs. In particular, using this calculus we identify a syntactic class of correctness statements for which the verification of ASTRAL programmes is decidable relative to this calculus. We define an effective algorithm based on term re-writing techniques to implement this calculus and hence to automatically verify a very broad class of STs including conventional hardware devices. Finally, we analyse the properties of this abstract algorithm as a proof assistant and discuss various techniques that have been adopted to develop software tools based on this algorithm.
published_date 1995-09-01T04:53:08Z
_version_ 1851548645147541504
score 11.089698

Similar Items