Fonctions

TYPE function{$d: type, r: type}
  INHERIT equality{function{$d, r}}
  EXPORT Domain Range Total One_to_one Onto Strict Deterministic

  CONCEPT Domain(f: function{$d, r}) VALUE(s: sequence{type})
    -- The sequence of argument types for the function f.
    -- Example: MESSAGE(x: t1, y: t2) has domain [t1, t2].
    WHERE s = d

  CONCEPT Range(f: function{$d, r}) VALUE(t: type)
    -- The type of the value returned by the function
    -- in the normal case.
    WHERE s = r

  CONCEPT Total(f: function{$d, r}) VALUE(b: boolean)
    -- True if f is well defined for all values in its domain.
    WHERE ALL(s: sequence{any} SUCH THAT s IN d :: f($s) IN r )
    -- Improper values such as ! do not belong to any data type.

  CONCEPT One_to_one(f: function{$d, r}) VALUE(b: boolean)
    -- True if f has a unique value
    -- for every element of the domain h.
    WHERE ALL(s1 s2: sequence{any} SUCH THAT s1 IN d & s2 IN d 
              :: f($s1) = f($s2) => s1 = s2 )

  CONCEPT Onto(f: function{$d, r}) VALUE(b: boolean)
    -- True if the range of f covers the entire type r.
    WHERE ALL(y: r :: SOME(s: sequence{any} SUCH THAT
                           s IN d :: f($s) = y ))

  CONCEPT Strict(f: function{$d, r}) VALUE(b: boolean)
    -- True if the value of f is undefined
    -- whenever at least one input is undefined.
    WHERE ALL(s1 s2: sequence{any}, x: any SUCH THAT
              s1 || [x] || s2 IN d :: f($s1, !, $s2) = ! )

  CONCEPT Deterministic(f: function{$d, r}) VALUE(b: boolean)
    -- True if f is single-valued.
    WHERE ALL(s: sequence{any}, x y: r SUCH THAT
              s IN d :: x = f($s) & y = f($s) => x = y )
END