# A Library for Peano Arithmetic¶

We hope the reader will learn the following techniques from this lesson:

Advanced injection functions Defining injection functions for value constructors of variant types, using the Fmap family of module functors

`Fmap`

,`Fmap2`

,`Fmap3`

, etc., which are provided by the module Logic.Reification and Reifiers Defining reifiers to convert data from the injected level to the logic level, again with help from the Fmap family of module functors.

Overwriting the show Function Overwriting, or redefining the “show” function for values of a logic type, to allow for more concise and human readable printing of them.

Relations on Peano Numbers Defining (possibly recursive) relations, e.g., comparison, addition and division on Peano numbers.

Scrutinizing Relations Making queries to relations using combinations of unknown arguments.

Analyzing the search behaviour Analyzing why a query returns certain answers.

Modifying the search behaviour Reordering the conjuncts within the body of a relation definition to modify the way in which the relation searches for answers in a given query.

The trick of generate and test Programming a relation so that answers to certain queries are found by brute-force.

The formula parser Observing that the implementation of the

`ocanren {}`

quotation takes care of the precedence, associativity and scope of the logic connectives, and replaces constructors of variant types by injection function names, and primitive values by their injected versions.Building a library Writing and testing a library in OCanren.

The techniques are presented in detail in sections below, to which the
labels ( **T.1**, **T.2**, etc) are linked. Each section is
self-contained and could be read independent of other sections.

The library has a systematic test file, which can be compiled (and linked) and executed by running the following shell commands in (your local copy of) the lesson directory:

```
make && ./peano.opt
```

A copy of the result of the test is answers.txt that
is obtained using the shell command `./peano.opt > answers.txt`

.

## Advanced Injection Functions¶

The primary injection operator is `!!`

which is used to cast primitive
values (such as characters and strings) and constant constructors of
variant types (particularly whose type constructors do not have a type
parameter) from the ground level to the injected level. For those
variant types whose type constructors have one or more type parameters,
the primitive injection operator is inadequate. We use instead *advanced
injection functions* to build injected values, which are defined using
distribution functions provided by the Fmap family of module functors
together with the injection helper `inj`

, all from the module Logic.
In our Peano Arithmetic library implementation, the
following block of code defines advanced injection functions `o`

and
`s`

for the abstract Peano number type `Ty.t`

, which correspond
respectively to the value constructors `O`

and `S`

:

```
module Ty = struct
@type 'a t = O | S of 'a with show, gmap
let fmap = fun f d -> GT.gmap(t) f d
end;;
include Ty
module F = Fmap(Ty)
let o () = inj @@ F.distrib O
let s n = inj @@ F.distrib (S n)
```

The general workflow of defining advanced injection functions is as follows:

We begin with a variant type whose type constructor

`t`

has one or more type parameters. This is always an OCanren abstract type, such as the abstract Peano number type or the abstract list type.We count the number of type parameters of the type constructor in order to choose the suitable module functor from the Fmap family: for one type parameter, use

`Fmap`

; for two type parameters, use`Fmap2`

; three type parameters,`Fmap3`

and so on.We request the

`gmap`

plugin for the type constructor, and use it to define a function named`fmap`

simply by renaming.We put the definitions of the type constructor

`t`

and the`fmap`

function in one module, and suppy that module as a parameter to the chosen Fmap family module functor. The result is a module`F`

with three functions one of which is`distrib`

, the distribution function.For each value constructor of the type

`t`

, we define a function whose name is the same as the value constructor except that the initial letter is set to lower case. For example,`Cons`

,`S`

and`NUL`

become respectively`cons`

,`s`

and`nUL`

.

For each value constructor

`Constr0`

of no argument, define:let constr0 = fun () -> Logic.inj @@ F.distrib Constr0

For each value constructor

`Constr1`

of one argument, define:let constr1 = fun x -> Logic.inj @@ F.distrib (Constr1 x)

For each value constructor

`Constru`

of*u*(> 1) arguments, define:let constru = fun x1 ... xu -> Logic.inj @@ F.distrib @@ Constru (x1, ..., xu)

