txlyre
/
avram


			
							123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235
							<!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.5 How avram Thinks</title>

<meta name="description" content="avram - a virtual machine code interpreter: 2.7.5 How avram Thinks">
<meta name="keywords" content="avram - a virtual machine code interpreter: 2.7.5 How avram Thinks">
<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="How-avram-Thinks"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="Standard-Library.html#Standard-Library" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="Variable-Freedom.html#Variable-Freedom" 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="How-avram-Thinks-1"></a>
<h3 class="subsection">2.7.5 How <code>avram</code> Thinks</h3>

<p>The definitions in the standard <code>silly</code> library pertaining to the
basic properties of the operator can provide a good intuitive
illustration of how computations are performed by <code>avram</code>.  This
task is approached in the guise of a few trivial correctness proofs
about them. Conveniently, as an infeasibly small language, <code>silly</code>
is an ideal candidate for analysis by formal methods.
</p>
<p>Technically the semantic function [[&hellip;]] has not been defined on
identifiers, but we can easily extend it to them by stipulating that the
meaning of an identifier <code><var>x</var></code> is the meaning of the program
<a name="index-identifiers"></a>
<code><var>main</var> = <var>x</var></code> when linked with a library containing the
declaration of <code><var>x</var></code>, where <code><var>main</var></code> is an identifier
not appearing elsewhere in the library.
</p>
<p>With this idea in mind, the following &ldquo;theorems&rdquo; can be stated,
all of which have a similar proof. The variables <var>x</var> and <var>y</var>
stand for any tree, and the variable <var>f</var> stands for any tree other
than <code>nil</code>.
</p>
<dl compact="compact">
<dt> <em>T0</em></dt>
<dd><p>[[<code>identity</code>]] <code><var>x</var></code> = <code><var>x</var></code>
</p></dd>
<dt> <em>T1</em></dt>
<dd><p>[[<code>left</code>]] <code>(<var>x</var>,<var>y</var>)</code> = <code><var>x</var></code>
</p></dd>
<dt> <em>T2</em></dt>
<dd><p>[[<code>right</code>]] <code>(<var>x</var>,<var>y</var>)</code> = <code><var>y</var></code>
</p></dd>
<dt> <em>T4</em></dt>
<dd><p>[[<code>meta</code>]] <code>(<var>f</var>,<var>x</var>)</code> = <code><var>f</var> (<var>f</var>,<var>x</var>)</code>
</p></dd>
<dt> <em>T5</em></dt>
<dd><p>[[<code>constant_nil</code>]] <code><var>x</var></code> = <code>nil</code>
</p></dd>
</dl>

