rel

Can be viewed as a generalization of the procedural model in the following sense.

• Procedures can have zero or more output values.
• Which arguments are input arguments and which are the output values can differ for different calls of the same procedure.

Introduces a new statement called choice: "Nondeterministically" selects one statement among alternatives. However, the execution is executed using deterministic search.

Choice can lead to slow code. However they are practical for small search spaces, and as an exploratory tool.

A relational program is executed sequentially, when a choice statement is encountered, the first alternative is picked. When a fail is encountered, execution backs off to the most recent choice statement that was executed, and then another alternative is picked.

The choice statement picks alternatives in the order they were specified - s1 first, then s2 and so on.

The execution strategy can be illustrated with a search tree. The nodes in the tree correspond to choice statements, and the subtrees are the alternatives. Each path in the tree corresponds to one possible execution of the program. The path can either lead to a solution, or fail to provide a solution (it ends in a node marked fail.)

Given the search tree, there are several strategies to pick one or more solution from it.

A relational program can specify different solution search strategies: DFS, BFS, search for only one solution, return all solutions etc. Suppose that the relational program runs inside an "environment". This controls which solution is searched, and when it is searched.

The Solve function provides encapsulated search. (This is not a kernel language feature.) The call {Solve F} where F is a function taking no arguments, returns a lazy list of solutions ordered in a "depth-first" order.

For example,

{Browse {List.take {Solve
                    fun {$}
                       choice
                          choice
                             choice
                                '1.1.1'
                             [] '1.1.2'
                             end
                          [] '1.2'
                          end
                       [] '2'
                       end
                    end} 4}}

% Displays ['1.1.1' '1.1.2' '1.2' '2']

A code for searching Hamiltonian Paths Ham.oz The file Solve.oz consists of the Solve routine found on the textbook site booksuppl.oz.Please create a separate file named Solve.oz to run the code.

A logic program can be thought to consist of axioms, a sentence from first-order predicate calculus called the query, and a theorem prover.

A theorem prover has limited power. It can prove only the theorems which are true in all models. That is, it is complete - it has the ability to prove or refute any query. (There may be models with respect to which some theorems are true, but not provable - for example, theorems about integers with integer arithmetic. This follows from G\"odel's incompleteness theorem.) Even in cases where it can find a proof or a refutation, it might take time exponential in the number of variables.

So we restrict the axiom forms in the language. For example, Prolog is based on Horn Clauses. These are axioms of the form

∀ x₁, …, x_k ⋅ a₁ ∧ a₂ ∧ … ∧ a_n –> a.

where all the variables in the axioms are bound. There is an efficient theorem prover for Horn Clauses using an algorithm known as resolution.

The relational computational model in Oz can do logic programming, without resolution.

The programmer can aid the theorem prover with operational knowledge. For example, we can sort a set of numbers by stating that there exists a permutation of an input list which is in ascending order. This will lead to a result, but inefficiently. We can supplement this information to restrict the search by giving additional axioms about efficient search procedures like mergesort.