The Functional Machine Calculus III: Choice (Early Announcement)

TL;DR

This paper extends the Functional Machine Calculus to include exception handling and loop constructs, enhancing its ability to model complex computational effects while maintaining desirable properties like confluence and typed termination.

Contribution

It introduces new extensions to the calculus that enable modeling of exceptions and loops, broadening its expressive power for computational effects.

Findings

Successfully encodes exception handling and loops

Maintains confluence and typed termination with extensions

Enhances modeling of complex computational effects

Abstract

The Functional Machine Calculus (Heijltjes 2022) is an extension of the lambda-calculus that preserves confluent reduction and typed termination, while enabling both call-by-name and call-by-value reduction behaviour and encoding the computational effects of mutable higher-order store, input/output, and probabilistic computation. In this note the calculus is extended to capture exception handling and loop constructs.