Publication
How to avoid the commuting conversions of IPC
| dc.contributor.author | Espírito Santo, José | |
| dc.contributor.author | Ferreira, Gilda | |
| dc.date.accessioned | 2025-12-29T14:35:53Z | |
| dc.date.available | 2025-12-29T14:35:53Z | |
| dc.date.issued | 2025-04-07 | |
| dc.description.abstract | Since the observation in 2006 that it is possible to embed IPC into the atomic polymorphic λ-calculus (a predicative fragment of system F with universal instantiations restricted to atomic formulas) different such embeddings appeared in the literature. All of them comprise the Russell-Prawitz translation of formulas, but have different strategies for the translation of proofs. Although these embeddings preserve proof identity, all fail in delivering preservation of reduction steps. In fact, they translate the commuting conversions of IPC to β-equality, or to other kinds of reduction or equality generated by new principles added to system F. The cause for this is the generation of redexes by the translation itself. In this paper, we present an embedding of IPC into atomic system F, still based on the same translation of formulas, but which maps commuting conversions to syntactic identity, while simulating the other kinds of reduction steps present in IPC by βη-reduction. In this sense the translation achieves a truly commuting-conversion-free image of IPC in atomic system F. | eng |
| dc.description.sponsorship | The author was partially financed by Portuguese Funds through FCT (Fundação para a Ciência e a Tecnologia) within the Projects UIDB/00013/2020 and UIDP/00013/2020. The author acknowledges the support of Fundação para a Ciência e a Tecnologia under the projects [UIDB/04561/2020, UIDB/00408/2020 and UIDP/00408/2020] and is also grateful to Centro de Matematica, Aplicações Fundamentais e Investigação Operacional and to LASIGE - Computer Science and Engineering Research Centre (Universidade de Lisboa). | |
| dc.identifier.citation | José Espírito Santo, Gilda Ferreira, How to avoid the commuting conversions of IPC, Theoretical Computer Science, Volume 1033, 2025, 115101, ISSN 0304-3975, https://doi.org/10.1016/j.tcs.2025.115101. | |
| dc.identifier.doi | 10.1016/j.tcs.2025.115101 | |
| dc.identifier.issn | 0304-3975 | |
| dc.identifier.uri | http://hdl.handle.net/10400.2/20574 | |
| dc.language.iso | eng | |
| dc.peerreviewed | yes | |
| dc.publisher | Elsevier BV | |
| dc.relation | Center of Mathematics of the University of Minho | |
| dc.relation | Center for Mathematics, Fundamental Applications and Operations Research | |
| dc.relation | LASIGE - Extreme Computing | |
| dc.relation.hasversion | https://www.sciencedirect.com/science/article/pii/S0304397525000398 | |
| dc.relation.ispartof | Theoretical Computer Science | |
| dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | |
| dc.title | How to avoid the commuting conversions of IPC | eng |
| dc.type | journal article | |
| dspace.entity.type | Publication | |
| oaire.awardTitle | Center of Mathematics of the University of Minho | |
| oaire.awardTitle | Center for Mathematics, Fundamental Applications and Operations Research | |
| oaire.awardTitle | LASIGE - Extreme Computing | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F00013%2F2020/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F04561%2F2020/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F00408%2F2020/PT | |
| oaire.citation.title | Theoretical Computer Science | |
| oaire.citation.volume | 1033 | |
| oaire.fundingStream | 6817 - DCRRNI ID | |
| oaire.fundingStream | 6817 - DCRRNI ID | |
| oaire.fundingStream | 6817 - DCRRNI ID | |
| oaire.version | http://purl.org/coar/version/c_71e4c1898caa6e32 | |
| person.familyName | Espírito Santo | |
| person.familyName | Ferreira | |
| person.givenName | José | |
| person.givenName | Gilda | |
| person.identifier.ciencia-id | A610-7A79-73AF | |
| person.identifier.ciencia-id | 0B1A-81E7-88B1 | |
| person.identifier.orcid | 0000-0002-6348-5653 | |
| person.identifier.orcid | 0000-0003-1447-9764 | |
| person.identifier.rid | H-9953-2013 | |
| person.identifier.scopus-author-id | 14037466100 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| relation.isAuthorOfPublication | 9994be17-d473-4de8-919c-cedfd920a1f6 | |
| relation.isAuthorOfPublication | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
| relation.isAuthorOfPublication.latestForDiscovery | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
| relation.isProjectOfPublication | 0382e7ad-5e57-45d3-a699-dc9da1ef20a5 | |
| relation.isProjectOfPublication | 7fccc76f-75a6-4346-89f1-0addcc4cfeed | |
| relation.isProjectOfPublication | 01a99baa-a025-45a3-bc2c-f4528aeae605 | |
| relation.isProjectOfPublication.latestForDiscovery | 0382e7ad-5e57-45d3-a699-dc9da1ef20a5 |