[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

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

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

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