<p>Replacing each identifier with its defining expression directly
demonstrates a logical equivalence between the relevant theorem and one
of the basic operator properties postulated in <a href="A-Minimal-Set-of-Properties.html#A-Minimal-Set-of-Properties">A Minimal Set of Properties</a>.
</p>
<p>For more of a challenge, it is possible to prove the next theorem.
</p>
<dl compact="compact">
<dt> <em>T6</em></dt>
<dd><p>For non-<code>nil</code> <code><var>f</var></code> and <code><var>g</var></code>,
([[<code>couple</code>]] <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code> =
<code>(<var>f</var> <var>x</var>,<var>g</var> <var>x</var>)</code>
</p></dd>
</dl>

<p>The proof is a routine calculation. Beware of the distinction between
the mathematical <code>nil</code> and the <code>silly</code> identifier <code>nil</code>.
</p>
<table><tr><td>&nbsp;</td><td><pre class="format">
   ([[<code>couple</code>]] <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code> =  ([[<code>((((left,nil),constant_nil),nil),right)</code>]] <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code>

by substitution of <code>couple</code> with its definition in the standard library

   = (<code>((((</code>[[<code>left</code>]]<code>,</code>[[<code>nil</code>]]<code>),</code>[[<code>constant_nil</code>]]<code>),</code>[[<code>nil</code>]])<code>,</code>[[<code>right</code>]]<code>)</code> <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code>

by definition of the semantic function [[&hellip;]] regarding pairs

   = (<code>((((</code>[[<code>left</code>]]<code>,</code>[[<code>()</code>]]<code>),</code>[[<code>constant_nil</code>]]<code>),</code>[[<code>()</code>]])<code>,</code>[[<code>right</code>]]<code>)</code> <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code>

by substitution of <code>nil</code> from its definition in the standard library

   = (<code>((((</code>[[<code>left</code>]]<code>,</code><code>nil</code><code>),</code>[[<code>constant_nil</code>]]<code>),</code><code>nil</code>)<code>,</code>[[<code>right</code>]]<code>)</code> <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code>

by definition of the semantic function in the case of [[<code>()</code>]]

   = (<code>(</code>[[<code>left</code>]] <code>(<var>f</var>,<var>g</var>),</code>[[<code>constant_nil</code>]] <code>(<var>f</var>,<var>g</var>)),</code>[[<code>right</code>]] <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code>

by property <em>P6</em> (twice)

   = <code>((<var>f</var>,nil),<var>g</var>) <var>x</var></code>

by theorems <em>T1</em>, <em>T2</em>, and <em>T5</em>

   = <code>(<var>f</var> <var>x</var>,<var>g</var> <var>x</var>)</code>

by property <em>P6</em> again.
</pre></td></tr></table>


<p>Something to observe about this proof is that it might just as well have
been done automatically. Every step is either the substitution of an
identifier or a pattern match against existing theorems and properties
of the operator. Another thing to note is that the use of identifiers
and previously established theorems helps to make the proof human
readable, but is not a logical necessity. An equivalent proof could have
been expressed entirely in terms of the properties of the operator. If
one envisions a proof like this being performed blindly and
mechanically, without the running commentary or other amenities, that
would not be a bad way of thinking about what takes place when
<code>avram</code> executes virtual code.
</p>
<p>Three more theorems have similar proofs. For non-<code>nil</code>
trees <code><var>p</var></code>, <code><var>f</var></code> and <code><var>g</var></code>, and any trees
<code><var>x</var></code> and <code><var>k</var></code>:
<a name="index-compose-1"></a>
<a name="index-constant-1"></a>
<a name="index-conditional-1"></a>
</p>
<dl compact="compact">
<dt> <em>T7</em></dt>
<dd><p>([[<code>compose</code>]] <code>(<var>f</var>,<var>g</var>)</code>) <var>x</var> = <var>f</var> <var>g</var> <var>x</var>
</p></dd>
<dt> <em>T8</em></dt>
<dd><p>([[<code>constant</code>]] <code><var>k</var></code>) <var>x</var> = <var>k</var>
</p></dd>
<dt> <em>T9</em></dt>
<dd><p>([[<code>conditional</code>]] <code>(<var>p</var>,(<var>f</var>,<var>g</var>)</code>) <var>x</var> =
<code><var>f</var> <var>x</var></code> if
<code><var>p</var> <var>x</var></code>  is non-<code>nil</code>,
but <code><var>g</var> <var>x</var></code> if <code><var>p</var> <var>x</var></code> = <code>nil</code>
</p></dd>
</dl>

<p>The proofs of these theorems are routine calculations analogous to the
proof of <em>T6</em>. Here is a proof of theorem <em>T7</em> for good
measure.
</p><table><tr><td>&nbsp;</td><td><pre class="format">
   ([[<code>compose</code>]] <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code> = ([[<code>couple(identity,constant_nil)</code>]] <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code>
</pre></td></tr></table>
<p>by substitution of <code>compose</code> with its definition in the standard library
</p><table><tr><td>&nbsp;</td><td><pre class="format">
   = (<code>(</code>[[<code>couple</code>]] <code>(</code>[[<code>identity</code>]]<code>,</code>[[<code>constant_nil</code>]]<code>))(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code>

by definition of the semantic function

   = <code>(</code>[[<code>identity</code>]] <code>(<var>f</var>,<var>g</var>),</code>[[<code>constant_nil</code>]]<code> (<var>f</var>,<var>g</var>)) <var>x</var></code>

by theorem <em>T6</em>

   = <code>((<var>f</var>,<var>g</var>),nil) <var>x</var></code>

by theorems <em>T0</em> and <em>T5</em>

   = <code><var>f</var> <var>g</var> <var>x</var></code>

by property <em>P5</em> of the operator.
</pre></td></tr></table>

<hr size="1">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="Standard-Library.html#Standard-Library" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="Variable-Freedom.html#Variable-Freedom" 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>