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
thas 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, useFmap2; three type parameters,Fmap3and so on.We request the
gmapplugin for the type constructor, and use it to define a function namedfmapsimply by renaming.We put the definitions of the type constructor
tand thefmapfunction in one module, and suppy that module as a parameter to the chosen Fmap family module functor. The result is a moduleFwith three functions one of which isdistrib, 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,SandNULbecome respectivelycons,sandnUL.
For each value constructor
Constr0of no argument, define:let constr0 = fun () -> Logic.inj @@ F.distrib Constr0
For each value constructor
Constr1of one argument, define:let constr1 = fun x -> Logic.inj @@ F.distrib (Constr1 x)
For each value constructor
Construof 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
injanddistribserves 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
constrconverts a value of the formConstr ([arg1], ..., [argn])to a value of the form[Constr (arg1, ..., argn)]. In other words,The injection function
constrtakes 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)))) anda 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
adivided by c equals a' exactly. Then findbsuch thatbdivided 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.