Recursive Language🔗ℹ

A language for writing recursively computable functions (or simply recursive functions), which are functions in recursion theory that consume natural numbers and produce a natural number. See Chapter 6 of Computability and Logic (George Boolos, John P. Burgess, and Richard Jeffrey) for details.

1 Language Features🔗ℹ

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 # ....

2 Example🔗ℹ

#lang recursive-language

import Pr, Cn, s, id, z, const;

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

print sum(2, 23); # should be 25

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

print prod(3, 3); # should be 9

fact =

Cn[Pr[const_1, Cn[prod, Cn[s, id_2^3], id_3^3]],

id_1^1, id_1^1];

print fact(fact(3)); # should be 720

print fact(Cn[s, s](4)); # should be 720

check fact(3) = 6;

3 Acknowledgments🔗ℹ

Thanks to Matthias Felleisen for giving me advice on Racket macrology back in 2018.