Functions, ghost functions and higher order functions

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)
Advertisements
  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: