txlyre
/
avram


			
							123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166
							<!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.3 A Minimal Set of Properties</title>

<meta name="description" content="avram - a virtual machine code interpreter: 2.7.3 A Minimal Set of Properties">
<meta name="keywords" content="avram - a virtual machine code interpreter: 2.7.3 A Minimal Set of Properties">
<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="A-Minimal-Set-of-Properties"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="On-Equality.html#On-Equality" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="A-Simple-Lisp-Like-Language.html#A-Simple-Lisp-Like-Language" 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="A-Minimal-Set-of-Properties-1"></a>
<h3 class="subsection">2.7.3 A Minimal Set of Properties</h3>

<p>For any trees <code><var>x</var></code>, <code><var>y</var></code>, and <code><var>k</var></code>, and any non-<code>nil</code>
trees <code><var>p</var></code>, <code><var>f</var></code>, and <code><var>g</var></code>, the new invisible operator satisfies these
conditions. In these expressions and hereafter, increasing abuse of
notation is perpetrated by not writing the <code>cons</code> in expressions of the form
<code>cons(<var>x</var>,<var>y</var>)</code>.
</p>
<dl compact="compact">
<dt> <em>P0</em></dt>
<dd><p><code>(nil,(nil,nil)) <var>x</var></code> = <code><var>x</var></code>
</p></dd>
<dt> <em>P1</em></dt>
<dd><p><code>(nil,((nil,nil),nil)) (<var>x</var>,<var>y</var>)</code> = <code><var>x</var></code>
</p></dd>
<dt> <em>P2</em></dt>
<dd><p><code>(nil,(nil,(nil,nil))) (<var>x</var>,<var>y</var>)</code> = <code><var>y</var></code>
</p></dd>
<dt> <em>P3</em></dt>
<dd><p><code>((nil,<var>k</var>),nil) <var>x</var></code> = <code><var>k</var></code>
</p></dd>
<dt> <em>P4</em></dt>
<dd><p><code>(((nil,(nil,nil)),nil),nil) (<var>f</var>,<var>x</var>)</code> = <code><var>f</var> (<var>f</var>,<var>x</var>)</code>
</p></dd>
<dt> <em>P5</em></dt>
<dd><p><code>((<var>f</var>,<var>g</var>),nil) <var>x</var></code> = <code><var>f</var> <var>g</var> <var>x</var></code>
</p></dd>
<dt> <em>P6</em></dt>
<dd><p><code>((<var>f</var>,nil),<var>g</var>) <var>x</var></code> = <code>(<var>f</var> <var>x</var>,<var>g</var> <var>x</var>)</code>
</p></dd>
<dt> <em>P7</em></dt>
<dd><p><code>((<var>p</var>,<var>f</var>),<var>g</var>) <var>x</var></code> = <code><var>f</var> <var>x</var></code> if
<code><var>p</var> <var>x</var></code>  is a non-<code>nil</code> tree,
but <code><var>g</var> <var>x</var></code> if <code><var>p</var> <var>x</var></code> = <code>nil</code>
</p></dd>
</dl>

<a name="index-properties"></a>
<a name="index-operator-properties"></a>
<p>Although other properties remain to be described, it is worth pausing at
this point because there is ample food for thought in the ones already
given. An obvious question would be that of their origin. The short
answer is that they have been chosen arbitrarily to be true by
definition of the operator. At best, the completion of the construction
may lead to a more satisfactory answer based on aesthetic or engineering
grounds.
</p>
<p>A more important question would be that of the relevance of the mystery
operator and its properties to the stated purpose of this section, which
is to specify the virtual machine code semantics. The answer lies in
that the operator induces a function for any given tree <code><var>t</var></code>,
such that the value returned by the function when given an argument
<var>x</var> is <code><var>t</var> <var>x</var></code>. This function is the one that is
implemented by the virtual code <var>t</var>, which is to say the way an
application will behave if we put <var>t</var> in its virtual code file. An
equivalent way of looking at the situation is that the virtual machine
does nothing but compute the result of this operator, taking the tree in
the virtual code file as its left operand and the input data as the
right operand. By knowing what the operator will do with a given pair of
operands, we know what to put into the virtual code file to get the
function we want.
</p>
<a name="index-universality"></a>
<a name="index-Turing-equivalence"></a>
<a name="index-exceptions-1"></a>
<a name="index-lists-4"></a>
<p>It is worthwhile to note that properties <em>P0</em> to <em>P7</em> are
sufficient for universality in the sense of Turing equivalence. That
means that any computable function could be implemented by the suitable
choice of a tree <var>t</var> without recourse to any other properties of the
operator. A compiler writer who finds this material boring could
therefore stop reading at this point and carry out the task of targeting
any general purpose programming language to the virtual machine based on
the specifications already given. However, such an implementation would
not take advantage of the features for list processing, exception
handling, or profiling that are also built into the virtual
machine and have yet to be described.
</p>
<hr size="1">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="On-Equality.html#On-Equality" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="A-Simple-Lisp-Like-Language.html#A-Simple-Lisp-Like-Language" 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>