| a map from one vector space to a vector space having the same field of scalars, with the properties that the map of the sum of two vectors is the sum of the maps of the vectors and the map of a scalar times a vector equals the scalar times the map of the vector. |
linear function
A recursive function is linear if it is of the form
f x = if p x then q x else h f x
where h is a "linear functional" which means that
(1) for all functions, a, b c and some function ht
h (if a then b else c) = if ht a then h b else h c
Function ht is known as the "predicate transformer" of h.
(2) If for some x,
h (\ y . bottom) x /= bottom
then
for all g, ht g x = True.
I.e. if h g x terminates despite g x not terminating then ht g x doesn't depend on g.
See also linear argument.
(1995-02-15)