No Cover Image

Journal article 553 views 71 downloads

Generating collection transformations from proofs

Michael Benedikt, Cécilia Pradic Orcid Logo

Proceedings of the ACM on Programming Languages, Volume: 5, Issue: POPL, Pages: 1 - 28

Swansea University Author: Cécilia Pradic Orcid Logo

  • 57933.pdf

    PDF | Version of Record

    © 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License

    Download (363.05KB)

Check full text

DOI (Published version): 10.1145/3434295

Abstract

Nested relations, built up from atomic types via product and set types, form a rich data model. Over the last decades the nested relational calculus, NRC, has emerged as a standard language for defining transformations on nested collections. NRC is a strongly-typed functional language which allows b...

Full description

Published in: Proceedings of the ACM on Programming Languages
ISSN: 2475-1421
Published: Association for Computing Machinery (ACM) 2021
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa57933
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2021-09-21T08:51:26Z
last_indexed 2021-11-25T04:16:43Z
id cronfa57933
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>57933</id><entry>2021-09-16</entry><title>Generating collection transformations from proofs</title><swanseaauthors><author><sid>3b6e9ebd791c875dac266b3b0b358a58</sid><ORCID>0000-0002-1600-8846</ORCID><firstname>Cécilia</firstname><surname>Pradic</surname><name>Cécilia Pradic</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2021-09-16</date><deptcode>SCS</deptcode><abstract>Nested relations, built up from atomic types via product and set types, form a rich data model. Over the last decades the nested relational calculus, NRC, has emerged as a standard language for defining transformations on nested collections. NRC is a strongly-typed functional language which allows building up transformations using tupling and projections, a singleton-former, and a map operation that lifts transformations on tuples to transformations on sets.In this work we describe an alternative declarative method of describing transformations in logic. A formula with distinguished inputs and outputs gives an implicit definition if one can prove that for each input there is only one output that satisfies it. Our main result shows that one can synthesize transformations from proofs that a formula provides an implicit definition, where the proof is in an intuitionistic calculus that captures a natural style of reasoning about nested collections. Our polynomial time synthesis procedure is based on an analog of Craig’s interpolation lemma, starting with a provable containment between terms representing nested collections and generating an NRC expression that interpolates between them.We further show that NRC expressions that implement an implicit definition can be found when there is a classical proof of functionality, not just when there is an intuitionistic one. That is, whenever a formula implicitly defines a transformation, there is an NRC expression that implements it.</abstract><type>Journal Article</type><journal>Proceedings of the ACM on Programming Languages</journal><volume>5</volume><journalNumber>POPL</journalNumber><paginationStart>1</paginationStart><paginationEnd>28</paginationEnd><publisher>Association for Computing Machinery (ACM)</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic>2475-1421</issnElectronic><keywords/><publishedDay>4</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2021</publishedYear><publishedDate>2021-01-04</publishedDate><doi>10.1145/3434295</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders>UKRI (EPSRC)</funders><projectreference>EP/M005852/1</projectreference><lastEdited>2023-06-23T18:17:14.8882378</lastEdited><Created>2021-09-16T18:00:47.9458635</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>Michael</firstname><surname>Benedikt</surname><order>1</order></author><author><firstname>Cécilia</firstname><surname>Pradic</surname><orcid>0000-0002-1600-8846</orcid><order>2</order></author></authors><documents><document><filename>57933__21095__98fb6c3d8ebc40d69dcf4ee4eb7ecfb5.pdf</filename><originalFilename>57933.pdf</originalFilename><uploaded>2021-10-05T14:44:46.3605339</uploaded><type>Output</type><contentLength>371761</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>© 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>http://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling v2 57933 2021-09-16 Generating collection transformations from proofs 3b6e9ebd791c875dac266b3b0b358a58 0000-0002-1600-8846 Cécilia Pradic Cécilia Pradic true false 2021-09-16 SCS Nested relations, built up from atomic types via product and set types, form a rich data model. Over the last decades the nested relational calculus, NRC, has emerged as a standard language for defining transformations on nested collections. NRC is a strongly-typed functional language which allows building up transformations using tupling and projections, a singleton-former, and a map operation that lifts transformations on tuples to transformations on sets.In this work we describe an alternative declarative method of describing transformations in logic. A formula with distinguished inputs and outputs gives an implicit definition if one can prove that for each input there is only one output that satisfies it. Our main result shows that one can synthesize transformations from proofs that a formula provides an implicit definition, where the proof is in an intuitionistic calculus that captures a natural style of reasoning about nested collections. Our polynomial time synthesis procedure is based on an analog of Craig’s interpolation lemma, starting with a provable containment between terms representing nested collections and generating an NRC expression that interpolates between them.We further show that NRC expressions that implement an implicit definition can be found when there is a classical proof of functionality, not just when there is an intuitionistic one. That is, whenever a formula implicitly defines a transformation, there is an NRC expression that implements it. Journal Article Proceedings of the ACM on Programming Languages 5 POPL 1 28 Association for Computing Machinery (ACM) 2475-1421 4 1 2021 2021-01-04 10.1145/3434295 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University UKRI (EPSRC) EP/M005852/1 2023-06-23T18:17:14.8882378 2021-09-16T18:00:47.9458635 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Michael Benedikt 1 Cécilia Pradic 0000-0002-1600-8846 2 57933__21095__98fb6c3d8ebc40d69dcf4ee4eb7ecfb5.pdf 57933.pdf 2021-10-05T14:44:46.3605339 Output 371761 application/pdf Version of Record true © 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License true eng http://creativecommons.org/licenses/by/4.0/
title Generating collection transformations from proofs
spellingShingle Generating collection transformations from proofs
Cécilia Pradic
title_short Generating collection transformations from proofs
title_full Generating collection transformations from proofs
title_fullStr Generating collection transformations from proofs
title_full_unstemmed Generating collection transformations from proofs
title_sort Generating collection transformations from proofs
author_id_str_mv 3b6e9ebd791c875dac266b3b0b358a58
author_id_fullname_str_mv 3b6e9ebd791c875dac266b3b0b358a58_***_Cécilia Pradic
author Cécilia Pradic
author2 Michael Benedikt
Cécilia Pradic
format Journal article
container_title Proceedings of the ACM on Programming Languages
container_volume 5
container_issue POPL
container_start_page 1
publishDate 2021
institution Swansea University
issn 2475-1421
doi_str_mv 10.1145/3434295
publisher Association for Computing Machinery (ACM)
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 Nested relations, built up from atomic types via product and set types, form a rich data model. Over the last decades the nested relational calculus, NRC, has emerged as a standard language for defining transformations on nested collections. NRC is a strongly-typed functional language which allows building up transformations using tupling and projections, a singleton-former, and a map operation that lifts transformations on tuples to transformations on sets.In this work we describe an alternative declarative method of describing transformations in logic. A formula with distinguished inputs and outputs gives an implicit definition if one can prove that for each input there is only one output that satisfies it. Our main result shows that one can synthesize transformations from proofs that a formula provides an implicit definition, where the proof is in an intuitionistic calculus that captures a natural style of reasoning about nested collections. Our polynomial time synthesis procedure is based on an analog of Craig’s interpolation lemma, starting with a provable containment between terms representing nested collections and generating an NRC expression that interpolates between them.We further show that NRC expressions that implement an implicit definition can be found when there is a classical proof of functionality, not just when there is an intuitionistic one. That is, whenever a formula implicitly defines a transformation, there is an NRC expression that implements it.
published_date 2021-01-04T18:17:09Z
_version_ 1769514602725376000
score 11.016235

Similar Items