Axioms and decidability for type isomorphism in the presence of sums

DOI10.1145/2603088.2603115MaRDI QIDQ4635638zbMATH OpenOpenAlexFDO

Authors Danko Ilik

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.2567

zbMATH Keywords

completeness of axiomsdecidabilitysum typestype isomorphism

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Models of arithmetic and set theory (03C62)

Abstract: We consider the problem of characterizing isomorphisms of types, or, equivalently, constructive cardinality of sets, in the simultaneous presence of disjoint unions, Cartesian products, and exponentials. Mostly relying on results about polynomials with exponentiation that have not been used in our context, we derive: that the usual finite axiomatization known as High-School Identities (HSI) is complete for a significant subclass of types; that it is decidable for that subclass when two types are isomorphic; that, for the whole of the set of types, a recursive extension of the axioms of HSI exists that is complete; and that, for the whole of the set of types, the question as to whether two types are isomorphic is decidable when base types are to be interpreted as finite sets. We also point out certain related open problems.

Recommendations

• Isomorphisms of generic recursive polynomial types
• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• A short survey of isomorphisms of types
• Provable isomorphisms of types
• scientific article; zbMATH DE number 1086719

Cited in

(7)

• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• Isomorphisms of generic recursive polynomial types
• scientific article; zbMATH DE number 517016 (Why is no real title available?)
• scientific article; zbMATH DE number 1424011 (Why is no real title available?)
• An intuitionistic formula hierarchy based on high‐school identities
• scientific article; zbMATH DE number 6744295 (Why is no real title available?)
• Intensional harmony as isomorphism

This page was built for publication: Axioms and decidability for type isomorphism in the presence of sums

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635638)