Modelling Recursion and Probabilistic Choice in Guarded Type Theory

TL;DR

This paper develops a framework within guarded type theory to model and reason about programming languages featuring recursion and probabilistic choice, bridging the gap between logic and effectful programming.

Contribution

It introduces methods to define and analyze recursive and probabilistic constructs in guarded type theory using higher inductive types and guarded recursion.

Findings

Defined operational and denotational semantics for probabilistic recursive languages.

Established a relation for proving program adequacy and reasoning about contextual equivalence.

Demonstrated the applicability of guarded type theory to effectful programming languages.

Abstract

Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these applications to languages with recursion and computational effects such as probabilistic choice, because these features are not easily represented in constructive type theory. We show how to define and reason about a programming language with probabilistic choice and recursive types, in guarded type theory. We use higher inductive types to represent finite distributions and guarded recursion to model recursion. We define both operational and denotational semantics, as well as a relation between the two. The relation can be used to prove adequacy, but we also show how to use it to reason about programs up to contextual equivalence.