User:IssaRice/Computability and logic/Decrement command in loop programs

(started typing this up as a question for math SE, but I think I got it)

Herbert Enderton’s Computability Theory: An Introduction to Recursion Theory defines a loop program as one made up of the following commands:

The clear command ${\textstyle X_{n}\leftarrow 0}$ that sets the value of the variable ${\textstyle X_{n}}$ to zero.
The increment command ${\textstyle X_{n}\leftarrow X_{n}+1}$ that increases the value of ${\textstyle X_{n}}$ by one.
The copy command ${\textstyle X_{n}\leftarrow X_{m}}$ that sets the value of ${\textstyle X_{n}}$ to that of ${\textstyle X_{m}}$ and leaves the value of ${\textstyle X_{m}}$ unchanged.
The loop command ${\textstyle {\text{loop}}\ X_{n};{\mathcal {P}};{\text{endloop}}\ X_{n}}$ that takes a program ${\textstyle {\mathcal {P}}}$ and executes it ${\textstyle X_{n}}$ times. Here the value of ${\textstyle X_{n}}$ may be changed inside the loop, but this will not affect the number of times ${\textstyle {\mathcal {P}}}$ is executed. (This ensures the overall program always terminates, assuming ${\textstyle {\mathcal {P}}}$ does.)

The output of a program is always stored in ${\textstyle X_{0}}$ . A function ${\textstyle f\colon \mathbb {N} ^{k}\to \mathbb {N} }$ is loop-computable if there is a loop program such that for every ${\textstyle x\in \mathbb {N} ^{k}}$ the program started with ${\textstyle (X_{1},\ldots ,X_{k})=x}$ (and zero in all the other variables) halts with ${\textstyle f(x)}$ in ${\textstyle X_{0}}$ .

The book then states (without proof, as far as I can tell) that a function taking values in ${\textstyle \mathbb {N} }$ is loop-computable if and only if it is primitive recursive.

I am confused that the above definition of a loop program does not have a decrement command. When I look at other definitions I see that they have a decrement command.

I have noticed that I can implement a decrement program given if-else conditionals, as follows:

loop X₁
    if counter != 0
        X₀ ← X₀ + 1
    endif
    counter ← counter + 1
endloop X₁

$n\neq 0\iff n\geq 1$ , so we just need a program that checks if the input is at least 1:

loop X₁
     X₀ ← 1
endloop X₁

If the input is at least 1, the program enters the loop, setting $X_{0}$ to one each time, resulting in 1 as the final output. If the input is 0, the loop is skipped ("loop zero times") and we return the default value of 0.

Now we need to figure out how to write a general conditional program like:

if condition:
    A
else:
    B

We can do this as follows:

X₂ ← χ(condition)
X₃ ← χ(¬condition)
loop X₂
    A
endloop X₂
loop X₃
    B
endloop X₃

Python code:

def at_least_one(x):
    result = 0
    for _ in range(x):
        result = 1
    return result

def decrement(n):
    result = 0
    counter = 0
    for _ in range(n):
        for _ in range(at_least_one(counter)):
            result += 1
        counter += 1
    return result