In the definition of a typical advanced injection function, the value constructor takes arguments which are at the injected level, and the combination of

`inj`

and`distrib`

serves to inject the top level value while preserving the structure of constructor application. If we explain by a schematic where a pair of enclosing square brackets`[]`

signifies the injected status of the enclosed data, we would say that:An advanced injection function

`constr`

converts a value of the form`Constr ([arg1], ..., [argn])`

to a value of the form`[Constr (arg1, ..., argn)]`

. In other words,The injection function

`constr`

takes arguments`[arg1], ..., [argn]`

and builds a value of the form`[Constr (arg1, ..., argn)]`

.

We advise the reader to find in the interface of the Logic module the Fmap module functor family and the functors’ argument types (which are module types): that would provide a more formal explanation of what advanced injection functions do and why they are defined in the given manner.

## Reification and Reifiers¶

Say we have a logic variable `x`

and a substitution
`[(x, Lam(z,y)); (y, App(a,b))]`

that associates `x`

with the term
`Lam(z,y)`

and `y`

with `App(a,b)`

where `y, z`

are also logic
variables. We would like to know what `x`

is with respect to the
substitution. It is straightforward to replace `x`

by `Lam(z,y)`

but
since `y`

is associated with `App(a,b)`

we can further replace `y`

in `Lam(z,y)`

, and finally we get the term `Lam(z,App(a,b))`

.
Although there is still an unbound part `z`

, we have no further
information about how `z`

might be instantiated, so we leave it there.
What we have done is called *reification* of the logic variable `x`

:
we instantiate it as much as possible, but allowing unbound logic
variables to occur in the result. A *reifier* is a function that reifies
logic variables.

We know that there are primary and advanced injection functions.
Similarly there are primary and advanced reifiers: the primary reifier
`Logic.reify`

reifies logic variables over base types (like character
and string) and simple variant types (i.e., those that have only
constant constructors). Advanced reifiers are for logic variables over
variant types whose type constructors have one or more type parameters
and there exist non-constant (value) constructors. The Peano Arithmetic
library defines an advanced reifier for the Peano number type:

```
let rec reify = fun env n -> F.reify reify env n;;
```

Advanced reifiers are defined using the Fmap module functor family. The
correct Fmap module functor for defining the reifier for a type is the
same as that selected for defining advanced injection functions for the
same type. The result of applying the correct Fmap module functor is a
module that provides, besides a distribution function, a reifier builder
named `reify`

, e.g., `F.reify`

in the case of our library. Note
there is an abuse of names: the name `reify`

has been used for both
reifiers and reifier builders. If a type constructor takes other types
are parameters, then the reifier for the top level type is built from
reifiers for the parameter types: we build “larger” reifiers from
“smaller” reifiers. The Peano number reifier is recursive because the
Peano number type is recursive: the reader should refer to the
signature of
`F.reify`

and see how the types of the reifier and the reifier builder
fit together.

## Overwriting the *show* Function¶

The default *show* function for a variant type converts values of that
type to strings in a straightforward way, e.g., a logic Peano number
representation of the integer 1 would be converted to the string
`"Value(S(Value O))"`

whilst “the successor of some unknown number”
could be `"Value(S(Var(1,[])))"`

. These are not too readable.

The Logic module has already
redefined the
*show* function for the type `Logic.logic`

so that the above values
would instead be converted to strings `"S(O)"`

and `"S(_.1)"`

respectively, omitting the verbose constructors `Value`

and `Var`

and displaying variables in the form `_.n`

where `n`

is the first
parameter of the constructor `Var`

. The redefinition happens within
the record value `logic`

which has a field `GT.plugins`

. This record
value origins from the `@type`

definition of the type constructor
`Logic.logic`

and is auto-generated by the GT package. The field
`GT.plugins`

is an object with several methods, one of which is
`show`

: other plugins (or methods) keep their default meanings but
`show`

is redefined.

However, when there are too many repetitions of the constructor `S`

,
the *show* function as redefined in the Logic module is no longer
suitable. Our Peano Arithmetic library therefore offers a further
customized redefinition just for displaying logic
Peano numbers, converting those values without free variables directly
to Arabic numbers and those with free variables a sum between an Arabic
number and the symbol `n`

.

In like manner, the reader may: - Redefine the *show* function to behave
in other ways, or - Redefine other plugins by modifying the
`GT.plugins`

field, or - Redefine plugins for other types.

Some additional remarks on the last point: the `@type`

definition of a
type constructor `typeconstr-name`

generates a record value also named
`typeconstr-name`

of the type `GT.t`

. This could be viewed by adding
the `-i`

option as indicated in the Makefile:

```
BFLAGS = -rectypes -g -i
```

See also the GT source.

## Relations on Peano Numbers¶

This section teaches the reader how to read and write relation definitions.

The reader is already familiar with reading and writing functions in OCaml. To read a function, just look at the type annotation (if any) to determine what are the input types and what is the output type, and then inspect the function body to see how the inputs are processed to produce the output. To write a function, first decide the type of the function, and then design the internal procedure that produces the output from the input.

In OCanren, a relation is a function only at the language implementation
level, and as users our experience with functions do not transfer well
when it comes to reading and writing relations. That’s why relational
programming claims the status of being a unique programming paradigm
distinct from imperative programming and functional programming. Working
with relations requires learning a new way of thinking: *declarative*
thinking.

Relation definitions are declarative, meaning that it first of all states a proposition. The emphasize is on “what” rather than “how”. It is the language implementation that takes care of “how”, but the user of the language should foucs on “what”. For example, look at the addition relation:

```
let rec add a b c =
ocanren{ a == O & b == c
| fresh n, m in
a == S n & c == S m & add n b m}
```

It says nothing about how to compute the sum `c`

of two numbers `a`

and `b`

, instead it only says what conditions must be satisfied so
that the addition relation exists among the three numbers `a`

, `b`

and `c`

— if `a`

equals `O`

and `b`

equals `c`

, or, if `a`

equals `S n`

and `c`

equals `S m`

and the numbers `n,b,m`

also
satisfy the addition relation, for some `n,m`

. No other way is given
in which we can establish the addition relation among three numbers.

Another example is the “less than” relation:

```
let rec lt a b =
ocanren{ fresh n in
b == S n &
{ a == O
| fresh n' in
a == S n'
& lt n' n }}
```

It says that `a`

is less than `b`

if there exist `n`

, such that
`b`

equals `S n`

, and either `a`

equals `O`

or there exist
`n'`

such that `a`

equals `S n'`

and `n'`

is less than `n`

.

Other relations in the library shall be read in this way, and they are
all written with the declarative reading in mind. The reader is
encouraged to write a relation for subtraction: `sub a b c`

iff
`a - b = c`

, or, put in another way: iff `b`

is `O`

and `a`

is
`c`

, or `b`

is `S n`

and `a`

is `S n'`

and `sub n' n c`

.

## Scrutinizing Relations¶

Taking the “less than” relation as an example, we can ask questions like:

Is zero less than one ? Is one less than two ? Is one less than zero ? Is two less than one?

What is less than five ? Five is less than what ?

What is less than what ?

The first set of questions above is for *checking*: we provide concrete
numbers and ask if they satisfy the relation. The remaining two sets of
questions are for *searching*: looking for numbers that satisfy the
relation. Note that the questions are organized: there coud be no
unknown, one unknown or two unknowns, and each argument position of the
relation might be an unknown. In general, for a relation of N arguments,
the total number of kinds of questions we can ask is ( R is the number
of unknowns in NCR):

NC0 + NC1 + NC2 + … + NCN-1 + NCN

Running the test shows that OCanren answers all the questions well. For example, the goal:

```
fun q -> ocanren { lt O (S O) & lt (S O) (S(S O)) }
```

asks about what is `q`

so that zero is less than one and one is less
than two, and the answer is just a free variable `n`

meaning that `q`

could be any
number and the relation always holds between the given numbers. The
similar goal:

```
fun q -> ocanren { lt (S O) O | lt (S(S O)) (S O) }
```

asks about what is `q`

so that one is less than zero or two is less
than one. There is no answer, meaning that there is no `q`

to make the
relation hold between the given numbers.

The goal below asks what is less than five:

```
fun q -> ocanren { lt q (S(S(S(S(S O))))) }
```

For this goal the answers `0,1,2,3,4`

are found, which is quite
satisfactory.

The relations `lte, add, div, gcd`

are also questioned systematically
in the test file.

Note that the addition relation can perform subtraction, and the division relation can do multiplication. For instance, the goal below asks “What adds 4 equals to 7 ?” and whose answer is “3”:

```
fun q -> ocanren { add q (S(S(S(S O)))) (S(S(S(S(S(S(S O))))))) }
```

This amounts to performing the subtraction `7 - 4`

. The next goal asks
“What divided by 5 equals 3 with remainder 0 ?” and the answer is “15”:

```
fun q -> ocanren { div q (S(S(S(S(S O))))) (S(S(S O))) O }
```

It amounts to the multiplication `3 * 5`

.

## Analyzing the Search Behaviour¶

When asking the `lt`

relation “what is less than 5” using the goal:

```
fun q -> ocanren { lt q (S(S(S(S(S O))))) } (G.1)
```

OCanren returns 0,1,2,3,4. Let’s see why. It really is a matter of
definition: we defined `lt a b`

to be a certain formula `(Eq.1)`

and
now we substitute 5 for `b`

in the formula `lt a b`

followed by
several steps of simplification then we get a formula `(Eq.12)`

that
literally says `a`

shall be 0, 1, 2, 3 or 4. Below are the details.

We reproduce the definition of `lt`

in the followinig simplified form:

```
lt a b = fresh n in b == S n
& { a == O | fresh n' in a == S n' & lt n' n }
(Eq.1)
```

Now replace `b`

by `(S(S(S(S(S O)))))`

in `(Eq.1)`

, we get:

```
lt a (S(S(S(S(S O))))) = fresh n in (S(S(S(S(S O))))) == S n
& { a == O | fresh n' in a == S n' & lt n' n }
(Eq.2)
```

Replace `(S(S(S(S(S O))))) == S n`

by `(S(S(S(S O)))) == n`

in
`(Eq.2)`

, we get:

```
lt a (S(S(S(S(S O))))) = fresh n in (S(S(S(S O)))) == n
& { a == O | fresh n' in a == S n' & lt n' n }
(Eq.3)
```

In `(Eq.3)`

, remove `fresh n in (S(S(S(S O)))) == n`

, then replace
all free occurences of `n`

by `(S(S(S(S O))))`

. The top level `&`

and the braces are no longer needed, so also being removed. We get:

```
lt a (S(S(S(S(S O))))) = a == O
| fresh n' in a == S n'
& lt n' (S(S(S(S O)))) (Eq.4)
```

From `(Eq.1)`

to `(Eq.4)`

what we have done is to provide a concrete
value (the Peano number 5) as the second argument of `lt`

and use the
result of unification to simplify the equation. The recursive call of
`lt`

in the right hand side of `(Eq.4)`

can be treated similarly: we
provide a concrete value (the Peano number 4) as the second argument of
`lt`

`(Eq.5)`

and use the result of unification to simplify the
equation `(Eq.6)`

, which is then used to substitute for the recursive
call of `lt`

in `(Eq.4)`

, as follows.

Replace `b`

by `(S(S(S(S O))))`

and`a`

by `n'`

in `(Eq.1)`

in a capture-avoiding manner, we get:

```
lt n' (S(S(S(S O)))) = fresh n in (S(S(S(S O)))) == S n
& { n' == O | fresh n'' in n' == S n'' & lt n'' n }
(Eq.5)
```

Using the result of unification we can simplify `(Eq.5)`

into:

```
lt n' (S(S(S(S O)))) = n' == O
| fresh n'' in n' == S n''
& lt n'' (S(S(S O))) (Eq.6)
```

