Internal Effectful Forcing in System T

TL;DR

This paper applies effectful forcing to demonstrate that the dialogue tree semantics of System T terms are definable within System T itself, using a novel dialogue-tree semantics and logical relations.

Contribution

It introduces an effectful forcing technique and a dialogue-tree semantics for System T, showing that these trees are definable within System T using Church encoding.

Findings

Dialogue trees are System T-definable.

Effectful forcing relates semantics to set-theoretical models.

Dialogue-tree semantics can be encoded within System T.

Abstract

The effectful forcing technique allows one to show that the denotation of a closed System T term of type $(\iota \to \iota) \to \iota$ in the set-theoretical model is a continuous function $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees.