Download Definitional Programming in GCLA Techniques, Functions, and

Definitional Programming in GCLA: Techniques, Functions, and Predicates
While the lazy function definitions we present share the property that evaluation
stops whenever a canonical object is reached, the rule definition we use cannot
avoid repeated evaluation of expressions.
In earlier work on functional programming in GCLA it is not the definition
but the rule definition that determines if lazy or eager evaluation is used. Lazy
evaluation then means that an expression is evaluated as little a possible before
an expression is returned and backtracking is used as the engine to evaluate
expressions further.
Given the definition of addition in Section 2.1, and with lazy evaluation, the
query
plus(s(0),0)\- C.
would then produce the answers:
C =
C =
C =
C =
no.
plus(s(0),0);
succ(plus(0,0));
s(plus(0,0));
s(0);
The eager evaluation strategy gives the same answers in the opposite order.
Although this might be interesting we do not feel that it is very useful for a
deterministic function like plus since all the answers represent exactly the same
value.
The definition of addition in Section 2.1 is an example of a strict function
definition. Using the calculus FL the query
plus(s(0),0) \- C.
will give the single answer C = s(0). It is actually a property of FL together with
the function definitions we present that, in both the lazy and strict case, we will
get only one answer unless the function itself is indeterministic. In short, given
a definition of a deterministic function F , there is only one possible derivation of
F ` C.
4.4.1
Defining Strict Functions
By a strict function definition we mean a definition which ensures that the value
returned from the function is a fully evaluated canonical value, that is, a canonical
object with no inner expressions remaining to be evaluated. We must therefore
find a systematic way to write function definitions that guarantees that only fully
evaluated expressions are returned from functions.
The solution to this problem is to be found in the method we use to build
data objects in definitions. Recall the ML type definition
24