Abstract
This thesis is an exploration in two parts dealing with the nature of termination in probabilistically-branching variants of the lambda calculus.The first part approaches the issue of probabilistic-termination of the Probabilistic Event lambda-calculus -- a confluent probabilistic calculus with the effect decomposed into choice and event-generation -- via a novel and simple type system. The thesis goes on to explore the semantics of this calculus through a machine operated by a sequential extension. A normalisation result on the terms of this extension, typed by probabilistically-parameterised stack transformations, reflects back onto the original system, giving the desired termination result.
The second part presents an unfinished investigation into almost-sure termination via sequential calculus, wherein we define an annotated two-sided sequent calculus, and outline its relationship to co-recursive loops and to continuations. Termination of the non-recursive fragment is shown via an embedding in a known natural deduction formulation, while the result for the full system -- which corresponds to almost-sure termination -- is left as a conjecture from the given probabilistic variant of the type system.
| Date of Award | 25 Jun 2025 |
|---|---|
| Original language | English |
| Awarding Institution |
|
| Supervisor | Willem Heijltjes (Supervisor) & Alessio Guglielmi (Supervisor) |