txlyre
/
avram


			
							123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194
							<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
<html>
<!-- Created on November 8, 2012 by texi2html 1.82
texi2html was written by: 
            Lionel Cons <[email protected]> (original author)
            Karl Berry  <[email protected]>
            Olaf Bachmann <[email protected]>
            and many others.
Maintained by: Many creative people.
Send bugs and suggestions to <[email protected]>
-->
<head>
<title>avram - a virtual machine code interpreter: 2.7.6 Variable Freedom</title>

<meta name="description" content="avram - a virtual machine code interpreter: 2.7.6 Variable Freedom">
<meta name="keywords" content="avram - a virtual machine code interpreter: 2.7.6 Variable Freedom">
<meta name="resource-type" content="document">
<meta name="distribution" content="global">
<meta name="Generator" content="texi2html 1.82">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css">
<!--
a.summary-letter {text-decoration: none}
blockquote.smallquotation {font-size: smaller}
pre.display {font-family: serif}
pre.format {font-family: serif}
pre.menu-comment {font-family: serif}
pre.menu-preformatted {font-family: serif}
pre.smalldisplay {font-family: serif; font-size: smaller}
pre.smallexample {font-size: smaller}
pre.smallformat {font-family: serif; font-size: smaller}
pre.smalllisp {font-size: smaller}
span.roman {font-family:serif; font-weight:normal;}
span.sansserif {font-family:sans-serif; font-weight:normal;}
ul.toc {list-style: none}
-->
</style>


</head>

<body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">

<a name="Variable-Freedom"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="How-avram-Thinks.html#How-avram-Thinks" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="Metrics-and-Maintenance.html#Metrics-and-Maintenance" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="Virtual-Machine-Specification.html#Virtual-Machine-Specification" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="Virtual-Code-Semantics.html#Virtual-Code-Semantics" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="Library-Reference.html#Library-Reference" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="avram.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="avram_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="Function-Index.html#Function-Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="avram_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<hr size="1">
<a name="Variable-Freedom-1"></a>
<h3 class="subsection">2.7.6 Variable Freedom</h3>

<p>The virtual code semantics is easier to specify using the
<code>silly</code> language than it would be without it, but still awkward in
some cases. An example is the following declaration from the standard
library,
<a name="index-hired"></a>
</p>
<table><tr><td>&nbsp;</td><td><pre class="example">hired = compose(
   compose,
   couple(
      constant compose,
      compose(couple,couple(constant,constant couple))))
</pre></td></tr></table>

<p>which is constructed in such a way as to imply the following theorem,
provable by routine computation.
</p>
<dl compact="compact">
<dt> <em>T9</em></dt>
<dd><p><code>(</code>[[<code>hired</code>]] <code><var>h</var>) (<var>f</var>,<var>g</var>)</code> = [[<code>compose</code>]]<code>(<var>h</var>,</code>[[<code>couple</code>]]<code>(<var>f</var>,<var>g</var>))</code>
</p></dd>
</dl>

<p>Intuitively, <code>hired</code> represents a function that takes a given
function to a higher order function. For example, if <code>f</code> were a
function that adds two real numbers, <code>hired f</code> would be a function that
takes two real valued functions to their pointwise sum.
</p>
<p>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
<code>silly</code> 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.
</p>
<a name="index-isolate"></a>
<a name="index-variables"></a>
<p>An algorithm called <code>isolate</code> does the job.
The input to <code>isolate</code> is a pair <code>(<var>e</var>,<var>x</var>)</code>, where
<code><var>e</var></code> is a syntactically correct <code>silly</code> expression in
which the identifier <code><var>x</var></code> may occur, but no other identifiers
dependent on <code><var>x</var></code> may occur (or else it&rsquo;s
garbage-in/garbage-out).  Output is a syntactically correct <code>silly</code>
expression <code><var>f</var></code> in which the identifier <code><var>x</var></code> does
not occur, such that [[<code><var>e</var></code>]] = [[<code><var>f</var> <var>x</var></code>]].
The algorithm is as follows,
</p>
<table><tr><td>&nbsp;</td><td><pre class="display">
if <code><var>e</var></code> = <code><var>x</var></code> then
   return <code>identity</code>
else if <code><var>e</var></code> is of the form <code>(<var>u</var>,<var>v</var>)</code>
   return <code>couple(isolate(<var>u</var>,<var>x</var>),isolate(<var>v</var>,<var>x</var>))</code>
else if <code><var>e</var></code> is of the form <code><var>u</var> <var>v</var></code>
   return <code>(hired apply)(isolate(<var>u</var>,<var>x</var>),isolate(<var>v</var>,<var>x</var>))</code>
else
   return <code>constant <var>e</var></code>

</pre></td></tr></table>

<a name="index-equality-1"></a>
<p>where equality is by literal comparison of expressions, and the
definition of <code>apply</code> is
<a name="index-apply"></a>
</p>
<table><tr><td>&nbsp;</td><td><pre class="example">apply = (hired meta)((hired compose)(left,constant right),right)
</pre></td></tr></table>

<p>which represents a function that does the same thing as the invisible
operator.
</p>
<dl compact="compact">
<dt> <em>T10</em></dt>
<dd><p>[[<code>apply</code>]] <code>(<var>f</var>,<var>x</var>)</code> = <code><var>f</var> <var>x</var></code>
</p></dd>
</dl>

<p>The <code>isolate</code> 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
<code><var>e</var></code> and a pair of identifiers <code>(<var>x</var>,<var>y</var>)</code> as
input, and returns an expression <code><var>f</var></code> such that
[[<code><var>e</var></code>]] = [[<code><var>f</var> (<var>x</var>,<var>y</var>)</code>]].
</p>
<table><tr><td>&nbsp;</td><td><pre class="display">
if <code><var>e</var></code> = <code><var>x</var></code> then
   return <code>left</code>
else if <code><var>e</var></code> = <code><var>y</var></code> then
   return <code>right</code>
else if <code><var>e</var></code> is of the form <code>(<var>u</var>,<var>v</var>)</code>
   return <code>couple(isolate(<var>u</var>,(<var>x</var>,<var>y</var>)),isolate(<var>v</var>,(<var>x</var>,<var>y</var>)))</code>
else if <code><var>e</var></code> is of the form <code><var>u</var> <var>v</var></code>
   return <code>(hired apply)(isolate(<var>u</var>,(<var>x</var>,<var>y</var>)),isolate(<var>v</var>,(<var>x</var>,<var>y</var>)))</code>
else
   return <code>constant <var>e</var></code>

</pre></td></tr></table>

<p>It might be noted in passing that something similar to these algorithms
would be needed in a compiler targeted to <code>avram</code> if the source
were a functional language with variables.
</p>
<hr size="1">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="How-avram-Thinks.html#How-avram-Thinks" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="Metrics-and-Maintenance.html#Metrics-and-Maintenance" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="Virtual-Machine-Specification.html#Virtual-Machine-Specification" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="Virtual-Code-Semantics.html#Virtual-Code-Semantics" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="Library-Reference.html#Library-Reference" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="avram.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="avram_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="Function-Index.html#Function-Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="avram_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<p>
 <font size="-1">
  This document was generated on <i>November 8, 2012</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
 </font>
 <br>

</p>
</body>
</html>