4.10.7 Function Definitions

A function definition consists of a sequence of rules of the form

Head :: Commit -> Expression

where Head and Commit are the same as for relation rules and Expression is a term. The :: Commit part of the rule is optional. The heads of each rule of a function have the same functor and arity.

When the function is called, the rules are tried and the first rule whose Head unifies with the function call and where Commit is true then the result returned is the evaluation of Expression. Note that rules without an explicit Commit have an implicit true commit and so no backtracking occurs.

As with action definitions, a catchall clause is added to the end so that if a function call does not match any of the rules then an exception is raised.

As examples, the definitions of the functions factorial and tree2list are given below (using the tree type given above).

fun factorial(nat) -> nat 
factorial(0) -> 1
factorial(N) ::  N1 = N-1 & type(N1,nat) -> N*factorial(N1)

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

Note that type(N1,nat) is necessary above in order that the type checker can type check the recursive call on factorial.