Function and Function Logic

Functions and Function Objects

We have to distiguish between functions (see chapter Functions) and function objects (this chapter).

Functions are declared at the toplevel of a module like the boolean functions ==>, and, ... Function objects are objects which represent functions and can be passed around as arguments to other functions. In other programming languages function objecs are sometimes called closures.

Functions can be converted to function objects and in many cases the compiler can do this conversion automatically.

We often use the term function for function objects as well, because it is usually clear from the context if a declared function or a function object is meant. However it has to be clear that functions and function objects are similar but different animals.

In this chapter we exclusively talk about function objects.

Function Type

The module function declares the type FUNCTION as the type of function objects.

-- file: function.ali
use
    predicate_logic
end

A: ANY
B: ANY

class
    FUNCTION[A,B]
inherit
    ghost ANY
end

The type FUNCTION[NATURAL,NATURAL] is the type of a function object which maps a natural number to a natural number.

By using tuples as the domain type it is possible to represent multiargument functions as well.

Since functions (aka function objects) are used very frequently in Albatross the type A->B can be used as a shorthand for FUNCTION[A,B]. The arrow operator is right associative so that A->B->C is parsed as A->(B->C) and represents the type FUNCTION[A,FUNCTION[B,C]] i.e. it represents a functions which maps an argument of type A to a function mapping an argument of type B to a value of type C.

Note that A->B->C and (A,B)->C are two different functions. The latter takes a tuple and maps it to a value of type C.

Equality of functions is not decidable. Therefore the type FUNCTION can inherit ANY only via a ghost inheritance relationship.

Function objects represent partial functions i.e. functions which might have preconditions. A total function is a special case of a partial function.

Basic Functions

The module function declares the following basic functions on function objects.

domain(f:A->B): ghost {A}
    -- The domain of the function 'f'

consistent(f,g:A->B): ghost BOOLEAN
        -- Do 'f' and 'g' have the same values on its common domain
    -> all(x) x in f.domain  ==>  x in g.domain  ==> f(x) = g(x)

(=) (f,g:A->B): ghost BOOLEAN
        -- Are the functions 'f' and 'g' equal?
    -> f.domain = g.domain and consistent(f,g)

All these functions are ghost functions because no algorithm is defined to compute their results.

Each function has a domain. The function (object) can be applied only to arguments in its domain. domain is a ghost function, i.e. it has to be proved that an argument is in the domain of a function in order to apply the function to the argument.

Two functions are consistent if they map arguments in their common domain to the same values.

Note that the expression all(x) f(x) = g(x) is an invalid expression because there is no guarantee that the functions f and g are applied to arguments in their domain. In the definition term of consistent the expression f(x) = g(x) is guarded by the two guards x in f.domain and x in g.domain and the lazy evaluation of ==> guarantees that f(x) = g(x) is evaluated only if the argument is in the corresponding domain.

Two functions are equal if the have the same domain are are consistent.

Function Expressions

Function objects are generated by function expressions. Type annotations are optional as long as the compiler can infer the type of the variable(s) and the return type.

Some examples of function expressions:

x -> x + 1

x:NATURAL -> x + 1

(x,y) -> x + y

(x,y:NATURAL): NATURAL -> x + y

agent(x)
    ensure
        -> x + 1
    end

agent(x:NATURAL):NATURAL
    ensure
        -> x + 1
    end

The general formats are

variable(s) -> expression

agent(variable(s)): optional_return_type
    require
        precondition_1
        precondition_2
    ensure
        -> expression
    end

The agent syntax allows to define function objects with preconditions.

Beta Reduction

Predicate and function expressions are very similar. They are expressed with a different syntax to allow more intuitive notations and to distighuish predicates which cannot have preconditions from functions which can have preconditions.

In both cases we have to declare a variable or a set of variables and an expression which calculates the result.

Function expressions like predicate expressions are equivalent to lambda expressions in lambda calculus. The Albatross compiler can do beta reductions with function expressions as well as shown in the following examples.

(x -> x + 1)(8*3)         ~>        8*3 + 1

((x,y) -> x * y)(a,7)     ~>        a * 7

Function Logic

The module function_logic uses function expressions to express more interesting things about functions.

E.g. we can define a function + so that f + (a,b) is the function f which has the same values as the function f except for a which maps to the value b. This function needs tuples (see chapter Tuple).

(+) (f:A->B, e:(A,B)): (A->B)
        -- The function 'f' except that it maps 'e.first' to e.second'.
    -> agent (a)
           require
               a = e.first or a in f.domain
           ensure
               -> if a = e.first then
                      e.second
                  else
                      f(a)
           end

Having this function it is possible to prove the theorems

all(f:A->B, a,x:A, b:B)
    ensure
         (f + (a,b))(a) = b

         x in f.domain ==> x /= a ==> (f + (a,b))(x) = f(x)
    end

The expression f|p should be the function f restricted to a domain whose arguments must be in f.domain and in p.

(|) (f:A->B, p:{A}): (A->B)
        -- The function 'f' whose domain is restricted to the arguments which are
        -- also in 'p'.
    -> agent (x)
           require
               x in f.domain
               x in p
           ensure
               -> f(x)
           end

The compiler can extract the domains of the resulting functions from the preconditions of the agent expressions.

(f + (a,b)).domain = {x: x = a or x in f.domain}

(f|p).domain       = {x: x in f.domain and x in p}

FUNCTION