Table of Contents

1  Example of building, and using Tiny-Prolog-in-OCaml
1.1  Building prolog
1.2  Examples
1.3  First example
1.4  Second example
1.5  Other examples
1.5.1  The odd predicate
1.5.2  Some family history
1.6  Conclusion

Example of building, and using Tiny-Prolog-in-OCaml

In [4]:
LANG=en
bash --version

GNU bash, version 4.4.12(1)-release (x86_64-pc-linux-gnu)
Copyright (C) 2016 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>

This is free software; you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Building prolog

In [10]:
# cd ~/publis/Tiny-Prolog-in-OCaml.git/
In [8]:
ls prolog/

Makefile  README.md  lib.ml  prolog*  prolog.ml  resolution.ml
In [9]:
cd prolog/

Vous quittez le dossier '/home/lilian/publis/Tiny-Prolog-in-OCaml.git'.
	Direction ==> prolog/

Let's build prolog, it's really easy:

In [11]:
/usr/bin/make clean
/usr/bin/make

rm -f *.cm[iox] *~ *.annot *.o
ocamlc -pp camlp4o -c lib.ml
ocamlc on -pp camlp4o -c lib.ml
ocamlc lib.cmo -c resolution.ml
ocamlc on lib.cmo -c resolution.ml
File "resolution.ml", line 104, characters 12-17:
Warning 52: Code should not depend on the actual values of
this constructor's arguments. They are only for information
and may change in future versions. (See manual section 8.5)
ocamlc -o prolog lib.cmo resolution.cmo prolog.ml
ocamlc on -o prolog lib.cmo resolution.cmo prolog.ml

The binary prolog that was just generated is an OCaml binary. Ii is not native, but we don't care. If you want a native binary, just do this:

In [12]:
/usr/bin/make prolog.opt

ocamlopt -pp camlp4o -c lib.ml
ocamlopt on -pp camlp4o -c lib.ml
ocamlopt lib.cmx -c resolution.ml
ocamlopt on lib.cmx -c resolution.ml
File "resolution.ml", line 104, characters 12-17:
Warning 52: Code should not depend on the actual values of
this constructor's arguments. They are only for information
and may change in future versions. (See manual section 8.5)
ocamlopt -o prolog.opt lib.cmx resolution.cmx prolog.ml
ocamlopt on -o prolog.opt lib.cmx resolution.cmx prolog.ml
In [15]:
cd ..
ls prolog/prolog prolog/prolog.opt
file prolog/prolog prolog/prolog.opt

Vous quittez le dossier '/home/lilian/publis'.
	Direction ==> Tiny-Prolog-in-OCaml.git
prolog/prolog*  prolog/prolog.opt*
prolog/prolog:     a /home/lilian/.opam/4.04.2/bin/ocamlrun script executable (binary data)
prolog/prolog.opt: ELF 64-bit LSB shared object, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 3.2.0, BuildID[sha1]=37d475d077169be2f4b7145c2adc52cf77dfbf61, with debug_info, not stripped

Examples

There is half a dozen of examples:

In [18]:
ls -larth examples/*.pl

-rw-r--r-- 1 lilian lilian 358 Aug 28  2017 examples/family_solution.pl
-rw-r--r-- 1 lilian lilian 546 Mar 19 16:40 examples/domino.pl
-rw-rw-r-- 1 lilian lilian 109 Mar 19 16:51 examples/tomandjerry.pl
-rw-rw-r-- 1 lilian lilian 387 Mar 21 16:17 examples/family.pl
-rw-r--r-- 1 lilian lilian  36 Mar 23 10:11 examples/even.pl
-rw-r--r-- 1 lilian lilian  36 Mar 23 10:11 examples/odd.pl
-rw-r--r-- 1 lilian lilian 228 Mar 23 10:13 examples/bunny.pl
-rw-r--r-- 1 lilian lilian 691 Mar 23 10:19 examples/natural_integer_arithmetics.pl
-rw-rw-r-- 1 lilian lilian 349 Mar 23 10:37 examples/natural_integer_arithmetics_nocomment.pl

For instance, a tiny one is the following:

In [22]:
cd examples

Vous quittez le dossier '/home/lilian/publis/Tiny-Prolog-in-OCaml.git'.
	Direction ==> examples
In [23]:
cat odd.pl

odd(s(o)).
odd(s(s(X))) <-- odd(X).

First example

even.pl define the even integers.

The prolog binary accepts a request as its last argument:

In [29]:
../prolog/prolog even.pl "even(o)."  # an empty valuation: it's true!

?- even(o).
  { }
In [27]:
../prolog/prolog even.pl "even(s(o))."  # aucune théorie : c'est false !

?- even(s(o)).
In [28]:
../prolog/prolog even.pl "even(s(s(o)))."  # une théorie vide : c'est true !

?- even(s(s(o))).
  { }

And prolog can also find all the even integers! It will only display a few (15), but it could find them all.

In [28]:
../prolog/prolog even.pl "even(X)."  # it will find 15 e

?- even(s(s(o))).
  { }

Vous pouvez expérimenter dans votre terminal, en faisant simplement ../prolog/prolog pair.pl and en tapant les requêtes. Je recommande l'utilisation de rlwrap ou ledit pour faciliter l'édition (mais je peux pas montrer ça dans un notebook).

Second example

In [72]:
../prolog/prolog natural_integer_arithmetics.pl "lowerEq(s(s(o)), s(s(s(o))))."  # 2 <= 3 ? yes

?- lowerEq(s(s(o)), s(s(s(o)))).
  { }
In [73]:
../prolog/prolog natural_integer_arithmetics.pl "lowerEq(s(s(s(s(o)))), s(s(s(o))))."  # 4 <= 3 ? no

?- lowerEq(s(s(s(s(o)))), s(s(s(o)))).
In [81]:
../prolog/prolog natural_integer_arithmetics.pl "sum(o,s(o),s(o))."  # 0+1 = 1 ? yes

?- sum(o,s(o),s(o)).
  { }
In [79]:
../prolog/prolog natural_integer_arithmetics.pl "sum(s(o),s(o),s(s(o)))."  # 1+1 = 2 ? yes

?- sum(s(o),s(o),s(s(o))).
  { }
In [80]:
../prolog/prolog natural_integer_arithmetics.pl "sum(s(o),o,s(s(o)))."  # 1+1 = 1 ? no

?- sum(s(o),o,s(s(o))).

Other examples

The odd predicate

In [82]:
cat even.pl

even(o).
even(s(s(X))) <-- even(X).
In [83]:
[ -f odd.pl ] && rm -vf odd.pl
echo "odd(s(o))." > odd.pl
echo "odd(s(s(X))) <-- odd(X)." >> odd.pl
In [84]:
../prolog/prolog odd.pl "odd(o)."  # false
../prolog/prolog odd.pl "odd(s(o))."  # true
../prolog/prolog odd.pl "odd(s(s(o)))."  # false

?- odd(o).
?- odd(s(o)).
  { }
?- odd(s(s(o))).

Some family history

Note: this example does NOT use anyone from my family. The names are purely imaginary. The only thing we need to define at first is a predicate parent(X, Y) that defines the fact that X is a father/mother/parent of Y. It is a direct down link in a family tree.

In [172]:
rm -vf aSmallFamily.pl

'aSmallFamily.pl' removed
In [173]:
echo "parent(cyrill, renaud)." >> aSmallFamily.pl
echo "parent(cyrill, claire)." >> aSmallFamily.pl
echo "parent(renaud, clovis)." >> aSmallFamily.pl
echo "parent(valentin, olivier)." >> aSmallFamily.pl
echo "parent(claire, olivier)." >> aSmallFamily.pl
echo "parent(renaud, claudia)." >> aSmallFamily.pl
echo "parent(claire, gaelle)." >> aSmallFamily.pl
In [174]:
../prolog/prolog aSmallFamily.pl "parent(cyrill, renaud)."  # true
../prolog/prolog aSmallFamily.pl "parent(claire, renaud)."  # false

?- parent(cyrill, renaud).
  { }
?- parent(claire, renaud).
In [175]:
../prolog/prolog aSmallFamily.pl "parent(X, renaud)."  # cyrill
../prolog/prolog aSmallFamily.pl "parent(X, gaelle)."  # claire
../prolog/prolog aSmallFamily.pl "parent(X, olivier)."  # claire, valentin

../prolog/prolog aSmallFamily.pl "parent(renaud, X)."  # clovis, claudia
../prolog/prolog aSmallFamily.pl "parent(gaelle, X)."  # {}
../prolog/prolog aSmallFamily.pl "parent(olivier, X)."  # {}

?- parent(X, renaud).
  { X = cyrill }
?- parent(X, gaelle).
  { X = claire }
?- parent(X, olivier).
  { X = valentin }
  { X = claire }
?- parent(renaud, X).
  { X = clovis }
  { X = claudia }
?- parent(gaelle, X).
?- parent(olivier, X).

Brother and sisters are defined by having a common parent, and cousins are defined by having a common grand-parent:

In [176]:
echo "brothersister(X,Y) <-- parent(Z,X), parent(Z,Y)." >> aSmallFamily.pl
echo "grandparent(X,Y) <-- parent(X,Z), parent(Z,Y)." >> aSmallFamily.pl
echo "cousin(X,Y) <-- grandparent(Z,X), grandparent(Z,Y)." >> aSmallFamily.pl
In [177]:
../prolog/prolog aSmallFamily.pl "brothersister(cyrill, claire)."  # false
../prolog/prolog aSmallFamily.pl "brothersister(renaud, claire)."  # true
../prolog/prolog aSmallFamily.pl "brothersister(claire, claire)."  # true

../prolog/prolog aSmallFamily.pl "grandparent(X,olivier)."  # cyrill
../prolog/prolog aSmallFamily.pl "grandparent(X,gaelle)."  # cyrill

?- brothersister(cyrill, claire).
?- brothersister(renaud, claire).
  { }
?- brothersister(claire, claire).
  { }
?- grandparent(X,olivier).
  { X = cyrill }
?- grandparent(X,gaelle).
  { X = cyrill }

I will let you find a correct recursive definition of this predicate ancester.

In [178]:
#echo "ancester(X,Y) <-- ancester(X,Z), grandparent(Z,Y)." >> aSmallFamily.pl
echo "ancester(X,Y) <-- parent(X,Y)." >> aSmallFamily.pl
echo "ancester(X,Y) <-- grandparent(X,Y)." >> aSmallFamily.pl
#echo "ancester(X,X)." >> aSmallFamily.pl

On peut vérifier tous les axiomes and règles qu'on a ajouté :

In [179]:
cat aSmallFamily.pl

parent(cyrill, renaud).
parent(cyrill, claire).
parent(renaud, clovis).
parent(valentin, olivier).
parent(claire, olivier).
parent(renaud, claudia).
parent(claire, gaelle).
brothersister(X,Y) <-- parent(Z,X), parent(Z,Y).
grandparent(X,Y) <-- parent(X,Z), parent(Z,Y).
cousin(X,Y) <-- grandparent(Z,X), grandparent(Z,Y).
ancester(X,Y) <-- parent(X,Y).
ancester(X,Y) <-- grandparent(X,Y).

Questions:

  • Olivier's ancesters are Valentin, Claire and Cyrill:
In [180]:
../prolog/prolog aSmallFamily.pl "parent(X,olivier)."
../prolog/prolog aSmallFamily.pl "grandparent(X,olivier)."

?- parent(X,olivier).
  { X = valentin }
  { X = claire }
?- grandparent(X,olivier).
  { X = cyrill }
In [181]:
../prolog/prolog aSmallFamily.pl "ancester(X,olivier)."

?- ancester(X,olivier).
  { X = valentin }
  { X = claire }
  { X = cyrill }
  • The common ancester of Olivier and Renaud is Cyrill:
In [182]:
../prolog/prolog aSmallFamily.pl "ancester(olivier,X),ancester(renaud,X)."

?- ancester(olivier,X),ancester(renaud,X).
In [183]:
../prolog/prolog aSmallFamily.pl "ancester(X,olivier),ancester(X,renaud)."

?- ancester(X,olivier),ancester(X,renaud).
  { X = cyrill }
  • Claudia and Gaëlle are not sister but they are cousin:
In [149]:
../prolog/prolog aSmallFamily.pl "brothersister(gaelle,claudia)."  # false
../prolog/prolog aSmallFamily.pl "cousin(gaelle,claudia)."  # true

?- brothersister(gaelle,claudia).
?- cousin(gaelle,claudia).
  { }
  • Claudia is Clovis's sister, and Olivier and Gaëlle are her cousins:
In [147]:
../prolog/prolog aSmallFamily.pl "brothersister(X,clovis)."
../prolog/prolog aSmallFamily.pl "cousin(X,clovis)."

?- brothersister(X,clovis).
  { X = clovis }
  { X = claudia }
?- cousin(X,clovis).
  { X = clovis }
  { X = claudia }
  { X = olivier }
  { X = gaelle }

Conclusion

That's it for today, folks!

Have a look to this other repository for more notebooks I wrote.