6
$\begingroup$

The “second Kleene algebra” $\mathcal{K}_2$ is defined, e.g. here on nLab, or in section 1.4.3 of van Oosten's book Realizability: an Introduction to its Categorical Side (2008), or as example 3.4 of the notes “Realizability” by Thomas Streicher (2017–2018), or (implicitly) in ¶1.9.12 of Troelstra's Metamathematical Investigations of Intuitionistic Arithmetic and Analysis (1973), or in various other places. Let me reproduce the essential part of the definition for readers' convenience:

Let $\mathcal{B} = \mathbb{N}^{\mathbb{N}}$ denote Baire space, endowed with its usual product topology. Given $\alpha \in \mathcal{B}$, define $F_\alpha$ a partial function from $\mathcal{B}$ to $\mathbb{N}$ by $$ F_\alpha(\beta) = n\quad\text{iff}\quad\exists k\in\mathbb{N}.(\alpha(\bar\beta\upharpoonright k)=n+1 \land \forall \ell<k.(\alpha(\bar\beta\upharpoonright k)=0)) $$ (undefined if no such $n$ exists) where $\bar\beta \upharpoonright k$ denotes an integer encoding the finite sequence $\langle\beta(0),\ldots,\beta(k-1)\rangle$. This defines a continuous function $U \to \mathbb{N}$ with $U \subseteq \mathcal{B}$ open, and any such function is of the form in question.

Now let $$ \alpha\bullet\beta = (n \mapsto F_\alpha(\langle n\rangle \smallfrown \beta)) $$ provided $F_\alpha(\langle n\rangle \smallfrown \beta)$ is defined for every $n$, undefined otherwise, where $\langle n\rangle \smallfrown \beta$ denotes the function $0 \mapsto n$ and $k+1 \mapsto \beta(k)$. Then $\mathcal{K}_2$ is $\mathcal{B}$ endowed with this partial operation $\bullet$.

This definition is not complicated, but it is… extremely opaque, and none of the sources I've cited bother to explain why we define things in this particular way ($F_\alpha(\beta)$ searches for the first nonzero value among the values returned by $\alpha$ on the finite subsequences of $\beta$ and subtracts one to it: why do we want to do precisely this? rather than, say, return the index $k$ where this nonzero value was found), apart from the fact that “it works” (it gives a partial combinatory algebra).

Kleene's first algebra $\mathcal{K}_1$ (namely $\mathbb{N}$ with the operation $e\bullet n = \varphi_e(n)$ for some standard enumeration $\varphi$ of partial recursive functions) is easy to develop an intuition for: it's the set of computable functions, i.e., computer programs, and the operation is that of taking data and feeding it to a computer program. I understand that the idea behind $\mathcal{K}_2$ is to do something similar for continuous functions on Baire space (and that $F_\alpha$ must play a role analogous to $\varphi_e$), but this doesn't really help me explain the particulars of the definition above (I feel like if in the case of $\mathcal{K}_1$ I'd been described what a Turing machine was without any explanation as to how this definition was reached). So:

Question: What's the intuition behind the definition of $\mathcal{K}_2$ and the reason for this particular choice of definition? Has anyone written an introduction to $\mathcal{K}_2$ analogous to what a first course on computability theory would be on $\mathcal{K}_1$?

$\endgroup$
1
  • $\begingroup$ A fairly paedagogical explanation is found in Andrej Bauer's notes on realizability, in the chapter titled “models of computation”, esp. the subsection “type-2 machines”. $\endgroup$
    – Gro-Tsen
    Commented Jun 16, 2023 at 13:45

3 Answers 3

7
$\begingroup$

There's a bit of explanation in my lecture notes on intuitionistic logic, in particular the section on function realizability.

The idea is that you want to encode continuous partial functions $\mathbb{N}^\mathbb{N} \to \mathbb{N}^\mathbb{N}$ as elements of $\mathbb{N}^\mathbb{N}$ analogously to how computable partial functions $\mathbb{N} \to \mathbb{N}$ can be encoded as elements of $\mathbb{N}$. It turns out the main idea comes up just encoding partial continuous functions $\mathbb{N}^\mathbb{N} \to \mathbb{N}$, so I'll talk about that.

