Recursive Language
1 Language Features
1.1 Import
1.2 Definition
1.3 Print
1.4 Check
1.5 Comment
2 Example
3 Acknowledgments
8.17.0.6

Recursive Language🔗ℹ

Sorawee Porncharoenwase <sorawee.pwase@gmail.com>

 #lang recursive-language package: 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.