An Operational Semantics of Simply-Typed Lambda Calculus with String Diagrams

by jesuslopon 7/10/2024, 11:29 AMwith 1 comments

by jesuslopon 7/10/2024, 11:29 AM

In 1996 DC Keenan wrote "To dissect a mockingbird" [1] giving a graphical notation for lambda calculus, expressing it in pictures with an evocative semantics. 28 years later the linked piece gives a categorical string-diagram version. Applications arise when you are interested in mappings that have extra behavior other than that of functions, as in probabilistic programming, automatic differentiation.

[1] https://dkeenan.com/Lambda/