It's easiest to break it into two steps. Write $\mathbb{N}^{< \omega}$ for finite sequences of numbers. Then given a function $f : \mathbb{N}^{< \omega} \to \mathbb{N} + \{\bot\}$, we can view it as a continuous partial function $F : \mathbb{N}^\mathbb{N} \to \mathbb{N}$ as follows. To compute $F(g)$ we feed finite approximations of $g$, e.g. the length $k$ approximation $[g(0), g(1), g(2), \ldots, g(k)]$. $f([g(0), g(1), g(2), \ldots, g(k)])$ can either lie in the $\mathbb{N}$ component of $\mathbb{N} + \{\bot\}$ or it's equal to $\bot$. The former tells us that we can compute the value of $F(g)$ from this list, and it is equal to $f([g(0), \ldots, g(k)])$ (unless it was already computed at an earlier stage). The latter, $f([g(0), \ldots, g(k)]) = \bot$, tells us $f$ has not been given enough information and needs a longer list before it can return a value.

Finally note that $\mathbb{N}^{< \omega}$ and $\mathbb{N} + \{\bot\}$ are both countable, so we can view $f$ as a function $\mathbb{N} \to \mathbb{N}$. In particular checking for a number $> 0$ and then subtracting $1$ comes from the bijection $\mathbb{N} + \{\bot\} \cong \mathbb{N}$.

$\endgroup$
2
$\begingroup$

Here is an equivalent definition. A realizer is a type-2 turing machine, except that instead of having finitely many states there are $\aleph_0$ many states. This means that the instruction table must be infinite as well.

Given some reasonable encoding function $e$ that encodes such a machine into an infinite string, we define $e(M) \bullet \alpha$ as the result of running $M$ when $\alpha$ is on the input tape.

Here are the required combinators. They are the encoding of these machines:

  • $k \bullet \alpha$: The initial state is $0$. When in state $n$, it writes $\alpha(n)$ to the output tape, moves the output head right, and then goes to state $n+1$. The symbol on the input tape is ignored.
  • $k$: Writes $e(k \bullet \alpha)$ as described in the previous point to the output tape, where $\alpha$ is on the input tape.
  • $(s \bullet \alpha) \bullet \beta$: Does the following three steps in parallel by dovetailing
    1. Run the machine encoded by $\alpha$, routing the output to an unused subset of the working tape.
    2. Run the machine encoded by $\beta$, routing the output to an unused subset of the working tape.
    3. Run the machine encoded by the result of step 1, but using the result of step 2 in place of the original input tape. If the machine is missing a needed instruction, pause until step 1 produces it. If the machine tries to move the simulated input head to a cell that step 2 has not produced yet, pause until step 2 does so.
  • $s \bullet \alpha$: Writes $e((s \bullet \alpha) \bullet \beta)$ as described in the previous point to output, where $\beta$ is on the input tape.
  • $s$: Writes $e(s \bullet \alpha)$ as described in the previous point to output, where $\alpha$ is on the input tape.

The last four machines exist via the Church-Turing thesis.

$\endgroup$
2
$\begingroup$

I'm adding an answer to my own question to point out one thing about Kleene's $\mathcal{K}_2$ which I had previously failed to understand and which is an important difference with $\mathcal{K}_1$ that probably deserves its own special caveat in any description of $\mathcal{K}_2$: in $\mathcal{K}_1$ one can “run programs in parallel”, but apparently one cannot do this in $\mathcal{K}_2$.

