Higher-Order Computability

Let $C$ and $D$ be computability models with types indexed by $T, U$ respectively. A simulation $\gamma$ of $C$ in $D$ (denotes $C \triangleright D$ ) consists of

a mapping associating each type $\tau \in T$ a representing type $\gamma \tau \in U$ ;
for each $\tau \in T$ , a relation $\Vdash^\gamma_\tau$ between elements of $D(\gamma \tau)$ and those of $C(\tau)$ .

subject to the following conditions

For each $\tau \in T$ and each $a \in C(\tau)$ , there is some $a' \in D(\gamma\tau)$ such that $a' \Vdash^\gamma_\tau a$ .
Every operation $f \in C[\sigma, \tau]$ is tracked by some $f' \in D[\gamma\sigma, \gamma\tau]$ , i.e. if $f(a)$ is defined and $a' \Vdash^\gamma_\tau a$ , then $f'(a')$ is defined and $f'(a') \Vdash^\gamma_\tau f(a)$ .

Example $T_1$ and $T_2$ [local-0]

See models of Turing machine.

By definition of $T_2$ , a simulation $T_2 \triangleright T_1$ is given. If $n \in \N$ and $m$ is a memory state, we take

m \Vdash n

iff $m$ represents $n$ in the sense we have defined. Every operation in $T_2$ is tracked by one in $T_1$ .

We cannot have a simulation $T_1 \triangleright T_2$ , because there are uncountably many memory states. But there is a simulation for variant of $T_1$ , by restricting $T_1$ 's memory states to those with a designated blank symbol in all but finitely many cells. Such memory states can be coded as natural numbers, and the action of any Turing machine may then be emulated by a partial computable function $\N \rightharpoonup \N$ . We thus obtain a simulation $T_1^\text{fin} \triangleright T_2$ .

Definition. Simulation of computability models [math-QAL6]

Example T1T_1T1​ and T2T_2T2​ [local-0]

Example $T_1$ and $T_2$ [local-0]