Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In a previous work (Coquand and Jaber 2010), we considered intuitionistic type theory with a type of natural numbers N and a type of Booleans N 2. The type C = N → N 2 represents Cantor space, the space of functions from natural numbers to Booleans, and it has a natural topology, with basic compact open subsets defined by a finite set of conditions of the form f n i  = b i about a function f : C. We have shown (Coquand and Jaber 2010) that any definable functional F : C → N 2 is uniformly continuous. This means that we can find a partition of Cantor space in a finite number of conditions \({p}_{1},\ldots,{p}_{n}\) with corresponding Boolean values \({b}_{1},\ldots,{b}_{n}\) such that F f = b i whenever f satisfies the condition p i . The argument in Coquand and Jaber (2010) is constructive, and thus can be seen implicitly an algorithm which computes an uniform modulus of continuity. We explicitate here a possible algorithm, which given such a functional F, produces a covering \({p}_{1},\ldots,{p}_{n}\) and a list \({b}_{1},\ldots,{b}_{n}\). To simplify the presentation, we limit ourselves to a type system which is an extension of Gödel system T (Gödel 1990) with a type of Booleans. This computation can be readily expressed in a functional programming language, here Haskell, using the notion of monads (Wadler 1992).

We briefly outline the paper. We first recall the syntax for terms and conditions. We then give a simple operational semantics corresponding to forcing. We prove the termination of this evaluation, and give an algorithm to compute the modulus of continuity of a given functional. These computation combines in a non trivial way realizability and Beth models, and we end by commenting on this point, following Goodman (1978). A first appendix presents a representation in the programming language Haskell and a second appendix explains how we can give computational sense to universal quantification over Cantor space by iterating this forcing construction.

2 Terms, Types and Conditions

2.1 Terms

The terms of Type Theory are untyped λ-calculus extended with constants, and with the following syntax.

$$t,u ::= x\ \vert \ \lambda x.t\ \vert \ t\ t\ \vert \ \mathsf{natrec}(t,t)\ \vert \ \mathsf{boolrec}(t,t)\ \vert \ S(t)$$

We consider terms up to α-conversion. Besides β-reduction, natrec and boolrec have the reduction rules

$$\mathsf{natrec}(a,g)\ 0 \rightarrow a\mathsf{natrec}(a,g)\ S(n) \rightarrow g\ a\ (\mathsf{natrec}(a,g)\ n)$$

and

$$\mathsf{boolrec}({a}_{0},{a}_{1})\ 0 \rightarrow {a}_{0}\mathsf{boolrec}({a}_{0},{a}_{1})\ 1 \rightarrow {a}_{1}$$

This forms an extension of β-reduction which still has the Church-Rosser property (Martin-Löf 1998), sometimes called β, ι-reduction (Barendregt 1997).

If k is a natural number, we write \(\overline{k}\) the term S k(0).

2.2 Typing Rules

The basic types are N, for natural numbers, and N k , for finite types with k elements. If A,  B are types then so is A → B. The typing judgements are of the form Γ ⊢ t: A, where Γ is a context \({x}_{1}:{A}_{1},\ldots,{x}_{n}:{A}_{n}\) (with x i ≠x j for i≠j).

The typing rules are as follows.

$$\frac{(x:A) \in \Gamma } {\Gamma \vdash x:A} \ \ \ \ \frac{\Gamma,x:A \vdash t : B} {\Gamma \vdash \lambda x.t : A \rightarrow B}\ \ \ \ \ \ \frac{\Gamma \vdash v : A \rightarrow B\ \ \ \ \Gamma \vdash u:A} {\Gamma \vdash v\ u : B}$$
$$\frac{} {\Gamma \vdash 0 : N}\ \ \ \ \frac{\Gamma \vdash t : N} {\Gamma \vdash S(t) : N}\ \ \ \ \frac{\Gamma \vdash a : B\ \ \ \ \ \ \Gamma \vdash g : N \rightarrow B \rightarrow B} {\Gamma \vdash \mathsf{natrec}(a,g) : N \rightarrow B}$$
$$\frac{} {\Gamma \vdash 0 : {N}_{2}}\ \ \ \ \frac{} {\Gamma \vdash 1 : {N}_{2}}\ \ \ \ \ \ \ \frac{\Gamma \vdash {a}_{0} : B\ \ \Gamma \vdash {a}_{1} : B} {\Gamma \vdash \mathsf{boolrec}({a}_{0},{a}_{1}) : {N}_{2} \rightarrow B}$$

2.3 Conditions

The conditions \(p,q,\ldots \) represent finite amount of information about the infinite object we want to describe. Since we want to force the addition of a Cohen real, the conditions are finite sub-graphs of function from natural numbers to Booleans. Thus the conditions can be represented as a finite list of equations

$$\mathsf{f}\ {n}_{1} = {b}_{1}\ \ \ \ \ldots \ \ \ \ \mathsf{f}\ {n}_{k} = {b}_{k}$$

where \({n}_{1},\ldots,{n}_{k}\) are distinct natural numbers and \({b}_{1},\ldots,{b}_{k}\) Booleans. The domain dom(p) of this condition p is the finite set \({n}_{1},\ldots,{n}_{k}\). We write q ≤ p if the condition q extends the condition p. One can think of a condition p as a compact open subset C p of Cantor space C, which is the space of functions from natural numbers to the discrete space of Booleans, with the product topology. A condition p represents also some finite amount of information about a generic element of Cantor space. If p and q are compatible conditions, we can consider pq = qp, by taking the union of the conditions p and q. We clearly have C q  ⊆ C p if q ≤ p and C pq  = C p  ∩ C q if p and q are compatible. Any condition p can be considered to be the product of elementary conditions f n = b. If n is not in the domain of p then the two conditions p(f n = 0) and p(f n = 1) form an elementary partition of p. By iterating this construction, we obtain the general notion of partition \({p}_{1},\ldots,{p}_{l}\) of a condition p (this includes as well the trivial partition p of p.) In general a non trivial partition p i ,  i ∈ I of p is built from one partition p i ,  i ∈ I 0 of p(f l = 0) and one partition p i ,  i ∈ I 1 of p(f l = 1) for some l not in the domain of p (Fig.10.1).

2.4 Generic Function

We extend the syntax of terms with a new function symbol f. To each condition p we associate the reduction relation →  p which extends β, ι reduction with the rule \(\mathsf{f}\ \overline{n} {\rightarrow }_{p}b\) whenever f n = b is in p. This extension still satisfies the Church-Rosser property, by the usual Martin-Löf/Tait argument (as presented for instance in Martin-Löf 1998). We define then t =  p u to mean that t and u have a common reduct for →  p .

Fig. 10.1
figure 1

An example of condition

Full size image

3 Computational Interpretation of Forcing

3.1 Operational Semantics

In ordinary type theory, the computation is described by a rewriting relation t → t′ between terms. Here the computation deals with a pair pt of a condition p (which can be thought as a state) and a term t. Furthermore the computation (process) may open during the computation independent computations, and the computation step is a relation pt → α between pt and a formal sum α = Σp i t i where \({p}_{1},\ldots,{p}_{n}\) is a partition of p. The definition is the following.