Now in `(Eq.4)`

replace `lt n' (S(S(S(S O))))`

by the right hand
side of `(Eq.6)`

:

```
lt a (S(S(S(S(S O))))) = a == O
| fresh n' in a == S n'
& { n' == O
| fresh n'' in n' == S n''
& lt n'' (S(S(S O))) } (Eq.7)
```

The right hand side of `(Eq.7)`

produces another value of `a`

which
is `S O`

, as follows. In `(Eq.7)`

, distribute `a == S n'`

we get:

```
lt a (S(S(S(S(S O))))) = a == O
| fresh n' in
a == S n' & n' == O
| a == S n' & fresh n'' in n' == S n'' & lt n'' (S(S(S O)))
(Eq.8)
```

Replace `a == S n' & n' == O`

by `a == S O`

in `(Eq.8)`

, we get:

```
lt a (S(S(S(S(S O))))) = a == O
| fresh n' in
a == S O
| a == S n' & fresh n'' in n' == S n'' & lt n'' (S(S(S O)))
(Eq.9)
```

In the right hand side of `(Eq.9)`

move `a == S O`

out of the scope
of the `fresh n' in`

, we have:

```
lt a (S(S(S(S(S O))))) = a == O
| a == S O
| fresh n' in
a == S n' & fresh n'' in n' == S n'' & lt n'' (S(S(S O)))
(Eq.10)
```

From `(Eq.1)`

to `(Eq.10)`

are steps of substitution, unification
and simplification. Recursive calls are expanded and then reduced, and
the initial formula `lt a (S(S(S(S(S O)))))`

is gradually unfolded so
that values of `a`

are revealed one by one. Continue this way, the
last but one equation would be:

```
lt a (S(S(S(S(S O))))) = a == O
| a == S O
| a == S (S O)
| a == S (S (S O))
| a == S (S (S (S O)))
| fresh n' in a == S n'
& fresh n'' in n' == S n''
& fresh n''' in n'' == S n'''
& fresh n'''' in n''' == S n''''
& fresh n''''' in n'''' == S n''''' & lt n''''' O
(Eq.11)
```

Note that `lt n''''' O`

expands to `fresh n in O == S n & ...`

which
is false, therefore the last equation is:

```
lt a (S(S(S(S(S O))))) = a == O
| a == S O
| a == S (S O)
| a == S (S (S O))
| a == S (S (S (S O))) (Eq.12)
```

From `(Eq.12)`

we read off the answers to the query.

The derivation from `(Eq.1)`

to `(Eq.12)`

, combined with the
operational semantics of OCanren in terms of stream manipulation,
explains why we get the answer that `a`

equals 0,1,2,3 or 4 from the
goal `(G.1)`

.

The reader may take an exercise to show that one plus one equals two by
simplifying the formula `add (S O) (S O) c`

.

## Modifying the Search Behaviour¶

We compare two versions of the *simplify* relation, differing from each
other only by a swap of conjuncts.

Both versions share the logic that the simplest form of `a/b`

is
`a'/b'`

where `a'`

(`b'`

) is `a`

(resp. `b`

) divided by the
greatest common divisor of `a`

and `b`

, provided `b`

is non-zero.
There is a short cut for the case where `a`

is zero, then `b'`

is
set to one directly.

The difference is that:

In one version we say, “a (b) divided by c equals a’ (resp. b’), and c is the gcd of a and b.”

In the other version we say, “c is the gcd of a and b, and a (b) divided by c equals a' (resp. b').”

In OCanren:

```
let simplify a b a' b' =
ocanren { fresh n in
b == S n &
{ a == O & a' == O & b' == S O
| fresh c, m in
a == S m
& div a c a' O (* div first, then gcd *)
& div b c b' O
& gcd a b c } }
let simplify' a b a' b' =
ocanren { fresh n in
b == S n &
{ a == O & a' == O & b' == S O
| fresh c, m in
a == S m
& gcd a b c (* gcd first, then div *)
& div a c a' O
& div b c b' O } }
```

