QuLog Function Rule Subset

The definition of a given function is made up of a contiguous sequence of function rules. Function rules take one of the following forms.
RuleHead -> Result
RuleHead :: RuleGuard -> Result

The first of the above forms is a special case of the second where RuleGuard is true. A consequence of this is that all the rules are committed rules, i.e. function calls are deterministic. This is one of the main differences between function rules and relation rules - relations are non-deterministic. Another difference is that relation calls can fail whereas functions are not allowed to fail. Instead, if no rules match the function call then a no_matching_function_rule exception it raised. This is flagging that we are outside of the domain of the function.

Consider the following definition of the factorial function.

fun fact(N:nat) -> nat
"Returns the factorial of N"
fact(0) -> 1
fact(N) :: N1 = N-1 & type(N1,nat) -> N*fact(N1)

The type check call is required as the type checker deduces the type of N1 is int after the subtraction. Can we avoid this type check call? We could if we change to the code below.

fun fact2(N:int) -> int
fact2(0) -> 1
fact2(N) -> N*fact2(N - 1)

However, we can give fact2 a negative number and this will lead to infinite computation. In an attempt to fix this we could add a guard to the second rule as follows.

fun fact3(N:int) -> int
fact3(0) -> 1
fact3(N) :: N > 0 -> N*fact3(N - 1)

Now the problem is that if we give this function a negative number we will raise a no_matching_function_rule exception. This is because fact3 is not a total function on its domain (int).

For the next example we consider converting between lists and ordered trees. Note that this code does not produce balanced trees.

def tree(T) ::= empty() | tr(tree(T),T,tree(T))

fun tree2list(tree(T)) -> list(T)
tree2list(empty()) -> []
tree2list(tr(LT, V, RT)) -> tree2list(LT) <> [V] <> tree2list(RT)

fun list2tree(list(int)) -> tree(int)
list2tree([]) -> empty()
list2tree([H|T]) -> add2tree(H, list2tree(T))

fun add2tree(TT, tree(TT)) -> tree(TT)
add2tree(T, empty()) -> tr(empty(), T, empty())
add2tree(T, tr(L, V, R)) :: T @< V -> tr(add2tree(T, L), V, R)
add2tree(T, tr(L, V, R)) -> tr(L, V, add2tree(T, R))

Recall that <> is the list concatenation function. We use the generic term ordering @<.

We finish this section by giving three examples of higher order functions - i.e. functions that take fuctions or relations as arguments. The example file contains several more such examples.

fun mapF((fun(T1) -> T2), list(T1)) -> list(T2)
mapF(_, []) -> []
mapF(_F, [H|T]) -> [F(H)|mapF(F, T)]

fun curry(fun(T1,T2) -> T3) -> fun(T1) -> fun(T2) -> T3
curry(F)(X)(Y) -> F(X,Y)

fun curryR(rel(T1,??T2)) -> fun(T1) -> rel(??T2),
curryR(rel(T1,?T2)) -> fun(T1) -> rel(?T2),
curryR(rel(T1,!T2)) -> fun(T1) -> rel(!T2)
curryR(Rel)(X)(Y) <= Rel(X,Y)

You will note that in each example we have a compound term with a variable functor. The type check allows this if the variable functor is known to be a ground code type as is the case in these examples.

In the second and third examples the head of the rule is a compound term whose function is itself a compound term. The third function definition is unusual - it is declared as a function but the rule is a relation rule. This is because curryR(Rel)(X) is a one argument relation and so when we apply this to its argument we get a relation call and so we need a relation rule.

Please note the complex type declaration for curryR. This intersection type allows different modes for the second argument that is reflected in the modes of the resulting relation. This maximizes the flexibility of use of this function.