2017-03-20
Relational Programming in Mozart/Oz
A video I watched recently on logic programming, A Vision for Relational Programming in miniKanren, by William Byrd gives some interesting examples of relational programming using miniKanren.
miniKanren is an embedded constraint logic programming language designed for writing programs as relations, rather than as functions or procedures. Unlike a function, a miniKanren relation makes no distinction between its inputs and outputs, leading to a variety of fascinating behaviors. For example, an interpreter written as a relation can also perform code synthesis, symbolic execution, and many other tasks.
The video demonstrates how a relational interpreter can be used not just to evaluate expressions but to also generate valid expressions given a result. Other examples of relational programming would be the Prolog examples in my Shen Prolog post where relational functions like member
can be used to enumerate all members of a list, as well as the traditional finding a member in a list.
I like to use the Mozart Programming System for exploring logic programming and this post goes through converting some examples in Mozart/Oz. Mozart is an implementation of the Oz programming language. The book "Concepts, Techniques, and Models of Computer Programming" is a good textbook for learning the different programming models that Mozart enables, including the relational model. For the examples here I'm using Mozart 1.3.x. It's an old language and implementation but I like to experiment with languages that are a bit different to mainstream languages.
The Prolog examples following can be tested in the online SWI Prolog implementation, Swish.
Basic example
The following function in Prolog has multiple values that be used as an argument:
foo(one).
foo(two).
foo(three).
Passing either one
, two
or three
succeeds:
foo(one).
true
foo(two).
true
foo(four).
false
Using backtracking it's possible to enumerate all valid arguments:
foo(X).
X = one
X = two
X = three
The function findall
can be used to return all values in a list:
findall(X, foo(X), Y).
Y = [one, two, three]
Backtracking in Mozart/Oz is not the default. Mozart provides the choice
statement to enable backtracking. A choice
statement contains a sequence of clauses separated by []
where a 'choice point' is created for each group of clauses. Each clause is tried in turn - if a particular clause fails then execution backtracks to a previous choice point and is resumed until one succeeds or all fails. The equivalent implementation of foo
in Mozart is:
fun {Foo}
choice
one
[]
two
[]
three
end
end
Prolog uses an automatic depth first search to find solutions. Mozart doesn't do automatic search - programs involving choice points must be run in a search engine that can implement any form of search required. A default search engine is provided that does depth first search. Here we create a search object and enumerate all the valid results manually:
Y = {New Search.object script(Foo)}
{Browse {Y next($)}
[one]
{Browse {Y next($)}
[two]
{Browse {Y next($)}
[three]
{Browse {Y next($)}
nil
The Mozart syntax can look a little strange at first but it's not too difficult to understand once it's learnt. New
instantiates an object. Search.object is the class of the object being created. script(Foo)
is a record that is being passed to the constructor of Search.object
. The Foo
is the function we created previously. The remaining statements call the next
method on the object. next
takes as an argument a variable that receives the result of the call. The use of $
tells Mozart to pass a temporary variable to receive the result, and return that result as the result of the call. This result is passed to Browse
which displays the result in the GUI browser. Results are returned in single element lists and when there are no more results, nil
is returned.
There is a library function to return all possible solutions in a list, Search.all:
{Browse {Search.all Foo 1 _ $}}
[one two three]
The ability to interactively drive the search enables writing programs that control the search process. The Explorer is a Mozart tool that uses this ability to show an interactive graph of the search space of a program. It can be run to show a graph of all solutions in Foo
with:
{Explorer.all Foo}
Membership testing
In Prolog a function to test membership of a list can be written as:
mem(X, [X|_]).
mem(X, [_|Y]) :- mem(X, Y).
This states that X
is a member of the list if X
is the head of the list (the first element), or if it is a member of the tail of the list.
mem(2, [1,2,3]).
true.
Thanks to Prolog's backtracking you can also use this function to enumerate all values in the list:
mem(X, [1,2,3]).
1
2
3
In Swish you need to click 'Next' to get each result. You can return all results as a list with findall
:
findall(X, mem(X, [1,2,3]), Y).
Y = [1, 2, 3].
This is what the non-backtrackable member function looks like in Mozart:
fun {Mem X Ys}
case Ys
of nil then false
[] Y|Yr then X==Y orelse {Mem X Yr}
end
end
{Browse {Mem 1 [1 2 3]}}
true
A backtrackable version of this code uses choice
instead of case
to create choice points in each clause:
proc {Mem X Ys}
choice
Ys = X|_
[]
Yr
in
Ys = _|Yr
{Mem X Yr}
end
end
Here proc
is used instead of fun
. A procedure doesn't return a value. It is expected to bind values to arguments to return a result. In this case either X
or Ys
will be bound depending on what is passed as an argument. Given the call Mem 1 [1 2 3]
then the first clause of choice
succeeds - the head of the list is equal to X
. With the call Mem X [1 2 3]
then X
will be successively bound to each element of the list depending on what order the search engine used to evaluate it uses. Mem 1 Y
will enumerate all possible lists containing 1
:
{Browse {Search.all proc {$ L} {Mem 1 [1 2 3]} end 1 _ $}}
[_]
{Browse {Search.all proc {$ L} {Mem L [1 2 3]} end 1 _ $}}
[1 2 3]
Y={New Search.object script(proc {$ L} {Mem 1 L} end)}
{Browse {Y next($)}}
[1|_]
{Browse {Y next($)}}
[_|1|_]
{Browse {Y next($)}}
[_|_|1|_]
The difference here compared to our search over Foo
is that an anonymous procedure is passed to the search engine. Foo
was aleady a single argument procedure so it didn't require a wrapper. The anonymous procedure takes a single argument which is expected to be bound to the result of a single iteration. In the first example no result is bound, just the fact that the Mem
call succeeds is enough. In the second, L
is bound to the first argument to Mem
resulting in a list of all valid first arguments. In the third, L
is bound to the second argument to Mem
resulting in a list of all valid lists that contain the element 1
. This is infinite so we only iterate the first few solutions.
Syntax checker
The miniKanren video referenced earlier, A Vision for Relational Programming in miniKanren, has an example of a simple language syntax checker implemented in the relational style. The equivalent Mozart implementation is:
proc {LCSyn Term}
choice
{IsAtom Term true}
[]
X T
in
Term = lambda(X T)
{IsAtom X true}
{LCSyn T}
[]
E1 E2
in
Term = [E1 E2]
{LCSyn E1}
{LCSyn E2}
end
end
A Term
is either an atom, a lambda
record containing an argument and body, or application of two expressions (here represented as a list). A Term
can be tested to see if it is valid with:
{Browse {Search.one.depth
proc {$ L}
{LCSyn lambda(foo bar)}
end
1 _ $}}
A result of [_]
indicates that it succeded (nil
would be a failure). Thanks to the magic of relational programming it's possible to enumerate all valid terms:
Y={New Search.object script(LCSyn)}
{Browse {Y next($)}}
[lambda(_ _)]
{Browse {Y next($)}}
[[_ _]]
{Browse {Y next($)}}
[[lambda(_ _) _]]
{Browse {Y next($)}}
[[[_ _] _]]
Reversible Factorial
As a final example, the following program implements a factorial function that can compute the factorial of a number, or the number given its factorial:
proc {Fact ?N ?F}
proc {Fact1 ?N ?F}
choice
N = 0
F = 1
[]
N1 F1
in
N1::0#FD.sup
F1::0#FD.sup
N >: 0
N1 =: N - 1
F =: N * F1
{Fact1 N1 F1}
end
end
in
N::0#FD.sup
F::0#FD.sup
{Fact1 N F}
{FD.distribute naive [N F]}
end
% Factorial of 5
{Browse {Search.all proc {$ L} {Fact 5 L} end 1 _ $}}
[120]
% What factorial gives the answer 24
{Browse {Search.all proc {$ L} {Fact L 24} end 1 _ $}}
[4]
This uses a few more Mozart features but is essentially a search through the choice points in a choice
statement. In this case it also uses Finate Domain Constraints. This allows telling Mozart what the range of a particular integer value can be, provides constraints upon that value and the search process will attempt to find a solution that results in the integer containing a single value. The syntax X::0#5
constrains the variable X
to be from zero to five. FD.sup
is a constant for an implementation defined maximum upper bound. Operators ending in :
impose constraints on values that can be backtracked during search. There's a limitation to this approach in that the finite domain constraint has an implementation defined maximum upper value and the search will fail if it hits this value which unfortunately limits the practicality of a reverse factorial.
Mozart/Oz summary
Mozart/Oz has a lot of other interesting functionality. Distributed objects, GUI programming, Concurrency, amongst others. It's a fun tool to experiment with and Concepts, Techniques, and Models of Computer Programming is an excellent read.
Unfortunately development of Mozart has slowed from its heyday. A reimplementation of Mozart, called Mozart 2 is being worked on that uses LLVM for the code generator and replaces the internal constraint programming system with the Gecode toolkit. Development seems to have stalled recently and it lacks many of the features that already exist in older Mozart versions. Hopefully it'll pick up steam again.
For this reason I continue to use Mozart 1.3.x. There is a 1.4.x version but it has some issues that make me avoid using it. The distributed layer was replaced with an implementation written in C++ which has some bugs that I've been unable to work around in projects where I used it. The distribution panel is broken due to the hooks it requires not being implemented by the new C++ layer. At some point Mozart 2 may be complete enough for me to move to that version. I make the occasional fixes to 1.3.x and 1.4.x to keep it building and running on Linux.
Even though Mozart seems to be in a holding pattern it's a great for exploring ideas and the list of papers is a good resource for learning about distributed programming, constraints and concurrency. Some interesting projects implemented in Mozart include:
- Beernet, a P2P network (source).
- Ebl/Tk (PDF), a GUI library where widgets can be migrated across devices (source).
- Roads, a web application framework (source).
- Transdraw, a distributed collaborative graphical editor (source).
- Strasheela, a constraint based music system which also has a good Oz tutorial.