The test file offers a comparison of these two
versions over their forward and backward search behaviours. By *forward
search* we mean that given a ratio *a/b* find its simplest form, e.g.,
18/12 is simplified to 3/2. By *backward search* we mean given a ratio
in the simplest form, find its equal ratios, e.g., 3/2 could be
simplified from 6/4, 9/6, 12/8, etc. The test shows that both versions
work well for forward search, but when it comes to backward search,
`simplify`

returns answers quickly but `simplify'`

took ages without
returning anything.

The ordering of the conjuncts, together with the state of the logic varaibles and the search behaviour of the sub-relations, results in apparently different operational meaning of the conjunctions in backward search, as follows:

*Variant 1*

div a c a’ O & div b c b’ O & gcd a b cFind a and c such that

`a`

divided by c equals a' exactly. Then find`b`

such that`b`

divided by c equals b' exactly. Now check that the gcd of a and b is c.Before the execution of the first conjunct, both a and c are unknowns. When the second conjunct is to be executed, c has already been found by the first conjunct, and only b is the unknown. Right before the execution of the thrid conjunct, all a,b,c have been found so only a check is due.

This analysis requires knowledge of the search behaviour of div arg1 arg2 arg3 arg4 in the following two cases:

Both arg1, arg2 are unknowns, but arg3, arg4 are known.

Only arg1 is unknown, the other three are known.

*Variant 2*

gcd a b c & div a c a’ O & div b c b’ OFind three unknowns`a,b,c` such that the relation gcd a b c holds, then check that a (b) is exactly dividable by c with quotient a’ (resp. b’).

Before the first conjunct is executed, all a,b,c are unknown, but by the time the second and third conjuncts are to be executed, the variables a,b,c are already computed by the first conjunct, therefore the last two conjuncts merely check the result.

This analysis requires knowledge of the search behaviour of gcd when provided with three free logic variables for its three arguments.

The relevant search behaviours of the sub-relations mentioned in the
table can be observed by running the test file or found in
answers.txt. For instance, to know the search
behaviour of `div`

when only its first and second argument are
unknown, we can make the specific query:

```
printf "\n What divided by what equals 3 with remainder 2 ? (give %d answers) \n\n" ans_no;
ocrun2 ~n:ans_no (fun q r -> ocanren { div q r (S(S(S O))) (S(S O)) })
```

The answers are:

```
What divided by what equals 3 with remainder 2 ? (give 20 answers)
(11, 3)
(14, 4)
(17, 5)
(20, 6)
(23, 7)
(26, 8)
(29, 9)
(32, 10)
(35, 11)
(38, 12)
(41, 13)
(44, 14)
(47, 15)
(50, 16)
(53, 17)
(56, 18)
(59, 19)
(62, 20)
(65, 21)
(68, 22)
```

We could see that the `div`

relation is enumerating all possible
divisors in ascending order, starting with the least possible divisor
which is 3 (the divisor must be greater than the remainder 2), together
with the corresponding dividends.

In backward search, therefore, the `simplify`

relation first finds a
`c`

-multiple of `a'`

for some `c`

, and then finds a
`c`

-multiple
of `b'`

for the same `c`

. Its check of the gcd relation as the last
step is starighforward if `a'/b'`

is already in the simplest form.
Note that the programmer provides `a'`

and `b'`

so practically
`a'/b'`

does not have to be in the simplest form, in which case the
`gcd`

check would fail. This all sounds like logical manners to find
integral multiples of a ratio that is in the simplest form. However, the
way in which `simplify'`

approaches the problem is firstly guessing an
arbitrary ratio together with the gcd of the numerator and the
denominator, and then it checks if the ratio happens to reduce to
`a'/b'`

. This obviously has a bad chance to hit the target. That’s why
`simplify`

works better than `simplify'`

for backward search, and
they only differ by a swap of conjuncts.

Note worthy is that the advantage of `simplify`

over `simplify'`

in
backward search is at the cost of some efficiency in forward search,
where `simplify'`

smartly finds the gcd of the numerator and the
denominator first and then divides to get the result, but `simplify`

