Recursive Language🔗ℹ

1.1 Import🔗ℹ

To make it clear what constructs and functions are used as a basis to define recursive functions, we need to explicitly import them with the import statement:

import <construct-1>, <construct-2>, ..., <construct-n>;

Following are core constructs:

• z and s functions (zero constant function and successor function, with arity 1)

• id_<place>^<arity> where <place> and <arity> are natural numbers (identity/projection functions, with arity <arity>)

• Cn[<f>, <g-1>, ..., <g-m>] (composition)

• Pr[<f>, <g>] (primitive recursion)

• Mn[<f>] (minimization)

Furthermore, following derived functions (presented in the book) are also provided for convenience.

• const_<n> where <n> is a natural number (constant function, with arity 1)

• sum and prod (addition and multiplication, with arity 2)

• pred (predecessor function, with arity 1)

• monus (subtraction on natural numbers, with arity 2)

• sgn and ~sgn (zero predicate and its negated form, with arity 1)

1.2 Definition🔗ℹ

We can define recursive functions using = where the LHS is an identifier name and the RHS is an expression that builds a recursive function. For example:

sum = Pr[id_1^1, Cn[s, id_3^3]];

prod = Pr[z, Cn[sum, id_1^3, id_3^3]];

defines sum to be the (primitive) recursive function Pr[id_1^1, Cn[s, id_3^3]] and prod to be the (primitive) recursive function Pr[z, Cn[sum, id_1^3, id_3^3]]

1.3 Print🔗ℹ

We can print results from function invocation by using the print statement.

print sum(10, 23);

Running the program will result in 33.

1.4 Check🔗ℹ

We can use the check construct to test that our recursive functions are correct on given inputs. For example:

check sum(10, 23) = 33;

checks that sum(10, 23) should have the result 33.

1.5 Comment🔗ℹ

Comment can be written by using # ....