Continuity in System T - The Proof Theory Blog

Continuity is one of the most important concepts in higher-order computability. Informally, a functional is continuous if we only require a finite part of its input to compute a finite part of its output. Though there are a number of ways of making this precise, at type level 2, that is, for functionals $F:\mathbb{N}^\mathbb{N}\to \mathbb{N}$ , continuity has a simple syntactic characterisation. We say that $F$ is continuous if it satisfies:

$(\forall \alpha:\mathbb{N}^\mathbb{N})(\exists N :\mathbb{N})(\forall \beta:\mathbb{N}^\mathbb{N})((\forall i<N)(\alpha_i=\beta_i) \Rightarrow F\alpha=F\beta)$

It is a well known fact that all type 2 functionals definable in Gödel’s System T are continuous in the above sense. At first glance, the reasons for this seem clear: We know that such functionals are computable, and therefore only ever evaluate their input $\alpha$ on a finite number of arguments before terminating with an output. But despite this, the literature contains a multitude of genuinely distinct proofs of this apparently simple result, and moreover, brand new proofs continue to appear! This would suggest that continuity in System T is not quite as straightforward seems…

Strong normalization and continuous models

Continuity in System T was something I used to take for granted. After all, everybody knows that System T is strongly normalizing. Therefore if $F$ is represented by the term $t:(0\to 0)\to 0$ , and we plug in some argument $\alpha$ , then $t\alpha$ reduces to some numerical $\underline{n}$ in a finite number of steps. In particular, $\alpha$ can be queried only a finite number of times, which is the same as saying that $t$ , or equivalently the functional $F$ it represents, is continuous.

Continuity of T-definable functionals is obvious because $t\alpha$ reduces to a numeral in a finite number of steps, in which $\alpha$ can only ever be queried a finite number of times.

But suppose we try to write down this proof in all its details, as can be found in e.g. Troelstra’s Metamathematical Investigations [1] (cf. §2.3.8)? First of all we need to actually prove that System T is normalizing, which is far from trivial. Then, to represent arbitrary function inputs $\alpha:\mathbb{N}\to\mathbb{N}$ formally in the term calculus we need to isolate some ‘oracle’ variable $x:0\to 0$ and extend System T with an additional reduction rule $x\underline{n}\to \underline{\alpha n}$ . Next, we need to check that our extended calculus with oracle reductions preserves the normalization property, and throughout we need to be aware of issues such as substitution and the distinction between term and their interpretation as set-theoretic functionals. So actually, things are not quite as easy as they sound.

Of course, there are alternative routes available to us. One could show that the type structure of total continuous functionals $\mathcal{C}^\omega$ forms a model of System T, and that all type 2 objects in that model satisfy the syntactic continuity property. A proof of this kind can be found in Scarpellini’s classic paper on limit spaces [2] for example. However, as with strong normalization, such arguments introduce new concepts at arbitrary finite type (such as the much trickier issue of continuity at all finite types), and so written down in full detail are, once more, far from simple.

In fact, one is tempted to admit that

Continuity of T-definable functionals is maybe not that obvious, because any proof inevitably involves a route through the higher types and typically the introduction of some more subtle notion at arbitrary finite type.

But can such a route through the finite types be found that does not resort to heavy machinery such as normalization or full models of continuous functionals?

Syntactic proofs of continuity

The last decade or so has seen the emergence of a wealth of new approaches for establishing continuity of T-definable functionals (or more generally terms in some type theory), which typically lean towards the use of simple, syntactic ideas. In many cases, this striving towards simplicity is at least partially motivated by the desire to formalize the proof, and thereby also produce a procedure for extracting moduli of continuity. Nevertheless, as a happy by-product of these efforts we now have a collection of elegant, self-contained and in many cases ingenious proofs of continuity, which bring in interesting techniques from both proof theory and programming languages. These include (and this list is by no means exhaustive):

the Dialectica interpretation (Kohlenbach [3], see also Hernest [4] for an implementation in MinLog),
monads and forcing (Coquand and Jaber [5], also with a Haskell implementation).,
dialogue trees (Escardó [6], formalized in Agda),
computational effects (Bickford and Rahli [7], formalization in Coq/Nuprl).

