% Continuity of Gödel's system T definable functionals % via effectful forcing % % Martin Escardo % % 24-31 July 2012, updated 3 August 2012, 21 and 28 Feb 2013 and 6 Mar 2013. % % This file proof-checks in Agda version 2.3.2. % % (NB. With earlier versions of Agda this file has unsolved metas % arising from the definition B = D ℕ ℕ.) % % This is a literate Agda file that generates latex, pdf and html. % Search for "code" to find the agda code. % % This is best viewed as http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf % in the form of an article. % % The source file is http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.lagda % You are probably browsing http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.html \documentclass{entcs} \usepackage{prentcsmacro} \usepackage{graphicx} \sloppy % The following is enclosed to allow easy detection of differences in % ascii coding. % Upper-case A B C D E F G H I J K L M N O P Q R S T U V W X Y Z % Lower-case a b c d e f g h i j k l m n o p q r s t u v w x y z % Digits 0 1 2 3 4 5 6 7 8 9 % Exclamation ! Double quote " Hash (number) # % Dollar $ Percent % Ampersand & % Acute accent ' Left paren ( Right paren ) % Asterisk * Plus + Comma , % Minus - Point . Solidus / % Colon : Semicolon ; Less than < % Equals = Greater than > Question mark ? % At @ Left bracket [ Backslash \ % Right bracket ] Circumflex ^ Underscore _ % Grave accent ` Left brace { Vertical bar | % Right brace } Tilde ~ % ---------------------------------------------------------------------- % Some useful commands when doing highlightning of Agda code in LaTeX. % ---------------------------------------------------------------------- % % This is actually agda.sty provided by the agda distribution, % suitably modified an extended for our purposes, and included here to % avoid hassle for the editors of the MFPS proceedings. \newcommand{\AgdaC}[1]{\mbox{#1}} \usepackage{ifxetex, xcolor, polytable} % XeLaTeX \ifxetex \usepackage{polyglossia} \usepackage{fontspec} \usepackage[]{unicode-math} % pdfLaTeX \else \usepackage{bbm, ucs, amsfonts, amssymb, stmaryrd} % mhe \usepackage[safe]{tipa} % See page 12 of the tipa manual for what % safe does. % FIX: This doesn't seem to help solve the pipe problem? % http://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex \usepackage[T1]{fontenc} \usepackage[utf8x]{inputenc} % FIX: Complete the list and send it upstream to the ucs package devs. \DeclareUnicodeCharacter{951}{$\eta$} % mhe \DeclareUnicodeCharacter{937}{$\Omega$} % mhe \DeclareUnicodeCharacter{931}{$\Sigma$} % mhe \DeclareUnicodeCharacter{928}{$\Pi$} % mhe \DeclareUnicodeCharacter{945}{$\alpha$} % mhe \DeclareUnicodeCharacter{960}{$\pi$} % mhe \DeclareUnicodeCharacter{963}{$\sigma$} % mhe \DeclareUnicodeCharacter{964}{$\tau$} % mhe \DeclareUnicodeCharacter{961}{$\rho$} % mhe \DeclareUnicodeCharacter{10214}{$\llbracket$} % mhe (stmaryrd) \DeclareUnicodeCharacter{10215}{$\rrbracket$} % mhe (stmaryrd) \DeclareUnicodeCharacter{9657}{$\triangleright$} \DeclareUnicodeCharacter{8759}{::} \DeclareUnicodeCharacter{8263}{$?\!?$} \DeclareUnicodeCharacter{737} {$^l$} % FIX: Ugly, apparently ^r is % defined, I can't find the % definition though. \DeclareUnicodeCharacter{8718}{$\blacksquare$} \DeclareUnicodeCharacter{8255}{$\_$} % FIX: Couldn't find \undertie. \DeclareUnicodeCharacter{9667}{$\triangleleft$} \DeclareUnicodeCharacter{10218}{$\langle\!\langle$} \DeclareUnicodeCharacter{10219}{$\rangle\!\rangle$} \fi % ---------------------------------------------------------------------- % Font styles. % Default font style. \newcommand{\AgdaFontStyle}[1]{\textsf{#1}} % String font style. \newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}} % Comment font style. \newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}} % Bounded variables font style. \newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}} % ---------------------------------------------------------------------- % Colours. % Aspect colours. \definecolor{AgdaComment} {HTML}{B22222} \definecolor{AgdaKeyword} {HTML}{CD6600} \definecolor{AgdaString} {HTML}{B22222} \definecolor{AgdaNumber} {HTML}{A020F0} \definecolor{AgdaSymbol} {HTML}{181818} % was {404040} % mhe \definecolor{AgdaPrimitiveType}{HTML}{0000CD} \definecolor{AgdaOperator} {HTML}{000000} % NameKind colours. \definecolor{AgdaBound} {HTML}{000000} \definecolor{AgdaInductiveConstructor} {HTML}{008B00} \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500} \definecolor{AgdaDatatype} {HTML}{0000CD} \definecolor{AgdaField} {HTML}{EE1289} \definecolor{AgdaFunction} {HTML}{0000CD} \definecolor{AgdaModule} {HTML}{A020F0} \definecolor{AgdaPostulate} {HTML}{0000CD} \definecolor{AgdaPrimitive} {HTML}{0000CD} \definecolor{AgdaRecord} {HTML}{0000CD} % Other aspect colours. \definecolor{AgdaDottedPattern} {HTML}{000000} \definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00} \definecolor{AgdaTerminationProblem}{HTML}{FFA07A} \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3} \definecolor{AgdaError} {HTML}{FF0000} % Misc. \definecolor{AgdaHole} {HTML}{9DFF9D} % ---------------------------------------------------------------------- % Commands. % Aspect commands. \newcommand{\AgdaComment} [1] {\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}} \newcommand{\AgdaKeyword} [1] {\AgdaFontStyle{\textcolor{AgdaKeyword}{#1}}} \newcommand{\AgdaString} [1]{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}} \newcommand{\AgdaNumber} [1]{\textcolor{AgdaNumber}{#1}} \newcommand{\AgdaSymbol} [1]{\textcolor{AgdaSymbol}{#1}} \newcommand{\AgdaPrimitiveType}[1] {\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}} \newcommand{\AgdaOperator} [1]{\textcolor{AgdaOperator}{#1}} % NameKind commands. \newcommand{\AgdaBound} [1]{\AgdaBoundFontStyle{\textcolor{AgdaBound}{#1}}} \newcommand{\AgdaInductiveConstructor}[1] {\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{#1}}} \newcommand{\AgdaCoinductiveConstructor}[1] {\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{#1}}} \newcommand{\AgdaDatatype} [1]{\AgdaFontStyle{\textcolor{AgdaDatatype}{#1}}} \newcommand{\AgdaField} [1]{\AgdaFontStyle{\textcolor{AgdaField}{#1}}} \newcommand{\AgdaFunction} [1]{\AgdaFontStyle{\textcolor{AgdaFunction}{#1}}} \newcommand{\AgdaModule} [1]{\AgdaFontStyle{\textcolor{AgdaModule}{#1}}} \newcommand{\AgdaPostulate}[1]{\AgdaFontStyle{\textcolor{AgdaPostulate}{#1}}} \newcommand{\AgdaPrimitive}[1]{\AgdaFontStyle{\textcolor{AgdaPrimitive}{#1}}} \newcommand{\AgdaRecord} [1]{\AgdaFontStyle{\textcolor{AgdaRecord}{#1}}} % Other aspect commands. \newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}} \newcommand{\AgdaUnsolvedMeta} [1] {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}} \newcommand{\AgdaTerminationProblem}[1] {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}} \newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}} \newcommand{\AgdaError} [1] {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}} % Misc. \newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}} \long\def\AgdaHide#1{} % Used to hide code from LaTeX. \newcommand{\AgdaIndent}[1]{\quad} % ---------------------------------------------------------------------- % The code environment. % \newcommand{\AgdaCodeStyle}{} \newcommand{\AgdaCodeStyle}{\small} \ifdefined\mathindent {} \else \newdimen\mathindent\mathindent\leftmargini \fi \newenvironment{code}% modified by mhe {\noindent\AgdaCodeStyle\pboxed}% {\endpboxed\par\noindent% \ignorespacesafterend} % Default column for polytable. \defaultcolumn{l} % End of Agda.sty. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \usepackage{amsmath} \usepackage{url} \usepackage[english]{babel} \usepackage{diagrams} \def\lastname{Escardo} % should be Escard\'o but this generates "Escard" in the pdf (entcs style's fault). \begin{document} \begin{frontmatter} \title{Continuity of G\"odel's system T definable functionals via effectful forcing} \author{Mart\'\i{n} Escard\'o\thanksref{myemail}} \address{School of Computer Science\\ University of Birmingham \\ Birmingham, England} \thanks[myemail]{Email: \href{mailto:m.escardo@cs.bham.ac.uk} {\texttt{\normalshape m.escardo@cs.bham.ac.uk}}} \begin{abstract} It is well-known that the Gödel's system T definable functions \AgdaC{(ℕ → ℕ) → ℕ} are continuous, and that their restrictions from the Baire type \AgdaC{(ℕ → ℕ)} to the Cantor type \AgdaC{(ℕ → 2)} are uniformly continuous. We offer a new, relatively short and self-contained proof. The main technical idea is a concrete notion of generic element that doesn't rely on forcing, Kripke semantics or sheaves, which seems to be related to generic effects in programming. The proof uses standard techniques from programming language semantics, such as dialogues, monads, and logical relations. We write this proof in intensional Martin-Löf type theory (MLTT) from scratch, in Agda notation. Because MLTT has a computational interpretation and Agda can be seen as a programming language, we can run our proof to compute moduli of (uniform) continuity of T-definable functions. \end{abstract} \begin{keyword} Gödel's system T, continuity, uniform continuity, Baire space, Cantor space, intensional Martin-Löf theory, Agda, dialogue, semantics, logical relation. \end{keyword} \end{frontmatter} \section{Introduction} \label{formulation} This is a relatively short, and self-contained, proof of the well-known fact that any function \AgdaC{$f$ : (ℕ → ℕ) → ℕ} that is definable in Gödel's system T is continuous, and that its restriction from the Baire type \AgdaC{(ℕ → ℕ)} to the Cantor type \AgdaC{(ℕ → 2)} is uniformly continuous~\cite{MR0325352,beeson}. We believe the proof is new, although it is related to previous work discussed below. The main technical idea is a concrete notion of generic element that doesn't rely on forcing, Kripke semantics or sheaves, which seems to be related to generic effects in programming~\cite{Plotkin03algebraicoperations}. Several well-known ideas from logic, computation, constructive mathematics and programming-language semantics naturally appear here, in a relatively simple, self-contained, and hopefully appealing, development. The idea is to represent a function \AgdaC{$f$ : (ℕ → ℕ) → ℕ} by a well-founded dialogue tree, and extract continuity information about $f$ from this tree. To calculate such a tree from a system T term \AgdaC{$t$: (ι ⇒ ι) ⇒ ι} denoting $f$, we work with an auxiliary interpretation of system T, which gives a function \AgdaC{$\tilde{f}$ : $(\tilde{\mathbb{N}}$ → $\tilde{\mathbb{N}})$ → $\tilde{\mathbb{N}}$}, where $\tilde{\mathbb{N}}$ is the set of dialogue trees. Applying $\tilde{f}$ to a certain \emph{generic sequence} $\tilde{\mathbb{N}}$ → $\tilde{\mathbb{N}}$, the desired dialogue tree is obtained. We now explain this idea in more detail. In the set-theoretical model of system T, the ground type ι is interpreted as the set ℕ of natural numbers, and if the types σ and τ are interpreted as sets~$X$ and $Y$, then the type σ ⇒ τ is interpreted as the set of all functions \AgdaC{$X$ → $Y$}. We consider an auxiliary model that replaces the interpretation of the ground type by the set $\tilde{\mathbb{N}}$, but keeps the interpretation of ⇒ as the formation of the set of all functions. In this model, the zero constant is interpreted by a suitable element $\tilde{0}$ of $\tilde{\mathbb{N}}$, the successor constant is interpreted by a function $\tilde{\mathbb{N}}$ → $\tilde{\mathbb{N}}$, and each iteration combinator is interpreted by a function ($X$ → $X$) → $X$ → $\tilde{\mathbb{N}}$ → $X$. An element of the set $\tilde{\mathbb{N}}$ is a well-founded dialogue tree that describes the computation of a natural number relative to an unspecified oracle \AgdaC{α : ℕ → ℕ}. An internal node is labeled by a natural number representing a query to the oracle, and has countably many branches corresponding to the possible answers. Each leaf is labeled by a natural number and represents a possible outcome of the computation. These dialogues represent computations in the sense of Kleene~\cite{KleeneSC:rfqftI}. If a particular oracle \AgdaC{α : ℕ → ℕ} is given, we get a natural number from any \AgdaC{$d \in \tilde{\mathbb{N}}$} via a decodification function \begin{quote} decode : (ℕ → ℕ) → $\tilde{\mathbb{N}}$ → ℕ. \end{quote} It turns out that there is a function \begin{quote} generic : $\tilde{\mathbb{N}}$ → $\tilde{\mathbb{N}}$ \end{quote} that can be regarded as a \emph{generic sequence} in the sense that, for any particular sequence \AgdaC{α : ℕ → ℕ}, \begin{small} \begin{diagram}[small] \tilde{\mathbb{N}} & \rTo^{\text{generic}} & \tilde{\mathbb{N}} \\ \dTo^{\text{decode α}} & & \dTo_{\text{decode α}} \\ \text{ℕ} & \rTo_{\text{α}} & \text{ℕ}. \end{diagram} \end{small} \noindent That is, the generic sequence codes any concrete sequence \AgdaC{α}, provided the sequence α itself is used as the concrete oracle for decodification. The idea is that the application of the function \AgdaC{generic} to a dialogue tree adds a new layer of choices at its leaves. Next we show that for any given term \AgdaC{$t$ : (ι ⇒ ι) ⇒ ι} denoting a function \AgdaC{$f$ : (ℕ → ℕ) → ℕ} in the standard interpretation and \AgdaC{$\tilde{f}$ : $(\tilde{\mathbb{N}}$ → $\tilde{\mathbb{N}})$ → $\tilde{\mathbb{N}}$} in the dialogue interpretation, we have that \begin{quote} \AgdaC{$f$ α = decode α ($\tilde{f}$ generic).} \end{quote} This is proved by establishing a logical relation between the set-theoretic and dialogue models. Thus we can compute a dialogue tree of $f$ by applying $\tilde{f}$ to the generic sequence. The set $\tilde{\mathbb{N}}$ is constructed as \AgdaC{B ℕ} for a suitable dialogue monad B. Then the interpretation of the constant zero is η 0 where η is the unit of the monad, the interpretation of the successor constant is given by functoriality as \AgdaC{B succ}, and the interpretation of the primitive recursion constant is given by the Kleisli extension of its standard interpretation. The object part \AgdaC{B $X$} of the monad is inductively defined by the constructors \begin{quote} η : $X$ → B $X$, \\ β : (ℕ → B $X$) → ℕ → B $X$, \end{quote} where η constructs leaves and β constructs a tree β φ $n$ given countably many trees φ and a label~$n$. With $X$ = ℕ, we have β η : ℕ → B ℕ, and the generic sequence is the Kleisli extension of β η. Thus, the generic sequence seems to be a sort of \emph{generic effect} in the sense of~\cite{Plotkin03algebraicoperations}. Notice that our interpretation is a call-by-name version of Moggi's semantics. Using this, it follows that if a function \AgdaC{$f$ : (ℕ → ℕ) → ℕ} is the set-theoretical interpretation of some system T term \AgdaC{$t$ : (ι ⇒ ι) ⇒ ι}, then it is continuous and its restriction to \AgdaC{ℕ → 2} is uniformly continuous, where $2$ is the set with elements $0$ and $1$. The reason is that a dialogue produces an answer after finitely many queries, because it is well-founded, and that a dialogue tree for a function \AgdaC{$(ℕ → 2) → ℕ$} is finite, because it is finitely branching. Recall that continuity means that, for any sequence of integers \AgdaC{α : ℕ → ℕ}, there is \AgdaC{$m$ : ℕ}, called a modulus of continuity of $f$ at the point~α, such that any sequence \AgdaC{α$'$} that agrees with α at the first $m$ positions gives the same result, that is, \AgdaC{$f$ α = $f$ α$'$}. Uniform continuity means that there is \AgdaC{$m$ : ℕ}, called a modulus of uniform continuity of $f$ on \AgdaC{ℕ → 2}, such that any two binary sequences α and α$'$ that agree at the first $m$ positions give the same result. Our arguments are constructive, and we write the full proof from scratch in intensional Martin-Löf type theory (MLTT), in Agda notation~\cite{bove:dybjer}, without the use of libraries. We don't assume previous familiarity with Agda, but we do require rudimentary knowledge of MLTT. The Agda source file for this program/proof~\cite{escardo:dialogue} is written in Knuth's \emph{literate} style, which automatically generates the \LaTeX\ file that produces this article. Agda both checks proofs and can run them. Notice that MLTT or Agda cannot prove or disprove that all functions \AgdaC{(ℕ → ℕ) → ℕ} are continuous, as they are compatible with both classical and constructive mathematics, like Bishop mathematics~\cite{bishop:foundations}. The theorem here is that certain functions \AgdaC{(ℕ → ℕ) → ℕ} are continuous: those that can be defined in system~T. \noindent{\itshape\bfseries Related work.} The idea of computing continuity information by applying a function to effectful arguments goes back to Longley~\cite{Longley99whenis}, who passes exceptions to the function. A similar approach is described in an example given by Bauer and Pretnar~\cite{bauer:pretnar}. The idea of working with computation trees is of course very old, going back to Brouwer~\cite{beeson} in intuitionistic mathematics, and to Kleene~\cite{KleeneSC:rfqftI} in computability theory in the form of dialogues, where the input is referred to as an oracle. Howard~\cite{Howard(80)} derives computation trees for system T, by operational methods, by successively reducing a term so that each time an oracle given by a free variable of type ι ⇒ ι is queried, countably many branches of the computation are created, corresponding to the possible answers given by the oracle. Hancock and Setzer use variations of dialogue trees to describe interactive computation in type theory~\cite{DBLP:conf/csl/HancockS00} (see also~\cite{Hancock_representationsof}). Our work is directly inspired by Coquand and Jaber's work on forcing in type theory~\cite{Coquand:2010:NFT:1839560.1839564,DBLP:series/leus/CoquandJ12}. Like Howard, they derive computation trees by operational methods. They extend dependent type theory with a constant for a generic element, and then decorate judgements with subscripts that keep track of approximation information about the generic element as the computations proceed (similarly to \cite{MR0325352}). In this way they extract continuity information. They prove the termination and soundness of this modification of type theory using Tait's computability method, which here is manifested as a logical relation between our two models. They also provide a Haskell implementation for the system~T case as an appendix, which uses a monad that is the composition of the list monad (for nondeterminism) and of the state monad. Their Haskell program implements a normalization procedure with bookkeeping information, tracked by the monad, that produces computation trees. Because they only account for uniform continuity in their Haskell implementation, such trees are finite. They describe their work as a computational interpretation of forcing and continuity as presented in Beeson~\cite{beeson}. The difference is that their approach is syntactical whereas ours is semantical, and the reader may sense an analogy with normalization by evaluation. Notice that these arguments only show that the \emph{definable} functions are continuous. To get a constructive model in which \emph{all} functions are continuous, they work with iterated forcing, which is related to our recent work~\cite{escardo:xu}, but this is another story. \noindent {\itshape\bfseries Organization.} (\ref{section:formal})~Formal proof in Agda. (\ref{section:informal})~Informal, rigorous proof. \noindent {\itshape\bfseries Acknowledgements.} I benefitted from remarks on a previous version of this paper by Thierry Coquand, Dan Ghica, Achim Jung, Chuangjie~Xu, and the anonymous referees. \section{Proof in Martin-L\"of type theory in Agda notation} \label{section:formal} \subsection{Agda preliminaries} \label{section:preliminaries} The purpose of this subsection is two-fold: (1) To develop a tiny Agda library for use in the following sections, and (2) to briefly explain Agda notation~\cite{bove:dybjer} for MLTT. We assume rudimentary knowledge of (intensional) Martin-L\"of type theory and the BHK interpretation of the quantifiers as products Π and sums~Σ. We don't use any feature of Agda that goes beyond standard MLTT. If we were trying to be purist, we would use W-types rather than some of our inductive definitions using the Agda keyword \emph{data}. Notice that the coloured text in the electronic version of this paper is the Agda code. The universe of all types is denoted by Set, and types are called sets (this is a universe \`a la Russell). Products \AgdaC{Π} are denoted by \AgdaC{∀} in Agda. % Any Agda file, has to be a named module: \AgdaHide{ % I don't think I am hiding anything else. \begin{code} module dialogue where \end{code} } Consider the definition of the (interpretation of) the standard combinators: \begin{code} Ķ : ∀{X Y : Set} → X → Y → X Ķ x y = x Ş : ∀{X Y Z : Set} → (X → Y → Z) → (X → Y) → X → Z Ş f g x = f x (g x) \end{code} The curly braces around the set variables indicate that these are implicit parameters, to be inferred by Agda whenever \AgdaC{Ķ} and \AgdaC{Ş} are used. If Agda fails to uniquely infer the missing arguments, one has to write e.g.\ \AgdaC{$Ķ$ \{$X$\} \{$Y$\} $x$ $y$} rather than the abbreviated form \AgdaC{$Ķ$ $x$ $y$}. The following should be self-explanatory: \begin{code} _∘_ : ∀{X Y Z : Set} → (Y → Z) → (X → Y) → (X → Z) g ∘ f = λ x → g(f x) data ℕ : Set where zero : ℕ succ : ℕ → ℕ rec : ∀{X : Set} → (X → X) → X → ℕ → X rec f x zero = x rec f x (succ n) = f(rec f x n) \end{code} Agda has a termination checker that verifies that recursions are well-founded, and hence all functions are total. We also need types of binary digits, finite lists, and finite binary trees: \begin{code} data ℕ₂ : Set where ₀ ₁ : ℕ₂ data List (X : Set) : Set where [] : List X _∷_ : X → List X → List X data Tree (X : Set) : Set where empty : Tree X branch : X → (ℕ₂ → Tree X) → Tree X \end{code} Sums are not built-in and hence need to be defined: \begin{code} data Σ {X : Set} (Y : X → Set) : Set where _,_ : ∀(x : X)(y : Y x) → Σ {X} Y \end{code} The definition says that an element of \AgdaC{Σ \{$X$\} $Y$} is a pair \AgdaC{($x$,$y$)} with \AgdaC{$x$ : $X$} and \AgdaC{$y$ : $Y$ $x$}. Notice that comma is not a reserved symbol: we define it as a binary operator to construct dependent pairs. Because \AgdaC{$Y$ = λ($x$ : $X$) → $Y$ $x$} if one assumes the η-law, and because the first argument is implicit, we can write \AgdaC{Σ $\{X\}$ $Y$} as \AgdaC{Σ Y} or \AgdaC{Σ \char`\\($x$ : $X$) → $Y$ $x$}, where backslash is the same thing as lambda. We will use backslash exclusively for sums. % (And hope it will be as invisible as possible.) \begin{code} π₀ : ∀{X : Set} {Y : X → Set} → (Σ \(x : X) → Y x) → X π₀(x , y) = x π₁ : ∀{X : Set} {Y : X → Set} → ∀(t : Σ \(x : X) → Y x) → Y(π₀ t) π₁(x , y) = y \end{code} The identity type \AgdaC{Id $X$ $x$ $y$} is written \AgdaC{$x$ ≡ $y$} with \AgdaC{$X$} implicit, and is inductively defined as ``the least reflexive relation'': \begin{code} data _≡_ {X : Set} : X → X → Set where refl : ∀{x : X} → x ≡ x sym : ∀{X : Set} → ∀{x y : X} → x ≡ y → y ≡ x sym refl = refl trans : ∀{X : Set} → ∀{x y z : X} → x ≡ y → y ≡ z → x ≡ z trans refl refl = refl cong : ∀{X Y : Set} → ∀(f : X → Y) → ∀{x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁ cong f refl = refl cong₂ : ∀{X Y Z : Set} → ∀(f : X → Y → Z) → ∀{x₀ x₁ : X}{y₀ y₁ : Y} → x₀ ≡ x₁ → y₀ ≡ y₁ → f x₀ y₀ ≡ f x₁ y₁ cong₂ f refl refl = refl \end{code} \subsection{Dialogues and continuity} \label{section:dialogues:continuity} We consider the computation of functionals \AgdaC{($X$ → $Y$) → $Z$} with dialogue trees. We work with the following inductively defined type of (well founded) dialogue trees indexed by three types $X$, $Y$ and $Z$. These are $Y$-branching trees with $X$-labeled internal nodes and $Z$-labeled leaves: \begin{code} data D (X Y Z : Set) : Set where η : Z → D X Y Z β : (Y → D X Y Z) → X → D X Y Z \end{code} A leaf is written \AgdaC{η $z$}, and it gives the final answer $z$ (η will be the unit of a monad). A forest is a $Y$-indexed family φ of trees. Given such a forest \AgdaC{φ} and \AgdaC{$x$ : $X$}, we can build a new tree \AgdaC{β φ $x$} whose root is labeled by $x$, which has a subtree \AgdaC{φ $y$} for each \AgdaC{$y$ : $Y$}. We can imagine \AgdaC{$x$ : $X$} as query, for which an oracle α gives some intermediate answer \AgdaC{$y$ = α $x$ : Y}. After this answer~\AgdaC{$y$}, we move to the subtree \AgdaC{φ $y$}, and the dialogue proceeds in this way, until a leaf with the final answer is reached: \begin{code} dialogue : ∀{X Y Z : Set} → D X Y Z → (X → Y) → Z dialogue (η z) α = z dialogue (β φ x) α = dialogue (φ(α x)) α \end{code} We say that a function \AgdaC{($X$ → $Y$) → $Z$} is \emph{eloquent} if it is computed by some dialogue: \begin{code} eloquent : ∀{X Y Z : Set} → ((X → Y) → Z) → Set eloquent f = Σ \d → ∀ α → dialogue d α ≡ f α \end{code} Here we are interested in the case \AgdaC{$X$=$Y$=$Z$=ℕ}. Think of functions \AgdaC{α : ℕ → ℕ} as sequences of natural numbers. The set of such sequences is called the Baire space: \begin{code} Baire : Set Baire = ℕ → ℕ \end{code} Functions \AgdaC{Baire → ℕ} are coded by a particular kind of dialogue trees, namely \AgdaC{B ℕ} where B is defined as follows: \begin{code} B : Set → Set B = D ℕ ℕ \end{code} We work with a refined version of continuity, which gives more information than the traditional notion introduced in Section~\ref{formulation}, where the modulus of continuity is a finite list of indices rather than an upper bound for the indices. The agreement relation determined by a list of indices is inductively defined as follows, where \AgdaC{\AgdaC{α ≡[ $s$ ] α$'$}} says that the sequences \AgdaC{α} and \AgdaC{α$'$} agree at the indices collected in the list \AgdaC{$s$}: \begin{enumerate} \item \AgdaC{α ≡[ [] ] α$'$}, \item \AgdaC{α $i$ ≡ α$'$ $i$ → α ≡[ $s$ ] α$'$ → α ≡[ $i$ ∷ $s$ ] α$'$}. \end{enumerate} We write this inductive definition as follows in Agda, where we give the name~[] to the proof of the first clause and the name ∷ to the proof of the second clause, that is, using the same constructor names as for the inductively defined type of lists: \begin{code} data _≡[_]_ {X : Set} : (ℕ → X) → List ℕ → (ℕ → X) → Set where [] : ∀{α α' : ℕ → X} → α ≡[ [] ] α' _∷_ : ∀{α α' : ℕ → X}{i : ℕ}{s : List ℕ} → α i ≡ α' i → α ≡[ s ] α' → α ≡[ i ∷ s ] α' continuous : (Baire → ℕ) → Set continuous f = ∀(α : Baire) → Σ \(s : List ℕ) → ∀(α' : Baire) → α ≡[ s ] α' → f α ≡ f α' \end{code} It is an easy exercise, left to the reader, to produce an Agda proof that this refined notion of continuity implies the traditional notion of continuity, by taking the maximum value of the list~$s$. Functions defined by dialogues are continuous, because a dialogue produces an answer after finitely many queries: \begin{code} dialogue-continuity : ∀(d : B ℕ) → continuous(dialogue d) dialogue-continuity (η n) α = ([] , lemma) where lemma : ∀ α' → α ≡[ [] ] α' → n ≡ n lemma α' r = refl dialogue-continuity (β φ i) α = ((i ∷ s) , lemma) where IH : ∀(i : ℕ) → continuous(dialogue(φ(α i))) IH i = dialogue-continuity (φ(α i)) s : List ℕ s = π₀(IH i α) claim₀ : ∀(α' : Baire) → α ≡[ s ] α' → dialogue(φ(α i)) α ≡ dialogue(φ(α i)) α' claim₀ = π₁(IH i α) claim₁ : ∀(α' : Baire) → α i ≡ α' i → dialogue (φ (α i)) α' ≡ dialogue (φ (α' i)) α' claim₁ α' r = cong (λ n → dialogue (φ n) α') r lemma : ∀(α' : Baire) → α ≡[ i ∷ s ] α' → dialogue (φ(α i)) α ≡ dialogue(φ (α' i)) α' lemma α' (r ∷ rs) = trans (claim₀ α' rs) (claim₁ α' r) \end{code} \noindent This formal proof is informally explained as follows. We show that \begin{quote} ∀($d$ : B ℕ) → continuous(dialogue $d$) \end{quote} by induction on $d$. Expanding the definition, this amounts to, using Agda notation, \begin{quote} ∀ $d$ → ∀ α → Σ \char`\\$s$ → ∀ α$'$ → α ≡[ $s$ ] α$'$ → dialogue $d$ α ≡ dialogue $d$ α$'$. \end{quote} For the base case $d$ = η $n$, the definition of the function dialogue gives \AgdaC{dialogue $d$ α = $n$}, and so we must show that, for any α, \begin{quote} Σ \char`\\$s$ → ∀ α$'$ → α ≡[ $s$ ] α$'$ → $n$ ≡ $n$. \end{quote} We can take $s = []$ and then we are done, because $n$ ≡ $n$ by reflexivity. This is what the first equation of the formal proof says. Thus notice that Agda, in accordance with MLTT, silently expands definitions by reduction to normal form. For the induction step $d$ = β φ $i$, expanding the definition of the dialogue function, what we need to prove is that, for an arbitrary α, \begin{quote} Σ \char`\\$s'$ → ∀ α$'$ → α ≡[ $s'$ ] α$'$ → dialogue (φ(α $i$)) α ≡ dialogue (φ α$'$ $i$) α$'$. \end{quote} The induction hypothesis is \AgdaC{∀($i$ : ℕ) → continuous(dialogue(φ(α $i$)))}, which gives, for any $i$ and our arbitrary α, \begin{quote} Σ \char`\\$s$ → ∀ α$'$ → α ≡[ $s$ ] α$'$ → dialogue(φ(α $i$)) α = dialogue(φ(α $i$)) α$'$. \end{quote} Using the two projections π₀ and π₁ we get $s$ and a proof that \begin{quote} ∀ α$'$ → α ≡[ $s$ ] α$'$ → dialogue(φ(α $i$)) α = dialogue(φ(α $i$)) α$'$. \end{quote} Hence we can take $s'$ = $i$ ∷ $s$, and the desired conclusion holds substituting equals for equals (with cong) using transitivity and the definition α $i$ ≡ α$'$ $i$ → α ≡[ $s$ ] α$'$ → α ≡[ $i$ ∷ $s$ ] α$'$. This amounts to the second equation of the proof, where in the pattern of the proof of the lemma we have $r$ : α $i$ ≡ α$'$ $i$ and $rs$ : α ≡[ $s$ ] α$'$. ~ We need the following technical lemma because it is not provable in intensional MLTT that any two functions are equal if they are pointwise equal. The proof is admitedly written in a rather laconic form. The point is that the notion of continuity depends only on the values of the function, and the hypothesis says that the two functions have the same values. Notice that the axiom of function extensionality (any two pointwise equal functions are equal) is not false but rather not provable or disprovable, and is consistent~\cite{HoTTbook}. \begin{code} continuity-extensional : ∀(f g : Baire → ℕ) → (∀ α → f α ≡ g α) → continuous f → continuous g continuity-extensional f g t c α = (π₀(c α) , (λ α' r → trans (sym (t α)) (trans (π₁(c α) α' r) (t α')))) eloquent-is-continuous : ∀(f : Baire → ℕ) → eloquent f → continuous f eloquent-is-continuous f (d , e) = continuity-extensional (dialogue d) f e (dialogue-continuity d) \end{code} The development for uniform continuity is similar to the above, with the crucial difference that a dialogue tree in C ℕ is finite: \begin{code} Cantor : Set Cantor = ℕ → ℕ₂ C : Set → Set C = D ℕ ℕ₂ \end{code} We work with a refined version of uniform continuity (cf.\ Section~\ref{formulation}), where the modulus is a finite binary tree \AgdaC{$s$} of indices rather than an upper bound of the indices. We could have worked with a list of indices, but the proofs are shorter and more direct using trees. The agreement relation defined by a tree of indices is inductively defined as follows, where α ≡[[ $s$ ]] α$'$ says that α and~α$'$ agree at the positions collected in the tree~$s$: \begin{code} data _≡[[_]]_ {X : Set} : (ℕ → X) → Tree ℕ → (ℕ → X) → Set where empty : ∀{α α' : ℕ → X} → α ≡[[ empty ]] α' branch : ∀{α α' : ℕ → X}{i : ℕ}{s : ℕ₂ → Tree ℕ} → α i ≡ α' i → (∀(j : ℕ₂) → α ≡[[ s j ]] α') → α ≡[[ branch i s ]] α' \end{code} Again we are using the same constructor names as for the type of trees. \begin{code} uniformly-continuous : (Cantor → ℕ) → Set uniformly-continuous f = Σ \(s : Tree ℕ) → ∀(α α' : Cantor) → α ≡[[ s ]] α' → f α ≡ f α' dialogue-UC : ∀(d : C ℕ) → uniformly-continuous(dialogue d) dialogue-UC (η n) = (empty , λ α α' n → refl) dialogue-UC (β φ i) = (branch i s , lemma) where IH : ∀(j : ℕ₂) → uniformly-continuous(dialogue(φ j)) IH j = dialogue-UC (φ j) s : ℕ₂ → Tree ℕ s j = π₀(IH j) claim : ∀ j α α' → α ≡[[ s j ]] α' → dialogue (φ j) α ≡ dialogue (φ j) α' claim j = π₁(IH j) lemma : ∀ α α' → α ≡[[ branch i s ]] α' → dialogue (φ (α i)) α ≡ dialogue (φ (α' i)) α' lemma α α' (branch r l) = trans fact₀ fact₁ where fact₀ : dialogue (φ (α i)) α ≡ dialogue (φ (α' i)) α fact₀ = cong (λ j → dialogue(φ j) α) r fact₁ : dialogue (φ (α' i)) α ≡ dialogue (φ (α' i)) α' fact₁ = claim (α' i) α α' (l(α' i)) UC-extensional : ∀(f g : Cantor → ℕ) → (∀(α : Cantor) → f α ≡ g α) → uniformly-continuous f → uniformly-continuous g UC-extensional f g t (u , c) = (u , (λ α α' r → trans (sym (t α)) (trans (c α α' r) (t α')))) eloquent-is-UC : ∀(f : Cantor → ℕ) → eloquent f → uniformly-continuous f eloquent-is-UC f (d , e) = UC-extensional (dialogue d) f e (dialogue-UC d) \end{code} We finish this section by showing that the restriction of an eloquent function \AgdaC{$f$ : Baire → ℕ} to the Cantor type is also eloquent. We first define a pruning function from \AgdaC{B ℕ} to \AgdaC{C ℕ} that implements restriction: \begin{code} embed-ℕ₂-ℕ : ℕ₂ → ℕ embed-ℕ₂-ℕ ₀ = zero embed-ℕ₂-ℕ ₁ = succ zero embed-C-B : Cantor → Baire embed-C-B α = embed-ℕ₂-ℕ ∘ α C-restriction : (Baire → ℕ) → (Cantor → ℕ) C-restriction f = f ∘ embed-C-B prune : B ℕ → C ℕ prune (η n) = η n prune (β φ i) = β (λ j → prune(φ(embed-ℕ₂-ℕ j))) i prune-behaviour : ∀(d : B ℕ)(α : Cantor) → dialogue (prune d) α ≡ C-restriction(dialogue d) α prune-behaviour (η n) α = refl prune-behaviour (β φ n) α = prune-behaviour (φ(embed-ℕ₂-ℕ(α n))) α eloquent-restriction : ∀(f : Baire → ℕ) → eloquent f → eloquent(C-restriction f) eloquent-restriction f (d , c) = (prune d , λ α → trans (prune-behaviour d α) (c (embed-C-B α))) \end{code} \subsection{Gödel's system T extended with an oracle} \label{section:oracle} For simplicity, we work with system \AgdaC{T} in its original combinatory form. This is no loss of generality, because both the combinatory and the lambda-calculus forms define the same elements of the set-theoretical model, and here we are interested in the continuity of the definable functionals. The system T type expressions and terms are inductively defined as follows: \begin{code} data type : Set where ι : type _⇒_ : type → type → type data T : (σ : type) → Set where Zero : T ι Succ : T(ι ⇒ ι) Rec : ∀{σ : type} → T((σ ⇒ σ) ⇒ σ ⇒ ι ⇒ σ) K : ∀{σ τ : type} → T(σ ⇒ τ ⇒ σ) S : ∀{ρ σ τ : type} → T((ρ ⇒ σ ⇒ τ) ⇒ (ρ ⇒ σ) ⇒ ρ ⇒ τ) _·_ : ∀{σ τ : type} → T(σ ⇒ τ) → T σ → T τ infixr 1 _⇒_ infixl 1 _·_ \end{code} Notice that there are five constants (or combinators) and one binary constructor (application). Notice also that one can build only well-typed terms. The set-theoretical interpretation of type expressions and terms is given by \begin{code} Set⟦_⟧ : type → Set Set⟦ ι ⟧ = ℕ Set⟦ σ ⇒ τ ⟧ = Set⟦ σ ⟧ → Set⟦ τ ⟧ \end{code} \begin{code} ⟦_⟧ : ∀{σ : type} → T σ → Set⟦ σ ⟧ ⟦ Zero ⟧ = zero ⟦ Succ ⟧ = succ ⟦ Rec ⟧ = rec ⟦ K ⟧ = Ķ ⟦ S ⟧ = Ş ⟦ t · u ⟧ = ⟦ t ⟧ ⟦ u ⟧ \end{code} An element of the set-theoretical model is called T-definable if there is a T-term denoting it: \begin{code} T-definable : ∀{σ : type} → Set⟦ σ ⟧ → Set T-definable x = Σ \t → ⟦ t ⟧ ≡ x \end{code} As discussed above, the main theorem, proved in the last subsection, is that every \AgdaC{T}-definable function \AgdaC{Baire → ℕ} is continuous. The system \AgdaC{T} type of such functionals is \AgdaC{(ι ⇒ ι) ⇒ ι}. We also consider system T extended with a formal oracle \AgdaC{Ω : ι ⇒ ι}: \begin{code} data TΩ : (σ : type) → Set where Ω : TΩ(ι ⇒ ι) Zero : TΩ ι Succ : TΩ(ι ⇒ ι) Rec : ∀{σ : type} → TΩ((σ ⇒ σ) ⇒ σ ⇒ ι ⇒ σ) K : ∀{σ τ : type} → TΩ(σ ⇒ τ ⇒ σ) S : ∀{ρ σ τ : type} → TΩ((ρ ⇒ σ ⇒ τ) ⇒ (ρ ⇒ σ) ⇒ ρ ⇒ τ) _·_ : ∀{σ τ : type} → TΩ(σ ⇒ τ) → TΩ σ → TΩ τ \end{code} In the standard set-theoretical interpretation, the oracle can be thought of as a free variable ranging over elements of the interpretation Baire of the type expression \AgdaC{ι ⇒ ι}: \begin{code} ⟦_⟧' : ∀{σ : type} → TΩ σ → Baire → Set⟦ σ ⟧ ⟦ Ω ⟧' α = α ⟦ Zero ⟧' α = zero ⟦ Succ ⟧' α = succ ⟦ Rec ⟧' α = rec ⟦ K ⟧' α = Ķ ⟦ S ⟧' α = Ş ⟦ t · u ⟧' α = ⟦ t ⟧' α (⟦ u ⟧' α) \end{code} To regard TΩ as an extension of T we need to work with an embedding: \begin{code} embed : ∀{σ : type} → T σ → TΩ σ embed Zero = Zero embed Succ = Succ embed Rec = Rec embed K = K embed S = S embed (t · u) = (embed t) · (embed u) \end{code} \subsection{The dialogue interpretation of system \AgdaC{T}} \label{section:dialogue:interpretation} We now consider an auxiliary interpretation of system T extended with an oracle in order to show that the original T-definable functions Baire → ℕ are continuous. In the alternative semantics, types are interpreted as the underlying objects of certain algebras of the dialogue monad. The ground type is interpreted as the free algebra of the standard interpretation, and function types as function sets. For the sake of brevity, we will include only the parts of the definition of the monad that we actually need for our purposes. \begin{code} kleisli-extension : ∀{X Y : Set} → (X → B Y) → B X → B Y kleisli-extension f (η x) = f x kleisli-extension f (β φ i) = β (λ j → kleisli-extension f (φ j)) i B-functor : ∀{X Y : Set} → (X → Y) → B X → B Y B-functor f = kleisli-extension(η ∘ f) \end{code} The following two lemmas are crucial. We first swap the two arguments of the dialogue function to have the view that from an element of the Baire type we get a B-algebra \AgdaC{B $X$ → $X$} for any \AgdaC{$X$}: \begin{code} decode : ∀{X : Set} → Baire → B X → X decode α d = dialogue d α \end{code} The decodification map is natural for any oracle α : Baire: % % B g % B X --------------> B Y % | | % decode α | | decode α % | | % v v % X ----------------> Y % g % \begin{small} \begin{diagram}[small] \text{B $X$} & \rTo^{\text{B $g$}} & \text{B $Y$} \\ \dTo^{\text{decode α}} & & \dTo_{\text{decode α}} \\ X & \rTo_{g} & Y. \end{diagram} \end{small} \begin{code} decode-α-is-natural : ∀{X Y : Set}(g : X → Y)(d : B X)(α : Baire) → g(decode α d) ≡ decode α (B-functor g d) decode-α-is-natural g (η x) α = refl decode-α-is-natural g (β φ i) α = decode-α-is-natural g (φ(α i)) α \end{code} The following diagram commutes for any \AgdaC{$f$ : $X$ → B $Y$}: % % kleisli-extension f % B X ---------------------> B Y % | | % decode α | | decode α % | | % V | % X ---------> BY ---------> Y % f decode α \begin{small} \begin{diagram}[small] \text{B $X$} & \rTo^{\text{~~~~~~~~~~~~kleisli-extension $f$}} & & & \text{B $Y$} \\ \dTo^{\text{decode α}} & & & & \dTo_{\text{decode α}} \\ X & \rTo_{f} & \text{B $Y$} & \rTo_{\text{decode α}} & Y. \end{diagram} \end{small} \begin{code} decode-kleisli-extension : ∀{X Y : Set}(f : X → B Y)(d : B X)(α : Baire) → decode α (f(decode α d)) ≡ decode α (kleisli-extension f d) decode-kleisli-extension f (η x) α = refl decode-kleisli-extension f (β φ i) α = decode-kleisli-extension f (φ(α i)) α \end{code} System TΩ type expressions are interpreted as the underlying sets of certain algebras of the dialogue monad. The base type is interpreted as the underlying set of the free algebra of the standard interpretation, and function types are interpreted as sets of functions, exploiting the fact that algebras are exponential ideals (if $Y$ is the underlying object of an algebra, then so is the set of all functions $X$ → $Y$ for any $X$, with the pointwise structure). \begin{code} B-Set⟦_⟧ : type → Set B-Set⟦ ι ⟧ = B(Set⟦ ι ⟧) B-Set⟦ σ ⇒ τ ⟧ = B-Set⟦ σ ⟧ → B-Set⟦ τ ⟧ \end{code} According to the official definition of an algebra of a monad, to show that a set $X$ is the underlying object of an algebra one must provide a structure map \AgdaC{B $X$ → $X$}. Alternatively, which is more convenient for us, one can provide a generalized Kleisli extension operator, defined as follows, where the base case is just Kleisli extension, and the induction step is pointwise extension: \begin{code} Kleisli-extension : ∀{X : Set} {σ : type} → (X → B-Set⟦ σ ⟧) → B X → B-Set⟦ σ ⟧ Kleisli-extension {X} {ι} = kleisli-extension Kleisli-extension {X} {σ ⇒ τ} = λ g d s → Kleisli-extension {X} {τ} (λ x → g x s) d \end{code} With this we can now define the dialogue interpretation of system TΩ. The generic element of the Baire type under this interpretation will interpret the Baire oracle Ω: \begin{code} generic : B ℕ → B ℕ generic = kleisli-extension(β η) \end{code} As discussed in Section~\ref{formulation}, the crucial property of the generic element is this: % the following diagram commutes for any \AgdaC{α : Baire}: % % generic % B ℕ ------------> B ℕ % | | % | | % decode α | | decode α % | | % | | % v v % ℕ --------------> ℕ % α \begin{small} \begin{diagram}[small] \text{B ℕ} & \rTo^{\text{generic}} & \text{B ℕ} \\ \dTo^{\text{decode α}} & & \dTo_{\text{decode α}} \\ \text{ℕ} & \rTo_{\text{α}} & \text{ℕ}. \end{diagram} \end{small} \begin{code} generic-diagram : ∀(α : Baire)(d : B ℕ) → α(decode α d) ≡ decode α (generic d) generic-diagram α (η n) = refl generic-diagram α (β φ n) = generic-diagram α (φ(α n)) \end{code} The alternative interpretations of zero and successor are obvious: \begin{code} zero' : B ℕ zero' = η zero succ' : B ℕ → B ℕ succ' = B-functor succ \end{code} And the interpretation of the primitive recursion combinator again uses Kleisli extension in an obvious way: \begin{code} rec' : ∀{σ : type} → (B-Set⟦ σ ⟧ → B-Set⟦ σ ⟧) → B-Set⟦ σ ⟧ → B ℕ → B-Set⟦ σ ⟧ rec' f x = Kleisli-extension(rec f x) \end{code} This gives the dialogue interpretation. Notice that the interpretations of K, S and application are standard. This is because we interpret function types as sets of functions: \begin{code} B⟦_⟧ : ∀{σ : type} → TΩ σ → B-Set⟦ σ ⟧ B⟦ Ω ⟧ = generic B⟦ Zero ⟧ = zero' B⟦ Succ ⟧ = succ' B⟦ Rec ⟧ = rec' B⟦ K ⟧ = Ķ B⟦ S ⟧ = Ş B⟦ t · u ⟧ = B⟦ t ⟧ (B⟦ u ⟧) \end{code} This semantics gives the desired dialogue trees: \begin{code} dialogue-tree : T((ι ⇒ ι) ⇒ ι) → B ℕ dialogue-tree t = B⟦ (embed t) · Ω ⟧ \end{code} \noindent The remainder of the development is the formulation and proof of the correctness of the dialogue-tree function. We conclude this section with the trivial proof that the embedding of T into TΩ preserves the standard interpretation and furthermore is independent of oracles: \begin{code} preservation : ∀{σ : type} → ∀(t : T σ) → ∀(α : Baire) → ⟦ t ⟧ ≡ ⟦ embed t ⟧' α preservation Zero α = refl preservation Succ α = refl preservation Rec α = refl preservation K α = refl preservation S α = refl preservation (t · u) α = cong₂ (λ f x → f x) (preservation t α) (preservation u α) \end{code} \subsection{Relating the two models} \label{section:logical:relation} The main lemma is that for any term \AgdaC{$t$ : TΩ ι}, \begin{quote} ⟦ $t$ ⟧$'$ α ≡ decode α (B⟦ $t$ ⟧). \end{quote} We use the following logical relation to prove this: \begin{code} R : ∀{σ : type} → (Baire → Set⟦ σ ⟧) → B-Set⟦ σ ⟧ → Set R {ι} n n' = ∀(α : Baire) → n α ≡ decode α n' R {σ ⇒ τ} f f' = ∀(x : Baire → Set⟦ σ ⟧)(x' : B-Set⟦ σ ⟧) → R {σ} x x' → R {τ} (λ α → f α (x α)) (f' x') \end{code} We need a (fairly general) technical lemma, which is used for constants with an interpretation using the Kleisli-extension operator. In our case, this is just the recursion combinator. The proof is by induction on type expressions, crucially relying on the lemma \emph{decode-kleisli-extension}, but is routine otherwise: \begin{code} R-kleisli-lemma : ∀(σ : type)(g : ℕ → Baire → Set⟦ σ ⟧)(g' : ℕ → B-Set⟦ σ ⟧) → (∀(k : ℕ) → R (g k) (g' k)) → ∀(n : Baire → ℕ)(n' : B ℕ) → R n n' → R (λ α → g (n α) α) (Kleisli-extension g' n') R-kleisli-lemma ι g g' rg n n' rn = λ α → trans (fact₃ α) (fact₀ α) where fact₀ : ∀ α → decode α (g' (decode α n')) ≡ decode α (kleisli-extension g' n') fact₀ = decode-kleisli-extension g' n' fact₁ : ∀ α → g (n α) α ≡ decode α (g'(n α)) fact₁ α = rg (n α) α fact₂ : ∀ α → decode α (g' (n α)) ≡ decode α (g' (decode α n')) fact₂ α = cong (λ k → decode α (g' k)) (rn α) fact₃ : ∀ α → g (n α) α ≡ decode α (g' (decode α n')) fact₃ α = trans (fact₁ α) (fact₂ α) R-kleisli-lemma (σ ⇒ τ) g g' rg n n' rn = λ y y' ry → R-kleisli-lemma τ (λ k α → g k α (y α)) (λ k → g' k y') (λ k → rg k y y' ry) n n' rn \end{code} The proof of the main lemma is by induction on terms, crucially relying on the lemmas \emph{generic-diagram} (for the term \AgdaC{Ω}), \emph{decode-is-natural} (for the term \AgdaC{Succ}) and \emph{R-kleisli-lemma} (for the term \AgdaC{Rec}). The terms \AgdaC{K} and \AgdaC{S} are routine (but laborious and difficult to get right in an informal calculation), and so is the induction step for application: \begin{code} main-lemma : ∀{σ : type}(t : TΩ σ) → R ⟦ t ⟧' (B⟦ t ⟧) main-lemma Ω = lemma where claim : ∀ α n n' → n α ≡ dialogue n' α → α(n α) ≡ α(decode α n') claim α n n' s = cong α s lemma : ∀(n : Baire → ℕ)(n' : B ℕ) → (∀ α → n α ≡ decode α n') → ∀ α → α(n α) ≡ decode α (generic n') lemma n n' rn α = trans (claim α n n' (rn α)) (generic-diagram α n') main-lemma Zero = λ α → refl main-lemma Succ = lemma where claim : ∀ α n n' → n α ≡ dialogue n' α → succ(n α) ≡ succ(decode α n') claim α n n' s = cong succ s lemma : ∀(n : Baire → ℕ)(n' : B ℕ) → (∀ α → n α ≡ decode α n') → ∀ α → succ (n α) ≡ decode α (B-functor succ n') lemma n n' rn α = trans (claim α n n' (rn α)) (decode-α-is-natural succ n' α) \end{code} \begin{code} main-lemma {(σ ⇒ .σ) ⇒ .σ ⇒ ι ⇒ .σ} Rec = lemma where lemma : ∀(f : Baire → Set⟦ σ ⟧ → Set⟦ σ ⟧)(f' : B-Set⟦ σ ⟧ → B-Set⟦ σ ⟧) → R {σ ⇒ σ} f f' → ∀(x : Baire → Set⟦ σ ⟧)(x' : B-Set⟦ σ ⟧) → R {σ} x x' → ∀(n : Baire → ℕ)(n' : B ℕ) → R {ι} n n' → R {σ} (λ α → rec (f α) (x α) (n α)) (Kleisli-extension(rec f' x') n') lemma f f' rf x x' rx = R-kleisli-lemma σ g g' rg where g : ℕ → Baire → Set⟦ σ ⟧ g k α = rec (f α) (x α) k g' : ℕ → B-Set⟦ σ ⟧ g' k = rec f' x' k rg : ∀(k : ℕ) → R (g k) (g' k) rg zero = rx rg (succ k) = rf (g k) (g' k) (rg k) main-lemma K = λ x x' rx y y' ry → rx main-lemma S = λ f f' rf g g' rg x x' rx → rf x x' rx (λ α → g α (x α)) (g' x') (rg x x' rx) main-lemma (t · u) = main-lemma t ⟦ u ⟧' B⟦ u ⟧ (main-lemma u) \end{code} This gives the correctness of the dialogue-tree function defined above: the standard interpretation of a term is computed by its dialogue tree. \begin{code} dialogue-tree-correct : ∀(t : T((ι ⇒ ι) ⇒ ι))(α : Baire) → ⟦ t ⟧ α ≡ decode α (dialogue-tree t) dialogue-tree-correct t α = trans claim₀ claim₁ where claim₀ : ⟦ t ⟧ α ≡ ⟦ (embed t) · Ω ⟧' α claim₀ = cong (λ g → g α) (preservation t α) claim₁ : ⟦ (embed t) · Ω ⟧' α ≡ decode α (dialogue-tree t) claim₁ = main-lemma ((embed t) · Ω) α \end{code} \noindent The desired result follows directly from this: \begin{code} eloquence-theorem : ∀(f : Baire → ℕ) → T-definable f → eloquent f eloquence-theorem f (t , r) = (dialogue-tree t , λ α → trans(sym(dialogue-tree-correct t α))(cong(λ g → g α) r)) corollary₀ : ∀(f : Baire → ℕ) → T-definable f → continuous f corollary₀ f d = eloquent-is-continuous f (eloquence-theorem f d) corollary₁ : ∀(f : Baire → ℕ) → T-definable f → uniformly-continuous(C-restriction f) corollary₁ f d = eloquent-is-UC (C-restriction f) (eloquent-restriction f (eloquence-theorem f d)) \end{code} \noindent This concludes the full, self-contained, MLTT proof in Agda notation, given from scratch. Because MLTT proofs are programs, we can run the two corollaries to compute moduli of (uniform) continuity of T-definable functions. Because MLTT itself has an interpretation in ZF(C), in which types are sets in the sense of classical mathematics, the results of this paper hold in classical mathematics too. Because the \LaTeX\ source for this article~\cite{escardo:dialogue} is simultaneously an Agda file that type-checks, the readers don't need to check the routine details of the proofs themselves, provided they trust the minimal core of Agda used here, and can instead concentrate on the interesting details of the constructions and proofs. One can envisage a future in which it will be easier to write (constructive and non-constructive) formal proofs than informal, rigorous proofs, letting our minds concentrate on the insights. This is certainly a provocative statement. But, in fact, the proof presented here was directly written in its formal form, without an informal draft other than a mental picture starting from the idea of generic sequence as described in the introduction, with some rudimentary help by Agda to perform the routine steps. Tactic-based systems such as e.g.\ Coq provide much more help, which in some instances can be considered as non-routine even if ultimately they are based on algorithms. But our principal motivation for writing this formal proof in an MLTT or realizability based computer system such as NuPrl, Coq, Lego, Agda, Minlog etc.\ is that mentioned above, that the proof is literally a program too, and hence can be used to compute moduli of (uniform) continuity, without the need to write a separate algorithm based on an informal, rigorous proof, as it is usually currently done, including by ourselves in previous work. Having said that, it is useful to have a self-contained informal rigorous proof, which we include in the next section. Before that, we conclude this section by running our formal constructive proof for the purposes of illustration. \subsection{Experiments} \label{section:experiments} To illustrate the concrete sense in which the above formal proof is constructive, we develop some experiments. These experiments are not meant to indicate the usefulness of the theorem proved above. They merely make clear that the theorems do have a concrete computational content. First of all, given a term \AgdaC{$t$ : (ι ⇒ ι) ⇒ ι}, we can compute its modulus of (uniform) continuity. \begin{code} mod-cont : T((ι ⇒ ι) ⇒ ι) → Baire → List ℕ mod-cont t α = π₀(corollary₀ ⟦ t ⟧ (t , refl) α) mod-cont-obs : ∀(t : T((ι ⇒ ι) ⇒ ι))(α : Baire) → mod-cont t α ≡ π₀(dialogue-continuity (dialogue-tree t) α) mod-cont-obs t α = refl infixl 0 _∷_ infixl 1 _++_ _++_ : {X : Set} → List X → List X → List X [] ++ u = u (x ∷ t) ++ u = x ∷ t ++ u flatten : {X : Set} → Tree X → List X flatten empty = [] flatten (branch x t) = x ∷ flatten(t ₀) ++ flatten(t ₁) mod-unif : T((ι ⇒ ι) ⇒ ι) → List ℕ mod-unif t = flatten(π₀ (corollary₁ ⟦ t ⟧ (t , refl))) \end{code} The following Agda declaration allows us to write e.g.\ $3$ rather than \AgdaC{succ(succ(succ zero))}: \begin{code} {-# BUILTIN NATURAL ℕ #-} {-# BUILTIN ZERO zero #-} {-# BUILTIN SUC succ #-} \end{code} A difficulty we face is that it is not easy to write system T programs in the combinatory version of system~T. Hence we start by developing some machinery. \begin{code} I : ∀{σ : type} → T(σ ⇒ σ) I {σ} = S · K · (K {σ} {σ}) I-behaviour : ∀{σ : type}{x : Set⟦ σ ⟧} → ⟦ I ⟧ x ≡ x I-behaviour = refl number : ℕ → T ι number zero = Zero number (succ n) = Succ · (number n) \end{code} Here is our first example: \begin{code} t₀ : T((ι ⇒ ι) ⇒ ι) t₀ = K · (number 17) t₀-interpretation : ⟦ t₀ ⟧ ≡ λ α → 17 t₀-interpretation = refl example₀ example₀' : List ℕ example₀ = mod-cont t₀ (λ i → i) example₀' = mod-unif t₀ \end{code} These examples both evaluate to []. To provide more sophisticated examples, we work with an impoverished context γ that allows us to consider just one free variable v, which is represented by the I combinator: \begin{code} v : ∀{γ : type} → T(γ ⇒ γ) v = I \end{code} Application for such a context amounts to the S combinator: \begin{code} infixl 1 _•_ _•_ : ∀{γ σ τ : type} → T(γ ⇒ σ ⇒ τ) → T(γ ⇒ σ) → T(γ ⇒ τ) f • x = S · f · x Number : ∀{γ} → ℕ → T(γ ⇒ ι) Number n = K · (number n) \end{code} Here is an example: \begin{code} t₁ : T((ι ⇒ ι) ⇒ ι) t₁ = v • (Number 17) t₁-interpretation : ⟦ t₁ ⟧ ≡ λ α → α 17 t₁-interpretation = refl example₁ : List ℕ example₁ = mod-unif t₁ \end{code} This evaluates to 17 ∷ []. \begin{code} t₂ : T((ι ⇒ ι) ⇒ ι) t₂ = Rec • t₁ • t₁ t₂-interpretation : ⟦ t₂ ⟧ ≡ λ α → rec α (α 17) (α 17) t₂-interpretation = refl example₂ example₂' : List ℕ example₂ = mod-unif t₂ example₂' = mod-cont t₂ (λ i → i) \end{code} These examples evaluate to 17 ∷ 17 ∷ 17 ∷ 0 ∷ 1 ∷ [] and to a list whose members are all 17. \begin{code} Add : T(ι ⇒ ι ⇒ ι) Add = Rec · Succ infixl 0 _+_ _+_ : ∀{γ} → T(γ ⇒ ι) → T(γ ⇒ ι) → T(γ ⇒ ι) x + y = K · Add • x • y t₃ : T((ι ⇒ ι) ⇒ ι) t₃ = Rec • (v • Number 1) • (v • Number 2 + v • Number 3) t₃-interpretation : ⟦ t₃ ⟧ ≡ λ α → rec α (α 1) (rec succ (α 2) (α 3)) t₃-interpretation = refl example₃ example₃' : List ℕ example₃ = mod-cont t₃ succ example₃' = mod-unif t₃ \end{code} These examples evaluate to 3 ∷ 2 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ [] and 3 ∷ 2 ∷ 1 ∷ 1 ∷ 0 ∷ 1 ∷ 2 ∷ 1 ∷ 0 ∷ 1 ∷ 1 ∷ 0 ∷ 0 ∷ 1 ∷ 1 ∷ 0 ∷ 1 ∷ []. \begin{code} length : {X : Set} → List X → ℕ length [] = 0 length (x ∷ s) = succ(length s) max : ℕ → ℕ → ℕ max 0 x = x max x 0 = x max (succ x) (succ y) = succ(max x y) Max : List ℕ → ℕ Max [] = 0 Max (x ∷ s) = max x (Max s) t₄ : T((ι ⇒ ι) ⇒ ι) t₄ = Rec • ((v • (v • Number 2)) + (v • Number 3)) • t₃ t₄-interpretation : ⟦ t₄ ⟧ ≡ λ α → rec α (rec succ (α (α 2)) (α 3)) (rec α (α 1) (rec succ (α 2) (α 3))) t₄-interpretation = refl example₄ example₄' : ℕ example₄ = length(mod-unif t₄) example₄' = Max(mod-unif t₄) \end{code} These examples evaluate to 215 and 3. \begin{code} t₅ : T((ι ⇒ ι) ⇒ ι) t₅ = Rec • (v • (v • t₂ + t₄)) • (v • Number 2) t₅-explicitly : t₅ ≡ (S · (S · Rec · (S · I · (S · (S · (K · (Rec · Succ)) · (S · I · (S · (S · Rec · (S · I · (K · (number 17))))· (S · I · (K · (number 17)))))) · (S · (S · Rec · (S · (S · (K · (Rec · Succ)) · (S · I · (S · I · (K · (number 2))))) · (S · I · (K · (number 3))))) · (S · (S · Rec · (S · I · (K · (number 1)))) · (S · (S · (K · (Rec · Succ)) · (S · I · (K · (number 2)))) · (S · I · (K · (number 3))))))))) · (S · I · (K · (number 2)))) t₅-explicitly = refl t₅-interpretation : ⟦ t₅ ⟧ ≡ λ α → rec α (α(rec succ (α(rec α (α 17) (α 17))) (rec α (rec succ (α (α 2)) (α 3)) (rec α (α 1) (rec succ (α 2) (α 3)))))) (α 2) t₅-interpretation = refl example₅ example₅' example₅'' : ℕ example₅ = length(mod-unif t₅) example₅' = Max(mod-unif t₅) example₅'' = Max(mod-cont t₅ succ) \end{code} These examples evaluate to 15551, 17 and 57. All evaluations reported above are instantaneous, except this last set, which takes about a minute in a low-end netbook. The use of Church encoding of dialogue trees produces a dramatic performance improvement~\cite{escardo:dialogue}, with an instantaneous answer in these examples, because Klesli extension and the functor don't need to walk through trees to be performed. \section{Informal, rigorous proof} \label{section:informal} \newcommand{\decode}{\operatorname{decode}} \newcommand{\generic}{\operatorname{generic}} \newcommand{\T}{\operatorname{T}} \newcommand{\D}{\operatorname{D}} \newcommand{\B}{\operatorname{B}} \newcommand{\To}{\Rightarrow} \newcommand{\Zero}{\operatorname{\mathtt{Zero}}} \newcommand{\Succ}{\operatorname{\mathtt{Succ}}} \newcommand{\Rec}{\operatorname{\mathtt{Rec}}} \newcommand{\K}{\operatorname{\mathtt{K}}} \renewcommand{\SS}{\operatorname{\mathtt{S}}} \newcommand{\interp}[1]{\llbracket #1 \rrbracket} \newcommand{\binterp}[1]{{\scriptstyle \B}\llbracket #1 \rrbracket} \newcommand{\N}{\mathbb{N}} We now provide a self-contained, informal, rigorous version of the formal proof given above, in a foundationally neutral exposition. We work with the combinatory version of (the term language of) G\"odel's system~$\T$. We have a ground type~$\iota$ and a right-associative type formation operation $-\To-$. Every term as a unique type. We have the constants \begin{enumerate} \item $\Zero \colon \iota$. \item $\Succ \colon \iota \To \iota$. \item $\Rec_{\sigma} \colon (\sigma \To \sigma) \To \sigma \To \iota \To \sigma$. \item $\K_{\sigma,\tau} \colon \sigma \To \tau \To \sigma$. \item $\SS_{\rho,\sigma,\tau} \colon (\rho \To \sigma \To \tau) \To (\rho \To \sigma) \To \rho \To \tau$. \end{enumerate} We omit the subscripts when they can be uniquely inferred from the context. If $t \colon \sigma \To \tau$ and $u \colon \tau$ are terms, then so is $tu \colon \tau$, with the convention that this application operation is left associative. Write $\T_\sigma$ for the set of terms of type~$\sigma$. In the \emph{standard interpretation}, we map a type expression $\sigma$ to a set $\interp{\sigma}$ and a term $t \colon \sigma$ to an element $\interp{t} \in \interp{\sigma}$. These interpretations are defined by induction as follows: \begin{gather*} \interp{\iota} = \N, \qquad \interp{\sigma \To \tau} = \interp{\tau}^{\interp{\sigma}} = ({\interp{\sigma}} \to \interp{\tau}) \,\,\text{(set of all functions $\interp{\sigma} \to \interp{\tau}$)}, \\[1ex] \interp{\Zero} = 0, \qquad \interp{\Succ} n = n+1, \qquad \interp{\Rec} f x n = f^n(x), \\[1ex] \interp{\K} x y = x, \qquad \interp{\SS} f g x = fx(gx), \qquad \interp{tu} = \interp{t}(\interp{u}). \end{gather*} For any given three sets $X,Y,Z$, the set $\D X Y Z$ of \emph{dialogue trees} is inductively defined as follows: \begin{enumerate} \item A leaf labeled by an element $z \in Z$ is a dialogue tree, written $\eta z$. \item If $\phi \colon Y \to \D X Y Z$ is a $Y$-indexed family of dialogue trees and $x \in X$, then the tree with root labeled by $x$ and with one branch leading to the subtree $\phi y$ for each $y \in Y$ is also a dialogue tree, written $\beta \phi x$. \end{enumerate} Such trees are well founded, meaning that every path from the root to a leaf is finite. The above notation gives functions \begin{eqnarray*} \eta & \colon & Z \to \D X Y Z, \\ \beta & \colon & (Y \to \D X Y Z) \to X \to \D X Y Z. \end{eqnarray*} Dialogue trees describe ``computations'' of functions $f \colon Y^X \to Z$. Leaves give answers, and labels of internal nodes are queries to an ``oracle'' $\alpha \in Y^X$, the argument of the function~$f$. For any dialogue tree $d \in \D X Y Z$, we inductively define a function $f_d \colon Y^X \to Z$ by \[ f_{\eta z}(\alpha) = z, \qquad f_{\beta \phi x}(\alpha) = f_{\phi(\alpha x)}(\alpha). \] The functions $Y^X \to Z$ that arise in this way are called \emph{eloquent}. Notice that the oracle $\alpha$ is queried finitely many times in this computation, because a dialogue tree is well founded. Hence the function $f = f_d \colon Y^X \to Z$ satisfies \[ \forall \alpha \in Y^X \quad \exists \text{finite $S \subseteq X$ } \quad \forall \alpha' \in Y^X, \alpha =_S \alpha' \implies f\alpha=f\alpha', \] where $\alpha =_S \alpha'$ is a shorthand for $\forall x \in S, \alpha x = \alpha'x$. When $X=Y=Z=\N$, this amounts to continuity in the product topology of $\N^\N$ with $\N$ discrete, which gives the Baire space. For $Y$ finite and $X,Z$ arbitrary, the dialogue tree is finitely branching and hence finite by well-foundedness (or directly by induction), and so the set of potential queries to the oracle is finite, so that, for any $f = f_d \colon Y^X \to Z$ with~$Y$ finite, \[ \exists \text{finite $S \subseteq X$ } \forall \alpha,\alpha' \in Y^X, \quad \alpha =_S \alpha' \implies f\alpha =f \alpha'. \] When $Y=2=\{0,1\}$ and $X=Z=\N$, this amounts to (uniform) continuity in the product topology of $2^\N$ with $2$ discrete, which gives the Cantor space. Clearly, any $\N$-branching tree $d \in \D \N \N \N$ can be pruned to a $2$-branching tree $d' \in \D \N 2 \N$ so that $f_{d'} : 2^\N \to \N$ is the restriction of $f_d \colon \N^\N \to \N$ from sequences to binary sequences. Hence if we show that every $\T$-definable function $\N^\N \to \N$ is eloquent, we conclude that every $\T$-definable function $\N^\N \to \N$ is continuous and its restriction to $2^\N$ is uniformly continuous. For this purpose, we consider an auxiliary model of system $\T$. Define $\B X = \D \N \N X$. We remark that although $\B$ is the object part of a monad, as discussed in the introduction, it is not necessary to know this for the purposes of this proof. The data given below do obey the required laws to get a monad, but the details are left to the interested reader. For any function $f \colon X \to \B Y$, inductively define $f^\sharp \colon \B X \to \B Y$ by \begin{eqnarray*} f^\sharp(\eta x) &=& f x, \\ f^\sharp(\beta \phi i) &=& \beta(\lambda j.f^\sharp(\phi j)) i. \end{eqnarray*} This says that the tree $f^\sharp(d)$ is $d$ with each leaf labeled by $x$ replaced by the subtree $f x$, with no changes to the internal nodes. Given $f \colon X \to Y$, we define $f \colon \B X \to \B Y$ by \[ \B f = (\eta \circ f)^\sharp. \] Hence $\B f(d)$ replaces each label $x$ of a leaf of $d$ by the label $f(x)$, and we have the naturality condition \begin{diagram}[small] \B X & \rTo^{\B f} & \B Y \\ \uTo^{\eta} & & \uTo_{\eta} \\ X & \rTo_{f} & Y. \end{diagram} For each $\alpha \in \N^\N$ and any set $X$, define a map $\decode_\alpha \colon \B X \to X$ by \[ \decode_\alpha (d) = f_d(\alpha). \] Then, by definition, $\decode_\alpha(\eta x) = x$, and hence the naturality of $\eta$ gives that of $\decode_\alpha$: \begin{equation} \label{decode-is-natural} \begin{diagram}[small] \B X & \rTo^{\B f} & \B Y \\ \dTo^{\decode_\alpha} & & \dTo_{\decode_\alpha} \\ X & \rTo_{f} & Y. \end{diagram} \end{equation} It is also easy to see, by induction on dialogue trees, that \begin{equation} \label{decode:kleisli:extension} \begin{diagram}[small] \B X & & \rTo^{f^\sharp} & & \B Y \\ \dTo^{\decode_\alpha} & & & & \dTo_{\decode_\alpha} \\ X & \rTo_{f} & \B Y & \rTo_{\decode_\alpha} & Y. \end{diagram} \end{equation} Now define \begin{eqnarray*} \generic & \colon & \B \N \to \B \N \\ \generic & = & (\beta \eta)^\sharp. \end{eqnarray*} Because $\beta \colon (\N \to \B \N) \to \N \to \B \N$ and $\eta \colon \N \to \B \N$, the function $\generic$ is well defined. Its crucial property is that \begin{equation} \label{generic:diagram} \begin{diagram}[small] \B \N & \rTo^{\generic} & \B \N \\ \dTo^{\decode_\alpha} & & \dTo_{\decode_\alpha} \\ \N & \rTo_{\alpha} & \N. \end{diagram} \end{equation} The proof that \[ \decode_\alpha(\generic d) = \alpha(\decode_\alpha d) \] is straightforward by induction on $d$. Now define the $\B$-interpretation of types as follows: \begin{gather*} \binterp{\iota} = \B(\interp{\iota}) = \B \N, \qquad \qquad \binterp{\sigma \To \tau} = \binterp{\tau}^{\binterp{\sigma}}. \end{gather*} For any type $\sigma$ and $f \colon X \to \binterp{\sigma}$, define $f^\sharp \colon \B X \to \binterp{\sigma}$ by induction on $\sigma$, where the base case $\sigma = \iota$ is given by the above definition, and the induction step $\sigma = (\rho \To \tau)$ is given pointwise as \[ f^\sharp d y = (\lambda x. f x y)^\sharp d. \] Notice that $f \colon X \to \binterp{\rho} \to \binterp{\tau}$ and $f^\sharp \colon \B X \to \binterp{\rho} \to \binterp{\tau}$. Next extend system $\T$ with a new constant $\Omega \colon \iota \To \iota$, a formal oracle, and define the $\B$-interpretation of terms as follows: \begin{gather*} \binterp{\Omega} = \generic, \quad \binterp{\Zero} = \eta 0, \quad \binterp{\Succ} = \B(\lambda n.n+1), \quad \binterp{\Rec} f x = (\lambda n.f^n(x))^\sharp, \\[1ex] \binterp{\K} x y = x, \qquad \binterp{\SS} f g x = fx(gx), \qquad \binterp{tu} = \binterp{t}(\binterp{u}). \end{gather*} We also need to consider the standard interpretation of system $\T$ extended with the oracle $\Omega$. We treat the oracle as a free variable, as hence the value of this free variable has to be provided to define the interpretation: \begin{gather*} \interp{\Omega} \alpha = \alpha, \qquad \interp{\Zero} \alpha = 0, \qquad \interp{\Succ} \alpha n = n+1, \qquad \interp{\Rec} \alpha f x n = f^n(x), \\[1ex] \interp{\K} \alpha x y = x, \qquad \interp{\SS} \alpha f g x = fx(gx), \qquad \interp{tu} \alpha = \interp{t}\alpha (\interp{u} \alpha). \end{gather*} We claim that for any term $t \colon \iota$, \[ \interp{t} \alpha = \decode_\alpha (\binterp{t}). \] To prove this, we work with a logical relation $R_\sigma$ between functions $\N^\N \to \interp{\sigma}$ and elements of $\binterp{\sigma}$ by induction on $\sigma$. For any $n \colon \N^\N \to \N$ and $n' \in \B \N$, we define \[ R_\iota n n' \iff \forall \alpha, n \alpha = \decode_\alpha n', \] and, for any $f \colon \N^\N \to \interp{\sigma} \to \interp{\tau}$ and $f' \colon \binterp{\sigma} \to \binterp{\tau}$, we define \[ R_{\sigma \to \tau} f f' \iff \forall x \colon \N^\N \to \interp{\sigma}, \,\, \forall x' : \binterp{\sigma}, \,\, R_{\sigma} x x' \to R_\tau (\lambda \alpha, f \alpha (x \alpha)) (f' x').\] We need a technical lemma for dealing with the dialogue interpretation of $\Rec$: \begin{claim} \label{R:kleisli:claim} For all $g \colon \N \to \N^\N \to \binterp{\sigma}$ and $g' \colon \N \to \binterp{\sigma}$, if \[ \forall k \in \N, \,\, R_{\sigma} (g k) (g' k), \] then $ \forall n \colon \N^\N \to \N, \,\, \forall n' \in \B \N, \,\, R_{\iota} n n' \to R_{\sigma} (\lambda \alpha \to g (n \alpha) \alpha) (g' n')^\sharp. $ \end{claim} The proof is straightforward by induction on types, using diagram~\ref{decode:kleisli:extension}. \begin{claim} $R_\sigma \, \interp{t} \, (\binterp{t})$ for every term $t \colon \sigma$. \end{claim} The proof is by induction on terms, using diagram~\ref{generic:diagram} for the term~$\Omega$, diagram~\ref{decode-is-natural} for the term~$\Succ$, and Claim~\ref{R:kleisli:claim} for the term~$\Rec$. The terms~$\K$ and~$\SS$ are immediate but perhaps laborious, and the induction step, namely term application, is easy. This gives, in particular: \begin{claim} For every term $t \colon (\iota \To \iota) \To \iota$, we have $ \interp{t} \alpha = \decode_\alpha (\binterp{t\Omega}).$ \end{claim} It follows that every $\T$-definable function $f \colon \N^\N \to \N$ is eloquent, with dialogue tree given by $\binterp{t\Omega}$, where $t \colon (\iota \To \iota) \To \iota$ is any term denoting~$f$, and hence continuous, with uniformly continuous restriction to~$2^\N$. \section{Discussion, questions and conjectures} It may not be apparent from the informal proof of Section~\ref{section:informal} that the argument is constructive, but Section~\ref{section:formal} provides a constructive rendering in Martin-L\"of type theory. We emphasize that our proof doesn't invoke the Fan Theorem~\cite{MR0325352,beeson} or any constructively contentious axiom. We have deliberately chosen system T in its combinatory form as the simplest and most memorable non-trivial higher-type language to illustrate the essence of the technique proposed here. It is clearly routine (as well as interesting and useful) to apply the technique to a number of well-known extensions of the simply-typed lambda-calculus. But, for instance, at the time of writing, dependent types seem to require further thought, particularly in the presence of universes. Can one, e.g.\ (generalize and) apply the technique developed here to show that all MLTT definable functions \AgdaC{(ℕ → ℕ) → ℕ} are continuous, and that their restrictions to \AgdaC{(ℕ → 2)} are uniformly continuous, in the main versions of (intensional) MLTT? More ambitiously, does the technique apply to Homotopy Type Theory~\cite{HoTTbook}? As pointed out by one of the anonymous referees, the syntactical techniques of~\cite{MR0325352} give more information: for any term $t$ of type $(\iota \Rightarrow \iota) \Rightarrow \iota$ one can construct a term $m : (\iota \Rightarrow \iota) \Rightarrow \iota$ such that $m$ internalizes the modulus of continuity of $t$. We adapted our technique to achieve this, as reported in~\cite{escardo:dialogue}, by working with Church encodings of dialogue trees defined within system~T, and turning our semantical interpretation into a compositional translation of system~T into itself. A corollary is that the dialogue trees of T-definable functions \AgdaC{(ℕ → ℕ) → ℕ}, being themselves T-definable, have height smaller than $\epsilon_0$. % \bibliographystyle{plain} % \bibliography{references} \begin{thebibliography}{10} \bibitem{bauer:pretnar} A.~Bauer and M.~Pretnar. \newblock Programming with algebraic effects and handlers. \newblock Submitted for publication, 2012. \bibitem{beeson} M.J. Beeson. \newblock {\em Foundations of Constructive Mathematics}. \newblock Springer, 1985. \bibitem{bishop:foundations} E.~Bishop. \newblock {\em Foundations of constructive analysis}. \newblock McGraw-Hill Book Co., New York, 1967. \bibitem{bove:dybjer} A.~Bove and P.~Dybjer. \newblock Dependent types at work. \newblock {\em Proceedings of Language Engineering and Rigorous Software Development, LNCS}, 5520:57--99, 2009. \bibitem{Coquand:2010:NFT:1839560.1839564} T.~Coquand and G.~Jaber. \newblock A note on forcing and type theory. \newblock {\em Fundam. Inf.}, 100(1-4):43--52, January 2010. \bibitem{DBLP:series/leus/CoquandJ12} T.~Coquand and G.~Jaber. \newblock A computational interpretation of forcing in type theory. \newblock In {\em Epistemology versus Ontology}, pages 203--213. Springer, 2012. \bibitem{escardo:dialogue} M.H. Escard\'o. \newblock Continuity of {G}\"odel's system {T} definable functionals via effectful forcing. \newblock Agda proof at \url{http://www.cs.bham.ac.uk/~mhe/dialogue/}, July 2012. \bibitem{Hancock_representationsof} P.~Hancock, D.~Pattinson, and N.~Ghani. \newblock Representations of stream processors using nested fixed points. \newblock In {\em Logical Methods in Computer Science}, page 2009. \bibitem{Howard(80)} W.~A. Howard. \newblock Ordinal analysis of terms of finite type. \newblock {\em The Journal of Symbolic Logic}, 45:493--504, 1980. \bibitem{KleeneSC:rfqftI} S.C. Kleene. \newblock Recursive functionals and quantifiers of finite types {I}. \newblock {\em Trans.\ Amer.\ Math.\ Soc}, 91, 1959. \bibitem{Longley99whenis} J.~Longley. \newblock When is a functional program not a functional program? \newblock In {\em Proceedings of Fourth ACM SIGPLAN International Conference on Functional Programming}, pages 1--7. ACM Press, 1999. \bibitem{DBLP:conf/csl/HancockS00} P.Hancock and A.~Setzer. \newblock Interactive programs in dependent type theory. \newblock In {\em CSL}, pages 317--331, 2000. \bibitem{Plotkin03algebraicoperations} G.~Plotkin and J.~Power. \newblock Algebraic operations and generic effects. \newblock {\em Applied Categorical Structures}, 11, 2003. \bibitem{HoTTbook} The Univalent~Foundations Program. \newblock Homotopy type theory: Univalent foundations of mathematics. \newblock Technical report, Institute for Advanced Study, 2013. \bibitem{MR0325352} A.~S. Troelstra, editor. \newblock {\em Metamathematical investigation of intuitionistic arithmetic and analysis}. \newblock Lecture Notes in Mathematics, Vol. 344. Springer-Verlag, Berlin, 1973. \bibitem{escardo:xu} C.~Xu and M.H. Escard\'o. \newblock A constructive model of uniform continuity. \newblock To appear in TLCA, 2013. \end{thebibliography} \end{document}