Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modelling Recursion and Probabilistic Choice in Guarded Type Theory

Philipp Jan Andries Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal

TL;DR

This work defines both operational and denotational semantics of FPC⊕, a programming language with probabilistic choice and recursive types, in guarded type theory and shows how to define and reason about FPC⊕, a programming language with probabilistic choice and recursive types, in guarded type theory.

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.

Modelling Recursion and Probabilistic Choice in Guarded Type Theory

TL;DR

This work defines both operational and denotational semantics of FPC⊕, a programming language with probabilistic choice and recursive types, in guarded type theory and shows how to define and reason about FPC⊕, a programming language with probabilistic choice and recursive types, in guarded type theory.

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.
Paper Structure (25 sections, 50 theorems, 205 equations, 7 figures)

This paper contains 25 sections, 50 theorems, 205 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Clocked Cubical Type Theory
  4. Basic properties and HITs
  5. Guarded recursion
  6. Coinductive types
  7. Finite distributions
  8. Convex delay algebras
  9. Probability of termination
  10. Step reductions
  11. Approximate step reductions
  12. Probabilistic FPC
  13. Contextual Refinement
  14. Denotational semantics
  15. Couplings and Lifting relations
  16. ...and 10 more sections

Key Result

lemma 1

Suppose $i : A \to B$ is injective in the sense of the existence of a map $\Pi x,y: A. (i(x) = i(y)) \to x= y$, and suppose $B$ is clock irrelevant. Then also $A$ is clock-irrelevant.

Figures (7)

  • Figure 1: Selected typing rules for Clocked Cubical Type Theory.
  • Figure 2: Typing rules for $\mathsf{FPC}_{\oplus}$. Rules for $\mathsf{pred}\,{}, \mathsf{inr}{\,},\mathsf{snd}{\,}$ omitted.
  • Figure 3: The evaluation function $\mathsf{eval}^{\kappa}{}$. Rules for $\mathsf{pred}\,{}, \mathsf{inr}{\,},\mathsf{snd}{\,}$ omitted.
  • Figure 4: Denotational semantics for $\mathsf{FPC}_{\oplus}$. Rules for $\mathsf{pred}\,{}, \mathsf{inr}{\,},\mathsf{snd}{\,}$ omitted.
  • Figure 5: Reasoning principles for ${}\, {}\overline{{}\,\mathcal{R}\,{}}^\kappa\, {}$
  • ...and 2 more figures

Theorems & Definitions (121)

  • lemma 1
  • definition 1: Convex Algebra
  • definition 2
  • proposition 1
  • lemma 2
  • theorem 1
  • definition 3: Convex Delay Algebra
  • proposition 2
  • proof
  • proposition 3
  • ...and 111 more