Intuition behind Kleene's “second algebra” $\mathcal{K}_2$ 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 \text{ \; iff \; }\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$?
 A: 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}$.
