The virtual code semantics is easier to specify using the
silly language than it would be without it, but still awkward in
some cases. An example is the following declaration from the standard
library,
hired = compose(
compose,
couple(
constant compose,
compose(couple,couple(constant,constant couple))))
which is constructed in such a way as to imply the following theorem, provable by routine computation.
([[hired]] h) (f,g) = [[compose]](h,[[couple]](f,g))
Intuitively, hired represents a function that takes a given
function to a higher order function. For example, if f were a
function that adds two real numbers, hired f would be a function that
takes two real valued functions to their pointwise sum.
Apart from its cleverness, such an opaque way of defining a function has
little to recommend it. The statement of the theorem about the function
is more readable than the function definition itself, probably because
the theorem liberally employs mathematical variables, whereas the
silly language is variable free. On the other hand, it is not
worthwhile to linger over further enhancements to the language, such as
adding variables to it. The solution will be to indicate informally a
general method of inferring a variable free function definition from an
expression containing variables, and hereafter omit the more
cumbersome definitions.
An algorithm called isolate does the job.
The input to isolate is a pair (e,x), where
e is a syntactically correct silly expression in
which the identifier x may occur, but no other identifiers
dependent on x may occur (or else it's
garbage-in/garbage-out). Output is a syntactically correct silly
expression f in which the identifier x does
not occur, such that [[e]] = [[f x]].
The algorithm is as follows,
if e = x then
return identity
else if e is of the form (u,v)
return couple(isolate(u,x),isolate(v,x))
else if e is of the form u v
return (hired apply)(isolate(u,x),isolate(v,x))
else
return constant e
where equality is by literal comparison of expressions, and the
definition of apply is
apply = (hired meta)((hired compose)(left,constant right),right)
which represents a function that does the same thing as the invisible operator.
apply]] (f,x) = f x
The isolate algorithm can be generalized to functions of
arbitrarily many variables, but in this document we will need
only a unary and a binary version. The latter takes an expression
e and a pair of identifiers (x,y) as
input, and returns an expression f such that
[[e]] = [[f (x,y)]].
if e = x then
return left
else if e = y then
return right
else if e is of the form (u,v)
return couple(isolate(u,(x,y)),isolate(v,(x,y)))
else if e is of the form u v
return (hired apply)(isolate(u,(x,y)),isolate(v,(x,y)))
else
return constant e
It might be noted in passing that something similar to these algorithms
would be needed in a compiler targeted to avram if the source
were a functional language with variables.