TY - GEN

T1 - Partiality, revisited

T2 - 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017

AU - Altenkirch, Thorsten

AU - Danielsson, Nils Anders

AU - Kraus, Nicolai

PY - 2017/3/16

Y1 - 2017/3/16

N2 - Capretta’s delay monad can be used to model partial computations, but it has the “wrong” notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the “right” notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory—a higher inductive-inductive type—we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.

AB - Capretta’s delay monad can be used to model partial computations, but it has the “wrong” notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the “right” notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory—a higher inductive-inductive type—we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.

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

UR - http://eprints.nottingham.ac.uk/38095/

U2 - 10.1007/978-3-662-54458-7_31

DO - 10.1007/978-3-662-54458-7_31

M3 - Conference contribution

AN - SCOPUS:85015911815

SN - 9783662544570

T3 - Lecture Notes in Computer Science

SP - 534

EP - 549

BT - Foundations of Software Science and Computation Structures

A2 - Esparza, Javier

A2 - Murawski, Andrzej S.

PB - Springer

Y2 - 22 April 2017 through 29 April 2017

ER -