A theory of linear typings as flows on 3-valent graphs

DOI10.1145/3209108.3209121MaRDI QIDQ5145371zbMATH OpenOpenAlexFDO

Authors Noam Zeilberger

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

graph theorylinear logicnowhere-zero flowslambda calculus and combinatory logicskew-closed categories

Mathematics Subject Classification ID

Flows in graphs (05C21) Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Abstract: Building on recently established enumerative connections between lambda calculus and the theory of embedded graphs (or "maps"), this paper develops an analogy between typing (of lambda terms) and coloring (of maps). Our starting point is the classical notion of an abelian group-valued "flow" on an abstract graph (Tutte, 1954). Typing a linear lambda term may be naturally seen as constructing a flow (on an embedded 3-valent graph with boundary) valued in a more general algebraic structure consisting of a preordered set equipped with an "implication" operation and unit satisfying composition, identity, and unit laws. Interesting questions and results from the theory of flows (such as the existence of nowhere-zero flows) may then be re-examined from the standpoint of lambda calculus and logic. For example, we give a characterization of when the local flow relations (across vertices) may be categorically lifted to a global flow relation (across the boundary), proving that this holds just in case the underlying map has the orientation of a lambda term. We also develop a basic theory of rewriting of flows that suggests topological meanings for classical completeness results in combinatory logic, and introduce a polarized notion of flow, which draws connections to the theory of proof-nets in linear logic and to bidirectional typing.

Recommendations

• Linear lambda terms as invariants of rooted trivalent maps
• On some enumerative problems in lambda calculus
• A new graphical calculus of proofs
• A correspondence between rooted planar maps and normal planar lambda terms
• Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic

Cited in

(5)

• A correspondence between rooted planar maps and normal planar lambda terms
• Proof Theory of Partially Normal Skew Monoidal Categories
• Bijections between planar maps and planar linear normal \(\lambda\)-terms with connectivity condition
• Eilenberg-Kelly reloaded
• Linear lambda terms as invariants of rooted trivalent maps

This page was built for publication: A theory of linear typings as flows on 3-valent graphs

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