Primitive recursive function: Difference between revisions

Revision as of 23:28, 6 July 2025

Revision as of 09:34, 30 July 2025

Line 117:

===Truncated subtraction===

The limited subtraction function (also called "[[monus]]", and denoted "<math>\stackrel.mathbin{\dot{-}}</math>") is definable from the predecessor function. It satisfies the equations

:<math>\begin{array}{rcll}

y \stackrel.mathbin{\dot{-}} 0 & = & y & \text{and} \\

y \stackrel.mathbin{\dot{-}} S(x) & = & Pred(y \stackrel.mathbin{\dot{-}} x) & . \\

\end{array}</math>

Since the recursion runs over the second argument, we begin with a primitive recursive definition of the reversed subtraction, <math>RSub(y,x) = x \stackrel.mathbin{\dot{-}} y</math>. Its recursion then runs over the first argument, so its primitive recursive definition can be obtained, similar to addition, as <math>RSub = \rho(P_1^1, Pred \circ P_2^3)</math>. To get rid of the reversed argument order, then define <math>Sub = RSub \circ (P_2^2,P_1^2)</math>. As a computation example,

:<math>\begin{array}{lll}

& Sub(8,1) \\

Line 147:

=== Predicate "Less or equal" ===

Using the property <math>x \leq y \iff x \stackrel.mathbin{\dot{-}} y = 0</math>, the 2-ary function <math>Leq</math> can be defined by <math>Leq = IsZero \circ Sub</math>. Then <math>Leq(x,y) = 1</math> if <math>x \leq y</math>, and <math>Leq(x,y) = 0</math>, otherwise. As a computation example,

:<math>\begin{array}{lll}

& Leq(8,3) \\