ϵ">]>
Literature.
[1] J. Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
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.
Substitution.
Auxiliary operations.
One-step reduction. (3 points)
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. (1 point) Find a well-formed recursive index of the addition function x+y .
Exercise. Find a well-formed recursive index of the modified subtraction function x -. y .
Exercise. Find a well-formed recursive index of the multiplication function x⋅y .
Exercise. (2 points) Find a well-formed recursive index of the exponentiation function xy .