Clausal Language (ver. 5.81.21, by P.J. Voda, J. Komara, J. Kluka)

Literature.

Chapter. Partial Recursive Functions.

Section. Arithmetization of Computation Model.

Subsection. Arithmetization of Reductions.

Arithmetization of recursive terms and recursive function symbols. See the module Mxgr.

Monadic numerals.

⌈ \underline{x} ⌉ = ?

Dc (t) = ?

Nm (0)

Nm S (t) \leftarrow Nm (t)

Auxiliary operations.

Pn (t) = ?

Dn (t_{1}, t_{2}, t_{3}) = ?

Nms (n, ts) \leftrightarrow \forall i i ≦ n : (1 ≦ i \to Nm ({[ts]}_{i}^{n}))

Substitution.

Ar (e) = ?

t [e; rs] = ?

One-step reduction. (5 points)

Rd (t) = ?

Section. Recursive Indices.

Well-formed recursive indices. See also the binary predicate $Rf (n, e)$ holding of well-formed recursive indices in the module Mxgr.

Exercise. Find a well-formed recursive index of the addition function $x + y$ .

Plus = λ_{2} . D (x_{1}, S (f_{2} (⟨ P (x_{1}), x_{2} ⟩)), x_{2})

Exercise. (1 point) Find a well-formed recursive index of the modified subtraction function $x \dot{-} y$ .

Minus = ?

Exercise. Find a well-formed recursive index of the multiplication function $x \cdot y$ .

Times = ?

Exercise. (2 points) Find a well-formed recursive index of the exponentiation function $x^{y}$ .

Exp = ?