It happens that there do exist non-trivial *universal* properties that are decidable. An example of such a property is expressed in terms of what we could call ``primitive recursive Kolmogorov complexity''.

**Definition.**
If $v=(v_0,\ldots,v_{n-1})$ is a sequence of natural numbers then let $K_{pr}(v)$ be the size of a shortest LOOP program computing a function $f$ extending $v$, i.e. satisfying $f(0)=v_0,\ldots,f(n-1)=v_{n-1}$.

Unlike the usual notions of Kolmogorov complexity, $K_{pr}$ is computable. However it is not primitive recursive.

For a function $f$, let $f|n$ be the finite sequence $(f(0),\ldots,f(n-1))$.

**Claim.** The property $$\forall n, K_{pr}(f|n)\leq n$$ is decidable, given a LOOP program for $f$.

*Proof.* Given a loop program $p$ for $f$, one has $K_{pr}(f|n)\leq |p|$ for all $n$. In order to check the property, one can only look at $n<|p|$. As $K_{pr}$ is computable, the property is decidable.

Observe that the property is not decidable if one is only given $f$ as oracle, as no finite prefix of $f$ is sufficient to ensure the property: for each finite sequence $v=(v_0,\ldots,v_{n-1})$ there is $v_n$ such that $K_{pr}(v_0,\ldots,v_n)>n+1$ hence no extension of $(v_0,\ldots,v_n)$ satisfies the property (the property is a closed subset of the Baire space that has empty interior).

More generally and for the same reasons, if $h:\mathbb{N}\to\mathbb{N}$ is a computable non-decreasing unbounded function then the property $P_h$ defined by
$$f\in P_h\iff\forall n, K_{pr}(f|n)\leq h(n)$$
is decidable given a LOOP program for $f$ but not given $f$ as oracle. If $h(1)$ is sufficiently large then $P_h$ is non-empty as it contains all the functions computed by LOOP programs of size $\leq h(1)$.

## An analog of Rice and Rice-Shapiro theorem.

So far, we know some basic properties that are decidable: extending a finite sequence $v$ (decidable given $f$), the property $P_h$ of having $h$-compressible prefixes (decidable given a LOOP program). Now, there is an analog of Rice and Rice-Shapiro theorems, stating that they form a ``subbasis'' (as in topology) of the semi-decidable properties: every semi-decidable property can be obtained as a union of finite intersections of these simple properties.

**Theorem.** Let $P$ be a property of primitive recursive function. The following are equivalent:

- $f\in P$ is semi-decidable given a LOOP program for $f$,
- $P$ is a computable disjunction of properties of the form
$$
f\text{ extends $v$ and }\forall n, K_{pr}(f|n)\leq h(n).
$$

The result is more general as it applies to any class of total computable functions that can be computably enumerated (for instance the polynomial-time computable functions, the provably total computable functions, etc.). All this can be found in the paper http://arxiv.org/abs/1503.05025.