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

Noam Zeilberger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)
101 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationLICS '18
Subtitle of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Place of PublicationNew York, NY, USA
PublisherAssociation for Computing Machinery (ACM)
Pages919-928
Number of pages10
ISBN (Print)9781450355834
DOIs
Publication statusPublished - 9 Jul 2018
EventThirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Publication series

NameSymposium on Logic in Computer Science
ISSN (Print)1043-6871

Conference

ConferenceThirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Country/TerritoryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Keywords

  • lambda calculus and combinatory logic
  • graph theory
  • nowhere-zero flows
  • linear logic
  • skew-closed categories

Fingerprint

Dive into the research topics of 'A theory of linear typings as flows on 3-valent graphs'. Together they form a unique fingerprint.

Cite this