Abstract
The Functional Machine Calculus (FMC) was recently introduced as a generalization of the lambdacalculus to include higherorder global state, probabilistic and non deterministic choice, and input and ouput, while retaining confluence. The calculus can encode both the callbyname and callbyvalue semantics of these effects. This is enabled by two independent generalizations, both natural from the perspective of the FMC’s operational semantics, which is given by a simple (multi)stack machine.
The first generalization decomposes the syntax of the lambdacalculus in a way that allows for sequential composition of terms and the encoding of reduction strate gies. Specifically, there exist translations of the callbyname and callbyvalue lambdacalculus which preserve operational semantics. The second parameterizes application and abstraction in terms of ‘locations’ (corresponding to the multiple stacks of the machine), which gives a unification of the operational semantics, syn tax, and reduction rules of the given effects with those of the lambdacalculus. The FMC further comes equipped with a simple type system which restricts and captures the behaviour of effects.
This thesis makes two main contributions, showing that two fundamental prop erties of the lambdacalculus are preserved by the FMC. The first is to show that the categorical semantics of the FMC, modulo an appropriate equational theory, is given by the free Cartesian closed category. The equational theory is validated by a notion of observational equivalence. The second contribution is a proof that typed FMCterms are strongly normalising. This is an extension (and small simplification) of Gandy’s proof for the lambdacalculus, which additionally emphasizes its latent operational intuition.
Date of Award  13 Jan 2023 

Original language  English 
Awarding Institution 

Supervisor  Willem Heijltjes (Supervisor) 
Keywords
 lambdacalculus
 computational effects
 normalisation
 categorical semantics