Home
Scholarly Works
Computing with Semirings and Weak Rig Groupoids
Conference

Computing with Semirings and Weak Rig Groupoids

Abstract

The original formulation of the Curry–Howard correspondence relates propositional logic to the simply-typed λ$$\lambda $$-calculus at three levels: the syntax of propositions corresponds to the syntax of types; the proofs of propositions correspond to programs of the corresponding types; and the normalization of proofs corresponds to the evaluation of programs. This rich correspondence has inspired our community for half a century and has been generalized to deal with more advanced logics and programming models. We propose a variant of this correspondence which is inspired by conservation of information and recent homotopy theoretic approaches to type theory.Our proposed correspondence naturally relates semirings to reversible programming languages: the syntax of semiring elements corresponds to the syntax of types; the proofs of semiring identities correspond to (reversible) programs of the corresponding types; and equivalences between algebraic proofs correspond to meaning-preserving program transformations and optimizations. These latter equivalences are not ad hoc: the same way semirings arise naturally out of the structure of types, a categorical look at the structure of proof terms gives rise to (at least) a weak rig groupoid structure, and the coherence laws are exactly the program transformations we seek. Thus it is algebra, rather than logic, which finally leads us to our correspondence.

Authors

Carette J; Sabry A

Series

Lecture Notes in Computer Science

Volume

9632

Pagination

pp. 123-148

Publisher

Springer Nature

Publication Date

January 1, 2016

DOI

10.1007/978-3-662-49498-1_6

Conference proceedings

Lecture Notes in Computer Science

ISSN

0302-9743

Labels

View published work (Non-McMaster Users)

Contact the Experts team