However, for me personally, one of the most satisfying works of this kind is the recent proof of continuity of T-definable functionals by Chuangjie Xu [8] (a formalization in Adga and an extraction mechanism for moduli of continuity is also provided). His proof is extraordinarily simple, and is based on a syntactic continuity predicate on types. To be more specific, to each type $\rho$ in System T he assigns the type $\rho^b$ given by $\mathbb{N}^b:=\mathbb{N}^\mathbb{N}\to\mathbb{N}$ and $(\rho\to\tau)^b:=\rho^b\to\tau^b$ , and this is accompanied by a corresponding translation on terms. This so-called “precooking” simply translates each term $t:\rho$ of T to a term $t^b:\rho^b$ containing a `gap’ for an oracle parameter $\alpha$ . The core of the proof is a simple syntactic extension of type 2 continuity to all finite types defined by:

$C_{\mathbb{N}}(f):\equiv \mbox{$f$ is continuous} \ \ \ \ \ \ C_{\rho\to\tau}(g):\equiv \forall x(C_\rho(x)\Rightarrow C_\tau(gx))$

By carrying out a subtle induction on terms involving this continuity predicate, Xu proves that $C_\rho(t^b)$ holds for any closed $t:\rho$ in System T, from which ordinary continuity of type 2 terms follows as a simple corollary. This sounds like a lot, but in reality it is achieved in just a few short pages, and in an entirely elementary fashion. I recommend this paper to anyone interested in lambda calculi and their properties: it’s a perfect example of mathematical economy, introducing nothing more than is strictly necessary to prove the theorem at hand!

Anyway, thanks to this remarkably clean proof, I finally feel safe in concluding that:

Continuity of T-definable functionals is obvious after all (you just need to find a clever proof…)

References

[1]

A. S. Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer-Verlag, 1973, vol. 344.
[Bibtex]

@book{troelstra:73:book,
title = {{Metamathematical Investigation of Intuitionistic Arithmetic and Analysis}},
author = {Troelstra, Anne S.},
doi = {10.1007/BFb0066739},
series = {Lecture Notes in Mathematics},
volume = {344},
publisher = {Springer-Verlag},
year = {1973},
}

[2] B. Scarpellini, “A model for barrecursion of higher types,” Compositio Mathematica, vol. 23, iss. 1, p. 123–153, 1971.
[Bibtex]

@article{scarpellini:71:barrec,
author = {Scarpellini, Bruno},
title = {A model for barrecursion of higher types},
journal = {Compositio Mathematica},
volume = {23},
number = {1},
pages = {123--153},
year = {1971},
}

[3]

U. Kohlenbach, “Pointwise hereditary majorization and some applications,” Archive for Mathematical Logic, vol. 31, p. 227–241, 1992.
[Bibtex]

@article{kohlenbach:92:maj,
author = {Kohlenbach, Ulrich},
title = {Pointwise hereditary majorization and some applications},
journal = {Archive for Mathematical Logic},
volume = {31},
pages = {227--241},
year = {1992},
doi = {10.1007/BF01794980},
}

[4]

M. Hernest, “Synthesis of moduli of uniform continuity by the monotone Dialectca interpretation in the proof-system MinLog,” Electronic Notes in Theoretical Computer Science, vol. 174, iss. 5, p. 141–149, 2007.
[Bibtex]

@article{hernest:07:moduli,
author = {Hernest, Mircea-Dan},
title = {Synthesis of moduli of uniform continuity by the monotone {D}ialectca interpretation in the proof-system {M}in{L}og},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {174},
number = {5},
pages = {141--149},
year = {2007},
doi = {10.1016/j.entcs.2007.01.023},
}

[5]

T. Coquand and G. Jaber, “A computational interpretation of forcing in type theory,” in Epistemology versus Ontology, P. Dybjer, S. Lindström, E. Palmgren, and G. Sundholm, Eds., Springer, 2012, vol. 27, p. 203–213.
[Bibtex]

@inbook{coquand-jaber:12:forcing,
author = {Coquand, Thierry and Jaber, Guilhem},
title = {A computational interpretation of forcing in type theory},
booktitle = {Epistemology versus Ontology},
series = {Logic, Epistemology, and the Unity of Science},
editor = {Dybjer, P. and Lindstr\"om, S. and Palmgren, E. and Sundholm, G.},
volume = {27},
publisher = {Springer},
pages = {203--213},
year = {2012},
doi = {10.1007/978-94-007-4435-6_10},
}

[6]

M. Escardó, “Continuity of Gödel’s System T definable functionals via effectful forcing,” Electronic Notes in Theoretical Computer Science, vol. 298, p. 119–141, 2012.
[Bibtex]

@article{escardo:13:continuity,
author = {Escard\'o, Mart\'in},
title = {Continuity of {G}\"odel's {S}ystem {T} definable functionals via effectful forcing},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {298},
pages = {119--141},
year = {2012},
doi = {10.1016/j.entcs.2013.09.010},
}

[7]

V. Rahli and M. Bickford, “Validating Brouwer’s continuity principle for numbers using named exceptions,” Mathematical Structures in Computer Science, vol. 28, iss. 6, p. 942–990, 2018.
[Bibtex]

@article{bickford-rahli:18:continuity,
author = {Rahli, Vincent and Bickford, Mark},
title = {Validating {B}rouwer's continuity principle for numbers using named exceptions},
journal = {Mathematical Structures in Computer Science},
volume = {28},
number = {6},
pages = {942--990},
year = {2018},
doi = {10.1017/S0960129517000172},
}

[8]

C. Xu, “A syntactic approach to continuity of T-definable functionals,” Logical Methods in Computer Science, vol. 16, iss. 1, 2020.
[Bibtex]

@article{xu:20:continuity,
title = {{A syntactic approach to continuity of T-definable functionals}},
author = {Xu, Chuangjie},
doi = {10.23638/LMCS-16(1:22)2020},
journal = {Logical Methods in Computer Science},
volume = {16},
number = {1},
year = {2020},
}

1 thought on “Continuity in System T”

Anupam Das says:

June 3, 2020 at 9:50 am

Thanks for the interesting post, Tom! I haven’t been through the same journey as you in understanding type 2 continuity in T, but I know what you mean about the subtlety of trying to prove normalisation with an oracle variable. Xu’s continuity predicate is really cool! Thanks for giving me the shortcut to enlightenment 😉

Strong normalization and continuous models

Syntactic proofs of continuity

References

1 thought on “Continuity in System T”

Leave a Reply Cancel reply