Function-variable-instantiation
Notion of function variable instantiation.
A function variable instantiation is
an alist
((fvar1 . fun1) ... (fvarN . funN))
where N is a non-negative integer,
fvar1, ..., fvarN are distinct
function variables,
and fun1, ..., funN are named functions
such that each funI has the same arity as
the corresponding fvarI.
The funI functions may be
function variables,
second-order functions,
or ``regular'' first-order functions.
An instantiation as above is applied
to a term term
by replacing each fvarI with funI.
This involves not only explicit occurrences of fvarI,
but also implicit occurrences as function variables upon which
second-order functions occurring in term depend on.
For the latter kind of occurrences,
suitable
instances
of such second-order functions must exist;
if they do not exist, the application of the instantiation fails.
Examples
Example 1
Given
(defunvar ?f (*) => *)
(defunvar ?g (*) => *)
(defun2 h[?f] (x) ...)
(defun2 k[?f] (x) ...)
(defun-inst h[consp] (h[?f] (?f . consp)))
the alist ((?f . consp) (?g . k[?f])) is an instantiation,
and the result of applying it to the term (h[?f] (?g a))
is the term (h[consp] (k[?f] a)).
