Examples

In this subsection, some of the features of the determinism analysis and transformation that were not covered by example 4.6 are described with the help of some additional examples:

• even: a simple deeply deterministic test predicate
• append and reverse: functional predicates showing how free variables can be handled in LL and how to avoid the specification of catch-all clauses

Example 4.6 only contained two deeply deterministic functional predicates. The following example shows how test predicates are compiled.

even is compiled into the following LL function definition:

(defun even (arg#1)
  (if (equal 0 arg#1)
      t
      (if (and (> arg#1 1) (even (- arg#1 2)))
          t
          (if (and (< arg#1 -1) (even (+ arg#1 2)))
              t
              nil))))

The transformation process is nearly identical to the transformation for functional predicates with the following exceptions:

1. the transformation into RELFUN functions is not necessary
2. in , and thus in , the return value () is always t
3. the if and let cascade created by LL closes with nil; here, the final nil explicitly covers the cases arg#1=1 and arg#1=-1

The next example, append and reverse, is used to show

• how to avoid the specification of catch-all clauses and
• how free variables can be handled in LL.

Since in untyped PROLOG and RELFUN there is no way to specify that append and reverse only operate on lists, the weird catch-all clauses and additional cuts are needed.

In order to avoid these and all cuts, it is possible to declare predicates to be total deterministic functional predicates. With such declarations, append and reverse can be specified as one is used to in PROLOG, which leaves it to the user to call them with the intended types:

append([], X, X).
append([H|T], X, [H|Y]) :- append(T,X,Y).

reverse([],[]).
reverse([H|T],X) :- reverse(T,T1), append(T1,[H],X).

The following LL function definitions result:

(defun append/3-1 (arg#1 arg#2)
  (if (equal nil arg#1)
      arg#2
      (if (consp arg#1)
          (cons (car arg#1) (append/3-1 (cdr arg#1) arg#2))
          (type-error))))

(defun reverse/2-1 (arg#1)
  (if (equal nil arg#1)
      nil
      (if (consp arg#1)
          (append/3-1 (reverse/2-1 (cdr arg#1)) (cons (car arg#1) nil))
          (type-error))))

Since no catch-all clauses were specified, (type-error) is generated. Furthermore, the resulting LL definitions are slightly different from the definitions a human programmer would have chosen: since the compiler does not know that append and reverse only operate on lists, type-checking code is generated: (consp arg#1).

In the design of LL, (free) logical variables were not taken into account. In our implementation, they are simply ignored: they cannot be accessed in LL functions, but lists and structures with unbound variables that were created in REL can be used as arguments for LL functions. From LL's point of view, free variables belong to a data type for which neither constructors nor selectors exist.

It is thus possible to append or reverse lists with the above LL functions even if they contain free variables. In the further execution of the embedding REL program, these free variables can be bound: the query

X is [a,b,Y,f[Z]], reverse(X,XR), Y is c, Z is d

yields the following bindings:

X = [a, b, c, f[d]]
XR = [f[d], c, b, a]
Y = c
Z = d