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

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

Standard

A theory of linear typings as flows on 3-valent graphs. / Zeilberger, Noam.

LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. New York, NY, USA : Association for Computing Machinery (ACM), 2018. p. 919-928.

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

Harvard

Zeilberger, N 2018, A theory of linear typings as flows on 3-valent graphs. in LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery (ACM), New York, NY, USA, pp. 919-928, Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Oxford, United Kingdom, 9/07/18. https://doi.org/10.1145/3209108.3209121

APA

Zeilberger, N. (2018). A theory of linear typings as flows on 3-valent graphs. In LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 919-928). Association for Computing Machinery (ACM). https://doi.org/10.1145/3209108.3209121

Vancouver

Zeilberger N. A theory of linear typings as flows on 3-valent graphs. In LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. New York, NY, USA: Association for Computing Machinery (ACM). 2018. p. 919-928 https://doi.org/10.1145/3209108.3209121

Author

Zeilberger, Noam. / A theory of linear typings as flows on 3-valent graphs. LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. New York, NY, USA : Association for Computing Machinery (ACM), 2018. pp. 919-928

Bibtex

@inproceedings{e965541f1b8a4b1bb401f15225c92bcf,
title = "A theory of linear typings as flows on 3-valent graphs",
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. ",
keywords = "lambda calculus and combinatory logic, graph theory, nowhere-zero flows, linear logic, skew-closed categories",
author = "Noam Zeilberger",
year = "2018",
month = jul
day = "9",
doi = "10.1145/3209108.3209121",
language = "English",
isbn = "9781450355834",
pages = "919--928",
booktitle = "LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science",
publisher = "Association for Computing Machinery (ACM)",
address = "United States",
note = "Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ; Conference date: 09-07-2018 Through 12-07-2018",

}

RIS

TY - GEN

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

AU - Zeilberger, Noam

PY - 2018/7/9

Y1 - 2018/7/9

N2 - 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.

AB - 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.

KW - lambda calculus and combinatory logic

KW - graph theory

KW - nowhere-zero flows

KW - linear logic

KW - skew-closed categories

U2 - 10.1145/3209108.3209121

DO - 10.1145/3209108.3209121

M3 - Conference contribution

SN - 9781450355834

SP - 919

EP - 928

BT - LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

PB - Association for Computing Machinery (ACM)

CY - New York, NY, USA

T2 - Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Y2 - 9 July 2018 through 12 July 2018

ER -