An inspiring conversation with Mikael More brought up unthought-of questions. What if we do try to use Hansei to solve typical logic programming puzzles? Can we even do it? Can we do it efficiently? How much of logic programming will remain? In particular, can we read the Hansei code as a clear, declarative statement of the problem, without being distracted by the details of the solution? This present web page documents the attempts to answer all these questions. Hansei turns out suitable for logic programming after all.
We discuss logic programming without logic variables in a separate article below. Here we argue why one might want to consider Hansei when solving a typical logic programming problem.
Hansei adheres to declarative programming, by separating building probabilistic models from inference. A model describes the properties of a possible world and defines computations and constraints on them. Inference finds possible worlds satisfying the properties and the constraints. Building models and writing inference (search) procedures are distinct activities with distinct abstractions; writing custom inference procedures is rare since the ones in Hansei often suffice.
Many uses of cuts, negation and committed choice in Prolog are a way of telling that certain predicate is (semi-)deterministic; in other words, the underlying relation is functional. In Hansei, it is the determinism that is the default; deterministic computations run `at full speed' of OCaml, with no overhead. Hansei is thus particularly suitable for logic programs with a large portion of deterministic, especially numeric, computations. Hansei, as underlying OCaml, is typed. Types are notably useful in logic programming, to avoid a typical Prolog problem, of a mis-spelled constant or variable leading to an incorrect answer rather than an error message. Without types, such errors are frustratingly difficult to find.
Probability estimations turn out useful too: if we prematurely terminate a Hansei search, we obtain an estimate of the probability of missing a solution. Assigning different weights to different choices (that is, using non-uniform probability distributions) is a way to supply heuristics to bias the search.
Except for probability, the arguments for Hansei are the arguments for functional logic programming, equally applicable to the languages like Curry. The strong case for functional-logic programming has been made elsewhere, see in particular surveys by Michael Hanus. The advantage of Hansei is that it is not a separate language: it is just a user-extensible OCaml library. The arguments for Hansei also apply to embeddings of non-determinism in a typed functional language (for example, MonadPlus in Haskell), provided the crucial feature of lazy sharing is supported.
HANSEI: Embedded Probabilistic Programming
Purely Functional Lazy Non-deterministic Programming
The paper describes the importance, equational theory and the implementation of lazy sharing. The implementation of letlazy in Hansei is based on the technique explained in the paper.
Logic programming without logic variables should be obvious. The minimal model semantics of Prolog needs no logic variables; after all, Herbrand basis is by definition a set of ground atoms. The fixpoint construction (iterating the immediate consequence operator) gives the algorithm of finding the minimal model with no use for variables or unification. The reality dims the hope: although the fixpoint construction is viable for definite Datalog programs, it is difficult to perform when the Herbrand basis is infinite and the logic program contains negation and committed choice.
Two recent theoretical results in functional logic programming, Antoy and Hanus (2006) and Dios Castro and Lopez-Fraguas (2006), point out that logic variables and non-determinism due to overlapping rules have the same computational power. The main idea is representing a logic variable by a generator of its domain, with sharing of the generator expressing repeated occurrences of the variable. The idea is intuitively clear: a logic variable indeed stands for some term, non-deterministically chosen from a suitable domain. The papers derive a systematic transformation of a program with logic variables into the one without, while preserving the set of derivations. Alas, preserving the set of derivations (reductions) is a rather weak notion of program equivalence. For example, it does not account for the multiplicity of results, considering a program that yields, say, a single 0 equivalent to a program yielding the infinite sequence of 0s. In logic programming practice, we usually do distinguish such programs, valuing programs that produce a finite set of answers in finite time. The other drawback of the theoretical frameworks used in both papers is the inability to reason about finite failure. A logic program that returns "NO" in finite time and the program that loops forever are regarded as equivalent in these frameworks. In practice we consider such programs as very different. Since the papers are written as theoretical, the details about sharing and fairness of generators are sketchy.
Aware of the theoretical hopes and practical shortcomings, we decided to press ahead and see just how far we can go expressing standard Prolog idioms in a language without logic variables. Pending adequate theoretical analysis, empirical case studies seem the only choice. The present web page documents our results. The somewhat unexpected conclusion is that we go quite far. Hansei as it is appears suitable for logic programming.
We have gone back to Herbrand: we build the Herbrand universe (the set of
all ground terms) and explore it to find a model of a program
(that is, tuples of terms that model all declared relations).
We build the universe by modeling `logic variables'
as generators for their domains. It greatly helps that Hansei is
typed; the type of a `logic variable' specifies its domain and, hence,
the generator. Since the Herbrand universe for most logic programs
is infinite, we need
non-strict evaluation. Furthermore, since logic variables may
occur several times, we must be able to correlate the generators. Although
Hansei is embedded in OCaml, which is strict, Hansei supports
on-demand evaluated non-deterministic computations with sharing:
so-called letlazy computations. Finally, since the search space
is generally infinite, we need a systematic way of exploring it,
without getting stuck in one infinite sub-region. Again Hansei provides
a number of search strategies, including sampling and iterative deepening.
(We shall use the latter in all our examples.)
Logic variables and unification have been introduced by Robinson as a way to `lift' ground resolution proofs of Herbrand, to avoid generating the vast number of ground terms. Logic variables effectively delay the generation of ground terms to the last possible moment and to the least extent. Doing computations only as far as needed is also the goal of lazy evaluation. It appears that lazy evaluation can make up for logic variables, rendering Herbrand's original approach practical.
Sergio Antoy and Michael Hanus: Overlapping rules and logic variables in Functional Logic Programs
ICLP 2006.
J. de Dios Castro and F.J. Lopez-Fraguas: Elimination of Extra Variables in Functional Logic Programs
Proc. V Jornadas sobre Programacion y Lenguajes (PROLE'06), pp. 121-135, 2006.
appendrelation. Append relates three lists l1, l2 and l3
such that l3 is the concatenation of l1 and l2. All throughout we
take our lists to be lists of booleans. We will contrast Prolog code
with Hansei code, developing both incrementally and interactively.
The responses of Prolog resp. OCaml top-level are indented.
In Prolog, the append relation is stated as:
append([],L,L).
append([H|T],L,[H|R]) :- append(T,L,R).
declaring that an empty list is a prefix of any list,
a list is a suffix of itself, and prepending to the prefix of a list prepends
to the list. Certainly append can concatenate two lists:
?- append([t,t,t],[f,f],X).
X = [t, t, t, f, f].
By passing a free logic variable as one of the two first arguments,
we can concatenate not fully-determined lists:
?- append([t,t,t],X,R).
R = [t, t, t|X].
We see the single result, which stands for every
list with the prefix [t,t,t]. Such a compact representation of an infinite
set is an asset. Alas, it is not always available, and is often a mirage.
For example, if we pass a free variable as the first argument of
append, Prolog responds differently:
?- append(X,[f,f],R).
R = [f, f] ;
R = [_G328, f, f] ;
R = [_G328, _G334, f, f] ;
R = [_G328, _G334, _G340, f, f] .
with an infinite set of answers, to be enumerated indefinitely. It
may not be fully apparent that our Prolog code has not faithfully
represented the original problem: to relate boolean lists. The last
two answers describe lists of more than mere booleans. We have to
impose the restriction, by defining the type predicates
bool(t).
bool(f).
boollist([]).
boollist([H|T]) :- bool(H), boollist(T).
and re-writing our queries:
?- append([t,t,t],X,R), boollist(X), boollist(R).
R = [t, t, t] ;
R = [t, t, t, t] ;
R = [t, t, t, t, t] ;
R = [t, t, t, t, t, t] ;
R = [t, t, t, t, t, t, t, t, t] .
?- append(X,[f,f],R), boollist(X), boollist(R).
R = [f, f] ;
R = [t, f, f] ;
R = [f, f, f] .
One of boollist(X) or boollist(R) would have
been enough: if X is a boolean list, so is R. Alas, Prolog has no
type inference and is unable to infer or take advantage of that fact.
To be safe, we add both predicates. The compact representation for the
lists with the [t, t, t] prefix has disappeared.
More seriously, the default depth-first search strategy of Prolog gives
us only half of the answers; we won't ever see the lists with an f
after the first three t.
We switch to Hansei. In a typed language, types -- the specification
of the problem -- come first. We start by defining the type blist of
boolean lists with a non-deterministic spine, along with the convenient
constructors:
type bl = Nil | Cons of bool * blist
and blist = unit -> bl;;
let nil : blist = fun () -> Nil;;
let cons : bool -> blist -> blist = fun h t () -> Cons (h,t);;
and the conversion to ordinary, fully deterministic lists,
to see the results.
let rec list_of_blist bl = match bl () with
| Nil -> []
| Cons (h,t) -> h:: list_of_blist t;;
val list_of_blist : blist -> bool list = <fun>
We now define append, seemingly as a function, in the fully standard,
also declarative, way.
let rec append l1 l2 = match l1 () with
| Nil -> l2
| Cons (h,t) -> cons h (fun () -> append t l2 ());;
val append : blist -> blist -> blist = <fun>
An attempt to concatenate two sample lists:
let t3 = cons true (cons true (cons true nil));;
let f2 = cons false (cons false nil);;
append t3 f2;;
- : blist = <fun>
turns out not informative. Recall that we use the Hansei library to build a probabilistic model, which we then have to run. Running the model determines the set of possible worlds consistent with the probabilistic model: the model of the model. The set of model outputs in these worlds is the set of answers. Hansei offers a number of ways to run models and obtain the answers and their weights. We will be using iterative deepening:
val reify_part : int option -> (unit -> 'a) -> (Ptypes.prob * 'a) listThe first argument is the depth search bound (infinite, if
None).
reify_part None (fun () -> list_of_blist (append t3 f2));;
- : (Ptypes.prob * bool list) list = [(1., [true; true; true; false; false])]
Running our first append model has given the expected result, with the expected
weight. Following along the Prolog code, we turn to appending to an
indeterminate list.
Indeterminate lists are represented by generators. Hence, we need
generators for bool and bool list domains. The generators must use letlazy,
to delay the generation until the value is needed; once the value has been
determined, it stays the same.
let a_boolean () = letlazy (fun () -> flip 0.5);;
val a_boolean : unit -> unit -> bool = <fun>
let rec a_blist () = letlazy (fun () -> dist [(0.5, Nil); (0.5, Cons(flip 0.5, a_blist ()))]);;
val a_blist : unit -> blist = <fun>
Let us see a sample of generated values, as a spot-check:
reify_part (Some 5) (fun() -> list_of_blist (a_blist ()));;
- : (Ptypes.prob * bool list) list =
[(0.5, []);
(0.125, [false]);
(0.03125, [false; false]);
(0.03125, [false; true]);
(0.125, [true]);
(0.03125, [true; false]);
(0.03125, [true; true])]
The lists of different lengths have different probabilities, or
different likelihoods of encountering them. We could use the accumulated
probability mass as the measure of the explored search space, terminating
the search once a threshold is reached. One is reminded of probabilistic
algorithms such as the Rabin-Miller primality test.
We are now ready to reproduce the Prolog code, passing a `free' variable
as an argument to append and obtaining a sequence of lists with the
given prefix or suffix. Unlike Prolog, we are
not stuck in a corner of the search space. We generate all lists
with the given prefix [true; true; true].
reify_part (Some 5) (fun() ->
let x = a_blist () in
list_of_blist (append t3 x));;
- : (Ptypes.prob * bool list) list =
[(0.5, [true; true; true]);
(0.125, [true; true; true; false]);
(0.03125, [true; true; true; false; false]);
(0.03125, [true; true; true; false; true]);
(0.125, [true; true; true; true]);
(0.03125, [true; true; true; true; false]);
(0.03125, [true; true; true; true; true])]
reify_part (Some 5) (fun() ->
let x = a_blist () in
list_of_blist (append x f2));;
- : (Ptypes.prob * bool list) list =
[(0.5, [false; false]);
(0.125, [false; false; false]);
(0.03125, [false; false; false; false]);
(0.03125, [false; true; false; false]);
(0.125, [true; false; false]);
(0.03125, [true; false; false; false]);
(0.03125, [true; true; false; false])]
Prolog's append is so elegant because it defines a relation among
three lists. One can specify any two lists and query for
the other one that makes the relation hold. For example, we check if
a given list has a given prefix, and if so, remove it:
?- append([t,t],X,[t,t,t,f,f]).
X = [t, f, f].
We can do the same in Hansei, effectively `running append backwards.'
We introduce a sample list to deconstruct and a function two compare
two lists. It is an ordinary function, not a built-in.
let t3f2 = append t3 f2;;
let rec bl_compare l1 l2 = match (l1 (), l2 ()) with
| (Nil,Nil) -> true
| (Cons (h1,t1), Cons (h2,t2)) -> h1 = h2 && bl_compare t1 t2
| _ -> false;;
val bl_compare : blist -> blist -> bool = <fun>
The prefix-removal example is as follows. In words: we assert that
there exists a boolean list x such that appending it to
[true; true] yields the list t3f2. We ask Hansei to find all
possible worlds in which the assertion holds and report the value
of x in these worlds.
reify_part None (fun() ->
let x = a_blist () in
let r = append (cons true (cons true nil)) x in
if not (bl_compare r t3f2) then fail ();
list_of_blist x);;
- : (Ptypes.prob * bool list) list = [(0.0078125, [true; false; false])]
Since the search bound was None, the returned single result came from
the exhaustive enumeration of the entire search space. The search space is
indeed infinite, but amenable to efficient exploration because most
of the possible worlds are inconsistent with the assertion and
could be rejected wholesale, without generating them. For example,
when comparing an indeterminate list to an empty list, bl_compare
returns the result after forcing a single choice. One can tell
if a list is empty by checking for the first Cons cell.
One does not need to know how many else elements there may be in the list.
In general, if the lists are not equal, it can be determined by
examining their finite prefix. Furthermore, if one of bl_compare's arguments
has a fixed length (as is the case in our example: t3f2 is the list
of 5 elements), the comparison finishes after forcing finitely many choices.
The ability of bl_compare to deal with partially determined lists
relates it to unification: unifying [X|Y] with the empty
list fails without the need to instantiate X or Y, in effect
performing the comparison with the infinite set of concrete lists.
We can likewise use append to check for, and remove, a given suffix.
We can also split a given list in all possible ways,
returning its prefixes and suffixes. If the list is finite, we obtain
the finite number of answers, in Prolog:
?- append(X,Y,[t,t,t,f,f]).
X = [], Y = [t, t, t, f, f] ;
X = [t], Y = [t, t, f, f] ;
X = [t, t], Y = [t, f, f] ;
X = [t, t, t], Y = [f, f] ;
X = [t, t, t, f], Y = [f] ;
X = [t, t, t, f, f], Y = [] ;
false.
and, similarly, in Hansei:
reify_part None (fun() ->
let x = a_blist () in
let y = a_blist () in
let r = append x y in
if not (bl_compare r t3f2) then fail ();
(list_of_blist x, list_of_blist y));;
- : (Ptypes.prob * (bool list * bool list)) list =
[(0.000244140625, ([], [true; true; true; false; false]));
(0.000244140625, ([true], [true; true; false; false]));
(0.000244140625, ([true; true], [true; false; false]));
(0.000244140625, ([true; true; true], [false; false]));
(0.000244140625, ([true; true; true; false], [false]));
(0.000244140625, ([true; true; true; false; false], []))]
The Hansei code follows the demonstrated pattern, of building
a probabilistic model returning a pair of two `random' lists
x and y, conditioned upon the asserted evidence that their
concatenation is t3f2. In the above code, the OCaml variable x
is used twice. Although it is bound to a generator, its two use
occurrences refer to the same generated value -- thanks to letlazy
in the definition of a_blist.
Our final example is last, relating a list to its last element.
We contrast Prolog code
last(E,L) :- append(_,[E],L).
?- last(E,[t,t,f]).
E = f ;
to Hansei code:
let last bl =
let x = a_blist () in
let e = a_boolean () in
if not (bl_compare (append x (cons (e ()) nil)) bl) then fail ();
e;;
val last : blist -> unit -> bool = <fun>
reify_part None (fun() -> last t3f2 ());;
- : (Ptypes.prob * bool) list = [(0.0009765625, false)]
There are still open questions. The following code produces the result with no restrictions on the search space:
reify_part None (fun () ->
let x = a_blist () in
let y = a_blist () in
if not (bl_compare x t3f2) then fail ();
if not (bl_compare x y) then fail ();
list_of_blist y);;
- : (Ptypes.prob * bool list) list = [(2.384185791015625e-07, [true; true; true; false; false])]
A slightly modified code, with (bl_compare x y) first, although
gives the same result, requires the restriction on the search
depth. The search space can no longer be efficiently enumerated.
Can we automatically reorder the comparison statements, to improve the
search? Another open problem is the `occurs check.' Its absence in Hansei
again necessitates the restriction on the search space.
None of the two open issues are fatal: restricting the search by
depth or by the remaining probability mass (effectively, by the
probability of missing a solution if one exists) is always possible
and even natural. It is nevertheless interesting to see if
the occurs check and the unification of two unbound variables
have a clear analogue in the variable-less case.
The gist of the problem is selecting a subset of actions to do on one day from the set of possible actions. In other words, we need to sample from a powerset. Such a sampling function could have been provided by Hansei. It is however easy and illustrative to define from scratch:
open ProbM;;
let powerset lst = List.fold_left (fun acc e -> if flip 0.5 then e::acc else acc) [] lst;;
val powerset : 'a list -> 'a list = <fun>
In words: to choose a subset of the set lst we decide, randomly and
independently, for each element of lst whether to take it or not.
We use OCaml lists to represent sets.
To spot-check our sampling procedure we compute the probability
table for all samples from powerset [1;2;3]:
exact_reify (fun () -> powerset [1;2;3]);;
- : int list Ptypes.pV =
[(0.125, Ptypes.V [3; 2; 1]);
(0.125, Ptypes.V [3; 2]);
(0.125, Ptypes.V [3; 1]);
(0.125, Ptypes.V [3]);
(0.125, Ptypes.V [2; 1]);
(0.125, Ptypes.V [2]);
(0.125, Ptypes.V [1]);
(0.125, Ptypes.V [])]
Indeed all subsets are present, with the equal probabilities.
We define another simple but helpful function, which asserts the
proposition x in the current world:
let mustbe x = if not x then fail ();;
val mustbe : bool -> unit = <fun>
We are ready to encode our problem. We define the datatype enumerating the possible actions:
type action = Shop | Walk | Barber | Supermarket;;To define the model we specify the sampling procedure for the actions and enumerate the constraints, following the most straightforward generate-and-test approach.
let schedule_model () =
let ndays = 3 in
We determine the set of actions to do on day d.
The set is chosen randomly from the set of all possible actions.
However, if we ask again which actions were chosen for day d,
we should get the same answer. Thus actions d acts as a
logic variable: its value, initially indeterminate, once
determined, does not change. We use the memo facility of
Hansei to define such memoized stochastic functions.
let actions = memo (fun d -> powerset [Shop; Walk; Barber; Supermarket]) inThe proposition
action_on a d states that on day d I do action a.
The proposition only_on a d asserts that I do action a only
on day d (and not on any other day):
let action_on a d = List.mem a (actions d) in
let only_on a d = [d] = List.filter (action_on a) [0;1;2] in
We now state the constraints.
For example, the first two lines below assert that there exists a
day on which I shop. I do not shop on any other day.
let d = uniform ndays in
let _ = mustbe (only_on Shop d) in
let d = uniform ndays in
let _ = mustbe (only_on Walk d) in
let d = uniform ndays in
let _ = mustbe (only_on Barber d) in
let d = uniform ndays in
let _ = mustbe (only_on Supermarket d) in
(* The same day as I go to the supermarket, I'll shop.
That is, there is a day that I perform the action Shop and the action Supermarket
*)
let d = uniform ndays in
let _ = mustbe (action_on Supermarket d && action_on Shop d) in
let d = uniform ndays in
let _ = mustbe (action_on Walk d && action_on Barber d) in
(* I'll go to the supermarket the day before the day I'll take a walk. *)
let d = uniform ndays in
let _ = mustbe (action_on Walk d && d > 0 && action_on Supermarket (d-1)) in
(* I'll take a walk Tuesday. *)
let _ = mustbe (action_on Walk 1) in
Finally, we return the schedule: the array of actions for each day.
This is the output of the model.
Array.init ndays actions;;
val schedule_model : unit -> action list array = <fun>
The model is defined. We now `solve' it, determining if
there exists a schedule satisfying all constraints. Hansei's reply
is nearly instantaneous.
exact_reify schedule_model;;
- : action list array Ptypes.pV =
[(1.11632658893461385e-07, Ptypes.V [|[Supermarket; Shop]; [Barber; Walk]; []| ])]
There is only one schedule satisfying the constraints:
on Monday I go to the supermarket and shop, on Tuesday I walk
and take a haircut. Hansei has also computed the `probability' of
the solution, which is the the estimate of the search space.
Each choice in the model corresponds to a possible world;
many possible worlds are
not consistent with the stated constraints and facts and are
rejected. The reported 1.11632658893461385e-07 is the weight of the
surviving possible world(s), the one(s) that satisfied all
constraints. Since all our choices were uniform,
the weight represents one in 1/1.11632658893461385e-07 = 8957952
that many worlds. Since worlds can be rejected wholesale, Hansei did not
have to generate all of them. If one fact
in a world contradicts the evidence, we do not need to know
the other facts; that is, we do not need to make the choices for them.all_different is a hassle to state and a chore to evaluate;
constraint logic programming (sub)systems (e.g.,
SICStus) typically rely on external constraint solvers, where
all-different is built-in. Even without `all-different' the puzzle is
hard; the naive generate-and-test approach is too
slow; a bit of creativity is required.
Hansei's formulation of the problem is straightforward and declarative: the naive generate-and-test. That was the point, to see how well Hansei copes without the benefit of a creative formulation or fine-tuning. Hansei copes quite well. It helped that deterministic parts of the puzzle more naturally express in a functional language with data structures and pattern-matching (Hansei's host language, OCaml) than in Prolog. We use non-determinism only when we need it. It also greatly helped that the all-different constraint, or sampling all permutations, turns out efficiently, lazily, implementable in Hansei.
zebra.ml [6K]
The complete, commented source code, with every significant line annotated.
Hansei determined that that puzzle has only one solution,
whose weight is 5e-12. The search space is large indeed.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML