Confluence with basic effects

Add to your list(s) Download to your calendar using vCal

• Willem Heijltjes (University of Bath)
• Friday 19 November 2021, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Anupam Das.

It is well-known that adding computational effects to the lambda-calculus introduces non-confluence. In this talk I will discuss an approach that, surprisingly, avoids this issue, and gives a confluent lambda-calculus with basic, “sequential” effects: input and output, mutable higher-order store, non-determinism, and probabilistic computation.

The premise is to combine the familiar idea that abstraction and application can operationally be viewed as pop- and push-actions for a stack machine, with the observation that effect operations such as input, output, update, and lookup are readily encoded in pop- and push-actions. By parameterizing abstraction and application in a set of “locations”, representing storage cells and input and output streams, one obtains a remarkably simple lambda-calculus with effects. Confluence is possible because the usual, operational meaning of effects corresponds to evaluation by an abstract machine (which has a fixed strategy), while beta-reduction (where non-confluence would arise) corresponds to manipulation of effect operations by their algebraic laws, in the sense of Plotkin and Power.

A further step is needed to give control over when effects are called – i.e. eager or lazy evaluation. A natural framework for this is the kappa-calculus, introduced by Hasegawa and extended to higher-order by Power and Thielecke. As it appears not well studied in the literature, some basic properties and semantic aspects are explored in this talk.

The resulting “Functional Machine Calculus” (FMC) combines kappa-calculus with basic effects, and beyond confluence it has some further interesting properties. The encoding of effects extends to types, yielding a new approach to typed higher-order store. A simple and natural proof shows that types guarantee termination of the stack machine. Semantically, beta-eta equivalence gives a premonoidal category, in the sense of Power and Robinson, while a coarser equivalence based on machine evaluation gives the free Cartesian closed category, making the FMC equivalent to lambda-calculus.

(Part of this is joint work with Chris Barrett and Guy McCusker.)

=== Zoom details ===

Topic: Theory Seminar – Willem Heijltjes Time: Nov 19, 2021 01:45 PM London

Join Zoom Meeting https://bham-ac-uk.zoom.us/j/87199065286?pwd=T0NFZlh3Zi9aUWpDK3A3SXpscE5NUT09

Meeting ID: 871 9906 5286 Passcode: 024452 One tap mobile +442039017895,,87199065286#,,,,024452# United Kingdom +442080806591,,87199065286#,,,,024452# United Kingdom

Dial by your location +44 203 901 7895 United Kingdom +44 208 080 6591 United Kingdom +44 208 080 6592 United Kingdom +44 330 088 5830 United Kingdom +44 131 460 1196 United Kingdom +44 203 481 5237 United Kingdom +44 203 481 5240 United Kingdom Meeting ID: 871 9906 5286 Passcode: 024452 Find your local number: https://bham-ac-uk.zoom.us/u/kdWTLZhluU

Join by SIP 87199065286@zoomcrc.com

Join by H.323 162.255.37.11 (US West) 162.255.36.11 (US East) 115.114.131.7 (India Mumbai) 115.114.115.7 (India Hyderabad) 213.19.144.110 (Amsterdam Netherlands) 213.244.140.110 (Germany) 103.122.166.55 (Australia Sydney) 103.122.167.55 (Australia Melbourne) 149.137.40.110 (Singapore) 64.211.144.160 (Brazil) 149.137.68.253 (Mexico) 69.174.57.160 (Canada Toronto) 65.39.152.160 (Canada Vancouver) 207.226.132.110 (Japan Tokyo) 149.137.24.110 (Japan Osaka) Meeting ID: 871 9906 5286 Passcode: 024452

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.