$$\frac{pt \rightarrow \Sigma {p}_{i}{t}_{i}} {p(t\ u) \rightarrow \Sigma {p}_{i}({t}_{i}\ u)}\qquad \frac{} {p((\lambda x.t)\ u) \rightarrow pt[x/u]}$$
$$\frac{} {p(\mathsf{boolrec}({t}_{0},{t}_{1})\ 0) \rightarrow p{t}_{0}}\quad \frac{} {p(\mathsf{boolrec}({t}_{0},{t}_{1})\ 1) \rightarrow p{t}_{1}}$$
$$\frac{} {p(\mathsf{natrec}({t}_{0},{t}_{1})\ 0) \rightarrow p{t}_{0}}\quad \frac{} {p(\mathsf{natrec}({t}_{0},{t}_{1})\ S(t)) \rightarrow p({t}_{1}\ t\ (\mathsf{natrec}({t}_{0},{t}_{1})\ t))}\quad$$
$$\frac{pt \rightarrow \Sigma {p}_{i}{t}_{i}} {p(\mathsf{natrec}({t}_{0},{t}_{1})\ t) \rightarrow \Sigma {p}_{i}(\mathsf{natrec}({t}_{0},{t}_{1})\ {t}_{i})}$$
$$\frac{pt \rightarrow \Sigma {p}_{i}{t}_{i}} {p(\mathsf{boolrec}({t}_{0},{t}_{1})\ t) \rightarrow \Sigma {p}_{i}(\mathsf{boolrec}({t}_{0},{t}_{1})\ {t}_{i})}$$

The remaining crucial rules are that \(p(\mathsf{f}\ \overline{k}) \rightarrow pb\) if f k = b is in p and otherwise \(p(\mathsf{f}\ \overline{k}) \rightarrow {p}_{0}0 + {p}_{1}1\) with p i  = p(f k = i). Finally, we have p(f S n(t)) → Σp i (f S n(t i )) whenever pt → Σp i t i .

We can then define the computation of the normal form (for ground types):

$$\frac{} {p0 \Rightarrow p0}\quad \frac{} {p1 \Rightarrow p1}\quad \frac{pt \Rightarrow \Sigma {p}_{i}\overline{{k}_{i}}} {pS(t) \Rightarrow \Sigma {p}_{i}\overline{1 + {k}_{1}}}\quad \frac{pt \rightarrow \Sigma {p}_{i}{t}_{i}\ \ \ \ \ {p}_{i}{t}_{i} \Rightarrow {\alpha }_{i}} {pt \Rightarrow \Sigma {\alpha }_{i}} \quad$$

Lemma 10.1.

If pt → Σp i t i or pt ⇒ Σp i t i then (p i ) is a partition of p and \(t {\rightarrow }_{{p}_{i}}^{{_\ast}}{t}_{i}\).

If α = Σp i t i is a formal sum, with (p i ) partition of p, and q ≤ p we can define qα = Σ(qp i )t i where we limit the sum to the p i compatible with q.

Lemma 10.2.

If pt → α and q ≤ p then qt → qα. If pt ⇒ α and q ≤ p then qt ⇒ qα.

3.2 Computability Predicate

We define p ⊩ φ N (t) inductively

  • p ⊩ φ N (0)

  • p ⊩ φ N (S(t)) if p ⊩ φ N (t)

  • p ⊩ φ N (t) if pt → Σp i t i with p i  ⊩ φ N (t i ) for all i

This is equivalent to the fact that we have a relation \(t \Rightarrow \Sigma {p}_{i}\overline{{k}_{i}}\). Similarly \(p \Vdash {\varphi }_{{N}_{2}}(t)\) is defined by the clauses

  • \(p \Vdash {\varphi }_{{N}_{2}}(0)\)

  • \(p \Vdash {\varphi }_{{N}_{2}}(1)\)

  • \(p \Vdash {\varphi }_{{N}_{2}}(t)\) if pt → Σp i t i with \({p}_{i} \Vdash {\varphi }_{{N}_{2}}({t}_{i})\) for all i

and this is equivalent to the fact that pt ⇒ Σp i v i with v i  = 0 or v i  = 1 for all i. Finally, p ⊩ φ A → B (t) means that q ≤ p and q ⊩ φ A (u) implies q ⊩ φ B (t u).

p ⊩ φ A (t) can be read as “p forces that t is computable at type A”. In the case A = N or A = N 2 this means that we have pt ⇒ α for some α, i.e. that the computation of pt terminates.

Lemma 10.3.

If p ⊩ φ A (t) and q ≤ p then q ⊩ φ A (t).

Proof.

This is direct if A is a function type and follows from Lemma 10.2 in the case A = N or A = N 2.

Lemma 10.4.

If pt → Σp i t i and p i ⊩ φ A (t i ) for all i then p ⊩ φ A (t).

Proof.

This is clear if A = N or A = N 2. If A = A 1 → A 2 and pt → Σp i t i and p i  ⊩ φ A (t i ) for all i and if q ≤ p then we have qt → Σ(qp i )t i by Lemma 10.2. If \(q \Vdash {\varphi }_{{A}_{1}}(u)\) we have q(t u) → Σ(qp i )(t i  u) and \(q{p}_{i} \Vdash {\varphi }_{{A}_{2}}({t}_{i}\ u)\). By induction we have \(q \Vdash {\varphi }_{{A}_{2}}(t\ u)\) as desired.

Lemma 10.5.

If p ⊩ φ A (t 0 ) and p ⊩ φ N→A→A (t 1 ) then p ⊩ φ N→A ( natrec(t0,t1)). Similarly, if p ⊩ φA(t0) and p ⊩ φA(t1) then \(p \Vdash {\varphi }_{{N}_{2}\rightarrow A}(\mathsf{boolrec}({t}_{0},{t}_{1}))\).

Proof.

This follows from Lemma 10.4.

Lemma 10.6.

The generic function is computable, i.e. \(p \Vdash {\varphi }_{N\rightarrow {N}_{2}}(\mathsf{f})\) for all p.

Proof.

We assume p ⊩ φ N (t) and we prove \(p \Vdash {\varphi }_{{N}_{2}}(\mathsf{f}\ t)\). We have \(pt \Rightarrow \Sigma {p}_{i}\overline{{k}_{i}}\) and, using Lemma 10.4, we are reduced to prove that \(p \Vdash {\varphi }_{{N}_{2}}(\mathsf{f}\ \overline{k})\), which is direct, by case if k is in the domain of p or not.

Theorem 10.1.

If \({x}_{1}:{A}_{1},\ldots,{x}_{n}:{A}_{n} \vdash t:A\) and \(p \Vdash {\varphi }_{{A}_{1}}({t}_{1}),\ldots,p \Vdash {\varphi }_{{A}_{n}}({t}_{n})\) then we have \(p \Vdash {\varphi }_{A}(t[{x}_{1}/{t}_{1},\ldots,{x}_{n}/{t}_{n}])\) . In particular, if ⊢ t:A then p ⊩ φ A (t) for all p.

Proof.

By induction on the proof of \({x}_{1}:{A}_{1},\ldots,{x}_{n}:{A}_{n} \vdash t:A\) using Lemmas 10.5 and 10.6.

If we have ⊢ F : C → N 2 it is possible to use this result and compute a modulus of uniform continuity for F as follows. Using Theorem 10.1 and Lemma 10.6, we have \(\Vdash {\varphi }_{{N}_{2}}(F\ h)\). Hence we have F h ⇒ Σp i v i with v i  = 0 or v i  = 1 for all i, and p i is a partition of Cantor space. By Lemma 10.1, we have \(F\ h {\rightarrow }_{{p}_{i}}^{{_\ast}}{v}_{i}\). We can see the modulus of continuity of F as the greatest k such that a condition of the form f k = b appears in one of the p i .

3.3 Baire Space

