How-avram-Thinks.html 12 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235
  1. <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
  2. <html>
  3. <!-- Created on November 8, 2012 by texi2html 1.82
  4. texi2html was written by:
  5. Lionel Cons <[email protected]> (original author)
  6. Karl Berry <[email protected]>
  7. Olaf Bachmann <[email protected]>
  8. and many others.
  9. Maintained by: Many creative people.
  10. Send bugs and suggestions to <[email protected]>
  11. -->
  12. <head>
  13. <title>avram - a virtual machine code interpreter: 2.7.5 How avram Thinks</title>
  14. <meta name="description" content="avram - a virtual machine code interpreter: 2.7.5 How avram Thinks">
  15. <meta name="keywords" content="avram - a virtual machine code interpreter: 2.7.5 How avram Thinks">
  16. <meta name="resource-type" content="document">
  17. <meta name="distribution" content="global">
  18. <meta name="Generator" content="texi2html 1.82">
  19. <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  20. <style type="text/css">
  21. <!--
  22. a.summary-letter {text-decoration: none}
  23. blockquote.smallquotation {font-size: smaller}
  24. pre.display {font-family: serif}
  25. pre.format {font-family: serif}
  26. pre.menu-comment {font-family: serif}
  27. pre.menu-preformatted {font-family: serif}
  28. pre.smalldisplay {font-family: serif; font-size: smaller}
  29. pre.smallexample {font-size: smaller}
  30. pre.smallformat {font-family: serif; font-size: smaller}
  31. pre.smalllisp {font-size: smaller}
  32. span.roman {font-family:serif; font-weight:normal;}
  33. span.sansserif {font-family:sans-serif; font-weight:normal;}
  34. ul.toc {list-style: none}
  35. -->
  36. </style>
  37. </head>
  38. <body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
  39. <a name="How-avram-Thinks"></a>
  40. <table cellpadding="1" cellspacing="1" border="0">
  41. <tr><td valign="middle" align="left">[<a href="Standard-Library.html#Standard-Library" title="Previous section in reading order"> &lt; </a>]</td>
  42. <td valign="middle" align="left">[<a href="Variable-Freedom.html#Variable-Freedom" title="Next section in reading order"> &gt; </a>]</td>
  43. <td valign="middle" align="left"> &nbsp; </td>
  44. <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>
  45. <td valign="middle" align="left">[<a href="Virtual-Code-Semantics.html#Virtual-Code-Semantics" title="Up section"> Up </a>]</td>
  46. <td valign="middle" align="left">[<a href="Library-Reference.html#Library-Reference" title="Next chapter"> &gt;&gt; </a>]</td>
  47. <td valign="middle" align="left"> &nbsp; </td>
  48. <td valign="middle" align="left"> &nbsp; </td>
  49. <td valign="middle" align="left"> &nbsp; </td>
  50. <td valign="middle" align="left"> &nbsp; </td>
  51. <td valign="middle" align="left">[<a href="avram.html#Top" title="Cover (top) of document">Top</a>]</td>
  52. <td valign="middle" align="left">[<a href="avram_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
  53. <td valign="middle" align="left">[<a href="Function-Index.html#Function-Index" title="Index">Index</a>]</td>
  54. <td valign="middle" align="left">[<a href="avram_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
  55. </tr></table>
  56. <hr size="1">
  57. <a name="How-avram-Thinks-1"></a>
  58. <h3 class="subsection">2.7.5 How <code>avram</code> Thinks</h3>
  59. <p>The definitions in the standard <code>silly</code> library pertaining to the
  60. basic properties of the operator can provide a good intuitive
  61. illustration of how computations are performed by <code>avram</code>. This
  62. task is approached in the guise of a few trivial correctness proofs
  63. about them. Conveniently, as an infeasibly small language, <code>silly</code>
  64. is an ideal candidate for analysis by formal methods.
  65. </p>
  66. <p>Technically the semantic function [[&hellip;]] has not been defined on
  67. identifiers, but we can easily extend it to them by stipulating that the
  68. meaning of an identifier <code><var>x</var></code> is the meaning of the program
  69. <a name="index-identifiers"></a>
  70. <code><var>main</var> = <var>x</var></code> when linked with a library containing the
  71. declaration of <code><var>x</var></code>, where <code><var>main</var></code> is an identifier
  72. not appearing elsewhere in the library.
  73. </p>
  74. <p>With this idea in mind, the following &ldquo;theorems&rdquo; can be stated,
  75. all of which have a similar proof. The variables <var>x</var> and <var>y</var>
  76. stand for any tree, and the variable <var>f</var> stands for any tree other
  77. than <code>nil</code>.
  78. </p>
  79. <dl compact="compact">
  80. <dt> <em>T0</em></dt>
  81. <dd><p>[[<code>identity</code>]] <code><var>x</var></code> = <code><var>x</var></code>
  82. </p></dd>
  83. <dt> <em>T1</em></dt>
  84. <dd><p>[[<code>left</code>]] <code>(<var>x</var>,<var>y</var>)</code> = <code><var>x</var></code>
  85. </p></dd>
  86. <dt> <em>T2</em></dt>
  87. <dd><p>[[<code>right</code>]] <code>(<var>x</var>,<var>y</var>)</code> = <code><var>y</var></code>
  88. </p></dd>
  89. <dt> <em>T4</em></dt>
  90. <dd><p>[[<code>meta</code>]] <code>(<var>f</var>,<var>x</var>)</code> = <code><var>f</var> (<var>f</var>,<var>x</var>)</code>
  91. </p></dd>
  92. <dt> <em>T5</em></dt>
  93. <dd><p>[[<code>constant_nil</code>]] <code><var>x</var></code> = <code>nil</code>
  94. </p></dd>
  95. </dl>
  96. <p>Replacing each identifier with its defining expression directly
  97. demonstrates a logical equivalence between the relevant theorem and one
  98. 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>.
  99. </p>
  100. <p>For more of a challenge, it is possible to prove the next theorem.
  101. </p>
  102. <dl compact="compact">
  103. <dt> <em>T6</em></dt>
  104. <dd><p>For non-<code>nil</code> <code><var>f</var></code> and <code><var>g</var></code>,
  105. ([[<code>couple</code>]] <code>(<var>f</var>,<var>g</var>)</code>) <code><var>x</var></code> =
  106. <code>(<var>f</var> <var>x</var>,<var>g</var> <var>x</var>)</code>
  107. </p></dd>
  108. </dl>
  109. <p>The proof is a routine calculation. Beware of the distinction between
  110. the mathematical <code>nil</code> and the <code>silly</code> identifier <code>nil</code>.
  111. </p>
  112. <table><tr><td>&nbsp;</td><td><pre class="format">
  113. ([[<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>
  114. by substitution of <code>couple</code> with its definition in the standard library
  115. = (<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>
  116. by definition of the semantic function [[&hellip;]] regarding pairs
  117. = (<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>
  118. by substitution of <code>nil</code> from its definition in the standard library
  119. = (<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>
  120. by definition of the semantic function in the case of [[<code>()</code>]]
  121. = (<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>
  122. by property <em>P6</em> (twice)
  123. = <code>((<var>f</var>,nil),<var>g</var>) <var>x</var></code>
  124. by theorems <em>T1</em>, <em>T2</em>, and <em>T5</em>
  125. = <code>(<var>f</var> <var>x</var>,<var>g</var> <var>x</var>)</code>
  126. by property <em>P6</em> again.
  127. </pre></td></tr></table>
  128. <p>Something to observe about this proof is that it might just as well have
  129. been done automatically. Every step is either the substitution of an
  130. identifier or a pattern match against existing theorems and properties
  131. of the operator. Another thing to note is that the use of identifiers
  132. and previously established theorems helps to make the proof human
  133. readable, but is not a logical necessity. An equivalent proof could have
  134. been expressed entirely in terms of the properties of the operator. If
  135. one envisions a proof like this being performed blindly and
  136. mechanically, without the running commentary or other amenities, that
  137. would not be a bad way of thinking about what takes place when
  138. <code>avram</code> executes virtual code.
  139. </p>
  140. <p>Three more theorems have similar proofs. For non-<code>nil</code>
  141. trees <code><var>p</var></code>, <code><var>f</var></code> and <code><var>g</var></code>, and any trees
  142. <code><var>x</var></code> and <code><var>k</var></code>:
  143. <a name="index-compose-1"></a>
  144. <a name="index-constant-1"></a>
  145. <a name="index-conditional-1"></a>
  146. </p>
  147. <dl compact="compact">
  148. <dt> <em>T7</em></dt>
  149. <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>
  150. </p></dd>
  151. <dt> <em>T8</em></dt>
  152. <dd><p>([[<code>constant</code>]] <code><var>k</var></code>) <var>x</var> = <var>k</var>
  153. </p></dd>
  154. <dt> <em>T9</em></dt>
  155. <dd><p>([[<code>conditional</code>]] <code>(<var>p</var>,(<var>f</var>,<var>g</var>)</code>) <var>x</var> =
  156. <code><var>f</var> <var>x</var></code> if
  157. <code><var>p</var> <var>x</var></code> is non-<code>nil</code>,
  158. but <code><var>g</var> <var>x</var></code> if <code><var>p</var> <var>x</var></code> = <code>nil</code>
  159. </p></dd>
  160. </dl>
  161. <p>The proofs of these theorems are routine calculations analogous to the
  162. proof of <em>T6</em>. Here is a proof of theorem <em>T7</em> for good
  163. measure.
  164. </p><table><tr><td>&nbsp;</td><td><pre class="format">
  165. ([[<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>
  166. </pre></td></tr></table>
  167. <p>by substitution of <code>compose</code> with its definition in the standard library
  168. </p><table><tr><td>&nbsp;</td><td><pre class="format">
  169. = (<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>
  170. by definition of the semantic function
  171. = <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>
  172. by theorem <em>T6</em>
  173. = <code>((<var>f</var>,<var>g</var>),nil) <var>x</var></code>
  174. by theorems <em>T0</em> and <em>T5</em>
  175. = <code><var>f</var> <var>g</var> <var>x</var></code>
  176. by property <em>P5</em> of the operator.
  177. </pre></td></tr></table>
  178. <hr size="1">
  179. <table cellpadding="1" cellspacing="1" border="0">
  180. <tr><td valign="middle" align="left">[<a href="Standard-Library.html#Standard-Library" title="Previous section in reading order"> &lt; </a>]</td>
  181. <td valign="middle" align="left">[<a href="Variable-Freedom.html#Variable-Freedom" title="Next section in reading order"> &gt; </a>]</td>
  182. <td valign="middle" align="left"> &nbsp; </td>
  183. <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>
  184. <td valign="middle" align="left">[<a href="Virtual-Code-Semantics.html#Virtual-Code-Semantics" title="Up section"> Up </a>]</td>
  185. <td valign="middle" align="left">[<a href="Library-Reference.html#Library-Reference" title="Next chapter"> &gt;&gt; </a>]</td>
  186. <td valign="middle" align="left"> &nbsp; </td>
  187. <td valign="middle" align="left"> &nbsp; </td>
  188. <td valign="middle" align="left"> &nbsp; </td>
  189. <td valign="middle" align="left"> &nbsp; </td>
  190. <td valign="middle" align="left">[<a href="avram.html#Top" title="Cover (top) of document">Top</a>]</td>
  191. <td valign="middle" align="left">[<a href="avram_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
  192. <td valign="middle" align="left">[<a href="Function-Index.html#Function-Index" title="Index">Index</a>]</td>
  193. <td valign="middle" align="left">[<a href="avram_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
  194. </tr></table>
  195. <p>
  196. <font size="-1">
  197. This document was generated on <i>November 8, 2012</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  198. </font>
  199. <br>
  200. </p>
  201. </body>
  202. </html>