Computability in higher types, P and the completeness of type assignment

applicative structure completeness theorem for type checking continuous functions effectively given domain formal type assignment to terms of \(\lambda \)-calculus Kleene-Kreisel countable functionals recursive functionals recursive operators at higher types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Higher-type and set recursion theory (03D65)

Review text

P\(\omega\), the powerset of the natural numbers, may be turned into an applicative structure by Myhill and Shepherdson, ``\(\cdot \). Then, for A, \(B\subseteq P\omega\), set \(A\to B=\{d\in P\omega | \forall a\in A\), da\(\in B\}\). Any effectively given domain can be embedded into \(P\omega\) by a continuous and computable retraction (notation: \(X\triangleleft_ cA_ X\), for some \(A_ X\subseteq P\omega\), which is also an effectively given domain). We first prove that if \(X\triangleleft_ cA_ X\) and \(Y\triangleleft_ cA_ Y\), then also \(A_ X\to A_ Y\) is an effectively given domain and (*): \(Cont(X,Y)\triangleleft_ cA_ X\to A_ Y\), i.e., the continuous functions can be embedded into \(A_ X\to A_ Y.\) Let now \(P\subseteq P\omega\) be the collection of single-valued sets, i.e., P is isomorphic to the effectively given domain of the partial functions on \(\omega\), and let T be the function-type symbols, with (1)\(\in T\). Then, for \(P^{(1)}=P\), \(P^{\sigma \to \tau}=P^{\sigma}\to P^{\tau}\) extends the classical recursive operators at higher types. By (*), Ershov's model of the Kleene-Kreisel countable functionals can effectively be embedded, by some \(G_{\sigma}'s\), into the type structure \(\{P^{\sigma}\}_{\sigma \in T}\) in \(P\omega\). Thus, the recursive functionals correspond to the r.e. sets in the due types, for example, f has type \(\sigma\to \tau\) iff \(G_{\sigma \to \tau}(f)\) is an r.e. set in \(P^{\sigma}\to P^{\tau}.\) \(\{\) \(P^{\sigma}\}_{\sigma \in T}\) clearly yields a model for formal type assignment to terms of \(\lambda\)-calculus, i.e., for any assignment B of types to variables and any \(\sigma\in T\) one has \(B\vdash \sigma M\Rightarrow M_{\xi_ B}\in P^{\sigma}\), where \(\xi_ B:Var\to P\omega\), according to B. We prove that also the reverse implication holds for typable terms. Thus, a completeness theorem for type checking is established over a model defined by an independent recursion-theoretical motivation.

Recommendations

Cites work

Cited in

(9)

Describes a project that uses

Uses Software

ML

This page was built for publication: Computability in higher types, P\(\omega\) and the completeness of type assignment

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q579245)