That is, $\mathcal{K}_1$ has the property that given $e_1,e_2$ (in $\mathcal{K}_1$, that is to say, $\mathbb{N}$) there exists $e$ such that that $e\bullet n$ is defined iff either $e_1\bullet n$ or $e_2\bullet n$ is defined, and moreover, when this is the case, $e\bullet n$ equals one of the values $e_1\bullet n$ or $e_2\bullet n$ which is defined (so, the one which is defined if only one is defined). Furthermore, we can find such $e$ effectively from $e_1,e_2$ (meaning that there is a $p$ such that $(p\bullet e_1)\bullet e_2$ gives such an $e$ as I wrote). Indeed, we do this by running $e_1$ and $e_2$ in parallel until one produces a result, and returning the result in question (this is a consequence of Kleene's normal form theorem).

This property, however, does not hold for $\mathcal{K}_2$: while it is true that ① given $\varepsilon_1,\varepsilon_2$ (in $\mathcal{K}_2$, that is to say, $\mathbb{N}^{\mathbb{N}}$) there exists $\varepsilon$ such that that $\varepsilon\bullet \nu$ is defined iff either $\varepsilon_1\bullet \nu$ or $\varepsilon_2\bullet \nu$ is defined, however we cannot ② add the condition that, $\varepsilon\bullet \nu$ equals one of the values $\varepsilon_1\bullet \nu$ or $\varepsilon_2\bullet \nu$ which is defined, not even if we assume that $\varepsilon_1\bullet \nu$ and $\varepsilon_2\bullet \nu$ are never simultaneously defined.

Indeed, this is obvious topologically: as explained in Andrej Bauer's notes on realizability, theorem 2.1.14, the partial maps $\mathbb{N}^{\mathbb{N}} \dashrightarrow \mathbb{N}^{\mathbb{N}}$ of the form $\nu \mapsto \varepsilon\bullet\nu$ are precisely the continuous maps on a $G_\delta$ domain. Now $G_\delta$ sets are closed under finite union, so this shows ①; however, given two continuous functions on disjoint $G_\delta$ sets there does not necessarily exist one which extends them on the union (disproving ②). Indeed, a trivial counterexample is given by the partial function $F_1\colon \mathbb{N}^{\mathbb{N}} \dashrightarrow \mathbb{N}^{\mathbb{N}}$ taking the constant function with value $0$ at the constant function with value $0$ and undefined elsewhere, and the partial function $F_2\colon \mathbb{N}^{\mathbb{N}} \dashrightarrow \mathbb{N}^{\mathbb{N}}$ taking the constant function with value $1$ everywhere except at the constant function with value $0$ and undefined there. Clearly $F_1$ and $F_2$ are continuous and each defined on a $G_\delta$, but the unique function $F$ extending them to the union of their domains, i.e. to $\mathbb{N}^{\mathbb{N}}$, is not continuous, so not realized by an element of $\mathcal{K}_2^{\mathrm{eff}}$. Moreover, each of $F_1$ and $F_2$ belong to the effective part of $\mathcal{K}_2$ (the one realized by Turing-computable functions in $\mathbb{N}^{\mathbb{N}}$), so this defect(?) of $\mathcal{K}_2$ caries over to $\mathcal{K}_2^{\mathrm{eff}}$.

The difficulty arises from the way we move from functions $\mathbb{N}^{\mathbb{N}} \dashrightarrow \mathbb{N}$ to functions $\mathbb{N}^{\mathbb{N}} \dashrightarrow \mathbb{N}^{\mathbb{N}}$. The former have no such problem: the ones described by an element of $\mathbb{N}^{\mathbb{N}}$ are precisely the continuous functions on an open domain, and we can glue such functions (feed the input function and take the first one that returns a value), but when going to $\mathbb{N}^{\mathbb{N}} \dashrightarrow \mathbb{N}$ things break apart as the previous counterexample shows.

I don't know if this should be considered a “defect” of $\mathcal{K}_2$, but I urge anyone writing a explanation of $\mathcal{K}_2$ to add a warning to the reader that this property we tend to take for granted in $\mathcal{K}_1$ does not hold for $\mathcal{K}_2$ and it's likely to confuse beginners.

$\endgroup$
1
  • 3
    $\begingroup$ A similar observation is this: in $\mathcal{K}_1$ the relation "$n \bullet m$ is defined" is semidecidable, but in $\mathcal{K}_2$ the relation "$\alpha \bullet \beta$ is defined" is a $\Pi^0_2$ statement (for every output cell there are initial segments of $\alpha$ and $\beta$ that determine its value). $\endgroup$ Commented Jan 4 at 21:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .