# Ghost functions

Boolean expressions of the form

all(x:X) p(a,x) -- x is a bound variable, a is free within the expression some(x:X) p(a,x)

are not computable in general, even if the boolean valued function “p” is

computable. I.e. the following constructs are illegal in executable code.

-- Illegal if expression!!! if all(x:X) p(a,x) then exp1 else exp2 end -- Illegal function definition!!! f_illegal(a:A): BOOLEAN ensure Result = all(x:X) p(a,x) end

The compiler cannot accept these constructs because it is unable to generate

code to calculate the expression/function.

But a function like “f_illegal” could be very useful in assertions. Since

there is no need to have runtime code for assertions, the fact that

“f_illegal” is not computable does not disturb as long as it is a

mathematically meaningful function.

In order to make this possible, Modern Eiffel has ghost types.

T -- a normal type ghost T -- a ghost type

Objects of ghost type are called ghost objects. Ghost objects cannot flow into

real computations. But it is possible to inject ghost objects into

assertions.

A function which returns ghost objects is a ghost function. Ghost functions

can only be used in assertions.

With this we can define a legal version of “f_illegal”.

f_legal(a:A): ghost BOOLEAN ensure Result = all(x:X) p(a,x) end

Ghost functions can be combined arbitrarly. I.e. “f_legal” is a valid

definition, regardless whether “p” is a computable function or not.

Ghost functions are a powerful means to structure complicated assertions.

# Functions as objects

Functions are objects and can be passed around arbitrarily. I.e. functions can

be attached to local variables, passed as arguments and returned as results.

Function objects have a type. A function receiving as argument an object of

type A and returning an object of type R has the type A->R.

A->R -- function taking one argument [A,B,...]->R -- function taking many arguments []->R -- function with no argument, i.e. constant function ghost(A->R) -- a ghost function type A -> ghost R -- the same ghost function type f:A->R -- variable representing a function f[a] -- function "f" evaluated with the argument "a" g:[A,B]->R -- variable representing a function with two arguments g[a,b] -- function "g" evalutated with the arguments "a" and "b" h:[A,B]->[R,T] -- variable representing a function with two argumens -- returning two values

The function “g” is a function that maps a tuple of type [A,B] to R. But as

described in the last post “Tuples and functions”, sequences of expressions

and tuples with matching types can be used interchangeably.

Therefore the function “g” can be called with “g[a,b]” as if it were a

function with two arguments instead of “g[ [a,b] ]” which were necessary if

Modern Eiffel would not have this conversion between sequences of expressions

and tuple expressions.

# The module “function”

## The class FUNCTION

The type A->R inherits from the type FUNCTION[A,R]. The declaration of

FUNCIONT[A,R] is contained within a module “function” and looks like

-- file: function.e deferred class FUNCTION[A,R] inherit COMPARABLE end

The fact that the class FUNCTION has only two formal generics, one for the

argument and one for the return type, is no restriction. A and R can be

arbitrary tuples. Therefore any multiargument-multireturn function

[A,B]->[R,T] can be represented as FUNCTION[ [A,B], [R,T] ].

## Basic functions of the module “function”

The module “function” has the following basic functions

feature is_defined(f:CURRENT, a:A): ghost BOOLEAN -- Is the function `f' defined at argument `a'? deferred end is_total(f:CURRENT): ghost BOOLEAN -- Is the function `f' defined for all arguments? ensure Result = all(a:A) f.is_defined(a) end [] (f:CURRENT, a:A): B -- Value of function `f' at argument `a'. require f.is_defined(a) deferred end end

All functions in Modern Eiffel are potentially partial functions. The function

“is_defined” represents the precondition of the function “f” and returns

whether the function is defined at a certain argument.

The function “is_total” tells whether the function is defined for all possible

arguments.

The function “value” returns the value of the function at a certain argument.

Only the function “value” can be called in computations. The functions

“is_defined” and “is_total” are ghost functions and can be used only in

assertions.

The operator “[]” stands for function application. The value of the function

“f” at argument “a” is returned by “f[a]”.

Note: We leave the syntax of ISE Eiffel that all functions must have names and

can have an optional operator alias. In the following we treat operators as

first class feature names. I.e. the operator symbols “=”, “<=", "/", "and",

"not", "or", … are valid feature names for functions with one argument

(prefix operator) or two arguments (binary operator). The bracket operator

"[]" can have an arbitrary number of arguments. This convention is essentially

the same as the one used in the programming language Scala.

## Equality of functions

Mathematically functions are sets of key-value pairs. Therefore we say the two

functions “f” and “g” are equal if their sets of key-value pairs are equal.