enumerates through all divisors of `a`

to find the one that is also a
divisor of `b`

and the gcd of `a,b`

— less efficient but still
acceptable for small numbers.

As an exercise, the reader could experiment with reordering the
conjuncts so that `gcd`

is placed in between the two `div`

’s.
How
would forward and backward search be influenced? A second question: what
will happen and why, if we use `simplify`

to find `a`

and `b`

, but
give `a'`

and `b'`

as 4 and 2 respectively, i.e., a ratio not in the
simplest form?

## The Trick of Generate-and-test¶

When using the `gcd`

relation to answer the question: “What and what
have gcd 7 ?”, the distribution of the answers
does not look balanced: the second number is 7 most of the time, while
the first number is growing. In comparison, the
answers given by the `gcd'`

relation has a more
satisfactory distribution: the first number increases and for each
possible first number, all possible second numbers are enumerated before
the first number is further increased. The `gcd'`

relation is defined
using the famous technique known as *generate-and-test*, which we
explain now.

Browsing the library source we could see that
`gcd'`

is defined in terms of `gcd`

together with the addition
relation and the Peano number predicate `isp`

(read “is P” or “is a
Peano Number”).

Provided a free variable as the argument, `isp`

enumerates all Peano
numbers, in other words, we can obtain the following equation from the
definition of `isp`

, where the right hand side is an infinite formula:

```
isp n = n == O | n == S O | n == S (S O) | n == S (S (S O)) | ...
```

Therefore, `isp`

could be a Peano number *generator* .

Moreover, when the third argument of `add`

is concrete but the first
and second argument are free variables, the `add`

relation can find
all ways to break up the third argument into two addends.

The sequence of `isp`

and `add`

in the body of `gcd'`

can then be
a Peano number pair generator, enumerating all possible pairs of Peano
numbers (in the same way Georg Cantor shows that the set of rational
numbers is enumerable). Now the way `gcd'`

works is clear: it
enumerates through (i.e., *generates*) all possible pairs and then
*tests* which pairs have the gcd 7. Since the pairs are generated
systematically , the final answers are organized in the way we saw.

Another example of generate-and-test is the `simplify a b a' b'`

relation. When `a,b`

are given but `a',b'`

are left unknown, the
first ``div` <peano.ml#L91>`__ generates all possible divisor-quotient
pairs for `a`

, and for each such pair the second
``div` <peano.ml#L92>`__ tests if the divisor also divides `b`

and if
so generates the quotient. The sequence of two `div`

’s then plays
the role of a generator of all common divisors of `a,b`

together with
the corresponding pairs of numbers which are `a,b`

divided by their
common divisors. The ``gcd`

sub-relation peano.ml#L93 finally
checks for the greatest common divisor, and the corresponding pair of
quotients is the answer for `a',b'`

.

In summary, generate-and-test is both a technique that the programmer
applies to solve certain problems (e.g., the `gcd'`

case), and a usual
way in which relational programs search for answers even if the
programmer does not intentionally apply it (e.g., the `simplify`

case).

## The Formula Parser¶

In the library implementation and the test file, we often see formulae
enclosed by the `ocanren{}`

quotation which takes care of, among
others, precedence and associativity of the logic connectives. It is an
OCanren-specific syntax extension which is described
OCanren-specific Camlp5 syntax extension

## Building a Library¶

Being essentially an OCaml library, an OCanren library shall have its
interface `.mli`

and implementation `.ml`

. The interface typically
contains type definitions (at the four levels), auxiliaries (such as
injection functions, reifiers, etc.) and the relations. Note also the
`@type`

syntax in the interface.

Relations shall be systematically tested. This means all possible
combinations of unknown arguments shall be queried wrt. each relation.
The benefits of such systematic test includes reducing surprises when
running the programs, and helping with debugging “bigger” relations that
are defined using smaller relations. For example, understanding the
search behaviour of `simplify`

requires knowledge of search behaviours
of `div`

and `gcd`

and in turn those of `lt`

, `lte`

and `add`

.