Our argument can be adapted to the case of Baire space N → N instead of Cantor space. The generic function f is now of type N → N and an elementary condition is of the form f n = m, where n and m are natural numbers. The partitions are not finite objects anymore but well-founded trees. The inductive definition of partition is the following: the condition p itself is a (trivial) partition of p, and if n is not in the domain of p, and for each m we have a partition P m of p(f n = m), then the union of all P m is a partition of p. Similarly the formal sums Σp i t i are now indexed by well-founded trees: we have the formal sum pt over p, and if n is not in the domain of p, and for each m we have a formal sum σ m over p(f n = m), then the formal sum Σ m σ m is a formal sum over p. The operational semantics have the same rules, except that \(p(\mathsf{f}\ \overline{k}) \rightarrow p\overline{l}\) if f k = l is in p and \(p(\mathsf{f}\ \overline{k}) \rightarrow \Sigma {p}_{n}\overline{n}\) with p n  = p(f k = n) otherwise. Whenever ⊢ F : (N → N) → N it is possible in this way to associate to F a well-founded tree (a bar on Baire space) with natural numbers at each leaves, by computing F f. This gives a strong form of the continuity of definable functionals on Baire space.Footnote 1

4 Conclusion

In the reference (Goodman 1978), Goodman compares recursive realizability and Kripke/Beth models as follows. Recursive realizability “emphasizes the active aspect of constructive mathematics\(\ldots \) However, Kleene’s notion has the weakness that it disregards that aspect of constructive mathematics which concern epistemological change\(\ldots \). Precisely that aspect of constructive mathematics which Kleene’s notion neglects is emphasized by Kripke’s semantics for intuitionistic logic\(\ldots \). However, Kripke’s notion makes it appear that the constructive mathematician is a passive observer of a structure which gradually reveals itself. What is lacking is the emphasis on the mathematician as active which Kleene’s notion provides.” He then presents a combination of realizability and Kripke semantics. We think that our work illustrates these remarks in a simple and concrete framework. Usual computation rules in type theory, with a rewriting relation on terms, don’t involve “epistemological change”. In our framework, the condition p represents a state of knowledge. While in usual Kripke/Beth semantics, these states of knowledge are independent of the computations, they are here needed in the computation, and the computation may create new states of knowledge.

5 A.1 Appendix 1: Representation in Haskell

The operational semantics given in the previous section has a natural representation in the programming language Haskell, using the notion of monad (Wadler 1992). Written in this way, the program is quite close to an ordinary evaluation program for Gödel system T by head reduction. The monad we use is a composition of the list monad (for nondeterminism) and of the state monad (Wadler 1992).

6 A.2 Appendix 2: Quantification on Cantor Space

6.1 A.2.1 New Conditions

We explain how one can use this operational interpretation of forcing to give a new computational interpretation of an universal quantification ∀: (C → N 2) → N 2 on Cantor space. There are already computational interpretations (Escardo 2007; Simpson 1998), using a general recursive program.Footnote 2 The interpretation we suggest relies on iterating the previous construction and introducing infinitely generic functions \({\mathsf{f}}_{0},{\mathsf{f}}_{1},\ldots \) It is reminiscent of iterated forcing in set theory, and of the interpretation of choice sequences in intuitionism (Troelstra and van Dalen 1988).

The first step is to extend the notion of condition. So far, a condition p represents a compact open subset of Cantor space. We can in the same way consider conditions \(r,s,\ldots \) which represent compact open subsets of the product space \({C}^{\mathbb{N}}\). The elementary conditions are now of the form f l  k = i, given an information about the generic function f l , and a condition r is a finite product of compatible elementary conditions. The set of conditions P is the union of the sets P n of condition containing only f l  k = i with l < n. The conditions we need \(p,q,\ldots \) are pairs p = (r, n), with r in P n . Such a condition represents a compact open subset X of C n. We define (s, m) ≤ (r, n) to mean n ≤ m and s ≤ r. To summarize, each condition p = (r, n) represents a finite amount of information about a finite number of generic functions, and to refine this condition we can either add new informations, or add a new generic function. (Intuitively, the conditions represent compact open subsets of a “variable” space.)

