Definition. Kleene's first model [math-SVXS]

2024-07-20 · Lîm Tsú-thuàn
Higher-Order Computability

Kleene's first model K1\mathcal{K}_1 is a computability model consists of

  • the single datatype N\N
  • operations are Turing computable partial functions N⇀N\N \rightharpoonup \N

The model has standard products, the computable operation

⟨m,n⟩=(m+n)(m+n+1)/2+m\langle m,n \rangle = (m+n)(m+n+1)/2 + m

defines a bijection N×N→N\N \times \N \to \N and satisfied weak product. Any element i∈Ni \in \N may serve as a weak terminal, because Λn.i\Lambda n. i is computable.

weakly cartesian closed structure [local-2]

Here N⇒N\N \Rightarrow \N can only be N\N, so need a suitable operation ⋅:N×N→N\cdot : \N \times \N \to \N. Let T0,T1,…T_0, T_1, \dots be some chosen enumeration of all Turing machines for computing partial functions N⇀N\N \rightharpoonup \N, then there is a Turing machine that accepts two inputs e,ae, a and returns the result of applying the machine TeT_e to the single input aa.

representable of f:N×N⇀Nf : \N \times \N \rightharpoonup \N [local-1]

The partial functions f:N×N⇀Nf : \N \times \N \rightharpoonup \N representable within the model via the standard product operations are just the partial computable ones. We may also see that these coincide exactly with those represented by some total computable f~:N→N\tilde{f} : \N \to \N, in the sense that f(c,a)≃f~(c)⋅af(c,a) \simeq \tilde{f}(c) \cdot a for all c,a∈Nc,a \in \N.

Proof [local-0]

One half of this is immediate: given a computable f~\tilde{f} the operation Λ(c,a).f~(c)⋅a\Lambda(c,a). \tilde{f}(c) \cdot a is computable. The other half is precisely the content of Kleene's s-m-n from basic computability theory: for any Turing machine TT accepting two arguments, there is a machine T′T' accepting one argument such that for each cc, T′(c)T'(c) is an index for a machine computing T(c,a)T(c,a) from aa.