Two sets “a” and “b” are equal if “a” is a subset of “b” and “b” is a subset

of “a”.

The following feature block in the module “function” codes these definitions

into Modern Eiffel.

feature -- equality is_contained(f,g:CURRENT): ghost BOOLEAN ensure Result = all(a:A) check f.is_defined(a) => g.is_defined(a) f.is_defined(a) => (f[a] = g[a]) end end = (f,g:CURRENT): ghost BOOLEAN ensure Result = (f.is_contained(g) and g.is_contained(a)) end is_strictly_contained(f,g:CURRENT): ghost BOOLEAN ensure Result = (f.is_contained(g) and f/=g) end end

## Properties of containment and equality

We expect containment to be reflexive, antisymmetric and transitive and

equality to be reflexive, symmetric and transitive. I.e. we expect the

following assertions to be true.

feature all(f,g,h:CURRENT) check reflexive: f.is_contained(f) antisymmetric: f.is_contained(g) => g.is_contained(f) => (f=g) transitive: f.is_contained(g) => g.is_contained(h) => f.is_contained(h) reflexive: f=f symmetric: (f=g) => (g=f) transitive: (f=g) => (g=h) => (f=h) end end

The proof engine of Modern Eiffel is able to proof these properties

automatically. The reader is encouraged to prove these assertions in order to

see that the proofs are straighforward.

## Parent class of FUNCTION

The above properties of “is_contained” and “=” satisfy the needed

properties for the type “PARTIALLY_ORDERED”. And indeed we can define the

class FUNCTION in the following manner.

deferred class FUNCTION[A,R] inherit ghost PARTIALLY_ORDERED rename is_less_equal as is_contained is_less as is_strictly_contained end end

Note that the parent type PARTIALLY_COMPARABLE must be inherited as a ghost

type because in the parent all functions are defined as computable

functions. Inheriting as ghost converts all functions inherited from the

parent to ghost functions.

This declaration of the class FUNCTION is highly recommendable because with

PARTIALLY_ORDERED as parent the module “function” inherits all proved

assertions of the parent class.

# Creation of function objects

## Convert functions into function objects

Any function can be converted to a function object. Having the function “func”

func(a:A,b:B):R require pre(a,b) ensure ... end

the following expressions are equivalent

func(a,b) -- call "func" directly local f:[A,B]->R := func -- create a function object and assign it to "f" then f[a,b] -- call the function object end

Note: While named functions like “func” are called in the usual manner with

parenthesized arguments, anonymous functions (i.e. function objects) are

called with the arguments provided in brackets.

The possibility gets interesting if we start to pass around function objects.

-- assume `gfunc' has the definition gfunc(f:[A,B]->R, x:X): T require ensure ... end -- then the following expression is valid gfunc(func,x)

## Create function objects from expressions

Any expression can be used to create a function object. Suppose we have an

expression “e” then “x->e” is a function which maps any argument to the value

of “e” with “x” replaced by the argument, i.e. “(x->e)[y]=e[x:=y]”.

-- general rule x->e (x->e)[y] = e[x:=y] -- some examples i->i+1 (i->i+1)[5] = 6 (i->i+1)[n+m] = (n+m)+1 i->(i+j)/k (i->(i+j)/k)[10] = (10+j)/k

In the expression “x->e” the variable “x” is a bound variable. It can be

renamed arbitrarly (but consistently on the left and the right hand side of

the arrow).

(x->e) = (y->e[x:=y]) (x->e) = (z->e[x:=z])

Some more possibilities to create function objects from expressions.

x:X->e -- explicitly typed argument [x,y,..]->e -- multiargument function [x:X,y:Y,...]->e -- multiargument function with explicitly typed arguments -- call of the function [x,y]->e ([x,y]->e)[a,b] = e[x,y:=a,b]

## Preconditions of function objects

All functions are potentially partial, i.e. they can have preconditions. The

preconditions are handed over to the function “is_defined” of the function

object.

In the above example the function “func(a:A,b:B):R” has the precondition

“pre(a,b)”. Therefore in the corresponding function object “f” the expression

“f.is_defined(a,b)” has the same value as “pre(a,b)”.

The same applies to function objects created from expressions. Any expression

“e” can have a set of preconditions “p1”, “p2”, …

e -- an expression p1,p2,... -- the precondition expressions of e (x->e).is_defined(y) = check (x->p1)[y], (x->p2)[y], ... end

Example

a/b -- e.g. division of natural numbers b/=0 -- precondition of "a/b" b->a/b -- function where the divisor is taken as the argument (b->a/b).is_defined(i) = (i/=0)