Skip to content

Abstracts.2018.GraphLam

Jump to bottom
Fabian edited this page Jan 15, 2020 · 3 revisions

A graphical calculus interpreting lambda-calculus

by Joel Sjögren

We use graphs to look at symmetries and asymmetries of the lambda calculus. A function t is typically thought of as a box which takes an input u and produces an output (t u). The graphical framework puts u and t u on an equal footing, in the sense that the names "input" and "output" for u and (t u) become arbitrary: use of an "output" (t u) is also an "input" to the contrapositive of t, and t and its contrapositive have very similar representations as graphs.

We will consider the inverse operations

  • pairing/unpairing
  • abstraction/application

and ponder the identifications

  • pairing = application
  • unpairing = abstraction

as well as the more radical

  • pairing = unpairing.

I will also show you how to translate "type programs" into the same graphs. Using this language we can express list reversal in a novel way, but the reversal of a concrete list does not reduce as fully as one might hope.

The operational semantics presented is a bit restrictive, as it is essentially GLC [1] which was superseded by chemlambda [2][3][4]. The latter is probably better, but I haven't understood how to use it yet. For normalizing lambda terms, either will do.

[Edit: The extent of normalization will correspond not to the usual untyped lambda calculus, but to the variant of lambda calculus which has explicit weakening and contraction. A counterexample to my claim just above is the application (3 3), where 3 is a church numeral (a -> a) -> (a -> a), which reduces to something akin to 3 * 3 * 3 but not 27. ]

References:

Clone this wiki locally