Two Guarded Recursive Powerdomains for Applicative Simulation

TL;DR

This paper introduces two guarded recursive powerdomain constructions within Clocked Cubical Type Theory to model non-determinism and recursion, enabling new proofs of applicative similarity as congruences in lambda calculus.

Contribution

It develops two novel guarded recursive powerdomain models for combining non-determinism with recursion in a type-theoretic setting, using synthetic guarded domain theory.

Findings

Defined two guarded recursive powerdomains for non-determinism and recursion.

Proved applicative similarity as a congruence for lambda calculus with non-determinism.

Utilized a denotational approach instead of operational reasoning.

Abstract

Clocked Cubical Type Theory is a new type theory combining the power of guarded recursion with univalence and higher inductive types (HITs). This type theory can be used as a metalanguage for synthetic guarded domain theory in which one can solve guarded recursive type equations, also with negative variable occurrences, and use these to construct models for reasoning about programming languages. Combining this with HITs allows for the use of type constructors familiar from set-theory based approaches to semantics, such as quotients and finite powersets in these models. In this paper we show how to reason about the combination of finite non-determinism and recursion in this type theory. Unlike traditional domain theory which takes an ordering of programs as primitive, synthetic guarded domain theory takes the notion of computation step as primitive in the form of a modal operator. We use this extra intensional information to define two guarded recursive (finite) powerdomain constructions differing in the way non-determinism interacts with the computation steps. As an example application of these we show how to prove applicative similarity a congruence in the cases of may- and must-convergence for the untyped lambda calculus with finite non-determinism. Such results are usually proved using operational reasoning and Howe's method. Here we use an adaptation of a denotational method developed by Pitts in the context of domain theory.