Journal article 736 views 98 downloads
Generating collection transformations from proofs
Proceedings of the ACM on Programming Languages, Volume: 5, Issue: POPL, Pages: 1 - 28
Swansea University Author: Cécilia Pradic
-
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)
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...
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 |
first_indexed |
2021-09-21T08:51:26Z |
---|---|
last_indexed |
2024-11-14T12:12:45Z |
id |
cronfa57933 |
recordtype |
SURis |
fullrecord |
<?xml version="1.0"?><rfc1807><datestamp>2023-06-23T18:17:14.8882378</datestamp><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>MACS</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>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</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 |
2023-06-23T18:17:14.8882378 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 MACS 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 Mathematics and Computer Science School COLLEGE CODE MACS 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-04T14:00:45Z |
_version_ |
1822682666020896768 |
score |
11.048929 |