DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2025.31

Simple Types for Probabilistic Termination

Authors: Willem Heijltjes and Georgina Majury

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

We present a new typing discipline to guarantee the probability of termination in probabilistic lambda-calculi. The main contribution is a particular naturality and simplicity: our probabilistic types are as simple types, but generated from probabilities as base types, representing a least probability of termination. Simple types are recovered by restricting probabilities to one. Our vehicle is the Probabilistic Event Lambda-Calculus by Dal Lago, Guerrieri, and Heijltjes, which presents a solution to the issue of confluence in probabilistic lambda-calculi. Our probabilistic type system provides an alternative solution to that using counting quantifiers by Antonelli, Dal Lago, and Pistone, for the same calculus. The problem that both type systems address is to give a lower bound on the probability that terms head-normalize. Following the recent Functional Machine Calculus by Heijltjes, our development takes the (simplified) Krivine machine as primary, and proceeds via an extension of the calculus with sequential composition and identity on the machine. Our type system then gives a natural account of termination probability on the Krivine machine, reflected back onto head-normalization for the original calculus. In this way we are able to avoid the use of counting quantifiers, while improving on the termination bounds given by Antonelli, Dal Lago, and Pistone.

Cite as

Willem Heijltjes and Georgina Majury. Simple Types for Probabilistic Termination. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{heijltjes_et_al:LIPIcs.CSL.2025.31,
  author =	{Heijltjes, Willem and Majury, Georgina},
  title =	{{Simple Types for Probabilistic Termination}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{31:1--31:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.31},
  URN =		{urn:nbn:de:0030-drops-227885},
  doi =		{10.4230/LIPIcs.CSL.2025.31},
  annote =	{Keywords: lambda-calculus, probabilistic termination, simple types}
}

Document

DOI: 10.4230/LIPIcs.CSL.2023.10

The Functional Machine Calculus II: Semantics

Authors: Chris Barrett, Willem Heijltjes, and Guy McCusker

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract

The Functional Machine Calculus (FMC), recently introduced by the second author, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects. In this paper, we explore the denotational semantics of the FMC. We have three main contributions: first, we argue that its syntax - in which both effects and lambda-calculus are realised using the same syntactic constructs - is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.

Cite as

Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus II: Semantics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barrett_et_al:LIPIcs.CSL.2023.10,
  author =	{Barrett, Chris and Heijltjes, Willem and McCusker, Guy},
  title =	{{The Functional Machine Calculus II: Semantics}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.10},
  URN =		{urn:nbn:de:0030-drops-174716},
  doi =		{10.4230/LIPIcs.CSL.2023.10},
  annote =	{Keywords: lambda-calculus, computational effects, denotational semantics, strong normalization}
}

Search Results

Documents authored by Heijltjes, Willem

Simple Types for Probabilistic Termination

Abstract

Cite as

The Functional Machine Calculus II: Semantics

Abstract

Cite as

Thanks for your feedback!

Could not send message