The Functional Machine Calculus

TL;DR

The paper introduces the Functional Machine Calculus (FMC), a model of higher-order computation with effects like state, input/output, and probabilistic behavior, extending lambda-calculus with effect encoding and algebraic reduction.

Contribution

It generalizes lambda-calculus with multiple stacks and sequencing, enabling effect encoding and algebraic effect reduction, and proves confluence and termination properties.

Findings

FMC encodes effects into abstraction and application, preserving lambda-calculus properties.

Algebraic reduction laws for effects enable effect combination without operational complexity.

FMC with types guarantees termination of computations.

Abstract

This paper presents the Functional Machine Calculus (FMC) as a simple model of higher-order computation with "reader/writer" effects: higher-order mutable store, input/output, and probabilistic and non-deterministic computation. The FMC derives from the lambda-calculus by taking the standard operational perspective of a call-by-name stack machine as primary, and introducing two natural generalizations. One, "locations", introduces multiple stacks, which each may represent an effect and so enable effect operators to be encoded into the abstraction and application constructs of the calculus. The second, "sequencing", is known from kappa-calculus and concatenative programming languages, and introduces the imperative notions of "skip" and "sequence". This enables the encoding of reduction strategies, including call-by-value lambda-calculus and monadic constructs. The encoding of effects into generalized abstraction and application means that standard results from the lambda-calculus may carry over to effects. The main result is confluence, which is possible because encoded effects reduce algebraically rather than operationally. Reduction generates the familiar algebraic laws for state, and unlike in the monadic setting, reader/writer effects combine seamlessly. A system of simple types confers termination of the machine.