2.7.6 Variable Freedom

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.

T9

([[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.

T10

[[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.

This document was generated on November 8, 2012 using texi2html 1.82.