# rel

## Table of Contents

## 1 Relational Model

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.

## 2 New Statements

### 2.1 Choice

It is a group of alternative statements.

choice s1 [] ... [] sn end

The choice statement selects and executes a statement. If this choice
is later found wrong, then an alternative is picked. The choice
statement introduces a part of the abstract machine to roll back
execution and pick another choice - this is called a **choice point**.

### 2.2 Fail

fail

A fail statement declares that the current alternative is wrong. In addition to a programmer explicitly executing the statement, it also executes implicitly when the bind operation fails. (e.g. 1 = true)

## 3 Search Tree

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.

## 4 Encapsulated Search:

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']

## 5 Code Example

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.

## 6 Logic Programming in Oz

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_{1}, …, x_{k} ⋅ a_{1} ∧ a_{2} ∧ … ∧ 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.

### 6.1 Operational Semantics and Logical Semantics

We can translate every statement in the relational kernel language (that is, the declarative kernel language of Chapter 2 + choose + fail) into equivalent first-order predicate sentences.

The following table gives a scheme *T* which translates relational
statements into their equivalent logical statements.

Relational Statement | Logical Formula | Notes |
---|---|---|

skip | true | |

fail | false | |

s_{1} s_{2} | T(s_{1}) ∧ T(s_{2}) | |

choice s1 [] … [] s_{n} end | T(s_{1}) ∨ … ∨ T(s_{n}) |

Binding:

X=Y | x=y | |

X=r(f_{1}:X_{1} … f_{n}:X_{n}) | x=r(f_{1}:x_{1} … f_{n}:x_{n}) | records |

Conditionals and Pattern Matches:

if X then s_{1} else s_{2} end | (x=true ∧ T(s_{1})) |
---|---|

∨ (x=false ∧ T(s_{2})) | |

case X | (∃ x_{1} … x_{n} . x=r(f_{1}:x_{1} … f_{n} x_{n}) ∧ T(s_{1})) ∨ |

of r(f_{1}:X_{1} … f_{n}:X_{n}) | |

then s_{1} else s_{2} end | |

(¬∃ x_{1} … x_{n} . x=r(f_{1}:x_{1} … f_{n} x_{n}) ∧ T(s_{2})) |

Variable declarations

local X in s end | ∃ x . T(s) | Why ∃? |

proc {P X_{1} … X_{n}} s end | ∀ x_{1} … x_{n} . p(x_{1} … x_{n}) <-> T(s) |

Procedure Application

{P Y_{1} … Y_{n}} | p(y_{1} … y_{n}) |

Different operational semantics can have the same logical semanttics,

X = Y s if X==Y then s else fail end s X=Y

all have the same logical semantics,

x = y ∧ T(s)

But of course, their operational semantics is different. For instance, suppose s refers to X, without binding it. Then the example in the center will suspend in the sequential model, where as the leftmost example could succeed. The rightmost example differs from the other two since it does not ensure that X binds to Y.

So to write a logic program, we have to do the following. Write the logic semantics, then choose an operational semantics for the program. The first should be simple, and the second efficiently executable.

### 6.2 Code Example

The following is a non-deterministic append.

The logical semantics.

(∀ a b c . append(a,b,c) ↔ (a=nil ∧ b=c) ∨ (∃ x a' c' . a=x |a' ∧ c=x |c' ∧ append(a',b,c')))

Date: 2011-11-15 14:24:04 IST

HTML generated by org-mode 6.33x in emacs 23