### Abstract

Misra [8] recently introduced a regular data structure, called powerlists, using which he showed how many data parallel algorithms, including Batcher's merge sort, bitonic sort, fast Fourier transform, prefix sum, can be described concisely using recursion. The elegance of these recursive descriptions is further reflected in deducing properties of these algorithms. It is shown in this paper how such proofs can be easily automated in a theorem prover RRL (Rewrite Rule Laboratory) based on equational and rewriting techniques. In particular, the cover set method for automating proofs by induction in RRL generates proofs which preserve the clarity and succinctness, to a large extant, of hand proofs given in [8]. This is illustrated using a correctness proof of Batcher's merge sort algorithm. Mechanically generated proofs from specifications ofpowerlists and parallel algorithms using different apl~roaches are contrasted. It is shown that one gets longer, complex proofs with many cases if powerlists are modeled as a subtype of lists. However, if powerlists are specified using a proposal by Kapur [2] in which the algebraic specification method is extended to associate applicability conditions with functions of a data type thus allowing constructors of a data structure to be partial, then one gets compact and elegant proofs, similar to the ones reported in [8]. Applicability conditions can be used to provide con. tezts for axioms and proofs just like type information. The effectiveness of the proposed axiomatic method becomes all the more evident while reasoning about nested powerlists for modeling n-dimensional arrays, for example, in specifying and reasoning about a transformation for embedding a multi-dimensional array into a hypercube such that adjacency of nodes is preserved by the transformation. A mechanically generated proof of this property of the embedding transformation, which was not proved in Misra's paper, is discussed in detail. This suggests that the proposed approach for automating reasoning about data parallel algorithms described recursively using powerlists should scale up, especially if structural properties of nested powerlists are built into RRL.

Original language | English (US) |
---|---|

Title of host publication | Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings |

Editors | V.S. Alagar, Maurice Nivat |

Publisher | Springer Verlag |

Pages | 416-430 |

Number of pages | 15 |

ISBN (Print) | 3540600434, 9783540600435 |

DOIs | |

State | Published - Jan 1 1995 |

Event | 4th International Conference on Algebraic Methodology and Software Technology, AMAST 1995 - Montreal, Canada Duration: Jul 3 1995 → Jul 7 1995 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 936 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 4th International Conference on Algebraic Methodology and Software Technology, AMAST 1995 |
---|---|

Country | Canada |

City | Montreal |

Period | 7/3/95 → 7/7/95 |

### Fingerprint

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings*(pp. 416-430). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 936). Springer Verlag. https://doi.org/10.1007/3-540-60043-4_68

**Automated reasoning about parallel algorithms using powerlists.** / Kapur, Deepak; Subramaniam, M.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 936, Springer Verlag, pp. 416-430, 4th International Conference on Algebraic Methodology and Software Technology, AMAST 1995, Montreal, Canada, 7/3/95. https://doi.org/10.1007/3-540-60043-4_68

}

TY - GEN

T1 - Automated reasoning about parallel algorithms using powerlists

AU - Kapur, Deepak

AU - Subramaniam, M.

PY - 1995/1/1

Y1 - 1995/1/1

N2 - Misra [8] recently introduced a regular data structure, called powerlists, using which he showed how many data parallel algorithms, including Batcher's merge sort, bitonic sort, fast Fourier transform, prefix sum, can be described concisely using recursion. The elegance of these recursive descriptions is further reflected in deducing properties of these algorithms. It is shown in this paper how such proofs can be easily automated in a theorem prover RRL (Rewrite Rule Laboratory) based on equational and rewriting techniques. In particular, the cover set method for automating proofs by induction in RRL generates proofs which preserve the clarity and succinctness, to a large extant, of hand proofs given in [8]. This is illustrated using a correctness proof of Batcher's merge sort algorithm. Mechanically generated proofs from specifications ofpowerlists and parallel algorithms using different apl~roaches are contrasted. It is shown that one gets longer, complex proofs with many cases if powerlists are modeled as a subtype of lists. However, if powerlists are specified using a proposal by Kapur [2] in which the algebraic specification method is extended to associate applicability conditions with functions of a data type thus allowing constructors of a data structure to be partial, then one gets compact and elegant proofs, similar to the ones reported in [8]. Applicability conditions can be used to provide con. tezts for axioms and proofs just like type information. The effectiveness of the proposed axiomatic method becomes all the more evident while reasoning about nested powerlists for modeling n-dimensional arrays, for example, in specifying and reasoning about a transformation for embedding a multi-dimensional array into a hypercube such that adjacency of nodes is preserved by the transformation. A mechanically generated proof of this property of the embedding transformation, which was not proved in Misra's paper, is discussed in detail. This suggests that the proposed approach for automating reasoning about data parallel algorithms described recursively using powerlists should scale up, especially if structural properties of nested powerlists are built into RRL.

AB - Misra [8] recently introduced a regular data structure, called powerlists, using which he showed how many data parallel algorithms, including Batcher's merge sort, bitonic sort, fast Fourier transform, prefix sum, can be described concisely using recursion. The elegance of these recursive descriptions is further reflected in deducing properties of these algorithms. It is shown in this paper how such proofs can be easily automated in a theorem prover RRL (Rewrite Rule Laboratory) based on equational and rewriting techniques. In particular, the cover set method for automating proofs by induction in RRL generates proofs which preserve the clarity and succinctness, to a large extant, of hand proofs given in [8]. This is illustrated using a correctness proof of Batcher's merge sort algorithm. Mechanically generated proofs from specifications ofpowerlists and parallel algorithms using different apl~roaches are contrasted. It is shown that one gets longer, complex proofs with many cases if powerlists are modeled as a subtype of lists. However, if powerlists are specified using a proposal by Kapur [2] in which the algebraic specification method is extended to associate applicability conditions with functions of a data type thus allowing constructors of a data structure to be partial, then one gets compact and elegant proofs, similar to the ones reported in [8]. Applicability conditions can be used to provide con. tezts for axioms and proofs just like type information. The effectiveness of the proposed axiomatic method becomes all the more evident while reasoning about nested powerlists for modeling n-dimensional arrays, for example, in specifying and reasoning about a transformation for embedding a multi-dimensional array into a hypercube such that adjacency of nodes is preserved by the transformation. A mechanically generated proof of this property of the embedding transformation, which was not proved in Misra's paper, is discussed in detail. This suggests that the proposed approach for automating reasoning about data parallel algorithms described recursively using powerlists should scale up, especially if structural properties of nested powerlists are built into RRL.

UR - http://www.scopus.com/inward/record.url?scp=84957804802&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957804802&partnerID=8YFLogxK

U2 - 10.1007/3-540-60043-4_68

DO - 10.1007/3-540-60043-4_68

M3 - Conference contribution

AN - SCOPUS:84957804802

SN - 3540600434

SN - 9783540600435

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 416

EP - 430

BT - Algebraic Methodology and Software Technology - 4th International Conference, AMAST 1995, Proceedings

A2 - Alagar, V.S.

A2 - Nivat, Maurice

PB - Springer Verlag

ER -