The reduction relations pt → α,  pt ⇒ α are as before, with p = (n, r), and t a term which may contain \({\mathsf{f}}_{0},\ldots,{\mathsf{f}}_{n-1}\) and α is now a formal sum Σp i t i where p i  = (n, r i ) and (r i ) is a partition of r.

6.2 A.2.2 Universal Quantification as Projection

An element r of P n represents a compact open subset X of C n. A formal sum of Booleans α = Σp i v i with p i  = (n, r i ) and r i partition of r represents a continuous function f α from X to the discrete space N 2.

We define the conjunction operation on formal sums of Booleans α ∧ β as

$$(\Sigma {p}_{i}{v}_{i}) \wedge (\Sigma {q}_{j}{w}_{j}) = \Sigma {p}_{i}{q}_{j}({v}_{i} \wedge {w}_{j})$$

in such a way that we have f α ∧ β = f α ∧ f β.

If r is a condition in P n + 1, we can write r = r′s with r′ in P n and s a product of conditions of the form f n  k = i. The condition (n + 1, r) can thus be thought as representing a product X ×Y, with X ⊆ C n corresponding to the condition (n, r′) and Y corresponding to s. If we consider a partition (r i ) of r in P n + 1, the formal sum α = Σp i v i , with p i  = (n + 1, r i ) represents a continuous function f α : X ×Y → N 2. We are going to define the formal sum p(α) = Σ(n, s j )w j which represents the function f p(α) : X → N 2 such that f p(α)(x) = 1 iff f α(x, y) = 1 for all y in Y.

This definition is by induction on the fact that (r i ) is a partition of r. If (r i ) is the unit partition then we take p((n + 1, r)v) = (n, r′)v. If it is a partition formed of a partition (r i ,  i ∈ I 0) of r(f l  k = 0) and a partition (r i ,  i ∈ I 1) of r(f l  k = 1), we can consider by induction

$${\beta }_{0} = \mathsf{p}({\Sigma }_{i\in {I}_{0}}{p}_{i}{v}_{i})\ \ \ \ \ \ {\beta }_{1} = \mathsf{p}({\Sigma }_{i\in {I}_{1}}{p}_{i}{v}_{i})$$

If l = n, we define p(α) = β0 ∧ β1 and if l < n, we define p(α) = β0 + β1.

6.3 A.2.3 Computation Rules

The only new reduction rule is the following

$$\frac{(n + 1,r)(F\ {\mathsf{f}}_{n}) \Rightarrow \alpha } {(n,r)(\forall \ F) \rightarrow \mathsf{p}(\alpha )}$$

The intuition is that we want to compute \(\forall \ F\) and we know that F mentions only the generic functions \({\mathsf{f}}_{0},\ \ldots,\ {\mathsf{f}}_{n-1}\), satisfying the condition r. We compute then F f n , where f n is “fresh” for F, and from the result of this computation we can compute \(\forall \ F\) using the function p.

The computability relation p ⊩ φ A (t) is defined as before, for p = (n, r) and t a term which may contain \({\mathsf{f}}_{0},\ldots,{\mathsf{f}}_{n-1}\).

Lemma 10.7.

All constant f l are computable, i.e. (n,1) ⊩ φC(f l ) if l < n. The constant \(\forall \) is computable, i.e. \(\Vdash {\varphi }_{C\rightarrow {N}_{2}}(\forall )\) .

Proof.

The proof that f l is computable is the same as the proof of Lemma 10.6.

If we have \((n,r) \Vdash {\varphi }_{C\rightarrow {N}_{2}}(F)\) we show that \((n,r) \Vdash {\varphi }_{{N}_{2}}(\forall \ F)\). For this it is enough to show that \((n + 1,r) \Vdash {\varphi }_{{N}_{2}}(F\ {\mathsf{f}}_{n})\), which follows from \((n,r) \Vdash {\varphi }_{C\rightarrow {N}_{2}}(F)\) and (n + 1, r) ⊩ φ C (f n ).